2025/02/21 by Bozga, Marius, Iosif, Radu, Sangnier, Arnaud +1 · 1 citation
#FOS: Computer and information sciences #Formal Languages and Automata Theory (cs.FL)
paper · doi:10.48550/arxiv.2502.15391
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.