Exact quantitative probabilistic model checking through rational search

Umang Mathur, Matthew S. Bauer, Rohit Chadha, A. Prasad Sistla, Mahesh Viswanathan

Research output: Contribution to journalArticlepeer-review


Model checking systems formalized using probabilistic models such as discrete time Markov chains (DTMCs) and Markov decision processes (MDPs) can be reduced to computing constrained reachability properties. Linear programming methods to compute reachability probabilities for DTMCs and MDPs do not scale to large models. Thus, model checking tools often employ iterative methods to approximate reachability probabilities. These approximations can be far from the actual probabilities, leading to inaccurate model checking results. On the other hand, specialized techniques employed in existing state-of-the-art exact quantitative model checkers, don’t scale as well as their iterative counterparts. In this work, we present a new model checking algorithm that improves the approximate results obtained by scalable iterative techniques to compute exact reachability probabilities. Our techniques are implemented as an extension of the PRISM model checker and are evaluated against other exact quantitative model checking engines.

Original languageEnglish (US)
Pages (from-to)90-126
Number of pages37
JournalFormal Methods in System Design
Issue number1-3
StatePublished - Dec 2020


  • Exact quantitative model checking
  • Markov chains
  • Markov decision processes
  • Probabilistic systems

ASJC Scopus subject areas

  • Software
  • Theoretical Computer Science
  • Hardware and Architecture


Dive into the research topics of 'Exact quantitative probabilistic model checking through rational search'. Together they form a unique fingerprint.

Cite this