Utilisation des langages d'arbres pour la modélisation et la vérification des systèmes à états infinis
Ce document présente différents outils pour représenter et manipuler des ensembles infinis de n-uplets d'arbres appelés langages de n-uplets d'arbres. Nous avons choisi la programmation logique comme formalisme pour décrire les langages de n-uplets d'arbre (c.à.d. les relations) et le...
Αποθηκεύτηκε σε:
| Κύριος συγγραφέας: | |
|---|---|
| Άλλοι συγγραφείς: | , |
| Μορφή: | Thèse et Mémoire papier |
| Γλώσσα: | Français |
| Έκδοση: |
[S.l.] :
[s.n.]
2007.
|
| Θέματα: | |
| Autres localisations: | Voir dans le Sudoc |
| Variante du titre: | Using tree languages for modelise and verify infinite states systems |
| Edition sous un autre format: | • Utilisation des langages d'arbres pour la modélisation et la vérification des systèmes à états infinis, par Pierre Pillot, 2010, Villeurbanne, [CCSD] |
| LEADER | 03496nam a22003017a 4500 | ||
|---|---|---|---|
| 001 | 255560 | ||
| 008 | 080627s2007 xxe ||| |||| 00| 0 fre d | ||
| 009 | PPN125260717 | ||
| 041 | 0 | |a fre |b fre |b eng | |
| 084 | |a 004 | ||
| 100 | 1 | |a Pillot, Pierre, |d 1979- . | |
| 240 | 1 | 0 | |a Using tree languages for modelise and verify infinite states systems |
| 245 | 1 | 0 | |a Utilisation des langages d'arbres pour la modélisation et la vérification des systèmes à états infinis |c par Pierre Pillot ; [sous la direction de] Pierre Réty,... [et de] Sébastien Limet,... |
| 260 | |a [S.l.] : |b [s.n.], |c 2007. | ||
| 300 | |a 1 vol. (130 p.) ; |c 30 cm. | ||
| 502 | |a Thèse de doctorat. Informatique. Orléans. 2007 | ||
| 504 | |a Bibliogr. p. 123-130 | ||
| 506 | |a Publication autorisée par le jury | ||
| 520 | |a Ce document présente différents outils pour représenter et manipuler des ensembles infinis de n-uplets d'arbres appelés langages de n-uplets d'arbres. Nous avons choisi la programmation logique comme formalisme pour décrire les langages de n-uplets d'arbre (c.à.d. les relations) et les techniques de transformations de programmes pour calculer les opérations sur ceux-ci. Dans un premier temps on étudie une classe de relations closes par la plupart des opérations ensemblistes, la classe des relations pseudo-régulières. Grâce à un lien entre programmes logiques et systèmes de réécriture, nous définissons des classes de systèmes de réécriture conditionnelle dont la clôture transitive est une relation pseudo-régulière. On applique ce résultat pour donner une classe décidable de formules du premier ordre basées sur le prédicat de joignabilité où R est un système de réécriture conditionnel pseudo-régulier. Ensuite on étend ce résultat au second ordre, les variables du second ordre étant interprétées comme des relations. A partir d'un algorithme général original décidant de la satisfiabilité de formules du second ordre sous certaines conditions, nous représentons une instance des variables du second ordre en système de réécriture conditionnel. On montre que ce travail peut permettre la synthèse automatique de programme. Dans un dernier temps, nous utilisons des sur-approximations pour des tests d'inconsistances. A cet effet, nous utilisons une classe de programmes logiques non réguliers dont le test du vide est décidable pour effectuer la sur-approximation. Nous appliquons finalement cette méthode à la vérification de protocoles cryptographiques. | ||
| 650 | |a Langages de programmation logique | ||
| 650 | |a Réécriture, Systèmes de (informatique) | ||
| 650 | |a Thèses et écrits académiques | ||
| 700 | 1 | |a Réty, Pierre, |d 19..- |4 ths | |
| 700 | 1 | |a Limet, Sébastien, |d 19..-...., |c professeur en informatique. |4 ths | |
| 710 | 2 | |a Université d'Orléans. |4 dgg | |
| 776 | 0 | |0 226595161 |t Utilisation des langages d'arbres pour la modélisation et la vérification des systèmes à états infinis |f par Pierre Pillot |d 2010 |c Villeurbanne |n [CCSD] | |
| 787 | 0 | 8 | |i Reproduced as: |0 247045616 |t Utilisation des langages d'arbres pour la modélisation et la vérification des systèmes à états infinis |f par Pierre Pillot |d 2007 |c Lille |n Atelier national de reproduction des thèses |p Microfiches |s Lille-thèses |
| 997 | |0 255560 |1 Thèse et Mémoire papier |a Ressource papier |c 0/Orléans/ |c 1/Orléans/BU Sciences, Technologies, STAPS/ |z Orléans, BU Sciences, Technologies, STAPS, TS 19-2007-50 |z Orléans, BU Sciences, Technologies, STAPS, TS 19-2007-50 b | ||