Verifying Parameterized Networks Specified by Vertex-Replacement Graph Grammars

TL;DR

This paper presents a reduction method transforming parameterized reachability problems from vertex-replacement graph grammars to hyperedge-replacement grammars, enabling the use of existing verification techniques for dense network architectures.

Contribution

It introduces a novel reduction from VR to HR grammars for parametric verification, broadening applicability to dense network structures.

Findings

Effective reduction from VR to HR grammars for PRP

Enables verification of dense network architectures

Facilitates applying HR-based verification techniques

Abstract

We consider the parametric reachability problem (PRP) for families of networks described by vertex-replacement (VR) graph grammars, where network nodes run replicas of finite-state processes that communicate via binary handshaking. We show that the PRP problem for VR grammars can be effectively reduced to the PRP problem for hyperedge-replacement (HR) grammars at the cost of introducing extra edges for routing messages. This transformation is motivated by the existence of several parametric verification techniques for families of networks specified by HR grammars, or similar inductive formalisms. Our reduction enables applying the verification techniques for HR systems to systems with dense architectures, such as user-specified cliques and multi-partite graphs.