16
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 ...
11
Take a path property that is not first-order expressible, e.g.
$$\nu x.p\wedge\Diamond\Diamond x$$
which says that there exists a path where the atomic proposition $p$ holds at every even position, and any valuation can be used on odd positions.
8
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.
6
The formula in your statement
Obviously E(A(F1)) with F1=E(A(F1)) is not well-defined for some Büchi automata. So what does inductively defined exactly mean in this case?
cannot arise if you built ECTL* inductively. This means, in standard academic parlance, we would present a syntax definition of the form below.
Let $Prop$ be a set of propositions and $...
6
Expanding on Markus' answer a bit, note that the alphabet $\Sigma$ is in turn the powerset $2^{Prop}$ of the set $Prop=\{p_1,\dots,p_k\}$ of atomic propositions, i.e. it represents the set of valuations $a:Prop\to\{T,F\}$ of the $p_i$.
In the LTL formula, most boolean subformulas involve only a few of the propositions. In the translation, any such ...
5
I think the key problem here is not understanding how inductive definitions of syntax work. Here are three approaches to understanding what a BNF grammar means.
Consider a simple grammar:
$$ t ::= \mathtt{true} ~~|~~ \mathtt{false} ~~|~~ 0 ~~|~~ \mathtt{succ}\ t ~~|~~ \mathtt{if}\ t\ \mathtt{then}\ t\ \mathtt{else}\ t$$
Following Pierce's Types and ...
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-...
4
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. ...
4
I think the simpler example is your property, which can be written for instance $E(((a+b)a)^\omega))$.
A simple way to show that is is not in CTL* is to show that this would imply that the word language $((a+b)a)^\omega$ is in LTL (because CTL* on linear structures is LTL).
This fact is a classical result.
To show it, it suffices (for instance) to use the ...
4
I only had a quick look at the paper, but it sounds as if they mean the following. If there are two transitions from state $s_1$ to state $s_2$ with different labels $a$ and $b$, they "group" them into one transition with label $\{a,b\}$. However, they write that they interpret the set in such a way that the resulting automaton still accepts the same words ...
3
Safety properties are closed under finite intersection. This can be seen by following Alpern and Schneider's characterisation which showed that safety properties are limit-closed when viewed topologically.
Liveness properties as defined by Alpern and Schneider are dense. They are not closed under intersection as soon as there are two elements in the state ...
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 ...
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
Intuitively, what happens here is that for $AFGp$, you check each individual path for whether after some point, $p$ will always be true - no matter what other choices are available in a given state.
In particular, for the path which always stays in the first state, this is true even though a $\neg p$-state is reachable. On all other paths it is true because ...
3
One thing we have to be clear on is the kind of property we are talking about: CTL and CTL* are branching-time logics, used to talk about tree languages, whereas LTL is a linear-time logic, which per se talks about words, but can be applied to trees by requiring all branches to satisfy the formula.
This already gives you a hint for some CTL properties ...
3
I'm not answering the full question but only part of it (I have no interest in branching time).
Your definition of $\mathit{even}$ would better read $\mathit{even}(p) \equiv \exists q.(q \land \Box ( q \leftrightarrow \mathsf{X} \lnot q ) \land \Box ( q \rightarrow p ))$. You are introducing $q$ only to remember if you are on an odd or even position, but ...
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
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 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
Your construction for bad prefixes is not correct on NBA's.
For instance take the NBA on alphabet $A=\{a,b\}$ with two initial states $q_a$ and $q_b$ where for both $x\in A$, $q_x$ goes to an accepting sink if the first letter is $x$ and to a rejecting sink if the first letter is not $x$.
Then the language recognized is $A^\omega$, but the set of "bad ...
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
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.
...
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
Maybe take a look at http://www.syntcomp.org/
This is a competition of tools solving the LTL synthesis problem (and some related problems).
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
See Venema, Yde. Temporal Logic. The blackwell guide to Philosophical Logic.
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
The paper mentions in the preliminaries that it encodes Allen Interval temporal logic into the FG-fragment of LTL (which only has the "globally" and "eventually" modalities). Full LTL is strictly more expressive (e.g., consider the formula a U b) and thus cannot be encoded in Allen Interval temporal logic.
1
More along the "related formalisms" direction.
PDL with intersection and converse: satisfiability and infinite-state model checking, Stefan Göller, Markus Lohrey, and Carsten Lutz, 2009
The Effects of Bounding Syntactic Resources on Presburger LTL, Stéphane Demri and Régis Gascon
The introduction section of the first paper has an extensive discussion of ...
Only top voted, non community-wiki answers of a minimum length are eligible
