Advanced Reduction Techniques for Model Checking

Jeroen Keiren

Promotor: prof.dr.ir. J.F. Groote (TU/e)
Co-promotor: dr.ir. T.A.C Willemse (TU/e)
Technische Universiteit Eindhoven
Date: 17 September, 2013, 14:00
Thesis: PDF

Summary

Modern-day software systems are highly complex, and typically consist of a number of interacting components running in parallel. Verification methods aim to prove correctness of such systems. Model checking is a commonly used verification technique, in which a model of the system under investigation is created. Subsequently, it is checked whether this model satisfies certain properties.

Model checking suffers from the infamous state space explosion problem: the number of states in a system grows exponentially in the number of parallel components. Part of the blow-up is also due to the presence of data in descriptions of model checking problems. Typically model checkers construct the full state space, causing the approach to break down already for a small number of parallel components. Properties are then checked on the state space, either directly, or by first combining the state space with a property, leading to, for example, a Boolean equation system or a parity game. The latter step leads to a further blow up.

In this thesis techniques are developed to counter this state space explosion problem in (parameterised) Boolean equation systems and parity games. The main contributions are as follows:

  • A structural operational semantics is presented that can equip Boolean equation systems with arbitrary right hand sides with a graph structure, called structure graph. Classical graph structures for analysing Boolean equation systems typically restrict right hand sides to purely conjunctive or disjunctive form, essentially reducing the equation system to a parity game. We use our graphs to study the effects of this restriction on right hand sides, and show that, in the context of bisimulation, this reduction never poses a disadvantage.
  • We investigate the reductions that can be achieved using strong bisimulation reduction of structure graphs, and we investigate idempotence identifying bisimulation. We show that, although it indeed identifies idempotence in a restricted subset of equation systems, it does not live up to its name for full-blown structure graphs.
  • The insights we gain by studying structure graphs motivate further investigation of weaker equivalences in the setting of parity games. Since the winner in parity games is determined by the infinitely often recurring priorities, intuitively, finite stretches of similar vertices can be compressed. We define the notions of stuttering equivalence and governed stuttering equivalence, and show that they preserve the winner in a parity game.
  • A new set of benchmarks for parity games is developed due to the unavailability of standard benchmarks. These benchmarks subsume the examples that are used for performance evaluation of solving algorithms in the literature. We provide a description of the benchmarks, and we analyse their characteristics. The efficacy of our equivalences for reducing parity games is evaluated using this set of benchmarks. It is shown that large reductions are possible, even reducing parity games to a single vertex with a self-loop. Average reductions of about 50% are achieved. Sometimes the technique allows solving parity games which cannot be solved directly; in general, however, the timing results do not show a clear advantage.
  • Finally, we move from a posteriori reduction of parity games, to static analysis techniques for parameterised Boolean equation systems, that allow the a priori reduction of the induced parity games. Essentially, we present a heuristic that performs a live variable analysis. We show that this analysis is more effective at reducing the complexity than existing techniques, i.e. the reductions that we obtain are larger. Correctness of our analysis is shown using a generalisation of the equivalences that we introduced for parity games and Boolean equation systems.