The goal of the BraVAS project is to develop a new and powerful approach to decide the reachability problems for VAS extensions and to analyse their complexity. The ambition here is to crack with a single hammer several long-lasting open problems that have all been identified as a barrier in different areas, but that are in fact closely related when seen as reachability.
Our main insight for attacking these difficult problems comes from a new perception of the KLM algorithm that can be interpreted as a counter-example guided abstract refinement algorithm (CEGAR). Jérôme Leroux and Sylvain Schmitz, the two authors of this milestone are partners of the BraVAS project. This presentation of the KLM algorithm agrees with the original construction, but it brings new key insights that are not apparent in the original one: the role of the completed spaces of well-quasi-ordered sets (wqo), and the use of an extension of the coverability algorithm to analyse the feasibility of a downward-closed set of execution, the so-called adherence property. Future investigations on the KLM algorithm will certainly take advantage of the powerful toolset recently developed for wqo-based techniques. This view also paves the way to generalisations to BVASes and other extensions. The ambition here is to crack with a single hammer several long-lasting open problems that have all been identified as a barrier in different areas, but that are in fact closely related when seen as reachability. As in any fundamental research, the main risk is that of not being able to reach the goal, viz., establishing the desired decidability and complexity results. However, recent work by the proponents shows that we are on the right track, and intermediate milestones may prove to be interesting in their own right. Moreover, the level of risk is reduced since the project is considering many different counter models.
The project is organized in an initial task followed by three main tasks.
A new understanding of the KLM algorithm: At its inception, the BraVAS project is based on a new understanding on the KLM algorithm. An important goal is to identify a logical language that captures the kind of properties needed to express adherence properties, so that we have a clear and abstract problem for which decidability and complexity must be investigated for all considered VASS extensions. This effort will be led by the main experts with whom the idea originated (Leroux \& Schmitz) and will profit from interaction with the other partners who can bring expertise on specific aspects like the algorithmic issues related to wqo, or the Fast-Growing complexity classes.
Handling downward-closed sets: This task is devoted to the development of data structures and algorithms for handling downward-closed subsets of a wqo via the canonical ideal decomposition. This is a generic technique that supports polynomial-time set-theoretical operations. This representation is already well understood for words over a finite alphabet or vectors from vectors of natural numbers but this task aims at developing it for more varied wqos. For example, the previous task needs to represent sets of executions. The ideal-based representation needs to be developed for trees for BVASes, but also for simpler wqos like sequences of sequences for executions of nets with linearly-ordered data tokens, or with unordered data tokens.
Accelerations and coverability sets for VASS extensions: In this task, we will develop a Karp and Miller approach for VASS extensions. The original Karp and Miller algorithm is known to be extremely useful for deciding various problems on VASSes. Basically, it computes the downward closure of non-decreasing sequences of reachable configurations thanks to the precise computation of the transitive closure of sequences of actions, called acceleration. The two main challenges to extend the Karp and Miller approach are (1) developing acceleration techniques, and (2) showing that they are complete for the effective computation of the downward-closure of reachability sets.
Complexity Analysis: This task will develop the tools originally proposed by Schmitz et al. for the complexity analysis of wqo-based algorithms. These tools have proved well-suited for proving tight upper bounds via length-function theorems, and for proving matching lower-bounds via robust encodings in standard complexity classes. However the project BraVAS will need specific developments that fit more closely the form of the KLM algorithm, and variants developed for VASS extensions.
Solving the reachability problem for VASS extensions like unordered data Petri nets (UDPN), pushdown VASes (PVAS) and branching VASes (BVAS), will have major and long-lasting impact on many areas where these and related models are central. This encompasses several areas in logic (linear logics, denotational semantics, ..), in computer-aided verification (in particular with models for concurrent programs), in database theory, in computational linguistics, etc. In all these areas, the above open problems, conjectured to be decidable, are stumbling blocks that have been arrived at in several independent ways.
If the aforementioned open problems are not solved in the course of the project, an important outcome of the project will be the identification of hard bottlenecks, closer to the heart of the problem. These bottlenecks will either inspire more focused questions and new avenues of investigation, or show the way to some undecidability proofs that we cannot envision now. Since undecidability is not expected, such negative results may spur a paradigm shift in some areas.
In addition, it is expected that some subtasks of the project will have their own impact, beyond our focus on VAS extensions.
Verification for VASSes: One clear outcome of our Task A is an improved understanding of the KLM algorithm for VAS reachability. By breaking it down into well-identified components, by using new concepts and data structures for downward-closed sets of runs, by introducing a logical language for handling boundedness and adherence questions, Task A will make it possible to envision an implementation of the KLM algorithm: we note that the KLM algorithm has never been actually implemented simply because of its sheer conceptual complexity.
Computing Downward Closures: Task B and C will provide new algorithms and data structures for ideals of well-quasi orderings and their downward-closed sets. This will have impact beyond our concerns with the KLM algorithm and its generalizations to VAS extensions. We observe that the computability of downward-closures has recently been identified as an important feature, e.g., for logical questions like separability or for decidability in distributed computing problems. It has also long been used for more practical questions like approximations in model-checking.
Fast-growing complexity: The bulk of Task D tackles problems of general interest, not limited to project BraVAS. It develops the FGH (for Fast-Growing) framework for computational problems that have 'non-elementary complexity'. The FGH framework is already put to good use in several groups unrelated to us: they use it to separate, or sometimes relate, models by comparing their computing power. The potential for applications is very large: any problem that is today just described as ``non-elementary'', can be better described withing the FGH framework.