17

The quick summary is that LTL with only past and no future modalities defines properties expressed over finite-words and these are the star-free subset of the regular languages. Standard LTL when extended with past-time modalities does not have more logical expressive power than LTL with only future modalities but properties can be defined in an ...


9

There are already some rather good related answers regarding LTL versus CTL. In a nutshell, LTL is first and foremost a logic of traces, and an LTL formula is true for a transition system $S$ if and only if it is true for each trace of $S$. CTL, on the other hand, is a branching-time logic, which can in a sense talk about multiple paths at the same time. ...


7

The logics are expressively the same, though past operators make LTL exponentially more succinct. You can start here, from which there are references.


5

Your first question is answered in this paper: https://www.cs.cornell.edu/fbs/publications/RecSafeLive.pdf Given an LTL formula, translate it into a Büchi automaton, and remove states that have no path to an accepting state. Then, change all states to be accepting. If the language of the automaton does not change, then the property is a safety property. ...


5

As mentioned in the comments, the translation is shown in: Volker Diekert and Paul Gastin. "First-order definable languages." (2008) http://www.lsv.fr/Publis/PAPERS/PDF/DG-WT08.pdf And it goes via a characterization of $LTL$ as $FO[<]$.


4

Sorry to provide the same answer as for this question, but this was proved in [1, Theorem 3.1]. [1] J. Cohen, D. Perrin and J.-É. Pin, On the expressive power of temporal logic for finite words, J. Comput. System Sci. 46 (1993), 271-294.


4

An algebraic characterisation of the restricted temporal logic (fragment using only next and eventually, but not until) is given in [1]. The expressive power of this fragment is the set of regular languages whose syntactic monoid are locally $\cal L$-trivial. I am not sure of the result you are looking for, but this article probably contains enough material ...


4

In general, we look at fixed-points of monotone functions over lattices, i.e. with some partial ordering over your elements. If your lattice is complete (it has a least and greatest element, called a bottom $(\bot)$ and a top $(\top)$), and the function whose fixed-point you're trying to find is monotone, then the Knaster-Tarski Theorem says that a fixed-...


3

Yes. The automata in question are often called "Looping" automata (so you have a keyword to start from). A possible starting point is the following paper: https://faculty.idc.ac.il/udiboker/files/MullerAutomata.pdf A looping automaton can be described as $\left<Q,\Sigma,\delta,Q_0\right>$ where the components are states, alphabet, transition ...


3

The "probabilistic" element in probabilistic model checking is that the system being checked is probabilistic, not that we add probabilities to an existing deterministic or non-deterministic system. Thus, what you are checking is whether a probabilistic system satisfies some property. For example "is it true that with probability at least 0.5, the system ...


3

The answer was buried in a small section of the same paper that I was citing. Adding past operators to TPTL, in contrast of what happens with LTL, causes a huge increase in complexity as the satisfiability problem becomes non-elementary. The fact is proven in the paper by showing how a mixture of future and past operators, combined with the freeze ...


2

The question you ask is more complex than it seems. ITLs have been defined in different ways and fashions, and the answer depends on the particular definition and the particular semantics. To get an intuition, you have to decide first if points are to be considered special intervals or excluded by the semantics; the second choice is more common, and it makes ...


2

I am not sure what you are referring to when you say "this is not covered in theory in general." The specific example that you give has been studied and is called antecedent failure. Formally verifying a microprocessor using a simulation methodology., D. L. Beatty and R. L. Bryant, 1994 One of the principal dangers of formal verification is what we ...


2

The statement $\langle M,i\rangle\models \varphi$ for all $i\in \mathbb{N}$ is equivalent to $\langle M,0\rangle\models G\varphi$. Thus, you can check the latter.


2

Pierre Wolper defined in 1983 extended temporal logic (ETL, in Information and Computation 56, 72–99, doi:10.1016/S0019-9958(83)80051-5), where a temporal operator $\mathcal A(\varphi_1,\dots,\varphi_n)$ can be introduced for a finite-state automaton $\mathcal A$. The formula is satisfied in an infinite word $u$ at position $i$, i.e. $u,i\models\mathcal A(\...


2

The "equally expressive" statement means that if a formula of PLTL is a statement about the future, i.e. if it's evaluated at the first instant $0$ of the time domain $\mathbb N$, then there exists an equivalent LTL formula. This means that nesting future and past operators is not more expressive than nesting just future operators, as long as the global ...


2

The important thing to notice is that in finite transition systems, two systems $K_1,K_2$ over an alphabet $\Sigma$ are not trace equivalent (for infinite traces) if and only if there exists a finite trace $w\in \Sigma^*$ that is in one of them, but not the other. Indeed, if $K_1$ and $K_2$ are not trace equivalent, denoted $L(K_1)\neq L(K_2)$, then w.l.o.g. ...


2

Your translation goes into Presburger arithmetic, which is decidable. You could take your translated formula, do quantifier elimination on it, and then hand it over to a proof-producing SMT solver. Since pretty much all SMT solvers are (fancy extensions of) DPLL, I would guess you can turn those proofs into resolution proofs without too much difficulty. ...


2

I'm not sure whether it would work in your case, but in order to show succinctness results in modal/temporal logic (e.g. the fact the two-variable logic over words in exponentially more succinct than unary temporal logic) one can employ formula size games or Adler-Immerman games. Probably the most recent paper to read is by Lauri Hella and Miikka Vilander. ...


1

Your question is formally the same as this one: how many symbols $X$ are needed to write the polynomial $XX + XXXX + XXXXXX = XX(1 + XX(1 + XX))$? Well, you obtained $6$ as an upper bound. It is also a lower bound because any expression involving less than $6$ symbols $X$ would define a polynomial of degree $< 6$. For the general case, I would not be ...


1

Note that by "equivalent", we actually need to interpret LTL over trees. Thus, we say that a CTL formula $\phi$ is equivalent to an LTL formula $\psi$, if $\phi$ is equivalent to the CTL* formula $A\psi$. Thus, we essentially compare LTL and CTL in the common grounds of CTL*. Given this, it's not hard to construct a procedure to check the equivalent. ...


1

This question should (and will) probably be migrated to cs.se. In the meantime, consider the computation tree of the depicted structure: in almost all paths, $p$ is seen only finitely often, making the premise of $GFp\to GFq$ false, so the formula is satisfied there. However, there is one path, namely $s_0^\omega$, in which $GFp$ does hold, but in this path ...


1

I think it depends on what you mean by linear-time temporal logics. If you mean temporal logics that have linear time semantics (i.e. cannot distinguish more than trace equivalence, a la van Glabbeek) then there are indeed logics that require counter examples that are not just lassos. HyperLTL is an example: https://www.react.uni-saarland.de/publications/...


1

To answer your second question: there is one property that is both safety and liveness: True. With this exception, however, it is fair to say that a property is either safety or liveness or neither. "Most" properties (like yours) are actually neither, but every property can be represented by the intersection of a safety and a liveness property. I think ...


1

A good starting point for practical LTL examples is LILY, as well as the PROSYD project. They provide some examples for LTL formulas, both "toy examples" and real-life applications. I think the website for the Prosyd project is a bit dead. By the way, your interpretation of the formula $P\to \Diamond Q$ is not exactly correct. First of all, it is not a ...


1

There were a lot of publication on extending and or formalizing RBAC/SOD with LTL or other flavors of temporal logics, not sure of other AC models. Google Scholar (or simple google) search with yield a bunch of articles. Most of them might be not sufficiently formal for somebody like yourself, yet might be of some interest. Not sure is LTL the best way. Yet ...


Only top voted, non community-wiki answers of a minimum length are eligible