Counting Abstraction for the Verification of Structured Parameterized Networks
Marius Bozga, Radu Iosif, Arnaud Sangnier, Neven Villani
TL;DR
This work addresses the challenge of verifying parameterised networks whose architectures are specified by hyperedge-replacement graph grammars. It introduces a counting abstraction that folds an infinite family of networks into a finite set of Petri nets, enabling over-approximate yet sound analysis of reachability and, in particular, coverability. It also identifies a decidable fragment, pebble-passing systems, and establishes complexity bounds of $\$2\mathrm{EXPTIME}$ upper and $\mathrm{PSPACE}$-hard lower for the associated coverability problem. The authors implement a prototype tool (ParCoSys) and demonstrate its effectiveness across diverse architectures (rings, stars, trees, leader election) using LoLA as back-end, highlighting practical applicability to architecture-driven verification. Overall, the paper advances scalable, architecture-aware parameterized verification by combining a finitary abstraction with a nontrivial decidable fragment and tangible tooling support.
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.