The following technical report is available from http://aib.informatik.rwth-aachen.de: http://aib.informatik.rwth-aachen.de/
The Probabilistic Model Checker Storm — Symbolic Methods for Probabilistic Model Checking Christian Hensel AIB 2018-06
In a world in which we increasingly rely on safety critical systems that simultaneously are becoming ever more complex, formal methods provide a means to mathematically rigorously prove systems correct. Model checking is a fully automated technique that is successfully applied in the verification of software and hardware circuits. However, in practice many systems exhibit stochastic behavior, for instance when components may fail or randomization is used as a key element to improve efficiency. Probabilistic model checking extends traditional (qualitative) model checking to deal with such systems. As model checking can be (simplistically) viewed as an exhaustive exploration of the state space of the model under consideration, it suffers from the curse of dimensionality: State spaces grow exponentially in the number of components and variables and they quickly become too large to be effectively manageable, a problem that is typically referred to as state space explosion.
Symbolic methods have helped to alleviate this problem substantially. Rather than considering states and transitions of the system individually, they instead exploit structure in the model and treat sets of states and transitions simultaneously. Model checkers based on symbolic techniques dominate the landscape of hardware and software model checking. In the probabilistic setting, symbolic methods too show potential but are arguably not on par with their qualitative counterparts. This thesis is concerned with advances in the field of symbolic techniques in the context of probabilistic model checking. The major contributions are fivefold:
(1) We propose the JANI modeling language to unify the multitude of input languages of probabilistic model checkers. It covers a large range of models involving randomization and timing aspects and offers well-defined points for future extensions. (2) We show how counterexamples on the level of JANI specifications can be synthesized. For this, we develop a method based on the connection of standard probabilistic model checking and a smart enumeration of the solutions of a satisfiability problem. (3) We combine the strengths of decision diagrams for the representation of gigantic systems and bisimulation minimization, a technique that reduces systems by factoring out symmetry. Our implementation is shown to drastically reduce the sizes of models involving probabilities, continuous time, nondeterminism and rewards. (4) We summarize, extend and implement a game-based abstraction-refinement framework that is able to treat infinite-state probabilistic automata. In contrast to other implementations, ours is openly available and computes strictly sound bounds through the use of rational arithmetic. (5) We present Storm, a new high-performance probabilistic model checker. It goes beyond the standard verification tasks through numerous features and in particular integrates the items (1) to (4) above. We show that it outperforms other state-of-the-art model checkers on the majority of instances of the PRISM benchmark suite.