checking can be efficiently reduced to linear time LTL model checking for the same overall bound. 24

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 (cf. Wolper47).

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 computational) complexity.

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. 8).

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 M— 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. 14 However, a very advantageous combination based on dynamically reorganizing the symbolic representation overcomes these limitations. 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