Improved static analysis of parameterised Boolean equation systems using control flow reconstruction

We present a method for fighting the state space explosion of parameterised Boolean equation systems (PBESs); these essentially are systems of mutually recursive Boolean fixed point equations, parameterised with data. PBESs can encode equivalence checking problems and model checking problems for symbolic, process algebraic specifications. Our method essentially consists of three phases: (1) the control flow in the PBES is reconstructed, detecting control flow parameters that were encoded in the description of the process, as well as control flow parameters that were introduced during the construction of the PBES; (2) we use a data flow analysis based on the control flow in the PBES to detect irrelevant data parameters and (3) we reset those data parameters of the equations in the PBES that were found to be irrelevant. Our reduction preserves the solution to the PBES, and never increases the size of the underlying Boolean equation system. The reduction is evaluated using a number of case studies