SCC-based improved reachability analysis for Markov decision processes

• Main Authors: GUI, Lin, SUN, Jun, SONG, Songzheng, LIU, Yang, DONG, Jin Song
• Format: text
• Language: English
• Published: Institutional Knowledge at Singapore Management University 2014
• Subjects: Convex Hull; Model Check; Markov Decision Process; Discrete Time Markov Chain; Reachability Analysis; Programming Languages and Compilers; Software Engineering
• Online Access: https://ink.library.smu.edu.sg/sis_research/4985; https://ink.library.smu.edu.sg/context/sis_research/article/5988/viewcontent/scc_based_improved.pdf
• Institution: Singapore Management University

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.