Verifying Parameterized Networks Specified by Vertex-Replacement Graph Grammars

TL;DR

This paper tackles the parametric reachability problem for networks described by vertex-replacement graph grammars, where nodes run finite-state processes that communicate synchronously. The authors introduce a constructive reduction that encodes VR-described networks as HR-described ones by expanding VR graphs with $oldsymbol{ ext{epsilon}}$-edges into sparse HR graphs, ensuring that reachability properties expressed via first-order arithmetic are preserved. They prove that there exists an effective HR grammar $oldsymbol{ ext{Gamma}}'$ such that $PRP_{oldsymbol{ ext{P}}}(oldsymbol{ extGamma},oldsymbol{ extalpha},oldsymbol{ extsf{L}})$ iff $PRP_{oldsymbol{ ext{P}}^{ ext{H}}}(oldsymbol{ ext{Gamma}}',oldsymbol{ extalpha},oldsymbol{ extsf{L}}^{ ext{H}})$, enabling the application of HR-based parametric verification techniques to VR-specified dense architectures. The reduction uses routing nodes and an expansion-based encoding to guarantee a one-to-one correspondence between VR and HR behaviors with respect to the targeted reachability formulas. The work thus provides a pathway to leverage HR verification tools for VR-described networks, with planned future work on implementation, experimentation on Azure-like topologies, and extending decidability results for pebble-passing HR systems to VR grammars.

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.

Figures (3)

• Figure 1: Azure Datacenter Switching Topology
• Figure 2: The complete bipartite graph $\overrightarrow{K}_{4,3}$ (a) and one possible encoding using $\epsilon$-edges (b).
• Figure 3: VR operations (a) HR operations (b). Ports are depicted as shallow circles; port labels are natural numbers.