2022/01/26 by Leroux, Jérôme, Sutre, Grégoire
#Acceleration #Infinite state system #Meta-transition #Symbolic representation
paper · doi:10.4230/dagsemproc.06081.4
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 emphuniform accelerated symbolic procedure (whereas previous algorithms were specifically designed for each subclass).