these

Universite Paris 7 - Denis DiderotUFR d’InformatiqueTHESEpour l’obtention du titre deDocteur de l’Universite Paris 7Specialite Informatiquepresentee parDenis Oddouxsur le sujetUtilisation des automates alternantspour un model-checking e cacedes logiques temporelles linerairessoutenue publiquement le 17 decembre 2003 devant le jury suivant :Jean-Eric Pin President du JuryBeatrice Berard RapporteuseNicolas Halbwachs RapporteurPaul Gastin Directeur de TheseThomas WilkePierre WolperRemerciementsJe 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, ThomasWilke et Pierre Wolper pour avoir accepte de participer au jury.Je tiens particulierement a remercier Paul Gastin pour m’avoir guide dans mon travailau cours de ces annees, pour son attention et son aide a mes travaux de recherche, pour sadisponibilite exceptionnelle, et pour avoir ete capable, en toutes circonstances, de trouverune 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 aucours des nombres pauses-gouter^ autour de la fontaine, ainsi que l’ensemble des personnesque j’ai pu rencontrer au cours de ces trois annees au LIAFA.Table des matieresTable des matieres 51 Introduction generale 91.1 Les methodes de veri cation . . . . . . . . . . . . . . . . . . . ...