Parisian Master of Research in Computer Science
Master Parisien de Recherche en Informatique (MPRI)

Differences

This shows you the differences between two versions of the page.

Link to this comparison view

cours:c-2-20 [2011/07/12 19:26] (current)
Line 1: Line 1:
 +
 +===== Jeux et logique (48h, 6 ECTS) =====
 +
 +Responsables : Anca Muscholl et Jean-Éric Pin
 +
 +==== Plan du cours et intervenants prévus pour 2005-2006 ====
 +
 +  -  Automates et mots infinis, logique premier ordre (12h, Jean-Eric Pin
 +  -  Logique sur mots infinis, automates a parite, jeux et strategies (12h, Olivier Carton
 +  -  Algorithmes de jeux de parite, automates d'arbres (12h, Anca Muscholl
 +  -  Jeux stochastiques, jeux et Internet (12h, Wieslaw Zielonka
 +
 +==== Objectifs ====
 +
 +Précisons qu'il s'agit ici des jeux à deux joueurs sur des graphes
 +finis ou infinis, qui sont différents des jeux utilisés en économie
 +ou en optimisation.
 +
 +Les jeux représentent un formalisme mathématique puissant utilisé
 +largement dans des branches très variées de l'informatique allant de
 +la théorie de la complexité jusqu'à la vérification formelle.
 +
 +Dans ce module nous allons nous intéresser surtout aux aspects liés
 +à la théorie des automates, la vérification et la logique, trois
 +domaines qui sont en fait étroitement reliés.
 +
 +Dans ce contexte on trouve plusieurs types de jeux déjà bien connus
 +et étudiés. Tout d'abord, les plus anciens de ces jeux, les jeux
 +d'Ehrenfeucht-Fraïssé, qui fournissent une méthode efficace
 +pour caractériser l'expressivité des formules logiques. Les jeux
 +d'Ehrenfeucht-Fraïssé ont été utilisés avec succès dans
 +l'étude de la logique temporelle linéaire en exhibant en même
 +temps les liens entre cette logique et la théorie des langages.
 +
 +Un autre exemple classique est donné par les jeux de parité où le
 +problème de calcul de la stratégie gagnante est directement lié
 +au problème de model-checking des formules de mu-calcul sur de
 +structures finies. Pour ce problème, qui est a été pendant
 +quelques années la question clé du domaine, une solution
 +polynomiale a été annoncée très récemment.
 +
 +De façon générale, les jeux donnent un cadre naturel pour
 +modéliser les interactions entre plusieurs entités. En
 +vérification formelle par exemple, on examine les systèmes
 +réactifs où on s'intéresse à l'interaction entre le programme
 +et son environnement, qui peuvent être représentés comme deux
 +joueurs adverses. Une des applications est la synthèse automatique de
 +contrôleurs, qui, dans cette approche, se réduit au calcul d'une
 +stratégie gagnante du joueur représentant le programme. Par
 +exemple, _spécifier//un module revient à définir
 +formellement un jeu, _synthétiser//un module revient à
 +calculer une stratégie gagnante et _vérifier//un module
 +vis-à-vis d'une spécification revient à vérifier qu'une
 +stratégie est gagnante.
 +
 +
 +==== Plan du cours ====
 +
 +=== Automates et mots infinis ===
 +
 +Cette partie du cours s'appuiera sur le livre <cite>Infinite Words</cite> de
 +D. Perrin et J.-E. Pin. Utiliser les automates finis pour
 +reconnaître des mots infinis est une idée un peu surprenante en
 +soi. On verra les différentes façons d'y parvenir (automates de
 +Büchi, de Muller et de Rabin) et les algorithmes correspondants. On
 +montrera ensuite comment les approches algorithmique, algébrique,
 +topologique et logique se combinent entre elles de façon
 +particulièrement attractive.
 +
 +=== Automates d'arbres et logique ===
 +
 +Cette partie du cours s'appuiera sur les chapitres de livres <cite>Automata
 +on infinite objects</cite> (Handbook of Theoretical Computer Science) et
 +<cite>Languages, automata, and logic</cite> (Handbook of Formal Languages), de
 +W. Thomas, ainsi que sur le livre <cite>Tree Automata Techniques and
 +Applications</cite>, de H. Comon et al. On montrera les liens entre les
 +automates d'arbres et la logique du second ordre, ainsi qu'entre les
 +jeux et les automates d'arbres alternants.
 +
 +=== Jeux de parité et jeux stochastiques ===
 +
 +Cette partie du cours montrera le lien entre le mu-calcul et les jeux
 +de parité, ainsi que les algorithmes récents proposé pour
 +décider le gagnant dans les jeux de parité sur les graphes finis. 
 +Ensuite elle introduira la théorie des jeux
 +stochastiques, qui jouent un rôle clé dans les problèmes de
 +contrôle, et les algorithmes permettant de déterminer le gagnant
 +pour des conditions simples de victoire.
 +
 +=== Jeux et graphes infinis ===
 +
 +Cette partie du cours sera dediée aux jeux sur des graphes infinis.
 +On montrera le théorème de determination et de l'existence de
 +stratégies sans mémoire pour les jeux à condition de chaine de
 +Rabin (Gurevich/Harrington, McNaughton, Zielonka). Ensuite on montrera
 +les résultats de décidabilité et de construction de stratégies
 +pour les jeux sur les graphes d'automates à pile et sur des modèles
 +étendus.
 +
 +=== Jeux combinatoires ===
 +
 +Cette partie du cours introduira la théorie des jeux combinatoires
 +à la Conway, en s'appuyant sur le livre <cite>On Numbers and Games</cite>
 +de John H. Conway.
 +
 +==== Prérequis ====
 +
 +Prérequis : connaissances de base sur les automates finis (théorème
 +de Kleene et algorithmes de base), les automates à pile, la
 +calculabilité et la complexité.
 +
 +==== Bibliographie ====
 +
 +<html><dl>
 +<dt>Automates, Jeux et Logique</dt>
 +<dd>
 +   * Dominique Perrin et Jean-Éric Pin, <cite>Infinite Words</cite>, Academic Press, Pure and Applied Mathematics Vol 141, 2004, ISBN 0-12-532111-2.
 +   * Erich Grädel, Wolfgang Thomas et Thomas Wilke, <cite>Automata, Logics, and Infinite Games</cite>, Springer, Lecture Notes in Computer Science **2500**, 2002.
 +</dd>
 +
 +<dt>Jeux finis</dt>
 +<dd>
 +   * E.Berlekamp, J.H.Conway, R.Guy, <cite>Winning ways for your mathematical plays</cite>, vol.1,2
 +   * John H. Conway, <cite>On Numbers and Games</cite>
 +   * Bernd Kummer, <cite>Spiele auf Graphen</cite>
 +</dd>
 +
 +<dt>Jeux boreliens et jeux de Wadge</dt>
 +<dd>
 +   * A. Kechris, <cite>Classical Descriptive Set Theory</cite>
 +</dd>
 +
 +<dt>Jeux boréliens</dt>
 +<dd>
 +   * Y. Moschovakis, <cite>Descriptive Set Theory</cite>
 +</dd>
 +
 +<dt>Jeux d'Ehrenfeucht Fraïssé</dt>
 +<dd>
 +   * H-D Ebbinghaus, J.Flum, <cite>Finite Model Theory</cite>
 +</dd>
 +
 +<dt>Jeux stochastiques</dt>
 +<dd>
 +   * J. Filar, K. Vrieze, <cite>Competitive Markov decision  processes</cite>, Springer, 1997.
 +</dd>
 +
 +<dt>Théorie classique des jeux</dt>
 +<dd>
 +   * N.N. Vorob'ev, <cite>Game theory</cite>, Springer Verlag
 +</dd>
 +
 +</dl></html>
 +
 +==== Équipe pédagogique ====
 +
 +|J.-E. Pin|DR|CNRS|LIAFA|
 +|O. Carton|PU|Paris 7|LIAFA|
 +|A. Muscholl|PU|Paris 7|LIAFA|
 +|W. Zielonka|PU|Paris 7|LIAFA|
 +|0. Serre|CR|CNRS|LIAFA|
 +
 +<p />
 +==== <a name="Documents et Transparents"> ]] Documents et Transparents  ====
 +<p />
 +[[http://liafa.jussieu.fr/~jep/MPRI/MPRI.html| J.-E. Pin]] 
 +<p />
 +[[http://www.liafa.jussieu.fr/~zielonka/Enseignement/MPRI2005/index.html| W. Zielonka]] 
 +
 +==== Les années précédentes ====
 +
 +      * [[2009-2010-C-2-20|Année 2009-2010]]
 +** Année  [[2008-2009-C-2-20|2008-2009]]
 +
 +------
 +   * Set ALLOWTOPICCHANGE = %MAINWEB%.WebMastersGroup, %MAINWEB%.MarcZeitoun
 +
  
 
Universités partenaires Université Paris-Diderot
Université Paris-Saclay
ENS Cachan École polytechnique Télécom ParisTech
ENS
Établissements associés Université Pierre-et-Marie-Curie CNRS INRIA CEA