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

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 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.