The discussion of the relative merits of linear versus branching
time frameworks goes back to early 1980s. One of the beliefs dominating
this discussion has been that "while specifying is easier in LTL
(linear-temporal logic), verification is easier for CTL
(branching-temporal logic)". Indeed, the restricted syntax of
CTL limits its expressive power and many important behaviors (e.g.,
strong fairness) can not be specified in CTL. On the other hand, while
model checking for CTL can be done in time that is linear in the size
of the specification, it takes time that is exponential in the
specification for LTL. Partly because of these arguments and partly
for historical reasons, the dominant temporal specification language
in industrial use is CTL.
In this talk we argue that in spite of the phenomenal success of
CTL-based model checking, CTL suffers from several fundamental
limitations as a specification language, all stemming from the fact
that CTL is a branching-time formalism: the language is unintuitive
and hard to use, it does not lend itself to compositional reasoning,
and it is fundamentally incompatible with dynamic validation.
In contrast, the linear-time framework is expressive and intuitive,
supports compositional reasoning and semi-formal verification, and
is amenable to combining enumerative and symbolic search methods.
Nevertheless, we claim that LTL is not expressive enough and
propose an extension of LTL as the ultimate temporal specification