TOP
Search the Dagstuhl Website
Looking for information on the websites of the individual seminars? - Then please:
Not found what you are looking for? - Some of our services have separate websites, each with its own search option. Please check the following list:
Schloss Dagstuhl - LZI - Logo
Schloss Dagstuhl Services
Seminars
Within this website:
External resources:
  • DOOR (for registering your stay at Dagstuhl)
  • DOSA (for proposing future Dagstuhl Seminars or Dagstuhl Perspectives Workshops)
Publishing
Within this website:
External resources:
dblp
Within this website:
External resources:
  • the dblp Computer Science Bibliography


Dagstuhl Seminar 14141

Reachability Problems for Infinite-State Systems

( Mar 30 – Apr 04, 2014 )

(Click in the middle of the image to enlarge)

Permalink
Please use the following short url to reference this page: https://www.dagstuhl.de/14141

Organizers

Contact


Schedule

Motivation

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

Verification of innite-state systems can be illustrated by considering the case of counter systems, i.e., computational models combining 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 are Turing powerful, and so all verification problems are undecidable. However, 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 was shown decidable in 1982, and this can be leveraged into many more positive results. Moreover, researchers developed techniques that, while necessarily incomplete, allow to analyze 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 and at counter automata are effectively definable in Presburger arithmetic (assuming some additional conditions).

The seminar will address, among other, the following questions:

  • 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

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.
Copyright Javier Esparza, Alain Finkel, Pierre McKenzie, and Joel Ouaknine

Participants
  • Mohamed-Faouzi Atig (Uppsala University, SE) [dblp]
  • Parosh Aziz Abdulla (Uppsala University, SE) [dblp]
  • Amir M. Ben-Amram (Academic College of Tel Aviv, IL) [dblp]
  • Michael Blondin (ENS - Cachan, FR) [dblp]
  • Bernard Boigelot (University of Liège, BE) [dblp]
  • Mikolaj Bojanczyk (University of Warsaw, PL) [dblp]
  • Rémi Bonnet (ENS - Cachan, FR) [dblp]
  • Ahmed Bouajjani (University of Paris VII, FR) [dblp]
  • Olivier Bournez (Ecole Polytechnique - Palaiseau, FR) [dblp]
  • Tomáš Brázdil (Masaryk University - Brno, CZ) [dblp]
  • Véronique Bruyère (University of Mons, BE) [dblp]
  • Michaël Cadilhac (University of Montréal, CA) [dblp]
  • Giorgio Delzanno (University of Genova, IT) [dblp]
  • Laurent Doyen (ENS - Cachan, FR) [dblp]
  • Diego Figueira (University of Edinburgh, GB) [dblp]
  • Alain Finkel (ENS - Cachan, FR) [dblp]
  • Pierre Ganty (IMDEA Software - Madrid, ES) [dblp]
  • Stefan Göller (Universität Bremen, DE) [dblp]
  • Jean Goubault-Larrecq (ENS - Cachan, FR) [dblp]
  • Christoph Haase (ENS - Cachan, FR) [dblp]
  • Peter Habermehl (University of Paris VII, FR) [dblp]
  • Radu Iosif (VERIMAG - Grenoble, FR) [dblp]
  • Petr Jancar (TU - Ostrava, CZ) [dblp]
  • Stefan Kiefer (University of Oxford, GB) [dblp]
  • Barbara König (Universität Duisburg-Essen, DE) [dblp]
  • Antonin Kucera (Masaryk University - Brno, CZ) [dblp]
  • Slawomir Lasota (University of Warsaw, PL) [dblp]
  • Ranko Lazic (University of Warwick - Coventry, GB) [dblp]
  • Jérôme Leroux (University of Bordeaux, FR) [dblp]
  • Richard Mayr (University of Edinburgh, GB) [dblp]
  • Pierre McKenzie (University of Montréal, CA) [dblp]
  • Roland Meyer (TU Kaiserslautern, DE) [dblp]
  • Joel Ouaknine (University of Oxford, GB) [dblp]
  • Andreas Podelski (Universität Freiburg, DE) [dblp]
  • Igor Potapov (University of Liverpool, GB) [dblp]
  • Fernando Rosa-Velardo (University Complutense - Madrid, ES) [dblp]
  • Sylvain Schmitz (ENS - Cachan, FR) [dblp]
  • Philippe Schnoebelen (ENS - Cachan, FR) [dblp]
  • Luc Segoufin (ENS - Cachan, FR) [dblp]
  • Jeffrey O. Shallit (University of Waterloo, CA) [dblp]
  • Grégoire Sutre (University of Bordeaux, FR) [dblp]
  • Wolfgang Thomas (RWTH Aachen, DE) [dblp]
  • Igor Walukiewicz (University of Bordeaux, FR) [dblp]
  • James Worrell (University of Oxford, GB) [dblp]

Related Seminars
  • Dagstuhl Seminar 00141: Verification of Infinite-state Systems (2000-04-02 - 2000-04-07) (Details)

Classification
  • semantics / formal methods
  • verification / logic

Keywords
  • reachability problems
  • verification
  • infinite-state systems