Contribution a l'algorithmique de la verification

André Arnold

Description

Niveau: Supérieur
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

Sujets

• Arnold
• Laboratoire bordelais de recherche en informatique
• Finkel
• Haddad
• Esparza
• Vérification

Informations

• Publié par: profil-nechor-2012
• Publié le: 01 juillet 2004
• Nombre de lectures: 57
• Langue: Français
• Poids de l'ouvrage: 2 Mo

Extrait

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