6
votes
LTL to automaton translation that can only read disjunctions of labels per transition
The models of an LTL formula $\varphi$, with atomic propositions $P$, are infinite words $w = \sigma_0\sigma_1\ldots$, where each $\sigma_i$ is a subset of $P$. To recognize such words, the edges of ...
- 134
5
votes
Linear Temporal Logic (LTL) Syntax Infinitely Often
Consider just $Fx$. It means that at some point in time, say $t_k$, from the perspective of current moment $t_0$, $x$ will be true. After this moment, $x$ may never again be true. Specificaly, at the ...
- 1,191
5
votes
Linear Temporal Logic with non-Boolean propositions (e.g. Integers)?
There has been some relatively recent work on constructive/intuitionistic variants or interpretations of LTL.
Kojima's and Igarashi's Constructive Linear-Time Temporal Logic: Proof Systems and Kripke ...
5
votes
Accepted
Equivalence rules for LTL - Getting stuck working with $ \square \lozenge $ & Until ($\textsf{ U}$ ) operators
In order to prove the equivalence of two formulas $\phi,\psi$, it is enough to show that for every computation $\pi$, it holds that $\pi\models \phi$ iff $\pi\models \psi$. This is semantic ...
- 17k
5
votes
Accepted
Is model checking PSpace-hard *in formula size*?
You are certainly right that the level of rigor found in old papers making such claims can be a bit low at times when viewed from today's perspective.
The claim is correct anyway, even if it does not ...
- 2,732
4
votes
What does "AF AX p" mean in CTL?
Your understanding of $AF AX p$ is correct (in my opinion). But whether it seems particularly strange or hard to understand is rather subjective. The argument you quote compares the expressiveness or ...
- 9,501
4
votes
Equivalence rules for LTL - Getting stuck working with $ \square \lozenge $ & Until ($\textsf{ U}$ ) operators
\begin{alignat*}{2}
\Box \varphi \to \Diamond q
&\equiv \neg \Box \varphi \lor \Diamond \psi &&\text{($\to$ elim)}\\
&\equiv \Diamond \neg \varphi \lor \Diamond \psi &&\text{(...
- 41
4
votes
Minimal Deterministic Buchi Automata Product
This is only a partial answer (as I believe that the state of the art is insufficient to answer your questions completely - I am happy to be proven wrong here), but I hope that it helps you anyway.
...
- 2,732
4
votes
Accepted
What kind of LTL formula can be represented by DBAs
You can define syntactic fragments of LTL that ensure that all properties expressible in these fragments are representable as DBAs. An example is given in the paper "A LTL Fragment for GR(1)-Synthesis"...
- 2,732
4
votes
Accepted
How to express the existence of winning strategy of the starter of a game in temporal logic?
I don't think it's possible in CTL nor LTL to model two competing players.
You would probably need ATL (Alternating-time Temporal Logic). In ATL, the formula $\langle\langle A \rangle\rangle \phi$ ...
- 15.5k
4
votes
Validity of □(P→ Q) → (◊P → ◊Q) in linear temporal logic
Think about what the formula means. The first part says that it's always true that $P$ implies $Q$; the second part says that, if $P$ is true somewhere, then $Q$ must be true ...
- 81.4k
4
votes
Accepted
Büchi automaton to Linear Temporal Logic
Since Büchi automata are strictly more expressive than LTL, such a translation is not possible in the general case.
For instance, the language $L = \{w_0 w_1 w_2 \ldots \in (2^{\{a\}})^\omega \mid \...
- 2,732
3
votes
Why is LTL Model Checking in PSPACE
It is correct that writing the Buchi automaton to memory takes exponential space.....which is why you don't do that.
The construction for the Buchi automaton is however very regular and can be done ...
- 2,732
3
votes
Accepted
LTL Until Tautology
Let us try to prove that $F(\neg a \vee b) \rightarrow a\,\mathcal{U}\,(b \vee \neg a)$ is a tautology. For this, we have to show that every word that is a model of $F(\neg a \vee b)$ is also a model ...
- 2,732
3
votes
Accepted
What is this operator in "The Temporal Logic of Programs" Pnueli 1977?
It's implication as indicated in en.wikipedia.org/wiki/List_of_mathematical_symbols
- 2,543
3
votes
Accepted
Non-deterministic Büchi vs Rabin: Automaton size for LTL->automaton
Consider a nondeterministic Büchi automaton $\mathcal{A} = \langle \Sigma, Q, q_0, \delta, \alpha\rangle$. The acceptance condition of $\mathcal{A}$ is a subset of states $\alpha\subseteq Q$, and an ...
- 1,594
3
votes
Accepted
$\omega$-regular expression to LTL
LTL is less expressive than $\omega$-regular expressions. For example, the expression
$$((a+b)b)^\omega$$
i.e. "there is $b$ in all the even places"
cannot be expressed in LTL.
In addition, observe ...
- 17k
3
votes
LTL to Büchi automaton, deterministic?
There are languages that are representable by an LTL formula but by no deterministic Büchi automaton (DBA).
Thus a translation from LTL to DBA cannot exist.
An example is the formula $\mathbf{F}\...
- 134
3
votes
Accepted
What is the LTL expression for "there is a value of y whose next value is 8"?
The important thing that is missing from your question is how you model your program, and specifically, what are the atomic propositions you allow.
If your atomic propositions are "y=0",...,"y=8", ...
- 17k
3
votes
Accepted
Test two LTL expression trees for equivalence
Unfortunately, the approach of constructing automata for each formula and testing their equivalence is pretty much the best you can do.
The problem of checking whether an LTL formula is valid, that is,...
- 17k
2
votes
Help understaning LTL formulae
You could build a Büchi automaton, but that might be harder than just understanding the formulas.
Let's consider the first formula:
$$(\diamond\square p \wedge \diamond \square q)\to\diamond\square(p\...
- 17k
2
votes
LTL properties in bounded model checking via assertions
The property "always eventually main terminates" should be expressible and verifiable in a bounded model checker. For such properties, the model checker would either verify the property or find a "...
- 540
2
votes
Accepted
LTL to GBA versus LTL to BA
There is no precise answer to this.
The smallest GBA for a given language is never larger than the smallest BA for a given language, simply by the fact that BAs are a special case of GBAs.
It is easy ...
- 2,732
2
votes
Accepted
distinguishing between CTL* formulas $A[FG p]$ and $AFAG p$ using transition system
(This is the "standard" example which proves that CTL is not a superset of LTL, in terms of expressiveness)
Consider this system:
state $q0$, transitions to $q0$ and $q1$
state $q1$, transition to $...
- 14.4k
2
votes
Accepted
LTL globally implies
You seem to be pretty confused, so let's sort some things out.
First, it's "implies", not "replies". That is, the formula $\phi\implies \psi$ means that if $\phi$ holds, then $\psi$ holds.
To be more ...
- 17k
2
votes
Acceptance conditions when translating LTL to Büchi automaton?
I will start with the last question and then come to the question at the top of your post.
The construction assumes that the LTL formula is given in negation normal form, so that no temporal operator ...
- 2,732
2
votes
How to graph search a LTL-generated Buchi automaton to generate valid execution paths
I would interpret your problem as follows:
Given a non-deterministic Büchi automaton representing some language $L$, you want to enumerate all shortest good prefixes of $L$ such that in every ...
- 2,732
2
votes
Accepted
Negation of the semantics of the Until operator in LTL
First, note that you did not really get the "first part the the expression correct". The first formula is, roughly, of the form
$$
\forall i, (p(i) \lor q(i))
$$
while the second one is of the form
$$...
- 14.4k
2
votes
Accepted
Are the two LTL properties $GF(\psi_1 \land F\psi_2 )$ and $GF(\psi_2 \land F\psi_1 )$ equivalent?
You are right, but you should prove it. Here's a proof sketch:
Proof setup:
Suppose that $GF(\psi_1 \land F\psi_2)$ is true and assume towards a contradiction that $\neg GF(F\psi_1 \land \psi_2)$....
- 15.5k
2
votes
Accepted
Model for formula $\Box (\psi \vee \phi) \Rightarrow (\Box \psi) \vee (\Box \phi)$
If you're just asking for any model satisfying the formula, you simply try to make one of these the case
The left hand side false
The right hand side true
Let's just pick number 2. You have to make ...
- 15.5k
Only top scored, non community-wiki answers of a minimum length are eligible