In: Doron A. Peled, Yih-Kuen Tsay (Eds.): Lecture Notes in Computer Science, 3707: Automated Technology for Verification and Analysis: Third International Symposium, ATVA 2005, Taipei, Taiwan, October 4-7, 2005, pages 489-503. Springer-Verlag, October 2005. URL: http://www.springerlink.com/openurl.asp?genre=article&id=doi:10.1007/1156294836,.
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 uniform accelerated symbolic procedure (whereas previous algorithms were specifically designed for each subclass).