PARAMETERISED BOOLEAN EQUATION SYSTEMS

Parameterised Boolean Equation Systems have applications in model checking, equivalence checking, static code analysis.

Boolean Equation Systems (BESs) are ordered sequences of equations of the form
(μ X = f) or (ν X = f)
where μ is the least fixpoint, ν is the greatest fixpoint, X is a propositional variable and f is a proposition. For an excellent and very enlightning study explaining their use for model checking, see the Ph.D. thesis of Angelika Mader.

Parameterised Boolen Equation Systems (PBESs) are BESs in which the notion of data is made explicit. PBESs are ordered sequences of equations of the form
(μ X(d:D) = φ) or (ν X(d:D) = φ)
where X is a predicate variable and φ is a predicate formula. The difference between PBESs and BESs is at the same conceptual level as the difference between "Parameterised" Labelled Transition Systems (such as symbolic transition systems and LPEs) and Labelled Transition Systems.

PBESs first appeared in Radu Mateescu's Ph.D. thesis, and, subsequently in this technical report by Radu Mateescu and Jan Friso Groote. As shown in that article, PBESs can serve as an intermediate formalisms for model checking processes in a setting with data. Four proof-rules are given to solve the model checking problem by hand.

In this article, Jan Friso Groote and I defined a semi-decision procedure and implemented a model checking prototype tool called MuCheck. The internals of this prototype revolve around finding the solution to a (generated) PBES, using Gauss Elimination and symbolic approximation techniques. Our findings with MuCheck provided the insight that its efficacy could be vastly improved by first returning to the root of the problem. In this article, we describe a (first) step into the theory of PBESs and the means to solve these. We discuss invariants, patterns and approximation as techniques for solving PBESs.

Late 2006, we have been working on extending the PBES-based model checking theory with timing. Based on our experiences with MuCheck, we have implemented the transformation of the real-time model checking problem into PBESs in the specification language mCRL2. Studying the resulting PBESs and finding solution methods for these is postponed in favour of solving several open ends in the theory for PBESs that are applicable to both timed and untimed systems (see below). Most of these results have been obtained in the context of the research project COMFORTS.

In a Concur'07 paper, Taolue Chen, Bas Ploeger, Jaco van de Pol and I have defined algorithms for translating various process equivalences into PBESs. Prototype implementations of these algorithms are available in mCRL2.

An extended abstract of an in-depth study of invariants for PBESs by me and Simona Orzan appeared in Concur'08. Among a host of results for invariants, a new pattern is proposed. A full version of the paper (roughly 50 pages), that includes additional lemmata, results and proofs, appeared in Theor. Comp. Sc., 411(11-13):1338-1371, 2010.

The computer-aided solving of a PBES is furthermore supported by Bas Ploeger's, Alexander van Dam's (M.Sc. student graduation project 2006-2007) and my work on a solution strategy for (partially) instantiating PBESs, which appeared in ICTAC'08. An extended and enhanced journal version of that paper appeared in Information & Computation.

Our later investigations have led Simona Orzan, Wieger Wesselink and myself to consider static analysis techniques for PBESs, which help to reduce the complexity of a given PBES such that the PBES may become computationally tractable. This work is based on preliminary investigations by Simon Janssen (MSc. student graduation project 2008), and appeared in TACAS'09.

On a related note, Jeroen Keiren (my former M.Sc. student, graduated 2009; and a former Ph.D. student) and I have started studying minimisation techniques for Boolean Equation Systems. Our early results, which appeared in Haifa Verification Conference 2009, indicate that variations of bisimulation reduction techniques are very powerful in this setting: both huge reductions in size and solving times have been observed consistently in over 300 experiments (and counting). The bisimulation reductions seem to surpass the power of the heuristics of the PGSolver library. Concurrently, Michel Reniers and I have studied bisimilarity of structure graphs underlying arbitrary closed Boolean Equation Systems; this work appeared in SOS 2009. Together with Jeroen Keiren, we have extended this work, fixing some nuances and bugs along the way, see the result in ACM's Transactions on Computational Logic. Together with Jeroen Keiren and Sjoerd Cranen, have been working on extending our work to deal with weaker equivalence relations. One equivalence relation we studied is stuttering equivalence, transposed to the setting of Parity Games. This work was published in NFM'11 and a follow up on that, tailoring stuttering equivalence to parity games, taking forced moves into account appeared in ICTAC'12.

Recent work by me has furthermore led to a finer notion of equivalence for PBESs, called consistent correlations, which appeared in CONCUR'10 in Paris, France. This work is of particular importance for boosting productivity in devising novel manipulations for PBESs, and, in particular, in proving their correctness. Maciej Gazda, PhD student in the NWO supported VOCHS project, axiomatised the preorder (which we call a consistent consequence) underlying this equivalence, and shown its decidability to be NP-hard. Details appeared in a SOFSEM'12 paper. Moreover, the preorder has inspired us to to investigate abstraction techniques for PBESs; a preliminary report appeared as a technical report and is currently under review for ACM's Transactions on Computational Logic.

Much remains to be done, for instance:
  • Automate the techniques of this article.
  • Tackle PBESs that emerge from real-time verification problems.
  • Find new patterns, in particular, those patterns that arise due to model checking real-time systems.
  • Study the use of confluence in PBESs.
  • ...