REACHARD

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.