Subscribe to the gold package and get unlimited access to Shamra Academy
Register a new userA short proof of correctness of the quasi-polynomial time algorithm for parity games
170
0
0.0
(
0
)
Added by
Hugo Gimbert
Publication date
2017
fields
Informatics Engineering
and research's language is
English
Authors
Hugo Gimbert
Ask ChatGPT about the research
No Arabic abstract
Recently Cristian S. Calude, Sanjay Jain, Bakhadyr Khoussainov, Wei Li and Frank Stephan proposed a quasi-polynomial time algorithm for parity games. This paper proposes a short proof of correctness of their algorithm.
rate research
Read More
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.
We prove that every distributional problem solvable in polynomial time on the average with respect to the uniform distribution has a frequently self-knowingly correct polynomial-time algorithm. We also study some features of probability weight of correctness with respect to generalizations of Procaccia and Rosenscheins junta distributions [PR07b].
An ever-important issue is protecting infrastructure and other valuable targets from a range of threats from vandalism to theft to piracy to terrorism. The defender can rarely afford the needed resources for a 100% protection. Thus, the key question is, how to provide the best protection using the limited available resources. We study a practically important class of security games that is played out in space and time, with targets and patrols moving on a real line. A central open question here is whether the Nash equilibrium (i.e., the minimax strategy of the defender) can be computed in polynomial time. We resolve this question in the affirmative. Our algorithm runs in time polynomial in the input size, and only polylogarithmic in the number of possible patrol locations (M). Further, we provide a continuous extension in which patrol locations can take arbitrary real values. Prior work obtained polynomial-time algorithms only under a substantial assumption, e.g., a constant number of rounds. Further, all these algorithms have running times polynomial in M, which can be very large.
The distance transform algorithm is popular in computer vision and machine learning domains. It is used to minimize quadratic functions over a grid of points. Felzenszwalb and Huttenlocher (2004) describe an O(N) algorithm for computing the minimum distance transform for quadratic functions. Their algorithm works by computing the lower envelope of a set of parabolas defined on the domain of the function. In this work, we describe an average time O(N) algorithm for maximizing this function by computing the upper envelope of a set of parabolas. We study the duality of the minimum and maximum distance transforms, give a correctness proof of the algorithm and its runtime, and discuss potential applications.
Partial methods play an important role in formal methods and beyond. Recently such methods were developed for parity games, where polynomial-time partial solvers decide the winners of a subset of nodes. We investigate here how effective polynomial-time partial solvers can be by studying interactions of partial solvers based on generic composition patterns that preserve polynomial-time computability. We show that use of such composition patterns discovers new partial solvers - including those that merge node sets that have the same but unknown winner - by studying games that composed partial solvers can neither solve nor simplify. We experimentally validate that this data-driven approach to refinement leads to polynomial-time partial solvers that can solve all standard benchmarks of structured games. For one of these polynomial-time partial solvers not even a sole random game from a few billion random games of varying configuration was found that it wont solve completely.
Log in to be able to interact and post comments
comments
Fetching comments
Sign in to be able to follow your search criteria
