License: Creative Commons Attribution 4.0 International license (CC BY 4.0)
When quoting this document, please refer to the following
DOI: 10.4230/DagSemProc.06081.4
URN: urn:nbn:de:0030-drops-7297
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2006/729/
Go to the corresponding Portal

Leroux, Jérôme ; Sutre, Grégoire

Flat counter automata almost everywhere!

pdf-format:
06081.LerouxJerome.ExtAbstract.729.pdf (0.2 MB)

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
Collection: 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 | Privacy Published by LZI