Contribution a l'algorithmique de la verification
122
pages
Français
Documents
2004
Le téléchargement nécessite un accès à la bibliothèque YouScribe Tout savoir sur nos offres
122
pages
Français
Documents
2004
Le téléchargement nécessite un accès à la bibliothèque YouScribe Tout savoir sur nos offres
Publié par
Publié le
01 juillet 2004
Nombre de lectures
58
Langue
Français
Poids de l'ouvrage
2 Mo
Contribution a l'algorithmique de la verification (Memoire d'habilitation a diriger des recherches) Jean-Michel COUVREUR Laboratoire Bordelais de Recherche en Informatique CNRS UMR 5800 - Universite Bordeaux I Laboratoire Specification et Verification CNRS UMR 8643 - ENS de Cachan Presente le 6 juillet 2004 a l'ENS de Cachan devant un jury compose de : – Andre Arnold examinateur – Javier Esparza examinateur – Alain Finkel examinateur – Paul Gastin president – Serge Haddad rapporteur – Philippe Schnoebelen examinateur – Igor Walukiewicz rapporteur – Pierre Wolper rapporteur
- verification
- produit de reseaux symetriques
- construction globale
- abordees dans le cadre de projets industriels
- prefixe fini complet
- produit de reseaux de petri
- structure originale de diagrammes de decision adaptee
Publié par
Publié le
01 juillet 2004
Nombre de lectures
58
Langue
Français
Poids de l'ouvrage
2 Mo
Contribution a l’algorithmique
de la veri cation
(Memoire d’habilitation a diriger des recherches)
Jean-Michel COUVREUR
Laboratoire Bordelais de Recherche en Informatique
CNRS UMR 5800 - Universite Bordeaux I
Laboratoire Specication et Verication
CNRS UMR 8643 - ENS de Cachan
Presente le 6 juillet 2004 a l’ENS de Cachan devant un jury compose de :
– Andre Arnold examinateur
– Javier Esparza examinateur
– Alain Finkel examinateur
– Paul Gastin president
– Serge Haddad rapporteur
– Philippe Schnoebelen examinateur
– Igor Walukiewicz rapporteur
– Pierre Wolper rapporteurTable des matieres
1 Introduction 1
2 Logique temporelle lineaire 3
2.1 Modeles du temps lineaire . . . . . . . . . . . . . . . . . . . . . . 5
2.2 Traduction d’une formule LTL en ω-automate . . . . . . . . . . . 6
2.2.1 Automates a transitions . . . . . . . . . . . . . . . . . . . 7
2.2.2 Construction globale . . . . . . . . . . . . . . . . . . . . . 8
2.2.3 Construction locale . . . . . . . . . . . . . . . . . . . . . . 15
2.2.4 Experimentations . . . . . . . . . . . . . . . . . . . . . . . 20
2.3 Tester le vide d’un ω-automate . . . . . . . . . . . . . . . . . . . 22
2.4 Verication de systemes probabilistes . . . . . . . . . . . . . . . 31
2.4.1 Notions de mesure . . . . . . . . . . . . . . . . . . . . . . 32
2.4.2 Systeme de transitions probabiliste . . . . . . . . . . . . . 33
2.4.3 Proprietes du produit synchronise . . . . . . . . . . . . . 34
2.4.4 Probleme de la satisfaction . . . . . . . . . . . . . . . . . 35
2.4.5 Probleme de l’evaluation . . . . . . . . . . . . . . . . . . . 37
2.4.6 Experimentations . . . . . . . . . . . . . . . . . . . . . . . 37
2.5 Conclusion . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40
3 Depliages de reseaux de Petri 43
3.1 Notions elementaires . . . . . . . . . . . . . . . . . . . . . . . . . 44
3.1.1 Reseaux de Petri . . . . . . . . . . . . . . . . . . . . . . . 44
3.1.2 Homomorphisme de reseaux . . . . . . . . . . . . . . . . . 46
3.1.3 Reseau d’occurrence . . . . . . . . . . . . . . . . . . . . . 47
3.2 Processus arborescent et depliage . . . . . . . . . . . . . . . . . . 49
3.2.1 Processus arborescents . . . . . . . . . . . . . . . . . . . . 50
3.2.2 Depliages . . . . . . . . . . . . . . . . . . . . . . . . . . . 51
3.3 Pre xes nis . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 52
3.3.1 De nition . . . . . . . . . . . . . . . . . . . . . . . . . . . 52
3.3.2 Ordres adequats et pre xes nis complets . . . . . . . . . 53
3.3.3 Verication de propriete de suˆrete . . . . . . . . . . . . . 56
3.3.4 Detection de comportements innis . . . . . . . . . . . . . 56
3.4 Graphes de pre xes
