Percentile Queries in Multi-Dimensional Markov Decision Processes

TL;DR

This paper investigates the complexity of percentile queries in multi-dimensional Markov decision processes, providing algorithms for strategy synthesis to meet multiple probabilistic constraints across various payoff functions.

Contribution

It introduces algorithms for synthesizing strategies in multi-dimensional weighted MDPs to satisfy percentile constraints for multiple objectives, extending existing models to the quantitative case.

Findings

Algorithms for strategy synthesis under percentile constraints.

Extension of multi-objective model checking to quantitative MDPs.

Analysis of complexity for various payoff functions.

Abstract

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. 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 $f$, thresholds $v_i$ (one per dimension), and probability thresholds $\alpha_i$, we show how to compute a single strategy to enforce that for all dimensions $i$, the probability of outcomes $\rho$ satisfying $f_i(\rho) \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.