Multi-objective Model Checking of Markov Decision Processes

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. Viewin...

• Type: Conference
• Year: 2007
• Where: TACAS
• Authors: Kousha Etessami, Marta Z. Kwiatkowska, Moshe Y. Vardi, Mihalis Yannakakis
• Keywords: Algorithms, Model Checking Problems, Multi-objective Model Checking, Pareto Curve, TACAS 2007