10.1007/978-3-642-54830-7_14
Chatterjee, Krishnendu
Krishnendu
Chatterjee0000-0002-4561-241X
Doyen, Laurent
Laurent
Doyen
Gimbert, Hugo
Hugo
Gimbert
Oualhadj, Youssouf
Youssouf
Oualhadj
Perfect-information stochastic mean-payoff parity games
LNCS
Springer
2014
2018-12-11T11:56:21Z
2020-01-21T13:19:22Z
conference
https://research-explorer.app.ist.ac.at/record/2212
https://research-explorer.app.ist.ac.at/record/2212.json
The theory of graph games is the foundation for modeling and synthesizing reactive processes. In the synthesis of stochastic processes, we use 2 1/2-player games where some transitions of the game graph are controlled by two adversarial players, the System and the Environment, and the other transitions are determined probabilistically. We consider 2 1/2-player games where the objective of the System is the conjunction of a qualitative objective (specified as a parity condition) and a quantitative objective (specified as a mean-payoff condition). We establish that the problem of deciding whether the System can ensure that the probability to satisfy the mean-payoff parity objective is at least a given threshold is in NP ∩ coNP, matching the best known bound in the special case of 2-player games (where all transitions are deterministic). We present an algorithm running in time O(d·n2d·MeanGame) to compute the set of almost-sure winning states from which the objective can be ensured with probability 1, where n is the number of states of the game, d the number of priorities of the parity objective, and MeanGame is the complexity to compute the set of almost-sure winning states in 2 1/2-player mean-payoff games. Our results are useful in the synthesis of stochastic reactive systems with both functional requirement (given as a qualitative objective) and performance requirement (given as a quantitative objective).