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:DSP:2006:729,
author = {J{\'e}r{\^o}me Leroux and Gr{\'e}goire Sutre},
title = {Flat counter automata almost everywhere!},
booktitle = {Software Verification: Infinite-State Model Checking and Static Program Analysis},
year = {2006},
editor = {Parosh Aziz Abdulla and Ahmed Bouajjani and Markus M{\"u}ller-Olm },
number = {06081},
series = {Dagstuhl Seminar Proceedings},
ISSN = {1862-4405},
publisher = {Internationales Begegnungs- und Forschungszentrum f{\"u}r Informatik (IBFI), Schloss Dagstuhl, Germany},
address = {Dagstuhl, Germany},
URL = {http://drops.dagstuhl.de/opus/volltexte/2006/729},
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
