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