École Polytechnique
Majeure 2
Spécialité Informatique
Vérification
des
Systèmes
Réactifs
Temps-Réel
Jean-Pierre Jouannaud
Professeur
Université Paris-Sud
École PolytechniqueAdresses de l’auteur :
LIX
Bureau 101
École Polytechnique
F-91128 Palaiseau CEDEX
Email :Jean-Pierre.Jouannaud@lix.polytechnique.fr
Tél : 01 69 33 40 70
Fax : Tél : 01 69 33 30 14
URL :http://www.lix.polytechnique.fr/
&
LRI, Bâtiment 490
bureau 128
Université Paris-Sud
F-91405 Orsay CEDEX
URL :http://www.lri.fr/~jouannau/ii Table des matières
Table des matières
1 Introduction 1
2 Automates de mots finis 3
2.1 Automates déterministes . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 3
2.2 non . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 4
2.3 Décision du vide d’un automate . . . . . . . . . . . . . . . . . . . . . . . . . . . . 6
2.4 Élimination des transitions vides d’un automate . . . . . . . . . . . . . . . . . . . . 7
2.5 Déterminisation d’un automate non-déterministe . . . . . . . . . . . . . . . . . . . 8
2.6 Minimisation d’un déterministe . . . . . . . . . . . . . . . . . . . . . . . 8
2.6.1 Automate minimal . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 9
2.6.2 Calcul de l’automate minimal . . . . . . . . . . . . . . . . . . . . . . . . . 10
2.7 Propriétés de pompage et de clôture des langages reconnaissables . . . . . . . . . . 13
2.8 Exercices . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 15
3 Modélisation de ...