Counting Abstraction for the Verification of Structured Parameterized Networks

TL;DR

This paper introduces a counting abstraction method for verifying parameterized networks with hyperedge-replacement graph grammars, producing finite Petri net over-approximations and identifying a decidable fragment with specific complexity bounds.

Contribution

It presents a novel counting abstraction technique and a prototype tool for verifying parameterized networks, along with a decidable fragment analysis.

Findings

Counting abstraction produces finite Petri nets over-approximating system behaviors.

Prototype tool successfully applied to non-trivial test cases.

Decidable fragment with coverability in 2EXPTIME and PSPACE-hard complexity.

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.