25/11/2004
Marc Zeitoun (LIAFA)
Jeux concurrents à mémoire causale

On peut modéliser le contrôle d'un système séquentiel évoluant dans un environnement (a priori hostile) par un jeu à deux joueurs : l'un représente l'environnement, l'autre le contrôleur à mémoire finie qui doit inhiber intelligemment des actions possibles du système afin que le comportement du système dans l'environnement satisfasse une propriété donnée à l'avance.

Trouver un contrôleur se ramène ainsi au calcul d'une stratégie gagnante pour le joueur « contrôleur ». Si l'ensemble des comportements souhaité est raisonnable (omega-rationnel), il est connu que l'on peut décider si une telle stratégie existe, et la synthétiser avec des algorithmes efficaces.

Dans le contexte séquentiel, chacun des joueurs a une information parfaite. Dans le contexte concurrent, le contrôleur que l'on veut synthétiser doit être distribué sur l'architecture du système. Chaque processus du système à contrôler se modélise alors par un joueur d'une même équipe, opposée à l'environnement. La différence majeure avec le cadre séquentiel est que ces joueurs n'ont pas une connaissance parfaite de l'état global du système, mais seulement une vue partielle. La mémoire utilisable par les stratégies des jeux correspondants est ainsi plus faible.

Lorsque chaque processus ne peut se que rappeler des actions qu'il a faites dans le passé, on parle de mémoire locale. Avec cette notion de mémoire, même les jeux d'accessibilité sont indécidables. Nous introduisons une autre notion de mémoire pour les processus d'un système concurrent, naturelle et implantable, appelée mémoire causale. Nous montrons que pour une large classe de systèmes incluant les cas indécidables précédents, le problème de synthèse de stratégie est décidable avec cette nouvelle notion.