Counterexamples in Probabilistic Verification

The topic of this thesis is roughly to be classified into the formal verification of probabilistic systems. In particular, the generation of counterexamples for discrete-time Markov Models is investigated. A counterexample for discrete-time Markov Chains (DTMCs) is classically defined as a (finite) set of paths. In this work, this set of paths is represented symbolically as a critical part of the original system, a so-called critical subsystem. This notion is extended to Markov decision processes (MDPs) and probabilistic automata (PAs). The results are introduced in four parts:

1. A model checking algorithm for DTMCs based on a decomposition of the system’s graph in strongly connected components (SCCs). This approach is extended to parametric discrete-time Markov Chains.

2. The generation of counterexamples for DTMCs and reachability properties based on graph algorithms. A hierarchical abstraction scheme to compute abstract counterexamples is presented, followed by a general framework for both explicitly represented systems and symbolically represented systems using binary decision diagrams (BDDs).

3. The computation of minimal critical subsystems using SAT modulo theories (SMT) solving and mixed integer linear programming (MILP). This is investigated for reachability properties and ω-regular properties on DTMCs, MDPs, and PAs.

4. A new concept of high-level counterexamples for PAs. Markov models can be specified by means of a probabilistic programming language. An approach for computing critical parts of such a symbolic description of a system is presented, yielding human-readable counterexamples.

All results have been published in conference proceedings or journals. A thorough evaluation on common benchmarks is given comparing all methods and also competing with available implementations of other approaches.