Flat counter automata almost everywhere!

Authors Jérôme Leroux, Grégoire Sutre

Thumbnail PDF


  • Filesize: 200 kB
  • 19 pages

Document Identifiers

Author Details

Jérôme Leroux
Grégoire Sutre

Cite AsGet BibTex

Jérôme Leroux and Grégoire Sutre. Flat counter automata almost everywhere!. In Software Verification: Infinite-State Model Checking and Static Program Analysis. Dagstuhl Seminar Proceedings, Volume 6081, pp. 1-19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2006)


This paper argues that flatness appears as a central notion in the verification of counter automata. A counter automaton is called flat when its control graph can be ``replaced'', equivalently w.r.t. reachability, by another one with no nested loops. From a practical view point, we show that flatness is a necessary and sufficient condition for termination of accelerated symbolic model checking, a generic semi-algorithmic technique implemented in successful tools like FAST, LASH or TReX. From a theoretical view point, we prove that many known semilinear subclasses of counter automata are flat: reversal bounded counter machines, lossy vector addition systems with states, reversible Petri nets, persistent and conflict-free Petri nets, etc. Hence, for these subclasses, the semilinear reachability set can be computed using a emph{uniform} accelerated symbolic procedure (whereas previous algorithms were specifically designed for each subclass).
  • Symbolic representation
  • Infinite state system
  • Acceleration
  • Meta-transition


  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    PDF Downloads