Verifying Reachability Properties in Markov Chains via Incremental Induction

There is a scalability gap between probabilistic and non-probabilistic verification. Probabilistic model checking tools are based either on explicit engines or on (Multi-Terminal) Binary Decision Diagrams. These structures are complemented in areas of non-probabilistic verification by more scalable techniques, such as IC3. We present a symbolic probabilistic model checking algorithm based on IC3-like incremental construction of inductive clauses to partition the state space, interleaved with incremental construction of a system of linear inequalities. This paper compares our implementation to standard quantitative verification alternatives: our experiments show that our algorithm is a step to more scalable symbolic verification of rare events in finite-state Markov chains.