Agence Nationale de la Recherche

ReacHard is a research project funded by the French national research agency (ANR) non-thematic program and supported by the Systematic cluster, starting in September 2011. It gathers researchers from two French laboratories, the LaBRI and the LSV, on the subject of reachability problems in counter systems.

Objectives of the Project

The ReacHard project considers some fundamental algorithmic questions in the automatic verification of counter systems, a simple class of infinite-state computational models that play a prominent role in many areas of computer science.

The main question we tackle is the reachability problem for VASS, or equivalently Petri Nets.

This problem is central and its decidability, first proved in 1982 (Mayr, 1981; Kosaraju, 1982; Lambert, 1992), has been widely used in several fields ranging from automated deduction to communication protocols, from artificial intelligence to programming language semantics or distributed algorithms.

However, it is fair to say that the reachability problem for VASS has been solved in an incomplete and unsatisfactory way. The decision algorithm for VASS reachability has never been implemented! This is because it is very complex both conceptually and computationally. As a consequence, the ideas underlying it did not spawn a rich and lively research field.

Three Recent Breakthroughs

ReacHard's research program is essentially based on three recent breakthroughs that open new avenues for the algorithmic verification of counter systems:

  1. A new approach to the reachability problem for Petri nets;
  2. Complexity-theory for well-structured systems;
  3. Extending the scope of Rackoff's EXPSPACE technique.