Flat counter automata almost everywhere!

Abstract

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).