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.
4
questions
33
votes
2
answers
1k
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 ...
- 2,167
4
votes
1
answer
134
views
Is model checking PSpace-hard *in formula size*?
Sistla/Clarke proved [SC82] that the LTL model-checking problem is PSpace-complete.
Sometimes people write that this problem is "PSpace-hard in $|\phi|$" (e.g. [LP85]). What does this mean formally?
...
- 1,045
2
votes
0
answers
324
views
Equivalence preserving operator from CTL* to LTL
The question is about an operator that transforms any CTL* formula ${\psi}$ into a (not necessarily equivalent) LTL formula ${A\psi^d}$, where $d$ means syntactically removing all $A,E$ quantifiers ...
2
votes
1
answer
588
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