# Counting Abstraction and Decidability for the Verification of Structured Parameterized Networks

Marius Bozga, Radu Iosif, Arnaud Sangnier, Neven Villani

► To cite this version:

Marius Bozga, Radu Iosif, Arnaud Sangnier, Neven Villani. Counting Abstraction and Decidability for the Verification of Structured Parameterized Networks. Computer Aided Verification, Jul 2025, Zagreb, Croatia. pp.238. hal-05194491

HAL Id: hal-05194491

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

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_1.png" /></figure>

Distributed under a Creative Commons Attribution 4.0 International License
# Counting Abstraction and Decidability for the Verification of Structured Parameterized Networks

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

¹ Univ. Grenoble Alpes, CNRS, Grenoble INP, VERIMAG, 38000, France

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

`{firstname}.{lastname}@univ-grenoble-alpes.fr`

² DIBRIS, Univ. of Genova, Italy

`{firstname}.{lastname}@unige.it`

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

**Abstract.** We consider the verification of parameterized networks of replicated processes whose architecture is described by hyperedge-replacement graph grammars in the style of Courcelle. 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 approximate the behaviors of the original system. The counting abstraction is implemented in a prototype tool, evaluated 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.

## 1 Introduction

The architecture is a crucial design aspect for the functionality of a computer network. For instance, the code of a consensus protocol changes depending on whether it is used in a ring or a clique-shaped network. The architecture also influences the traffic balance and overall efficiency of communication. Formal modelling of network architectures is a key enabler for the use of verification algorithms that prove absence of error scenarios in a distributed environment (e.g., deadlocks, races or mutual exclusion violations), or convergence towards a desired goal (e.g., building a spanning-tree or electing a leader).

The impressive size of present day networks requires parameterized models, that describe infinite families of networks having an unbounded number of nodes. The problem of parameterized verification (i.e., proving correctness for any number of processes) often amounts to model-checking a small cut-off of the system (see [8] for a survey). In cases where a cut-off does not exist or is too large, symbolic representations of invariants (i.e., sets of configurations closed under local and communication actions) using e.g., boolean constraints [19], well-structured transitions systems [1], monadic second-order logic [11] or finite-state automata [28] can be used to decide a parameterized safety problem in a matter of seconds. This is because, in particular, parameterized verification methods do not suffer from the state explosion problem of classical model-checking techniques, that scale poorly in the number of concurrent processes.

However, a current limitation is that most techniques rely on hard-coded network topologies, typically cliques [22], rings [14] or combinations thereof [5]. Many archi-
tecture description languages have been developed by the software engineering community (see, e.g., [13] and [15] for surveys) to support network design but, in general, these languages lack support for verification. Only a few recent parameterized verification techniques take architectures as input of the problem, described using, e.g., first-order [9] or separation logic [12]. Such descriptive (logic-based) languages are typically hard to use, because of the generality of their semantics, that requires complex frame conditions to specify what is actually not part of the architecture.

*Contributions* We consider the parametric verification problem for process networks specified by graph grammars that use operations of the standard hyperedge-replacement (HR) algebra of graphs [17] to describe how graphs are inductively built from smaller subgraphs. This constructive aspect of graph grammars makes them appealing for network design, because recursive specification of types and datastructures are widespread among programmers. Graph grammars are, moreover, at the core of a solid theory (see [17] for a comprehensive survey). 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.

Because the parameterized verification problem is undecidable, even for chain-like networks, we consider two orthogonal lines of work. First, following the seminal work of German and Sistla [22], where identities of processes communicating through rendezvous in a clique is ignored to keep only the number of processes in each state, we define a *counting abstraction* that folds the infinite set of networks specified using a HR grammar into a finite set of Petri nets, which subsumes the behaviors of the original set of networks. As a consequence, if a set of places is not covered by an execution of some of the resulting Petri nets, then it is not covered by the original set of behaviors. These coverability problems can be used to express mutual exclusion, and can encode other properties (e.g., finite-valued consensus). Even though, computing the counting abstraction for clique networks is fairly simple [22], it is less trivial for families of networks specified by a grammar. We circumvent these technical challenges by defining appropriate HR algebras, in which the abstraction can be computed by a finite Kleene iteration of the grammar. This line of work is motivated by several recent advances on the theory [20] and tool support [31] for the reachability and coverability problem for Petri nets. The abstraction has been implemented in a prototype tool and a number of experiments showing the effectiveness of the method have been carried out.

Second, we define a decidable fragment of the original problem, by restricting the local behavior of the nodes to pebble-passing systems, where a finite (but unbounded) number of identical pebbles can be moved from one node to another. We inspire ourselves from token-passing systems[4,6] for which a restriction on the behavior of each process allows to get decidability results of some verification problems. Note that in our case, the processes definition are simple, but we allow an unbounded number of tokens/pebbles. Interestingly, our decidable restriction applies only to the local behavior and does not restrict the family of networks considered, other than that they must be the language of a given HR grammar. Examples of problems from this decidable fragment include token-rings, tree-traversal used, in general, for notification and binary consen-
sus among the participants of general (HR-specified) architectures. We have studied the complexity of the decidable fragment and found it to be doubly-exponential in the unary size of the coverability property and in the maximal tree-width the set of networks generated by the grammar. At the same time, we found the problem to be PSPACE-hard.

*Related Work* Traditionally, verification of unbounded networks of parallel processes considers known architectural patterns, typically cliques or rings [22,14]. Because the price for decidability is drastic restriction on architecture styles [8], more recent works propose practical semi-algorithms, e.g., *regular model checking* [24] or *automata learning* [16]. Here the architecture is implicitly determined by the class of language recognizers: word automata encode pipelines or rings, whereas tree automata describe trees.

Specifying parameterized concurrent systems inductively is reminiscent of *network grammars* [29,26,23], that use inductive rules to describe systems with linear (pipeline, token-ring) architectures obtained by composition of an unbounded number of processes. In contrast, our language is based on the HR graph algebra. Verification of network grammars against safety properties (reachability of error configurations) requires the synthesis of *network invariants* [33], computed by costly fixpoint iterations [27] or by abstracting (forgetting the particular values of indices in) the composition of a small number of instances [25]. A more recent line of work considers a lightweight invariant synthesis method based on the inference of *structural invariants*<fnref n="3" /> of an infinite family of Petri nets, for parameterized systems whose network architectures are specified using logic [9,12]. This method is geared towards deadlock-freedom and mutual exclusion, whereas our counting abstraction method works for coverability properties, in general.

Other methods to verify safety properties of parameterized networks consist in changing the semantics of behaviors to obtain an over-approximation having a decidable safety verification problem. In [2], the authors have implemented such a scheme using a *monotonic abstraction*, where the resulting abstraction is a *well-structured transition systems* [1]. They first consider pipeline architectures, where communication is done by checking existentially or universally the state of the other process. In [3], a similar technique is applied to networks with clique architectures, where processes can manipulate shared boolean and natural variables. In contrast, both our methods target network architectures defined by unrestricted HR graph grammars.

## 2 Preliminaries

We denote by $\mathbb{N}$ the set of positive integers, including zero. 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 denoted $\|A\|$. A singleton $\{a\}$ will be denoted $a$. By $A \subseteq_{fin} B$, we mean that $A$ is a finite subset of $B$. The union of two disjoint sets $A$ and $B$ is denoted as $A \uplus B$. The Cartesian product of two sets $A$ and $B$ is denoted $A \times B$. As usual, we denote by $A^*$ the set of (possibly empty) sequences of elements from $A$.

For a function $f: A \to B$ and $C \subseteq A$, we write $f(C) \stackrel{def}{=} \{f(c) \mid c \in C\}$ and $f \downarrow_C \stackrel{def}{=} \{(c, f(c)) \mid c \in C\}$. The inverse of a function $f: A \to B$ is the relation $f^{-1} \stackrel{def}{=} \{(f(a), a) \mid a \in A\}$. To alleviate notation, we write $f(x,y)$ instead of $f((x,y))$, when no confusion

<footnote n="3">³ Invariants that depend on the structure of a Petri net, which hold for any of its executions.</footnote>
arises. For two functions $f: A \to B$ and $g: C \to D$, the function $f \times g: A \times B \to C \times D$
maps each pair $(a, c) \in A \times C$ into the pair $(f(a), g(c)) \in B \times D$. A bijective function
$f: A \to A$ is a finite permutation if the set $\{a \in A \mid f(a) \neq a\}$ is finite. In particular,
$a \leftrightarrow b$ denotes the finite permutation that switches $a$ with $b$ and leaves the other elements
of the domain unchanged. A finite partial function is denoted as $f: A \to_{fin} B$ and $dom(f)$,
$img(f)$ denote its domain and range, respectively. When $f: A \to C$ and $g: B \to C$
coincide on their shared domain $A \cap B$, we write $f \cup g: A \cup B \to C$ the function such
that $(f \cup g) \downarrow_A = f$ and $(f \cup g) \downarrow_B = g$. The full version of the paper contains proofs of
technical results [10].

## 2.1 Petri Nets

A *net* is a tuple $N = (Q, T, W)$, where $Q$ is a finite set of *places*, $T$ is a finite set of *transitions* such that $Q \cap T = \emptyset$ and $W: (Q \times T) \cup (T \times Q) \to N$ is a *weighted incidence relation* between places and transitions. We denote by $Q_N, T_N$ and $W_N$ the places, transitions and incidence relation of $N$, respectively. For all $x, y \in Q \cup T$ such that $W(x, y) > 0$, we say that there is an *edge of weight* $W(x, y)$ between $x$ and $y$. For an element $x \in Q \cup T$, we define the set of *predecessors* $x^\bullet \stackrel{\text{def}}{=} \{y \in Q \cup T \mid W(y, x) > 0\}$, *successors* $x^\text{•} \stackrel{\text{def}}{=} \{y \in Q \cup T \mid W(x, y) > 0\}$ and *predecessor-successor pair* $x^\bullet \stackrel{\text{def}}{=} (x^\bullet, x^\text{•})$.

A marking of $N = (Q, T, W)$ is a function $m: Q \to \mathbb{N}$. A transition $t$ is enabled in $m$ if $m(q) \ge W(q, t)$, for each place $q \in Q$. For all markings $m, m'$ and transitions $t \in T$, we write $m \stackrel{t}{\rightsquigarrow} m'$ when $t$ is enabled in $m$ and $m'(q) = m(q) - W(q, t) + W(t, q)$, for all $q \in Q$. Given two markings $m$ and $m'$, a finite sequence of transitions $\mathbf{t} = (t_1, \dots, t_n)$ is a *firing sequence*, written $m \stackrel{\mathbf{t}}{\rightsquigarrow} m'$, if and only if either (i) $n = 0$ and $m = m'$, or (ii) $n \ge 1$ and there exist markings $m_1, \dots, m_{n-1}$ such that $m \stackrel{t_1}{\rightsquigarrow} m_1 \stackrel{t_2}{\rightsquigarrow} \dots \stackrel{t_{n-1}}{\rightsquigarrow} m_{n-1} \stackrel{t_n}{\rightsquigarrow} m'$. A sequence $\mathbf{t}$ is *fireable* from $m$ whenever there exists a marking $m'$ such that $m \stackrel{\mathbf{t}}{\rightsquigarrow} m'$.

A Petri net (PN) is a pair $\mathcal{N} = (\mathbb{N}, m_0)$, where $\mathbb{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 firing sequence $\mathbf{t}$ such that $m_0 \stackrel{\mathbf{t}}{\rightsquigarrow} m$. We denote by $\text{reach}(\mathcal{N})$ the set of reachable markings of $\mathcal{N}$. The reachability problem asks, given a PN $\mathcal{N}$ and a marking $m$, does $m \in \text{reach}(\mathcal{N})$? The coverability problem asks, for a given PN $\mathcal{N}$ and marking $m$, does there exists a marking $m' \in \text{reach}(\mathcal{N})$ such that $m \le m'$? Here the order of markings is the pointwise order on $\mathbb{N}$, i.e., $m \le m'$ iff $m(q) \le m'(q)$ for all $q \in Q_{\mathcal{N}}$. The coverability problem is more concisely stated using the set of covered markings $\text{cover}(\mathcal{N}) \stackrel{\text{def}}{=} \{m \mid \exists m' \in \text{reach}(\mathcal{N}) \cdot m \le m'\}$, i.e., given $\mathcal{N}$ and $m$, does $m \in \text{cover}(\mathcal{N})$?

## 2.2 Parameterized Systems

We begin by defining parameterized communicating systems, i.e., graphs whose vertices model network nodes that run identical copies of one or more process types. Neighbouring processes synchronize their transitions according to the observable edge labels of the network graph. In most of the literature (see, e.g., [7] for a survey) process types are represented by finite labeled transition systems (LTS), e.g., with disjoint
<figure><img src="image_4.png" /><figcaption>**Fig. 1.** Two process types (a), A system with chain-shape network $S_1$ (top) and a system with star-shape network $S_2$ (bottom) (b). Behavior of $S_1$ (c). Behavior of $S_2$ (d)</figcaption></figure>

observable and internal alphabets of transition labels. For simplicity, here we use PNs whose transitions mimick closely the transitions of a LTS, thus avoiding the formal definition of the latter.

Let $\Lambda$ and $\Delta$ be finite disjoint alphabets of vertex and edge labels, respectively. A (binary labeled) *graph* is a tuple $G = (V, E, \lambda)$, where $V$ is a finite set of vertices, $E \subseteq V \times \Delta \times V$ is a set of labeled binary edges and $\lambda: V \to \Lambda$ maps each vertex to a vertex label. Edges $(v_1, a, v_2)$ are written $v_1 \xrightarrow{a} v_2$. We denote by $V_G$, $E_G$ and $\lambda_G$ the vertices, edges and vertex labeling of $G$, respectively. We do not distinguish isomorphic graphs, *i.e.*, graphs that differ only in the identities of their vertices.

**Definition 1.** 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}} \cup T_p^{\text{int}}$, and each transition has exactly one predecessor and one successor. Let $\mathcal{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, both with weight exactly 1, every reachable marking of a process type has exactly one initial token. A PN having this property is said to be *automata-like*. We denote by $Q_P$ and $T_P^{\text{obs}}$ the sets of places and observable transitions from some $p \in P$, respectively.

*Example 1.* Figure 1 (a) shows two process types *Cont* and *Proc*. They both represent entities that can hold a token and they can either grab a token, if they do not have it, or release the token, otherwise. The first one, which we identify as a controller, has only observable transitions, whereas the second one, which represents a worker process, has two internal transitions *start* and *stop* depicted in yellow. These transitions are used to
simulate the fact that when the worker has the token, it can move to a working state, from which he cannot release the token and when it stops working, it can move back to a state from which the token can be released.

**Definition 2.** A system $S = (V, E, \lambda)$ is a graph whose vertices are labeled with process types from $\mathcal{P}$ ($\Lambda = \mathcal{P}$) and edges with pairs of observable transitions from $T_{\mathcal{P}}^{\text{obs}}$ (i.e., $\Delta = T_{\mathcal{P}}^{\text{obs}} \times T_{\mathcal{P}}^{\text{obs}}$), such that $t_i \in T_{\lambda(v_i)}^{\text{obs}}$, for both $i = 1, 2$, for each edge $v_1 \xrightarrow{(t_1, t_2)} v_2 \in E_S$.

**Example 2.** Figure 1 (b) shows two systems labeled with the process types given by Figure 1 (a). They both represent a network with four entities, one controller of type *Cont* and three working processes of type *Proc*. In $S_1$, the controller can pass a token to the first working process, which can pass the token to the second one which can pass the token to the third one. In $S_2$, the controller is at the center and it communicate with all the working processes that get and release the token.

The communication (i.e., synchronization between processes) in a system is formally captured by the following notion of behavior:

**Definition 3.** 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 = (V, E, \lambda)$ is $\beta(S) \stackrel{\text{def}}{=} (N, m_0)$, where:

- $Q_N \stackrel{\text{def}}{=} \{(q, v) | q \in Q_{\lambda(v)}, v \in V\}$, a place $(q, v)$ corresponds to the place $q$ of the process type $\lambda(v)$ that labels the vertex $v$;

- $T_N \stackrel{\text{def}}{=} E \cup \{(t, v) | t \in T_{\lambda(v)}^{\text{int}}, v \in V\}$, 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 $\lambda(v)$ that labels the vertex $v$;

- the weight function $W_N$ is defined below:

$$W_N((q, v), v_1 \xrightarrow{(t_1, t_2)} v_2) \stackrel{\text{def}}{=} \begin{cases} W_{\lambda(v)}(q, t_i), & \text{if } v = v_i, \text{ for } i = 1, 2 \\ 0, & \text{otherwise} \end{cases}$$

$$W_N(v_1 \xrightarrow{(t_1, t_2)} v_2, (q, v)) \stackrel{\text{def}}{=} \begin{cases} W_{\lambda(v)}(t_i, q), & \text{if } v = v_i, \text{ for } i = 1, 2 \\ 0, & \text{otherwise} \end{cases}$$

$$W_N((q, v), (t, v')) \stackrel{\text{def}}{=} \begin{cases} W_{\lambda(v)}(q, t), & \text{if } v = v' \\ 0, & \text{otherwise} \end{cases}, \quad W_N((t, v'), (q, v)) \stackrel{\text{def}}{=} \begin{cases} W_{\lambda(v)}(t, q), & \text{if } v = v' \\ 0, & \text{otherwise} \end{cases}$$

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

For example, Figure 1 (c) and (d) show the behaviors of the systems from Figure 1 (b). By construction, among places $\{(q, v) | q \in Q_{\lambda(v)}\}$ for any $v$, there is exactly one token in all reachable markings because $\lambda(v)$ is automata-like. By extension we say that such behaviors are automata-like.

A parameterized system $S = \{S_1, S_2, \dots\}$ is a possibly infinite set of systems, called instances. A parameterized system has an infinite set of behaviors, denoted as $\beta(S)$, i.e., one for each instance. The verification problems considered in this paper are, given a parameterized system $S$ and a marking $m$ for a subset $Q$ of the places in $\mathcal{P}$, does there exist an instance of $S$ whose behavior reaches (covers) a marking that agrees with $m$ over $Q$? We shall define these problems formally, once we have introduced the language for the specification of parameterized systems.
## 2.3 Algebras

We recall a few notions on algebras needed in the following. A *signature* is a set of function symbols $F = \{\text{op}_1, \text{op}_2, \dots\}$. An *F-term* is a term built with function symbols from $F$ and variables of arity zero. An *F-term* is *ground* if it has no variables. An *F-algebra* $\mathcal{A} = (\mathcal{A}, \text{op}_1^{\mathcal{A}}, \text{op}_2^{\mathcal{A}}, \dots)$ interprets the function symbols from $F$ as functions over the *domain* $\mathcal{A}$. Given F-algebras $\mathcal{A}$ and $\mathcal{B}$ having domains $\mathcal{A}$ and $\mathcal{B}$, respectively, a *homomorphism* is a function $h : \mathcal{A} \to \mathcal{B}$ such that $h(\text{op}^{\mathcal{A}}(a_1, \dots, a_n)) = \text{op}^{\mathcal{B}}(h(a_1), \dots, h(a_n))$, for each function symbol $\text{op} \in \text{F}$ of arity $n$ and $a_1, \dots, a_n \in \mathcal{A}$. The *kernel* of a function $f : \mathcal{A} \to \mathcal{B}$ is the equivalence relation $\sim_{\ker(f)} \subseteq \mathcal{A} \times \mathcal{A}$ defined as $a_1 \sim_{\ker(f)} a_2 \iff f(a_1) = f(a_2)$. An equivalence relation $\sim \subseteq \mathcal{A} \times \mathcal{A}$ is an *F-congruence* if and only if, for each function symbol $\text{op} \in \text{F}$ of arity $n$ and $a_1, a'_1, \dots, a_n, a'_n \in \mathcal{A}$ such that $a_i \sim a'_i$, for all $i \in [1, n]$, we have $\text{op}^{\mathcal{A}}(a_1, \dots, a_n) \sim \text{op}^{\mathcal{A}}(a'_1, \dots, a'_n)$.

**Proposition 1.** Let $\mathcal{A}$ be an F-algebra having domain $\mathcal{A}$, and $f : \mathcal{A} \to \mathcal{B}$ be a function such that $\sim_{\ker(f)}$ is an F-congruence. Then $f$ is a homomorphism between $\mathcal{A}$ and $\mathcal{B} \stackrel{\text{def}}{=} (f(\mathcal{A}), \{\text{op}^{\mathcal{B}}\}_{\text{op}\in\text{F}})$, where $\text{op}^{\mathcal{B}}(b_1, \dots, b_n) \stackrel{\text{def}}{=} f(\text{op}^{\mathcal{A}}(f^{-1}(b_1), \dots, f^{-1}(b_n)))^4$, for each function symbol $\text{op} \in \text{F}$ of arity $n$ and all $b_1, \dots, b_n \in f(\mathcal{A})$. Consequently, $f(\theta^{\mathcal{A}}) = \theta^{\mathcal{B}}$, for each ground F-term $\theta$.

We introduce a standard signature of operations on graphs and define two algebras, of open systems and behaviors. Let $\Sigma$ be a countably infinite set of *source labels*, fixed in the rest of the paper. With no loss of generality, we assume that $\Sigma$ is partitioned into disjoint sets indexed by the process types $\mathcal{P} = \{p_1, \dots, p_k\}$, i.e., $\Sigma = \Sigma_{p_1} \uplus \dots \uplus \Sigma_{p_k}$. A *source label* $\sigma \in \Sigma$ uniquely identifies a process type $\text{>Type}(\sigma) \in \mathcal{P}$ such that $\sigma \in \Sigma_{\text{>Type}(\sigma)}$. A function $\alpha : \Sigma \to \Sigma$ is *P-preserving* if $\text{>Type}(\alpha(\sigma)) = \text{>Type}(\sigma)$, for all $\sigma \in \Sigma$.

The signature of the *hyperedge-replacement graph algebra (HR)* [17] consists of the constants $a_{\sigma_1}, a_{\sigma_2}$, for all edge labels $a \in \Delta$ and source labels $\sigma_1, \sigma_2 \in \Sigma$, the unary symbols $\text{ restrict}_{\tau}$, for all $\tau \subseteq_{\text{fin}} \Sigma$, rename$_\alpha$, for all $\mathcal{P}$-preserving finite permutations $\alpha : \Sigma \to \Sigma$ and the binary symbol $\oplus$. By HR congruence we mean an equivalence relation that is a congruence for the HR signature.

An *open system* is a pair $\check{S} \stackrel{\text{def}}{=} (S, \xi)$, where $S = (V, E, \lambda)$ is a system and $\xi : \Sigma \to_S V_S$ is an injective partial function that assigns source labels to vertices of $S$ such that $\text{>Type}(\sigma) = \lambda(\xi(\sigma))$, for each $\sigma \in \text{dom}(\xi)$, i.e., the source label of a vertex has the process type of that vertex. We say that a vertex $v \in V_S$ is the $\sigma$-source of $\check{S}$ if $\xi(\sigma) = v$. The *type* of $\check{S}$ is $\text{>Type}(\check{S}) \stackrel{\text{def}}{=} \text{dom}(\xi)$, i.e., the set of source labels that occurs in $S$. Since systems (Definition 2) are in fact open systems of empty type, we blur the distinction and refer to open systems as systems from now on.

The algebra $\mathcal{S}$ (Figure 2) interprets the HR signature over the set $\mathcal{S}$ of systems:

- $a_{\sigma_1, \sigma_2}^{\mathcal{S}}$ is the system having a single $a$-labeled edge between its two vertices labeled with process types $\text{>Type}(\sigma_1)$ and $\text{>Type}(\sigma_2)$, that are the $\sigma_1$- and $\sigma_2$-sources, respectively, for each edge label $a \in \Delta$ and source labels $\sigma_1, \sigma_2 \in \Sigma$.

- $\text{ restrict}_{\tau}^{\mathcal{S}}(S, \xi) \stackrel{\text{def}}{=} (S, \xi|_{\tau})$ removes the source labels that are not in $\tau \subseteq_{\text{fin}} \Sigma$,

<footnote n="4">⁴ The right-hand side of this definition is a singleton that we identify with its element.</footnote>
<figure><img src="image_5.png" /><figcaption>**Fig. 2.** Homomorphisms between the HR algebras used in this paper. The circled algebras are the finite and effectively computable ones.</figcaption></figure>

- rename$\alpha(S, \xi) \stackrel{\text{def}}{=} (S, \xi \circ \alpha^{-1})$ relabels the sources according to $\alpha$; note that $\xi \circ \alpha^{-1}$ is an injective partial mapping, since $\alpha$ is a finite permutation of $\Sigma$,

- $(S_1, \xi_1) \oplus^S (S_2, \xi_2)$ is the disjoint union of $(S_1, \xi_1)$ and $(S_2, \xi_2)$, followed by:

* fusion of each pair of common $\sigma$-sources $v_i \in V_{S_i}$, for $\sigma \in \text{type}(S_1) \cap \text{type}(S_2)$ and $i = 1, 2$, into a $\sigma$-source labeled with ptype($\sigma$),

* fusion of all identical edges into a single edge with the same label and endpoints.

Every other HR algebra considered in the rest of this paper will be defined from $\mathcal{S}$ via an homomorphism. Figure 2 shows the diagram of these algebras and homomorphisms. Each such homomorphism $h$ (except for $\psi$, which has a trivial definition) has a reference to a lemma proving that $\sim_{\text{ker}(h)}$ is an HR congruence.

An open behavior is a pair $\mathcal{N} \stackrel{\text{def}}{=} (\mathcal{N}, \xi)$, where $\mathcal{N}$ is a behavior and $\xi : \Sigma \times Q_P \to_{\text{fin}} Q_{\mathcal{N}}$ is an injective partial function assigning pairs $(\sigma, q)$ to places of $\mathcal{N}$, where $\sigma$ is a source label and $q$ is a place from some process type in $\mathcal{P}$. A place $r \in Q_{\mathcal{N}}$ is a $(\sigma, q)$-source of $\mathcal{N}$ if $\xi(\sigma, q) = r$ and type($\mathcal{N}$) $\stackrel{\text{def}}{=} \text{dom}(\xi)$ denotes the type of $\mathcal{N}$. Since behaviors (Definition 3) are actually open behaviors of empty type, we blur the distinction and refer to open behaviors as behaviors, when no confusion arises.

To define the algebra of behaviors, we extend the $\beta$ function introduced by Definition 3 to (open) systems, as follows. The behavior of the system $\tilde{S} = (S, \xi)$ is $\beta(\tilde{S}) \stackrel{\text{def}}{=} (\beta(S), \tilde{\xi})$, where $\beta(S)$ is given in Definition 3 and the source labeling $\tilde{\xi}$ is $\tilde{\xi}(\sigma, q) \stackrel{\text{def}}{=} (q, \xi(\sigma))$ if $\xi(\sigma)$ is defined and $(q, \xi(\sigma)) \in Q_{\mathcal{N}}$, and undefined otherwise, for all $\sigma \in \Sigma$ and $q \in Q_P$.

**Lemma 1.** $\sim_{\text{ker}(\beta)}$ is a HR congruence.

We introduce an algebra $\mathcal{B}$ of behaviors (Figure 2), whose domain and interpretation of HR function symbols are defined as in Proposition 1. Since $\sim_{\text{ker}(\beta)}$ is a HR congruence (Lemma 1), it follows that $\beta$ is a homomorphism between $\mathcal{S}$ and $\mathcal{B}$. As we discuss next, a grammar that describes a parameterized system $S = \{S_1, S_2, \dots\}$ can be reused to describe its set of behaviors $\beta(S)$.

## 2.4 Grammars

A *grammar* over a signature $\mathcal{F}$ 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 \rho[X_1, \dots, X_n]$, where $X, X_1, \dots, X_n \in \Xi$ are nonterminals and $\rho$ is an F-term whose only variables are $X_1, \dots, X_n$, or (2) $X \to \mathcal{F}$, where $\mathcal{F} \in \Xi$; the rules of this form are called *axioms*. Given 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 $\rho$, for some rule $X \to \rho$ of $\Gamma$. An *X-derivation* is a sequence of steps
starting with a nonterminal X. The derivation is complete if it ends in a ground term.
Let $\mathcal{L}_X^\mathcal{A}(\Gamma) \stackrel{\text{def}}{=} \{\theta^\mathcal{A} | X \Rightarrow_\Gamma^* \theta \text{ is a complete derivation}\}$ and $\mathcal{L}^\mathcal{A}(\Gamma) \stackrel{\text{def}}{=} \bigcup_{X \in \Pi} \mathcal{L}_X^\mathcal{A}(\Gamma)$ be
the language of $\Gamma$ in the algebra $\mathcal{A}$.

The following result, also known as the Filtering Theorem, allows to build a grammar for the intersection between the language of a grammar and a recognizable set, i.e., the image of a finite set via an inverse homomorphism [17, Theorem 3.88]:

**Theorem 1.** Let $\mathbb{F} = \{\text{op}_1, \text{op}_2, \dots\}$ be a signature, $\mathcal{A} = (\mathcal{A}, \text{op}_1^\mathcal{A}, \text{op}_2^\mathcal{A}, \dots)$ and $\mathbb{B} = (\mathbb{B}, \text{op}_1^\mathbb{B}, \text{op}_2^\mathbb{B}, \dots)$ be $\mathbb{F}$-algebras, such that $\mathbb{B}$ is finite, and $h$ be a homomorphism between $\mathcal{A}$ and $\mathbb{B}$. For each $\mathbb{F}$-grammar $\Gamma$ and set $C \subseteq \mathbb{B}$, one can build a grammar $\Gamma_{h,C}$ such that $\mathcal{L}^\mathcal{A}(\Gamma_{h,C}) = \mathcal{L}^\mathcal{A}(\Gamma) \cap h^{-1}(C)$.

The construction of the filtered grammar $\Gamma_{h,C}$ is effective: for each rule $X \to \rho[X_1, \dots, X_n]$ of $\Gamma$ and each sequence of elements $b, b_1, \dots, b_n \in \mathbb{B}$ such that $b = \rho^\mathcal{B}(b_1, \dots, b_n)$, the grammar $\Gamma_{h,C}$ has a rule $X^b \to \rho[X_1^{b_1}, \dots, X_n^{b_n}]$; the axioms of $\Gamma_{h,C}$ are $\to X^c$, for each axiom $\to X$ of $\Gamma$ and each element $c \in C$.

The grammars from the rest of the paper use the $\mathbb{H}\mathbb{R}$ signature to describe parameterized systems. The following example shows two grammars that specify parameterized systems with chain-like and star-like network topologies, as in Figure 1 (b):

**Example 3.** The grammar $\Gamma_{Chain}$ below defines systems with chain-like network topologies and at least three processes including the controller (Figure 1 (b) top):

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

The right-hand sides of the last two rules correspond to the graphs on the right. Similarly, the $\Gamma_{Star}$ grammar below defines systems with star-shaped network topology and at least two processes including the controller (Figure 1 (b) bottom):

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

The following argument will be repeated several times: if $\mathcal{A}$ is some $\mathbb{H}\mathbb{R}$ algebra related to $\mathcal{S}$ by a homomorphism $h$, then $h(\mathcal{L}^\mathcal{S}(\Gamma)) = \mathcal{L}^\mathcal{A}(\Gamma)$, for each grammar $\Gamma$ written using the $\mathbb{H}\mathbb{R}$ signature. Moreover, if the domain of $\mathcal{A}$ is finite, the language $\mathcal{L}^\mathcal{A}(\Gamma)$ is finite and effectively computable by a finite Kleene iteration, provided that the interpretation of each function symbol from the $\mathbb{H}\mathbb{R}$ signature in $\mathcal{A}$ is effectively computable. The finite and effectively computable algebras in question are circled in Figure 2.

As a consequence of Lemma 1, a grammar that specifies a parameterized system defines also its set of behaviors:

**Lemma 2.** For each $\mathbb{H}\mathbb{R}$ grammar $\Gamma$, we have $\beta(\mathcal{L}^\mathcal{S}(\Gamma)) = \mathcal{L}^\mathcal{B}(\Gamma)$.
We consider the problems of reachability and coverability for parameterized systems specified by grammars and give the formal definitions of the decision problems:

**Definition 4.** The Reach($\Gamma$, $Q$, $m$) (resp. Cover($\Gamma$, $Q$, $m$)) problem takes in input a grammar $\Gamma$, a set of places $Q \subseteq Q_P$, a mapping $m: Q \to \mathbb{N}$ and asks for the existence of a system $S \in \mathcal{L}^S(\Gamma)$ and marking $\bar{m} \in \text{reach}(\beta(S))$ (resp. $\bar{m} \in \text{cover}(\beta(S)))$ where $\sum_{v \in V_S: q \in Q_{\lambda_S(v)}} \bar{m}(q, v) = m(q)$, for all $q \in Q$.

Unsurprisingly, both problems are undecidable, even for simple grammars defining parameterized systems with chain-like topologies (see Example 3), when the structure of the process types is unrestricted.

**Theorem 2.** *The Reach and Cover problems are undecidable.*

*Proof sketch.* With 3 process types one can write a grammar whose language consists of nets that simulate executions of two-counter Minsky machines, and the halting problem thus reduces to coverability. $\square$

# 3 Counting Abstraction

We define the *counting abstraction* of a set of behaviors as a set of PNs having finitely many underlying nets with possibly infinitely many initial markings each. The basic idea is to fold (i) the copies of the same place from some process type into a single place and (ii) the transitions having the same sets of predecessors and successors into a single transition. We show that the counting abstraction of the set of behaviors of a parameterized system described by an HR grammar can be computed by evaluating the same grammar in a finite HR algebra. Moreover, the infinite set of initial markings of a folded PN can be finitely described by another PN derived from the initial grammar describing the system. While the counting abstraction itself is not inherently tied to HR, and may abstract any family, the generation of initial markings on the other hand is strongly based on the HR-grammar (Section 3.2).

## 3.1 Folding

We define a folding function on the domain $\mathbb{B}$ of system behaviors. Let $\check{S} = (S, \xi)$ be a system and $(\mathcal{N}, \xi) = \beta(\check{S})$ be its behavior (Definition 3). The folding is defined as quotienting a behavior $\mathcal{N}$ via an equivalence relation $\equiv$ on the places of $\mathcal{N}$. Note that quotienting is a standard operation, meaning that equivalent places and transitions having the same sets of predecessor and successor equivalence classes $[q]_{\equiv}$, for $q \in Q_{\mathcal{N}}$, are joined together, the result being denoted as $\mathcal{N}_{/\equiv}$.

We recall that the places of $\mathcal{N}$ are pairs $(q, v)$, where $q \in Q_P$, $v \in V_S$ and the sources of the behavior are labeled by the function $\xi$. A function $\eta: \Sigma \to V_S$, having $\text{dom}(\eta) \supseteq \text{dom}(\xi)$, defines the following equivalence relation $\equiv_{[\eta]} \subseteq Q_{\mathcal{N}} \times Q_{\mathcal{N}}$:

$$ (q_1, v_1) \equiv_{[\eta]} (q_2, v_2) \iff q_1 = q_2 \text{ and } \{v_1, v_2\} \cap \text{img}(\eta) \neq \emptyset \Rightarrow v_1 = v_2 \quad (1) $$
<figure><img src="image_8.png" /><figcaption>Fig. 3. Foldings of the behaviors given in Figure 1 (c) and (d), respectively.</figcaption></figure>

i.e., two places of $\mathcal{N}$ corresponding to the same place of a process type (within two distinct instances thereof) are considered equivalent, except for the sources with labels $\eta$, that are equivalent only with themselves. The equivalence class of a place $(q, v) \in Q_{\mathcal{N}}$ is denoted $[(q, v)]_{\equiv_{\eta}}$. Because we have assumed that the set of places corresponding to different process types are disjoint, $(q_1, v_1) \equiv_{[\xi]} (q_2, v_2)$ implies that $\lambda_S(v_1) = \lambda_S(v_2)$, i.e., the two vertices are instances of the same process type.

The folding of $(\mathcal{N}, \bar{\xi})$ is defined as $\phi(\mathcal{N}, \bar{\xi}) \stackrel{\text{def}}{=} (\mathcal{N}_{/\equiv_{[\xi]}}, \bar{\xi}_{/\equiv_{[\xi]}})$, where, for each mapping $\eta: \Sigma \to V_S$ having $\text{dom}(\eta) \supseteq \text{dom}(\xi)$, we define $\bar{\xi}_{/\equiv_{[\eta]}}(\sigma, [q]_{\equiv_{[\eta]}}) \stackrel{\text{def}}{=} [\bar{\xi}(\sigma, q)]_{\equiv_{[\eta]}}$ if $\sigma \in \text{dom}(\eta)$, else undefined, for each $\sigma \in \Sigma$. We refer to Figure 3 for examples.

The following lemma allows to define an algebra of abstract behaviors $\mathcal{B}^\sharp$ (Figure 2) from the algebra $\mathcal{B}$ of behaviors, using Proposition 1. The domain of $\mathcal{B}^\sharp$ is the set $\mathcal{B}^\sharp$ of folded behaviors, i.e., quotients of behaviors $(\mathcal{N}, \bar{\xi})$ w.r.t. the $\equiv_{[\xi]}$ relation.

**Lemma 3.** *$\sim_{\text{ker}(\phi)}$ is an HR congruence.*

As an immediate consequence of Lemma 3, we obtain that $\phi$ is a homomorphism between $\mathcal{B}$ and $\mathcal{B}^\sharp$, hence the same HR grammar can be used to both specify an infinite set of behaviors and compute its folded abstraction:

**Corollary 1.** For each HR grammar $\Gamma$, we have $\phi(\mathcal{L}^\Gamma(\Gamma)) = \mathcal{L}^{\mathcal{B}^\sharp}(\Gamma)$.

Because $\mathcal{P}$ is a finite set of process types, each having finitely many places, the folded language $\mathcal{L}^{\mathcal{B}^\sharp}(\Gamma)$ has a finite set of underlying nets. This is because each transition $t$ in a behavior $\mathcal{N} \in \mathcal{L}^\Gamma(\Gamma)$ has at most two incoming/outgoing edges. Since the same holds for each transition of its quotient, i.e., $\mathcal{N}_{/\equiv_{[\xi]}}$, there are finitely many places and transitions in each underlying net of some $\mathcal{N} \in \mathcal{L}^{\mathcal{B}^\sharp}(\Gamma)$. Nevertheless, the language $\mathcal{L}^{\mathcal{B}^\sharp}(\Gamma)$ is unbounded, because the set of initial markings is unbounded. In order to represent this set in a finite way, we shall proceed in two steps:

1. Isolate the initial markings that correspond to a given net from $\mathcal{L}^{\mathcal{B}^\sharp}(\Gamma)$; we address this problem using the Filtering Theorem (Theorem 1).

2. Give a finite representation to the set of initial markings of each net; we tackle this problem using Esparza's idea [18] of building PNs that simulate the derivations of the "filtered" grammars obtained in the previous step.

To formally define the finite set of underlying nets from a language $\mathcal{L}^{\mathcal{B}^\sharp}(\Gamma)$, we consider the function $\psi$ on the domain $\mathcal{B}^\sharp$, that drops the initial marking:

$$ \psi((N, m_0), \xi) \stackrel{\text{def}}{=} (N, \bar{\xi}) \qquad (2) $$
Then, $\psi(\mathcal{L}^{\mathcal{B}^\sharp}(\Gamma))$ is finite, because the numbers of places and transitions in each net from this set are bounded by $\|Q_P\|$ and $\|Q_P\|^4$ (i.e., each transition has at most 2 incoming and 2 outgoing edges of weight 1), respectively.

Since none of the operations from $\mathcal{B}^\sharp$ modify the initial markings, it is straightforward that $\sim_{\ker(\psi)}$ is a HR congruence. We define the algebra $\mathcal{B}^\flat$ (Figure 2) having the finite domain $\mathcal{B}^\flat \stackrel{\text{def}}{=} \psi(\mathcal{B}^\sharp)$ and the usual interpretations of the HR function symbols given by Proposition 1. By standard arguments (similar to Lemma 2 and Corollary 1), we obtain that $\psi$ is a homomorphism between $\mathcal{B}^\sharp$ and $\mathcal{B}^\flat$, i.e., $\psi(\mathcal{L}^{\mathcal{B}^\sharp}(\Gamma)) = \mathcal{L}^{\mathcal{B}^\flat}(\Gamma)$.

As previously discussed, $\mathcal{L}^{\mathcal{B}^\flat}(\Gamma)$ is a finite set. However, to ensure that this set can be effectively computed, the computation of the interpretation of the HR signature in $\mathcal{B}^\flat$ needs to be effective:

**Proposition 2.** For each function symbol $\text{op}$ from the HR signature, the function $\text{op}^{\mathcal{B}^\flat}$ is effectively computable.

By the previous arguments, the language $\mathcal{L}^{\mathcal{B}^\flat}(\Gamma)$ is finite and effectively computable, hence it can be produced by a finite Kleene iteration of the monotonic function that maps a tuple of sets indexed by the nonterminals of $\Gamma$ into their $\mathcal{B}^\flat$ interpretations, given by the rules of $\Gamma$. Let $\{(N_1, \bar{\xi}_1), \dots, (N_n, \bar{\xi}_n)\} \stackrel{\text{def}}{=} \mathcal{L}^{\mathcal{B}^\flat}(\Gamma)$ be this set. Using the Filtering Theorem (Theorem 1) one can effectively build grammars $\Gamma_1, \dots, \Gamma_n$ such that:

$$ \psi(\mathcal{L}^{\mathcal{B}^\sharp}(\Gamma_i)) = \mathcal{L}^{\mathcal{B}^\flat}(\Gamma_i) = \{(N_i, \bar{\xi}_i)\}, \text{ for each } i \in [1, n] \quad (3) $$

More precisely, the Filtering Theorem gives, for each $i \in [1, n]$, a grammar $\Gamma_i$ such that $\mathcal{L}^{\mathcal{B}^\sharp}(\Gamma_i) = \mathcal{L}^{\mathcal{B}^\flat}(\Gamma) \cap \psi^{-1}(\{(N_i, \bar{\xi}_i)\})$. By applying $\psi$ to both sides of the equality, we obtain (Equation 3), thus taking care of the first step of the construction (1).

## 3.2 Initial Markings

Let $\Gamma = (\Xi, \Pi)$ be any of the grammars $\Gamma_1, \dots, \Gamma_n$ (Equation 3). To simplify matters at hand, we assume w.l.o.g that the right-hand side of each rule in $\Gamma$ has exactly one occurrence of an HR function symbol, i.e., a constant $a_{\sigma_1, \sigma_2}$, a unary function symbol $\text{restrict}_\tau$ or $\text{rename}_\alpha$, or the binary function symbol $\oplus$, applied to 0, 1 or 2 variables, respectively. Note that each grammar can be put in this form, at the cost of adding polynomially many extra nonterminals.

First, we annotate each nonterminal $X \in \Xi$ with sets of sources $\tau$ that are visible (i.e., have been introduced by a constant $a_{\sigma_1, \sigma_2}$ and have not been removed by some application of $\text{restrict}_\tau$) in each complete derivation starting in $X^\tau$, where $X^\tau$ is a short-hand for the pair $(X, \tau)$. The annotated grammar $\hat{\Gamma} = (\hat{\Xi}, \hat{\Pi})$ can be built from $\Gamma$ by a standard worklist iteration<fnref n="5" /> The language of the annotated grammar $\hat{\Gamma}$ is the same as the original grammar $\Gamma$. Next, we use the annotated grammar $\hat{\Gamma} = (\hat{\Xi}, \hat{\Pi})$, to build a PN $\mathcal{J}(\hat{\Gamma})$ that generates the initial markings of $\Gamma$ in the set of folded PNs (Corollary 1).

This construction is quite intuitive: by reinterpreting each rule of $\hat{\Gamma}$ as a transition of $\mathcal{J}(\hat{\Gamma})$, we get a PN whose firing sequences mimick derivations of $\hat{\Gamma}$ in which the

<footnote n="5">⁵ The annotation algorithm is given in the full version of the paper. [10]</footnote>
<figure><img src="image_9.png" /><figcaption>**Fig. 4.** $\mathcal{J}(\hat{\Gamma}_{Chain})$ (left) and $\mathcal{J}(\hat{\Gamma}_{Star})$ (right), showing how to initialize the marking of stars and chains generated by the grammars presented in Example 3.</figcaption></figure>

rules/transitions of $\hat{\Gamma}$ and $\mathcal{J}(\hat{\Gamma})$ are applied in the same order. More precisely, we create a Petri net with one place representing each nonterminal $X \in \Xi$, in which each rule of the form $X \to \rho[X_1, ..., X_n]$ is translated to some transition $t$ such that $\bullet t^* = (X, \{X_1, ..., X_n\})$, and each rule of the form $X \to \rho$ is translated to some transition $t$ such that $\bullet t^* = (O, X)$ (here $O \notin \Xi$ is a newly created place that receives the initial token, as in Figure 4). This construction is such that a partial derivation having $k$ occurrences of the nonterminal variable $X$, when reinterpreted as a firing sequence, leads to a marking with $k$ tokens in the place corresponding to $X$. Assume that $X^\tau \Rightarrow^* \hat{\Gamma}^\tau$ $\theta$ is a complete derivation, i.e., $\theta$ is a ground HR term. Then, every instance of some process type $p$ that occurs in the system $(S, \xi) \stackrel{\text{def}}{=} \theta^S$ starts in a vertex labeled by a source label $\sigma \in \Sigma$ such that, either:

(a) $\sigma$ is removed by an application of $\text{restrict}_{\tau'}$ such that $\sigma \notin \tau'$, then $\sigma$ occurs in the subtree of $\theta$ rooted at the particular occurrence of $\text{restrict}_{\tau'}$ that removed it, or

(b) $\sigma$ is visible at the root of $\theta$, i.e., $\sigma \in \tau$.

When processing the rules of the form $X^\tau \to \text{restrict}_{\tau'}(X_1^{\tau_1})$ and $\to X^\tau$ in the construction of $\mathcal{J}(\hat{\Gamma})$, we add an outgoing edge to each place $q$ that is initially marked in $\text{ptype}(\sigma)$, for some $\sigma \in \tau_1 \setminus \tau'$ or $\sigma \in \tau$. Then, for every instance of the process type that occurs in the system, its initial marking will be added to $q$ by a firing sequence of $\mathcal{J}(\hat{\Gamma})$. We refer to Figure 4 for examples of initialization PNs obtained by this construction applied to $\hat{\Gamma}_{Chain}$ and $\hat{\Gamma}_{Star}$, i.e., the annotated versions of the two grammars from Example 3. For a PN $\mathcal{N}$ and a set of places $Q \subseteq Q_{\mathcal{N}}$, we denote by:

$$ \text{reach}_{\mathcal{Q}}^{0}(\mathcal{N}) \stackrel{\text{def}}{=} \{m \in \text{reach}(\mathcal{N}) \mid m(q) = 0, \text{ for all } q \in Q\} \quad (4) $$

the set of reachable markings having zero tokens in a place from $Q$. For a set $\mathcal{M}$ of markings and a set $Q$ of places, we denote by $\mathcal{M} \downarrow_Q$ the set of restrictions of each $m \in \mathcal{M}$ to the places in $Q$. The relation between the set of folded PNs described by an annotated grammar $\hat{\Gamma}$ and the PN $\mathcal{J}(\hat{\Gamma})$ is formally captured below:

**Lemma 4.** Let $\hat{\Gamma} = (\Xi, \hat{\Pi})$ be an annotated grammar. Then, we have:

$$ \{\text{init}_{\mathcal{N}} \mid (\mathcal{N}, \xi) \in \mathcal{L}^{\mathcal{B}^*}(\hat{\Gamma})\} = \text{reach}_{\{O\} \cup \Xi}^{0}(\mathcal{J}(\hat{\Gamma})) \downarrow_{Q_{\mathcal{N}}} $$
## 3.3 Soundness

We now have all the elements to describe our counting abstraction method and prove its soundness, i.e., if the reachability (resp. coverability) problem has a negative answer for the abstraction, then the concrete reachability (resp. coverability) problem has a negative answer.

For each grammar $\Gamma_i = (\Xi_i, \Pi_i)$ defined at (Equation 3), that corresponds to the (open) net $(N_i, \xi_i)$, for $i \in [1, n]$, we define the PN $\mathfrak{N}(\Gamma_i) \stackrel{\text{def}}{=} (\mathcal{N}_i, \xi_i)$, where:

$$Q_{\mathcal{N}_i} \stackrel{\text{def}}{=} Q_{\mathfrak{J}(\hat{\Gamma}_i)} \cup Q_{N_i} \quad T_{\mathcal{N}_i} \stackrel{\text{def}}{=} T_{\mathfrak{J}(\hat{\Gamma}_i)} \uplus T_{N_i} \quad W_{\mathcal{N}_i} \stackrel{\text{def}}{=} W_{\mathfrak{J}(\hat{\Gamma}_i)} \cup W_{N_i} \quad \text{init}_{\mathcal{N}_i} \stackrel{\text{def}}{=} \text{init}_{\mathfrak{J}(\hat{\Gamma}_i)}$$

Note that $\text{reach}^0_{Q_{\mathfrak{J}(\hat{\Gamma}_i)} \setminus Q_{N_i}}(\mathfrak{N}(\Gamma_i))$ is the set of markings of $\mathfrak{N}(\Gamma_i)$ that can be reached after the full generation of its initial marking, i.e., from those markings that have no more tokens in any of the places of $\mathfrak{J}(\hat{\Gamma}_i)$, excepted the initially marked places of $Q_P$.

Our verification method for the grammar-based parameterized reachability and coverability problems (Definition 4) relies on the construction of a finite number of PNs $\mathfrak{N}(\Gamma_1), \dots, \mathfrak{N}(\Gamma_n)$ from a given grammar $\Gamma$ that describes a set of systems.

The soundness of the method is formally captured below:

**Theorem 3.** Let $\Gamma$ be an HR grammar such that $\mathcal{L}^{\mathfrak{B}}(\Gamma) = \{(N_1, \xi_1), \dots, (N_n, \xi_n)\}$, $Q \subseteq Q_P$ a set of places, $m: Q \to \mathbb{N}$ a mapping. Then, one can effectively build grammars $\Gamma_1, \dots, \Gamma_n$ such that $\mathcal{L}^{\mathfrak{B}}(\Gamma_i) = \{(N_i, \xi_i)\}$, for all $i \in [1, n]$ and:

1. Reach($\Gamma$, $Q$, $m$) has a negative answer if $m \notin \bigcup_{i=1}^n \text{reach}^0_{Q_{\mathfrak{N}(\Gamma_i)} \setminus Q_P}(\mathfrak{N}(\Gamma_i)) \downarrow_Q$.

2. Cover($\Gamma$, $Q$, $m$) has a negative answer if $m \notin \bigcup_{i=1}^n \text{cover}(\mathfrak{N}(\Gamma_i)) \downarrow_Q$.

Note that, if Reach($\Gamma$, $Q$, $m$) (resp. Cover($\Gamma$, $Q$, $m$)) has a negative answer, then each instance the parameterized system described by $\Gamma$ (i.e., the set of systems $\mathcal{L}^S(\Gamma)$) is safe with respect to the property encoded by the marking $m$, i.e., does not reach (resp. cover) the marking $m$ over the set of places $Q$. For instance, mutual exclusion (only one process of a certain type in a certain state) is naturally encoded as a coverability problem.

## 3.4 False Positives

As we have announced, our abstraction is sound but not complete. Before we explore a decidable fragment, we show here a simple example of a net on which false positives appear (i.e., the abstraction exhibits a violation of safety, but the original net is safe).

Figure 5 illustrates one phenomenon that is a possible cause of false positives. Here, the folding changes the connectivity of the network: two instances of $p_b$ are folded together and make a path from $p_a$ to $p_c$ appear that was absent from the original system. The coverability query $m_{\text{tgt}}(q_c^1) \ge 1$ is unsatisfiable in $\theta^{\mathcal{B}}$, but satisfiable in $\theta^{\mathcal{B}^2}$.

To enable the verification of infinite systems that exhibit a similar issue, here is one possible approach. We give ourselves a new process type $p'_b$, identical copy of $p_b$, and we alter the grammar and/or the assignment ptype(·) to distinguish between the instances we do not want folded together. Here we could change ptype($\sigma'_b$) = $p_b'$ (instead of $p_b$). The same abstraction applied to the new system will not fold together
<figure><img src="image_10.png" /><figcaption>**Fig. 5.** 3 process types with the same net, and a way of connecting them that produces a false positive when folded. $\theta \stackrel{\text{def}}{=} (t^+, t^+)^{\sigma_a, \sigma_b} \oplus (t^-, t^+)^{\sigma'_a, \sigma'_b}$ with ptype$(\sigma_a) = p_a$, ptype$(\sigma_b) = ptype(\sigma'_b) = p_b$, ptype$(\sigma_c) = p_c$. The safety property is $m_{\text{tgt}}(q_c^1) \ge 1$.</figcaption></figure>

instances of $p_b$ with instances of $p'_b$, making the false positive disappear. In general on infinite families, we may modify the grammar to select a subset of instances of a process type to instead use a copy of the process type that is folded separately. Repeating this process finitely many times keeps the abstraction finite. This refinement technique constitute what we call a *partial unfolding*, because we select a few instances to not be folded with the rest. Automated detection of when this technique is applicable, and more advanced transformations of the grammar constitute a research avenue orthogonal to the abstraction technique we explore here, and may be the topic of future work.

# 4 A Decidable Fragment

We have shown that the parameterized coverability problem is undecidable, for systems with fairly simple network topologies (chains) and unrestricted process types (Theorem 2). We refine this result by proving that only restricting the process types, but not the topology of the network, suffices to recover decidability. This approach is inspired by [5], in which *token-passing systems (TPS)* are found to admit cutoffs, and thus decidable model-checking, provided that the architecture is definable in monadic second order logic and of bounded tree-width, like ours. TPS and PPS are similar, with the tradeoff that TPS may have internal transitions, but only one token in the system.

Albeit based on a simple communication pattern (i.e., passing a pebble from one node to a neighbour having no pebble), our decidable fragment is non-trivial: we found it to be in 2EXPTIME, with a PSPACE-hard lower bound.

## 4.1 Pebble-Passing Systems

The class of pebble-passing systems (PPS) is defined by restricting the process types and interactions of a system, as in Figure 6. The example from Figure 5 also happens to be of this form. We give the formal definition below:

**Definition 5.** Let $\mathcal{P}_{\text{pps}}$ be a set of process types, where $Q_p = \{q_p^\perp, q_p^\parallel\}$ and $T_p = T_p^{\text{obs}} = \{\text{send}, \text{recv}\}$, such that $\bullet \text{send}^* = (q_p^\perp, q_p^\parallel)$ and $\bullet \text{recv}^* = (q_p^\parallel, q_p^\perp)$, for each $p \in \mathcal{P}_{\text{pps}}$. Let $\Delta_{\text{pps}} \stackrel{\text{def}}{=} \{(\text{send}, \text{recv}), (\text{recv}, \text{send})\}$ be a set of edge labels. A system $S = (V, E, \lambda)$ over $\mathcal{P}_{\text{pps}}$ and $\Delta_{\text{pps}}$ is said to be pebble-passing.
<figure><img src="image_11.png" /><figcaption>**Fig. 6.** Two process types (left), and two kinds of interactions (right), which all other process types and interactions in our restriction have the same shape as.</figcaption></figure>

Intuitively, a token in $q_{\perp}^{p}$ (i.e., $m(q_{\perp}^{p}) = 1$) represents the ownership of a ressource, called pebble, and a token in $q_{\perp}^{p}$ is the absence of a pebble, called hole. Since each process type is automata-like (i.e., has a token in exactly one place), each node of the system can have either a pebble or a hole, in all the reachable markings of its behavior (Definition 3). An edge $(v, (send, recv), v')$ (*resp.* $(v, (recv, send), v')$) will be denoted $v \to v'$ (*resp.* $v' \to v$). Intuitively, firing an interaction $v \to v'$ moves a pebble from $v$ to $v'$ and simultaneously moves a hole from $v'$ to $v$. Thus each transition preserves the total numbers of pebbles and holes in the system, respectively.

Pebble-passing systems have very strict constraints on their process types and interactions, but no constraints on the set of network topologies, other than that it is definable by an HR grammar written with constants of the form $(send, recv)_{\sigma_1, \sigma_2}$ or $(recv, send)_{\sigma_1, \sigma_2}$, for some source labels $\sigma_1, \sigma_2 \in \Sigma$, where $\Sigma$ is the set of source labels that may occur in a grammar. We denote by $\text{HR}_{\text{pps}}$ the signature of these grammars. The rest of this section is concerned with the proof of the following theorem:

**Theorem 4.** *The Cover problem for grammars written using the $\text{HR}_{\text{pps}}$ signature is in $2\text{EXPTIME}$ and $\text{PSPACE}$-hard.*

The proof of Theorem 4 is organized as follows. The double exponential upper bound relies on a result showing that, in order to cover a target marking $m_{\text{tgt}}$ it is sufficient to consider only firing sequences that cross (i.e., move a pebble to and from) each place at most *K* times, where *K* is the size of the unary encoding of $m_{\text{tgt}}$. Based on this result (Lemma 6), we define an effectively computable algebra $\mathcal{F}$ (Figure 2), having the property that the coverability problem reduces to a membership test on the language of the input grammar in $\mathcal{F}$. Here the use of HR guarantees that $\mathcal{F}$ is finite. The upper bound follows from the fact that $\mathcal{L}^{\mathcal{F}}(\Gamma)$ is computable in double exponential time (see Proposition 3 for a precise estimation). The lower bound uses a polynomial reduction from the emptiness problem for 2-way nondeterministic automata [21] (2NFA). This construction works because (1) 2NFAs run on words which have a chain-like and thus HR-expressible structure, and (2) 2NFAs have only finite memory, which we are able to encode within the constraints of PPS.

## 4.2 Firing Sequences

For the rest of this section, let $\mathcal{S} = (\mathcal{S}, \xi)$ be a fixed open pebble-passing system, having an underlying system $\mathcal{S} = (\mathcal{V}, \mathcal{E}, \lambda)$ whose behavior is $\beta(\mathcal{S}) \stackrel{\text{def}}{=} (\mathcal{N}, \mathcal{m}_0)$. Below, we introduce an equivalent characterization of the firing sequences of $\beta(\mathcal{S})$.
The footprint of a marking m is a mapping $fp_m: V \to \{0,1\}$ defined as $fp_m(v) \stackrel{\text{def}}{=} m(q_\top^{\lambda(v)}, v)$, for each vertex $v \in V$. Note that $fp_m$ evaluates to 1 on pebble and to 0 on hole vertices. We say that a marking footprint $\pi$ is valid over $V \subseteq V$ iff $0 \le \pi(v) \le 1$ for each vertex $v \in V$, resp. valid, when $V=V$ follows from the context.

Given a subset of states $Q \subseteq Q_P$ and a marking to cover $m_{tgt} : Q \to \mathbb{N}$, the coverability problem asks for the existence of a reachable marking $m : Q_N \to \{0,1\}$ such that, for each process type $p \in \mathcal{P}$ and each place $q \in Q$:

$$ \|\{v \in \lambda^{-1}(p) | fp_m(v) = 0\}\| \ge m_{tgt}(q_{\perp}^p) \quad (5) $$

$$ \|\{v \in \lambda^{-1}(p) | fp_m(v) = 1\}\| \ge m_{tgt}(q_{\perp}^p) \quad (6) $$

The footprint $fp_{v \to v'} : V \to \mathbb{Z}$ of an edge $v \to v' \in E$ is defined as $fp_{v \to v'}(u) \stackrel{\text{def}}{=} 1$ if $u = v$, $-1$ if $u = v'$ and $0$, otherwise. We extend footprints to sequences of edges $e \in E^*$ as in $fp_e \stackrel{\text{def}}{=} \sum_{e \in e} \tau_e$. Because each edge $v \to v' \in E$ corresponds to the transition that moves a token from $(q_\top^{\lambda(v)}, v)$ to $(q_\perp^{\lambda(v)}, v)$ (resp. from $(q_\perp^{\lambda(v')}, v')$ to $(q_\top^{\lambda(v')}, v')$) in the PN $\beta(S)$, we shall abuse notation and write $\beta(v \to v')$ for the transition corresponding to $v \to v'$ in $\beta(S)$ and $\beta(e)$ for the sequence of transitions corresponding to $e \in E^*$.

We remark that, for each firing sequence $m \stackrel{\beta(e)}{\rightsquigarrow} m'$, we have $fp_{m'} - fp_m = fp_e$. Intuitively, $fp_e$ is a witness of the fact that the effect of firing the transitions $\beta(e)$ is to move pebbles from $\{v | fp_e(v) = -1\}$ to $\{v | fp_e(v) = 1\}$; the vertices from $\{v | fp_e(v) = 0\}$ may store pebbles in between, but are ultimately restored to their initial state.

We denote by $\#_e(e)$ the number of times the edge $e$ occurs in the sequence $e$. We use the shorthands $\#_{u \to}(e) \stackrel{\text{def}}{=} \sum_{u' \in V} \#_{u \to u'}(e)$ and $\#_{\to u}(e) \stackrel{\text{def}}{=} \sum_{u' \in V} \#_{u' \to u}(e)$. We define the following partial orders between sequences of edges: $e' \preceq e \iff \#_e(e') \le \#_e(e)$, for each $e \in E$, and $e' \sqsubseteq e \iff e' \preceq e$ and $fp_{e'} = fp_e$. The following lemma characterizes the existence of fireable sub-sequences:

**Lemma 5.** For each marking $m$ and sequence of edges $e$, the following are equivalent:

(i) $fp_m + fp_e$ is a valid marking footprint,

(ii) there exists a sequence of edges $e' \sqsubseteq e$ such that $\beta(e')$ is fireable from $m$.

Using the previous lemma, we prove that, in order to cover a given marking $m_{tgt}$, it suffices to consider only those firing sequences that cross each vertex a bounded number of times, where the bound is the size of the unary encoding of $m_{tgt}$. To that end, we define the degree of a sequence $e \in E^*$ as the maximum number of occurrences of one vertex in the sequence, i.e., $\deg(e) \stackrel{\text{def}}{=} \max\{\#_{u \to}(e), \#_{\to u}(e) | u \in V\}$. From now on, the domain of $m_{tgt}$ will implicitly be the set $Q \subseteq Q_P$. To simplify the following statement, we say that $m : Q_N \to \mathbb{N}$ covers $m_{tgt}$ iff $\sum_{(q,v) \in Q_N} m(q, v) \ge m_{tgt}(q)$, for each $q \in Q$ and that $m_{tgt}$ is coverable by $S$ iff there exists $m \in \text{reach}(\beta(S))$ that covers $m_{tgt}$. Since, in a pebble-passing system, markings can be equated to their footprints, we say that $fp_m$ covers $m_{tgt}$ whenever $m$ and $m_{tgt}$ satisfy the conditions (5) and (6) above.

**Lemma 6.** A marking $m_{tgt}$ is coverable by $S$ iff there exists $e \in E^{* \le K}$ such that $fp_{m_0} + fp_e$ covers $m_{tgt}$, where $K \stackrel{\text{def}}{=} \sum_{q \in Q} m_{tgt}(q)$, and $E^{* \le K} \stackrel{\text{def}}{=} \{e \in E^* | \deg(e) \le K\}$.
4.3 Flows

To check coverability, we consider an algebra $\mathcal{F}$ whose elements represent the sequences of edges that cross each vertex at most $K$ times. The domain of $\mathcal{F}$ is $\mathbb{F} \subseteq \text{pow}([0, K]^\Sigma \times [0, K]^\Sigma \times [0, K]^Q)$. The elements $(f^+, f^-, n) \in \mathbb{F}$ represent sequences of edges, such that $f^+(\sigma)$ (resp. $f^-(\sigma)$) is the in-degree (resp. out-degree) of the $\sigma$-source of $S$ and $n(q)$ is the number of tokens that end in $q \in Q$. Intuitively, a tuple $(f^+, f^-, n)$ witnesses the existence of a sequence that covers $n$, that can later be combined with other sequences which compensate its surplus $f^+$ and deficit $f^-$ on the sources of $S$. Since we consider only systems with finitely many sources (guaranteed by HR) and since $Q \subseteq Q$ is finite, $\mathcal{F}$ is a finite algebra. We will later characterize its exact size. Formally, we define the following mappings, where $S$ denotes the set of open systems, i.e., systems with sources:

$$ \omega: \mathbb{E}^{* \leq K} \times \mathbb{V}^{\Sigma} \to [0, K]^{\Sigma} \times [0, K]^{\Sigma} \times [0, K]^{Q} $$

$$ \omega(\mathbf{e}, \xi) = (f^+, f^-, n) \iff $$

$$ \left\{ \begin{array}{l} f^+(\boldsymbol{\sigma}) = \#_{\xi(\boldsymbol{\sigma})} (\mathbf{e}) \qquad f^-(\boldsymbol{\sigma}) = \#_{\to \xi(\boldsymbol{\sigma})} (\mathbf{e}) \\ n(q_{\perp}^{\boldsymbol{p}}) = \min(\mathrm{m}_{\mathrm{tgt}}(q_{\perp}^{\boldsymbol{p}}), \|\{v \in \lambda^{-1}(\boldsymbol{p}) \setminus \mathrm{img}(\xi) \mid (\mathrm{fp}_{\mathrm{init}_{\boldsymbol{p}}} + \mathrm{fp}_{\mathrm{e}})(v) = 0\}\|) \\ n(q_{\perp}^{\boldsymbol{p}}) = \min(\mathrm{m}_{\mathrm{tgt}}(q_{\perp}^{\boldsymbol{p}}), \|\{v \in \lambda^{-1}(\boldsymbol{p}) \setminus \mathrm{img}(\xi) \mid (\mathrm{fp}_{\mathrm{init}_{\boldsymbol{p}}} + \mathrm{fp}_{\mathrm{e}})(v) = 1\}\|) \end{array} \right. $$

$$ \eta: S \to \text{pow}([0, K]^\Sigma \times [0, K]^\Sigma \times [0, K]^Q) $$

$$ \eta(S, \xi) \stackrel{\text{def}}{=} \{\omega(\mathbf{e}, \xi) \mid \mathbf{e} \in \mathbb{E}_{S}^{* \leq K}, \mathrm{fp}_{\text{init}_{\beta(S)}} + \mathrm{fp}_{\mathrm{e}} \text{ is a valid marking footprint over } V_S \setminus \text{img}(\xi)\} $$

We define the finite algebra of flows $\mathcal{F}$ using Proposition 1, where $\eta$ is taken to be the homomorphism between $S$ and $\mathcal{F}$:

**Lemma 7.** $\sim_{\text{ker}(\eta)}$ is a HR congruence.

This implies $\eta(\mathcal{L}^S(\Gamma)) = \mathcal{L}^\mathcal{F}(\Gamma)$, so all we need is a way of computing $\mathcal{L}^\mathcal{F}(\Gamma)$. The remainder of the proof for the upper bound from Theorem 4 thus relies on the fact that the interpretation of the HR signature in $\mathcal{F}$ is effectively computable, which is the purpose of the proposition below. The size of the grammar $\Gamma$ is the total number of occurrences of a nonterminal or function symbol in a rule from $\Gamma$, denoted as $|\Gamma|$.

**Proposition 3.** The size of each element $f \in \mathbb{F}$ is $2^{O((\|\Sigma\|+\|\mathcal{P}\|)\cdot\log K)}$ and the function $\mathrm{op}^\mathcal{F}(f_1, \dots, f_n)$ can be computed in time $2^{O((\|\Sigma\|+\|\mathcal{P}\|)\cdot\log K)}$, for each HR-function symbol $\mathrm{op}$ of arity $n \ge 0$ and all elements $f_1, \dots, f_n \in \mathbb{F}$. Moreover, for each grammar $\Gamma$ using source labels from $\Sigma$, the language $\mathcal{L}^\mathcal{F}(\Gamma)$ is computable in time $2^{\Gamma|\cdot 2^{O((\|\Sigma\|+\|\mathcal{P}\|)\cdot\log K)}}$.

Deciding whether $\mathrm{m}_{\mathrm{tgt}}$ is coverable by some instance $S \in \mathcal{L}^S(\Gamma)$, for a given HR grammar $\Gamma$, is done by checking $\mathrm{restrict}_0^\mathcal{F}(\mathcal{L}^\mathcal{F}(\Gamma)) \cap \{(0, 0, \mathrm{m}_{\mathrm{tgt}})\} \stackrel{?}{=} \emptyset$. We apply $\mathrm{restrict}_0$ to $\mathcal{L}^\mathcal{F}(\Gamma)$ to ensure that the sequences of edges considered lead to valid marking footprints on every vertex of a system $(S, \xi) \in \mathcal{L}^S(\Gamma)$, including the sources from $\mathrm{img}(\xi)$, that were exempt from satisfying this condition (see the above definition of $\eta$). Computing $\mathrm{restrict}_0^\mathcal{F}(\mathcal{L}^\mathcal{F}(\Gamma))$ simply adds a linear factor compared to $\mathcal{L}^\mathcal{F}(\Gamma)$, and so does checking if it contains $(0, 0, \mathrm{m}_{\mathrm{tgt}})$. Thus we have an overall $2\text{EXPTIME}$ upper bound.
<table><caption>**Fig. 7.** Table of experiments. “PPS”, these are pebble-passing systems (Section 4). “TPS”, these are token-passing systems ([4]). “Result”, $S/T$ means that of $T$ safety properties, we proved $S$. “Size”, $(\bigcirc p, \bigcirc t) \times n$ means that LoLA analyzed $n$ nets, consisting of on average $p$ places and $t$ transitions. “Runtime”, $(p+l) \pm e$ means that ParCoSys ran for $p+l$ milliseconds with a standard deviation of $e$ milliseconds, including $p$ computing the abstraction and $l$ waiting for LoLA.</caption><thead><tr><th>Name</th><th>Architecture</th><th>PPS</th><th>TPS</th><th>Result</th><th>Size</th><th>Runtime (ms)</th></tr></thead><tbody><tr><td>fig-1c</td><td>chain</td><td>✓</td><td>✓</td><td>2/2</td><td>(12, 13) x 2</td><td>(59 + 9) ± 6</td></tr><tr><td>fig-1d</td><td>star</td><td>✓</td><td>✓</td><td>2/2</td><td>(11, 10) x 2</td><td>(59 + 9) ± 4</td></tr><tr><td>fig-5</td><td>trivial</td><td>✓</td><td>✓</td><td>1/2</td><td>(13, 10) x 3</td><td>(49 + 2) ± 4</td></tr><tr><td>ring</td><td>ring</td><td>✓</td><td>✓</td><td>2/2</td><td>(9, 11) x 16</td><td>(80 + 21) ± 4</td></tr><tr><td>double-ring</td><td>ring</td><td>✓</td><td>✓</td><td>1/1</td><td>(8, 14) x 34</td><td>(113 + 44) ± 10</td></tr><tr><td>philos</td><td>ring</td><td></td><td></td><td>1/1</td><td>(16, 14) x 8</td><td>(134 + 21) ± 5</td></tr><tr><td>consensus</td><td>star</td><td></td><td></td><td>5/5</td><td>(29, 23) x 6</td><td>(83 + 26) ± 6</td></tr><tr><td>leader-election</td><td>ring</td><td></td><td></td><td>1/2</td><td>(27, 32) x 2</td><td>(58 + 35) ± 5</td></tr><tr><td>tree-dfs</td><td>binary tree</td><td>✓</td><td>✓</td><td>2/2</td><td>(19, 16) x 2</td><td>(52 + 5) ± 4</td></tr><tr><td>tree-down</td><td>binary tree</td><td>✓</td><td>✓</td><td>1/1</td><td>(11, 12) x 20</td><td>(125 + 36) ± 7</td></tr><tr><td>tree-halves</td><td>binary tree</td><td></td><td></td><td>4/4</td><td>(26, 23) x 8</td><td>(92 + 190) ± 7</td></tr><tr><td>tree-nav</td><td>chained binary tree</td><td>✓</td><td>✓</td><td>2/2</td><td>(12, 19) x 12</td><td>(139 + 46) ± 7</td></tr><tr><td>lock</td><td>star</td><td></td><td>✓</td><td>1/3</td><td>(9, 11) x 4</td><td>(59 + 8) ± 5</td></tr><tr><td>star</td><td>star</td><td>✓</td><td>✓</td><td>3/3</td><td>(12, 11) x 4</td><td>(58 + 11) ± 5</td></tr><tr><td>star-ring</td><td>chained star</td><td></td><td>✓</td><td>3/3</td><td>(17, 14) x 2</td><td>(63 + 12) ± 4</td></tr><tr><td>server-loop</td><td>ring of stars</td><td></td><td></td><td>2/3</td><td>(19, 19) x 8</td><td>(112 + 4627) ± 20</td></tr><tr><td>coverapprox</td><td>star</td><td></td><td></td><td>1/2</td><td>(3, 8) x 6</td><td>(70 + 62) ± 8</td></tr><tr><td>simplify-me</td><td>star</td><td></td><td></td><td>1/2</td><td>(7, 9) x 4</td><td>(64 + 21) ± 5</td></tr><tr><td>propagation</td><td>ring</td><td></td><td></td><td>1/2</td><td>(13, 13) x 4</td><td>(90 + 278) ± 10</td></tr><tr><td>open</td><td>ring</td><td></td><td></td><td>0/1</td><td>(13, 14) x 4</td><td>(74 + 269) ± 13</td></tr></tbody></table>

The PSPACE lower bound is obtained by a polynomial reduction from the PSPACE-complete emptiness problem for 2-way nondeterministic finite automata (2NFA). The idea of the reduction is to simulate a run of a 2NFA on a given word by a grid-like system. This system encodes each letter of the word horizontally, and each state of the automaton vertically. The possible movements of the pebble are determined by the transition relation of the 2NFA. Since there are finitely many states in the automaton, we have a grid of constant height and unbounded width, which is expressible in HR.

# 5 Experiments

We have implemented the counting abstraction method in the prototype tool ParCoSys (Parameterized Coverability) [30]. The input of the tool is a grammar describing the system and a safety property to be checked. The output is a finite set of Petri nets that is fed to the LoLA analyzer [32]. Our choice for LoLA was driven by its robustness and performance, but any Petri net analyzer can be used as back-end, in principle.
We tested<fnref n="6" /> our tool on the examples listed in Figure 7

- fig-1c and fig-1d are the systems used as examples in Figure 1 (c) and (d) respectively. We easily verify nonduplication of the token ($m_{tgt}(tok) + m_{tgt}(tokC) > 1$) and mutual exclusion of processes in the critical section work ($m_{tgt}(work) > 1$).

<footnote n="6">⁶ The times were obtained on a Intel Ultra 7 laptop, with 16GiB RAM, under Ubuntu 24.04. All benchmark specifications and logs are provided as additional material [30].</footnote>
- fig-5 is the example shown in Figure 5. Here the "Result" 1/2 denotes that $m_{tgt}(q_c^1) > 0$ exhibits a false positive with the default folding, but there is an easy refinement of the grammar that leads to a successful verification on the second attempt.

- ring is a standard token ring, on which we verify mutual exclusion ($m_{tgt}(tok) > 1$).

- double-ring is a token ring with two tokens instead of one ($m_{tgt}(tok) > 2$). It is mainly interesting as an example of a PPS that is not TPS.

- philos implements the algorithm of dining philosophers. We prove that adjacent processes $p_1$ and $p_2$ do not enter their critical section *eating* simultaneously ($m_{tgt}(eating^{p_1}) > 0 \land m_{tgt}(eating^{p_2}) > 0$).

- consensus has a star of processes performing 2-valued consensus. All processes must choose the same value: ($m_{tgt}(choose_0) > 0 \land m_{tgt}(choose_1) > 0$)).

- leader-election performs a leader election with predetermined winner (found in [9]). We prove that $p_0$ is the unique winner ($m_{tgt}(win^{p_0}) > 0 \land m_{tgt}(win) > 0$).

The rest of the tests are more *ad hoc*, designed to showcase a wider range of architectures as well as interesting false positives:

- tree-dfs, tree-down, tree-halves, tree-nav are binary trees on which we prove different ways of expressing mutual exclusion with one or two tokens.

- lock should satisfy a mutual exclusion ($m_{tgt}(on) > 1$), but a false positive occurs. A partial unfolding (Section 3.4) allows proving the desired property.

- star and star-ring are stars with easy mutual exclusion properties.

- server-loop is a ring where each node has itself a star of child processes. One false positive here could theoretically be solved by a partial unfolding, but we have not yet implemented the logic that would allow for this specific pattern.

- cover-approx, simplify-me and propagation each have a false positive that can be solved by a refinement technique consisting of deleting transitions that are found to be unfireable during intermediate stages of the fixed point computation.

- open so far evades our ideas for refinements. We can prove that partial unfolding on its own is insufficient, since all finite foldings exhibit false positives.

# 6 Conclusions

We present two orthogonal verification results for parameterized process networks with topology specified using hyperedge-replacement graph grammars. The first result is a finitary counting abstraction, that consists in collapsing nodes of the same type in the parameterized family of Petri nets that gives the semantics of behaviors. The second result identifies a decidable fragment of the (undecidable) parameterized verification problem and evaluates its complexity bounds.

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

**Disclosure of interests.** The authors have no competing interests to declare that are relevant to the content of this article.
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, S. Jacobs, A. Khalimov, and S. Rubin. Parameterized model checking of token-passing systems. In *VMCAI'14*, volume 8318 of *Lecture Notes in Computer Science*, pages 262–281. 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. B. Aminof and S. Rubin. Model checking parameterised multi-token systems via the composition method. In *IJCAR'16*, volume 9706 of *Lecture Notes in Computer Science*, pages 499–515. Springer, 2016.

7. R. Bloem, S. Jacobs, and A. Khalimov. *Decidability of Parameterized Verification*. Morgan & Claypool Publishers, 2015.

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

9. M. Bozga, J. Esparza, R. Iosif, J. Sifakis, and C. Welzel. Structural invariants for the verification of systems with parameterized architectures. In A. Biere and D. Parker, editors, *Tools and Algorithms for the Construction and Analysis of Systems - 26th International Conference, TACAS 2020, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2020, Dublin, Ireland, April 25-30, 2020, Proceedings, Part I*, volume 12078 of *Lecture Notes in Computer Science*, pages 228–246. Springer, 2020.

10. M. Bozga, R. Iosif, A. Sangnier, and N. Villani. Counting abstraction for the verification of structured parameterized networks (full version), 2025. arxiv.org/abs/2502.15391.

11. M. Bozga, R. Iosif, and J. Sifakis. Checking deadlock-freedom of parametric component-based systems. *J. Log. Algebraic Methods Program.*, 119:100621, 2021.

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

13. J. Bradbury, J. Cordy, J. Dingel, and M. Wermelinger. A survey of self-management in dynamic software architecture specifications. In *Proceedings of the 1st ACM SIGSOFT workshop on Self-managed systems*, pages 28–33. ACM, 2004.

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

15. A. Butting, R. Heim, O. Kautz, J. O. Ringert, B. Rumpe, and A. Wortmann. A classification of dynamic reconfiguration in component and connector architecture description. In *Proceedings of MODELS 2017 Satellite Event: Workshops (ModComp)*, volume 2019 of *CEUR Workshop Proceedings*, pages 10–16. CEUR-WS.org, 2017.

16. Y. Chen, C. Hong, A. W. Lin, and P. Rümmer. Learning to prove safety over parameterised concurrent systems. In D. Stewart and G. Weissenbacher, editors, *2017 Formal Methods in Computer Aided Design, FMCAD 2017*, pages 76–83. IEEE, 2017.

17. 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.
18. J. Esparza. Petri nets, commutative context-free grammars, and basic parallel processes. In *Fundamentals of Computation Theory*, pages 221–232. Springer Berlin Heidelberg, 1995.

19. J. Esparza, M. A. Raskin, and C. Welzel. Regular model checking upside-down: An invariant-based approach. In B. Klin, S. Lasota, and A. Muscholl, editors, *33rd International Conference on Concurrency Theory, CONCUR 2022, September 12-16, 2022, Warsaw, Poland*, volume 243 of *LIPIcs*, pages 23:1–23:19. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2022.

20. A. Finkel and J. Leroux. Recent and simple algorithms for petri nets. *Softw. Syst. Model.*, 14(2):719–725, 2015.

21. Z. Galil. Hierarchies of complete problems. *Acta Informatica*, 1976.

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

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

24. Y. Kesten, O. Maler, M. Marcus, A. Pnueli, and E. Shahar. Symbolic model checking with rich assertional languages. *Theoretical Computer Science*, 256(1):93 – 112, 2001.

25. Y. Kesten, A. Pnueli, E. Shahar, and L. D. Zuck. Network invariants in action. In *CONCUR 2002 - Concurrency Theory, 13th International Conference*, volume 2421 of LNCS, pages 101–115. Springer, 2002.

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

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

28. A. W. Lin and P. Rümmer. Regular model checking revisited. In E. Olderog, B. Steffen, and W. Yi, editors, *Model Checking, Synthesis, and Learning - Essays Dedicated to Bengt Jonsson on The Occasion of His 60th Birthday*, volume 13030 of Lecture Notes in Computer Science, pages 97–114. Springer, 2021.

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

30. N. Villani, R. Iosif, A. Sangnier, and M. Bozga. Parcosys: Counting abstraction for the verification of structured parameterized networks, Apr. 2025. Ongoing development version at https://gricad gitlab univ-grenoble-alpes fr neven parcosys.

31. K. Wolf. Petri net model checking with lola. In V. Khomenko and O. H. Roux, editors, *Application and Theory of Petri Nets and Concurrency - 39th International Conference, PETRI NETS 2018, Bratislava, Slovakia, June 24-29, 2018, Proceedings*, volume 10877 of Lecture Notes in Computer Science, pages 351–362. Springer, 2018.

32. K. Wolf and N. Lohmann. Lola: A low level petri net analyzer. https://theo.informatik.uni-rostock.de/theo-forschung/tools/lola/.

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