Les jeux à la rescousse de la vérification

A priori, les graphes modélisant des programmes peuvent posséder un ensemble infini de sommets, typiquement lorsque les variables peuvent prendre des valeurs arbitrairement grandes. Cela rend très difficile l’étude de ces graphes en général. À titre d’exemple, le fameux problème de Syracuse s’intéresse à la terminaison de la boucle décrite (voir la figure 3 ci-dessous) quelle que soit la valeur initiale de la variable x. Même pour ce programme très simple, on ne connaît pas la réponse, et donc encore moins de technique permettant de répondre automatiquement à cette question : on sait même en fait qu’il n’existe pas de programme permettant de résoudre ce problème (c’est l’indécidabilité du problème de l’arrêt étudiée initialement par Alan Turing). Dans la suite, pour pallier cette impossibilité, on se limite à des graphes finis de systèmes. Cela demande souvent d’abstraire les valeurs entières ou flottantes, pour se limiter à un domaine fini de valeurs.

De la vérification à la synthèse

La technique du model checking est mature : de nombreux outils académiques et industriels ont été mis au point et permettent de vérifier des systèmes critiques variés. Les scientifiques tentent désormais d’aller plus loin, en limitant la source principale de bug dans les systèmes : l’intervention humaine. En effet, un bug n’est pas tant un problème du logiciel ou du matériel que la conséquence d’une erreur humaine de conception. Si l’on amoindrit le rôle de l’humain, on diminue les chances de produire des bugs. L’utopie rêvée par les héritiers du model checking est la synthèse automatique. Dans ce cas, on part d’un système partiellement décrit, où certaines parties non critiques du logiciel ont été écrites manuellement, mais où il reste des sections à écrire : on modélise ce système partiel à l’aide d’un graphe dans lequel certaines actions ne sont pas encore fixées (il y a donc un choix à faire entre plusieurs arcs). L’objectif est alors de produire automatiquement un modèle entièrement décrit qui satisfait une spécification : l’écriture de la spécification est laissée à l’humain, dans l’idée (discutable) qu’une spécification est plus aisée à écrire que le programme lui-même. On parle souvent de synthèse de contrôleur : le rôle du contrôleur, qui n’est donc pas un humain, est de guider l’évolution du système afin de satisfaire la spécification. Il ne peut pas contrôler la totalité du système qui est le plus souvent ouvert sur le monde extérieur : par exemple, une fusée doit pouvoir interagir avec des éléments extérieurs (la tour de contrôle) et son environnement (au travers de capteurs : vitesse, altitude…). On cherche donc à décrire un contrôleur qui permettra de satisfaire la spécification quelle que soit la façon dont évoluent les éléments extérieurs. D’autres travaux traitent de synthèse de programme, en utilisant des techniques radicalement différentes.

L’analogie avec un jeu devient alors flagrante : le contrôleur et son environnement peuvent être vus comme deux joueurs, se défiant sur une arène dont les règles du jeu sont dictées par le graphe du système partiellement décrit et la condition de gain pour le contrôleur est donnée par la spécification à satisfaire. Les sommets du graphe sont souvent distribués au joueur, permettant à chacun de jouer à son tour, de la même façon qu’aux échecs on alterne entre un tour du joueur Blanc et du joueur Noir. À son tour, le joueur qui possède le sommet où le système se trouve décide quel arc il utilise pour passer au sommet suivant.

Notons que, dans ce paradigme, l’environnement est un joueur parfaitement antagoniste, dont l’unique objectif est de faire échouer le contrôleur : cela permet de s’assurer que même dans le pire des cas possibles, le système critique ne rencontrera jamais de problème. La synthèse de contrôleur revient alors à trouver, automatiquement si possible, une stratégie gagnante du contrôleur dans ce jeu, c’est-à-dire une recette que le joueur contrôleur doit suivre, lui garantissant de gagner toute partie qu’il jouera contre l’environnement. Si l’on pense à la synthèse du programme d’un bras robotique utilisé le long d’une chaîne de production, le contrôleur a la responsabilité de déplacer le bras selon les contraintes physiques et peut-être aussi la vitesse du tapis roulant face à lui, alors que l’environnement gère l’arrivée d’objets sur la chaîne de production et les éventuelles interruptions du tapis roulant dues aux parties de la ligne qui suivent le bras robotique. La spécification du bras robotique, c’est-à-dire la condition de gain pour le contrôleur, pourrait être de trier les objets par couleur, en les déplaçant sur des tapis identifiés par les couleurs possibles (cf Figure 4).

Le défi est donc de trouver des algorithmes permettant de synthétiser automatiquement de telles stratégies gagnantes pour le contrôleur. C’est un domaine scientifique que l’on appelle la théorie algorithmique des jeux. Non seulement, comme on peut le faire en théorie des jeux appliquée à la biologie ou l’économie, on étudie l’interaction d’agents rationnels qui s’affrontent le long de ce qu’on appelle un jeu, mais en plus on insiste sur la capacité, ou non, de pouvoir réaliser cette étude automatiquement, sans intervention humaine.

Le jeu des pirates

Illustrons cela à l’aide d’un exemple. Imaginons un groupe de cinq pirates qui vient de découvrir un trésor contenant \(100\) pièces d’or. Les pirates sont organisés suivant un ordre hiérarchique simple : la capitaine Élisa, un quartier-maître Dorian, une timonière Cora, son second Barny et tout en bas de l’échelle le matelot pingouin Atchoum. La répartition du butin se réalise en plusieurs phases, résumées dans la figure 5 ci-dessous. Dans un premier temps, la capitaine propose une répartition entre les cinq pirates, puis tout le monde vote (oui ou non) et si au moins la moitié des pirates est d’accord avec la répartition, celle-ci est effectuée et la distribution s’arrête. Sinon, la capitaine est jetée aux requins et c’est son quartier-maître qui devient capitaine et propose à son tour une répartition. À nouveau, tout le monde vote et la répartition n’est actée que si au moins la moitié des pirates est d’accord. Et ainsi de suite, jusqu’à ce qu’une distribution soit acceptée.

Prenons le point de vue de la capitaine Élisa. Son objectif est non seulement de survivre, mais aussi de conserver la plus grande part possible du butin : en termes de vérification de système, la spécification (survivre) est donc complétée par une mesure à optimiser (ici le butin, mais on pourrait imaginer vouloir minimiser l’énergie dépensée ou maximiser la probabilité de succès, dans d’autres situations). Quelle proposition doit-elle ainsi proposer ? Avant de continuer votre lecture, prenez le temps d’y réfléchir un peu… 

Dans la mesure où il n’y a qu’un nombre fini de possibilités de répartition, on pourrait naïvement les générer toutes et simuler les règles du jeu pour en déduire la proposition optimale. Cependant le nombre de possibilités est très grand en pratique (c’est le nombre de Stirling de seconde espèce, qui grandit exponentiellement en fonction du nombre de pirates et du nombre de pièces) et l’approche naïve n’aboutit donc pas. Il nous faut trouver mieux, en réfléchissant un peu…

Puisqu’il faut qu’elle convainque au moins deux autres pirates (pour obtenir une majorité de trois voix, en comptant la sienne), on peut se dire intuitivement qu’elle va diviser le butin en trois environ et donner un tiers du butin à ses deux seconds, Dorian et Cora. Mais la question se pose alors de savoir si une telle répartition lui permet de rester en vie. L’un des deux protagonistes a-t-il intérêt à ne pas accepter cette proposition a priori généreuse ? Autre question, non moins importante pour la vénale Élisa : peut-elle imaginer une proposition plus intéressante pour elle que de ne conserver qu’un tiers du butin ?

Pour nous aider à y voir plus clair, appliquons un raisonnement (ressemblant à une récurrence) consistant à considérer une situation simplifiée à l’extrême puis à augmenter la difficulté petit à petit. Considérons d’abord le cas fort morbide où les trois premiers pirates ont été jetés aux requins, Barny et Atchoum étant les deux seuls pirates encore en vie. Puisque Barny ne va pas refuser sa propre proposition, il peut conserver la totalité du butin et ainsi spolier entièrement Atchoum : il conserve ainsi les \(100\) pièces d’or. Réintroduisons alors Cora dans l’histoire pour voir ce qu’elle a intérêt à faire en sachant la stratégie de Barny si elle venait à disparaître. C’est plus compliqué dans ce cas puisque Cora doit convaincre au moins l’un des deux autres pirates pour survivre. Le plus simple, pour elle, est de corrompre la seule pirate qui n’obtient rien dans le cas où Cora est jetée aux requins, c’est-à-dire Atchoum. Et nos pirates étant des êtres parfaitement rationnels, Atchoum se contentera d’une seule pièce d’or pour voter pour la proposition faite par Cora : celle-ci peut donc proposer la répartition consistant à conserver \(99\) pièces d’or et en donner \(1\) à Atchoum. Le pauvre Barny repart bredouille dans cette situation. Un raisonnement similaire permet de se convaincre qu’avec l’ajout du quatrième pirate Dorian, il lui suffit de corrompre le pirate percevant le moins de butin dans la situation précédente, à savoir Barny. Dorian peut donc proposer en toute sécurité de conserver \(99\) pièces d’or et en donner \(1\) à Barny. Finalement, cela permet d’en conclure la stratégie optimale pour Élisa : elle doit convaincre au moins deux autres pirates de voter pour elle, et elle a tout intérêt à corrompre les pirates qui ne touchent rien dans la situation précédente (où Élisa serait jetée aux requins). Il lui suffit donc de conserver \(98\) pièces d’or et de donner \(1\) pièce à Cora et \(1\) pièce à Atchoum. Élisa gagne alors bien plus que le tiers du butin, même si le partage est pour le moins inéquitable… Voici un tableau résumant les différentes étapes du raisonnement :

À vous de poursuivre le raisonnement dans le cas où il y aurait un sixième, puis un septième pirate. Combien de pirates au maximum peut-il y avoir avant que la capitaine ne puisse plus s’assurer de survivre avec \(100\) pièces d’or ? On peut aussi considérer une variante du jeu où la capitaine doit obtenir une majorité stricte des voix pour survivre…

Résoudre les jeux pour la synthèse de contrôleur

La théorie algorithmique des jeux permet de généraliser ce genre de raisonnement par récurrence à des situations plus complexes. Dans l’application à la vérification, les jeux qui nous intéressent se déroulent sur des graphes (celui du système partiellement décrit) avec deux joueurs seulement (le contrôleur et l’environnement) qui jouent chacun leur tour, selon le joueur à qui appartient le sommet courant. Dans le cas relativement simple où l’objectif du contrôleur est d’éviter la survenue d’un bug (certains sommets cibles du graphe), on parle de jeu de sûreté. Pour résoudre ces jeux, on considère le point de vue de l’environnement qui a l’objectif antagoniste d’atteindre les sommets cibles de bug : on parle alors d’un objectif d’accessibilité. C’est là que le raisonnement par récurrence devient utile. Pour être sûr de gagner dans un certain sommet qui lui appartient, l’environnement doit pouvoir choisir un successeur dans lequel il peut gagner. Inversement, c’est le contrôleur qui gagne dans un sommet qui lui appartient si tout successeur de ce sommet est perdant pour l’environnement (et donc gagnant pour le contrôleur). En partant des sommets de bug (où l’environnement a gagné d’office), on peut donc propager sommet après sommet qui des deux joueurs peut gagner (ou ne peut pas empêcher de perdre). Ce genre de récurrence de théorie des jeux porte le nom d’attracteur, puisqu’on cherche tous les sommets où l’environnement peut attirer la partie dans un sommet cible de bug. Un exemple d’application de l’attracteur est présenté dans la figure 6 ci-dessous. 

Ces techniques d’attracteur sont à la base de bien d’autres algorithmes permettant de résoudre des jeux avec des objectifs plus compliqués. Par exemple, certains systèmes critiques doivent pouvoir fonctionner sans interruption aussi longtemps qu’il plaira aux utilisateurs. Pensez à un ascenseur par exemple, qui ne doit jamais s’interrompre (sauf si c’est planifié par un humain responsable de son entretien). Il est alors plus simple de considérer que le système fonctionnera pendant un temps infini. Dans ce cadre, le contrôleur pourrait vouloir passer infiniment souvent par certains sommets cibles : cela veut dire que régulièrement, on doit visiter un sommet cible du graphe, ce qui peut servir à modéliser par exemple que, sous certaines bonnes hypothèses, un ascenseur passe régulièrement au rez-de-chaussée de l’immeuble, sans rester coincé à faire des navettes uniquement entre les étages supérieurs. Les attracteurs permettent de résoudre ces objectifs aussi puisqu’il s’agit pour le contrôleur d’atteindre un des sommets cibles, puis depuis ce sommet-là, trouver une stratégie pour y revenir une fois : il lui suffit alors de continuer à appliquer cette même stratégie pour y revenir aussi souvent qu’il le désire (et donc une infinité de fois si la partie durait un temps infini).

Des jeux à objectifs quantitatifs

D’autres cas où ces attracteurs sont fort utiles concernent des extensions quantitatives des jeux sur graphes. Le contrôleur souhaite satisfaire une spécification (par exemple atteindre un sommet cible) tout en minimisant les coûts pour y parvenir (ou en maximisant son butin, dans le cas des pirates). On parle de jeu de plus court chemin puisque le contrôleur cherche finalement à produire un plus court chemin vers un sommet cible, quel que soit le comportement de l’environnement. Dans le cas à \(1\) joueur, il existe des algorithmes très efficaces pour résoudre ce problème que les coûts soient des nombres positifs (l’algorithme de Dijkstra suffit alors, plus de détails dans l’article « Le plus court chemin ») ou des nombres quelconques (l’algorithme de Bellman-Ford, par exemple, convient). Lorsqu’on a deux joueurs, on peut adapter ces idées, en intégrant les raisonnements par attracteurs, pour résoudre les jeux correspondants. Un exemple de jeu de plus court chemin et de sa résolution est décrit sur la figure 7 ci-dessous.

Cependant, cela commence à devenir plus complexe en termes de temps de calcul, en particulier dans le cas de nombres quelconques (positifs ou négatifs) où l’on ne connait pas à ce jour d’algorithme résolvant le problème en temps polynomial (en fonction de la taille du jeu). Le meilleur algorithme connu à ce jour demande un temps pseudo-polynomial c’est-à-dire qui dépend (linéairement) des coûts dans le jeu, contrairement aux techniques d’attracteur vues précédemment et l’algorithme de Dijkstra qui ne dépendent (polynomialement) que du nombre de sommets dans le graphe. Cela reflète une particularité de ces jeux : le contrôleur nécessite de la mémoire pour jouer optimalement dans de tels jeux (cf figure 8 ci-dessous), c’est-à-dire que le contrôleur ne peut pas toujours suivre la même stratégie lorsqu’il passe par un certain sommet du graphe, il doit parfois suivre un arc et parfois un autre. C’est très différent des autres classes de jeux cités avant, où des stratégies sans mémoire (c’est-à-dire où le contrôleur n’a pas besoin de changer d’avis) suffisent.

Autres extensions

À partir de ces objectifs de base sur des jeux représentant des systèmes partiellement décrits, on peut considérer des extensions permettant de modéliser mieux les situations réelles à synthétiser. En particulier, beaucoup de systèmes critiques doivent agir en temps réel, et les spécifications peuvent donc intégrer ces aspects temporels : dans un système d’ABS gérant le freinage d’une voiture, il est ainsi important que l’appui sur la pédale de frein résulte dans le futur en le freinage de la voiture, mais on veut en plus que celui-ci intervienne relativement rapidement après, sans quoi l’accident est inévitable. D’autres extensions permettent de remplacer la mémoire, dont on a vu avant qu’elle pouvait être nécessaire pour jouer optimalement, par des tirages aléatoires. En effet, dans certains cas, on arrive à simuler la mémoire en utilisant un tirage aléatoire (avec une chance sur 10 suivre un arc, et avec 9 chances sur 10 d’en suivre un autre) : l’usage de probabilités est indispensable aussi dans d’autres domaines de la théorie des jeux, par exemple lorsqu’on souhaite trouver une stratégie optimale dans le jeu pierre-feuille-ciseaux (c’est-à-dire un équilibre de Nash dans un jeu donné sous forme stratégique, où toutes les combinaisons de stratégies des joueurs sont associées à une valeur gagnée par chaque joueur dans ce cas – voir l’article « Quand l’informatique rencontre les sciences économiques » sur les liens entre les équilibres de Nash et l’économie). Finalement, d’autres extensions considèrent les pannes que le système peut rencontrer au cours de son évolution : cela se modélise par la suppression dynamique de certains arcs dans le graphe, au moins pour un certain temps. Le contrôleur doit pouvoir dynamiquement mettre à jour sa stratégie dans ce genre de cas : des ponts ont ainsi commencé à être tracés avec la théorie évolutionnaire des jeux, un autre sous-domaine de la théorie des jeux s’intéressant à l’évolution des stratégies des protagonistes au cours du temps.