|
Evènement pour le groupe Modélisation et Verification
Date | 2009-12-10 11:00-12:15 |
Titre | Les problèmes de couverture et finitude pour les systèmes d'addition de vecteurs arborescents. |
Résumé | Les systèmes d'addition de vecteurs arborescents (BVAS) forment un modèle
formel de calcul qui est
utilisé par exemple en linguistique ou pour la vérification de protocoles
cryptographiques. Ce modèle a
aussi des liens étroits avec des logiques de données interprétées sur des
arbres avec valeurs mais aussi
avec la logique linéaire MELL. La décidabilité du problème d'accessibilité
pour ces systèmes demeure
encore aujourd'hui ouverte, et ce problème est équivalent à divers
problèmes essentiels des domaines
cités plus haut.
Récemment, Verma et Goubault-Larrecq ont réussi à montrer que les
problèmes de finitude et de
couverture pour les BVAS sont décidables.
Dans cet exposé, je vais présenter comment caractériser la complexité des
problèmes de couverture
et de finitude pour les BVAS. Une partie de la preuve consiste à raffiner
les travaux de Rackoff dans le
cas linéaire correspondant au modèle des réseaux de Petri.
Ce travail a été mené conjointement avec Marcin Jurdzinski, Oded Lachish
et Ranko Lazic
(University of Warwick, UK). |
Lieu | Salle 076, LaBRI, Rez-de-chaussée |
Orateur | Stéphane Demri |
Email | demri@lsv.ens-cachan.fr |
Url | LSV, ENS-Cachan |
Aucun document lié à cet événement. RetourRetour à l'index
| |