Counting Abstraction for the Verification of Structured Parameterized Networks
Abstract
We consider the verification of parameterized networks of replicated processes whose architecture is described by hyperedge-replacement graph grammars. 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 over-approximate the behaviors of the original system. The counting abstraction is implemented in a prototype tool, evalutated 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.
Cite
@article{arxiv.2502.15391,
title = {Counting Abstraction for the Verification of Structured Parameterized Networks},
author = {Marius Bozga and Radu Iosif and Arnaud Sangnier and Neven Villani},
journal= {arXiv preprint arXiv:2502.15391},
year = {2025}
}