LTL (linear temporal logic or linear-time temporal logic) is a temporal logic that can encode assertions about the future of traces.

learn more… | top users | synonyms (1)

1
vote
1answer
53 views

Transition systems that satisfy LTL but not CTL, and vice versa

I am learning about temporal logic and model checking systems. One conceptual exercise that I am struggling with is how to create a transition system which satisfies only one of two given properties, ...
0
votes
1answer
68 views

Techniques (tools) to convert temporal logic (CTL,CTL* or LTL) to μ-calculus formulae

Suppose one wants to use a μ-calculus model checker, but specify things in temporal logics, which is easier (more intuitive). Is there a technique (even better, a tool) that automatically translates ...
7
votes
3answers
368 views

Why use $\mu$-calculus and not LTL,CTL,CTL*?

It is known that the temporal logics LTL,CTL,CTL* can be translated/embedded into the $\mu$-calculus. In other words, the (modal) $\mu$-calculus subsumes these logics, (i.e. it is more expressive.) ...
2
votes
3answers
189 views

Howto formally go about proving that two LTL formulas are equivalent?

Do they need to "unwind" exactly to the same set of paths or does it suffice when one set is contained in the other ? Or is it sufficient to argue that M,s satisfies both LTL formulas for any ...
3
votes
1answer
41 views

Is there a mistake in the expression for clean behavior in Pnueli's article from 81'?

I am reading an article called The temporal semantics of concurrent programs . On page $9$, there is a small section (numbered as $2$) called "clean behavior". I think that there is a problem with ...
2
votes
1answer
88 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
47 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 ...
3
votes
1answer
82 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
93 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
67 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
133 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
80 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}$ ...
20
votes
2answers
478 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 ...
7
votes
1answer
166 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 ...