TY - GEN

T1 - A pseudo-quasi-polynomial algorithm for mean-payoff parity games

AU - Daviaud, Laure

AU - Jurdziński, Martin

AU - Lazić, Ranko

N1 - Funding Information:
This research has been supported by the EPSRC grant EP/P020992/1 (Solving Parity Games in Theory and Practice).
Publisher Copyright:
© 2018 ACM.

PY - 2018/7/9

Y1 - 2018/7/9

N2 - In a mean-payoff parity game, one of the two players aims both to achieve a qualitative parity objective and to minimize a quantitative long-term average of payoffs (aka. mean payoff). The game is zero-sum and hence the aim of the other player is to either foil the parity objective or to maximize the mean payoff. Our main technical result is a pseudo-quasi-polynomial algorithm for solving mean-payoff parity games. All algorithms for the problem that have been developed for over a decade have a pseudo-polynomial and an exponential factors in their running times; in the running time of our algorithm the latter is replaced with a quasi-polynomial one. By the results of Chatterjee and Doyen (2012) and of Schewe, Weinert, and Zimmermann (2018), our main technical result implies that there are pseudo-quasi-polynomial algorithms for solving parity energy games and for solving parity games with weights. Our main conceptual contributions are the definitions of strategy decompositions for both players, and a notion of progress measures for mean-payoff parity games that generalizes both parity and energy progress measures. The former provides normal forms for and succinct representations of winning strategies, and the latter enables the application to mean-payoff parity games of the order-theoretic machinery that underpins a recent quasi-polynomial algorithm for solving parity games.

AB - In a mean-payoff parity game, one of the two players aims both to achieve a qualitative parity objective and to minimize a quantitative long-term average of payoffs (aka. mean payoff). The game is zero-sum and hence the aim of the other player is to either foil the parity objective or to maximize the mean payoff. Our main technical result is a pseudo-quasi-polynomial algorithm for solving mean-payoff parity games. All algorithms for the problem that have been developed for over a decade have a pseudo-polynomial and an exponential factors in their running times; in the running time of our algorithm the latter is replaced with a quasi-polynomial one. By the results of Chatterjee and Doyen (2012) and of Schewe, Weinert, and Zimmermann (2018), our main technical result implies that there are pseudo-quasi-polynomial algorithms for solving parity energy games and for solving parity games with weights. Our main conceptual contributions are the definitions of strategy decompositions for both players, and a notion of progress measures for mean-payoff parity games that generalizes both parity and energy progress measures. The former provides normal forms for and succinct representations of winning strategies, and the latter enables the application to mean-payoff parity games of the order-theoretic machinery that underpins a recent quasi-polynomial algorithm for solving parity games.

UR - http://www.scopus.com/inward/record.url?scp=85051139038&partnerID=8YFLogxK

U2 - 10.1145/3209108.3209162

DO - 10.1145/3209108.3209162

M3 - Conference contribution

AN - SCOPUS:85051139038

T3 - Proceedings - Symposium on Logic in Computer Science

SP - 325

EP - 334

BT - Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2018

PB - The Institute of Electrical and Electronics Engineers (IEEE)

T2 - 33rd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2018

Y2 - 9 July 2018 through 12 July 2018

ER -