Leroux, Jérôme ;
Sutre, Grégoire
Flat counter automata almost everywhere!
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 emph{uniform}
accelerated symbolic procedure (whereas previous algorithms were
specifically designed for each subclass).
BibTeX - Entry
@InProceedings{leroux_et_al:DagSemProc.06081.4,
author = {Leroux, J\'{e}r\^{o}me and Sutre, Gr\'{e}goire},
title = {{Flat counter automata almost everywhere!}},
booktitle = {Software Verification: Infinite-State Model Checking and Static Program Analysis},
pages = {1--19},
series = {Dagstuhl Seminar Proceedings (DagSemProc)},
ISSN = {1862-4405},
year = {2006},
volume = {6081},
editor = {Parosh Aziz Abdulla and Ahmed Bouajjani and Markus M\"{u}ller-Olm},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/opus/volltexte/2006/729},
URN = {urn:nbn:de:0030-drops-7297},
doi = {10.4230/DagSemProc.06081.4},
annote = {Keywords: Symbolic representation, Infinite state system, Acceleration, Meta-transition}
}
|
Keywords: |
|
Symbolic representation, Infinite state system, Acceleration, Meta-transition |
|
Seminar: |
|
06081 - Software Verification: Infinite-State Model Checking and Static Program Analysis
|
|
Issue date: |
|
2006 |
|
Date of publication: |
|
09.11.2006 |
09.11.2006
