Treffer: Counting Abstraction and Decidability for the Verification of Structured Parameterized Networks

Title:
Counting Abstraction and Decidability for the Verification of Structured Parameterized Networks
Authors:
Bozga, Marius, Iosif, Radu, Sangnier, Arnaud, Villani, Neven
Contributors:
VERIMAG (VERIMAG - IMAG), Centre National de la Recherche Scientifique (CNRS)-Université Grenoble Alpes (UGA)-Institut polytechnique de Grenoble - Grenoble Institute of Technology (Grenoble INP), Université Grenoble Alpes (UGA), Dipartimento di Informatica, Bioingegneria, Robotica e Ingegneria dei Sistemi Genova (DIBRIS), Università degli studi di Genova = University of Genoa (UniGe), ANR-23-CE48-0005,PaVeDyS,Verification paramétrée de systemes distribues dynamiques(2023), ANR-23-CE25-0004,ADAPT,Adaptation dynamique de systèmes à composants hiérarchiques(2023)
Source:
Computer Aided Verification (CAV), Volume 2, Lecture Notes in Computer Science ; Computer Aided Verification ; https://hal.science/hal-05194491 ; Computer Aided Verification, Jul 2025, Zagreb, Croatia. pp.238
Publisher Information:
CCSD
Publication Year:
2025
Subject Terms:
Distributed system architectures, Graph grammar, Petri net coverability problem, Verification, [INFO]Computer Science [cs]
Subject Geographic:
Zagreb, Croatia
Document Type:
Konferenz conference object
Language:
English
Relation:
info:eu-repo/semantics/altIdentifier/arxiv/2502.15391; ARXIV: 2502.15391
Availability:
https://hal.science/hal-05194491
https://hal.science/hal-05194491v1/document
https://hal.science/hal-05194491v1/file/paper.pdf
Rights:
http://creativecommons.org/licenses/by/ ; info:eu-repo/semantics/OpenAccess
Accession Number:
edsbas.38A4B08B
Database:
BASE

Weitere Informationen

International audience ; We consider the verification of parameterized networks of replicated processes whose architecture is described by hyperedge-replacement graph grammars in the style of Courcelle. Due to the undecidability of verification problems such as reachability or coverability of a given configuration, in which we count the number of replicas in each local state, we develop two orthogonal verification techniques. We present a counting abstraction able to produce, from a graph grammar describing a parameterized system, a finite set of Petri nets that overapproximate the behaviors of the original system. The counting abstraction is implemented in a prototype tool, evaluated on a non-trivial set of test cases. Moreover, we identify a decidable fragment, for which the coverability problem is in 2EXPTIME and PSPACE-hard.