IDEALS Home University of Illinois at Urbana-Champaign logo The Alma Mater The Main Quad

Reasoning About MDPs as Transformers of Probability Distributions

Show full item record

Bookmark or cite this item:

Files in this item

File Description Format
PDF mdptransdist.pdf (404KB) MDP_TRANS_DIST PDF
Title: Reasoning About MDPs as Transformers of Probability Distributions
Author(s): Korthikanti, Vijay Anand; Viswanathan, Mahesh; Kwon, YoungMin; Agha, Gul A.
Subject(s): Markov Decision Processes Probability Distributions Semantics Model Checking
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 $\omega$-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.
Issue Date: 2010
Type: Text
Publication Status: published or submitted for publication
Date Available in IDEALS: 2010-06-26

This item appears in the following Collection(s)

Show full item record

Item Statistics

  • Total Downloads: 128
  • Downloads this Month: 1
  • Downloads Today: 0


My Account


Access Key