# Tag Info

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 ...

### 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 ...

### 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 ...
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 ...
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 ...
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 ...

### 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. ...

### 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 ...

### 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{(...

### 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 ...
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$ ...
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"...
Accepted

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", ...
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,...

### 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\...

### 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 "...
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 ...