June 1, 2015Mickaël Randour (LSV - Ens Cachan)
Markov decision processes (MDPs) with multi-dimensional weights are useful to analyze systems with multiple objectives that may be conflicting and require the analysis of trade-offs. In this work, we study the complexity of percentile queries in such MDPs and give algorithms to synthesize strategies that enforce such constraints. Given a multi-dimensional weighted MDP and a quantitative payoff function~$, thresholds $ (one per dimension), and probability thresholds $alpha_i$, we show how to compute a single strategy to enforce that for all dimensions $, the probability of outcomes $
ho$ satisfying (
ho) geq v_i$ is at least $alpha_i$. We consider classical quantitative payoffs from the literature (sup, inf, lim sup, lim inf, mean-payoff, truncated sum, discounted sum). Our work extends to the quantitative case the multi-objective model checking problem studied by Etessami et al. in unweighted MDPs. Joint work with Jean-François Raskin and Ocan Sankur.