8 votes
Accepted

Proving Linear Time Temporal Logic formula □ ◊ f ⇔ ◊ □ f

You are not missing anything. These expressions are indeed not equivalent. Assume $f$ in your case is an atomic proposition. Then the computation: $f,\neg f,(f,\neg f)^\omega$ satisfies $□◊f$, but not ...
user avatar
  • 16.2k
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 ...
user avatar
  • 124
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 ...
user avatar
5 votes
Accepted

CTL vs LTL - when a formula satisfy a model

For what it concerns LTL, your understanding is almost correct except that there may be more than one initial states in a transition system. An LTL formula $\varphi$ holds in state $s$ of a ...
user avatar
  • 9,219
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 ...
user avatar
  • 16.2k
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 ...
user avatar
  • 2,682
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. ...
user avatar
  • 2,682
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 ...
user avatar
  • 9,219
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{(...
user avatar
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 ...
user avatar
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$ ...
user avatar
  • 13.3k
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"...
user avatar
  • 2,682
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 \...
user avatar
  • 2,682
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 ...
user avatar
  • 2,682
3 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 ...
user avatar
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 ...
user avatar
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 ...
user avatar
  • 16.2k
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
user avatar
  • 2,477
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 ...
user avatar
  • 2,682
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}\...
user avatar
  • 124
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", ...
user avatar
  • 16.2k
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,...
user avatar
  • 16.2k
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\...
user avatar
  • 16.2k
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 "...
user avatar
  • 540
2 votes
Accepted

Find equivalent LTL formula, without Y (Yesterday) operator. How can I handle first state?

Initial states are somewhat of an anomaly. A similar problem is encountered in the $X$ operator when you try to define LTL over finite words. That is, it somehow would have made more sense to define ...
user avatar
  • 16.2k
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 ...
user avatar
  • 2,682
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 $...
user avatar
  • 14.2k
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 ...
user avatar
  • 16.2k
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 ...
user avatar
  • 2,682
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 ...
user avatar
  • 2,682

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