4.4 General Temporal properties
4.4.2 Beyond CTL •
Now, one might ask what kind of formulae are not in CTL• – and are im-possible to translate into CTL• using the equations of figure 4.1? A typical example would be
Θ = ∀(✷Ψ∨✷Ψ)
where Ψ and Ψ are formulae in CTL•. None of the equations are applicable as neither ∀ nor ✷ distributes over disjunction. Nevertheless, we will show how one can find an assertion in the modalµ-calculus equivalent to Θ using a slightly more advanced idea than the simple translationI.
First, suppose that we have a constant†with valuation the set of states that cannot perform any transitions, i.e.
V(†) = {s∈S |s →}
Then † T,V will be a set of ‘empty’ sequences (consisting of single states).
Using this constant can now be written as:
Φ = Φ∨ †.
It is not hard to prove that✷ satisfy ✷Φ = Φ∨✷Φ
(4.2)
4.4 General Temporal properties 105 (If we stick to the class of models with total transition relations, here and everywhere else the prime could be removed and everything will still be true.) Now, let us rewrite Θ using this equation:
Θ = ∀(∨✷Ψ)
=∀((Ψ∧ ✷Ψ)∨((Ψ∧ ✷Ψ))
=∀((Ψ∨Ψ)∧(Ψ∨ ✷Ψ)∧(Ψ∨✷Ψ)∧ ✷Ψ∨✷Ψ))
= ∆∧ ∀( ✷Ψ∨ ✷Ψ))
where ∆ = (Ψ∨Ψ)∧(Ψ∨ ∀ ✷Ψ)∧(Ψ∨ ∀ ✷Ψ) using the equations of figure 4.4.1 as Ψ and Ψ are CTL• formulae
= ∆∧ ∀ (✷Ψ∨✷Ψ))
= ∆∧ ∀ ∀(✷Ψ∨✷Ψ))
= ∆∧ ∀ Θ
Hence, taking F(X) = ∆∨ ∀ X we have that F(Θ) = Θ. Now, suppose that Φ is another formula satisfying F(Φ) = Φ, is there any relationship between Φ and Θ? In fact, we will argue that Φ ≤Θ where
Φ≤Θ⇔def ΦT,V ⊆ ΘT,V for all T and V.
In other words, Θ is the maximum fixed-point of F. Actually, we will prove the (apparently) stronger result that if U is a post-fixed point of the map on P(RT) induced by F, which we denote byF, hence F(U)⊇U, then
U ⊆ Θ (4.3)
for some fixedT andV. AsF yields state formulae when applied to state for-mulae (and Fyields subsets with the state property when applied to such subsets) we can intuitively speaking ‘translate F’ into a modal µ-calculus formula:
Proposition 4.3 Giuen a transition system T and a valuation V. For all CT L• formulae Ψ and Ψ we have
s|=∀(✷Ψ∨✷Ψ)
⇔
s∈[[νX.(A∨A)∧(A∨[.]νY.A∧[.]Y)∧(A ∨[.]νY.A∧[.]Y)∧[.]X]]
⇔
s ∈[[νX.(A∨νY.A∧[.]Y)∧(A ∨νY.A∧[.]Y)∧[.]X]]
where A=I(Ψ), A =I(Ψ).
Proof: The last implication is by simple rewriting. For the first bi-implication, we continue the above discussion assuming that U is a set of runs, s.t. U ⊆ F(U), and prove 4.3. We first prove thatU is suffix-closed, i.e. for allk ∈ω,
∀δ∈U. k <|δ| ⇒δk+1 ∈U For the base case we get
δ∈U =F(U) =∆ ∩ ∀(U)
which implies that, for all δ with δ0 = δ0,(δ)1 ∈ U hence in particular δ1 ∈U. From this it can also be seen that U has the state property.
For the inductive stepwe assume that δ ∈ U. Then as above we get δ1 ∈U, which by the induction hypothesis implies (δ1)k+1 =δk+2 ∈U.
As δk ∈U for all k≤ |δ| and henceδk ∈ ∆ we have δk ∈[[∆]] . Now, we must argue that for all δ∈U we have
∀k ≤ |δ|. δk ∈[[Ψ]]
or (4.4)
∀k ≤ |δ|. δk ∈[[Ψ]]
implying that δ ∈ ✷Ψ∨✷Ψ and hence as U has the state property that U ⊆ Θ. We already know that for all k ≤ |δ| we have δk ∈ [[∆]] thus in particular δk ∈[[Ψ]] orδk ∈[[Ψ]]. Hence it is enough proving
δk∈/[[Ψ]] ⇒ ∀l ≥k. δl ∈[[Ψ]] (4.5) Assume given such a k. Thenδk∈[[Ψ]] and as δk ∈[[∆]] also
δk∈[[Ψ]]∨[[∀ ✷Ψ]], hence
δk ∈[[∀ ✷Ψ]],
4.4 General Temporal properties 107 This implies that for all l > k, we have δl ∈[[Ψ]] and we are done.
Assuming for a moment that we extend the syntax for linear time for-mula with fixed-point operators with semantics an element of the lattice P(Runs), we have actually shown that
Θ = νX.∆∧ ∀ X.
Now, notice that ∆ is a CTL• formula with
I(∆) = (A∨A)∧(A∨[.]νY.A∧[.]Y)∧(A∨[.]νY.A∧[.]Y) where A=I(Ψ) and A =I(Ψ). We extend I to fixed-points by taking
I(νX.Ψ) = νX.I(Ψ) I(X) = X hence
I(Θ) =νX.I(∆)∧[.]X and we claim that
[[Θ]] = [[νX.∆∧ ∀ X]] = [[νX.I(∆)∧[.]X]].
(Proving this formally requires the use of a theorem relating fixed-points in different lattices, the reduction lemma of section 3.2 suffices.) ✷
If we considered instead another assertion outside CTL•, Θ = ∀(✸Ψ∨✷Ψ) with Ψ and Ψ CTL• formulae we could try to employ the same trick using
✸Ψ = Ψ ∨ ✸Ψ
for the ✸-modality. This time both a minimum and a maximum fixed-point will be involved. We start rewriting Θ:
Θ = ∀(✸Ψ∨✷Ψ)
= ∀(Ψ∨ ✸Ψ∨(Ψ∧ ✷Ψ))
= ∀((Ψ∨Ψ∨ ✸Ψ)∧(Ψ∨ ✸Ψ∨ ✷Ψ∨ †))
= (Ψ∨Ψ∨ ∀ ✸Ψ)∧(Ψ∨ † ∨ ∀∀(✸Ψ∨✷Ψ))
= ∆∧(Ξ∨ ∀ Θ)
where ∆ = Ψ∨Ψ ∨ ∀ ✸Ψ and Ξ = Ψ∨ †
Notice, that ∆ and Ξ are in CTL•. Hence, Θ is a fixed-point of the function F(X) = ∆∧(Ξ∨ ∀ X) and again it can actually be shown that all other (post-)fixed-points will be less, thus
Θ = νX.∆∧(Ξ∨ ∀ X) and we find theµ-calculus formula
νX.I(∆)∧(I(Ξ)∨[.]X), where
I(∆) =I(Ψ)∨I(Ψ)∨[.]µY.[.]Y ∨I(Ψ) and
I(Ξ) =I(Ψ)∨ †.
It is not obvious how far this idea of ‘pulling out CTL•-formulae’ can be taken and it is an interesting task to find out using this idea whether a more succinct translation than that of Dam [31] from CTL∗ into the modal µ-calculus is possible.
4.5 Bibliographic Notes
More literature on how to express properties in the modalµ-calculus can be found in for example Emerson and Clarke [34], Kozen [49], Emerson and Lei [35], Dam [31], and Stirling [79]. Case studies using the modal µ-calculus can be found in Walker [87] and Bruns [18].
We have shown how a variety of properties can be expressed in the extended modalµ-calculus including linear time temporal properties, equiv-alences, preorders, and characteristic formulae. We shall later in section 5.10 see how to get algorithms for automatically checking all these relations.
As we have seen, the modalµ-calculus seems to be a good candidate for a low-level general language for expressing behaviours of concurrent systems and could as such be used as the backbone of a general verification tool.
Cleaveland and Steffen present in [26] ideas of computing preorders very much like the present approach, however, whereas they suggest checking
4.5 Bibliographic Notes 109 s ≤ s for a preorder ≤ by generating a characteristic formula C of ≤ with respect to s by ad hoc means and verify whether s satisfies s, we get the same effect much simpler by writing down directly the definition of ≤ as a formula in the extended modalµ-calculus allowing model checking algorithms to be applied directly, and in effect we can get characteristic formulasfor free through the reduction for product; hence also characteristic formulas for all the preorders investigated by Steffen [75].
Chapter 5
Model Checking in Finite-State Systems
In this chapter we consider the problem of determining satisfaction for finite-state systems, a task which is often referred to as model checking.
The compositional method from chapter 3 already offers one way of per-forming model checking: Given a finite-state process and a closed assertion we can repeatedly apply the reductions until we end up with a boolean ex-pression with atoms that are correctness assertions about the nil process.
These correctness assertions can easily be removed by the reduction for nil, and we arrive at a boolean expression which can be evaluated to produce the answer. This, however, is not an efficient algorithm.
Instead, using the reduction for product we will describe a very simple way of transforming the satisfaction problem into a problem of determining the value of a boolean fixed-point expression – a boolean expression involving simultaneous fixed-point operators over boolean-valued variables – and de-scribe algorithms for evaluating such expressions in an efficient manner.
Remark 5.1 In the analysis of time and space complexities we are going to make in the sequel, we will make use of some general assumptions about the representations of assertions and transition systems. Firstly, variables and labels will be assumed to be represented by natural numbers, which in turn will be assumed to be representable in a constant amount of memory.1
1As usual in camplexity analysis we make the assumptions that integers amount of memory and that an arbitrary memory address can be accessed in can be stored in a
Secondly, functions from an interval of the natural numbers to a set of ‘sim-ple’ values, e.g. numbers, will be represented efficiently such that access to the value at one particular element in the domain can be performed in constant time (like ‘arrays’ in many programming languages). Thirdly, we assume that directed graphs consisting of a set of nodes (an interval of nat-ural numbers) and a set of edges (pairs of natnat-ural numbers) are represented such that a list containing the edges out of one particular node can be found in constant time and such that this list can be traversed in linear time. A labelled transition system and a simple equation system can be implemented by such a graph representation – for the transition systems, labels are also attached to the edges. Fourth, the set of states is assumed to be an interval of the natural numbers such that subsets of states can be represented as their characteristic functions with contant time tests for membership.
These assumptions are met by the class of machine models calledRAM models; an abstract machine model which in practice is realized by all general purpose computers. We will later discuss to what extent even weaker models suffice for implementing our algorithms.
Often we will use statements like this algorithm runs ‘in time and space K(n)’, where it actually should be ‘in time and space asymptotically bounded by K(n)’. We will use the notation O(K(n)) for this statement. All these assumptions and slight abuses of language are standard when analyzing com-plexities of algorithms (see for example Hopcroft and Ullman [43]). ✷
5.1 Tansforming Satisfaction to Boolean Ex-pressions
We will start by looking only at assertions in µKwhere,Q, i.e. the standard calculus extended withwhereµ-clauses and constants, and discuss the gener-alizations toµKextin section 5.9. Assume we have given a finite-state process pand a closed assertion in µKwhere,Q. The transformation of the satisfaction problem
|=p:A
constant constant time (the ’uniform cost criterion’, cf. Aho, Hopcroft and Ullman [3]).
5.1 Tansforming Satisfaction to Boolean Expressions 113 to a boolean expression with fixed-points will proceed in three steps. FirstA is transformed to positive, normal form by pushing negations inwards. Sec-ondly, the fixed-points ofAare transformed to asimple form. And thirdly we
‘divide’ this assertion by the processpto get a boolean fixed-point expression.
The first two steps were described in section 2.6.1 and section 3.7. (The idea of translating into a simple form is due to Arnold and Crubille [9].) The third stepof the translation will turn out to be a special case of the reduction for product! To motivate this translation, assume given a finite-state process p and a closed assertion A. Instead of deciding whether
|=p:A (5.1)
holds, we could take an apparent detour by considering instead the process (nil×p){Ξ}where Ξ : Act∗ Act∗ is defined by
Ξ(x) =
a if x≡ ∗ ×a, a ∈Act undefined otherwise.
Then it should be obvious that (5.1) is valid, if and only if,
|= (nil×p){Ξ}:A (5.2)
is valid.
For (5.2) we can apply first the reduction for relabelling to get an asser-tion red{Ξ}(A) which is actually going to be like A except that all modalities ahave changed to∗ ×aand then proceed with the reduction for product to get the assertionB = red×p(red{Ξ}(A)) which by theorems 3.4 and 3.7 has the property that (5.2) is valid, if and only if,
|=nil:B (5.3)
is valid.
However, if we consider howB looks, we discover that in itno modalities except modaliities over the idling action appear. As [[∗A]]nilρ= [[A]]nilρeven these trivial modalities can be removed and we get an equivalent b which is a boolean expression with simultaneous fixed-points, the value of which determines the validity of (5.3) and hence of (5.1).
The combined reduction consisting of applying first the reduction for relabelling, then the reduction for product and finally removing the trivial modalities will be called dividing A with p and is tabulated in figure 5.1.
Figure 5.1: The division operator; A/s (respectively (A/-s)) abbreviates reds(A;σ, V) (respectively red,s(A;σ, V)).
From the above discussion we get as an immediate corollary of theorem 3.8:
Corollary 5.1 Assume given a finite transition system T with states S = {s1, . . . , sn}, a valuation V and an assertion A in µKwhere,Q. Then for a change of variables σ which is fresh for A,
[[A[σ]]]T,Vρ=in([[red→sn(A;σ, V)]]nil,Vρ)
where V is an arbitrary valuation and in is the composition of the in-map from the reduction of relabelling and the reduction of product, i.e. the map in : (P(nil))n → P(S) with
in(→un) = {si |ui ={nil}}.
5.1 Tansforming Satisfaction to Boolean Expressions 115 How do we now evaluate b = redsi(A;σ, V)? As b contains fixed-points this is not a trivial task. Semantically, when interpreting b over the one-state transition system pointed by nil, the denotation ofb will be either the property ∅or the property{nil}. However, the two-point latticeP({nil}) of properties of nil is nothing else than an isomorphic copy of the well-known Sierpinski space O = {0,1} with ordering 0 < 1, so for convenience we consider the semantics of boolean fixed-point expressions as being given as an assertion about nil, but we will use 0, for false, and 1, for true, for the values ∅ and {nil}. Hence, we can define for a closedb,
[[b]] =
0 if [[b]]nilρ=∅ 1 if [[b]]nilρ={nil}
for an arbitrary environment ρ. We proceed similarly for tuples-b.
Now, for a monotonic functionf onOwe observe the following property of fixed-points:
Proposition 5.1 I f f : O → O is a monotonic function then µf = f(0) and νf =f(1).
Proof: Trivial. ✷
Using this simple observation we can compute the value of b by first applying Bekiˇc’s theorem to get only unary fixed-points and replace all the fixed-points with their bodies applied to 0 (for minimum fixed-points) or to 1 (for maximum fixed-points) resulting in a simple boolean expression that only contains disjunctions and conjunctions over the atoms 0 and 1 and which is easily evaluated to yield the result.
However, the use of Bekiˇc’s theorem has the potential danger of increas-ing exponentially the size of the expression, so although the evaluation is simple (“linear time”) the expression to evaluate can be huge. Curiously enough, this simple observation seems to offer an explanation of why the tableau-based methods of Stirling and Walker [80] and Cleaveland [23], and the methods of Larsen [53] and Winskel [92] have bad complexities com-pared to the algorithms we are going to present (see section 5.2 below for a discussion of this point).
Instead we will transform simple, simultaneous fixed-points -x = -b to a normalized form, which resembles a kind of directed graphs. Inspired by this analogy we give graph-like algorithms for computing the fixed-points.
In section 5.3 we present a global algorithm computing the values of all of -x and in section 5.6 a local algorithm computing only a certain minimal part of-x.
But before proceeding to the evaluation we state and prove the correct-ness of the three-steptranslation just given.
Proof: Take A0 to be the positive normal form of A. Surely, A0 can be computed from A in linear time and this without changing the alternation depth. Let A1 be the simple form of A0 as given by lemma 3.5. Take b = reds(A1;σ, V) for some change of variables σ. Hence, since the division is a special case of the reduction for product, (i)−(v) follows from lemma 3.5 and lemma 3.6. Finally, it is easy from the definition of division, to observe that since A1 is simple so isb. ✷
For a single unnested fixed-point (Xiwhereµ
X→l = A→l ) with| A→m |= kour transformation first derives a simplek-ary fixed-point (Yj whereµ
Y→k =
→k
B ) and then, given a transition system withn states, transforms this into ank-ary fixed-point (yjiwhereµ
→nk
y = b→nk ) where b→nk only consists of conjunctions and disjunctions over variables. By these transformations we have reduced the problem of finding a fixed-point over the latticeP(S)l to a problem of finding a fixed-point of a boolean function over the lattice Onk.
We will normalize the equations of the boolean fixed-point expression slightly more: