TY - GEN

T1 - Reasoning about MDPs as transformers of probability distributions

AU - Korthikanti, Vijay Anand

AU - Viswanathan, Mahesh

AU - Agha, Gul

AU - Kwon, Young Min

N1 - Copyright:
Copyright 2010 Elsevier B.V., All rights reserved.

PY - 2010

Y1 - 2010

N2 - We consider Markov Decision Processes (MDPs) as transformers on probability distributions, where with respect to a scheduler that resolves nondeterminism, the MDP can be seen as exhibiting a behavior that is a sequence of probability distributions. Defining propositions using linear inequalities, one can reason about executions over the space of probability distributions. In this framework, one can analyze properties that cannot be expressed in logics like PCTL*, such as expressing bounds on transient rewards and expected values of random variables, and comparing the probability of being in one set of states at a given time with that of being in another set of states. We show that model checking MDPs with this semantics against ω-regular properties is in general undecidable. We then identify special classes of propositions and schedulers with respect to which the model checking problem becomes decidable. We demonstrate the potential usefulness of our results through an example.

AB - We consider Markov Decision Processes (MDPs) as transformers on probability distributions, where with respect to a scheduler that resolves nondeterminism, the MDP can be seen as exhibiting a behavior that is a sequence of probability distributions. Defining propositions using linear inequalities, one can reason about executions over the space of probability distributions. In this framework, one can analyze properties that cannot be expressed in logics like PCTL*, such as expressing bounds on transient rewards and expected values of random variables, and comparing the probability of being in one set of states at a given time with that of being in another set of states. We show that model checking MDPs with this semantics against ω-regular properties is in general undecidable. We then identify special classes of propositions and schedulers with respect to which the model checking problem becomes decidable. We demonstrate the potential usefulness of our results through an example.

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

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

U2 - 10.1109/QEST.2010.35

DO - 10.1109/QEST.2010.35

M3 - Conference contribution

AN - SCOPUS:78649487899

SN - 9780769541884

T3 - Proceedings - 7th International Conference on the Quantitative Evaluation of Systems, QEST 2010

SP - 199

EP - 208

BT - Proceedings - 7th International Conference on the Quantitative Evaluation of Systems, QEST 2010

T2 - 7th International Conference on the Quantitative Evaluation of Systems, QEST 2010

Y2 - 15 September 2010 through 18 September 2010

ER -