Relating Linear and Branching Model Checking
--------------------------------------------

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 paper we relate branching and linear model checking.  With
each LTL formula f, we associate a CTL formula f_A that is obtained
from f by preceding each temporal operator by the universal path
quantifier A.  We first describe a number of attempts to utilize the
tight syntactic relation between f and f_A in order to use CTL
model-checking tools in the process of checking the formula f. Neither
attempt, however, suggests a method that is guaranteed to perform
better than usual LTL model checkers.  We then claim that, in
practice, LTL model checkers perform nicely on formulas with
equivalences of CTL. In fact, they often proceed essentially as the
ones for CTL.