joint work with Laure Daviaud and Ranko Lazić
- Speaker(s)
- Marcin Jurdziński
- Affiliation
- University of Warwick
- Date
- March 21, 2018, 2:15 p.m.
- Room
- room 5050
- Title in Polish
- A pseudo-quasi-polynomial algorithm for solving mean-payoff parity games
- Seminar
- Seminar Automata Theory
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.
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.
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.
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.
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.