these

Universite Paris 7 - Denis Diderot
UFR d’Informatique
THESE
pour l’obtention du titre de
Docteur de l’Universite Paris 7
Specialite Informatique
presentee par
Denis Oddoux
sur le sujet
Utilisation des automates alternants
pour un model-checking e cace
des logiques temporelles lineraires
soutenue publiquement le 17 decembre 2003 devant le jury suivant :
Jean-Eric Pin President du Jury
Beatrice Berard Rapporteuse
Nicolas Halbwachs Rapporteur
Paul Gastin Directeur de These
Thomas Wilke
Pierre WolperRemerciements
Je remercie Jean-Eric Pin de m’avoir fait l’honneur de presider le jury de cette these,
Beatrice Berard et Nicolas Halbwachs d’avoir accepte d’en ^etre les rapporteurs, Thomas
Wilke et Pierre Wolper pour avoir accepte de participer au jury.
Je tiens particulierement a remercier Paul Gastin pour m’avoir guide dans mon travail
au cours de ces annees, pour son attention et son aide a mes travaux de recherche, pour sa
disponibilite exceptionnelle, et pour avoir ete capable, en toutes circonstances, de trouver
une solution constructive a chacune de mes di cult es.
Je remercie en n les joyeux lurons de PPS pour leur accueil et leur soutien moral au
cours des nombres pauses-gouter^ autour de la fontaine, ainsi que l’ensemble des personnes
que j’ai pu rencontrer au cours de ces trois annees au LIAFA.Table des matieres
Table des matieres 5
1 Introduction generale 9
1.1 Les methodes de veri cation . . . . . . . . . . . . . . . . . . . . . . . . . . 9
1.1.1 Les tests . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 9
1.1.2 Les methodes formelles . . . . . . . . . . . . . . . . . . . . . . . . . 10
1.1.3 Methodes formelles ou tests, que choisir ? . . . . . . . . . . . . . . . 11
1.2 Le model-checking . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 11
1.2.1 Le modele . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 12
1.2.2 La speci cation . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 12
1.2.3 Les algorithmes de model-checking . . . . . . . . . . . . . . . . . . 13
1.3 Contenu de la these . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 13
I Notions de base 15
2 Logiques temporelles lineaires 17
2.1 LTL . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 18
2.1.1 De nitions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 18
2.1.2 Simpli cation . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 19
2.2 PLTL : LTL avec passe . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 20
2.3 Exemples . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 22
3 Model-checking pour LTL et PLTL 23
3.1 Formalismes utilises . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 23
3.2 Algorithme general de model-checking . . . . . . . . . . . . . . . . . . . . . 24
3.2.1 Complexite . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 24
3.2.2 Principe general . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 25
3.2.3 Explications . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 26
3.3 De la logique temporelle aux automates . . . . . . . . . . . . . . . . . . . . 27
3.3.1 La methode des tableaux . . . . . . . . . . . . . . . . . . . . . . . . 27
3.3.2 Methodes incrementales . . . . . . . . . . . . . . . . . . . . . . . . 29
56 Table des matieres
II Model-checking e cace pour LTL 31
Introduction . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
Motivations . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
Approche utilisee . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
Simpli cations . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
Implementation . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
Plan de la partie . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
4 Automates alternants 37
4.1 De nitions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
4.1.1 Combinaisons booleennes positives . . . . . . . . . . . . . . . . . . 37
4.1.2 Automates alternants . . . . . . . . . . . . . . . . . . . . . . . . . . 38
4.1.3 Q-for^et, execution, langage . . . . . . . . . . . . . . . . . . . . . . . 38
4.1.4 Q-DAGs . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40
4.2 Exemple . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42
4.3 De LTL aux automates alternants tres faibles . . . . . . . . . . . . . . . . 44
4.3.1 Construction . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44
4.3.2 Preuve de l’equivalence . . . . . . . . . . . . . . . . . . . . . . . . . 45
4.3.3 Complexite . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49
5 Automates de Buc hi generalises 51
5.1 De nition . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 51
5.2 Exemple . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 52
5.3 Des automates alternants tres faibles aux automates de Buc hi generalises . 52
5.3.1 Construction . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 52
5.3.2 Preuve de l’equivalence . . . . . . . . . . . . . . . . . . . . . . . . . 54
5.3.3 Complexite . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 56
6 Model-checking pour LTL 57
6.1 Des automates de Buc hi generalises aux automates de Buc hi classiques . . 57
6.1.1 Construction . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 58
6.1.2 Automates d’acceptation . . . . . . . . . . . . . . . . . . . . . . . . 58
6.1.3 Preuve de l’equivalence . . . . . . . . . . . . . . . . . . . . . . . . . 60
6.1.4 Complexite . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 61
6.2 Automates de Buc hi generalises et model-checking . . . . . . . . . . . . . . 61
6.2.1 Principe . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 61
6.2.2 Complexite . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 61
7 Implementation 63
7.1 Optimisation des structures de donnees . . . . . . . . . . . . . . . . . . . . 63
7.1.1 L’etiquetage des transitions . . . . . . . . . . . . . . . . . . . . . . 63
7.1.2 Transitions des automates alternants . . . . . . . . . . . . . . . . . 64
7.1.3 De nitions et constructions . . . . . . . . . . . . . . . . . . . . . . 65Table des matieres 7
7.2 Simpli cation des automates . . . . . . . . . . . . . . . . . . . . . . . . . . 67
7.2.1 Simpli cation des transitions . . . . . . . . . . . . . . . . . . . . . . 68
7.2.2 des etats . . . . . . . . . . . . . . . . . . . . . . . . . 71
7.2.3 Utilisation des composantes fortement connexes . . . . . . . . . . . 72
7.2.4 Simpli cation a la volee . . . . . . . . . . . . . . . . . . . . . . . . 73
7.3 Resultats experimentaux . . . . . . . . . . . . . . . . . . . . . . . . . . . . 73
7.4 L’outil ltl2ba . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 76
7.4.1 Utilisation . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 76
7.4.2 Structure du programme . . . . . . . . . . . . . . . . . . . . . . . . 77
7.4.3 Interface web . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 78
7.4.4 References web . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 78
III L’extension a PLTL 81
Introduction . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 83
Motivations . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 83
Choix d’une approche . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 83
Approche utilisee . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 84
Plan de la partie . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 85
8 Automates alternants a double sens 87
8.1 De nitions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 87
8.1.1 Automates alternants a double sens . . . . . . . . . . . . . . . . . . 87
8.1.2 progressants . . . . . . . . . . . . . . . . . . . . . . . . 89
8.2 Exemple . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 95
8.3 Des automates alternants tres faibles a double sens aux automates progressants 96
8.3.1 Construction . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 96
8.3.2 Preuve de l’equivalence . . . . . . . . . . . . . . . . . . . . . . . . . 97
8.3.3 Complexite . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 99
8.4 De PLTL aux automates progressants tres faibles . . . . . . . . . . . . . . 99
8.4.1 Construction . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 99
8.4.2 Preuve de l’equivalence . . . . . . . . . . . . . . . . . . . . . . . . . 101
8.4.3 Complexite . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 110
9 Automates de Buc hi a memoire 111
9.1 De nition . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 112
9.2 Des automates progressants tres faibles aux automates de Buc hi a memoire 112
9.2.1 Premiere construction . . . . . . . . . . . . . . . . . . . . . . . . . 112
9.2.2 Preuve de l’equivalence . . . . . . . . . . . . . . . . . . . . . . . . . 113
9.2.3 Complexite . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 114
9.2.4 Deuxieme Construction . . . . . . . . . . . . . . . . . . . . . . . . . 114
9.2.5 Preuve de l’