Final Report on SERC/EPSRC Grant GR/H 16056

Verification of Infinite State Systems—theory, methods and applications

Objectives and schedule of project

The aim of the grant was to investigate theory and techniques appropriate for verifying systems with infinite, or effectively infinite, state spaces. For the first year, Dr Bradfield was the researcher supported by the grant; on his appointment to a lecturership, he became a co-investigator, and Dr Javier Esparza and Mr Alan Blair were employed as researchers for eighteen and six months, respectively, Dr Esparza concentrating on theoretical issues, and Mr Blair on application issues.

Phases of the project

Dates Employee Topic
Oct 91 Bradfield Decidability of bisimulation and model-checking.
–  Tool prototype development.
Sep 92  reported in [5, 14, 24, 26]
Apr 93 Esparza Decidability of bisimulation and model-checking
–  for nets and BPP.
Sep 94  Model-checking with true concurrency.

Model-checking via games. Compositional model-checking. reported in [1, 7, 10, 13, 16, 18, 19, 20, 22, 28]

Jan 94 Blair  Tool development.
–  Tool prototype for CCS.
Jun 94  reported in [2, 6, 3]

Achievements

Decidability questions (bisimulation).

The main verification technique studied in this grant was model-checking, that is, determining whether a system satisfies a property expressed in some temporal logic. Another commonly used technique is the use of process equivalences such as bisimulation, to determine whether an implementation is equivalent, in an appropriate sense, to a specification. Both of these techniques are in principle easy to apply to finite systems, for which they are decidable. However, for infinite systems, neither technique is in general decidable, and perhaps the most exciting theoretical problems addressed in this grant are those of determining when the model-checking problem and the bisimulation checking problem are decidable. For both model-checking and bisimulation, one can restrict the class of processes under consideration; and for model-checking, one can also consider more or less powerful logics. Many interesting results have been obtained, including solutions to some fairly long-standing open problems.

In the case of bisimulation, the result that bisimulation is decidable for normed BPA (also known as normed context-free processes), in which the only combinators are non-deterministic choice and sequential composition, has been extended in [14] to the full class of BPA processes (in which there need not exist a terminating behaviour, as there must for normed processes). The tableau-style technique for deciding bisimulation for normed BPA, developed in [24], has been applied in [13] to prove the decidability of bisimulation for BPP (basic parallel processes), which have choice and parallel composition, but not sequential composition. All other standard equivalences are undecidable for these classes of process. (However, weak bisimulation is semi-decidable for BPP [19].) [23].

Visits by Dr Petr Jančar (Ostrava) have led to results on bisimilarity checking for various classes of Petri nets. Notably, bisimulation is decidable for unlabelled nets, but undecidable for labelled nets [25]. A survey of these and related results may be found in [22].

Decidability questions (model-checking).

The researchers in this grant have concentrated more on model-checking. One question raised in the grant proposal was that of model-checking context-free processes (BPA) against formulae of the modal mu-calculus, the powerful fix-point temporal logic that is the centre of our research. This problem is known to be decidable, by means of a complex reduction to Rabin’s tree theorem, but no elementary (in either the general or complexity-theoretic sense) decision procedure is known. Other researchers have produced less complex algorithms for the alternation-free fragment of the logic (in which there is no essential interdependence between minimal and maximal fix-points) [12]. We have concentrated on developing simple tableau-style proof systems; unfortunately the general problem remains unsolved, although a simple and elegant proof for the alternation-free fragment exists [7].

Considerable success has been obtained by studying the model-checking problem for the modal mu-calculus and related logics on classes of Petri nets. The thesis [4] showed that model-checking the full mu-calculus on general Petri nets is of very high complexity, being undecidable even for the alternation-free fragment (but decidable for the purely conjunctive fragment). In subsequent work we have considered smaller classes of Petri nets, and restricted sub-logics; most of the results are negative. Even for one of the weakest branching-time logics, known as UB^{−}, in which only ‘possibly’ and ‘on some successor state’ are available, the model-checking problem is undecidable on general Petri nets [16]. However, it is decidable for the subclass of BPP-nets (a natural class of nets, which corresponds to the basic parallel processes mentioned above), and for the class of 1-safe conflict-free nets, it is even polynomial [18]. The addition of a ‘possibly always’ operator gives the logic UB, and this is undecidable even for BPP-nets [15]; thus all useful branching time logics are undecidable for most useful classes of net.

If one considers instead linear-time logics, the decidability boundary is different. The pure linear-time mu-calculus is decidable on general Petri nets [16]; however, if one adds atomic propositions of the form ‘there are no tokens on place P ’, it becomes undecidable, even for BPP-nets. Further refinements have been obtained in [15].

Recently, interesting results have been obtained by comparing the model-checking problem for standard interleaving semantics of nets, and that for a ‘truly concurrent’ interpretation. In [21] it is shown that although a logic equivalent to the well-known CTL* is undecidable in the normal interleaving interpretation of BPP-nets, as is implied by the results above, if one adopts instead the standard partial order semantics for Petri nets (‘branching processes’), the logic is decidable for BPP-nets.

Structured model-checking.

Another theme of the project is the development of model-checking techniques that allow the exploitation of the structure of models. The main result here is the development of (with Winskel and Andersen) of a compositional proof system for the modal mu-calculus on a general process algebra (including CCS) [1]. This proof system combines earlier work on compositionality with techniques from local model-checking; it is sound for all processes, and complete for finite-state processes (with well-behaved recursion).

Other work related to this topic is reported in [20], in which the recently developed Petri Box calculus of Best, Devillers et al. is used to demonstrate the combination of techniques from Petri nets and process algebras, applied to mutual exclusion algorithms. The Petri Box Calculus holds some promise for structured techniques, and will be the subject of future research by the investigators. Also relevant is Bruns’ doctoral work (preliminary report in [10]), in which operators are added to temporal logic to allow reasoning based on process abstraction.

Application work.

Application work has concentrated on the development of a prototype tool to demonstrate the possibilities of computer-assisted verification of infinite systems using tableau techniques. While a researcher on the grant, Bradfield wrote a Petri net version of such a tool, which handles many of the tasks required in tableau-style model-checking [5]. It manages tableaux, ensures that all applications of proof rules are valid, determines when tableaux have been completed, and provides verification of the sometimes (necessarily) complex well-foundedness proof supplied by the user. In the case of Petri nets, the reasoning power required can be reasonably restricted—the ability to reason with boolean combinations of linear inequalities, currently implemented, is often sufficient, although in general much more power may be needed.

The problem of checking systems expressed in (value-passing) CCS is very much more difficult, and this was tackled by Blair in his M.Sc. dissertation [2], supervised by Bradfield. Some progress was made towards finding feasible representations and reasoning techniques. Blair was then employed for six months with the task of improving the design and implementation of the tool, and continuing with his work on CCS. As a result of this work [6], a public beta release is imminent, described in [3]. Blair also started case study work with CCS, concentrating on the MSMIE protocol, which was formally verified in a restricted version by other LFCS researchers [11] using the Concurrency Workbench. This case study, and the CCS version of the tool, require considerable further work.

References.

[1] H. R. Andersen, C. P. Stirling and G. Winskel, A compositional proof system for the modal mu-calculus. Proc. 9th IEEE Symposium on Logic in Computer Science, IEEE Computer Society Press, 1994, 144–153.

[2] P. A. Blair, Infinite state model checking for CCS, dissertation submitted for the M.Sc. in Computer Science, University of Edinburgh (1993).

[3] P. A. Blair and J. C. Bradfield, A tutorial introduction to the Edinburgh Infinite State Model-checker, LCFS technical report, in preparation.

[4] J. C. Bradfield, Verifying Temporal Properties of Systems. Birkhäuser, Boston, Mass. ISBN 0-8176-3625-0 (1991).

[5] J. C. Bradfield, A proof assistant for symbolic model-checking. Proc. CAV ’92. (LNCS 663) 316–329 (1993).

[6] J. C. Bradfield, Verifying temporal properties of systems, Proc. XXI Sofsem ’94 (ed. M. Bartošek), 1–14. Czech Society for Computer Science (1994).

[7] J. C. Bradfield and J. Esparza, Model-checking context-free processes. Unpublished manuscript.

[8] J. C. Bradfield and C. Stirling, Verifying temporal properties of processes. Procs. CONCUR ’90. (LNCS 458) 115–125 (1990).

[9] J. C. Bradfield and C. Stirling, Local model checking for infinite state spaces. Theoret. Comput. Sci. 96 157–174 (1992).

[10] G. Bruns, A practical technique for process abstraction, Proc. CONCUR ’93, LNCS 715 36–49 (1993).

[11] G. Bruns and S. O. Anderson, The formalization and analysis of a communications protocol. Formal Aspects of Computing 6 96–112 (1994).

[12] O. Burkart and B. Steffen, Model checking for context-free processes. Proc. CON-CUR ’92, LNCS 630 123–137 (1992).

[13] S. Christensen, Y. Hirshfeld and F. Moller, Bisimulation equivalence is decidable for basic parallel processes. Proc. CONCUR ’93, LNCS 715, 143–157 (1993).

[14] S. Christensen, H. Hüttel and C. Stirling, Bisimulation equivalence is decidable for all context-free processes. To appear in Information and Computation.

[15] J. Esparza, unpublished manuscript.

[16] J. Esparza, On the decidability of model-checking for several μ-calculi and Petri nets, Proc. CAAP ’94, LNCS 787 115–129 (1994).

[17] J. Desel and J. Esparza, Free Choice Petri Nets. Cambridge Tracts in Theoretical Computer Science 40, Cambridge University Press (1994).

[18] J. Esparza, Model-checking using net unfoldings. Proc. TAPSOFT ’93, LNCS 668 613–628 (1993).

[19] J. Esparza, Petri nets, commutative context-free grammars and Basic Parallel Processes. To appear in Proc. FCT ’95 (1995).

[20] J. Esparza and G. Bruns, Trapping mutual exclusion in the Box Calculus, to appear in Theoret. Comput. Sci.

[21] J. Esparza and A. Kiehn, On the model checking problem for branching time logics and Basic Parallel Processes, to appear in Proc. CAV ’95.

[22] J. Esparza and M. Nielsen, Decidability issues for Petri nets – a survey, J. Inform. Process. Cybernet. 30 (1994) 3, 143–160.

[23] H. Hüttel, Undecidable equivalences for basic parallel processes, Proc. FSTTCS 13 (1993).

[24] H. Hüttel and C. Stirling, Actions speak louder than words: proving bimilarity for context-free processes. Proc. LICS ’91 376–386. IEEE Computer Society Press, 1991.

[25] P. Jančar, Decidability questions for bisimilarity of Petri nets and some related problems, Proc. STACS ’94, LNCS 774 581–594 (1994).

[26] C. Stirling, Modal and temporal logics. In Handbook of Logic in Computer Science Vol 2, ed. S. Abramsky, D. Gabbay, and T. Maibaum, OUP, 477–563 (1992).

[27] C. Stirling, Modal and temporal logics for processes. Proc. Banff Higher Order Workshop, to appear in LNCS (1994).

[28] C. Stirling, Local model checking games. Proc. CONCUR ’95, to appear in LNCS (1995).