some image logo

HOME

SEARCH

CURRENT ISSUE

REGULAR ISSUES

   Volume 1 (2005)

   Volume 2 (2006)

   Volume 3 (2007)

   Volume 4 (2008)

      Issue 1

      Issue 2

      Issue 3

      Issue 4

   Volume 5 (2009)

   Volume 6 (2010)

   Volume 7 (2011)

   Volume 8 (2012)

   Volume 9 (2013)

   Volume 10 (2014)

   Volume 11 (2015)

   Volume 12 (2016)

   Volume 13 (2017)

SPECIAL ISSUES

SURVEY ARTICLES

AUTHORS

ABOUT

SERVICE

LOGIN

FAQ

SUPPORT

CONTACT

VOLUME 4, ISSUE 4, PAPER 8


Multi-Objective Model Checking of Markov Decision Processes

©Kousha Etessami, University of Edinburgh
©Marta Kwiatkowska, Oxford University
©Moshe Y. Vardi, Rice University
©Mihalis Yannakakis, Columbia University

Abstract
We study and provide efficient algorithms for multi-objective model checking problems for Markov Decision Processes (MDPs). Given an MDP, M, and given multiple linear-time (ω-regular or LTL) properties φi, and probabilities ri[0,1], i=1,...,k, we ask whether there exists a strategy σ for the controller such that, for all i, the probability that a trajectory of M controlled by σ satisfies φi is at least ri. We provide an algorithm that decides whether there exists such a strategy and if so produces it, and which runs in time polynomial in the size of the MDP. Such a strategy may require the use of both randomization and memory. We also consider more general multi-objective ω-regular queries, which we motivate with an application to assume-guarantee compositional reasoning for probabilistic systems.
Note that there can be trade-offs between different properties: satisfying property φ1 with high probability may necessitate satisfying φ2 with low probability. Viewing this as a multi-objective optimization problem, we want information about the "trade-off curve" or Pareto curve for maximizing the probabilities of different properties. We show that one can compute an approximate Pareto curve with respect to a set of ω-regular properties in time polynomial in the size of the MDP.
Our quantitative upper bounds use LP methods. We also study qualitative multi-objective model checking problems, and we show that these can be analysed by purely graph-theoretic methods, even though the strategies may still require both randomization and memory.

Publication date: November 12, 2008

Full Text: PDF | PostScript
DOI: 10.2168/LMCS-4(4:8)2008

Hit Counts: 8709

Creative Commons