Taming Hard Reachability Problems for Counter Systems – REACHARD

We used tools algebraic, geometry, logic and complexity to solve accessibility problems. For example, the sets definable in some logics are also seen as satisfactory systems of equations, and associated with vector spaces. The complexity of these structures is also studied. This has allowed us to characterize the complexity of the most common well quasi orderings.

Our research has proposed new reachability algorithms for counters machines and clarified the complexities; they will therefore facilitate verification counters machines associated with protocols and programs such as the TTP protocol that ensures consistency of braking on all four wheels of a car. New international partnerships have seen the day: a collaboration with researchers of the Chair DIGITEO and another with Professor Ranko Lazic from the University of Warwick.

Give an example: Leroux has responded positively to the conjecture stated in task 4.1. It shows that the acceleration techniques are complete for computing the set of reachable states of a semilinear VAS.

The list of other results in the report is complete and too long to be copied here.

In addition to the academic use of the results already shown in this report (publications, conferences, schools, collaborations, ...), the last two theoretical results deserve to be detailed: early January 2015, two members of the project ReacHard found the first upper bound for the complexity to the problem of accessibility in the VASS and two other members of the project ReacHard found the exact complexity of accessibility for 2-dimension VASS. Both problems have been open for over 30 years. These results have motivated us to start (early January 2015), with partners from the Chair DIGITEO (University of Montréal, Canada), the construction of a prototype to check the accessibility in VASS of any dimension.

Give an example among others: we tackle now the detection of semilinearity. This characterization should allow build algorithms to decide the general problem of reachabiliity for non-semilinear VAS. We will work on the complexity of deciding the context-freeness issue of a VAS.

The list of other prospects in the report is complete and too long to be copied here.

We produced 11 papers in international journals and 32 papers in international conferences. The list is in the full report and too long to be copied here.

Context:

Since its invention in the early 1980s, model-checking is a well-known
approach to the automatic verification of computing systems, be they
digital circuits, communication protocols, algorithms. It applies at all
stages, from early high-level behavioral specifications, to actually
deployed software. In the last 30 years, model-checking has been
continuously adapted to new kinds of systems, and its main limitation,
namely the state-explosion problem, has been consistently fought and
circumvented by inventing new modelization approaches and abstraction
methods, new ad-hoc algorithms for special cases, new data structures
for improved efficiency. Verification of infinite-state systems is best illustrated by
considering the case of counter systems. These counter systems are central when
modeling distributed protocols, programs with recursive parallel threads, programs with
pointers, broadcast protocols, databases, etc. When it
comes to model-checking counter systems and their variants, the main
results are that verification is undecidable when zero-tests are
allowed, while several problems can be decided when zero-tests are forbidden---one speaks of
VASS, for "vector addition systems", or equivalently "Petri
nets". In the case of VASS, reachability was shown decidable in 1982 and
the reachability problem for VASS and related decidable
problems on subclasses of counter systems are pivot problems not only
for the verification of infinite-state systems but also for problems
appearing in very active research areas related to various logics and
automata for data words/trees. Hence, the design of efficient
algorithms for the reachability problem for VASS may have a great
impact, not only in the realm of formal verification. It is however a
very difficult problem. Therefore, improving the computational cost for solving the
reachability problem for Petri nets would also improve the complexity
of the formal verification of numerous classes of infinite-state
systems.

Main objectives:

Strikingly, the decision algorithm for VASS reachability has never
been implemented. This is because of its high complexity, both
conceptual (the algorithm is very hard to understand and to describe)
and computational (it is assumed that the complexity of the algorithm
is not primitive-recursive). In fact, it is fair to say that the
problem is not solved satisfactorily.
The main objective of the project is to propose a satisfactory
solution to the reachability problem for vector addition systems,
that will provide significant improvements both conceptually and
computationally. Recent breakthroughs on the problem and on related
problems for variant models, some of them realized by the participants
of the project, will also allow us to propose solutions
for several extensions, including for instance VASS with one zero-test
or branching VASS. Furthermore, our goal is to take advantage of the
new proof techniques involving semilinear separators in order to
design algorithms that are amenable for implementation. Thanks to the
expertise of the different partners and participants from LaBRI and
LSV, we propose to develop original techniques in order to
understand the mathematical structure of reachability sets,
to perform a computational analysis for reachability problems on
VASS and to design new algorithms. All the participants are also
currently writing a joint book on counter systems, which will
present an up-to-date view of the techniques to solve reachability
problems for counter systems, with a special emphasis on problems
for vector addition systems with states.
This book will be a major deliverable of the project.