Symbolic Approximation of the Bounded Reachability Probability in Large Markov Chains (Extended)

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

23 May 2014

We present a novel technique to analyse the bounded reachability 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 to easily determine the probability mass they represent. To effectively dispatch the resulting formulas using an SMT solver, we employ a finite-precision abstraction on the Markov chain and a custom quantifier elimination strategy. Through experimental evaluation on PRISM benchmark models we demonstrate the feasibility of the approach on models that are out of reach for previous methods.

Publication type | TechReport |

Number | MSR-TR-2014-74 |

- Analyzing and Synthesizing Genomic Logic Functions
- Efficiently Solving Quantified Bit-Vector Formulas
- The Rhapsody Semantics of Statecharts

> Publications > Symbolic Approximation of the Bounded Reachability Probability in Large Markov Chains (Extended)