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

February 07, 2012 | Instantiation of Parameterised Boolean Equation Systems to Parity Games |

Room: Zi 5126 | Gijs Kant |

12:30-13:30 | 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. |