%0 Conference Proceedings
%F leroux05c
%A Leroux, J.
%A Sutre, G.
%T Flat counter automata almost everywhere!
%B 3rd Int. Symp. on Automated Technology for Verification and Analysis (ATVA'05)
%E Springer, 
%V 	 3707
%P 489-503
%S LNCS
%C Taipei, Taiwan
%X 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)
%U http://www.irisa.fr/vertecs/Publis/Ps/2005-ATVAb.pdf
%U http://dx.doi.org/10.1007/11562948_36
%8 October
%D 2005