Dealing with large state spaces


Matthias Kuntz


28th Feb. 2008






The verification of quantitative aspects like performance and dependability, by means of model checking has become an important and vivid area of research over the past decade. Example results of this research are the logics CSL (continuous stochastic logic) and SPDL (stochastic propositional dynamic logic) and their corresponding model checking algorithms. The evaluation of properties expressed in CSL/SPDL makes it necessary to solve large systems of linear (differential) equations, usually by means of numerical analysis. Both the inherent time and especially space complexity of the numerical algorithms make it practically infeasible to model check systems with more than some 100 million states, whereas realistic system models may have billions of states. A possible solution of this problem is to replace the original state space with a probabilistically equivalent, but smaller one. In this talk, two different approaches to this problem will be presented:

1. Property-driven state space generation:

For model-checking a highly relevant class of CSL/SPDL formulae (probabilistic path formulae) it is possible to drastically reduce the state space size during the model checking procedure. Here, an approach is presented, that directly generates this reduced state space from a given high-level system specification and the CSL/SPDL property that is to be verified, thus avoiding the generation of a unnecessarily large system model.

2. Markovian bisimulation:

The most prominent equivalence relation is bisimulation, for which also a stochastic variant exists (Markovian bisimulation). Markovian bisimulation allows for a substantial reduction of the state space size. But, these savings in space come at the cost of an increased time complexity for the computation of the bisimulation quotient. In this talk, the results of both a serial and distributed implementation of a Markovian bisimulation algorithm (aimed at CSL model checking) will be presented.