Symbolic Approximation of the Bounded Reachability Probability in Large Markov Chains

Markus N. Rabe, Christoph M. Wintersteiger, Hillel Kugler, Boyan Yordanov, and Youssef Hamadi

We present a novel technique to analyze the bounded reach- ability probability problem for large Markov chains. The essential idea is to incrementally search for sets of paths that lead to the goal region and to choose the sets in a way that allows us to easily determine the prob- ability mass they represent. To effectively analyze the system dynamics using an SMT solver, we employ a finite-precision abstraction on the Markov chain and a custom quantifier elimination strategy. Through ex- perimental evaluation on PRISM benchmark models we demonstrate the feasibility of the approach on models that are out of reach for previous methods.
Errata: (1) page 5, proposition 1: The sequence of r variables should start with r_1 instead of r_0.

11th International Conference on Quantitative Evaluation of SysTems (QEST 2014).

Copyright by Springer.

(pdf)