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.

Follow up work by me 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. Upon closer scrutiny, a subtle bug was found in the axiomatisation (it contained an unsound, but fortunately redundant rule); a subsequent formalisation in the proof assistant Coq, due to Myrthe van Delft under the joint supervision of Herman Geuvers and myself, restored the correctness claim (see our ITP'17 paper).

The consistent consequence preorder has inspired us to to investigate abstraction techniques for PBESs. A preliminary report revolving around the idea of using consistent consequence as a technique for abstraction appeared as a technical report in January 2013, and a thoroughly reworked version appeared in ACM's Transactions on Computational Logic in 2015, see here. Work along this line is currently continued by one of my PhD students, Thomas Neele.

Next to the work on using abstraction for solving PBESs, we have been exploring ways of exploiting advances made in SMT solving (preliminary investigations led to the following ATVA paper in 2015), of theory explaining how to extract evidence, such as counterexamples and witnesses for model checking problems and equivalence checking problems from PBESs (see our CONCUR 2013 paper and our CSL 2015 paper; the latter theory we are currently implementing in our mCRL2 tool set). At the algorithmic level, we are constantly improving the parity game-based solvers for solving PBESs, by exploring and experimenting with new parity game algorithms, using parallelism and using symbolic representations.

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.
  • ...