TY - GEN

T1 - Model checking MDPs with a unique compact invariant set of distributions

AU - Chadha, Rohit

AU - Korthikanti, Vijay Anand

AU - Viswanathan, Mahesh

AU - Agha, Gul

AU - Kwon, Youngmin

PY - 2011

Y1 - 2011

N2 - The semantics of Markov Decision Processes (MDPs), when viewed as transformers of probability distributions, can described as a labeled transition system over the probability distributions over the states of the MDP. The MDP can be seen as defining a set of executions, where each execution is a sequence of probability distributions. Reasoning about sequences of distributions allows one to express properties not expressible in logics like PCTL, examples include expressing bounds on transient rewards and expected values of random variables, as well as comparing the probability of being in one set of states at a given time with another set of states. With respect to such a semantics, the problem of checking that the MDP never reaches a bad distribution is undecidable [10]. In this paper, we identify a special class of MDPs called semi-regular MDPs that have a unique non-empty, compact, invariant set of distributions, for which we show that checking any ω-regular property is decidable. Our decidability result also implies that for semi-regular probabilistic finite automata with isolated cut-points, the emptiness problem is decidable.

AB - The semantics of Markov Decision Processes (MDPs), when viewed as transformers of probability distributions, can described as a labeled transition system over the probability distributions over the states of the MDP. The MDP can be seen as defining a set of executions, where each execution is a sequence of probability distributions. Reasoning about sequences of distributions allows one to express properties not expressible in logics like PCTL, examples include expressing bounds on transient rewards and expected values of random variables, as well as comparing the probability of being in one set of states at a given time with another set of states. With respect to such a semantics, the problem of checking that the MDP never reaches a bad distribution is undecidable [10]. In this paper, we identify a special class of MDPs called semi-regular MDPs that have a unique non-empty, compact, invariant set of distributions, for which we show that checking any ω-regular property is decidable. Our decidability result also implies that for semi-regular probabilistic finite automata with isolated cut-points, the emptiness problem is decidable.

KW - Markov Decision Processes

KW - Model Checking

KW - Probability Distributions

KW - Semantics

UR - http://www.scopus.com/inward/record.url?scp=80055053126&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=80055053126&partnerID=8YFLogxK

U2 - 10.1109/QEST.2011.22

DO - 10.1109/QEST.2011.22

M3 - Conference contribution

AN - SCOPUS:80055053126

SN - 9780769544915

T3 - Proceedings of the 2011 8th International Conference on Quantitative Evaluation of Systems, QEST 2011

SP - 121

EP - 130

BT - Proceedings of the 2011 8th International Conference on Quantitative Evaluation of Systems, QEST 2011

T2 - 2011 8th International Conference on Quantitative Evaluation of Systems, QEST 2011

Y2 - 5 September 2011 through 8 September 2011

ER -