Symbolic Approximation of the Bounded Reachability Probability in Large Markov Chains
Abstract:
We present a novel technique to analyze 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 that allows us to easily determine the probability mass they represent.
We encode the search for sets of paths as a sequence of quantified bitvector problems. To effectively discharge the quantified bit vector problems using an SMT solver, we employ a finite-precision abstraction on the Markov chain and a custom quantifier elimination strategy. The experimental evaluation on the PRISM benchmark models demonstrates that the approach scales to models that are out of reach for previous methods.