34e École de Printemps en Informatique Théorique (EPIT 2006)
Ile de Ré, du dimanche 28 mai au vendredi 2 juin 2006
Organisation : Paul-André Melliès (PPS) et Anca Muscholl (LIAFA)
| Samson Abramsky (Oxford, UK) | Algorithmic and Concurrent Game Semantics |
| Jacques Duparc (Lausanne, Suisse) | Describing the Complexity of ω-Languages with Games |
| Paul Gastin (LSV, ENS Cachan) | Distributed synthesis: synchronous and asynchronous semantics |
| Erich Grädel (Aachen, Allemagne) | Games and Fixed Point Logics |
| Martin Hyland (Cambridge, UK) | Games and proofs |
| Luke Ong (Oxford, UK) | Infinite trees, higher-order recursion schemes and game semantics |
| Tristan Tomala (Ceremade, Paris Dauphine) | Jeux répétés et transmission d'information |
| Igor Walukiewicz (Bordeaux) | Pushing the limits of the μ-calculus |
| Wieslaw Zielonka (Paris) | Jeux de parité stochastiques |
En trente ans à peine, l'informatique est passée des systèmes fermés (les calculateurs d'antan) aux systèmes ouverts (sur la toile et les réseaux). Aussi, l'ordinateur d'aujourd'hui n'a plus rien de l'entité autonome et récursive que l'on connaissait il y a quelques années. Il s'assimile au contraire à une communauté concertante d'agents interactifs, qui évoluent de manière indépendante et concurrente. Décrire et vérifier le bon comportement d'un tel « écosystème calculatoire » représente un défi scientifique majeur de notre époque – et fait l'objet de recherches très actives à l'interface entre Informatique et Mathématique. Car au delà du désordre combinatoire apparent, il s'agit de repenser la théorie classique de la récursivité (héritée de Gödel, Kleene et Turing) et de produire les fondations conceptuelles et mathématiques de cette « informatique ouverte » à venir.
La théorie des jeux est l'un des candidats les plus sérieux pour une telle refondation. Il y a plusieurs raisons à cela. Tout d'abord, cette théorie offre un cadre naturel pour modéliser les interactions entre plusieurs entités ou agents concertants. Ensuite, la théorie des jeux s'est imposée depuis une quinzaine d'années dans des branches très variées de l'informatique, depuis l'étude mathématique des langages de programmation (Sémantique) jusqu'à la spécification et la validation formelle de programmes concurrents (Vérification). Enfin, la théorie des jeux est fortement ancrée et déjà très étudiée dans d'autres domaines de l'informatique et/ou des mathématiques, tels que la logique, les systèmes dynamiques et les sciences économiques.
L'École de Printemps 2006 se concentrera sur les développements récents de la théorie des jeux en Sémantique et en Vérification. Dans chacune de ces deux thématiques, on s'intéresse au comportement d'un programme placé en face d'un environnement d'évaluation. Dans l'approche ludique qui nous intéresse ici, les deux entités, programme et environnement, sont compris comme deux joueurs (ou deux stratégies) adverses qui s'affrontent en une partie sur un certain jeu défini par la spécification du système.
Dans un langage de programmation typé, chaque programme dispose d'un certain type, qui en spécifie les propriétés cardinales. Interpréter le langage consiste à transporter la « grammaire » du langage de type dans la « grammaire » d'une certaine catégorie de jeu. De la sorte, on sait associer un jeu à chaque type du langage ; et à chaque programme et environnement d'un type donné une stratégie et une contre-stratégie du jeu associé à ce type. La sémantique offre ainsi un cadre algébrique pour calculer explicitement le jeu et les stratégies associés à un programme et à son environnement. Cette sémantique est par nature modulaire et compositionnelle : la sémantique d'un programme est le produit de la sémantique de ses composantes. On peut donc remplacer sans risque une composante d'un programme par une composante plus efficace et de même sémantique.
Dans ce cadre, spécifier un programme revient à définir formellement un jeu ; tandis que vérifier que le programme satisfait la spécification revient à vérifier que la stratégie est gagnante dans le jeu défini par la spécification. Une question plus difficile consiste ensuite à synthétiser un programme qui se comporterait bien vis-à-vis d'une spécification donnée, quelque soit le comportement de l'environnement. Ce problème de synthèse automatique peut être formulé de la sorte : il s'agit de calculer une stratégie gagnante dans le jeu défini par la spécification – cela afin d'en déduire le programme synthétisé. On peut vouloir aussi contrôler un programme existant afin de satisfaire une spécification donnée (quelque soit le comportement de l'environnement). Dans ce cas, le contrôleur est une stratégie gagnante qui représente le programme valide dans le fragment du jeu exploré par le programme initial.
Il transparait de ce court exposé que la théorie des jeux offre un point de ralliement naturel entre deux branches de l'informatique mathématique (Sémantique et Vérification) qui s'étaient séparées à la fin des années 1970. De fait, la question de la Vérification est apparue récemment en Sémantique lorsqu'on a ramené l'équivalence contextuelle entre certains programmes d'Algol Idéalisé à l'égalité de langages rationnels ou de langages algébriques restreints (déterministes, avec visibilité, ...). Réciproquement, la question de la Sémantique est apparue tout aussi récemment en Vérification autour des problèmes de modularité et de compositionalité, étudiés par exemple dans les jeux d'interfaces.
Il apparait donc primordial aujourd'hui de réunir les meilleurs spécialistes de la théorie des jeux sous les deux aspects mentionnés, la Sémantique et la Vérification. La convergence de ces deux communautés autour de la théorie des jeux est un préalable indispensable à l'émergence d'une théorie générale de la sémantique et de la vérification des programmes ouverts sûrs. De ce point de vue, l'Ecole de Printemps 2006 sera un événement fondateur. Il s'agira en effet de la première rencontre nationale ou internationale dédiée à la théorie des jeux, dans laquelle les deux communautés Sémantique et Vérification se rencontreront à pied d'égalité. Les organisateurs de cette Ecole représentent deux laboratoires très actifs dans le domaine des jeux. Le LIAFA fait partie du réseau européen TMR GAMES (2002-2006), dont les objectifs portent sur les aspects des jeux liés à la vérification. Le laboratoire PPS a fait quant à lui de la sémantique des jeux l'un de ses principaux domaines de recherche et d'expertise.
Partenaires et soutiens de l'École de Printemps 2006
Cette page est maintenue par Samuel Mimram.
