Evènement pour le groupe Modélisation et Verification


Date 2009-12-10  11:00-12:15
TitreLes 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). 
LieuSalle 076, LaBRI, Rez-de-chaussée 
OrateurStéphane Demri 
Emaildemri@lsv.ens-cachan.fr 
UrlLSV, ENS-Cachan 



Aucun document lié à cet événement.

Retour
Retour à l'index