| |
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: 1797 |
 Creative Commons | |
