Jump to : Download | Abstract | Contact | BibTex reference | EndNote reference |
Download paper Adobe portable document format (pdf)
Copyright noticeThis 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 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).
@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), Volume 3707 of LNCS},
editor = {Springer, },
Pages = {489--503},
Address = {Taipei, Taiwan},
Month = {October},
Year = {2005}
}
Get EndNote Reference (.ref)