2026-07-23T19:59:25Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:729 2024-03-06T11:06:43Z ddc:004 open_access

Flat counter automata almost everywhere! Leroux, Jérôme Sutre, Grégoire Symbolic representation Infinite state system Acceleration Meta-transition 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). Schloss Dagstuhl – Leibniz-Zentrum für Informatik Jérôme Leroux and Grégoire Sutre 2006 Is Part Of Dagstuhl Seminar Proceedings, Volume 6081, Software Verification: Infinite-State Model Checking and Static Program Analysis (2006) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/DagSemProc.06081.4 urn:nbn:de:0030-drops-7297 https://drops.dagstuhl.de/entities/document/10.4230/DagSemProc.06081.4 eng https://creativecommons.org/licenses/by/4.0/legalcode