Y.: Symbolic approximation of the bounded reachability probability in large Markov chains

Abstract. 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.