Grande Salle de VERIMAG
29 octobre 2009 - 14h00
Les problèmes de couverture et finitude pour les systèmes d'addition de vecteurs arborescents.
par Stephane Demri de ENS CACHAN
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.
This is a joint work with Marcin Jurdzinski, Oded Lachish and Ranko Lazic (University of Warwick, UK).
