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.

Filter by
Sorted by
Tagged with
33 votes
2 answers

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 ...
Daniil's user avatar
  • 2,167
4 votes
1 answer

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? ...
Ayrat's user avatar
  • 1,045
2 votes
0 answers

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 ...
tender hopper's user avatar
2 votes
1 answer

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, ...
KJ50's user avatar
  • 131