Abstract
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. In this article, we present a new algorithm and its implementation that improves approximate results obtained by scalable techniques like value iteration to compute exact reachability probabilities.
Download
We have implemented our technique in our tool RationalSearch.
Download RationalSearch here . Instructions for setting up RationalSearch are underway.
RationalSearch is implemented as an extension of PRISM .
We thank PRISM developers for helping us setting up PRISM .
Contributors
References
- Exact Quantitative Model Checking Through Rational Search
Matthew S. Bauer, Umang Mathur, Rohit Chadha, A. P. Sistla, Mahesh Viswanathan
Proceedings of International Conference on Formal Methods in Computer-Aided Design (FMCAD), 2017, to appear
Contact
-
Email: umathur3@illinois.edu, msbauer2@illinois.edu
