Partial-order reduction for parity games and parameterised Boolean equation systems

AbstractIn model checking, reduction techniques can be helpful tools to fight the state-space explosion problem. Partial-order reduction (POR) is a well-known example, and many POR variants have been developed over the years. However, none of these can be used in the context of model checking stutter-sensitive temporal properties. We propose POR techniques for parity games, a well-established formalism for solving a variety of decision problems, including model checking. As a result, we obtain the first POR method that is sound for the full modal $$\upmu $$ μ -calculus. We show how our technique can be applied to the fixed point logic called parameterised Boolean equation systems, which pro…