Symbolic Approximation of the Bounded Reachability Probability in Large Markov Chains

  • Markus N. Rabe
  • Christoph M. Wintersteiger
  • Hillel Kugler
  • Boyan Yordanov
  • Youssef Hamadi
Conference paper

DOI: 10.1007/978-3-319-10696-0_30

Part of the Lecture Notes in Computer Science book series (LNCS, volume 8657)
Cite this paper as:
Rabe M.N., Wintersteiger C.M., Kugler H., Yordanov B., Hamadi Y. (2014) Symbolic Approximation of the Bounded Reachability Probability in Large Markov Chains. In: Norman G., Sanders W. (eds) Quantitative Evaluation of Systems. QEST 2014. Lecture Notes in Computer Science, vol 8657. Springer, Cham

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. 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 experimental evaluation on PRISM benchmark models we demonstrate the feasibility of the approach on models that are out of reach for previous methods.

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

Copyright information

© Springer International Publishing Switzerland 2014

Authors and Affiliations

  • Markus N. Rabe
    • 1
  • Christoph M. Wintersteiger
    • 2
  • Hillel Kugler
    • 2
  • Boyan Yordanov
    • 2
  • Youssef Hamadi
    • 2
  1. 1.Saarland UniversityGermany
  2. 2.Microsoft ResearchU.S.A.

Personalised recommendations