leroux05c

J. Leroux, G. Sutre. Flat counter automata almost everywhere!. In 3rd Int. Symp. on Automated Technology for Verification and Analysis (ATVA'05), Springer (ed.), LNCS, Volume 3707, Pages 489-503, Taipei, Taiwan, October 2005.

Download [help]

Download paper: Doi page

Download paper: Adobe portable document (pdf)

Copyright notice: This material is presented to ensure timely dissemination of scholarly and technical work. Copyright and all rights therein are retained by authors or by other copyright holders. All persons copying this information are expected to adhere to the terms and constraints invoked by each author's copyright. These works may not be reposted without the explicit permission of the copyright holder.
This page is automatically generated by bib2html v216, © INRIA 2002-2007, Projet Lagadic

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)

BibTex Reference

@InProceedings{leroux05c,
   Author = {Leroux, J. and Sutre, G.},
   Title = {Flat counter automata almost everywhere!},
   BookTitle = {3rd Int. Symp. on Automated Technology for Verification and Analysis (ATVA'05)},
   editor = {Springer, },
   Volume = {    3707},
   Pages = {489--503},
   Series = {LNCS},
   Address = {Taipei, Taiwan},
   Month = {October},
   Year = {2005}
}

EndNote Reference [help]

Get EndNote Reference (.ref)