Publication Type

Conference Proceeding Article

Version

publishedVersion

Publication Date

5-2014

Abstract

Markov decision processes (MDPs) are extensively used to model systems with both probabilistic and nondeterministic behavior. The problem of calculating the probability of reaching certain system states (hereafter reachability analysis) is central to the MDP-based system analysis. It is known that existing approaches on reachability analysis for MDPs are often inefficient when a given MDP contains a large number of states and loops, especially with the existence of multiple probability distributions. In this work, we propose a method to eliminate strongly connected components (SCCs) in an MDP using a divide-and-conquer algorithm, and actively remove redundant probability distributions in the MDP based on the convex property. With the removal of loops and parts of probability distributions, the probabilistic reachability analysis can be accelerated, as evidenced by our experiment results.

Keywords

Convex Hull, Model Check, Markov Decision Process, Discrete Time Markov Chain, Reachability Analysis

Discipline

Programming Languages and Compilers | Software Engineering

Research Areas

Software and Cyber-Physical Systems

Publication

Proceedings of the 16th International Conference on Formal Engineering Methods, ICFEM 2014, Luxembourg, November 3–5

First Page

171

Last Page

186

ISBN

9783319117362

Identifier

10.1007/978-3-319-11737-9_12

Publisher

Springer Link

City or Country

Luxembourg

Additional URL

https://doi.org/10.1007/978-3-319-11737-9_12

Download

Share

COinS