Un automate déterministe en histoire (en , abrégé HD) est, en informatique théorique, un modèle intermédiaire entre les automates déterministes et les automates non déterministes. Son non-déterminisme peut être résolu à la volée, en ne s'appuyant que sur le préfixe du mot déjà lu, sans connaissance de la suite de l'entrée.
Déterminisme et non-déterminisme Un automate fini lit un mot lettre par lettre et décide s'il appartient à un langage. On distingue deux familles :
Un automate fini déterministe (AFD) : depuis chaque état, une lettre donnée mène vers exactement un état suivant. Le chemin parcouru est entièrement déterminé par le mot lu. Un automate fini non déterministe (AFN) : une lettre peut mener vers plusieurs états possibles. Le mot est accepté s'il existe au moins un chemin acceptant. Implicitement, un AFN peut « deviner » la bonne branche, ce qui peut nécessiter de connaître la suite du mot.
Les automates HD constituent une troisième famille : comme les AFN, ils peuvent avoir plusieurs transitions possibles depuis un état ; mais comme les AFD, leur comportement peut être simulé lettre par lettre, sans jamais anticiper le futur.
Définition formelle
Structure Un automate fini non déterministe est un quintuplet , où :
est un alphabet fini ; est un ensemble fini non vide d'états ; est l'ensemble des états initiaux ; est la fonction de transition ; est la condition d'acceptation, qui diffère selon qu'on s'intéresse à des automates sur mots finis ou infinis. Pour les automates sur mots finis, la condition d'acceptation désigne un ensemble d'états finals : une exécution est acceptante si elle se termine dans un état de . Pour les automates sur mots infinis (notés -automates), les conditions d'acceptation sont plus variées : conditions de Büchi, coBüchi, parité, etc., qui portent sur les états visités infiniment souvent. Pour une présentation détaillée, on pourra se référer aux conditions décrites dans la section dédiée de l'article sur les automates sur les mots infinis.
Une exécution de sur un mot est un chemin sur les états (ou transitions) de , démarrant depuis un état initial et suivant la fonction de transition. Une exécution est acceptante si elle satisfait . Le langage reconnu par , noté , est l'ensemble des mots pour lesquels il existe une exécution acceptante.
Le jeu de lettres La propriété du déterminisme en histoire est définie à l'aide d'un jeu à deux joueurs appelé « jeu de lettres » (), introduit par Henzinger et Piterman.
Étant donné un automate , le jeu de lettres sur oppose deux joueurs, Adam et Ève, qui jouent à tour de rôle :
Adam construit un mot , lettre par lettre ; Ève construit simultanément une exécution de sur , transition par transition.
Plus précisément, à chaque tour :
Adam choisit une lettre ; Ève choisit une transition de sur .
La condition de victoire diffère selon la nature du mot construit : Sur les mots finis : Adam peut choisir de terminer la partie à tout moment. Ève gagne la partie si, à la fin, soit , soit l'exécution construite est acceptante sur . Il s'agit d'une condition de sûreté : à chaque tour, si le mot construit jusqu'ici appartient à , l'exécution partielle construite doit déjà être sur la bonne voie. Sur les mots infinis : une partie est une suite infinie de coups. Ève gagne la partie si soit , soit est une exécution acceptante de sur
Dans les deux cas, la contrainte cruciale est qu'Ève doit choisir chaque transition avant de connaître les lettres futures choisies par Adam : elle ne dispose que des lettres de l'histoire de la partie en cours.
Résolveur Une stratégie gagnante d'Ève dans le jeu de lettres est appelée « résolveur » (). Pour une définition moins anthropomorphique, un résolveur est une fonction :
où est l'ensemble des transitions de . Concrètement, prend en entrée :
l'historique des transitions déjà empruntées ; la lettre courante ;
et retourne la transition à emprunter à l'étape .
On notera que le résolveur s'appuie sur l'historique des transitions (et non seulement sur le préfixe du mot lu), ce qui lui permet de connaître l'état courant de l'automate ainsi que le chemin parcouru jusqu'ici. Sur mots finis comme sur mots infinis, cette information est suffisante : le résolveur n'a jamais besoin de connaître la suite du mot.
Le résolveur induit ainsi une exécution sur tout mot , définie par :
avec , , , etc.
Un résolveur est valide si l'exécution qu'il induit est acceptante sur tout mot du langage .
Le déterminisme en histoire Enfin, l'automate est dit « déterministe en histoire » si Ève possède une stratégie gagnante dans le jeu de lettres sur , c'est-à-dire s'il existe un résolveur tel que pour tout mot :
Cette définition s'applique aussi bien aux mots finis qu'aux mots infinis, la condition d'acceptation étant celle de l'automate concerné. On notera que tout automate déterministe est trivialement HD (le résolveur est simplement la fonction de transition), et que la réciproque est fausse en général.
Exemple vignette|droite|300px|Comparaison de deux automates coBüchi reconnaissant le langage « finiment de b ». L'automate du haut n'est pas HD, celui du bas l'est.
Pour illustrer ce concept, considérons le langage des mots infinis sur l'alphabet contenant un nombre fini de « b » (c'est un langage de -mots). Bien que les deux automates ci-contre reconnaissent ce langage avec une condition de coBüchi, leur structure de décision diffère :
L'automate (en haut) n'est pas déterministe en histoire. Pour construire une exécution acceptante sur un mot infini du langage, il doit « deviner » le futur : il faut transiter vers l'état précisément sur le « a » qui suit le dernier « b » du mot infini. Un résolveur, ne connaissant que le préfixe lu, ne peut pas identifier ce moment de façon certaine — car à tout instant, d'autres « b » pourraient encore apparaître dans la suite infinie du mot.
L'automate (en bas) est déterministe en histoire. Contrairement au précédent, il permet de corriger une décision prématurée : si le résolveur passe en alors qu'un « b » survient encore, une transition rejetante (en pointillés rouges) le ramène en . Puisque tout mot infini du langage ne contient qu'un nombre fini de « b », le résolveur finira par rester définitivement dans l'état acceptant après le dernier incident, satisfaisant la condition de coBüchi par simple historique.
Jeux à jetons
Afin de décider algorithmiquement si un automate est déterministe en histoire, on dispose d'une famille de jeux combinatoires appelés « jeux à jetons » (), généralisés par Bagnol et Kuperberg à partir du jeu à un jeton introduit par Löding. Ces jeux permettent, pour certaines classes d'automates, de caractériser le déterminisme en histoire de façon plus efficace que le jeu de lettres original. Le jeu à un jeton
Dans le jeu à un jeton , Adam déplace un seul jeton. Pour en comprendre la portée, on introduit la notion de transition non-prudente : une transition choisie par Ève après avoir construit un préfixe d'exécution sur un préfixe de mot est non-prudente s'il existe une continuation telle que mais qu'aucune exécution acceptante ne prolonge sur . Une stratégie est dite prudente si elle ne choisit jamais de transition non-prudente.
On démontre que G₁ caractérise le déterminisme en histoire pour les automates sur mots finis via l'argument en trois points suivant:
Dans le jeu de lettres, un coup non-prudent est fatal pour Ève : Adam peut toujours jouer la continuation qui la met en défaut. Dans , un coup non-prudent n'est pas toujours fatal, car le jeton d'Adam pourrait lui aussi se trouver dans l'impossibilité de construire une exécution acceptante. Cependant, si Ève possède une stratégie gagnante dans , elle doit en particulier gagner contre la stratégie copie d'Adam, dans laquelle Adam fait suivre son jeton exactement les mêmes transitions qu'Ève, jusqu'au premier coup non-prudent d'Ève, puis construit une exécution acceptante sur la continuation qui témoigne de ce manque de prudence. Une telle partie serait gagnante pour Adam ; une stratégie gagnante pour Ève doit donc éviter tout coup non-prudent contre la stratégie copie. Ève dispose ainsi d'une stratégie prudente dans le jeu de lettres — il lui suffit d'imaginer que le jeton d'Adam suit ses propres transitions. Pour les automates sur mots finis, toute stratégie prudente dans le jeu de lettres est gagnante pour Ève : toute partie perdante pour Ève contient nécessairement un coup non-prudent.
En revanche, ne caractérise pas le déterminisme en histoire pour les automates de Büchi ou coBüchi sur mots infinis. Un contre-exemple classique est l'automate reconnaissant le langage des -mots contenant finalement seulement des (avec un état acceptant qui est un puits) : cet automate n'est pas déterministe en histoire, mais Ève peut gagner en attendant que le jeton d'Adam atteigne avant d'y déplacer le sien.
Le jeu à k jetons
Le jeu à jetons sur un automate ressemble au jeu de lettres, à ceci près qu'Adam construit simultanément exécutions de en déplaçant jetons le long des transitions, en plus du mot. La condition de victoire ne fait plus référence à l'appartenance du mot à , mais uniquement aux exécutions construites par Adam.
Plus précisément, à chaque tour : Adam choisit une lettre ; Ève choisit une transition de sur ; Adam choisit transitions de sur .
Pour les automates sur mots infinis, une partie est une suite infinie de tels tours. Elle est constituée du -mot construit par Adam, de l'exécution infinie construite par Ève, et des exécutions infinies , , construites par Adam. Ève gagne la partie si soit aucune des exécutions de Adam n'est acceptante sur , soit l'exécution de Ève est acceptante sur .
On note également pour désigner le fait qu'Ève gagne ce jeu.
Le jeu à deux jetons et le lemme clé
Le jeu à deux jetons est plus puissant et caractérise le déterminisme en histoire pour les automates de Büchi et coBüchi sur mots infinis. L'intérêt de ce jeu repose sur le résultat fondamental suivant.
Ce lemme implique qu'il suffit de vérifier plutôt que l'ensemble des .
Résolution du jeu à deux jetons par jeu de parité
Construction de l'arène
Le jeu se modélise comme un jeu sur un graphe bipartite , où les deux types de sommets correspondent aux tours des deux joueurs.
Les positions sont de la forme , où est l'état courant d'Ève, et sont les états des deux jetons d'Adam, et est la dernière lettre jouée :
: sommets d'Ève, de la forme
: sommets d'Adam, de la forme . ou, pour l'état initial, de la forme : . La position initiale est . Adam choisit la première lettre , ce qui mène à .
Les mouvements sont les suivants :
Ève : ; Adam : .
À chaque tour, Ève choisit donc sa propre transition sur la lettre courante, puis Adam avance ses deux jetons et choisit la prochaine lettre. Le graphe ainsi construit est de taille .
Encodage en jeu de parité
Pour un automate de Büchi d'ensemble acceptant , on définit une fonction de priorité sur tous les sommets :
L'interprétation de ces priorités est la suivante :
Priorité 2 (paire) : Ève valide un état acceptant, ou aucun joueur ne valide - Ève n'est pas en défaut ;
Priorité 1 (impaire) : au moins un jeton d'Adam visite un état acceptant, mais Ève rate cet état -Adam « marque un point » ;
Priorité 0 : aucun joueur ne visite d'état acceptant - situation neutre.
L'objectif d'Ève est que la priorité maximale visitée infiniment souvent soit paire, ce qui est exactement la condition de victoire d'un jeu de parité standard.
Résolution et complexité
Le jeu de parité obtenu se résout par les algorithmes classiques dédiés aux jeux de parité sur graphes finis. Ces algorithmes opèrent directement sur la structure finie de l'arène, sans nécessiter de déterminisation.
Combiné au lemme clé, ce résultat donne le théorème suivant :