checking can be efficiently reduced to linear time LTL model
checking for the same overall bound.
1. 4. expressiveness
An important criterion for a logic is expressiveness,
reflecting what correctness properties can and cannot
be captured by the logic. Interesting properties include
safety properties (“nothing bad happens,” e.g., g¬bad),
liveness properties (“something good happens,” e.g.,
Fgoal), and fairness properties (“something is recurrent”,
e.g., gFtry). It is arguable that expressiveness in model
checking is the most fundamental characteristic, perhaps
even more critical than efficiency. It is imperative that one
be able to express all the correctness properties that are
needed. If this basic requirement is not met, there is no
point in using the verification method in the first place. In
actual usage, a particular formalism, commonly a system
of TL, provides the needed expressive power. It includes a
few basic temporal operators, which can be combined to
yield virtually limitless assertions. Another benefit of TL
is that it is related to natural language, which can facilitate its use.
The ability to describe complex patterns of system
behavior is basic. LTL is naturally suited to the task. Along
paths, it is in a sense expressively complete, equivalent
to the First Order Language of Linear Order,
19 e.g. gP =
∀t (t ³ 0 ⇒ P(t)). A property such as g2P, meaning that P
holds at all even moments 0, 2, 4,...is not expressible
in LTL. It can be useful in hardware verification applications where it is needed to count clock cycles. The (linear
time) mu-calculus as well as PSL can express this property
CTL is well suited to capture correctness over computation trees. The branching time capability of distinguishing
between necessary and possible behaviors using explicit
path quantifiers (a, e) provides significant expressive power.
The existence of a bad path, eFbad, is not expressible by any
formula ah where h is in LTL, nor even any universal CTL*
formula where all path quantifiers are a (and only atomic
propositions appear negated). Thus, LTL is not closed
under semantic negation: writing the invariant g¬bad
means ag¬bad whose semantic negation is eFbad which,
as above, is not expressible by any ah formula.
21 There has
been an ongoing debate as to whether LTL or branching
time logic is better for program reasoning. Linear time
offers the advantage of simplicity, but at the cost of significantly less expressiveness. Branching time’s potentially
greater expressiveness may incur greater conceptual (and
A related criterion is succinctness, reflecting how
compactly a property can be expressed. The CTL* formula e(FP1 ∧ FP2) is not a CTL formula, but is semantically equivalent to the longer CTL formula eF(P1 ∧ eFP2) ∨
eF(P2 ∧ eFP1). For n conjuncts, the translation is exponential in n. In practice, the most important is the criterion of
convenience, reflecting how easily and naturally properties
can be expressed. Expressiveness and succinctness may be
partially amenable to mathematical definition and investigation. Succinctness and convenience often correlate but
not always. Convenience, however, is inherently informal.
Yet it is extremely important in actual use. That is why, e.g.,
many person-years were devoted to formulating industrial-strength logics such as PSL.
1. 5. efficiency
Another important criterion, efficiency, is related to questions of the complexity of the model checking problem
for a logic and the performance of model checking algorithms for the logic. An algorithm that has potentially
high complexity in theory but is repeatedly observed to
exhibit significantly lower complexity in actual use is
likely to be preferred to one with better theoretical complexity but inferior observed performance. Moreover,
there are trade-offs. For instance, a more expressive logic
is likely to be less efficient. A more succinct logic is likely
to be more convenient yet even less efficient. Some experience is required to reach a good trade-off. For many model
checking applications, M is sufficiently small that it can
be explicitly represented in computer memory. Such basic
enumerative model checking may be adequate for systems
with 106 states.
However, many more systems M have an astronomically
or even infinitely large state space. There are some fundamental strategies to cope with large state spaces. Foremost,
is the use of abstraction where the original, large, complex
system M is simplified, by suppressing inessential detail
(cf. Clarke and Emerson10), to get a (representation of a)
smaller and simpler system M —.
Compact representations of the state graph yield another
important strategy. The advent of symbolic model checking,
combining CTL, fixpoint computation, and data structures
for compact representation of large state sets, made it possible to check many systems with an astronomical number
of states (cf. Burch et al.
If there are many replicated or similar subcomponents, it
is often possible to factor out the inherent symmetry in the
original M resulting in an exponentially reduced abstract
43 (cf. Sistla et al. and Clarke et al.
43, 9). Most work on symmetry has required the use of explicit representation of M.
Natural attempts to combine symmetry and symbolic representation were shown inherently infeasible.
a very advantageous combination based on dynamically
reorganizing the symbolic representation overcomes these
25 Finally, one may have an infinite state system
comprised of, e.g., a (candidate) dining philosophers solution Mn for all sizes n > 1. In many situations, this parameterized correctness problem is reducible to model checking
a fixed finite-size system Mc (cf. Clarke et al., and Emerson
and Kahlon9, 22).
1. 6. evolution of model checking
The early reception of model checking was restrained.
Model checking originated in the theoretical atmosphere of
the early 1980s. There was a field of study known as Logics
of Programs, which dealt with the theory and sometime use
of logic for reasoning about programs. Various modal and
temporal logics played a prominent role. The key technical
issue under investigation for such a logic was satisfiability:
Given any formula f, determine whether there exists some
structure M such that M |= f. Analyzing the decidability and