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

Coordinateur : Jérôme Leroux, Laboratoire Bordelais de Recherche en Informatique

Partenaire : Sylvain Salvati, Université de Lille, Inria CRIStAL

Équipe : Links du Groupe Thématique : SISE

Dates : 2017 - 2020

Résumé :

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 KLML 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ées. 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és 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’algorithme KLM pouvait être compris comme 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 élémentaire : Borner par dessus ou par dessous le temps d’execution d’un algorithme —comme KLM— qui repose sur un beau pré-ordre est un problème difficile qui est rarement considéré dans le domaine de 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.

abstract :

Vector additions systems, aka VASSes, have been investigated intensely since the 1960s, often under the form of Petri nets. Their reachability problems have been shown decidable in the early 1980s, opening the way to decide many problems. However, the decidability proof and the associated KLM algorithm (for "Kosaraju-Lambert-Mayr") is very complex, hard to adapt or extend. It is still being developed but does not yet provide an implementable paradigm. VASS reachability is EXPSPACE-hard, and this is all we know about it. Determining the complexity of that problem is the main unsolved question in the area.

Several VASS extensions exist and raise very challenging problems :

• for deciding data logics, Figueira et al. introduced an extension of VASSes where a clever mechanism enhances counter capabilities. Unordered data nets is another model that has been introduced for data-enriched logics. It is not known whether its reachability problems are decidable.

• More classically, questions on distributed algorithms or recursive programs have led to the introduction of pushdown VASes, a model whose reachability problem is still open after several decades.

• Branching VASes, aka BVASes, are VASSes extended with a weak form of alternation. BVASes have been introduced independently to to attack problems in security protocols, in the context of logics in data tree, and in linear logic and lambda-calculi but it turned out that equivalent models had been developed in the ’90s in computational linguistics. The decidability status of reachability in BVASes is still open.

Recently, Leroux and Schmitz showed that the KLM algorithm can be understood as computing a finite representation for the downward closure of the set of executions of a VASS from source to target, using a suitable ordering on the set of executions. This approach paves a way to adapt the KLM decomposition to various extended models or problems.

Nonelementary complexity : Bounding, from above or below, the running time of algorithms that —like KLM— rely on well-quasi-orderings is a difficult problem that is rarely tackled in the field of automata-theoretic verification. In recent years, Figueira, Schmitz, and Schnoebelen have developed new tools for bounding the length of bad sequences in well-quasi-orderings. These techniques are currently demonstrating their relevance in a flurry of applications.