<figure><img src="image_1.png" /></figure>

HAL
open science

# Verifying Parameterized Networks Specified by Vertex-Replacement Graph Grammars

Radu Iosif, Arnaud Sangnier, Neven Villani

<figure><img src="image_2.png" /></figure>

## To cite this version:

Radu Iosif, Arnaud Sangnier, Neven Villani. Verifying Parameterized Networks Specified by Vertex-Replacement Graph Grammars. NETYS, May 2025, Rabat, Morocco. hal-05194506

HAL Id: hal-05194506

https://hal.science/hal-05194506v1

Submitted on 31 Jul 2025

HAL is a multi-disciplinary open access
archive for the deposit and dissemination of sci-
entific research documents, whether they are pub-
lished or not. The documents may come from
teaching and research institutions in France or
abroad, or from public or private research centers.

L'archive ouverte pluridisciplinaire HAL, est
destinée au dépôt et à la diffusion de documents
scientifiques de niveau recherche, publiés ou non,
émanant des établissements d'enseignement et de
recherche français ou étrangers, des laboratoires
publics ou privés.

<figure><img src="image_3.png" /></figure>

Distributed under a Creative Commons Attribution 4.0 International License
Verifying Parameterized Networks Specified by
Vertex-Replacement Graph Grammars

Radu Iosif¹, Arnaud Sangnier², and Neven Villani¹

¹ Univ. Grenoble Alpes, CNRS, Grenoble INP, VERIMAG, 38000, France
{firstname}.{lastname}@univ-grenoble-alpes.fr

² DIBRIS, Univ. of Genova, Italy
{firstname}.{lastname}@unige.it

**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.

# 1 Introduction

As pointed out in recent literature, "network verification is a necessary part of deploying modern hyperscale datacenters" [19]. In this context, verification considers global properties of routing control, such as access between point A and point B. Very often, the intended functionality of a network can be derived from its architecture, typically known at early stages of network design.

The huge scale of present-day datacenters, of ~$10^4$ routers for a regional hub and continuously growing, requires parametric verification techniques, that work no matter how many servers in a rack, switches in a cluster, clusters in a layer, etc. Despite decades of theoretical research and an impressive body of results (see [7] for a nice survey), these techniques consider mostly hard-coded architectures, either dense (e.g., cliques [16]) or sparse (e.g., rings [11]) families of graphs with a common topological pattern.

The problem of verifying networks with user-specified architecture has gained re-
cent momentum, with the development of parametric verification techniques for sys-
tems described using logic [5] or graph grammars [20]. In principle, logic-based graph
specification languages are good at describing global properties, such as planarity, k-
colorability or reachability, which make them more suitable for the specification of
correctness properties, than network design.

On the other hand, graph grammars are appealing for their constructive aspect,
i.e., defining how large graphs are built from smaller subgraphs. Moreover, this re-
cursive way of describing sets of graphs is common among programmers and software
engineers, who are familiar with inductively defined datastructures (lists, trees, etc.)
<figure><img src="image_4.png" /><figcaption>**Fig. 1.** Azure Datacenter Switching Topology</figcaption></figure>

used in both imperative and functional programming. Graph grammars are at the core of the theory of formal languages (see [13] for a comprehensive survey). Based on the underlying set of operations (i.e., graph algebra), we distinguish between *vertex-replacement* (VR) and *hyperedge-replacement* (HR) grammars. In principle, HR graph grammars can specify families of graphs having bounded tree-width, such as chains, rings, stars, trees (of unbounded rank) and beyond, e.g., overlaid structures such as trees or stars with certain nodes linked in a list. Since cliques and grids are families of unbounded tree-width, neither can be specified using HR graph grammars. On the other hand, *vertex-replacement* (VR) grammars are strictly more expressive [12]. For instance, VR grammars can describe the sets {$K_n$}$_{n \ge 1}$ of cliques and {$K_{n,m}$}$_{n,m \ge 1}$ of complete bipartite graphs, among others.

A concrete motivation for using VR grammars to design datacenter networks can be found in the informal description of the Azure datacenter architecture [17,19], deployed in the Microsoft hyperscale cloud network (Figure 1). The *top-of-rack* (ToR) switches connect servers hosted in a rack. Several ToR switches are connected together by a number of *leaf* switches. Leaf switches are in turn connected together by a set of *spine* switches, that connect the datacenter to the Azure regional network. These networks cannot be described as cliques, because of their layered structure. However, the links between each layer (i.e., ToR, leaf, spine, regional spine) and its adjacent layers form a complete bipartite graph, thus lying outside the scope of HR grammars, which cannot define complete bipartite graphs of unbounded sizes<fnref n="3" />.

The precise relation between the expressivity of VR and HR grammars has been elegantly coined in a result by Courcelle, stating that a set defined by a VR grammar can also be defined by an HR grammar if and only if it is sparse [12]. Moreover, each VR grammar can be transformed into an HR grammar producing a set of graphs with $\epsilon$-edges, such that the elimination of these edges from the HR language yields the original VR language. For instance, the elimination of $\epsilon$-edges from the graph from Figure 2 (b) yields the complete bipartite graph $K_{4,3}$ from Figure 2 (a).

*Contribution* We leverage the idea of transforming VR grammars into HR grammars modulo elimination of $\epsilon$-edges to define a reduction from the parametric reachability

<footnote n="3">³ Each set {$K_{n,m}$}$_{n \in N, m \in M}$ for $N, M$ infinite subsets of $\mathbb{N}$, has unbounded tree-width, whereas HR-grammars define bounded tree-width sets.</footnote>
<figure><img src="image_5.png" /><figcaption>Fig. 2. The complete bipartite graph $\vec{K}_{4,3}$ (a) and one possible encoding using $\varepsilon$-edges (b).</figcaption></figure>

<figure><img src="image_6.png" /></figure>

problem (PRP) for systems described by VR grammars and finite-state local behaviors, with correctness properties given by unrestricted arithmetic formulae over a set of variables, tracking how many processes are in a given local state, to the PRP problem for systems described by HR grammars, having the same correctness property. This is motivated by several recent developments in the verification of parametric systems with HR-style architecture descriptions. In particular, [10] reports on an inference of structural invariants (i.e., over-approximations of the reachable set, that can be derived from the structure of the network) for architectures described using a variant of Separation Logic with inductive definitions (same expressivity as HR grammars). Moreover, [9] gives an abstraction technique that folds similar network nodes into a finite Petri net, whose coverability problem over-approximates the original parametric coverability problem. In this paper, we give a more general reduction method, that preserves all safety properties specified by arithmetic assertions, rather than the particular case of coverability.

*Related Work* The literature on parametric verification is too large to be recalled here. We point to [7] for a survey on the (un)decidability results, typically concerning clique or ring architectures. The specification of network architectures using inductive definitions can be traced back to the work on *network grammars* [22,20,18], that use inductive rules to describe systems with linear (pipeline, token-ring) architectures. These initial works target mainly safety properties, by inferring network invariants [23,21]. Pipeline and clique architectures are also considered by methods based on the theory of well-structured transition systems [1], such as monotonic abstraction [2,3].

A prominent exception, that considers the verification of clique-width bounded architectures specified using Monadic Second Order Logic (MSO) against $CTL^* \setminus \emptyset$ properties is [5]. Their result uses a reduction from the parametric model checking problem (PMCP) to the decidability of MSO over graphs of bounded clique-width [13]. Our result is orthogonal, because we consider VR grammars that strictly subsume the MSO-definable sets of bounded clique-width. It is, however, an interesting question if our reduction can be used to establish a more general decidability result. A promising lead would be to use the decidability of PMCP for HR systems with local behaviors that mimick the passing of a pebble from one node to another [9].

*Notation* We denote by $\mathbb{Z}$ ($\mathbb{N}$) the set of (positive) integers. For $i, j \in \mathbb{N}$, we denote by $[i, j]$ the set $\{i, \dots, j\}$, considered empty if $i > j$. The cardinality of a finite set $A$ is written $|A|$. A singleton $\{a\}$ is simply denoted $a$. The union of two disjoint sets $A$ and $B$ is denoted as $A \cup B$. The Cartesian product of two sets $A$ and $B$ is denoted $A \times B$. As usual, we define $A^*$ the set of (possibly empty) finite sequences of elements from $A$, and $A^\infty$ the set of finite or infinite sequences over $A$. Finally $\mathcal{P}(A)$ is the powerset of $A$.
## 2 Graphs

For simplicity reasons, in this paper we consider only networks whose topologies are described by oriented binary graphs, where vertices model processes and edges model a symmetric rendezvous between two processes, i.e., we do not distinguish the process initiating the communication and consider that both participants have equal roles.

Let $\Lambda$ and $\Delta$ be finite disjoint alphabets of vertex and edge labels, respectively. A *graph* is a tuple $G = (V_G, E_G, \lambda_G)$, where $V_G$ is a finite set of vertices, $E_G \subseteq V_G \times \Delta \times V_G$ is a set of edges, such that $(v, \delta, v') \in E_G$ implies $v \neq v'$ (i.e., graphs have no self-loops) and $\lambda_G : V_G \to \mathcal{P}(\Lambda)$ assigns a set of labels to each vertex. We do not distinguish graphs that are isomorphic. We denote by $\mathcal{G}(\Lambda, \Delta)$ the set of graphs with vertex and edge labels from $\Lambda$ and $\Delta$, or simply $\mathcal{G}$, if $\Delta$ and $\Lambda$ are understood.

We shall consider parameterized networks described as infinite sets of graphs. Albeit infinite, these sets have a finite description, given by finitely many inductive rules stating how the graphs in the set are built from smaller graphs. This constructive<fnref n="4" /> approach to the specification of infinite sets of graphs relies on graph algebras, being at the core of an impressive body of theoretical work (see [13] for a survey).

### 2.1 Algebras

We present two classical graph algebras, namely *vertex-replacement* (*VR*) and *hyperedge-replacement* (*HR*). Let $\Lambda$ and $\Delta$ be fixed in the following. We consider a set $\Pi \subseteq \Lambda$ of distinguished vertex labels, called *ports*, such that $\|\lambda_G(v) \cap \Pi\| \le 1$, for each graph $G \in \mathcal{G}(\Lambda, \Delta)$ and each vertex $v \in V_G$. In other words, a vertex is labeled with at most one port. We say that a vertex $v \in V_G$ is a $\pi$-port of $G$ whenever $\pi \in \lambda_G(v)$. The *sort* of a graph is the set of ports that occur in the labels of the vertices from the graph.

The labels from $\Lambda \setminus \Pi$ will be needed later to associate vertices with local behaviors, referred to as process types. For the time being, we assume the set of process types to be $\Lambda \setminus \Pi = \{\lambda_1, \dots, \lambda_n\}$ and that the set of port labels is partitioned accordingly, i.e., $\Pi = \Pi_{\lambda_1} \uplus \dots \uplus \Pi_{\lambda_n}$. We say that the *process type* of a port $\pi \in \Pi$ is $\lambda \in \Lambda \setminus \Pi$, denoted $\text{ptype}(\pi) = \lambda \iff_{\text{def}} \pi \in \Pi_{\lambda}$. A partial function $\alpha : \Pi \to \Pi$ is *type-preserving* iff $\alpha(\pi)$, if defined, has the same process type as $\pi$, for each $\pi \in \Pi$.

The domain of the *VR-algebra* is the set $\mathcal{G}$ of graphs. The operations of VR are the following, see Figure 3 (a) for an illustration:

- **Disjoint union:** $G_1 \oplus_{p_1,p_2} G_2 \stackrel{\text{def}}{=} H$ iff the sorts of $G_1$ and $G_2$ are $p_1$ and $p_2$, respectively, $V_H = V_{G_1} \uplus V_{G_2}$, $E_H = E_{G_1} \uplus E_{G_2}$ and $\lambda_H = \lambda_{G_1} \uplus \lambda_{G_2}$ where, if $V_{G_1} \cap V_{G_2} \neq \emptyset$ or $E_{G_1} \cap E_{G_2} \neq \emptyset$, we replace $G_2$ by an isomorphic copy disjoint from $G_1$. We write $\oplus$ instead of $\oplus_{p_1,p_2}$ when the argument sorts are understood.

- **Edge creation:** for an edge label $\delta \in \Delta$ and port labels $\pi_1 \neq \pi_2 \in \Pi$, add$_{\delta,\pi_1,\pi_2} (G) \stackrel{\text{def}}{=} H$ iff $V_H = V_G$, $E_H = E_G \cup \{(v_1, \delta, v_2) | v_1, v_2 \in V_G, \pi_i \in \lambda_G(v_i), i = 1, 2\}$ and $\lambda_H = \lambda_G$; in other words, add$_{\delta,\pi_1,\pi_2}$ adds a directed $\delta$-edge from each $\pi_1$-port to each $\pi_2$-port of its argument. No edge is added if such an edge already exists. Moreover, because $\pi_1$

<footnote n="4">⁴ As opposed to the descriptive method of defining sets of graphs by their common properties, using e.g., monadic second-order logic.</footnote>
<figure><img src="image_7.png" /><figcaption>**Fig. 3.** VR operations (a) HR operations (b). Ports are depicted as shallow circles; port labels are natural numbers.</figcaption></figure>

and $\pi_2$ are different labels and each vertex has at most one port label, no self-loops are introduced by this operation.

- **Port redefinition:** for a type-preserving partial function $\alpha : \Pi \to \Pi$, $\text{relab}_\alpha(\mathcal{G}) \stackrel{\text{def}}{=} H$ iff $V_H = V_G$, $E_H = E_G$ and $\lambda_H(v) = \{\alpha(\pi) \mid \pi \in \lambda_G(v) \cap \Pi\} \cup (\lambda_G(v) \setminus \Pi)$, for each $v \in V_H$, i.e., the port labels are redefined according to $\alpha$ (if $\alpha(\pi)$ is undefined, the port label is erased) and the other labels are unchanged.

- **Single-vertex graphs:** for a port label $\pi \in \Pi$, $\bullet \pi \stackrel{\text{def}}{=} H$ iff $V_H = \{u\}$ for some vertex $u$, $E_H = \emptyset$ and $\lambda_H(u) = \{\pi, \text{ptype}(\pi)\}$.

For simplicity, we use the same notation for a VR operation above and its corresponding function symbol. Since $\Delta$ and $\Pi$ are finite sets, the above set of function symbols is finite. A VR-term $\theta[x_1, \dots, x_n]$ consists of function symbols (i.e., the binary $\oplus$ and unary $\oplus_{\delta, \pi_1, \pi_2}$ and $\text{relab}_\alpha$) and the variables $x_1, \dots, x_n$ of arity zero. A term is ground if it has no occurrences of variables. We write $\text{val}^{\text{VR}}(\theta)$ for the graph obtained by interpreting the function symbols in the ground term $\theta$ as the corresponding VR-operations.

**Example 1.** The VR-term $\theta \stackrel{\text{def}}{=} \text{relab}_0(\text{add}_{a, \pi, \pi'}((\bigoplus_{i \in 1, \dots, 4} \bullet \pi) \oplus (\bigoplus_{j \in 1, \dots, 3} \bullet \pi'))) \text{ evaluates to the complete bipartite graph val^{VR}(\theta) = }$ $\overrightarrow{K}_{4,3}$ with directed edges $a$, see Figure 2 (a). Edge labels are $\Delta = \{a\}$, port labels are $\Pi = \{\pi, \pi'\}$, and vertex labels are $\Lambda = \Pi \cup \{\text{ptype}(\pi), \text{ptype}(\pi')\}$. The $\pi$-ports are $u_1, \dots, u_4$ and the $\pi'$-ports are $v_1, \dots, v_3$ in Figure 2 (a). We write $\emptyset$ for the empty partial function, that removes all port labels.

The domain of the *HR-algebra* is the set $G^{\text{HR}}(\Lambda, \Delta) \subseteq G(\Lambda, \Lambda)$ of graphs $G$, written $G^{\text{HR}}$ when $\Lambda$ and $\Delta$ are understood, where $\lambda_G(v_1) \cap \lambda_G(v_2) \cap \Pi \neq \emptyset$ implies $v_1 = v_2$, for any two vertices $v_1, v_2 \in V_G$. In other words, a port labels at most one vertex. In the usual terminology, ports are called *sources*, when the *HR-algebra* is understood from the context. The operations of *HR* are the following, see Figure 3 (b) for an illustration:

- **Composition:** $G_1 \|_{\mathbf{p}_1, \mathbf{p}_2} G_2 \stackrel{\text{def}}{=} H$ iff $H$ is obtained from the disjoint union of $G_1, G_2 \in G^{\text{HR}}$ of sorts $\mathbf{p}_1$ and $\mathbf{p}_2$, respectively (taking an isomorphic copy of $G_2$ disjoint from $G_1$, if necessary) by joining all pairs of vertices $v_i \in V_{G_i}$, for $i = 1, 2$ such that $\lambda_{G_1}(v_1) \cap \lambda_{G_2}(v_2) \cap \Pi \neq \emptyset$. The label of a vertex $v$ obtained by joining $v_1 \in V_{G_1}$ with $v_2 \in V_{G_2}$ is $\lambda_{G_1}(v_1) \cup \lambda_{G_2}(v_2)$. Since the label of a vertex in a graph from $G^{\text{HR}}$ contains at most one source, the composition of any two graphs from $G^{\text{HR}}$ is contained in $G^{\text{HR}}$. We write $\|$ instead of $\|_{\mathbf{p}_1, \mathbf{p}_2}$ when the argument sorts are understood.
- Source redefinition: $\text{relab}_\alpha$ is defined in the same way as for VR, with the further restriction that $\alpha$ is an injective partial function. This restriction is necessary to ensure that $\text{relab}_\alpha(G) \in G^{\text{HR}}$ if $G \in G^{\text{HR}}$.

- Single-vertex graphs: are defined in the same way as for VR.

- Single-edge graphs: for an edge label $\delta \in \Delta$ and two port labels $\pi_1 \neq \pi_2 \in \Pi$, $\overrightarrow{\delta}_{\pi_1, \pi_2}^{\text{def}} = H$ iff $V_H = \{v_1, v_2\}$, $E_H = \{(v_1, \delta, v_2)\}$, $\lambda_H(v_i) = \{\pi_i, \text{ptope}(\pi_i)\}$, for $i = 1, 2$.

HR-terms are defined just as VR-terms and $\text{val}^{\text{HR}}(\Theta)$ denotes the graph obtained by interpreting the function symbols in the ground term $\Theta$ as the corresponding HR-operations.

**Example 2.** We write $(\pi)$ for the partial function that acts as the identity on $\{\pi\}$, erasing all source labels except $\pi$. The HR-term $\theta' \stackrel{\text{def}}{=} \text{relab}_0(\overrightarrow{d}_{\pi_\epsilon, \pi'_\epsilon}) \parallel (\parallel_{i \in 1, \dots, 4} \text{relab}_{(\pi_\epsilon)}(\overrightarrow{\epsilon}_{\pi_\epsilon, \pi_\epsilon})) \parallel (\parallel_{j \in 1, \dots, 3} \text{relab}_{(\pi'_\epsilon)}(\overrightarrow{\epsilon'}_{\pi'_\epsilon, \pi'_\epsilon}))$ evaluates to the graph shown in Figure 2 (b). The edge labels are $\Delta = \{a, \epsilon\}$, the port labels are $\Pi = \{\pi, \pi', \pi_\epsilon, \pi'_\epsilon\}$, the vertex labels are $\Lambda = \Pi \cup \{\text{ptope}(\pi), \text{ptope}(\pi'), \text{ptope}(\pi_\epsilon), \text{ptope}(\pi'_\epsilon)\}$. The $\pi, \pi', \pi_\epsilon$ and $\pi'_\epsilon$-ports in Figure 2 are respectively $u_{1, \dots, 4}, v_{1, \dots, 3}, u_\epsilon, v_\epsilon$.

## 2.2 Grammars

Graph grammars are a standard way to represent sets of graphs. Let $\Omega$ be an algebra, either VR or HR. A $\Omega$-grammar is a pair $\Gamma = (\Xi, \Pi)$ consisting of a finite set $\Xi$ of nonterminals and a finite set $\Pi$ of rules of the form, either (1) $X \to t[X_1, \dots, X_n]$, where $X, X_1, \dots, X_n \in \Xi$ are nonterminals and $t$ is a $\Omega$-term whose only variables are $X_1, \dots, X_n$, or (2) $X \to t$, where $X \in \Xi$; the rules of this form are called axioms. Given $\Omega$-terms $\Theta$ and $\eta$, a step $\Theta \Rightarrow_\Gamma \eta$ obtains $\eta$ from $\Theta$ by replacing an occurrence of a nonterminal $X$ with the term $t$, for some rule $X \to t[X_1, \dots, X_n]$ of $\Gamma$. A $X$-derivation is a sequence of steps starting with a nonterminal $X$. The derivation is complete if it ends with a ground term. Let $\mathcal{L}_X(\Gamma) \stackrel{\text{def}}{=} \{\text{val}^\Omega(\Theta) \mid X \Rightarrow_\Gamma^* \Theta\}$ is a complete derivation} and $\mathcal{L}(\Gamma) \stackrel{\text{def}}{=} \bigcup_{X \in \Pi} \mathcal{L}_X(\Gamma)$ be the language of $\Gamma$, the algebra $\Omega$ being understood from the rules of $\Gamma$. A set of graphs is VR (resp. HR) iff it is the language of a VR (resp. HR) grammar.

**Example 3.** The VR-grammar $\Gamma$ below produces the term $\Theta$ from Example 1. The language of this grammar contains Figure 2 (a). The HR-grammar $\Gamma'$ produces the term $\Theta'$ from Example 2. The language of this grammar contains Figure 2 (b).

$$ \Gamma: \left\{ \begin{array}{rcl} & \to S & \\ S & \to & \text{relab}_0(\text{add}_{a,\pi,\pi'}(K)) \\ K & \to & \bullet\pi \\ K & \to & \bullet\pi' \\ K & \to & K \oplus K \end{array} \right. $$

$$ \Gamma' : \left\{ \begin{array}{rcl} & \to S & \\ S & \to & \text{relab}_0(\overrightarrow{d}_{\pi_\epsilon, \pi'_\epsilon} \parallel K) \\ K & \to & \text{relab}_{(\pi_\epsilon)}(\overrightarrow{\epsilon}_{\pi_\epsilon, \pi_\epsilon}) \\ K & \to & \text{relab}_{(\pi'_\epsilon)}(\overrightarrow{\epsilon'}_{\pi'_\epsilon, \pi'_\epsilon}) \\ K & \to & K \parallel K \end{array} \right. $$

It is known that the expressivity of VR-grammars strictly subsumes that of HR-grammars [15]. The relation between VR and HR is made precise by the following:

**Definition 1.** Let $\mathcal{E}$ be a set of edge labels disjoint from $\Delta$. An $\mathcal{E}$-graph is a graph $G \in G(\Lambda, \Delta \cup \mathcal{E} \cup \overleftarrow{\mathcal{E}})$ such that

$$ \overleftarrow{\mathcal{E}}^{\text{def}} = \{\overleftarrow{e} \mid e \in \mathcal{E}\}, \text{ and for every edge } (u, e, v), e \in \mathcal{E}, \text{ there exists an edge } (v, \overleftarrow{e}, u). $$
- the subgraph of $G$ consisting of $\mathcal{E}$-labeled edges and the vertices that have incoming $\mathcal{E}$-labeled edges is a forest, i.e., every non-root vertex points to a single parent.

The expansion of an $\mathcal{E}$-graph $G \in \mathcal{G}(\Lambda, \Delta \cup \mathcal{E} \cup \mathcal{E}^-)$ is $\exp(G) \in \mathcal{G}(\Lambda, \Delta)$, where:

- $V_{\exp(G)}$ is the set of vertices of $G$ that are not the target of an $\mathcal{E}$-labeled edge,

- $E_{\exp(G)}$ is the set of edges $(v_1, \delta, v_2)$ for which there exist $\mathcal{E}$-labeled paths from $v_i$ to some vertices $v'_i \in G$, for $i = 1, 2$, such that $(v'_1, \delta, v'_2) \in E_G$, for some $\delta \in \Delta$,

- $\lambda_{\exp(G)}(v) \stackrel{\text{def}}{=} \lambda_G(v)$.

**Proposition 1 (Proposition 2.4 in [12]).** For each VR-grammar $\Gamma$, one can build a HR-grammar $\Gamma'$ such that $\mathcal{L}(\Gamma) = \exp(\mathcal{L}(\Gamma'))$.

*Example 4.* The HR-grammar $\Gamma'$ from Example 3 is obtained by transformation of the VR-grammar $\Gamma$ from the same example, such that $\mathcal{L}(\Gamma) = \exp(\mathcal{L}(\Gamma'))$, where $\mathcal{E} = \{\varepsilon\}$. We omit $\mathcal{E}$-edges from this figure: their placement is simply the inverse of $\mathcal{E}$-edges.

# 3 Parameterized Systems

We aim at describing a family of networks by a VR-grammar. To model the behavior of a network, we associate to each vertex in the graph a *process type*, which is a finite-state machine represented as a Petri net of a particular form. We denote by $\mathbb{P}$ the fixed and finite set of process types. In the rest of this paper, the alphabet of vertex labels is assumed to be $\Lambda \stackrel{\text{def}}{=} \mathbb{P} \cup \Pi$, where $\Pi = \bigcup_{p \in \mathbb{P}} \Pi_p$, $\Pi_p$ is a set of port labels partitioned according to the process types, i.e., $\Pi_p$ is the set of ports corresponding to the process type $p$. The intuition is that different vertices labeled with a process type run copies of that process type, called *processes*. Neighbouring processes communicate by joining their transitions in a symmetric synchronous rendezvous, represented by a pair of transitions, that labels the edge between their host vertices. Hence, the alphabet $\Delta$ of edge labels is considered to be the set of pairs of transitions from the process types $\mathbb{P}$.

## 3.1 Petri Nets

We make the definition of process types precise by recalling Petri nets. A *net* is a tuple $N = (Q_N, T_N, W_N)$, where $Q_N$ is a finite set of *places*, $T_N$ is a finite set of *transitions*, disjoint from $Q_N$, and $W_N : (Q_N \times T_N) \cup (T_N \times Q_N) \to \mathbb{N}$ is a *weighted incidence relation* between places and transitions. For all $x, y \in Q_N \cup T_N$ such that $W_N(x, y) > 0$, we say that there is an *edge of weight* $W_N(x, y)$ between $x$ and $y$. For an element $x \in Q_N \cup T_N$, we define the set of *predecessors* $\bullet x \stackrel{\text{def}}{=} \{y \in Q_N \cup T_N \mid W_N(y, x) > 0\}$, *successors* $x \stackrel{\text{def}}{=} \{y \in Q_N \cup T_N \mid W_N(x, y) > 0\}$ and *predecessor-successor pair* $\bullet x \bullet \stackrel{\text{def}}{=} (\bullet x, x \bullet)$.
If not obvious from the context, we will specify the net in which the predecessor and successor and considered: $(\bullet x)_N, (x \bullet)_N, (\bullet x \bullet)_N$.

A *marking* of $N$ is a function $m : Q_N \to \mathbb{N}$. A transition $t$ is *enabled* in the marking $m$ if $m(q) \ge W_N(q, t)$, for each place $q \in Q$. For all markings $m$, $m'$ and transitions $t \in T$, we write $m \leadsto m'$ whenever $t$ is enabled in $m$ and $m'(q) = m(q) - W_N(q, t) + W_N(t, q)$, for all $q \in Q_N$. Given a marking $m$, a sequence of transitions $\rho = (t_1, t_2, ... ) \in (T_{\mathcal{N}})^\infty$ is
<figure><img src="image_8.png" /><figcaption>**Fig. 4.** Examples of process types (a). The behavior of a $\vec{K}_{4,3}(\text{send}, \text{recv})$ system (b)</figcaption></figure>

a firing sequence iff either (i) $\rho$ is empty, or (ii) there exist markings $m_1, m_2, \dots$ such that $m \stackrel{i_1}{\rightsquigarrow} m_1, m_1 \stackrel{i_2}{\rightsquigarrow} m_2, m_2 \stackrel{i_3}{\rightsquigarrow} \dots$. When $\rho$ has finite length $n$, we can write $m \stackrel{\rho}{\rightsquigarrow} m_n$, and we say that $\rho$ is a firing sequence from $m$ to $m_n$.

A Petri net (PN) is a pair $\mathcal{N} = (N, m_0)$, where $N$ is a net and $m_0$ is the initial marking of $N$. For simplicity, we write $Q_{\mathcal{N}} \stackrel{\text{def}}{=} Q_N$, $T_{\mathcal{N}} \stackrel{\text{def}}{=} T_N$, $W_{\mathcal{N}} \stackrel{\text{def}}{=} W_N$ and $\text{init}_{\mathcal{N}} \stackrel{\text{def}}{=} m_0$ for the elements of $\mathcal{N}$. A marking $m$ is reachable in $\mathcal{N}$ iff there exists a finite firing sequence $\rho$ such that $m_0 \stackrel{\rho}{\rightsquigarrow} m$. We denote by $\text{Paths}(\mathcal{N})$ the set of finite or infinite firing sequences of $\mathcal{N}$ starting from $\text{init}_{\mathcal{N}}$.

## 3.2 Behaviors

We formalize the behavior of a system (i.e., a graph whose vertices are labeled by process types) using PNs. To do so, we associate to each process type a PN having a special form:

**Definition 2.** A process type $p$ is a PN having weights at most 1 and exactly one marked place initially, whose transitions are partitioned into observable $T_p^{\text{obs}}$ and internal $T_p^{\text{int}}$, i.e., $T_p = T_p^{\text{obs}} \uplus T_p^{\text{int}}$, such that each transition has exactly one predecessor and one successor. Let $\mathbb{P} = \{p_1, \dots, p_k\}$ be a finite fixed set of process types such that $Q_{p_i} \neq \emptyset$, for all $i \in [1, k]$ and $Q_{p_i} \cap Q_{p_j} = \emptyset$, for all $1 \le i < j \le k$.

Because a process type has exactly one initial token and all transitions have one predecessor and one successor, every reachable marking of a process type has exactly one token. We denote by $Q_{\mathbb{P}} \stackrel{\text{def}}{=} \biguplus_{p \in \mathbb{P}} Q_p$ and $T_{\mathbb{P}}^{\text{obs}} \stackrel{\text{def}}{=} \biguplus_{p \in \mathbb{P}} T_p^{\text{obs}}$ the sets of places and observable transitions from some $p \in \mathbb{P}$, respectively.

**Example 5.** Figure 4 (a) shows two examples of process types, *Once* and *Loop*. Observable transitions are shown in black, and internal transitions in yellow. They have $Q_{\text{Once}} = \{\text{on}, \text{off}\}$, $T_{\text{Once}}^{\text{obs}} = T_{\text{Once}} = \{\text{send}\}$, $Q_{\text{Loop}} = \{\text{free}, \text{busy}\}$, $T_{\text{Loop}}^{\text{obs}} = \{\text{recv}\}$ and $T_{\text{Loop}}^{\text{int}} = \{\text{handle}\}$.

**Definition 3.** A system $S = (V_S, E_S, \lambda_S) \in \mathcal{G}(\mathbb{P} \uplus \Pi, T_{\mathbb{P}}^{\text{obs}} \times T_{\mathbb{P}}^{\text{obs}})$ is a graph whose vertices $v \in V_S$ are labeled with exactly one process type $\text{proc}_S(v) = p \stackrel{\text{def}}{\iff} \lambda_S(v) \cap \mathbb{P} = \{p\}$ and at most one port $\text{port}_S(v) = \pi \stackrel{\text{def}}{\iff} \lambda_S(v) \cap \Pi = \{\pi\}$. Edges $v_1 \xrightarrow{(t_1, t_2)} v_2 \in E_S$ are labeled with pairs of observable transitions, such that $t_i \in T_{\text{proc}_S(v_i)}^{\text{obs}}$, for $i = 1, 2$. We denote by $S(\mathbb{P}) \stackrel{\text{def}}{=} \mathcal{G}(\mathbb{P}, T_{\mathbb{P}}^{\text{obs}} \times T_{\mathbb{P}}^{\text{obs}})$ the set of systems of empty sort, i.e., without ports.
The communication (i.e., synchronization between processes) in a system is formally captured by the following notion of behavior:

**Definition 4.** A behavior is a PN $\mathcal{N}$ such that $1 \le \|\bullet t\| = \|t\| \le 2$, for each $t \in T_{\mathcal{N}}$. The behavior of a system $S$ is $\beta(S) \stackrel{\text{def}}{=} (N, m_0)$, where:

- $Q_N \stackrel{\text{def}}{=} \{(q, v) \mid q \in Q_{\text{proc}_S(v)}, v \in V_S\}$, a place $(q, v)$ corresponds to the place $q$ of the process type that labels the vertex $v$,

- $T_N \stackrel{\text{def}}{=} E \cup \{(t, v) \mid t \in T_{\text{proc}_S(v)}^{\text{int}}, v \in V_S\}$, the transitions are either edges of the system (i.e., modeling the synchronizations of two processes) or pairs $(t, v)$ corresponding to an internal transition $t$ of the process type that labels the vertex $v$,

- the weight function $W_N$ is such that internal transitions are preserved, and observable transitions are merged according to edge labels. That is, for every $v$ such that $(\bullet t)_{\text{proc}_S(v)} = (\{q\}, \{q'\})$ we have $(\bullet (t, v))_N = (\{(q, v)\}, \{(q', v')\})$, and for every edge $e = (v \xrightarrow{t,t'} v')$ with $(\bullet t)_{\text{proc}_S(v)} = (\{q_1\}, \{q_2\})$ and $(\bullet t')_{\text{proc}_S(v')} = (\{q'_1\}, \{q'_2\})$ we have $(\bullet e)_{\text{N}} = (\{(q_1, v), (q'_1, v')\}, \{(q_2, v), (q'_2, v')\})$.

- $m_0(q, v) \stackrel{\text{def}}{=} \text{init}_{\text{proc}_S(v)}(q)$, for all $v \in V_S$ and $q \in Q_{\text{proc}_S(v)}$.

**Example 6.** Figure 4 (b) shows the behavior of $\vec{K}_{4,3}(\text{send}, \text{recv})$, having the architecture shown in Figure 2 (a), with the red vertices $u_1...4$ labeled with the process type *Once* and blue vertices $v_1...3$ labeled with the process type *Loop*, from Figure 4. The edges are labeled by the pair $(\text{send}, \text{recv})$ of observable transitions from *Once* and *Loop*.

## 3.3 The Parametric Reachability Problem

A parametric VR (*resp.* HR) system is described by a VR (*resp.* HR) grammar $\Gamma$. We define our decision problem as a parametric reachability problem asking if there exists an instance of a parametric system, described by a grammar, whose behavior reaches an error configuration from a given set. If the answer is negative, we have a proof that the parametric system is correct.

Let $\mathcal{X}$ be a fixed countably infinite set of variables, interpreted over natural numbers. An arithmetic formula $\alpha$ is a (possibly quantified) first-order formula using variables in $\mathcal{X}$, constants denoting natural numbers, the binary operations of addition and multiplication and the (in)equality relation. We denote by $\mathcal{A}$ the set of such formulæ. Let $\mathcal{N}$ be a PN and $\ell: Q_{\mathcal{N}} \to \mathcal{X}$ be a partial function that labels certain places of $\mathcal{N}$ with variables. The boolean value $[[\alpha]]_m^\ell \in \{\text{true, false}\}$ of an arithmetic formula $\alpha$ in a marking $m: Q_{\mathcal{N}} \to \mathcal{N}$ is obtained by replacing each variable $x$ that occurs free in $\alpha$ by the integer value $\sum_{q \in \ell^{-1}(x)} m(q)$, i.e., the total number of tokens from the places associated with $x$ in $m$. We further define $\text{Atoms}^\ell(m) \stackrel{\text{def}}{=} \{\alpha \in \mathcal{A} \mid [[\alpha]]_m^\ell = \text{true}\}$, i.e., the set of arithmetic formulæ satisfied by a given marking and a variable labeling. A PN $\mathcal{N}$ satisfies a reachability specification $\alpha$ for a place labeling $\ell$, written $(\mathcal{N}, \ell) \models \alpha$, iff there exists a finite firing sequence $\rho$ leading to a reachable marking $\text{init}_{\mathcal{N}} \stackrel{\rho}{\rightsquigarrow} m'$ such that $\alpha \in \text{Atoms}^\ell(m')$.

We specialize the satisfiability of a reachability specification by an arbitrary PN to the satisfiability by the behavior of a system $S \in \mathcal{S}(\mathbb{P})$ and a labeling $L: Q_{\mathbb{P}} \to \mathcal{X}$ of the
places from the process types $\mathbb{P}$ with variables:

$$ (S, L) \models \alpha \iff \mathbf{def} \Rightarrow (\beta(S), L \circ \downarrow_1) \models \alpha $$

where $\downarrow_1$ is the projection of a pair on its first component, i.e., $L \circ \downarrow_1$ labels each pair $(q, v) \in Q_{\beta(S)}$ by the variable $L(q)$, if the latter is defined. Intuitively, we require of $\ell$ that it assigns the same variable to all “copies” of the same place $\{(q, v) | v \in V_S\}$. Hence, the boolean value $[[\alpha]]_m^{L \circ \ell}$ of an atomic proposition in a marking $m$ of $\beta(S)$ is obtained by mapping each free variable $x$ from $\alpha$ to the total number of tokens from a place $(q, v) \in Q_{\beta(S)}$ such that $L(q) = x$. This paper is concerned with the following problem:

**Definition 5.** Let $\mathbb{P}$ be a set of process types. The Parametric Reachability Problem PRP$_{\mathbb{P}}(\Gamma, \alpha, L)$ takes as input a grammar $\Gamma$ such that $\mathcal{L}(\Gamma) \subseteq \mathcal{S}(\mathbb{P})$, a reachability formula $\alpha$ and a place labeling $L: Q_{\mathbb{P}} \to \mathcal{X}$, and asks if there exists some system $S \in \mathcal{L}(\Gamma)$ for which $(S, L) \models \alpha$ holds.

**Example 7.** Choosing $\Gamma$ the $\mathbb{V}\mathbb{R}$-grammar (Example 3), the set of variables $\mathcal{X} \stackrel{\text{def}}{=} \{x, y\}$, the place labeling $L = [\text{on} \mapsto x, \text{off} \mapsto y]$ defined on the process types from Figure 4 (a), and the formula $\alpha \stackrel{\text{def}}{=} y \ge x + 2$, we find that PRP$_{\mathbb{P}}(\Gamma, \alpha, L)$ has a positive answer, because the behavior Figure 4 (b) which belongs to $\beta(\mathcal{L}(\Gamma))$ admits a reachable marking $m$ with 3 tokens on off and 1 token on on, satisfying $[[\alpha]]_m^{L \circ \ell} = [[3 \ge 1 + 2]] = \text{true}$.

In the light of inherent theoretical boundaries, related to the undecidability of the above parametric verification problem [14], several semi-algorithmic methods have been proposed, for parametric HR systems [9] and parametric systems described using similar formalisms, such as a dialect of separation logic with inductive definitions [10] and a recursive term algebra [8]. In particular, the architecture description languages used in [10,8] have similar graph composition and relabeling as the more standard HR grammars. For these methods, the verification of certain coverability properties (e.g., absence of deadlocks and critical section violations) relies on the generation of structural invariants for the parametric family of behaviors, directly from the specification of the architectures and the process types. Examples include *trap invariants*, i.e., sets of places that, once marked, remain forever marked, and *mutex invariants*, i.e., sets of places of which at most one is marked. The generation of structural invariants can be redefined for HR grammars at little cost.

In contrast, there is virtually no verification method for parametric $\mathbb{V}\mathbb{R}$ systems. Many decidability results in the literature consider parametric systems with clique architectures [16], that can be described by simple $\mathbb{V}\mathbb{R}$-grammars. A prominent result is the decidability of the more general parametric model checking problem (PMCP) for *token-passing systems* (where communication is restricted to the passing of a token between processes) with MSO-definable bounded clique-width architectures [4, Theorem 26]. It is known that each MSO-definable set of bounded clique-width is definable by a $\mathbb{V}\mathbb{R}$ grammar, but not viceversa. Moreover, an orthogonal<fnref n="5" /> decidability result for parametric HR token-passing systems is given in [9, Theorem 4]. It is an interesting open problem whether this decidability result for HR systems carries over to $\mathbb{V}\mathbb{R}$ systems, but this exceeds the scope of the current paper, and will be considered in future work.

<footnote n="5">⁵ This result applies to all HR sets of architectures, not just the MSO-definable ones.</footnote>
<figure><img src="image_9.png" /><figcaption>Fig. 5. A process type $p$ (a), the corresponding process type $p_{1/2}$ (b), and $\varepsilon_t$ (c).</figcaption></figure>

# 4 Translating VR to HR Systems

The existence of several verification techniques for parametric systems with HR architectures and the scarcity of similar results for VR systems motivates us to define a translation from VR to HR systems, that preserves the answer of the PRP decision problem (Definition 5). This translation uses expansion to encode dense graphs as sparse graphs (see Figure 2). Since labeled graphs are used as system models (Definition 3), the behavior of a sparse graph must be equivalent to the behavior of its expansion, on what concerns the satisfiability of reachability formulae, thus reducing each instance of the PRP problem for a VR grammar to an instance of the same problem for an HR grammar.

**Theorem 1.** There exist computable $\mathbb{P}^{\mathcal{H}}$ and $\mathbb{L}^{\mathcal{H}}$, process types and place labeling respectively, such that for any VR-grammar $\Gamma$, variable labeling $\mathcal{L}: \mathbb{Q}_{\mathbb{P}} \to \mathcal{X}$ and reachability formula $\alpha$, one can effectively build a HR-grammar $\Gamma'$ such that $\text{PRP}_{\mathbb{P}}(\Gamma, \alpha, \mathbb{L}) \iff \text{PRP}_{\mathbb{P}^{\mathcal{H}}}(\Gamma', \alpha, \mathbb{L}^{\mathcal{H}})$

This result shows that it is possible to solve each instance of the parametric model checking problem that takes a VR grammar as input by an effective reduction to an instance of the same problem for a HR grammar, which, as previously mentioned, has received more attention lately [9].

Intuitively the translation works as follows: vertices in the HR system are either “real” vertices from the original VR system, or routing nodes. A unique vertex of the HR system will act as representative of all vertices currently $\pi$-ports in the VR system, and communication between a $\pi$-port $v$ and a $\pi'$-port $v'$ in the VR system will in the HR system roughly take the form of (1) a request from $v$ to its representative $v_\pi$ through a chain of routing nodes, (2) similarly a request from $v'$ to its representative $v_{\pi'}$, (3) a direct communication between $v_\pi$ and $v_{\pi'}$ (4) an acknowledgement from $v_\pi$ to $v$ following the inverse chain of routing nodes, (5) an acknowledgement from $v_{\pi'}$ to $v'$. This is a simplification because in reality steps (1–2) and (4–5) above may be interleaved, and rather than a single representative there is one representative per observable transition. We define below the process types that correspond to routing nodes, give an intuition of how they function, then show the actual inductive translation.

Let $\mathbb{P}$ be the set of process types used by the VR grammars, in the rest of this section. We define a new set of process types $\mathbb{P}^{\mathcal{H}}$ such that $\mathbb{Q}_{\mathbb{P}} \subseteq \mathbb{Q}_{\mathbb{P}^{\mathcal{H}}}$, see Figure 5 (b) for an example. First, let $\mathbb{P}_{1/2} \stackrel{\text{def}}{=} \{p_{1/2} \mid p \in \mathbb{P}\}$ be a set of process types disjoint from $\mathbb{P}$. A generic $p_{1/2}$ is defined below from $p \in \mathbb{P}$. Intuitively, $p_{1/2}$ simulates the behavior of $p$ in the context of communication through routing nodes: each observable transition is split into two halves, one sending a request, then eventually receiving the acknowledgement.
<figure><img src="image_10.png" /><figcaption>**Fig. 6.** An $\varepsilon_{up}$-path meeting an $\varepsilon_{dn}$-path to simulate the interaction (up, dn) between two vertices of type p from Figure 5 (a).</figcaption></figure>

- $Q_{p1/2} \stackrel{\text{def}}{=} Q_p \uplus \{t_{1/2} \mid t \in T_p^{\text{obs}}\}$, each $t_{1/2}$ is a new place associated with the transition $t$,

- $T_{p1/2} \stackrel{\text{def}}{=} T_p^{\text{int}} \uplus \{\text{try}_t, \text{commit}_t \mid t \in T_p^{\text{obs}}\}$, i.e., each observable transition $t$ of p is split into $\text{try}_t$ (an attempt at firing $t$) and $\text{commit}_t$ ($t$ has been fired remotely),

- $W_{p1/2} \stackrel{\text{def}}{=} W_p \downarrow_{Q_p \times T_p^{\text{int}} \uplus T_p^{\text{int}} \times Q_p} \{ (q, \text{try}_t, 1), (\text{try}_t, t_{1/2}, 1) \mid q \in Q_p, t \in T_p^{\text{obs}}, W_p(q,t) = 1 \} \uplus \{(t_{1/2}, \text{commit}_t, 1), (\text{commit}_t, q, 1) \mid t \in T_p^{\text{obs}}, W_p(t,q) = 1\}$, i.e., whenever $t$ is an observable transition from $q$ to $q'$, there are observable transitions $\text{try}_t$ from $q$ to $t_{1/2}$ and $\text{commit}_t$ from $t_{1/2}$ to $q'$ in $p_{1/2}$.

- $\text{init}_{p1/2} \stackrel{\text{def}}{=} \text{init}_p$.

Second, for each observable transition $t \in T_p^{\text{obs}}$, we consider a new process type $\varepsilon_t$, defined below. See Figure 5 (c) for an example. This is what we call the “routing nodes”.

- $Q_{\varepsilon_t} \stackrel{\text{def}}{=} \{\text{idle}_t, \text{active}_t, \text{wait}_t, \text{reply}_t\}$,

- $T_{\varepsilon_t} = T_{\varepsilon_t}^{\text{obs}} \stackrel{\text{def}}{=} \{\text{recv, send, ack, reset, t}\}$,

- $W_{\varepsilon_t}$ consists of the following edges, all of weight 1:

* $\text{recv} \stackrel{\text{def}}{=} (\text{idle}_t, \text{active}_t)$

* $\text{send} \stackrel{\text{def}}{=} (\text{active}_t, \text{wait}_t)$

* $t \stackrel{\text{def}}{=} (\text{active}_t, \text{reply}_t)$

* $\text{ack} \stackrel{\text{def}}{=} (\text{wait}_t, \text{reply}_t)$

* $\text{reset} \stackrel{\text{def}}{=} (\text{reply}_t, \text{idle}_t)$

- $\text{init}_{\varepsilon_t}(\text{idle}_t) \stackrel{\text{def}}{=} 1$ and $\text{init}_{\varepsilon_t}(\text{active}_t) = \text{init}_{\varepsilon_t}(\text{wait}_t) = \text{init}_{\varepsilon_t}(\text{reply}_t) \stackrel{\text{def}}{=} 0$.

Finally, $\mathbb{P}^{\mathcal{H}} \stackrel{\text{def}}{=} \mathbb{P}_{1/2} \cup \{\varepsilon_t \mid t \in T_p^{\text{obs}}\}$, “real vertices” and “routing nodes” respectively.

**Example 8.** Figure 5 (a) shows examples of p, $p_{1/2}$, and $\varepsilon_t$. Instances of $\varepsilon_t$ exist for $t \in T_p^{\text{obs}} = \{\text{up, dn}\}$. Two processes of type p communicate via a (up, dn) transition, which is encoded by a sequence of transitions, see Figure 6:

<figure><img src="image_11.png" /></figure>

This matches the earlier intuition: the leftmost process tries to execute up and sends a request through routers $\varepsilon_{up}$. At the same time, the right process tries to execute dn and sends a request through routers $\varepsilon_{dn}$. When both requests reach adjacent routers, the transition (up, dn) is jointly executed. Following that, an acknowledgement is sent back to the processes that initiated the communication as a sequence of (reset, ack).

The variable labeling $\mathcal{L} : Q_{\mathbb{P}} \to \mathcal{X}$ induces the following labeling $\mathcal{L}^{\mathcal{H}} : Q_{\mathbb{P}^{\mathcal{H}}} \to \mathcal{X}$:

$\mathcal{L}^{\mathcal{H}}(q) \stackrel{\text{def}}{=} \mathcal{L}(q)$, for each $q \in Q_{\mathbb{P}}$

$\mathcal{L}^{\mathcal{H}}(\text{active}_t) \stackrel{\text{def}}{=} \mathcal{L}(\bullet t)$

$\mathcal{L}^{\mathcal{H}}(\text{reply}_t) \stackrel{\text{def}}{=} \mathcal{L}(t \bullet)$

undefined everywhere else

The rest of the paper is the proof of Theorem 1, instanciated with these $\mathbb{P}^{\mathcal{H}}$ and $\mathcal{L}^{\mathcal{H}}$.
## 4.1 Proof of Theorem 1

The main idea is to use the $\epsilon_t$ processes to define, for a VR-term $\theta$, a HR-term $\mathcal{H}(\theta)$ that evaluates to a sparse system, from which the system $\mathrm{val}^{\mathrm{VR}}(\theta)$ can be retrieved using graph expansion, i.e., $\mathrm{val}^{\mathrm{VR}}(\theta) = \exp(\mathrm{val}^{\mathrm{HR}}(\mathcal{H}(\theta)))$ (Definition 1). Using the set of port labels $\Pi^{\mathcal{H}} \stackrel{\mathrm{def}}{=} \{\pi_{1/2}, (\pi, t), (\bar{\pi}, t) \mid \pi \in \Pi, t \in \mathcal{T}_{\mathrm{MAS}}^{\mathrm{obs}}\}$ where the process type of $\pi_{1/2}$ is $(\mathrm{MAS}(\pi))_{1/2}$ and the process type of $(\pi, t)$ and $(\bar{\pi}, t)$ is $\epsilon_t$, we define $\mathcal{H}(\theta)$ inductively on the structure of $\theta$. That is, in addition to a source label $\pi_{1/2}$ for each port label $\pi \in \Pi$ that occurs in $\theta$, we add two copies of each port label for each observable transition. Intuitively, $(\pi, t)$ will be the port label denoting the root of the tree of $\epsilon_t$ processes, and $(\bar{\pi}, t)$ will be used as backup when we need a fresh copy of $(\pi, t)$. We define a renaming function fresh : $\Pi^{\mathcal{H}} \to \Pi^{\mathcal{H}}$ by $\mathrm{fresh}(\bar{(\pi, t)}) = (\pi, t)$, and undefined everywhere else. That way fresh substitutes each source for its copy and forgets the original one. We also use the renaming function obs : $\Pi^{\mathcal{H}} \to \Pi^{\mathcal{H}}$ which is the identity on $\Pi \times \mathcal{T}_{\mathrm{MAS}}^{\mathrm{obs}}$ and undefined everywhere else, i.e., obs forgets every port label except the $(\pi, t)$ labels.

Concretely, creating new edges between $\epsilon_t$-vertices is done by the below functions:

$$E_{\varepsilon}^{t}(\pi, \pi') \stackrel{\mathrm{def}}{=} \overline{(\mathrm{send}, \mathrm{recv})}_{(\pi,t), (\bar{\pi}', t)} \parallel \overline{(\mathrm{reset}, \mathrm{ack})}_{(\bar{\pi}', t), (\pi,t)} \quad \begin{array}{c} (\pi,t) \xrightarrow{\mathrm{send}, \mathrm{recv}} \\ (\bar{\pi}', t) \xrightarrow{\mathrm{reset}, \mathrm{ack}} \end{array}$$

$$E_{1/2}^{t}(\pi) \stackrel{\mathrm{def}}{=} \overline{(\mathrm{try}, \mathrm{recv})}_{\pi_{1/2}, (\pi,t)} \parallel \overline{(\mathrm{reset}, \mathrm{commit})}_{(\pi,t), \pi_{1/2}} \quad \begin{array}{c} (\pi,t) \xrightarrow{\mathrm{try}, \mathrm{recv}} \\ (\bar{\pi}, t) \xrightarrow{\mathrm{reset}, \mathrm{commit}} \end{array}$$

Recall that the main invariant during the translation is that whenever $v$ in the VR system is a $\pi$-port, its corresponding vertex in the HR system is linked to the unique representative of $(\pi, t)$ through a chain of routers $\epsilon_t$.

An essential gadget used by the construction is the encoding of a relabeling function $\alpha: \Pi \to \Pi$ (which is by definition type-preserving) by a graph denoted $\mathrm{enc}(\alpha)$. We show an example of $\mathrm{enc}(\alpha)$, where $\alpha$ is the function $[\pi_1 \mapsto \pi_2, \pi_2 \mapsto \pi_1, \pi_3 \mapsto \pi_4]$. So as to not clutter the figure, we simply write $E_{\varepsilon}$ to label the entire bundle of edges $\{E_{\varepsilon}^t | t \in \mathcal{T}_{\mathrm{MAS}}^{\mathrm{obs}}\}$ and we write $(\pi, -)$ for $\{(\pi, t) | t \in \mathcal{T}_{\mathrm{MAS}}^{\mathrm{obs}}\}$.

<figure><img src="image_12.png" /></figure>

Intuitively, as the renaming $\alpha$ turns every $\pi$-port into an $\alpha(\pi)$-port, $\mathrm{enc}(\alpha)$ links the previous representatives of $(\pi, -)$ to the new representatives of $(\alpha(\pi), -)$, preserving the invariant. The translation $\mathcal{H}$ is defined inductively on the structure of the term $\theta$:

$$\mathcal{H}(\bullet\pi) \stackrel{\mathrm{def}}{=} \mathrm{relab}_{\mathrm{obs}}\left(\bullet\pi_{1/2} \parallel \left(\parallel_{t \in \mathcal{T}_{\mathrm{MAS}}^{\mathrm{obs}}}(E_{1/2}^{t}(\pi))\right)\right) \quad \text{Figure 7 (a)}$$

$$\mathcal{H}(\mathrm{add}_{(t,t'),\pi,\pi'}(\theta_1)) \stackrel{\mathrm{def}}{=} \overrightarrow{(t,t')}_{(\pi,t), (\bar{\pi}',t')} \parallel \mathcal{H}(\theta_1) \quad \text{Figure 7 (b)}$$

$$\mathcal{H}(\mathrm{relab}_{\alpha}(\theta_1)) \stackrel{\mathrm{def}}{=} \mathrm{relab}_{\mathrm{fresh}}(\mathcal{H}(\theta_1) \parallel \mathrm{enc}(\alpha)) \quad \text{Figure 7 (c,c',c'')}$$

$$\mathcal{H}(\theta_1 \oplus_{\mathbf{p}_1 \cdot \mathbf{p}_2} \theta_2) \stackrel{\mathrm{def}}{=} \mathrm{relab}_{\mathrm{fresh}}(\mathcal{H}(\theta_1) \parallel \mathrm{enc}(\mathrm{id}_{\mathbf{p}_1 \cap \mathbf{p}_2})) \\ \parallel \mathrm{relab}_{\mathrm{fresh}}(\mathcal{H}(\theta_2) \parallel \mathrm{enc}(\mathrm{id}_{\mathbf{p}_1 \cap \mathbf{p}_2})) \quad \text{Figure 7 (d,d',d'')}$$

These are quite straightforward once we understand the invariant: the translation of $\bullet\pi$
<figure><img src="image_13.png" /><figcaption>**Fig. 7.** Construction of $\mathcal{H}$ for each VR symbol. Relabeling uses $\alpha = [\pi_1 \mapsto \pi_2, \pi_2 \mapsto \pi_1, \pi_3 \mapsto \pi_4]$, and composition uses $\mathbf{p}_1 = \{\pi_1, \pi_2, \pi_3\}$ and $\mathbf{p}_2 = \{\pi_1, \pi_2, \pi_4\}$. Ports in gray are hidden during a relabeling.</figcaption></figure>

creates a new vertex and links it to all relevant routing nodes, the rule for $\text{add}_{(t,t'),\pi,\pi'}$ establishes a communication between the representatives of $(\pi, t)$ and $(\pi', t')$, the one for $\oplus$ creates a unique common representative, and the relabeling is as explained earlier.

The relation between the systems $\text{val}^{\text{VR}}(\theta)$ and $\text{val}^{\text{HR}}(\mathcal{H}(\theta))$ is captured by the below lemma. Its proof is the same as in [12, Proposition 2.4], where the new edges have the same label, instead of the following sets of edge labels (Definition 1):

$$ \begin{aligned} \mathcal{E} &\stackrel{\text{def}}{=} \{(\text{try}_t, \text{recv}) \mid t \in \mathbb{T}_{\mathbb{P}}^{\text{obs}}\} \cup \{(\text{send}, \text{recv})\} \\ \overleftarrow{\mathcal{E}} &\stackrel{\text{def}}{=} \{(\text{reset}, \text{commit}_t) \mid t \in \mathbb{T}_{\mathbb{P}}^{\text{obs}}\} \cup \{(\text{reset}, \text{ack})\} \end{aligned} $$

We denote $(\text{commit}_t, \text{reset}) \stackrel{\text{def}}{=} (\overleftarrow{\text{try}}_t, \text{recv})$ and $(\text{ack}, \text{reset}) \stackrel{\text{def}}{=} (\overleftarrow{\text{send}}, \text{recv})$ (Definition 1). The meaning and orientation of these edges are shown on an example in Figure 6.

**Lemma 1.** Let $\theta$ be a ground VR-term, $S \stackrel{\text{def}}{=} \text{val}^{\text{VR}}(\theta)$ and $S' \stackrel{\text{def}}{=} \text{val}^{\text{HR}}(\mathcal{H}(\theta))$. Then, $S = \text{exp}(S')$. For each $v, v' \in \mathcal{V}_{S'}$, if $E \neq \emptyset$ is the set of edges from $v$ to $v'$, then exactly one of the following holds:

1. $(\text{proc}_{S'}(v), \text{proc}_{S'}(v')) = (\mathbf{p}_{1/2}, \varepsilon_t)$, $E = \{(\text{try}_t, \text{recv}), (\text{commit}_t, \text{reset})\}$ and $t \in \mathbb{T}_{\mathbb{P}}^{\text{obs}}$;

2. $(\text{proc}_{S'}(v), \text{proc}_{S'}(v')) = (\varepsilon_t, \varepsilon_{t'})$ and $E = \{(t, t')\}$;

3. $\text{proc}_{S'}(v) = \text{proc}_{S'}(v') = \varepsilon_t$ and $E = \{(\text{send}, \text{recv}), (\text{ack}, \text{reset})\}$.

*Proof.* The proof of $S = \text{exp}(S')$ is the same as [12, Proposition 2.4]. The rest of the points follow from the definition of $\mathcal{H}$. $\square$

The behaviors of $\text{val}^{\text{VR}}(\theta)$ and $\text{val}^{\text{HR}}(\mathcal{H}(\theta))$ are related by the following notion of path stuttering (inspired by [6, Definition 7.89]):
**Definition 6.** Let $S \in S(\mathbb{P})$ and $S' \in S(\mathbb{P}^H)$ be two systems and $L: \mathbb{Q}_{\mathbb{P}} \to \mathcal{L}$ be a variable labeling. Given two finite or infinite firing sequences $\rho \in \text{Paths}(\beta(S))$ and $\rho' \in \text{Paths}(\beta(S'))$, we say that $\rho'$ is a stuttering of $\rho$, and write $\rho \trianglelefteq_L \rho'$, when there exists a finite or infinite sequence $A_0, A_1, \dots \in \mathbb{A}^\infty$ and integers $n_0, n_1, \dots \ge 1$ such that:

$$ \text{Atoms}^{L \circ 1}(\rho) = A_0, A_1, \dots \quad \text{and} \quad \text{Atoms}^{L^H \circ 1}(\rho') = \underbrace{A_0, \dots, A_0}_{n_0 \text{ times}}, \underbrace{A_1, \dots, A_1}_{n_1 \text{ times}}, \dots $$

This relation is lifted to systems as $S \trianglelefteq_L S'$, if and only if the following hold:

1. for each $\rho \in \text{Paths}(\beta(S))$ there exists $\rho' \in \text{Paths}(\beta(S'))$ such that $\rho \trianglelefteq_L \rho'$,

2. for each $\rho' \in \text{Paths}(\beta(S'))$ there exists $\rho \in \text{Paths}(\beta(S))$ such that $\rho \trianglelefteq_L \rho'$.

In particular $S \trianglelefteq S'$ implies that $S$ and $S'$ have sets of reachable configurations that satisfy the same atoms.

**Theorem 2.** Let $S \in S(\mathbb{P})$ and $S' \in S(\mathbb{P}^H)$ be systems and $L: \mathbb{Q}_{\mathbb{P}} \to \mathcal{L}$ be a variable labeling such that $S \trianglelefteq_L S'$. Then, for any arithmetic formula $\alpha$, we have

$$ (S, L) \models \alpha \iff (S', L^H) \models \alpha $$

Finally, applying Theorem 2 to the lemma below (proof in Appendix 5) gives Theorem 1.

**Lemma 2.** Let $\theta$ be a VR-term over the alphabets $\Lambda \stackrel{\text{def}}{=} \mathbb{P} \uplus \Pi$ and $\Delta \stackrel{\text{def}}{=} \Gamma^\text{obs} \times \Gamma^\text{obs}$, and $L: \mathbb{Q}_{\mathbb{P}} \to \mathcal{L}$ be a variable labeling. Then $\text{val}^{\text{VR}}(\theta) \trianglelefteq_L \text{val}^{\text{HR}}(\mathcal{H}(\theta))$.

For the proof of Theorem 1, let $\Gamma'$ be the HR grammar obtained by replacing each occurrence of a VR operation $\text{op}$ from $\Gamma$ by the HR operation $\mathcal{H}(\text{op})$. “⇒” If $\text{PRP}_{\mathbb{P}}(\Gamma, \alpha, L)$ has a positive answer, there exists a system $S \in \mathcal{L}(\Gamma)$ such that $(S, L) \models \alpha$. Hence, there exists a ground VR-term $\theta$ such that $\text{val}^{\text{VR}}(\theta) = S$ and $\theta$ is the result of a complete derivation of $\Gamma$. By the definition of $\Gamma'$, $\mathcal{H}(\theta)$ is a ground HR-term resulting from a complete derivation of $\Gamma'$. By Lemma 2, $\text{val}^{\text{VR}}(\theta) \trianglelefteq_L \text{val}^{\text{HR}}(\mathcal{H}(\theta))$, hence we obtain $(\text{val}^{\text{HR}}(\mathcal{H}(\theta)), L^H) \models \alpha$, by Theorem 2 and $\text{PRP}_{\mathbb{P}^H}(\Gamma', \phi, L^H)$ has a positive answer. The “<” direction uses a symmetric argument. $\square$

# 5 Conclusions and Future Work

We consider the parametric reachability problem for families of networks of finite-state processes specified using VR graph grammars. Our approach is to reduce the problem to HR grammars, for which several verification techniques have been developed lately. The reduction is based on a construction of an HR grammar that expands to the language of a given VR grammar, by elimination of epsilon-edges. We prove that this construction preserves any reachability property expressed using first-order arithmetic over variables that count the number of processes in each state.

Future work involves an implementation of the proposed reduction, based on existing tools for parametric verification of networks specified using HR grammars [9]. In particular, we plan to experiment with Azure-like network topologies and suitable routing (existence of an available route) properties. We also plan to extend the decidability result for pebble-passing systems with HR grammars [9] to VR grammars.
**Acknowledgements.** This research is supported by the French National Research Agency project "Parametric Verification of Dynamic Distributed Systems" (PaVeDyS) under grant number ANR-23-CE48-0005. We also wish to thank the anonymous reviewers for their helpful suggestions.

**Disclosure of interests.** The authors have no competing interests to declare that are relevant to the content of this article.

# Appendix

## Proof of Lemma 2

In this entire section, let $\theta$ be a fixed ground VR-term written using the set $\Lambda = \mathbb{P} \uplus \Pi$ of vertex labels. It is easy to check that $\mathcal{H}(\theta)$ is a ground HR-term written using the set $\Lambda^{\mathcal{H}} \stackrel{\text{def}}{=} \mathbb{P}^{\mathcal{H}} \uplus \Pi^{\mathcal{H}}$ of vertex labels, where the sets $\mathbb{P}^{\mathcal{H}}$ of process types and $\Pi^{\mathcal{H}}$ of ports have been defined above. We write $S$ (resp. $S'$) for $\text{val}^{\text{VR}}(\theta)$ (resp. $\text{val}^{\text{HR}}(\mathcal{H}(\theta))$).

Take a reachable marking $\mathfrak{m}$ of $\beta(S')$, and any transition $t \in \mathbb{T}_{\mathfrak{p}}^{\text{obs}}$. We say that a vertex $v$ of type $\varepsilon_t$ is *idle* if $\mathfrak{m}(\text{idle}_t, v) = 1$. We say that $v$ of type $\varepsilon_t$ is *waiting on t* if $\mathfrak{m}(\text{wait}_t, v) = 1$. We say that $v$ of type $\rho_{1/2}$ is *waiting on t* if $\mathfrak{m}(t_{1/2}, v) = 1$. Finally, given a label $\delta \in \mathcal{E}$ and an edge $(v', \delta, v) \in \mathcal{E}_{S'}$, we say that $v'$ is an *E-predecessor* of $v$.

**Fact 1** For any reachable marking $\mathfrak{m}$ of $\beta(S')$, a vertex $v$ of type $\varepsilon_t$ is non-idle in $\mathfrak{m}$ if and only if there exists a $\mathcal{E}$-predecessor of $v$ that is waiting on $t$ in $\mathfrak{m}$. Furthermore if there exists such an $\mathcal{E}$-predecessor, there will be exactly one.

*Proof.* This proof is by induction. Since the property must hold for any reachable marking, we show that it holds for $\text{init}_{\beta(S')}$, then that is it preserved by every firing of a transition.

In $\text{init}_{\beta(S')}$ all vertices of type $\varepsilon_t$ are in their initial state and thus have a token in $\text{idle}_t$. All vertices of type $p \in \mathbb{P}$ have a token in a place of $Q_{\mathbb{P}}$, not a place from $(\mathbb{T}_{\mathbb{P}})_{1/2}$. Therefore in the initial configuration, non-idle processes do not exist, and no process is waiting. The property is thus easy to verify.

For the inductive step, consider any transition that can occur in $\beta(S')$, resulting in the firing $\mathfrak{m} \xrightarrow{\delta} m'$. The structural properties that we established in Lemma 1 guarantee that the following case analysis is exhaustive:

- firing an internal transition $t$ in $v$: no vertex of type $\varepsilon_t$ is involved, and the vertex $v$ in which the transition occurs is not waiting in either $m$ or $m'$ since $\bullet t$ and $t\bullet$ are both places of $Q_{\mathbb{P}}$ not $(\mathbb{T}_{\mathbb{P}})_{1/2}$. Therefore the property holds in $m'$.

- firing $(v', (\text{try}_t, \text{recv}), v)$: for this interaction to be fireable requires that $\mathfrak{m}(\bullet t, v') = 1$ ($v'$ is not waiting in $\mathfrak{m}$) and $\mathfrak{m}(\text{idle}_t, v) = 1$ ($v$ is idle in $\mathfrak{m}$). The inductive hypothesis applied to the latter fact yields that all $\mathcal{E}$-predecessors of $v$ are not waiting on $t$ in $\mathfrak{m}$, so when the firing makes $v$ non-idle and $v'$ waiting on $t$ by $\mathfrak{m}'(t_{1/2}, v') = 1$ and $\mathfrak{m}'(\text{active}_t, v) = 1$, it makes $v'$ the unique $\mathcal{E}$-predecessor of $v$ that is waiting on $t$ in $\mathfrak{m}$. Meanwhile $v'$ is not of type $\varepsilon_t$ so is not subject to the condition, $v$ did not become waiting on $t$ so the possible $\mathcal{E}$-successor of $v$ is not affected, and all other
processes retain the same state so must satisfy the same property in $m'$ as they did
in m. Therefore $m \stackrel{(v', (try_t, recv), v)}{\rightsquigarrow} m'$ preserves the desired property.

- firing $(v', (send, recv), v)$: in the same spirit as the previous case, this transition makes the token of $v'$ move from $active_t$ to $wait_t$, so $v'$ remains non-idle and additionally becomes waiting on $t$ in $m'$, and at the same time the token of $v$ moves from $idle_t$ to $active_t$, so $v$ becomes non-idle but remains non-waiting.
Once again, $v$ has gained exactly one waiting $\mathcal{E}$-predecessor, and all other vertices are unaffected, so $m'$ satisfies the property.

- firing $(v', (t', t), v)$: this time we must have $m(\mathit{active}_t, v') = \mathit{m}(\mathit{active}_{t'}, v') = 1$, and $\mathit{m}(\mathit{reply}_t, v') = \mathit{m}(\mathit{reply}_{t'}, v') = 1$. All vertices are non-idle in $m'$ if and only if they are non-idle in $m$, and they are waiting on $t$ in $m'$ if and only if they are waiting on $t$ in $m$. The desired property is thus easily preserved.

- firing $(v', (\mathit{commit}_t, \mathit{reset}), v)$: this transition makes $v'$ (waiting in $m$) return to non-waiting in $m'$, and $v$ (non-idle in $m$) return to idle in $m'$. This case is exactly symmetrical to the firing of $(v', (\mathit{try}_t, \mathit{recv}), v)$ and an analogous reasoning shows that it preserves the property at hand.

- firing $(v', (\mathit{ack}, \mathit{reset}), v)$: similarly this case is symmetrical to $(v', (\mathit{send}, \mathit{recv}), v)$ and accordingly can be handled by the same reasoning.

Thus the property is preserved by all firings of transitions of $\beta(S')$, and therefore holds in all reachable markings. $\square$

We define a relation $\approx$ between markings $m : Q_{\beta(S)} \to \mathbb{N}$ and $m' : Q_{\beta(S')} \to \mathbb{N}$, where $m \approx m'$ if for every place $(q, v) \in Q_{\beta(S)}$ such that $m(q, v) = 1$ we have one of the following properties:

(i) $m'(q, v) = 1$, or

(ii) $\exists t \in q. \exists v' \in V_{S'}. \mathit{WaitPath}_{m'}(v, v') \wedge m'(t_{1/2}, v) = 1 \wedge m'(\mathit{active}_{t'}, v') = 1$, or

(iii) $\exists t \in q. \exists v' \in V_{S'}. \mathit{WaitPath}_{m'}(v, v') \wedge m'(t_{1/2}, v) = 1 \wedge m'(\mathit{reply}_t, v') = 1$.

where we define the predicate $\mathit{WaitPath}_{m'}(v, v')$ as the existence of an $\mathcal{E}$-labeled path $v, v_1, v_2, \dots, v_k, v'$ from $v$ to $v'$ such that $m'(\mathit{wait}_t, v_i) = 1$ for every $1 \le i \le k$. Furthermore we say that $m'$ is *canonical* if only condition (i) is ever satisfied.

Intuitively $m'$ is canonical and $m \approx m'$ when $m'$ has tokens in the same places as $m$ does. For non-canonical $m'$, we can tolerate transitions that are partially executed and depending on whether the partial execution of $t$ is less or more than half we count the token as being either in $\bullet t$ or in $t^\bullet$ (recall: an $\mathcal{E}$-labeled path of $S'$ simulates a transition of $S$, and the progress of this simulation is less than half if we have a path of $\mathit{wait}_t$ until an $\mathit{active}_t$, and more than half if we have a path of $\mathit{wait}_t$ until a $\mathit{reply}_t$).

**Fact 2** For any $m \approx m'$, we have $\mathit{Atoms}^\ell(m) = \mathit{Atoms}^{\ell\mathcal{H}}(m')$

*Proof.* Due to Lemma 1 and Fact 1, we know that when in the definition of $\approx$ above we talk about an $\mathcal{E}$-labeled path $\mathit{WaitPath}_{m'}(v, v')$ in the form of $v, v_1, \dots, v_k, v'$, it necessarily means that all $v_1, \dots, v_k$ are vertices of type $\varepsilon_t$, and that they are disjoint from any other instanciation of $\mathit{WaitPath}_{m'}$ for a different place. In particular this implies that the conditions (i), (ii), (iii) are mutually exclusive, and any token in a place $\mathit{active}_t$ or
reply$_t$ can be injectively mapped to some vertex $v$ with a token in $t_{1/2}$ from which there
is a WaitPath$_{m'}$ as described.

This induces a bijection between {$v \in V_S \mid m(q, v) = 1$}, and {$v \in V_{S'} \mid m'(q, v) = 1$} $\uplus$
{$v \in V_{S'} \mid m'(\text{active}_t, v) = 1$ for $t \in q^\bullet$} $\uplus$ {$v \in V_{S'} \mid m'(\text{reply}_t, v) = 1$ for $t \in \bullet q$}, implying that they have the same cardinal. It happens that $\sum_{q \in \ell^{-1}(x)} m(q)$ is exactly the cardinal of the first set, and $\sum_{q \in (\ell^H)^{-1}(x)} m'(q)$ is the cardinal of the second. We conclude that $\ell$ and $\ell^H$ have the same interpretation of $x$, and since this applies to every $x \in \mathcal{X}$ we conclude that the same atoms are satisfied in $m$ and in $m'$. $\square$

**Fact 3** If $m'_0 \stackrel{\delta}{\rightsquigarrow} m'_1$ in $\beta(S')$ and $\delta \in \mathcal{E} \cup \overleftarrow{\mathcal{E}}$, then for all $m$ marking of $\beta(S)$ we have $m \approx m'_0$ if and only if $m \approx m'_1$.

*Proof.* Once again we rely on Lemma 1 and Fact 1. Consider an interaction that can be fired between some $v$ and $v'$, and assume that it results in the transition from $m'_0$ to $m'_1$. Since $\approx$ is defined pointwise on each place of $\beta(S)$ that holds a token, and since $m$ is unchanged, it suffices to look at exactly the places of $\beta(S')$ that are changed by $m'_0 \stackrel{\delta}{\rightsquigarrow} m'_1$. In all configurations we will show that the equivalence is preserved simply by changing which of the conditions (i), (ii), (iii) hold on each place. In all that follows we will write $t$ the transition that we consider (fully determined by the type $\epsilon_t$ of $v'$), and $v_0 \in V_S$ the vertex that is currently being considered for the equivalence. The cases are as follows:

- $(v, (\text{try}_t, \text{recv}), v')$: $m$ is linked to $m'_0$ on $(\bullet t, v)$ by condition (i). Furthermore $v_0 = v$. We show that after firing $\delta = (\text{try}_t, \text{recv})$ the markings are now linked by condition (ii) on the path $v, v'$.

In $m'_0$, the vertex $v$ which is of type $p_{1/2}$ has a token in place $\bullet t$. We know this
because it is the only way that its transition try$_t$ is fireable, and this is why condition
(i) is satisfied. Similarly there must be a token in (idle$_t$, $v'$) so that recv is fireable.
After firing $\delta$ we now have $m'_1$ $(t_{1/2}, v) = 1$ and $m'_1$ $(\text{active}_t, v') = 1$. This satisfies the
condition for (ii) with WaitPath$_{m'_1}$ $(v, v')$ instanciated by the trivial path $v, v'$. Every
step of this reasoning is in fact an equivalence, so we also get the other direction of
the statement.

- $(v, (\text{send}, \text{recv}), v')$: $m$ and $m'_0$ are linked on $(\bullet t, v_0)$ by condition (ii), in the form of $\text{WaitPath}_{m'_0}(v_0, v)$ instanciated by some $v_0, v_1, \dots, v_k, v$. We show that $m$ and $m'_1$ are still linked by condition (ii), but on $v'$ instead of $v$.

The interaction (send, recv) belongs to $\mathcal{E}$, so $v_0, v_1, \dots, v_k, v, v'$ is still an $\mathcal{E}$-labeled path. In fact after we fire $\delta$, we get $m'_1$ (wait$_t$, $v$) = 1 which means that $v_0, v_1, \dots, v_k, v, v'$ instanciates $\text{WaitPath}_{m'}(v_0, v')$. Lastly we have $m'_1$ (active$_t$, $v'$) = 1, thus satisfying condition (ii).

- $(v, (\text{commit}_t, \text{reset}), v')$: $m$ is linked to $m'_0$ on $(t^\bullet, v_0)$ by condition (iii). With a reasoning analogous to the first case, including the fact that $v_0 = v$, we can prove that $m$ and $m'_1$ are instead linked by condition (i).

- $(v, (\text{ack}, \text{reset}), v')$: $m$ is linked to $m'_0$ on $(t^\bullet, v_0)$ by condition (iii). With a reasoning analogous to the second case, we can prove that $m$ and $m'_1$ are still linked by condition (iii), but using a shorter $\text{WaitPath}(v_0, v)$ instead of $\text{WaitPath}(v_0, v')$.

☐
**Fact 4** For any markings $m_1, m_2 : Q_{\beta(S)} \to \mathbb{N}$, transition $\delta \in T_{\beta(S)}$ such that $m_1 \stackrel{\delta}{\rightsquigarrow} m_2$ in $\beta(S)$, and any $m_1' : Q_{\beta(S')} \to \mathbb{N}$, if $m_1 \approx m_1'$ and $m_1'$ is canonical then there exist a marking $m_2' : Q_{\beta(S')} \to \mathbb{N}$, an $\mathcal{E}$-sequence **p**, and an $\overleftarrow{\mathcal{E}}$-sequence **q**, such that $m_1' \stackrel{\mathbf{p}, \delta, q}{\rightsquigarrow} m_2'$ in $\beta(S')$ and $m_2 \approx m_2'$ with $m_2'$ canonical.

*Proof.* Firstly if $\delta$ is an internal transition, then the canonicity of $m_1 \approx m_2$ and the fact that process types in $\mathbb{P}_{1/2}$ have the same internal transitions as those of $\mathbb{P}$, give that $\delta$ must also be fireable in $m_2$. We thus choose both **p** and **q** to be the empty sequence.

Otherwise, we assume that from $m_1$ to $m_2$, the interaction $\delta = (t, t')$ occurs between vertices $v$ and $v'$. As we hinted at in Example 8, we choose **p** to be $(\text{try}_t, \text{recv})$, $(\text{send}, \text{recv})$, ..., $(\text{send}, \text{recv})$ on an $\varepsilon_t$-path starting from $v$, followed by $(\text{try}_{t'}, \text{recv})$, $(\text{send}, \text{recv})$, ..., $(\text{send}, \text{recv})$, on an $\varepsilon_{t'}$-path starting from $v'$. After that we execute $(t, t')$, then propagate backwards for **q** as $(\text{reset}, \text{ack})$, ..., $(\text{reset}, \text{ack})$, $(\text{reset}, \text{commit}_t)$ and $(\text{reset}, \text{ack})$, ..., $(\text{reset}, \text{ack})$, $(\text{reset}, \text{commit}_{t'})$ along the same two paths in reverse.

Since $m_1'$ is canonical, all vertices of type $\varepsilon_t$ and $\varepsilon_{t'}$ in $S'$ have a token in $\text{idle}_t$ in $m_1'$. Since $S = \exp(S')$, the existence of an interaction $(t, t')$ between $v$ and $v'$ implies that there are some $u, u'$ in $S'$ and there exist an $\varepsilon_t$-path from $v$ to $u$ and an $\varepsilon_{t'}$-path from $v'$ to $u'$. Along such paths, the sequence of transitions described above is a firing sequence if initially all vertices of type $\varepsilon_t$ and $\varepsilon_{t'}$ are in state $\text{idle}_t$ and $\text{idle}_{t'}$ respectively, and they will return to state $\text{idle}_t$ or $\text{idle}_{t'}$ once the entire sequence is fired.

Thus $m_1' \stackrel{\mathbf{p}, \delta, q}{\rightsquigarrow} m_2'$, $m_2'$ is canonical, and $m_2 \approx m_2'$. $\square$

**Fact 5** Every (finite or infinite) firing sequence in Paths($\beta(S)$) admits a stuttering firing sequence in Paths($\beta(S')$).

*Proof.* Let $\text{init}_{\beta(S)} = m_0 \stackrel{\delta_0}{\rightsquigarrow} m_1 \stackrel{\delta_1}{\rightsquigarrow} m_2 \stackrel{\delta_2}{\rightsquigarrow} \dots$ be a (finite or infinite) firing sequence $\rho \in \text{Paths}(\beta(S))$. Using the initialization that $\text{init}_{\beta(S)} \approx \text{init}_{\beta(S')}$, and the latter is canonical (since the initial token of $\varepsilon_t$ is in $\text{idle}_t$ for all $t$), we can inductively apply Fact 4 at every step to construct a firing sequence $\text{init}_{\beta(S')} = m_0' \stackrel{\mathbf{p}_0, \delta_0, q_0}{\rightsquigarrow} m_1' \stackrel{\mathbf{p}_1, \delta_1, q_1}{\rightsquigarrow} m_2' \stackrel{\mathbf{p}_2, \delta_2, q_2}{\rightsquigarrow} \dots$ which is a path $\rho' \in \text{Paths}(\beta(S'))$. In this construction all $\mathbf{p}_i$ and $\mathbf{q}_i$ are $\mathcal{E}$-sequences and $\overleftarrow{\mathcal{E}}$-sequences respectively, thus invariant for $\approx$ (Fact 3). This in turn implies that they do not change the set of atomic propositions that hold (Fact 2).

A path $\text{Atoms}^\ell(\rho) = A_0 A_1 A_2 \dots$, where $\rho \in \text{Paths}(\beta(S))$ is thus transformed by this construction into a path $\text{Atoms}^{\ell'}(\rho') = A_0^{1+|\mathbf{p}_0|} A_1^{1+|\mathbf{q}_0|+|\mathbf{p}_1|} A_2^{1+|\mathbf{q}_1|+|\mathbf{p}_2|} \dots$ which gives $\rho \sqsubseteq_L \rho'$, for some $\rho' \in \text{Paths}(\beta(S'))$. $\square$

**Fact 6** Any firing sequence of $\mathcal{E} \cup \overleftarrow{\mathcal{E}}$-transitions must be finite.

*Proof.* In principle, the proof is straightforward: we define a cost function on places and show that every $\mathcal{E}$-labeled transition moves a token to a place that has a strictly
smaller cost. Let $c: Q_{\beta(S')} \to \mathbb{N}$ be defined as follows:

$$c(\text{wait}_t, v) = c(\text{idle}_t, v) = c(t_{1/2}, v) = 0 \quad \text{for any } t, v$$

$$c(\text{active}_t, v) = 1 + c(\text{active}_t, v') \quad \text{if } \exists v'. v \xrightarrow{\mathcal{E}} v'$$

$$c(\text{active}_t, v) = 0 \quad \text{otherwise}$$

$$c(q, v) = 1 + \max_{t \in q^*} \max_{v:v \xrightarrow{\mathcal{E}} v'} c(\text{active}_t, v') \quad \text{for any } q, v$$

$$c(\text{reply}_t, v) = 1 + \max_{v':v' \xrightarrow{\mathcal{E}} v} c(t^*, v) + \max_{v':v' \xrightarrow{\mathcal{E}} v} c(\text{reply}_t, v') \quad \text{for any } t, v$$

This function, apart from being obviously nonnegative, is well-defined everywhere: the acyclicity of the subgraph of $S'$ composed only of $\mathcal{E}$-edges guarantees that the system of equations above has a solution. More precisely:

- $c$ is obviously well-defined for places of the form $(\text{wait}_t, v)$, $(\text{idle}_t, v)$, or $(t_{1/2}, v)$;

- when a token is in a place $(\text{active}_t, v)$ it can only be involved in transitions in the direction of $\mathcal{E}$ which is acyclic. Furthermore vertices $\varepsilon_t$ form a forest so if $v'$ such that $v \xrightarrow{\mathcal{E}} v'$ exists then it is unique, thus $c$ is also well-defined for places of the form $(\text{active}_t, v)$;

- finally $c$ over $(q, v)$ and $(\text{reply}_t, v)$ is defined in terms of $\mathcal{E}$-predecessors, which are not unique (thus why we need a max), but still form an acyclic graph.

Given a marking $m$, we define

$$\text{fuel}(m) \stackrel{\text{def}}{=} \sum_{q \in Q_{S'}} m(q)c(q)$$

Observe that since $m(q)$ can only take the value 0 or 1, the fuel of a marking is the sum of the cost of every place with a token. Our objective is now to show that whenever $m \xrightarrow{t_0} m'$ for $t_0 \in T_{\beta(S')}$ labeled by $\delta \in \mathcal{E} \cup \overleftarrow{\mathcal{E}}$, we have $\text{fuel}(m) > \text{fuel}(m')$. We do this by showing the equivalent fact that $\text{fuel}(m) - \text{fuel}(m') > 0$ because most of it cancels out: partition the set of vertices into $t_0$ (loses a token when we fire $t_0$), $t_0^*$ (receives a token when we fire $t_0$), and the rest (unchanged), and we are left with simply

$$\text{fuel}(m) - \text{fuel}(m') = \sum_{q \in t} c(q) - \sum_{q \in t^*} c(q)$$

Now for the case analysis on $\delta$:

- $(v, (\text{try}_t, \text{recv}), v')$: $\text{fuel}(m) - \text{fuel}(m') = c(\bullet t, v) + c(\text{idle}_t, v') - c(t_{1/2}, v) - c(\text{active}_t, v') = c(\bullet t, v) - c(\text{active}_t, v')$. Since $v \xrightarrow{\mathcal{E}} v'$, $(\text{active}_t, v')$ is already accounted for in $c(\bullet t, v) = 1 + \max_{t \in (\bullet t)^*} \max_{v:v \xrightarrow{\mathcal{E}} v'} c(\text{active}_t, v')$, and thus $c(\bullet t, v) > c(\text{active}_t, v')$. We easily conclude that $\text{fuel}(m) - \text{fuel}(m') > 0$.

- $(v, (\text{send}, \text{recv}), v')$: $\text{fuel}(m) - \text{fuel}(m') = c(\text{active}_t, v) + c(\text{idle}_t, v') - c(\text{idle}_t, v) - c(\text{active}_t, v') = c(\text{active}_t, v) - c(\text{active}_t, v') = (1 + c(\text{active}_t, v')) - c(\text{active}_t, v') = 1$ strictly positive as expected.
- $(v, (\text{commit}_t, \text{reset}), v')$: fuel($m$) - fuel($m'$) = $c(t_{1/2}, v) + c(\text{reply}_t, v') - c(t^\bullet, v) - c(\text{idle}_t, v') = c(\text{reply}_t, v') - c(t^\bullet, v)$. Since the quantity $c(\text{reply}_t, v)$ occurs in $\max_{v:v \stackrel{\delta}{\to} v'} c(\text{reply}_t, v)$ which is part of the sum that constructs $c(\text{reply}_t, v')$, the inequality is obvious.

- $(v, (\text{ack}, \text{reset}), v')$: The same reasoning as the previous case applies, since this time fuel($m$) - fuel($m'$) = $c(\text{reply}_t, v) - c(\text{reply}_t, v')$ and once again $c(\text{reply}_t, v')$ occurs in $\max_{v:v \stackrel{\delta}{\to} v'} c(\text{reply}_t, v)$ leading to $c(\text{reply}_t, v) - c(\text{reply}_t, v') > 0$.

In all cases we obtain fuel($m$) > fuel($m'$). The function fuel, as we have already justified, is a well-defined finite nonnegative quantity. It follows that an infinite firing sequence of $\mathcal{E} \cup \overleftarrow{\mathcal{E}}$-labeled edges cannot exist. $\square$

**Fact 7** For any markings $m'_1, m'_2 : Q_{\beta(S')} \to \mathbb{N}$, transition $\delta \in T_{\beta(S')}$ such that $m'_1 \stackrel{\delta}{\rightleftharpoons} m'_2$ in $\beta(S)$, and any $m_1 : Q_{\beta(S)} \to \mathbb{N}$, if $m_1 \approx m'_1$ and $\delta \notin \mathcal{E} \cup \overleftarrow{\mathcal{E}}$ then there exists a marking $m_2 : Q_{\beta(S)} \to \mathbb{N}$ such that $m_1 \stackrel{\delta}{\rightleftharpoons} m_2$ in $\beta(S)$ and $m_2 \approx m'_2$.

*Proof*. If $\delta = t$ is an internal transition, it means that for some $(q, v) = \bullet t$ we have $m'_1(q, v) = 1$. Thee definition of $\approx$ this implies $m_1(q, v) = 1$ and thus $\delta$ is also fireable in $\beta(S)$ and obviously leads to $m_2 \approx m'_2$.

Otherwise $\delta = (t, t')$ is an observable transition. It must occur between some $e$ and $e'$ of respective types $\epsilon_t$ and $\epsilon_{t'}$, and in $m_2$ they must have a token in active$_t$ and active$_{t'}$ respectively. By the characterization from Fact 1, there must furthermore exist some vertices $v, v'$ such that there is an $\epsilon_t$-path from $v$ to $e$ and an $\epsilon_{t'}$-path from $v'$ to $e'$, and all vertices along those paths have a token in wait$_t$ or wait$_{t'}$ respectively. Finally, still from Fact 1, we obtain that in $m'_1$, $v$ and $v'$ have a token in $t_{1/2}$ and $t'_{1/2}$ respectively.

Knowing that $m_1 \approx m'_1$, this means that $m_1(\bullet t, v) = 1$ and $m_1(\bullet t', v) = 1$, and thus $(t, t')$ is fireable in $m'_1$. Firing it yields $m'_2$ with $m_2(t^\bullet, v) = 1$ and $m_2(t'^\bullet, v) = 1$. On the other hand $m'_2$ only differs from $m'_1$ in that instead of having $m'_1(\text{active}_t, e) = 1$ and $m'_1(\text{active}_{t'}, e') = 1$ we now have $m'_2(\text{reply}_t, e) = 1$ and $m'_2(\text{reply}_{t'}, e') = 1$. In the definition of $\approx$, we thus easily check that $m_2 \approx m'_2$. $\square$

**Fact 8** Every (finite or infinite) firing sequence in Paths($\beta(S')$) is a stuttering of a firing sequence in Paths($\beta(S)$).

*Proof*. Let $\text{init}_{\beta(S')} = m'_0 \stackrel{t_1}{\rightleftharpoons} m'_1 \stackrel{t_2}{\rightleftharpoons} \dots$ be a firing sequence $\rho' \in \text{Paths}(\beta(S'))$. Let $i_0 = 0$ then $i_1, i_2, \dots$ be an enumeration of all the indices $i$ for which $t_i \notin \mathcal{E} \cup \overleftarrow{\mathcal{E}}$. Starting from $\text{init}_{\beta(S')} = m_0$, we apply Fact 7 for every $i_j$ in increasing order, to get a firing sequence $\rho$ defined by $m_0 \stackrel{t_1}{\rightleftharpoons} m_1 \stackrel{t_2}{\rightleftharpoons} \dots$ and such that $m_j \approx m'_{i_j}$ for every $j \ge 0$. Applying Fact 3 in-between gives that $m_j \approx m'_{k}$ for every $i_j \le k < i_{j+1}$, and Fact 6 guarantees that there are finitely many stuttering steps. We can finally conclude $\text{Atoms}^\ell(\rho) \subseteq \text{Atoms}^{\ell\mathcal{H}}(\rho')$. $\square$

<figure><img src="image_14.png" /></figure>

Finally we conclude from Fact 5 and Fact 8 that $\beta(S) \subseteq_L \beta(S')$: $\beta(S)$ and $\beta(S')$ have the same set of paths, up to finite stuttering on the side of $S'$.
References

1. P. A. Abdulla, K. Cerans, B. Jonsson, and Y. Tsay. General decidability theorems for infinite-state systems. In *Proceedings, 11th Annual IEEE Symposium on Logic in Computer Science, New Brunswick, New Jersey, USA, July 27-30, 1996*, pages 313–321. IEEE Computer Society, 1996.

2. P. A. Abdulla, G. Delzanno, N. B. Henda, and A. Rezine. Monotonic abstraction: on efficient verification of parameterized systems. *Int. J. Found. Comput. Sci.*, 20(5):779–801, 2009.

3. P. A. Abdulla, G. Delzanno, and A. Rezine. Approximated parameterized verification of infinite-state processes with global conditions. *Formal Methods Syst. Des.*, 34(2):126–156, 2009.

4. B. Aminof, T. Kotek, S. Rubin, F. Spegni, and H. Veith. Parameterized model checking of rendezvous systems. In P. Baldan and D. Gorla, editors, *CONCUR 2014 - Concurrency Theory - 25th International Conference, CONCUR 2014, Rome, Italy, September 2-5, 2014. Proceedings*, volume 8704 of *Lecture Notes in Computer Science*, pages 109–124. Springer, 2014.

5. B. Aminof, T. Kotek, S. Rubin, F. Spegni, and H. Veith. Parameterized model checking of rendezvous systems. *Distributed Comput.*, 31(3):187–222, 2018.

6. C. Baier and J. Katoen. *Principles of model checking*. MIT Press, 2008.

7. R. Bloem, S. Jacobs, A. Khalimov, I. Konnov, S. Rubin, H. Veith, and J. Widder. *Decidability of Parameterized Verification*. Synthesis Lectures on Distributed Computing Theory. Morgan & Claypool Publishers, 2015.

8. M. Bozga and R. Iosif. Specification and safety verification of parametric hierarchical distributed systems. In G. Salaün and A. Wijs, editors, *Formal Aspects of Component Software - 17th International Conference, FACS 2021, Virtual Event, October 28-29, 2021, Proceedings*, volume 13077 of *Lecture Notes in Computer Science*, pages 95–114. Springer, 2021.

9. M. Bozga, R. Iosif, A. Sangnier, and N. Villani. Counting abstraction for the verification of structured parameterized networks. *CoRR*, abs/2502.15391, 2025.

10. M. Bozga, R. Iosif, and J. Sifakis. Verification of component-based systems with recursive architectures. *Theor. Comput. Sci.*, 940(Part):146–175, 2023.

11. M. Browne, E. Clarke, and O. Grumberg. Reasoning about networks with many identical finite state processes. *Information and Computation*, 81(1):13–31, 1989.

12. B. Courcelle. Structural properties of context-free sets of graphs generated by vertex replacement. *Information and Computation*, 116(2):275–293, 1995.

13. B. Courcelle and J. Engelfriet. *Graph Structure and Monadic Second-Order Logic: A Language-Theoretic Approach*. Encyclopedia of Mathematics and its Applications. Cambridge University Press, 2012.

14. E. A. Emerson and K. S. Namjoshi. Reasoning about rings. In *POPL*, pages 85–94, 1995.

15. J. Engelfiet and G. Rozenberg. A comparison of boundary graph grammars and context-free hypergraph grammars. *Information and Computation*, 84(2):163–206, 1990.

16. S. M. German and A. P. Sistla. Reasoning about systems with many processes. *J. ACM*, 39(3):675–735, 1992.

17. A. Greenberg, J. R. Hamilton, N. Jain, S. Kandula, C. Kim, P. Lahiri, D. A. Maltz, P. Patel, and S. Sengupta. V12: a scalable and flexible data center network. *SIGCOMM Comput. Commun. Rev.*, 39(4):51–62, Aug. 2009.

18. D. Hirsch, P. Inverardi, and U. Montanari. Graph grammars and constraint solving for software architecture styles. In *Proceedings of the Third International Workshop on Software Architecture*, ISAW '98, page 69–72, New York, NY, USA, 1998. Association for Computing Machinery.
19. K. Jayaraman, N. S. Bjørner, J. Padhye, A. Agrawal, A. Bhargava, P. C. Bissonnette, S. Foster, A. Helwer, M. Kasten, I. Lee, A. Namdhari, H. Niaz, A. Parkhi, H. Pinnamraju, A. Power, N. M. Raje, and P. Sharma. Validating datacenters at scale. In J. Wu and W. Hall, editors, *Proceedings of the ACM Special Interest Group on Data Communication, SIGCOMM 2019*, Beijing, China, August 19-23, 2019, pages 200–213. ACM, 2019.

20. D. Le Metayer. Describing software architecture styles using graph grammars. *IEEE Transactions on Software Engineering*, 24(7):521–533, 1998.

21. D. Lesens, N. Halbwachs, and P. Raymond. Automatic verification of parameterized linear networks of processes. In *The 24th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages*, pages 346–357. ACM Press, 1997.

22. Z. Shtadler and O. Grumberg. Network grammars, communication behaviors and automatic verification. In J. Sifakis, editor, *Automatic Verification Methods for Finite State Systems, International Workshop*, volume 407 of LNCS, pages 151–165. Springer, 1989.

23. P. Wolper and V. Lovinfosse. Verifying properties of large sets of processes with network invariants. In *Automatic Verification Methods for Finite State Systems, International Workshop*, volume 407 of LNCS, pages 68–80. Springer, 1989.