Multi-Objective Model Checking of Markov Decision Processes

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 r\_i ε[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 r\_i. 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.

21 pages, 2 figures

Cited by in corpus (11)

• Markov Decision Processes with Multiple Long-run Average Objectives
• Permissive Controller Synthesis for Probabilistic Systems
• The Complexity of Nash Equilibria in Simple Stochastic Multiplayer Games
• Decision Problems for Nash Equilibria in Stochastic Games
• Safety-Constrained Reinforcement Learning for MDPs
• Stochastic Games with Disjunctions of Multiple Objectives (Technical Report)
• Stochastic Games with Disjunctions of Multiple Objectives
• Simple Strategies in Multi-Objective MDPs (Technical Report)
• Decidability Results for Multi-objective Stochastic Games
• Pareto Curves for Probabilistic Model Checking
• Synthesis of Optimal Resilient Control Strategies