p p AGp:

figure 1. Basic temporal operators.

p

pp

pp

EFp:

AFp:

p

p

pp

is thus inevitable) and eFp (along some future, P eventually holds and is thus possible). The branching time logic CTL* subsumes both CTL and LTL. (See Figure 1.)

Temporal logic formulae are interpreted over a given finite state graph, also called a (Kripke) structure, M comprised of a set S of states, a total binary transition relation R ⊆ S × S, and a labelling L of states with atomic facts (propositions such as P) true there. There may also be a distinguished (start) state s0. As usual in mathematical logic, to be precise in defining a logic we use the meta-notation M, s0 |= f as shorthand for “in structure M at state s0 formula f is true,” for f a CTL (or CTL*) formula. When s0 is understood, we may write M |= f. For example, M, s0 |= aFP iff for all paths x = s0, s1, s2, . . . in M we have ∃i ³ 0, P ∈ L(si).

When doing specification in practice we may write just aFp to assert that formula p is inevitable. An LTL formula h is interpreted over a path and then over a structure by implicit universal path quantification: in practical specification we write h but mean ah.

The LTL formula g¬(C1 ∧ C2) captures mutual exclusion for the critical sections, corresponding to assertions C1 and C2, of processes 1 and 2, respectively. In CTL, we would write ag¬(C1 ∧ C2) for mutual exclusion, and ag(T1 ⇒ aFC1) for “whenever process 1 enters its trying region (T1) it inevitably enters its critical section (C1).” The CTL formula ageFstart asserts the system can always be restarted; this is not expressible in LTL. The CTL* formula egFsend asserts the existence of a fair behavior along which the send condition occurs repeatedly. Such fairness conditions are important in ensuring that goals are fulfilled in concurrent systems.

The logics LTL, CTL, and CTL* have turned out to be very influential, spawning industrial extensions and uses, plus many academic applications as well as theoretical results. There are prominent industrial logics, tailored for hardware verification using special “macros,” i.e., compact high-level operators that expand into longer combinations of basic operators. These include IBM Sugar based on CTL, Intel For-Spec based on LTL, and PSL (IEEE-1850 standard), incorporating features from CTL*.

Finally, there is also the (propositional) mu-calculus31 (cf. Emerson and Clarke20), a particular but very general TL. It permits temporal correctness properties to be

characterized as fixed points or fixpoints of recursive definitions. For example eFp = p ∨ ex(eFp). The mu-calculus plays a vital role in model checking. It is very expressive: CTL, CTL*, as well as LTL, can be encoded in the mu-calculus. The fixed point characterizations of temporal correctness properties underlie many conventional and symbolic model checking algorithms, as well as tools used in practice.

1. 3. model checking

In the early 1980s Clarke and Emerson proposed model checking, a method for automatic (and algorithmic) verification of finite state concurrent systems10; independently Quielle and Sifakis proposed essentially the same method. 41 In model checking, TL is used to specify correct system behavior. An efficient, flexible search procedure is used to find correct temporal patterns in the finite state graph of the concurrent system. The orientation of the method is to provide a practical verification method. The technical formulation of the model checking problem is simply: Given a finite structure M, state s, and a TL formula f, does M, s |= f An alternative formulation is, given M and f, calculate {s : M, s |= f}. The main result of Clarke and Emerson10 is that CTL model checking can be done in time O(|f| · |M| 2); that is, in time polynomial in the formula and the structure sizes. (The result in Queille and Sifakis41 was with respect to a slighly weaker TL.)

The algorithm was based on fixpoint characterizations of basic temporal modalities. For example, let f (Z) denote p ∨ axZ. We see that aFp = f (aFp) is a fixpoint of f(Z), since AFp holds iff p holds or axaFp holds. In general, there may be multiple fixpoints. It can be shown that aFp is the least fixpoint, which we shall write mZ = f (Z), with f (Z) as above. Intuitively, least fixpoints capture only well-founded or finite behaviors. The fixpoint characterization mZ = f (Z) of a property makes it possible to calculate iteratively the set of states where aFp is true. This utilizes the fact that every formula corresponds to the set of states in which it is true. We compute the maximum of the ascending chain of increasingly larger under-approximations to the desired set of states: false ⊆ f ( false) ⊆ f 2(false ) ⊆ . . . ⊆ f k( false) = f k+ 1(false), where k is at most the size of the (finite) state space. More generally, the Tarski–Knaster Theorem (cf. Tarski44) permits the ascending iterative calculation  fi(false) of any temporal property r characterized as a least fixpoint mZ = f (Z), provided that f (Z) is monotone, which is ensured by Z only appearing un-negated. For greatest fixpoints, one starts the calculation at true. Essentially the same algorithm was given in Queille and Sifakis. 41

The following are noteworthy extensions. CTL model checking can be done in time O(|M| · |f|), 11 i.e., linear in the size of the state graph and linear in the size of the formula. LTL model checking can be done in time O(|M| · exp(|f|); since M is usually very large while f is small, the exponential factor may be tolerable. 33 The automata-theoretic approach to LTL model checking is described in Vardi and Wolper. 46 A succinct fixpoint characterization of fairness from Emerson and Lei23 is used to make LTL model checking more efficient in practice. Branching time CTL* model