30. März – 04. April 2014, Dagstuhl-Seminar 14141

Reachability Problems for Infinite-State Systems


Javier Esparza (TU München, DE)
Alain Finkel (ENS – Cachan, FR)
Pierre McKenzie (University of Montréal, CA)
Joel Ouaknine (University of Oxford, GB)

Auskunft zu diesem Dagstuhl-Seminar erteilt

Dagstuhl Service Team


Dagstuhl Report, Volume 4, Issue 3 Dagstuhl Report
Programm des Dagstuhl-Seminars [pdf]


Many standard verification problems can be rephrased as reachability problems, and there exist powerful methods for determining reachability in infinite-state systems. However, applications require not only decidability results, but provably optimal algorithms. The seminar focussed on complexity and algorithmic issues for the verification of infinite-state systems, with special emphasis on reachability problems.

Verification of finite-state systems can be illustrated by considering the case of counter systems, i.e., computational models combining a finite-state control with counters. Counter systems have been used to model distributed protocols, programs with recursive parallel threads, programs with pointers, broadcast protocols, replicated finite-state programs, asynchronous programs, etc. If zero-tests are allowed -- one speaks of "Minsky machines" --, counter systems have the power of Turing machines, and so all their verification problems are undecidable. On the other hand, many problems can be decided when zero-tests are forbidden -- one speaks of VASS, for "vector addition systems with states", or equivalently "Petri nets". In particular, reachability for VASS was shown decidable in 1982, and this can be leveraged into many more positive results. Moreover, researchers developed techniques that, while necessarily incomplete, allow analysing many questions: reversal-bounded analysis à la Ibarra, accelerations à la FAST, or well-structured extensions of VASS, see e.g., the forward analysis procedure. In turn, these techniques have led to many new theoretical results. For instance, it has been shown that the reachability sets of both reversal-bounded counter automata and flat counter automata are effectively definable in Presburger arithmetic (assuming some additional conditions).

The seminar addressed the following topics:

  • Complexity of reachability on various models: parameterized counter systems, lossy channel systems, lossy counter systems, at counter systems, reversal-bounded counter systems, and other.
  • Decidability and complexity of reachability problems for Petri nets extensions: timed Petri nets, Petri nets with one zero-test, with one unbounded counter, linear dynamical systems, BVASS, data nets, and other.
  • Recent development and uses of the theory of well-structured transition systems.
  • Decidability and complexity of reachability for systems with multiple (constraints) stacks: multiphase, reversal-bounded, and other.
  • Games on infinite-state systems: counter automata, timed systems, weighted automata. Games with energy constraints.
  • Monadic logics with costs.
  • New developments in the algorithmics of Presburger logics; SMT-solvers.
Summary text license
  Creative Commons BY 3.0 Unported license
  Javier Esparza, Alain Finkel, Pierre McKenzie, and Joel Ouaknine

Related Dagstuhl-Seminar


  • Semantics / Formal Methods
  • Verification / Logic


  • Reachability problems
  • Verification
  • Infinite-state systems


In der Reihe Dagstuhl Reports werden alle Dagstuhl-Seminare und Dagstuhl-Perspektiven-Workshops dokumentiert. Die Organisatoren stellen zusammen mit dem Collector des Seminars einen Bericht zusammen, der die Beiträge der Autoren zusammenfasst und um eine Zusammenfassung ergänzt.


Download Übersichtsflyer (PDF).

Dagstuhl's Impact

Bitte informieren Sie uns, wenn eine Veröffentlichung ausgehend von Ihrem Seminar entsteht. Derartige Veröffentlichungen werden von uns in der Rubrik Dagstuhl's Impact separat aufgelistet  und im Erdgeschoss der Bibliothek präsentiert.


Es besteht weiterhin die Möglichkeit, eine umfassende Kollektion begutachteter Arbeiten in der Reihe Dagstuhl Follow-Ups zu publizieren.