« Jeu de parité » : différence entre les versions

Un article de Wikipédia, l'encyclopédie libre.
Navigation interactive dans l’historique
← Modification précédenteModification suivante →
Contenu supprimé Contenu ajouté
VisuelWikicode
JackBot (discuter | contributions)
Robots
489 017 modifications
Fschwarzentruber (discuter | contributions)
8 056 modifications
Ligne 8 : Ligne 8 :


== Algorithmique ==
== Algorithmique ==
Déterminer si le joueur 1 a une stratégie gagnante dans un jeu de parité depuis un sommet initial est dans NP ∩ coNP, plus précisément dans UP ∩ coUP<ref>{{Article|langue=en|titre=Deciding the winner in parity games is in UP ∩ co-UP|périodique=Information Processing Letters|volume=68|numéro=3|date=1998-11-15|issn=0020-0190|doi=10.1016/S0020-0190(98)00150-1|lire en ligne=https://www.sciencedirect.com/science/article/pii/S0020019098001501|consulté le=2018-02-12|pages=119–124}}</ref>{{,}}<ref>{{Ouvrage|langue=en|prénom1=Hartmut|nom1=Klauck|titre=Automata Logics, and Infinite Games|passage=107–129|éditeur=Springer, Berlin, Heidelberg|collection=Lecture Notes in Computer Science|date=2002|isbn=3540363874|doi=10.1007/3-540-36387-4_7|lire en ligne=https://link.springer.com/chapter/10.1007/3-540-36387-4_7|consulté le=2018-02-12}}</ref>. Il est aussi dans QP (en temps quasipolynomial)<ref>{{Article|langue=|auteur1=|prénom1=Cristian S.|nom1=Calude|prénom2=Sanjay|nom2=Jain|prénom3=Bakhadyr|nom3=Khoussainov|prénom4=Wei|nom4=Li|titre=Deciding parity games in quasipolynomial time|périodique=Proceedings of the 49th Annual ACM SIGACT Symposium on Theory of Computing|éditeur=ACM|date=2017-06-19|isbn=9781450345286|issn=|doi=10.1145/3055399.3055409|lire en ligne=http://dl.acm.org/citation.cfm?id=3055399.3055409|consulté le=2018-02-12|pages=252–263}}</ref> . C'est une question ouverte que de savoir si ce problème est dans [[P (complexité)|P]].
Déterminer si le joueur 1 a une stratégie gagnante dans un jeu de parité depuis un sommet initial est dans NP ∩ coNP, plus précisément dans UP ∩ coUP<ref>{{Article|langue=en|titre=Deciding the winner in parity games is in UP ∩ co-UP|périodique=Information Processing Letters|volume=68|numéro=3|date=1998-11-15|issn=0020-0190|doi=10.1016/S0020-0190(98)00150-1|lire en ligne=https://www.sciencedirect.com/science/article/pii/S0020019098001501|consulté le=2018-02-12|pages=119–124}}</ref>{{,}}<ref>{{Ouvrage|langue=en|prénom1=Hartmut|nom1=Klauck|titre=Automata Logics, and Infinite Games|passage=107–129|éditeur=Springer, Berlin, Heidelberg|collection=Lecture Notes in Computer Science|date=2002|isbn=3540363874|doi=10.1007/3-540-36387-4_7|lire en ligne=https://link.springer.com/chapter/10.1007/3-540-36387-4_7|consulté le=2018-02-12}}</ref>. Il est aussi dans QP (en temps quasipolynomial)<ref>{{Article|langue=|auteur1=|prénom1=Cristian S.|nom1=Calude|prénom2=Sanjay|nom2=Jain|prénom3=Bakhadyr|nom3=Khoussainov|prénom4=Wei|nom4=Li|titre=Deciding parity games in quasipolynomial time|périodique=Proceedings of the 49th Annual ACM SIGACT Symposium on Theory of Computing|éditeur=ACM|date=2017-06-19|isbn=9781450345286|issn=|doi=10.1145/3055399.3055409|lire en ligne=http://dl.acm.org/citation.cfm?id=3055399.3055409|consulté le=2018-02-12|pages=252–263}}</ref> . C'est une question ouverte que de savoir si ce problème est dans [[P (complexité)|P]]. Il existe plusieurs algorithmes pour résoudre un jeu de parité :

* Recursive (RE)<ref name="ZL" /> ;
* ''Small-progress measures'' (SPM)<ref>{{Article|prénom1=Marcin|nom1=Jurdzinski|titre=Small Progress Measures for Solving Parity Games|éditeur=Springer-Verlag|date=2000-02-01|isbn=3540671412|lire en ligne=http://dl.acm.org/citation.cfm?id=646514.695804|consulté le=2018-05-02|pages=290–301}}</ref> ;
* APT, qui s'appuie sur tester la vacuité d'un automate de parité alternant


== Propriétés ==
== Propriétés ==

Version du 2 mai 2018 à 14:00

En informatique théorique, un jeu de parité est un jeu à deux joueurs sur un graphe orienté colorié. Chaque joueur possède son propre sous-ensemble de sommets. Une partie est un chemin infini dans le graphe. Le premier joueur gagne lorsque la couleur la plus grande visitée une infinité de fois est paire. Les jeux de parités sont importants en vérification de modèles et ont un lien avec le mu-calcul.

Exemple

Exemple d'un jeu de parité

La figure ci-contre montre un graphe orienté à huit sommets. Le joueur 1 joue dans les sommets ronds et le joueur 2 joue dans les sommets carrés. Les numéros indiqués dans les sommets sont les couleurs. Par exemple, la couleur du sommet rond en haut à gauche est 4. Le joueur 1 gagne si la couleur la plus grande visitée une infinité de fois est paire. Ainsi, dans la zone bleue, le joueur 1 a une stratégie gagnante, donnée par les arcs en bleu. Si on part du sommet 1, un exemple de partie est 141416161414... et la couleur la plus grande visitée une infinité de fois est soit 4, soit 6, et est paire dans tous les cas.

Dans la zone rouge par contre, le joueur 2 gagne car il peut forcer à ce que la couleur visitée une infinité de fois la plus grande est impaire. Dans la partie 82032030302..., la couleur visité une infinité de fois la plus grande est 3, et donc impaire.

Algorithmique

Déterminer si le joueur 1 a une stratégie gagnante dans un jeu de parité depuis un sommet initial est dans NP ∩ coNP, plus précisément dans UP ∩ coUP[1],[2]. Il est aussi dans QP (en temps quasipolynomial)[3] . C'est une question ouverte que de savoir si ce problème est dans P. Il existe plusieurs algorithmes pour résoudre un jeu de parité :

  • Recursive (RE)[4] ;
  • Small-progress measures (SPM)[5] ;
  • APT, qui s'appuie sur tester la vacuité d'un automate de parité alternant

Propriétés

Tout jeu de parité appartient au troisième niveau de la hiérarchie de Borel, ainsi le jeu est déterminé[6], c'est-à-dire que l'un des joueurs possède une stratégie gagnante. En d'autres termes, il n'y a pas de sommets à partir duquel aucun joueur n'a de stratégie gagnante (dans l'exemple donné ci-dessus, dans tous les sommets, un des joueurs a une stratégie gagnante : dans les sommets 4, 1, 6, le joueur 1 a une stratégie gagnante et dans les sommets 0, 3, 2, 5, 8, c'est le joueur 2 qui a une stratégie gagnante).

De plus, on peut montrer que l'on peut se contenter de stratégies qui ne dépendent pas de l'histoire mais uniquement du sommet courant[7],[8],[4] : dans l'exemple ci-dessus, le premier joueur choisit d'aller dans le sommet 1 depuis le sommet 6, et cela ne dépend pas de l'histoire : que l'histoire ait été 416 ou 41414146, ou tout autre histoire se terminant par le sommet 6, il décide d'aller dans le sommet.

Model checking

Le problème de model checking du formule du mu-calcul se ramène à résoudre un jeu de parité[9]. Pour cela, on transforme une formule du mu-calcul en automate d'arbres infinis avec condition de parité. Le problème de model checking se réduit donc à l'appartenance de la structure finie donnée au langage de l'automate d'arbres infinis. L'automate accepte la structure ssi le joueur 1 a une stratégie gagnante dans un jeu de parité construit à partir de l'automate et de la structure[10].

Notes et références

  1. ↑ (en) « Deciding the winner in parity games is in UP ∩ co-UP », Information Processing Letters, vol. 68, no 3,‎ , p. 119–124 (ISSN 0020-0190, DOI 10.1016/S0020-0190(98)00150-1, lire en ligne, consulté le )
  2. ↑ (en) Hartmut Klauck, Automata Logics, and Infinite Games, Springer, Berlin, Heidelberg, coll. « Lecture Notes in Computer Science », (ISBN 3540363874, DOI 10.1007/3-540-36387-4_7, lire en ligne), p. 107–129
  3. ↑ Cristian S. Calude, Sanjay Jain, Bakhadyr Khoussainov et Wei Li, « Deciding parity games in quasipolynomial time », Proceedings of the 49th Annual ACM SIGACT Symposium on Theory of Computing, ACM,‎ , p. 252–263 (ISBN 9781450345286, DOI 10.1145/3055399.3055409, lire en ligne, consulté le )
  4. ↑ a et b W Zielonka, « Infinite Games on Finitely Coloured Graphs with Applications to Automata on Infinite Trees », Theor. Comput. Sci., vol. 200, nos 1–2,‎ , p. 135–183 (DOI 10.1016/S0304-3975(98)00009-7)
  5. ↑ Marcin Jurdzinski, « Small Progress Measures for Solving Parity Games », {{Article}} : paramètre « périodique » manquant, Springer-Verlag,‎ , p. 290–301 (ISBN 3540671412, lire en ligne, consulté le )
  6. ↑ Donald A. Martin, « Borel Determinacy », Annals of Mathematics, vol. 102, no 2,‎ , p. 363–371 (DOI 10.2307/1971035, lire en ligne, consulté le )
  7. ↑ Erreur de référence : Balise <ref> incorrecte : aucun texte n’a été fourni pour les références nommées EJ
  8. ↑ A. Mostowski: Games with forbidden positions, University of Gdansk, Tech. Report 78 (1991)
  9. ↑ (en) Júlia Zappe, Automata Logics, and Infinite Games, Springer, Berlin, Heidelberg, coll. « Lecture Notes in Computer Science », (ISBN 3540363874, DOI 10.1007/3-540-36387-4_10, lire en ligne), p. 171–184
  10. ↑ (en) Daniel Kirsten, Automata Logics, and Infinite Games, Springer, Berlin, Heidelberg, coll. « Lecture Notes in Computer Science », (ISBN 3540363874, DOI 10.1007/3-540-36387-4_9, lire en ligne), p. 153–167
Ce document provient de « https://fr.wikipedia.org/w/index.php?title=Jeu_de_parité&oldid=148072891 ».