We have now presented various model-checking algorithms for finite-state sys-tems. Besides their immediate use as an automatic way of getting assertions verified for finite-state systems, they provide a means of getting algorithms for computing equivalences, preorders and other relations that can be ex-pressed as assertions in the extended calculus – provided these assertions meet criteria which make them transformable into the standard calculus.
This gives for instance algorithms for all relations that are expressible as guarded assertions in µKext, including very familiar relations like those de-scribed in chapter 4. How does this – in principle, infinity of algorithms – compare with more ad hoc constructed algorithms? To answer this question we utilize the two examples from the previous section giving rather precise bounds on the sizes of certain kinds of assertions.
For the ‘strong relations’ like strong bisimulation, ready simulation, ready bisimulation, and prebisimulation example 5.2 shows that they have reduced boolean fixed-points assertions of size O(tt) of alternation depth one, hence the global algorithms will execute in time O(tt). For the ‘weak
5.10 Some Applications: Equivalences and
Preorders Revisited 157
Relation Modal µ-calculus Algorithm from elsewhere Note Strong bisim., ∼ O(tt) O((l+l)(t+t) log(s+s)) 1
(1) from Cai and Paige [20] — generalized to non-singleton sets of actions from the original paper Paige and Tarjan [65].
(2) from Estenfeld et. al. [37].
(3) from Bloom and Paige [14].
(4) from Cleaveland and Steffen [26].
Table 5.1: Worst-case running times of some immediately derived algorithms.
The local counterparts would have all the running times multiplied with log(ss). Ready bisimulation is also often called 2/3-bisimulation.
relations’ like weak bisimulation, congruence, simulation preorder, and weak prebisimulation example 5.3 shows that they have reduced boolean assertions of sizeO(tt) with at mostssreferences from the innermost fixed-point to the outermost, and they have alternation depth two, hence the global algorithms will execute in time O(sstt).
The results are summarized in table 5.1.
Not surprisingly the algorithms we get from the µ-calculus cannot in general compete with the carefully constructed algorithms for bisimulation equivalence, which take full advantage of the knowledge of the relation being an equivalence allowing a representation by its equivalence classes. However, for the preorders the difference is minor. For ready simulation the difference is down to the difference between (t+t)(s+s) and tt, i.e. if the transi-tion system is sparse there is no real difference. For the prebisimulatransi-tion we achieve the same complexity as Cleaveland and Steffen; and for the remaining preorders we have found no non-trivial bounds – only the trivial algorithms computing approximants, which has running time O(sstt) for the relations
of alternation depth one andO((ss)2tt) for alternation depth two.
What we also have islocal algorithms for all these relations including the possible benefits from local approaches, and they have worst-case complexi-ties that are at most a logarithmic factor worse than the global algorithms.
5.11 Bibliographic Notes
The idea of model checking was pioneered by Clarke and Emerson [21] who described a model checker for CTL. The grouparound Clarke has been mainly interested in verification of hardware designs based on the logics CTL and CTL∗ and has used a method based on compact representations of sets of states (‘BDD’s’) to handle large state-spaces (see for example Burch et. al.
[19]).
Emerson and Lei [35] described the first non-trivial model checker for the modalµ-calculus. They essentially exploited the observation from Bekiˇc’s theorem used in the normalization of assertions in section 5.7 to give a model checker running in timeO(|A|ad+1|S|ad|T|).4 The global algorithm from sec-tion 5.4 (first published in [6]) improves this bound to O(|A|ad|S|ad−1|T|).
(Later the same bound has been achieved by Cleaveland, Dreim¨uller and Steffen [24], though it is not obvious whether they use the stronger defini-tion of alternadefini-tion depth used in this thesis.) Taking into account that most properties seem to be expressible in alternation depth two, for which the improvement is from O(|A|3|S|2|T|) to O(|A|2|S||T|), this is a considerable difference. For alternation depth one, the improvement is fromO(|A|2|S||T|) to O(|A||T|), a result that has independently been achieved by algorithms of Cleaveland and Steffen [27] and Vergauwen and Lewi [85] which like our algorithm all are building on the idea of Arnold and Crubille [9] of using sim-ple assertions as an intermediate form. (They all refer to their algorithms as being linear although they are linear in theproduct of the size of the transi-tion system and the size of the assertransi-tion — and for Arnold and Crubille the square of the size of the assertion.)
The idea of local model checkers for the modal µ-calculus is due to
4Recall that they use a slightly different definition of alternation depth. However, we claim without proof, that their algorithm is really running in the time determined by our stronger measure. If this should not be the case, the improvement from our global algorithm is even bigger.
5.11 Bibliographic Notes 159 Larsen [53]. (He refers to the modal µ-calculus as ‘Hennessy-Milner logic with recursion’.) Larsen’s paper describes a tableau-like method restricted to the case of one-level fixed-points, i.e. a subset of alternation depth one, and was later extended to the full calculus as a method based on tableaux by Stirling and Walker [80] who named the approachlocal model checking. It has been recast as a rewrite method by Winskel [92] which gives a very simple proof of correctness. The motivation of Stirling and Walker was to give a proof system for showing satisfaction, and its implementation as an algorithm is by Cleaveland [23]. The tableau-method has been used as the basis for an implementation in the Edinburgh-Sussex Concurrency Workbench [25] and Larsen’s algorithm is used in the TAV System [55].
All these local methods suffer from severe inefficiencies. They have bad worst-case behaviour and have exponential running times in the size of the transition systems – even the optimizations suggested by Cleaveland [23]
does not improve on this fact. However, Larsen has recently published an improvement of his original algorithm, which for one fixed-point has poly-nomial running time. Nevertheless, it is not as efficient as the algorithm of section 5.6 running in time O(|A||T|log(|A||S|)). Xinxin describes in his thesis [96] a possible extension of Larsen’s algorithm to the full calculus.
His algorithm is rather involved and the complexity measure he gives, al-though polynomial in the alternation depth, is considerably worse than the bound of O(|A|ad|S|ad−1|T| log(|A||S|)) proposed as likely in section 5.7.3 and substantiated by the two-components algorithm running in worst-case time O(|A|2|S||T| log(|A||S|)).
Cleaveland and Steffen presents in [26] ideas of computing preorders very much like the approach outlined in section 5.10, however, whereas they sug-gest checking 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 it, we get the same effect in a much simpler way by writing down directly the definition of ≤ as a formula in the extended modal µ-calculus thereby allowing model checking algorithms to be applied directly. Moreover, we can get characteristic formulas for free through the reduction for product and hence also characteristic formulas for all the preorders investigated in Steffen [75].
The complexity bounds we have given are all based on the technique of amortized complexity analysis as explained in for instance Cormen, Leiserson and Rivest [28].
Chapter 6
Computing Fixed-Points in Finite Cpo’s and Lattices
The local model-checking algorithms in chapter 5 are based on ideas of shar-ing values and tracing changes along dependencies; ideas that are not in-herently connected to the problem of model checking. In this chapter we exploit this observation by considering the problem of finding minimum so-lutions to general monotonic equation systems; present a local algorithm, prove it correct, and discuss possibly applications and the relation to the model-checking algorithms. Except from the discussion on the relation to the model-checking algorithms, which among other things will provide cor-rectness proofs for these algorithms, this chapter is self-contained and has no direct relevance to the verification of concurrent systems and is as such independent of the rest of the thesis.
6.1 Summary
We present a very simple, yet general algorithm for computing simultane-ous, minimum fixed-points of monotonic functions, or turning the viewpoint slightly, an algorithm for computing minimum solutions to a system of mono-tonic equations. The algorithm is local (demand-driven, lazy, . . . ), i.e. it will try to determine the value of a single component in the simultaneous fixed-point by investigating only certain necessary parts of the description of the monotonic function, or in terms of the equational presentation, it will
determine the value of a single variable by investigating only a part of the equational system.
In the worst-case this involves inspecting the complete system, and the algorithm will be a logarithmic factor worse than a global algorithm (com-puting the values of all variables simultaneously). But despite its simplicity the local algorithm has some advantages which promises much better perfor-mance on typical cases. The algorithm should be seen as a schema that for any particular application needs to be refined to achieve better efficiency, but the general mechanism remains the same. As such it seems to achieve per-formance comparable to, and for some examples improving upon, carefully designed ad hoc algorithms, still maintaining the benefits of being local.
We will illustrate this point by tailoring the general algorithm to con-crete examples in such (apparently) diverse areas as type inference, model checking, and strictness analysis. Especially in connection with the last ex-ample, strictness analysis, and more generally abstract interpretation, it is illustrated how the local algorithm provides a very minimal approach when determining the fixed-points, reminiscent of, but improving upon, what is known as Pending Analysis [97].