Computer Science
T.U. Eindhoven
4pm Tuesday 11th of November, 2008
Room 4.31/4.33, Informatics Forum
Parameterised Boolean Equation Systems (PBESs) are systems of fixed-point equations with predicate variables in the left-hand side and boolean expressions with quantifiers and predicate variables on the right-hand side. They provide a fundamental framework for the verification of complex reactive systems, by encoding various problems, e.g. model checking and equivalence checking. PBESs are usually solved by incomplete methods like symbolic approximation or instantiation.
I will present some recent work on developing the notion of global invariants for PBESs. Invariants express a fixed relation between data variables and therefore accelerate or even enable the termination of the symbolic approximation process. We show that using invariants is sound, that is there is a precise correspondence between the solution of a PBES and the solution of its invariant-strengthened version. We also show that invariants are robust w.r.t. all common PBES transformations and that the existing encodings of verification problems into PBESs preserve the invariants of the original processes involved.
The theory of PBES invariants turns out to be especially useful for the verification of systems with an arbitrary number of processes. I will demonstrate the use of PBESs and PBES invariants on two such examples.