Multidimensional beyond worst-case and almost-sure problems for mean-payoff objectives

Abstract

The beyond worst-case threshold problem (BWC), recently introduced by Bruyère et al., asks given a quantitative game graph for the synthesis of a strategy that i) enforces some minimal level of performance against any adversary, and ii) achieves a good expectation against a stochastic model of the adversary. They solved the BWC problem for finite-memory strategies and unidimensional mean-payoff objectives and they showed membership of the problem in NP$\cap$coNP. They also noted that infinite-memory strategies are more powerful than finite-memory ones, but the respective threshold problem was left open. We extend these results in several directions. First, we consider multidimensional mean-payoff objectives. Second, we study both finite-memory and infinite-memory strategies. We show that the multidimensional BWC problem is coNP-complete in both cases. Third, in the special case when the worst-case objective is unidimensional (but the expectation objective is still multidimensional) we show that the complexity decreases to NP$\cap$coNP. This solves the infinite-memory threshold problem left open by Bruyère et al., and this complexity cannot be improved without improving the currently known complexity of classical mean-payoff games. Finally, we introduce a natural relaxation of the BWC problem, the beyond almost-sure threshold problem (BAS), which asks for the synthesis of a strategy that ensures some minimal level of performance with probability one and a good expectation against the stochastic model of the adversary. We show that the multidimensional BAS threshold problem is solvable in P.