Feb 07, 2012: Gijs Kant: Instantiation of Parameterised Boolean Equation Systems to Parity Games

February 07, 2012Instantiation of Parameterised Boolean Equation Systems to Parity Games
Room: Zi 5126Gijs Kant

In this talk a few improvements of an existing verification method are presented. The verification methods involves encoding satisfaction of a formula in modal mu-calculus (a modal logic in which for instance CTL* can be encoded) by a process algebraic specifications with data as a Parameterised Boolean Equation Systems (PBES). Parameterised Boolean Equation Systems are sequences of Boolean fixed point equations with data variables. Checking if the specification satisfies a formula is then equivalent to solving the equation system. Also bisimulation of process specifications can be encoded as a PBES.

Solving a PBES is usually done by instantiation to a Parity Game (PG) and then solving the game. Instantiation means that parameters in the PBES get concrete values and that quantifiers in the equations are enumerated. A parity game is a game between two players encoded as a game graph. Solving parity games is a active field of research in itself. Instantiation of a PBES to a PG is a relatively straightforward step, but still it is the bottleneck of the verification method.

We enhance the instantiation in two steps. First, we transform the PBES to a Parameterised Parity Game (PPG), a PBES with each expression either conjunctive or disjunctive. Also we define an encoding of variables with parameters into state vectors, a grouped transition relation and a dependency matrix to indicate the dependencies between parts of the state vector and transition groups. Then we use LTSmin, that offers transition caching, efficient storage of states and both distributed and symbolic state space generation, for generating the game graph.

Benchmarks on some large case studies, show that the these enhancements speed up the instantiation significantly and decrease memory usage drastically.