Graphes monotones pour jeux de parité et à paiement moyen

In a parity game, Eve and Adam take turns in moving a token along the edges of a directed graph, which are labelled by integers called priorities. This interaction results in an infinite path, and Eve wins the game if the maximal priority appearing infinitely often is even. In the more general setting of mean-payoff games, priorities are replaced by positive or negative integers interpreted as payoffs from Eve to Adam; Eve seeks to minimize their long-term average. Both parity and mean-payoff games are positional: optimal decisions can be made depending only on the current position. The problems of determining the winner for these two games thus belong to NP and coNP, and have attracted considerable attention since the early nineties when parity games were shown equivalent to the model-checking problem for the mu-calculus. Both games moreover find numerous practical application, most notably they provide adequate models for synthesis problems on reactive systems. Despite decades of efforts toward polynomial time algorithms, it was only recently that a breakthrough was achieved in this direction by Calude, Jain, Khoussainov, Li and Stephan, who presented in early 2017 an algorithm running in quasipolynomial time for solving parity games. Quickly after, several different algorithms with similar runtime were discovered, and later unified by the separating approach proposed by Bojanczyk and Czerwinski, and identified as value iteration algorithms. We introduce monotonic graphs for studying structural and algorithmic aspects of such infinite duration games. These natural objects have numerous (more or less) implicit occurrences in the literature. We start by showing that the existence of universal well-ordered such graphs characterises (half) positionality of arbitrary winning conditions. This yields a novel approach to establishing and combining such structural results. We then advocate that (universal) monotonic graphs provide different handles for constructing algorithms. Finite monotonic graphs induce value iteration algorithms, which are shown to be roughly equivalent to Bojanczyk and Czerwinski's separating approach in general. This allows us to formulate lower bounds for mean-payoff games, and conclude that value iteration algorithms are inadequate to improve on the current state of the art. We also study value iteration algorithms for different well-known extensions of these games. Monotonic graphs also give a generic formalisation for strategy improvement algorithms. More precisely, we establish that valuations induced by monotonic graphs are fit for strategy improvement if and only if they are positional for the opponent. This encompasses known strategy improvement frameworks, allows us to propose new algorithms and perhaps more importantly, introduces a new tool for their difficult study. Surprisingly, monotonic graphs also find applications for symmetric algorithms, such as those based on attractors. For parity as well as mean-payoff games, we find that monotonic graphs allow us to shed light and improve on the recent state of the art.Dans un jeu de parité, Eve et Adam déplacent tour à tour un jeton le long d'un graphe dirigé dont les arêtes sont étiquetées par des entiers appelés priorités. Cette interaction produit un chemin infini ; Eve remporte la partie si la plus grande priorité apparaissant infiniment souvent est paire. Dans le cadre plus général offert par les jeux à paiement moyen, les priorités sont remplacées par des entiers potentiellement négatifs représentant des paiements d'Eve à Adam. Eve cherche donc à minimiser leur moyenne à long terme. Les deux types de jeux sont positionnels : des décisions optimales peuvent être prises en fonction seulement de la position actuelle. La détermination du gagnant dans ces deux jeux se situe donc à l'intersection de NP et de coNP. Ces questions algorithmiques sont l'objet d'une attention considérable depuis le début des années 1990, au moment où il a été établi que les jeux de parité sont équivalents au problème de la vérification pour la logique du mu-calcul. Les deux jeux ont de nombreuses applications pratiques ; ils fournissent notamment des modèles adéquats pour le problème de la synthèse de systèmes réactifs. Malgré des dizaines d'années de recherche d'algorithmes fonctionnant en temps polynomial, c'est seulement en 2017 que le premier algorithme quasipolynomial pour les jeux de parité a été découvert par Calude, Jain, Khoussainov, Li et Stephan. Peu après, plusieurs autres algorithmes quasipolynomiaux pour les jeux de parité ont été présentés, puis unifiés grâce à l'approche de séparation proposée par Bojanczyk et Czerwinski, et enfin identifiés comme des algorithmes d'itération de valeur. Nous introduisons les graphes monotones dans le but d'étudier les aspects structurels et algorithmiques des jeux à durée infinie. Ces objets naturels ont fait de nombreuses apparitions (plus ou moins) implicites dans la littérature. Nous montrons en premier lieu que, pour des conditions de gain arbitraires, l'existence de graphes monotones universels bien ordonnés caractérisent la positionnalité pour Eve. Cela donne une nouvelle technique pour établir et combiner de tels résultats structurels. Nous avançons ensuite que les graphes monotones offrent différentes possibilités pour construire des algorithmes. Les graphes monotones finis induisent des algorithmes d'itération de valeur, dont on montre qu'ils sont équivalents dans un cadre général à l'approche (forte) de séparation de Bojanczyk et Czerwinski. Cela nous permet en particulier de formuler des bornes inférieures pour les jeux à paiement moyen, et donc d'établir que les méthodes d'itération de valeur ne peuvent améliorer l'état de l'art. Nous étudions aussi les algorithmes d'itération de valeur pour différentes extensions courantes de ces jeux. Les graphes monotones donnent aussi un cadre générique pour formuler des algorithmes d'amélioration de stratégies. Plus précisément, nous montrons que les valuations induites par des graphes monotones permettent de tels algorithmes si et seulement si elles sont positionnelles pour l'adversaire. Ce résultat capture les différents cadres connus, nous permet d'en proposer d'autres, et introduit un nouvel outil à l'étude difficile de ces algorithmes. Étonnament, les graphes monotones s'appliquent aussi à l'étude d'algorithmes symétriques, tels que ceux qui sont fondés sur des calculs d'attracteurs. Ils permettent d'envisager sous un nouvel angle les jeux de parité ainsi que les jeux à paiement moyen, et dans les deux cas, de mieux comprendre et d'améliorer l'état de l'art