Applications pratiques des jeux de parité

12

Existe-t-il des exemples d'applications pratiques des jeux de parité, c'est-à-dire des systèmes, dans le monde réel, qui peuvent être représentés comme des jeux de parité?

La documentation généralement associée sur les jeux de parité n'a presque jamais d'exemple pratique de cette application.

kafka
la source
3
La sémantique de jeu du μ-calcul modal est liée aux jeux à deux joueurs avec des informations parfaites, en particulier les jeux à parité infinie. Voir aussi la section Relation avec la logique et la théorie des automates dans l'article de wikipedia sur les jeux de parité.
Thomas Klimpel
1
Il n'est pas vraiment destiné à être appliqué directement, mais plutôt comme une partie importante des théories (automates, jeux, logiques) ayant d'autres applications.
Denis

Réponses:

11

Voici une application assez différente de ce que vous aviez en tête. La programmation linéaire a de nombreuses applications pratiques. Il existe de nombreux algorithmes de programmation linéaire et ceux basés sur la méthode simplex de George Dantzig sont parmi les plus couramment mis en œuvre. Un paramètre important de simplex est appelé la règle de pivotement. Victor Klee et George Minty fournit un ensemble de polytopes sur lesquels la règle de pivotement suggérée par Dantzig nécessiterait un nombre exponentiel d'étapes de pivotement. Depuis lors, des exemples démontrant une limite inférieure exponentielle ont été découverts pour presque toutes les règles de pivotement déterministes.

Simplex peut cependant utiliser des règles de pivotement aléatoires. Gil Kalai en 1992 a introduit une règle de pivotement aléatoire et a prouvé une limite supérieure sous-exponentielle pour simplex avec cette règle. Toujours en 1992, Micha Sharir et Emo Welzl ont défini des problèmes de type LP qui incluent une programmation linéaire standard et avec Jiří Matoušek ont également proposé des variantes aléatoires du simplexe et prouvé des limites supérieures sous-exponentielles pour cette variante. Des limites inférieures subexponentielles ont également été découvertes sur des problèmes de type LP, mais jusqu'en 2010 environ, il n'y avait pas d'exemples concrets de programmes linéaires sur lesquels ces limites inférieures pouvaient être démontrées. Voir ces deux articles sur le blog de Gil Kalai pour un autre récit de cette histoire, le lien avec la conjecture de Hirsch et les liens avec la littérature.

Qu'est-ce que cela a à voir avec les jeux de parité? Quelques étapes sont nécessaires pour établir une connexion. Un problème ouvert dans la recherche sur les jeux de parité jusqu'en 2009 était de déterminer si certains algorithmes d'itération de politique pour résoudre les jeux de parité pouvaient avoir un comportement exponentiel. Voir les articles de Marcin Jurdziński pour en savoir plus. Oliver Friedmann, à partir de 2009 , a présenté des exemples de jeux de parité sur lesquels certains algorithmes d'itération de politique nécessitaient un temps exponentiel. En exploitant une connexion entre les jeux de parité et certains problèmes de type LP, il a dérivé des limites inférieures sous-exponentielles pour diverses règles de pivotement pour simplex. (Notez cependant que l'un des résultats, qui concernait l'algorithme à facettes aléatoires, a été montré par Oliver Friedmann, Thomas Hansen et Uri Zwick être erroné.)

J'espère que vous conviendrez que c'est un exemple assez fascinant et convaincant d'une application de jeux de parité.

Il existe également une réponse plus directe à votre question. Supposons que l'on veuille concevoir un contrôleur discret qui régule le comportement d'un système physique (thermostat, usine chimique, etc.) en fonction de l'état du système et de l'état de l'environnement. La question de savoir si un contrôleur existe pour fournir les garanties souhaitées par un concepteur peut être réduite à la résolution de jeux de parité. Vous pouvez donc penser à un jeu de parité en termes de systèmes, d'environnements et de contrôleurs.

Un autre paramètre est l'analyse de programme. Supposons que vous vouliez déterminer automatiquement si un programme satisfait une propriété de correction dans le modal -calculus. La vérification des modèles est une approche pour résoudre ce problème et la vérification des modèles -calculus est profondément liée aux jeux de parité. μμμ

Vijay D
la source
3
Les articles qui ont introduit la facette aléatoire ont prouvé des limites supérieures sous- exponentielles sur le nombre (attendu) d'étapes de pivotement (actuellement la réponse indique des limites inférieures). Les nouvelles bornes inférieures sont de forme similaire, c'est-à-dire sous-exponentielles et non exponentielles.
Rahul Savani
2
Il vaut peut-être la peine de souligner que certaines des limites inférieures de Friedmann, Hansen et Zwick sont défectueuses: arxiv.org/abs/1410.7871
Sasho Nikolov
Merci Sasho. C'est ce qui arrive quand j'arrête de suivre la littérature!
Vijay D