Sometimes and Not Never Re-revisited: On Branching Versus Linear Time

Moshe Y. Vardi
Rice University

The difference in the complexity of branching and linear model checking has been viewed as an argument in favor of the branching paradigm. In particular, the computational advantage of CTL model checking over LTL model checking makes CTL a popular choice, leading to efficient model-checking tools for this logic. Can we use these tools in order to verify linear properties? In this talk, we describe two approaches that relate branching and linear model checking. In the first approach we associate with each LTL formula $\psi$ a CTL formula $\psi_{A}$ that is obtained from $\psi$ by preceding each temporal operator by the universal path quantifier $A$. In particular, we characterize when $\psi$ is logically equivalent to $\psi_{A}$. Our second approach is motivated by the fact that the alternation-free $\mu$-calculus, which is more expressive than CTL, has the same computational advantage as CTL when it comes to model checking. We characterize LTL formulas that can be expressed in the alternation-free $\mu$-calculus; these are precisely the formulas that are equivalent to deterministic B\"uchi automata. We then claim that these results are possibly of theoretical, rather than of practical interest, since in practice, LTL model checkers seem to perform rather nicely on formulas that are equivalent to CTL or alternation-free $\mu$-calculus formulas.