License
when quoting this document, please refer to the following
URN: urn:nbn:de:0030-drops-7297
URL: http://drops.dagstuhl.de/opus/volltexte/2006/729/
Leroux, Jérôme ; Sutre, Grégoire

Flat counter automata almost everywhere!

pdf-format:
Dokument 1.pdf (201 KB)

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

DROPS-Home | Fulltext Search | Imprint Published by LZI