LTL (linear temporal logic or linear-time temporal logic) is a temporal logic that can encode assertions about the future of traces.
1
vote
1answer
30 views
Equivalence of logical Formula (Kripke structures)
Can someone explain me how to find if these formulas are equivalent with Kripke structures?
AG(Fp or Fq) , A(GFp or GFq)
AGF(p and q) , A(GFp and GFq)
AFG(p and q) , A(FGp and FGq)
Thank you in ...
3
votes
2answers
38 views
Temporal logic for interface invariants
I am looking for some sort of temporal logic for expressing invariants in interfaces. Since interfaces do not specify data representation, the invariants must rely solely on the publicly available ...
2
votes
1answer
67 views
LTL: Show $\neg(aUb) \Leftrightarrow \neg b U (\neg a \land \neg b) \lor G \neg b$
I got as far as
\begin{align}
w \vDash \neg (a U b) &\Leftrightarrow \neg (w \vDash a U b)
\Leftrightarrow \neg (\exists_{i\geq0} : w^i \vDash b \land \forall_{0\leq k < i} : w^k \vDash a) ...
3
votes
1answer
48 views
Equivalence of GFp and Gp in LTL
In linear time logic, is $\mathbf{GF}p$ equivalent to $ \mathbf{G}p$ ?
$\mathbf{GF}p$ means that it is always the case that p is true eventually.
Let $\mathbf{G} p$ be defined as: $\forall j \ge0,\ ...
3
votes
0answers
46 views
Spot the formalism (some kind of process logic)
Consider the following specification technique.
A specification consists of a finite set of triples $\langle C, A, C' \rangle$,
where $A$ is the name of an action and $C, C'$ are conditions, that is,
...
2
votes
3answers
104 views
Why is GFp -> GFq false in LTL, even though GFp and GFq are false?
Consider the Kripke structure:
$$
\begin{array}{ccccccc}
\to & (p, \neg q) & \to & (\neg p, \neg q) & \to & (\neg p, q) \\
& \circlearrowright & & \circlearrowright ...
3
votes
1answer
65 views
Time to construct a GNBA for LTL formula
I have a problem with the proof for constructing a GNBA (generalized nondeterministic Büchi automaton) for a LTL formula:
Theorem: For any LTL formula $\varphi$ there exists a GNBA $G_{\varphi}$ ...
19
votes
2answers
326 views
Equivalence of Büchi automata and linear $\mu$-calculus
It's a known fact that every LTL formula can be expressed by a Büchi $\omega$-automaton. But, apparently, Büchi automata are a more powerful, expressive model. I've heard somewhere that Büchi automata ...
5
votes
1answer
68 views
Algorithm to translate a deterministic Büchi automaton to LTL (when possible)
Linear temporal logic and deterministic Büchi automata are incomparable: DBA cannot express $FGa$, and LTL cannot express "at least each odd letter is 'a'". But sometimes it is interesting to know ...
