 HOMEPROJECT DESCRIPTION PROJECT MEMBERS |
Parameterised Boolean Equation Systems are at the essence of model checking, process algebras and much more!
Boolean Equation Systems (BESs) are ordered sequences of equations of the form
(μ X = ƒ) or (ν X = ƒ)
where μ is the least fixpoint, ν is the greates fixpoint, X is a propositional variable and ƒ is a proposition. For an excellent and very enlightning study of 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 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.
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. We did not address theoretical considerations such as completeness.
Much remains to be done, for instance:
| ||
|
|