the model-checker of Winskel can be viewed as a way of gener-ating and evalugener-ating at the same time the expression that results from applying Bekiˇc’s theorem to the boolean fixed-point expres-sion originating from the diviexpres-sion (µX.A)/si.
As we have already seen Bekiˇc’s theorem can generate highly exponentially sized expres-sions, explaining why the algorithm as it stands is very bad.3 Exactly the same thing happens with the tableau-methods of Larsen [53]
and Stirling and Walker [80] (see for instance Winskel’s discussion about the relations between the methods), even the improvements suggested by Cleaveland [23] do not remove the exponential behaviour. However, Larsen [54] has recently proposed an improvement to his original algorithm, which for one fixed-point gives a polynomial time algorithm. His improvement can be seen as exploiting the observation that some of the subexpressions generated in applying Bekiˇc’s theorem imply others allowing for a certain amount of “re-use” of information. This re-use is, however, not enough to achieve the efficiency of the algorithms we present in subsequent sections.
5.3 A Global Algorithm
In this section we will describe an algorithm for computing the minimum fixed-point of a normalized, simple equation system →nx = →nb . It will be global in the sense that it computes the complete fixed-point, and it will have time and space complexity O(|→nb |). If →nb is constructed from an unnested fixed-point formula (Xi whereµ
→l
X = A→l ) and a transition system T as described in section 5.1, the size of →nb will be O(|A||T|), hence we have a global model checking algorithm that in the worst-case is linear in the product of the size of the assertion and the size of the transition system.
We present the algorithm in the version for finding minimum fixed-points, the case of maximum fixed-points being completely dual.
3Note that the fix is not simply a question of storing information (called “dynamic programming” see e.g. Aho, Hopcroft and Ullman [3]), since Bekiˇc’s theorem generates exponentially manydifferent subexpressions.
Recall, that →nb with free variables V ={x1, . . . , xn} induces a mono-tonic function f : OV → OV, and the fixed-point we are interested in com-puting is the ‘environment’ µf. The algorithm will start with the bottom element of the latticeOV and gradually increase it until eventually the min-imum fixed-point will be reached. Pictorially one can think of the algorithm as ‘chasing ones’ around the graph described by →bn : Starting with vari-ables that have empty conjunctions on the right-hand sides and therefore must have value one, we look for dependent variables that can be forced to be one, repeating until no further variables can be forced to one thereby as it will turn out having found the minimum fixed-point.
Figure (5.3) describes the algorithm. The function st : V → Z, where Z is the set of integers, denotes the ‘strength’ of variables, i.e. st(xi) is the number of successors that must be one before the variable xi will be forced to be one. The functionf induced by →bn can be extended to a function on strengths by taking for all xi ∈V: which have enough successors that are one (negative values indicating the
‘excess’ of ones). A strength defines an environment st ∈OV by st(v) =
1 if st(v)≤0 0 if st(v)>0
It is now easy to see that if ˙f(st) = st then f(st) = st, implying that st is a fixed-point of f. The algorithm will compute a strength st with this property.
In the algorithm, the set A will denote an ‘active’ set of variables with value one for which the consequences of becoming one has not yet been com-puted. Correctness can be shown from the invariant I:
I ⇔def A⊆st≤0 &
5.3 A Global Algorithm 123
Theorem 5.2 The algorithm of figure 5.3 correctly computes the minimum fixed-point µf and it can be implemented to run in time O(|→nb |).
Figure 5.3: A global algorithm: Chasing 1’s. The set of predecessors of a variable xj is the setPred(xj) ={xi |xj belongs to theχi on the right-hand side of xi}.
Proof: It is a simple exercise to show that the invariantI holds immediately before the loopand that it is preserved by the body. When the while-loopterminates we have A = ∅ which from the invariant implies that st = f˙ (st) and st is a fixed-point, which by the second conjunct of the invariant is less than or equal to the minimum fixed-point, hence ˆst=µf.
For the time complexity, we assume that A is implemented as for in-stance a stack with constant insertion and deletion times. The strength is simply a map from the variables to the integers, which according to our as-sumptions can be implemented with constant access times. Now, first notice that whenever a variable has been removed from A, it will never be inserted again as this only happens when its strength equals zero, and strengths al-ways decrease. Hence the body of the while-loopwill at most be executed once for each variable. Each execution of the innermost for-all-looptakes time proportional to the size of Pred(v), i.e. the number of predecessors of the variable v. In total the while-looptakes time proportional to the sum of
the number of predecessors, i.e. the total number of edges inG, and is thus bounded by |→nb |. The first loopand the last assignment are also bounded by|→nb |.
As the algorithm looks at predecessors of variables the ‘graph’ must initially be reversed, which can easily be done in linear time (see e.g. Tarjan [81]). ✷