Jeu de parité

En informatique théorique, un jeu de parité est un jeu à deux joueurs sur un graphe orienté où chaque sommet est étiqueté par un entier, appelé couleur ou priorité. 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 plus grande couleur visitée une infinité de fois est paire (chez certains auteurs, c'est lorsque la plus petite couleur visitée une infinité de fois est paire/impaire ; ces variantes sont fondamentalement équivalentes). Les jeux de parité sont importants en vérification de modèles, en particulier lorsque la propriété temporelle est exprimée en 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.

Lien avec la vérification de modèles

Le problème de vérification de modèles (model checking en anglais) du formule du mu-calcul se ramène à résoudre un jeu de parité. 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.

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. Il est aussi dans QP, i.e. en temps quasipolynomial, en temps O(n^{log d}), ou de manière équivalente O(d^{log n}) où d est le nombre de couleurs et n le nombre de noeuds dans le graphe. 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é :

• un algorithme récursif conçu par Zielonka (RE)  ;
• Small-progress measures (SPM) ;
• APT, qui s'appuie sur tester la vacuité d'un automate de parité alternant
• un algorithme où on se ramène un jeu de sûreté (en utilisant un automate dit parity separating automaton)^{[réf. nécessaire]}. Cet algorithme est aussi en O(d^{log n}). Par ailleurs, on peut montrer une borne inférieure sur la taille des parity separating automata : elle est pseudo-polynomiale.

Les algorithmes précédents sont explicites, dans le sens où le graphe orienté est représenté explicitement. Ainsi, ces algorithmes ne sont pas efficaces en pratique car le graphe qui représente des systèmes réels sont trop grands. On parle du problème d'explosion du nombre d'états (state-explosion problem en anglais), problème présent en général en vérification de modèles. C'est pourquoi on représente le graphe de manière symbolique à l'aide de diagrammes de décision binaire. L'algorithme RE a été implémenté en symbolique. Une version symbolique de SPM a été étudié théoriquement.

SPM

Le concept essentiel de l'algorithme SPM est la fonction de rang : on attribue à chaque sommet un vecteur de compteurs (mesure de progression), qui rassemble le nombre de fois que le joueur 1 peut forcer à visiter une priorité impaire avant qu'une priorité plus grande soit vue. Si la valeur est suffisamment petite, le sommet est déclaré comme gagnant pour le joueur 1. SPM calcule la mesure de progression en mettant à jour les valeurs d'un sommet à partir des valeurs de ses successeurs ; autrement dit en calculant un plus petit point fixe pour tous les sommets.

APT

La notion de jeu de parité est étendue en rajoutant deux sous-ensembles de sommets disjoints : l'ensemble des sommets visités et l'ensemble des sommets évités.

RE

L'algorithme RE introduit par Zielonka repose sur le paradigme diviser pour régner. Il utilise aussi le concept d'attracteur. Étant donné un sous-ensemble U de sommets, l'attracteur de U pour le joueur i est l'ensemble des sommets depuis lesquels le joueur i peut forcer à atteindre U. À chaque étape, l'algorithme supprime les sommets de priorité maximale p, ainsi que les sommets où le joueur i avec i = p mod 2 qui attire vers ces derniers. On obtient un jeu restant. Sur ce jeu restant, on appelle récursivement l'algorithme pour obtenir les deux ensembles gagnants W₀ et W₁ pour les joueurs 0 et 1 sur le jeu restant. Si le joueur i gagne sur le sous-jeu, alors il gagne aussi sur le jeu initial. Sinon, le joueur i ne gagne pas ce sous-jeu, i.e. W_1-i est non vide, l'algorithme calcule alors l'attracteur pour le joueur 1-i de W_1-i et on résout récursivement ce sous-jeu.

Formellement, soit $G=(V,V_{0},V_{1},E,\Omega )$ un jeu de parité où $V_{0}$ resp. $V_{1}$ sont les ensembles de sommets appartenant au joueur 0 resp. 1, $V=V_{0}\cup V_{1}$ est l'ensemble de tous les sommets, $E\subseteq V\times V$ est l'ensemble des transitions, et $\Omega :V\rightarrow \mathbb {N}$ la fonction qui donne la priorité à chaque sommet. Soit $U\subseteq V$ un ensemble de sommets et $i=0,1$ un joueur. Le i-attracteur de U est le plus petit ensemble de sommets $Attr_{i}(U)$ incluant U et tel que le joueur i peut forcer à visiter U depuis tout sommet de $Attr_{i}(U)$. L'ensemble $Attr_{i}(U)$ peut être calculer par itération car c'est un point fixe :

${\begin{aligned}Attr_{i}(U)^{0}&:=U\\Attr_{i}(U)^{j+1}&:=Attr_{i}(U)^{j}\cup \{v\in V_{i}\mid \exists (v,w)\in E:w\in Attr_{i}(U)^{j}\}\cup \{v\in V_{1-i}\mid \forall (v,w)\in E:w\in Attr_{i}(U)^{j}\}\\Attr_{i}(U)&:=\bigcup _{j=0}^{\infty }Attr_{i}(U)^{j}\end{aligned}}$

En d'autres mots, on commence avec l'ensemble initial U puis, on ajoute à chaque étape, tous les sommets du joueur i qui peuvent atteindre l'ensemble courant en une étape, et tous les sommets du joueur 1-i qui atteignent forcément l'ensemble courant quelle que soit la transition choisie par le joueur 1-i.

Voici un pseudo-code l'algorithme de Zielonka W₀, W₁) qui est une partition de l'ensemble des sommets avec W_i est l'ensemble des sommets depuis lesquels le joueur i gagne.

 fonction $resoudre(G)$
     p:= priorité maximale du jeu G
     si $p=0$
         retourner $V,\{\}$
     alors
         U:= ensemble des sommets de G de priorité p
         $i:=p{\bmod {2}}$
         $A:=Attr_{i}(U)$
         $W_{0}',W_{1}':=resoudre(G\setminus A)$
         si $W_{i}'=V$
              retourner $V,\{\}$
         $B:=Attr_{1-i}(W_{1-i}')$
         $W_{0}'',W_{1}'':=resoudre(G\setminus B)$
         retourner $W_{i}'',(W_{1-i}''\cup B)$

Propriétés

Tout jeu de parité appartient au troisième niveau de la hiérarchie de Borel, ainsi le jeu est déterminé, 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. 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.

Les jeux de parités sont des cas particuliers des jeux de moyenne récompense (mean payoff games). Plus précisément, on peut transformer tout jeu de parité en un mean payoff game équivalent : remplacer une priorité (couleur) p par (-n)^p, où n est le nombre de nœuds.