Share on Facebook Tweet on Twitter Share on LinkedIn Share by email
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

Abstract

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.

Details

Publication typeTechReport
NumberMSR-TR-2014-74
> Publications > Symbolic Approximation of the Bounded Reachability Probability in Large Markov Chains (Extended)