# Questions tagged [linear-temporal-logic]

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

96 questions
Filter by
Sorted by
Tagged with
92 views

### LTL to automaton translation that can only read disjunctions of labels per transition

Is there any automaton (or automaton translation) as expressive as LTL that can only read disjunctions of atomic propositions per each transition? Standard LTL-to-automaton algorithms allow the ...
• 175
570 views

### How to draw a Non Deterministic Buchi Automaton (NBA) from the given property?

I'm new to LTL and Buchi automaton, and I have a hard time in constructing NBA from the given formula or the property. Could somebody please help me? The following property is given, P= "Whenever ...
1 vote
479 views

### LTL Until Tautology

Today I had to prove some tautologies as an exercise, one of them was: (Ga)->(Fb) equivalent aU(b v ¬a) It is clear that I have to prove the implication in both ways. After putting into negation ...
• 45
286 views

### LTL Formula Until with same atoms (aUa)

I am trying to solve some past papers in preparations for my next exam and I've stumbled across the following exercise: While I managed to solve most parts of the exercise, I am still unsure about ...
• 45
251 views

1 vote
161 views

### What kind of LTL formula can be represented by DBAs

I am looking for the portion of LTL formula that can be expressed by deterministic buchi automata. Is there any classification of this such?
• 175
118 views

### Buchi Automaton G(Xa->b)

I have a question regarding buchi automatons. The automata for the LTL formula, G(Xa->b) is as the attached picture. Why dosen't a have to be true in order to make the automaton correct? My ...
373 views

### Non-deterministic Büchi vs Rabin: Automaton size for LTL->automaton

Is there any general result to show that which automaton is more succinct? I have a set of LTL properties and I would like to know (show) which automaton is more efficient in term of state number and ...
• 175
1k views

### $\omega$-regular expression to LTL

Is there any systematic (algorithmic) method to convert an $\omega$-regular expression like $(a^∗)(b)(b^∗)(a^∗)(c^\omega)$ to an LTL property?
• 175
239 views

### Are there any LTL to _non_ deterministic Rabin automaton translators?

I know of two translators LTL -> deterministic Rabin automaton: Rabinizer3 ltl2dstar They produce deterministic automata, which can be much larger than their possible non-deterministic variants. Is ...
• 1,075
886 views

### What does "AF AX p" mean in CTL?

Both Logic in Computer Science (Huth and Ryan, 2004) and Branching vs. Linear Time: Final Showdown (Vardi, 2002), state something to this effect (paraphrased): In LTL, X F p and F X p are ...
• 131
1k views

### Equivalence rules for LTL - Getting stuck working with $\square \lozenge$ & Until ($\textsf{ U}$ ) operators

Need to prove equivalence for (or disprove equivalence for): $\hspace{1cm}\square ϕ → \lozenge ψ ≡ ϕ\textsf{ U }(ψ ∨ ¬ϕ) \\$ My current attempt using the LTL equivalnce rules to determine ...
• 53
1 vote
151 views

• 541
620 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, ...
• 131
1 vote
799 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 ...
• 129
3k 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.) ...
• 129
3k 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 ...
• 153
56 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 ...
• 267
337 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 ...
• 23
101 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 ...