IDEAL-BASED ALGORITHMS FOR VASSES AND WELL-STRUCTURED SYSTEMS – BRAVAS

Les systèmes d'addition de vecteurs, aussi appelés VASSs, ont été intensivement étudiés depuis les années 60, souvent sous la forme de réseaux de Petri. Le problème d'accessibilité pour ces systèmes fut montré décidable au début des années 80, ouvrant la voie permettant de décider algorithmiquement de nombreux problèmes. Cependant, la preuve de décidabilité et l'algorithme KLM associé (pour "Kosaraju-Lambert-Mayr'') est très complexe, difficile à adapter ou à étendre. Il y a toujours des travaux sur ce problème mais ils ne permettent toujours pas d'avoir une implémentation de l'algorithme. Le problème de l'accessibilité des VASS est EXPSPACE-dur, et c'est tout ce que l'on sait. Trouver la complexité de ce problème est la principale question dans ce domaine.

De nombreuses extensions de VASSs existent et mènent à des défis très importants:

* Pour décider des logiques avec données, Figueira et d'autres ont introduit une extension des VASSs possédant un mécanisme ingénieux améliorant la capacité des compteurs. Les réseaux de Petri avec données est un autre modèle qui a été introduit pour des logiques sur les donnés. Nous ne savons pas si le problème de l'accessibilité est décidable pour cette classe.

* Plus classiquement, des questions sur l'algorithmique distribuée ou les programmes récursifs ont menés à l'introduction du modèle des VASs avec pile, un modèle dont le problème de l'accessibilité est ouvert depuis plusieurs décennies.

* Les VASs branchants, aussi appelé BVAS, sont des VASSs étendus avec une forme faible d'alternance. Les BVASs ont été introduits indépendamment pour attaquer des problèmes en sécurité de protocoles, dans le contexte de logiques sur des arbres avec données, en logique linéaire, et en lambda-calcul mais tous ces modèles sont en fait équivalent à des modèles qui ont été développé dans les années 90 en logique computationnelle. Le status décidable de l'accessibilité pour les BVASs est toujours ouvert.

Récemment, Leroux et Schmitz ont montré que l'algorithm KLM pouvait être compris come un calcul d'une représentation finie de la cloture par le bas de l'ensemble des executions d'un VASS d'une source à une destination en utilisant un ordre bien choisi sur les executions. Cette nouvelle approche trace le chemin pour adapter la décomposition KLM à de nombreuses extensions et problèmes.

Complexité non élementaire: Borner par dessus ou par dessous le temps d'execution d'un l'algorithme -- comme KLM -- qui repose sur un beau pré-ordre est un problème difficile qui est rarement considéré dans le domaine le vérification formelle à base d'automates. Ces dernières années, Figueira, Schmitz, et Schnoebelen ont développé de nouveaux outils pour borner la longueur des mauvaises séquences pour un beau pré-ordre. Ces techniques se montrent actuellement très utiles dans une grande variété d'applications.