Monotonic graphs for parity and mean-payoff games

Graphes monotones pour jeux de parité et à paiement moyen 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.