Verification of reactive systems via instantiation of Parameterised Boolean Equation Systems

Verification problems for finite- and infinite-state processes, like model checking and equivalence checking, can effectively be encoded in Parameterised Boolean Equation Systems (PBESs). Solving the PBES then solves the encoded problem. The decidability of solving a PBES depends on the data sorts that occur in the PBES. We describe a pragmatic methodology for solving PBESs, viz., by attempting to instantiate them to the sub-fragment of Boolean Equation Systems (BESs). Unlike solving PBESs, solving BESs is a decidable problem. Based on instantiation, verification using PBESs can effectively be done fully automatically in most practical cases. We demonstrate this by solving several complex verification problems using a prototype implementation of our instantiation technique. In addition, practical issues concerning this implementation are addressed. Furthermore, we illustrate the effectiveness of instantiation as a transformation on PBESs when solving verification problems involving systems of infinite size.