Reductions for Parity Games and Model Checking

Thomas Neele

first promotor: T.A.C. Willemse (TU/e)
second promotor: J.F. Groote (TU/e)
Eindhoven University of Technology
Date: 16 September, 2020
Thesis: PDF


The design and implementation of software systems has long been recognised to be a difficult task. In the field of theoretical computer science, formal methods aim to assist the design process by providing mathematical theories that allow one to reason about the behaviour of (concurrent) processes. One of the most effective techniques for
analysing concurrent behaviour is model checking, which has seen many applications over the past 40 years. A typical model checking algorithm takes a high-level specification of a system’s behaviour and a requirement in the shape of a formal property and checks whether the transition system underlying the specification atisfies the property. A fundamental challenge in model checking is the so-called state-space explosion: the arbitrary interleaving of the behaviour of many parallel processes causes an exponential blow-up in the size of the underlying transition system.

This thesis explores several new techniques that aim to address the state-space explosion problem by reducing parity games and their high-level encoding, parameterised Boolean equations systems (PBESs). A PBES is a sequence of Boolean equations augmented with data, where each
equation is furthermore labelled with a fixpoint, allowing one to distinguish the largest and smallest solutions. PBESs can encode many types of decision problems, among them model checking problems.
Computing the solution to a PBES answers the decision problem it encodes. PBES solving often involves generating its underlying parity game, which frequently are very large due to the state-space explosion, motivating the application of reduction techniques. All of the reductions we propose exploit the fact that PBESs allows very coarse abstractions, while (partially) preserving their solution. The contents of the thesis can be divided up into three parts.

The first part discusses symbolic techniques that enable solving of PBESs with an infinite underlying parity game. As a prerequisite, we introduce a normal form for PBESs that enables symbolic reasoning about the transitions it induces in the underlying game. The solving procedures proposed here perform partition refinement, based on a bisimulation relation between the nodes of the parity game. This
technique is provably more general than similar techniques for behavioural specifications. Furthermore, experimental results show that it also outperforms other tools. Our tool is the first implementation of
a semi-decision procedure for deciding bisimilarity of arbitrary infinite processes.

The second part of the thesis discusses partial-order reduction (POR), which is a technique that aims to deal with the state-space explosion problem by not exploring all similar interleavings of parallel
processes. First, we identify a theoretical problem in related work and show that one variant of POR is not guaranteed to preserve linear-time properties, contrary to what is claimed in an often-cited theorem. We propose a solution and show exactly in which derivative works the problem manifests itself. Subsequently, we apply partial-order reduction to PBESs and parity games. Compared to traditional POR approaches that operate on transition systems, this has the benefit that POR can also be
applied when checking stutter-sensitive properties. Furthermore, the property is automatically taken into consideration during the reduction. Experiments show that substantial reductions can be achieved.

The final part deals with PBESs that contain quantifiers over data. Quantifiers that have a larger-than-necessary scope can cause the underlying parity game to grow unnecessarily. We introduce several
techniques for transforming PBESs with quantifiers and show how their scope can be reduced. Furthermore, we discuss guards for PBESs: expressions that characterise when two equations depend on each other. Guards are a fundamental tool in several other static analysis techniques. The guards we compute are stronger than those proposed before, and thus contain more information on dependencies.