Contribution à l’étude des jeux sur des graphes de processus à pile

La vérification 

L’informatique et les systèmes automatisés occupent autour de nous une place chaque jour plus grande. Il en découle que la fiabilité de ces systèmes est un enjeu capital, aussi bien du point de vue économique que du point de vue de la sécurité de chacun d’entre nous. Nous sommes tous conscients de l’importance prise par l’informatique dans notre société. Même si le fameux bug de l’an 2000 n’a pas été aussi terrible qu’on nous le prédisait, il faut bien reconnaître qu’il n’est pas difficile de dresser une liste de défaillances informatiques, parfois stupides mais difficiles à contourner, rencontrées au cours des dernières années. Aussi la vérification des systèmes revêt-elle un caractère crucial. La conception d’un système passe par de nombreuses étapes qui impliquent une grande diversité d’intervenants. Certains d’entre eux ont une vision assez abstraite du système, tandis que d’autres se confrontent au difficile problème de l’implantation. La conception abstraite du système doit donc être réalisable dans la pratique de façon performante, sous peine de perdre fortement de son intérêt.

Il en va de même pour la vérification. Afin de vérifier un système, on commence par le modéliser. On spécifie ensuite une propriété que l’on souhaite vérifier, dans un formalisme adapté, qui passe le plus souvent par une formule logique. On regarde enfin si le modèle vérifie la spécification. Le problème est double : les phases de modélisation et de spécification doivent permettre une phase de vérification, réalisable non seulement d’un point de vue théorique, mais également d’un point de vue pratique.

La phase de modélisation se doit d’être générale pour pouvoir être réutilisable : il serait dommage de définir un modèle pour un programme faisant trois appels récursifs au plus, et de devoir refaire tout le travail lorsque l’on s’intéresse à un même programme faisant cette fois-ci quatre appels récursifs au plus. Cependant, un modèle trop puissant rendrait la phase de vérification délicate, voire impossible. Une autre notion importante dans la modélisation d’un système est son caractère fini ou non. Par exemple, on peut modéliser un ascenseur dans un immeuble à trois étages par un nombre fini de paramètres, qui peuvent chacun prendre un nombre fini de valeurs. Considérons à présent un programme qui effectue un nombre arbitraire d’appels récursifs : il ne peut être modélisé de façon finie, car la taille de sa pile d’appels récursifs n’est pas bornée. Dans ce cas, on cherchera un modèle finiment descriptible de systèmes infinis.

Et les jeux dans tout ça? 

On distingue fréquemment deux types de systèmes : les systèmes fermés et les systèmes ouverts. Dans le premier cas, le système n’a pas d’interaction avec l’environnement, alors que dans le second cas l’environnement est actif. Un système ouvert peut représenter un programme et son environnement. Reprenons notre exemple d’ascenseur : le programme est l’ascenseur, tandis que l’environnement est constitué d’utilisateurs qui peuvent appeler l’ascenseur et spécifier un étage où aller. On peut alors se demander si l’ascenseur amène toujours ses passagers à bon port, c’est-àdire si lorsqu’un étage est demandé, l’ascenseur s’y arrêtera quoi qu’il se passe entre temps (appels de l’ascenseur, plusieurs arrêts demandés,. . . ). La vérification des systèmes ouverts peut être réalisée à l’aide d’un jeu. On peut représenter le système par un ensembles de sommets reliés entre eux par des transitions. Le modèle du système possède deux types d’états appelés sommets : ceux où la prochaine action sera effectuée par le programme, et ceux où elle sera réalisée par l’environnement. On décide que les sommets où le programme va effectuer la prochaine action appartiennent à un premier joueur, Eve, tandis que les sommets régis par l’environnement appartiennent à un second joueur, Adam. Une partie dans un jeu débute dans le sommet qui correspond à l’état initial du système. Le joueur à qui ce sommet appartient choisit une action à effectuer, et va dans le sommet correspondant à l’état résultant de cette action. Le joueur à qui le nouveau sommet appartient choisit une action et ainsi de suite. Une partie est la simulation d’une exécution du système. Si ce dernier ne se bloque pas, la partie est infinie. Les propriétés que l’on souhaite le plus souvent vérifier sont de la forme «quoi que fasse l’environnement, l’exécution est une bonne exécution». On dira alors qu’Eve remporte une partie si celle-ci correspond à une bonne exécution. Sinon c’est Adam qui gagne. Le système vérifie la propriété si toutes les parties sont remportées par Eve.

Une variante du problème de vérification est celui de la synthèse d’un contrôleur. On a cette fois-ci un système ouvert, dans lequel les comportements du système dans un état sont multiples. Par ailleurs, on possède une spécification que l’on veut voir satisfaite, quelle que soit le comportement de l’environnement. En général, les comportements du programme sont trop peu restreints pour cette spécification face à un environnement malicieux. On cherche alors à restreindre les comportements afin que le nouveau système satisfasse la propriété. On parle alors de synthèse de contrôleur. En terme de jeu, le problème de synthèse d’un contrôleur correspond à la recherche d’une stratégie gagnante pour Eve. Une stratégie est une manière de jouer, c’est-à-dire une procédure qui décide quelle action choisir, en fonction du sommet courant et du passé de la partie. Une stratégie est gagnante si elle assure la victoire dès lors qu’on la respecte. Si Eve possède une stratégie, on en déduit un contrôleur et réciproquement. Lorsque l’on synthétise un contrôleur, on voudrait, en vue d’une implémentation, que celui-ci soit le plus simple possible. Dans le formalisme des jeux, cela revient à restreindre la mémoire qu’Eve peut utiliser pour calculer sa stratégie. Une autre question importante est de restreindre au minimum le programme. Dans le formalisme des jeux, cela revient à chercher une stratégie la plus permissive possible.

Structures de base 

Mots et langages

Mots
Un alphabet est un ensemble fini ou infini de symboles. Les éléments d’un alphabet sont des lettres. Dans la suite, un alphabet sera le plus souvent désigné par une lettre majuscule romaine, par exemple A,B ou C, et les lettres par des lettres minuscules romaines, par exemple a, b ou c. Un mot sur un alphabet A est une suite de lettres de A. Un mot fini est une suite finie de lettres tandis qu’un mot infini est une suite indexée par les entiers naturels. On représente un mot fini par la juxtaposition des lettres qui le composent. Par exemple jeux représente le mot à quatre lettres associé à la suite j,e,u,x. Le mot vide, c’est-à-dire le mot associé à la suite vide est noté ε. Etant donnés un mot fini u et un mot (fini ou infini) v, la concaténation de u et de v sera notée u · v ou plus simplement uv, s’il n’y a pas d’ambiguïté. Un mot fini u est un préfixe d’un mot (fini ou infini) v, ce que l’on note u ⊑ v, s’il existe un mot w tel que v = uw. Un mot fini u est un suffixe d’un mot fini v, s’il existe un mot w tel que v = wu. Un mot fini u est un facteur d’un mot (fini ou infini) v, s’il existe deux mots w1 et w2 tels que v = w1uw2. Enfin, un mot u est un sous-mot d’un mot v si la suite des lettres de u est une sous-suite de la suite des lettres de v. Soit un mot u préfixe (respectivement suffixe, facteur ou sous-mot) d’un mot v, u est un préfixe (respectivement suffixe, facteur ou sous-mot) strict de v si et seulement si u et v sont distincts. Pour tout mot u de longueur n et tout entier 0 ≤ k ≤ n, on désigne par u↾k le préfixe de u de longueur k.

Par exemple, si l’on considère le mot automate, auto en est un préfixe, tomate un suffixe, ma un facteur et atome un sous-mot. On note |u| la longueur (éventuellement infinie) du mot u. Si a est une lettre, |u|a désigne le nombre d’occurrences de a dans u. Etant donnés un mot u et un entier n ≥ 0, on désigne par u n le mot formé de n concaténations de u. En particulier u 0 est le mot vide ε. Etant donné un mot fini u = a1a2 · · · an, on appelle miroir de u, le mot ue = anan−1 · · · a1. Par exemple, si u = olivier, ue = reivilo. Un mot égal à son miroir sera appelé palindrome. Les mots anna et esoperesteicietserepose sont des exemples de palindromes. Soit un alphabet A. On note A∗ l’ensemble des mots finis sur A, A+ l’ensemble des mots finis différents  du mot vide, Aω l’ensemble des mots infinis sur A, et A∞ l’ensemble des mots finis ou infinis sur A. Enfin, étant donnée une suite (ui)i≥1 ∈ (A∗ ) N de mots finis sur un alphabet A, on définit le mot, fini ou infini, lim(ui)i≥1, appelé limite de la suite (ui)i≥1, et défini comme le mot maximal pour l’inclusion vérifiant ce qui suit : pour tout j ≥ 1, il existe un entier r telle que la j-ème lettre de lim(ui)i≥1 est la même que la j-ème lettre de up pour tout p ≥ r.

Langages
Un langage désigne un ensemble de mots et sera, en général, noté par une lettre majuscule romaine, par exemple L. On distinguera deux cas particuliers de langages: les langages de mots finis et les langages de mots infinis, également appelés ω-langages (la lettre ω faisant référence au caractère infini des mots de ces langages). Un langage de mots finis sur un alphabet A sera donc un sous-ensemble de A∗ , tandis qu’un ω-langage sur l’alphabet A sera un sous-ensemble de Aω . La grande majorité des langages considérés par la suite seront de l’une des deux formes précédentes. Un langage L est fermé par préfixe lorsque pour tout mot u dans L, tout préfixe de u est dans L. Plusieurs opérations peuvent être effectuées sur les langages. Les langages étant des ensembles, on rappelle les opérations booléennes :
– étant donnés deux langages L1 et L2, le langage L = L1 ∪L2 = {u ∈ A∞ | u ∈ L1 ou u ∈ L2} est appelé union de L1 et L2.
– étant donnés deux langages L1 et L2, le langage L = L1 ∩L2 = {u ∈ A∞ | u ∈ L1 et u ∈ L2} est appelé intersection de L1 et L2.
– étant donnés deux langages L1 et L2, le langage L = L1 \ L2 = {u ∈ A∞ | u ∈ L1 et u /∈ L2} est appelé différence de L1 et L2.
– étant donné un langages L, le langage L = A∞ \ L est appelé complémentaire de L. Lorsque L est un langage de mots finis (respectivement de mot infinis) et que le contexte est clair, on appellera également complémentaire le langage A∗ \ L (respectivement Aω \ L). Outre les opérations booléennes, il existe d’autres opérations naturelles sur les langages, fondées sur la notion de concaténation pour les mots :

– étant donnés un langage L1 de mot finis et un langage L2 quelconque, le langage L = L1L2 est le langage {u1u2 ∈ A∞ | u1 ∈ L1 et u2 ∈ L2}. Le langage L est appelé produit de L1 et L2.
– étant donné un langage L de mots finis, on définit par récurrence la suite de langages finis (L i )i≥0 par L0 = {ε} et L i+1 = L iL. On parle alors de puissances d’un langage.
– étant donné un langage de mots finis L, l’union des puissances de L, notée L∗ et définie par L∗ =[i≥0Li , est appelée étoile de L. Une variante consiste à ne considérer que les puissances non nulles de L, c’est-à-dire à poser L + = [ i>0 L i .
– étant donné un langage de mots finis L ne contenant pas le mot vide, le langage de mots infinis L ω = {u = u0u1u2 · · · | (ui)i≥0 ∈ L N} est appelé ω-itération de L.
– étant donné un langage de mots finis L ne contenant pas le mot vide, le langage L∞ = L∗ ∪ L ω est appelé ∞-itération de L.

Table des matières

Introduction
1 Définitions et notations
1.1 Structures de base
1.1.1 Mots et langages
1.1.2 Arbres
1.1.3 Graphes
1.2 Langages et automates
1.2.1 Langages rationnels de mot finis
1.2.2 Langages algébriques de mots finis
1.2.3 Langages rationnels de mots infinis
1.2.4 Langages algébriques de mots infinis
1.3 Quelques familles de graphes infinis finiment représentables
1.3.1 Graphe associé à un processus à pile
1.3.2 Sous-classes
1.4 Machine de Turing, calculabilité et complexité
2 Jeux à deux joueurs sur un graphe
2.1 Définitions
2.1.1 Jeu, partie, condition de gain
2.1.2 Stratégies et positions gagnantes
2.2 Jeux sur des graphes de processus à pile
2.2.1 Définition du graphe de jeu et représentation
2.2.2 Conditions d’accessibilité, de Büchi et de parité
2.2.3 Conditions de gain sur la hauteur de pile
2.2.4 Condition de parité en escalier
2.2.5 Stratégie à pile
2.3 Complexité borélienne
2.3.1 Complexité borélienne d’une condition de gain
2.3.2 Jeu de Wadge
2.4 Quelques résultats classiques
3 Jeux sur des graphes de processus à pile : petit historique et contributions de la thèse
4 Ensembles de positions gagnantes
4.1 Quelques définitions et un peu d’intuition
4.1.1 Remarques préliminaires
4.1.2 Deux propriétés sur les conditions de gain
4.1.3 Jeux conditionnés et ensembles de retours
4.2 Cas particulier des conditions invariantes par translations
4.2.1 Ensembles de retours et positions gagnantes
4.2.2 Régularité des ensembles de positions gagnantes
4.2.3 A propos de l’effectivité
4.2.4 Comment décider le gagnant depuis une position quelconque?
4.2.5 Composition des stratégies
4.3 Généralisation
4.3.1 Conditions d’accessibilité et conditions ω-régulières sur les états
4.3.2 Enrichissement déterministe de jeu
4.3.3 Conditions régulières de pile
4.3.4 Combinaisons booléennes
5 Conditions de parité et d’explosion
5.1 Factorisation des parties
5.1.1 M/B factorisation
5.1.2 De l’utilité de la M/B factorisation
5.2 Réduction : la condition de parité
5.2.1 Factorisation dans Ge
5.2.2 Implication directe
5.2.3 Implication réciproque
5.2.4 Un exemple complet
5.2.5 A propos de la taille du graphe fini
5.3 Conditions d’explosion stricte
5.3.1 La réduction
5.3.2 A propos de la preuve
5.3.3 A propos de la taille du graphe fini
5.4 De l’explosion stricte à l’explosion
5.5 Condition de répétition et de bornage
5.6 Condition de parité en escalier
5.6.1 La réduction
5.6.2 A propos de la preuve
5.6.3 A propos de la taille du graphe fini
5.6.4 A propos des stratégies
5.6.5 Bornes supérieures et inférieures
Conclusion

Télécharger le rapport complet