Reasoning about MDPs as transformers of probability distributions

Vijay Anand Korthikanti, Mahesh Viswanathan, Gul Agha, Young Min Kwon

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Abstract

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.

Original languageEnglish (US)
Title of host publicationProceedings - 7th International Conference on the Quantitative Evaluation of Systems, QEST 2010
Pages199-208
Number of pages10
DOIs
StatePublished - 2010
Event7th International Conference on the Quantitative Evaluation of Systems, QEST 2010 - Williamsburg, VA, United States
Duration: Sep 15 2010Sep 18 2010

Publication series

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

Other

Other7th International Conference on the Quantitative Evaluation of Systems, QEST 2010
Country/TerritoryUnited States
CityWilliamsburg, VA
Period9/15/109/18/10

ASJC Scopus subject areas

  • Control and Systems Engineering

Fingerprint

Dive into the research topics of 'Reasoning about MDPs as transformers of probability distributions'. Together they form a unique fingerprint.

Cite this