###
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.