Skip to Main content Skip to Navigation
Conference papers

Dirac-Based Reduction Techniques for Quantitative Analysis of Discrete-Time Markov Models

Abstract : Iterative methods are widely used in probabilistic model checking to compute quantitative reachability values. Redundant computation is a significant drawback of iterative methods that affects the performance of probabilistic model checking. In this paper we propose a new approach to avoid redundant computations for reachability analysis of discrete-time Markov processes. Redundant computations can be avoided by considering transitions with Dirac distributions. If two states of a Markov chain are connected with a Dirac transition, the iterative method can postpone the update of the source state until the value of the destination state is computed. Using this approach, we propose two heuristics to improve the performance of iterative methods for computing unbounded reachability probabilities in discrete-time Markov chains and Markov decision processes. The proposed heuristics can be lifted to the computations of expected rewards and have been implemented in PRISM model checker. Several standard case studies have been used and experimental results show that our heuristics outperform most well-known previous iterative methods.
Document type :
Conference papers
Complete list of metadata
Contributor : Hal Ifip Connect in order to contact the contributor
Submitted on : Wednesday, March 10, 2021 - 4:05:17 PM
Last modification on : Wednesday, March 10, 2021 - 4:09:46 PM
Long-term archiving on: : Friday, June 11, 2021 - 7:06:57 PM


 Restricted access
To satisfy the distribution rights of the publisher, the document is embargoed until : 2023-01-01

Please log in to resquest access to the document


Distributed under a Creative Commons Attribution 4.0 International License



Mohammadsadegh Mohagheghi, Behrang Chaboki. Dirac-Based Reduction Techniques for Quantitative Analysis of Discrete-Time Markov Models. 3rd International Conference on Topics in Theoretical Computer Science (TTCS), Jul 2020, Tehran, Iran. pp.1-16, ⟨10.1007/978-3-030-57852-7_1⟩. ⟨hal-03165383⟩



Record views