Verifying Reachability Properties in Markov Chains via Incremental Induction

TL;DR

This paper introduces an incremental symbolic verification method for Markov chains that combines IC3-like techniques with linear inequalities, improving scalability for verifying rare probabilistic events.

Contribution

It presents a novel incremental verification algorithm that integrates IC3-inspired clause construction with linear inequality systems for probabilistic model checking.

Findings

Outperforms standard methods in scalability for rare event verification

Demonstrates effectiveness on finite-state Markov chains

Provides a new approach combining symbolic techniques with probabilistic analysis

Abstract

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.