# Parameterized Verification of Timed Networks with Clock Invariants

Étienne André, Swen Jacobs, Shyam Lal Karra, Ocan Sankur

► To cite this version:

Étienne André, Swen Jacobs, Shyam Lal Karra, Ocan Sankur. Parameterized Verification of Timed Networks with Clock Invariants. FSTTCS 2025 - 45th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science, Dec 2025, Goa, India. 10.4230/LIPIcs.FSTTCS.2025.8 . hal-05450304

HAL Id: hal-05450304

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

Submitted on 9 Jan 2026

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 CC BY 4.0 - Attribution - International License
# Parameterized Verification of Timed Networks with Clock Invariants

## Anonymous

anonymous affiliation

### Abstract

We consider parameterized verification problems for networks of timed automata (TAs) based on different communication primitives. To this end, we first consider disjunctive timed networks (DTNs), i.e., networks of TAs that communicate via location guards that enable a transition only if there is another process in a certain location. We solve for the first time the case with unrestricted clock invariants, and establish that the parameterized model checking problem (PMCP) over finite local traces can be reduced to the corresponding model checking problem on a single TA. Moreover, we prove that the PMCP for networks that communicate via lossy broadcast can be reduced to the PMCP for DTNs. Finally, we show that for networks with *k*-wise synchronization, and therefore also for timed Petri nets, location reachability can be reduced to location reachability in DTNs. As a consequence we can answer positively the open problem from Abdulla et al. (2018) whether the universal safety problem for timed Petri nets with multiple clocks is decidable.

**2012 ACM Subject Classification** Theory of computation → Concurrency

**Keywords and phrases** Networks of Timed Automata, Parameterized Verification, Timed Petri Nets

**Digital Object Identifier** 10.4230/LIPIcs.CVIT.2016.1

## 1 Introduction

Formally reasoning about concurrent systems is difficult, in particular if correctness guarantees should hold regardless of the number of interacting processes—a problem also known as *parameterized verification* [3, 7], since the number of processes is considered a parameter of the system. Parameterized verification is undecidable in general [13] and even in very restricted settings, e.g., for safety properties of finite-state processes with rather weak communication primitives, such as token-passing or transition guards [31, 22]. A long line of research has identified classes of systems and properties for which parameterized verification is decidable [22, 27, 23, 24, 21, 17, 9, 25], usually with finite-state processes.

Timed automata (TAs) [8] provide a computational model that combines real-time constraints with concurrency, and are therefore an expressive and widely used formalism to model real-time systems. However, TAs are usually used to model a constant and *fixed* number of system components. When the number *n* of components is very large or unknown, considering their static combination becomes highly impractical, or even impossible if *n* is unbounded. However, there are several lines of research studying networks with a parametric number of timed components (see e.g., [6, 16, 4, 11, 1, 10]).

One of these lines considers different variants of timed Petri nets (we here consider the version defined in [2]), and networks of timed automata with *k*-wise synchronization [6, 5], a closely related model. Due to the expressiveness of the synchronization primitive, results for these models are often negative or limited to severely restricted cases. For example, in networks of timed automata with a controller process and multiple clocks per process, location reachability is undecidable (even in the absence of clock invariants that could force a process to leave a location) [5]. The problem is decidable with a single clock per process and without clock invariants [6]. Decidability remains open for location reachability in networks *without* a controller process and with multiple clocks (with or without clock invariants), which is equivalent to the universal safety problem for timed Petri nets that is mentioned as

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

<figure><img src="image_3.png" /></figure>
1:2 Parameterized Verification of Timed Networks with Clock Invariants

an open problem in [2].

Another model that has received attention recently and is very important for the work we present is that of *Disjunctive Timed Networks* (DTNs) [30, 12]. It combines the expressive formalism of TAs with the relatively weak communication primitive of disjunctive guards [22]: transitions can be guarded with a location (called “guard location”), and such a transition can only be taken by a TA in the network if another process is in that location upon firing. For example, in the DTN in Fig. 1, the transition from init to reading is guarded by location post: for a process to take this transition, at least one other process must be in post.

Parameterized model checking of DTNs was first studied in [30], who considered local trace properties in the temporal logic MITL, and showed that the problem can be solved with a cutoff, i.e., a number of processes that is sufficient to determine satisfaction in networks of any size. However, their result is restricted to the case when guard locations do not have clock invariants. This restriction is crucial to their proof, and they furthermore showed that statically computable cutoffs do not exist for the case when TAs can have clock invariants on all locations.

<figure><img src="image_4.png" /><figcaption>Figure 1 Asynchronous data read example</figcaption></figure>

However, the non-existence of cutoffs does not imply that the problem is undecidable. In [12], the authors improved the aforementioned results by avoiding the construction of a cutoff system and instead using a modified zone graph algorithm. Moreover, they gave sufficient conditions on the TAs to make the problem decidable even in the presence of clock invariants on guard locations. However, these conditions are semantic, and it is not obvious how to build models that satisfy them; for instance, our motivating example in Fig. 1 does not satisfy them. The decidability of the case without restrictions on clock invariants thus remained open.

In this paper, we show that properties of finite local traces (and therefore also location reachability) are decidable for DTNs without restrictions on clock invariants. Moreover, we show that checking local trace properties of systems with lossy broadcast communication [21, 11] or with *k*-wise synchronization can be reduced to checking local trace properties of DTNs. Note that our simulation of these systems by DTNs crucially relies on the power of clock invariants, and would not be possible in the previous restricted variants of DTNs.

To see why checking local trace properties of DTNs with invariants is technically difficult, consider first the easy case from [30], where guard locations cannot have invariants. In this case, it is enough to determine for every guard location *q* the minimal time *δ* at which it can be reached: since a process cannot be forced to leave, *q* can be occupied at any time in [*δ*, ∞), and transitions guarded by *q* can be assumed to be enabled at any time later than *δ*. This is already the underlying insight of [30], and in [12] it is embedded into a technique that replaces location guards with clock guards *t* ≥ *δ*, where *t* is a clock denoting the time elapsed since the beginning. In contrast, if guard locations can have invariants, a process in *q* can be forced to leave after some time. Therefore, the set of global times where *q* can be occupied is an arbitrary set of timepoints, and it is not obvious how it can be finitely represented.

**Detailed Example.** We introduce an example that motivates the importance of clock invariants in modeling concurrent timed systems, and will be used as a running example. It is inspired by the verification of asynchronous programs [26]. In this setting, processes can be “posted” at runtime to solve a task, and will terminate upon completing the task.
<figure><img src="image_5.png" /><figcaption>Figure 2 Example of a computation in $A^3$ for $A$ as depicted by Fig. 1.</figcaption></figure>

Our example in Fig. 1 features one clock $c$ per process; symbols $\sigma_i$ and $\sigma_{err}$ are transition labels. An unbounded number of processes start in the initial location `init`. In the inner loop, a process can move to location `listen` in order to see whether an input channel carries data. Once it determines that this is the case, it moves to `post`, thereby giving the command to post a process that reads the data, and then can return to `init`. In the outer loop, if another process gives the command to read data, i.e., is in `post`, then another process can accept that command and move to `reading`. After some time, the process will either determine that all the data has been read and move to `done`, or it will timeout and move to `post` to ask another process to carry on reading. However, this scheme may run into an error if there are processes in `done` and `reading` at the same time, modeled by a transition from `reading` to `error` that can only be taken if `done` is occupied.

While this example is relatively simple, checking reachability of location error (in a network with arbitrarily many processes) is not supported by any existing technique. This is because clock invariants on guard locations are not supported at all by [30], and are supported only in special cases (that do not include this example) by [12]. Also other results that could simulate DTNs do not support clock invariants at all [6, 4].

Moreover, note that clock invariants may be essential for correctness of such systems: in a system $A^3$, consisting of three copies of the automaton in Fig. 1, location error is reachable; a computation that reaches error is given in Fig. 2. However, if we add a clock invariant $c \le 0$ to location `post` (forcing processes that enter `post` to immediately leave it again), it becomes unreachable<fnref n="1" />.

**Contributions.** We present new decidability results for parameterized verification problems with respect to three different system models as outlined below.

- **DTNs (Section 3).** For DTNs, we show that, surprisingly, and despite the absence of cutoffs [30], the parameterized model checking problem for finite local traces is decidable in the general case, without any restriction on clock invariants. Our technique circumvents the non-existence of cutoffs by constructing a modified region automaton, a well-known data structure in timed automata literature, such that communication via disjunctive guards is directly taken into account. In particular, we focus on analyzing the traces of a single (or a finite number of) process(es) in a network of arbitrary size.

While our algorithm uses some techniques from [12], there are fundamental differences: in particular, we introduce a novel abstraction of global time into a finite number of “slots”,

<footnote n="1">¹ To see this, consider the intervals of global time in which the different locations can be occupied: first observe that `post` in the inner loop can now only be occupied in intervals $[4k, 4k]$ (for $k \in \mathbb{N}$), and therefore processes can only move into `reading` at these times. From there, they might move into `post` after two time units, so overall `post` can be occupied in intervals $[2k, 2k]$ for $k \ge 2$, and `reading` in any interval $[2k, 2(k+1)]$. Since clock $c$ is always reset upon entering `reading`, `done` can only be occupied in intervals $[2k+1, 2k+1]$ for $k \ge 2$, whereas for a process in `reading` the clock constraint on the transition to `error` can only be satisfied in intervals $[2k, 2k+1)$. Therefore, `error` is not reachable with the additional clock invariant on `post`.</footnote>
1:4 Parameterized Verification of Timed Networks with Clock Invariants

which are elementary intervals with integer bounds, designed to capture the information
necessary for disjunctive guard communication. When a transition with a location guard
is to be taken at a given slot, we check whether the given guard location appears in the
same slot. It turns out that such an abstract treatment of the global time is sound: we
prove that in this case, one can find a computation that enables the location guard at
any real time instant inside the given slot. Thus, the infinite set of points at which a
location guard is enabled is a computable union of intervals; and we rely on this property
to build a finite-state abstraction to solve our problem.

■ **Lossy Broadcast Timed Networks (Section 4).** We investigate the relation between communication with disjunctive guards and with *lossy broadcast* [21, 11]. For finite-state processes, it is known that lossy broadcast can simulate disjunctive guards wrt. reachability [14], but the other direction is unknown.<fnref n="2" /> As our second contribution, we establish the decidability of the parameterized model checking problem for local trace properties in timed lossy broadcast networks. This result is obtained by proving that communication by lossy broadcast is equivalent to communication by disjunctive guards for networks of timed automata *with* clock invariants for local trace properties.

- **Synchronizing Timed Networks and Timed Petri Nets (Section 5).** Finally, we show that the location reachability problem for controllerless multi-clock timed networks with *k*-wise synchronization can be reduced to the location reachability problem for DTNs with clock invariants.

As a consequence, it follows that the universal safety problem for timed Petri nets with
multiple clocks, stated as an open problem in [2], is also decidable.

In the last two cases, we develop DTN gadgets (Figs. 6 to 8 in Appendix B) that require clock invariants on guard locations. This is why clock invariants are crucial in our formalism, which is a nontrivial extension of [12]. Note that in both cases we get decidability even for variants of the respective system models with clock invariants, which was not considered in [11] or [2].

For all of the above systems, location reachability can be decided in EXPSPACE.

Due to space constraints, formal proofs of some of our results are given in the appendix.

2 Preliminaries

Let $\mathcal{C}$ be a set of clock variables, also called *clocks*. A *clock valuation* is a mapping $v : \mathcal{C} \to \mathbb{R}_{\ge 0}$.
For a valuation $v$ and a clock $c$, we denote the fractional and integral parts of $v(c)$ by $\text{frac}(v(c))$
and $\lfloor v(c) \rfloor$ respectively. We denote by $\mathbf{0}$ the clock valuation that assigns 0 to every clock,
and by $v + \delta$ for $\delta \in \mathbb{R}_{\ge 0}$ the valuation s.t. $(v + \delta)(c) = v(c) + \delta$ for all $c \in \mathcal{C}$. Given a subset
$\mathcal{C}_r \subseteq \mathcal{C}$ of clocks and a valuation $v$, $v[\mathcal{C}_r \leftarrow 0]$ denotes the valuation $v'$ such that $v'(c) = 0$ if
$c \in \mathcal{C}_r$ and $v'(c) = v(c)$ otherwise. We call *clock constraints* $\Psi(\mathcal{C})$ the terms of the following
grammar: $\psi ::= \top | \psi \land \psi | c \sim d | c \sim c' + d$ with $d \in \mathbb{N}$, $c, c' \in \mathcal{C}$ and $\sim \in \{<, \le, =, \ge, >\}$.

A clock valuation $v$ satisfies a clock constraint $\psi$, denoted by $v \models \psi$, if $\psi$ evaluates to $\top$
after replacing every $c \in \mathcal{C}$ with its value $v(c)$.

**Definition 1.** A timed automaton (TA) $A$ is a tuple $(Q, \hat{q}, \mathcal{C}, \Sigma, \mathcal{T}, \text{Inv})$ where $Q$ is a finite set of locations with initial location $\hat{q}$, $\mathcal{C}$ is a finite set of clocks, $\Sigma$ is a finite alphabet that contains a subset $\Sigma^{-}$ of special symbols, including a distinguished symbol $\epsilon \in \Sigma^{-}$,

<footnote n="2">² [14] considers IO nets which are equivalent to systems with disjunctive guards. It gives a negative result for a specific simulation relation, but does not prove that simulation is impossible in general.</footnote>
$\mathcal{T} \subseteq Q \times \Psi(C) \times 2^C \times \Sigma \times Q$ is a transition relation, and $\text{Inv} : Q \to \Psi(C)$ assigns to every location $q$ a clock invariant $\text{Inv}(q)$.

TAs were introduced in [8] and clock invariants, also simply called invariants, in [28]. We assume w.l.o.g. that invariants only contain upper bounds on clocks (as lower bounds can be moved into the guards of incoming transitions). $\Sigma^-$ will be used to label silent transitions and unless explicitly specified otherwise (in Sections 4 and 5), we assume that $\Sigma^- = \{\epsilon\}$.

**Example 2.** If we ignore the location guards post (from init to reading) and done (from reading to error), then the automaton in Fig. 1 is a classical TA with one clock $c$. For example, the invariant of done is $c \le 1$ and the transition from init to reading resets clock $c$.

A configuration of a TA $A$ is a pair $(q, v)$, where $q \in Q$ and $v : C \to \mathbb{R}_{\ge 0}$ is a clock valuation. A delay transition is of the form $(q, v) \xrightarrow{\delta} (q, v + \delta)$ for some delay $\delta \in \mathbb{R}_{\ge 0}$ such that $v + \delta \models \text{Inv}(q)$. A discrete transition is of the form $(q, v) \xrightarrow{\sigma} (q', v')$, where $\tau = (q, g, C_r, \sigma, q') \in \mathcal{T}$, $v \models g, v' = v[C_r \leftarrow 0]$ and $v' \models \text{Inv}(q')$. A transition $(q, v) \xrightarrow{\epsilon} (q', v')$ is called an $\epsilon$-transition. We write $(q, v) \xrightarrow{\delta, \sigma} (q', v')$ if there is a delay transition $(q, v) \xrightarrow{\delta} (q, v + \delta)$ followed by a discrete transition $(q, v + \delta) \xrightarrow{\sigma} (q', v')$.

A timed path of $A$ is a finite sequence of transitions $\rho = (q_0, v_0) \xrightarrow{\delta_0, \sigma_0} \dots \xrightarrow{\delta_{l-1}, \sigma_{l-1}} (q_l, v_l)$. For a timed path $\rho = (q_0, v_0) \xrightarrow{\delta_0, \sigma_0} \dots \xrightarrow{\delta_{l-1}, \sigma_{l-1}} (q_l, v_l)$, let $\delta(\rho) = \sum_{0 \le i < l} \delta_i$ be the total time delay of $\rho$. The length of $\rho$ is $2l$. A configuration $(q, v)$ has a timelock if there is $b \in \mathbb{R}_{\ge 0}$ s.t. $\delta(\rho) \le b$ for every timed path $\rho$ starting in $(q, v)$. We write $(q_0, v_0) \xrightarrow{*} (q_l, v_l)$ if there is a timed path $\rho = (q_0, v_0) \xrightarrow{\delta_0, \sigma_0} \dots \xrightarrow{\delta_{l-1}, \sigma_{l-1}} (q_l, v_l)$; $\rho$ is a computation if $q_0 = \hat{q}$ and $v_0 = 0$.

The trace of the timed path $\rho$ is the sequence of pairs of delays and labels obtained by removing transitions with a label from $\Sigma^-$ and adding the delays of these to the following transition (see Appendix A.1). The language of $A$, denoted $\mathcal{L}(A)$, is the set of traces of all of its computations.

We now recall guarded timed automata as an extension of timed automata with location guards, that will allow, in a network, to test whether some other process is in a given location in order to pass the guard.

**Definition 3 (Guarded Timed Automaton (GTA)).** A GTA $A$ is a tuple $(Q, \hat{q}, C, \Sigma, \mathcal{T}, \text{Inv})$, where $Q$ is a finite set of locations with initial location $\hat{q}$, $C$ is a finite set of clocks, $\Sigma$ is a finite alphabet that contains a subset $\Sigma^-$ of special symbols, including a distinguished symbol $\epsilon \in \Sigma^-$, $\mathcal{T} \subseteq Q \times \Psi(C) \times 2^C \times \Sigma \times (Q \cup \{\top\}) \times Q$ is a transition relation, and $\text{Inv} : Q \to \Psi(C)$ assigns to every location $q$ an invariant $\text{Inv}(q)$.

Intuitively, a transition $\tau = (q, g, C_r, \sigma, \gamma, q') \in \mathcal{T}$ takes the automaton from location $q$ to $q'$; $\tau$ can only be taken if clock guard $g$ and location guard $\gamma$ are both satisfied, and it resets all clocks in $C_r$. Note that satisfaction of location guards is only meaningful in a network of TAs (defined below). Intuitively, a location guard $\gamma$ is satisfied if it is $\top$ or if another automaton in the network currently occupies location $\gamma$. We say that $\gamma$ is trivial if $\gamma = \top$. We say location $q$ has no invariant if $\text{Inv}(q) = \top$.

**Example 4.** In the GTA in Fig. 1, the transition from init to reading is guarded by location guard post. The transition from init to listen has a trivial location guard (trivial location guards are not depicted in our figures). Location init has no invariant.

**Definition 5 (Unguarded Timed Automaton).** Given a GTA $A$, we denote by $\text{UG}(A)$ the unguarded version of $A$, which is the TA obtained from $A$ by removing location guards, and adding a fresh clock $t$, called the global clock, that does not appear in the guards or resets. Formally, $\text{UG}(A) = (Q, \hat{q}, C \cup \{t\}, \mathcal{T}', \text{Inv})$ with $\mathcal{T}' = \{(q, g, C_r, \sigma, q') | (q, g, C_r, \sigma, \gamma, q') \in \mathcal{T}\}$.
1:6 Parameterized Verification of Timed Networks with Clock Invariants

For a GTA A, let $A^n$ denote a network of guarded timed automata (NGTA), consisting of
$n$ copies of A. Each copy of A in $A^n$ is called a *process*.

A configuration **c** of an NGTA $A^n$ is a tuple $((q_1, v_1), \dots, (q_n, v_n))$, where every $(q_i, v_i)$ is a configuration of A. The semantics of $A^n$ can be defined as a timed transition system $(\mathcal{C}, \hat{c}, T)$, where $\mathcal{C}$ denotes the set of all configurations of $A^n$, $\hat{c}$ is the unique initial configuration $(\hat{q}, \mathbf{0})^n$, and the transition relation $T$ is the union of the following delay and discrete transitions:

**delay transition** $((q_1, v_1), \dots, (q_n, v_n)) \xrightarrow{\delta} ((q_1, v_1 + \delta), \dots, (q_n, v_n + \delta))$ if $\forall i \in \{1, \dots, n\}: v_i + \delta \models \text{Inv}(q_i)$, i.e., we can delay $\delta \in \mathbb{R}_{\ge 0}$ units of time if all clock invariants are satisfied at the end of the delay.

**discrete transition** $((q_1, v_1), \dots, (q_n, v_n)) \xrightarrow{(i, \sigma)} ((q'_1, v'_1), \dots, (q'_n, v'_n))$ for some $i \in \{1, \dots, n\}$ if $1) (q_i, v_i) \xrightarrow{\sigma} (q'_i, v'_i)$ is a discrete transition of A with $\tau = (q_i, g, C_r, \sigma, \gamma, q'_i)$, $2) \gamma = \top$ or $q_j = \gamma$ for some $j \in \{1, \dots, n\} \setminus \{i\}$, and $3) q'_j = q_j$ and $v'_j = v_j$ for all $j \in \{1, \dots, n\} \setminus \{i\}$.

That is, location guards $\gamma$ are interpreted as disjunctive guards: unless $\gamma = \top$, at least one other process needs to occupy location $\gamma$ in order for process $i$ to pass this guard.

We write $\mathbf{c} \xrightarrow{\delta, (i, \sigma)} \mathbf{c}''$ for a delay transition $\mathbf{c} \xrightarrow{\delta} \mathbf{c}'$ followed by a discrete transition $\mathbf{c}' \xrightarrow{(i, \sigma)} \mathbf{c}''$. Then, a timed path of $A^n$ is a finite sequence $\pi = \mathbf{c}_0 \xrightarrow{\delta_0, (i_0, \sigma_0)} \dots \xrightarrow{\delta_{l-1}, (i_{l-1}, \sigma_{l-1})} \mathbf{c}_l$.

For a timed path $\pi = \mathbf{c}_0 \xrightarrow{\delta_0, (i_0, \sigma_0)} \dots \xrightarrow{\delta_{l-1}, (i_{l-1}, \sigma_{l-1})} \mathbf{c}_l$, let $\delta(\pi) = \sum_{0 \le i < l} \delta_i$ be the total time delay of $\pi$. The definition of timelocks extends naturally to configurations of NGTAs. A timed path $\pi$ of $A^n$ is a computation if $\mathbf{c}_0 = \hat{\mathbf{c}}$. Its length is equal to $2l$.

We write $q \in \mathbf{c}$ if $\mathbf{c} = ((q_1, v_1), \dots, (q_n, v_n))$ and $q = q_i$ for some $i \in \{1, \dots, n\}$, and similarly $(q, v) \in \mathbf{c}$. We say that a location $q$ is reachable in $A^n$ if there exists a reachable configuration $\mathbf{c}$ s.t. $q \in \mathbf{c}$.

**Example 6.** Consider the NGTA $A^3$ where A is the GTA shown in Fig. 1. A computation $\pi$ of this network is depicted in Fig. 2, in which a process reaches error with $\delta(\pi) = 5$. The computation is $((\text{init}, c = 0), (\text{init}, c = 0), (\text{init}, c = 0)) \xrightarrow{1,(1,\sigma_0)} ((\text{listen}, c = 1), (\text{init}, c = 1), (\text{init}, c = 1)) \xrightarrow{3,(1,\sigma_1)} ((\text{post}, c = 0), (\text{init}, c = 4), (\text{init}, c = 4)) \xrightarrow{0,(2,\sigma_3)} ((\text{post}, c = 0), (\text{reading}, c = 0), (\text{init}, c = 4)) \xrightarrow{1,(2,\sigma_5)} ((\text{post}, c = 1), (\text{done}, c = 1), (\text{init}, c = 5)) \xrightarrow{0,(3,\sigma_3)} ((\text{post}, c = 1), (\text{done}, c = 1), (\text{reading}, c = 0)) \xrightarrow{0,(3,\sigma_{\text{err}})} ((\text{post}, c = 1), (\text{done}, c = 1), (\text{error}, c = 0))$. Therefore, error is reachable in $A^3$.

The trace of the timed path $\pi$ is a sequence $\text{trace}(\pi) = (\delta'_0, (i'_0, \sigma'_0)) \dots (\delta'_{l-1}, (i'_{l-1}, \sigma'_{l-1}))$ obtained by removing all discrete transitions $(j, \sigma_j)$ of $\pi$ with $\sigma_j \in \Sigma^-$, and adding all delays of these transitions to the following discrete transition, yielding the $\delta'_j$. The language of $A^n$, denoted $\mathcal{L}(A^n)$, is the set of traces of all of its computations.

**Example 7.** For the computation $\pi$ in Example 6, $\text{trace}(\pi) = (1, (1, \sigma_0)), (3, (1, \sigma_1)), (0, (2, \sigma_3)), (1, (2, \sigma_5)), (0, (3, \sigma_3)), (0, (3, \sigma_{\text{err}}))$.

We will also use *projections* of these global objects onto subsets of the processes. That is, if $\mathbf{c} = ((q_1, v_1), \dots, (q_n, v_n))$ and $\mathcal{I} = \{i_1, \dots, i_k\} \subseteq \{1, \dots, n\}$, then $\mathbf{c}_{\downarrow_{\mathcal{I}}}$ is the tuple $((q_{i_1}, v_{i_1}), \dots, (q_{i_k}, v_{i_k}))$, and we extend this notation to computations $\pi_{\downarrow_{\mathcal{I}}}$ by keeping only the discrete transitions of $\mathcal{I}$ and by adding the delays of the removed discrete transitions to the delay of the following discrete transition of $\mathcal{I}$ (see Appendix A.2 for a full definition).

We introduce a special notation for projecting to a single process and define, for any natural number $1 \le a \le n$, $\pi_{\downarrow a}$ a computation of $\text{UG}(A)$, obtained from $\pi_{\downarrow \{a\}}$ by discarding the index $a$ from all transitions; that is, $\pi_{\downarrow a}$ has the form $(q_0, v_0) \xrightarrow{(\delta'_{k_0}, \sigma_{k_0})} \dots \xrightarrow{(\delta'_{k_m}, \sigma_{k_m})} (q_{m+1}, v_{m+1})$.
We also extend this to traces; that is, trace($\pi$)↓<sub>a</sub> = (δ'<sub>k<sub>0</sub></sub>, σ<sub>k<sub>0</sub></sub>) ... (δ'<sub>k<sub>m</sub></sub>, σ<sub>k<sub>m</sub></sub>), which is a trace of UG(A). For a set of traces L, and set I of processes, we write L↓<sub>I</sub> = {tt↓<sub>I</sub> | tt ∈ L}.

Note that while the projection of a computation is not necessarily a computation itself, since location guards may not be satisfied. What is important for us is that the projection of the language $\mathcal{L}(A^n)$ to a subset $\mathcal{I}$ of processes contains only traces that are a projection $tt↓_\mathcal{I}$, where $tt = \text{trace}(\pi)$ and $\pi$ is a computation of $A^n$.

**Example 8.** For the computation $\pi$ in Example 6, $\pi_{\downarrow 3} = (\text{init}, c = 0) \xrightarrow{(5,\sigma_3)} (\text{reading}, c = 0) \xrightarrow{(0,\sigma_{err})} (\text{error}, c = 0)$ and $\text{trace}(\pi)_{\downarrow 3} = (5, \sigma_3), (0, \sigma_{err})$.

A prefix of a computation $\pi = c_0 \xrightarrow{\delta_0, (i_0, \sigma_0)} \dots \xrightarrow{\delta_{l-1}, (i_{l-1}, \sigma_{l-1})} c_l$, is a sequence $c_0 \xrightarrow{\delta_0, (i_0, \sigma_0)} \dots \xrightarrow{\delta_{l'}, (i_{l'}, \sigma_{l'})} c_{l'}$ with $l' \le l-1$. If $\pi$ is a timed path and $d \in \mathbb{R}_{\ge 0}$, then $\pi^{\le d}$ denotes the maximal prefix of $\pi$ with $\delta(\pi^{\le d}) \le d$, and similarly for timed paths $\rho^{\le d}$ of a single GTA. For timed paths $\pi_1$ of $A^{n_1}$ and $\pi_2$ of $A^{n_2}$ with $\delta(\pi_1) = \delta(\pi_2)$, we denote by $\pi_1 \parallel \pi_2$ their composition into a timed path of $A^{n_1+n_2}$ whose projection to the first $n_1$ processes is $\pi_1$, and whose projection to the last $n_2$ processes is $\pi_2$ (see Appendix A.2).

**Definition 9 (Disjunctive Timed Network).** A given GTA A induces a disjunctive timed network (DTN) $A^\infty$, defined as the following family of NGTAs: $A^\infty = \{A^n \mid n \in \mathbb{N}_{>0}\}$ (we follow the terminology and use abbreviations of [30]). We define $\mathcal{L}(A^\infty) = \bigcup_{n \in \mathbb{N}_{>0}} \mathcal{L}(A^n)$ and consider $\mathcal{L}(A^\infty)_{\downarrow I} = \bigcup_{n \in \mathbb{N}_{>0}} \mathcal{L}(A^n)_{\downarrow I}$.

## 2.1 The Parameterized Model Checking Problem

We formalize properties of DTNs as sets of traces that describe the intended behavior of a fixed number of processes running in a system with arbitrarily many processes. That is, a local property $\varphi$ of $k$ processes, also called a $k$-indexed property, is a subset of $(\mathbb{R}_{\ge 0} \times ([1, k] \times \Sigma))^*$. For $k=1$, for simplicity, we consider it as a subset of $(\mathbb{R}_{\ge 0} \times \Sigma)^*$. We say that $A^n$ satisfies a $k$-indexed local property $\varphi$, denoted $A^n \models \varphi$, if $\mathcal{L}(A^n)_{\downarrow [1,k]} \subseteq \varphi$. Note that, due to the symmetry of the system, it does not matter which $k$ processes we project $\mathcal{L}(A^n)$ onto, so we always project onto the first $k$.

**Parameterized model checking problem (PMCP):**

INPUT: a GTA A and a $k$-indexed local property $\varphi$

PROBLEM: Decide whether $A^n \models \varphi$ holds $\forall n \ge k$.

Local trace properties allow to specify for instance any local safety property of a single process (with $I = [1, 1]$), as well as mutual exclusion properties (with $I = [1, 2]$) and variants of such properties for larger $I$.

PMCP can be solved by checking whether $\mathcal{L}(A^\infty)_{\downarrow [1,k]} \subseteq \varphi$. Our solution consists in building a TA that recognizes $\mathcal{L}(A^\infty)_{\downarrow [1,k]}$. Note that language inclusion is undecidable on TAs [8], but many interesting problems are decidable. These include MITL model checking [20] and simpler problems such as reachability: given symbol $\sigma_0 \in \Sigma$, the reachability PMCP is the PMCP where $\varphi$ is the set of traces that contain an occurrence of $\sigma_0$. Reachability of a location of A can be solved by PMCP by choosing appropriate transition labels.

**Example 10.** In the example of Fig. 1, a natural local property we are interested in is the reachability of the label $\sigma_{err}$. Formally, the local property for process 1 can be written as a 1-indexed property: $(\mathbb{R}_{\ge 0} \times ([1, 1] \times \Sigma))^* \cdot \{(d, (1, \sigma_{err})) \mid d \in \mathbb{R}_{\ge 0}\} \cdot (\mathbb{R}_{\ge 0} \times ([1, 1] \times \Sigma))^*.
3 Model Checking DTNs

3.1 Definitions

We recall here the standard notions of regions and region automata, and introduce the slots
of regions which refer to the intervals of possible valuations of a global clock.

**Regions.** Given $A$, for all $c \in C$, let $M(c)$ denote the maximal bound that $c$ is compared to: $M(c) = \max\{d \in \mathbb{Z} \mid \text{"$c \sim d$"}, "$c - c' \sim d$", "$c' - c \sim d$" appears in a guard or invariant of $A\}$ (we set $M(c) = 0$ if this set is empty). $M$ is called the maximal bound function for $A$. Define $M_{\max} = \max\{M(c) \mid c \in C\}$. We say that two valuations $v$ and $v'$ are equivalent w.r.t. $M$, denoted by $v \approx_M v'$, if the following conditions hold for any clocks $c, c'$ [18, 19]:

1. either $\lfloor v(c) \rfloor = \lfloor v'(c) \rfloor$ or $v(c) > M(c)$ and $v'(c) > M(c)$;

2. if $v(c), v'(c) \le M(c)$ then $\text{frac}(v(c)) = 0 \iff \text{frac}(v'(c)) = 0$;

3. if $v(c) \le M(c)$, $v(c') \le M(c')$ then $\text{frac}(v(c)) \le \text{frac}(v(c')) \iff \text{frac}(v'(c)) \le \text{frac}(v'(c'))$;

4. for any interval $I$ among $(-\infty, -M(c'))$, $[-M(c'), -M(c')]$, $(-M(c'), -M(c') + 1)$, \dots, $[M(c), M(c)]$, $(M(c), \infty)$, we have $v(c) - v(c') \in I \iff v'(c) - v'(c') \in I$.

An *M-region* is an equivalence class of valuations induced by $\approx_M$. We denote by $[v]_M$
the region to which $v$ belongs. We omit $M$ when it is clear from context.

For an *M*-region *r*, if a valuation *v* ∈ *r* satisfies a clock guard *g*, then every valuation in *r* satisfies *g*. We write *r* |= *g* to mean that every valuation in *r* satisfies *g*.

Given an *M*-region *r* and a clock *c*, let $r_{\downarrow c}$ denote the projection of the valuations of *r* to *c*, i.e., $r_{\downarrow c} = \{v(c) \mid v \in r\}$. Given a valuation *v* and a clock *c* ∈ *C*, let $v_{\downarrow -c}$ denote the projection of *v* to the clocks other than *c*, i.e., $v_{\downarrow -c} : C \setminus \{c\} \to \mathbb{R}_{\ge 0}$ is defined by $v_{\downarrow -c}(c') = v(c')$ for all $c' \in C \setminus \{c\}$. By extension, given a region *r* and a clock *c*, let $r_{\downarrow -c} = \{v_{\downarrow -c} \mid v \in r\}$.

**Region Automaton.** The region automaton of a TA $A$ is a finite automaton with alphabet $\Sigma \cup \{\text{delay}\}$, denoted by $\mathcal{R}_M(A)$, defined as follows.

The region states are pairs $(q, r)$ where $q \in Q$ and $r$ is an $M$-region. The initial region state is $(\hat{q}, \hat{r})$ where $\hat{q}$ is the initial location of $A$ and $\hat{r}$ is the singleton region containing $0$.

There is a transition $(q, r) \xrightarrow{\text{delay}} (q, r')$ in $\mathcal{R}_M(A)$ iff there is a transition $(q, v) \xrightarrow{\delta} (q, v')$ in $A$ for some $\delta \in \mathbb{R}_{\ge 0}$, $v \in r$ and $v' \in r'$. We say that $r'$ is a *time successor of* $r$. Note that we can have $r' = r$. Furthermore, $(q, r')$ is the *immediate time successor of* $(q, r)$ if $(q, r) \xrightarrow{\text{delay}} (q, r')$, $r' \neq r$, and whenever $(q, r) \xrightarrow{\text{delay}} (q, r'')$, we have $(q, r') \xrightarrow{\text{delay}} (q, r'')$.

There is a transition $(q, r) \xrightarrow{\sigma} (q', r')$ in $\mathcal{R}_M(A)$ iff there is a transition $(q, v) \xrightarrow{\sigma} (q', v')$ with label $\sigma$ in $A$ for some $v \in r$ and $v' \in r'$. We write $(q, r) \rightarrow (q', r')$ if either $(q, r) \xrightarrow{\text{delay}} (q', r')$ or $(q, r) \xrightarrow{\sigma} (q', r')$ for some $\sigma \in \Sigma$.

A path in $\mathcal{R}_M(A)$ is a finite sequence of transitions $\rho_r = (q_0, r_0) \xrightarrow{\sigma_0} \dots \xrightarrow{\sigma_{n-1}} (q_n, r_n)$ for some $n \ge 0$ where $\sigma_i \in \Sigma \cup \{\text{delay}\}$. A path of $\mathcal{R}_M(A)$ is a computation if it starts from the initial region state.

It is known that $\mathcal{R}_M(A)$ captures the *untimed* traces of $A$, i.e., the projection of the traces of $A$ to $\Sigma$ [8].

**Slots.** Now, we can introduce slots. We will show later that slots are a sufficiently precise abstraction of time for DTNs. In this paragraph, we assume that TAs have a distinguished global clock *t* which is never reset and does not appear in clock guards. We will thus consider a clock set $C \cup \{t\}$ (making *t* appear explicitly for clarity).

Let $N_A$ denote the number of pairs $(q, r)$ where $q \in Q$ and $r$ is an $M$-region (thus a region on the clock set $C$ without $t$). Recall that $N_A$ is exponential in $|C|$ [8, 19]. Let us consider a bound function $M^{\gamma}: C \cup \{t\} \to \mathbb{N}$ for $A$ such that for $c \in C \setminus \{t\}$, $M^{\gamma}(c) = M(c)$, and $M^{\gamma}(t) = 2^{N_A+1}$. Throughout the paper, the bound functions will be denoted by $M^{\gamma}(\cdot)$
whenever the clock set contains the distinguished global clock $t$, and $M(\cdot)$ otherwise. The former will be referred to as $M^{\gamma}$-regions, and the latter as $M$-regions.

We define the slot of an $M^{\gamma}$-region $r$ as $\text{slot}(r) = r_{\downarrow t}$. It is known that for any region $r$ (with any bound function) and clock $c$, $r_{\downarrow c}$ is an interval [29]. Moreover, if $v(c)$ for every $v \in r$ is below the maximal constant $M^{\gamma}(c)$, then $r_{\downarrow c}$ is either a singleton interval of the form $[k, k]$, or an open interval of the form $(k, k+1)$ for some $k \in \mathbb{N}$.

For a slot $s$, let us define next($s$) as follows. **1.** if $s = (k, k+1)$ for some $k \in \mathbb{N}$, then next($s$) = $[k+1, k+1]$; **2.** if $s = [k, k]$ and $k < M^{\gamma}(t)$, then next($s$) = $(k, k+1)$; **3.** if $s = [M^{\gamma}(t), M^{\gamma}(t)]$, then next($s$) = $(M^{\gamma}(t), \infty)$. **4.** if $s = (M^{\gamma}(t), \infty)$ then next($s$) = $s$.

We define the slot of a valuation $v$ on $C \cup \{t\}$ as slot($r$) where $r$ is the (unique) $M^{\gamma}$-region s.t. $v \in r$. Slots, seen as intervals, can be bounded or unbounded.

**Example 11.** Consider the clock set $\{x, y, t\}$ and the region $r$ defined by $\lfloor x \rfloor = \lfloor y \rfloor = 1$, $\lfloor t \rfloor = 2$, $0 < \text{frac}(x) < \text{frac}(y) < \text{frac}(t) < 1$ (with $M^{\gamma}(\cdot) = 4$ for all clocks). Then, slot($r$) = (2, 3).

As a second example, assume $M^{\gamma}(x) = 2$, $M^{\gamma}(y) = 3$ and $M^{\gamma}(t)$ is, say, 2048. Consider the region $r'$ defined by $x > 2 \land \lfloor y \rfloor = 1 \land 0 < \text{frac}(y) < 1 \land \lfloor t \rfloor = 2048 \land \text{frac}(t) = 0$. Then, slot($r$) = [2048, 2048]. In addition, next(slot($r$)) = (2048, $\infty$).

We now introduce the shifting operation which consists of increasing the global clock value, without changing the values of other clocks.

**Lemma 12.** Given any $M^{\gamma}$-region $r$ and $k \in \mathbb{Z}$ such that $\sup(\text{slot}(r)) + k \le M^{\gamma}(t)$, and $\inf(\text{slot}(r)) + k \ge 0$, there exists a $M^{\gamma}$-region $r'$ which satisfies $\text{slot}(r') = \text{slot}(r) + k$ and $r'_{\downarrow -t} = r_{\downarrow -t}$, and $r'$ can be computed in polynomial time in the number of clocks.

The region $r'$ in Lemma 12 will be denoted by $r_{\text{slot}+k}$. We say that it is obtained by shifting the slot by $k$ in $r$. We extend this notation to sets of regions and sets of region states, that is, $W_{\text{slot}+k} = \{(q, r_{\text{slot}+k}) \mid (q, r) \in W\}$ where $W$ is a set of region states. For a set of region states $W$, we define $W_{\downarrow -t} = \{(q, r_{\downarrow -t}) \mid (q, r) \in W\}$.

**Example 13.** Consider the clock set $\{x, y, t\}$ and the region $r$ defined in Example 11 satisfying $\lfloor x \rfloor = \lfloor y \rfloor = 1$, $\lfloor t \rfloor = 2$, $0 < \text{frac}(x) < \text{frac}(y) < \text{frac}(t) < 1$ (with $M^{\gamma}_{\max} = 4$). Then, slot($r$) = (2, 3), and $r_{\text{slot}+1}$ is defined by the same constraints as above except that $\lfloor t \rfloor = 3$, and slot($r_{\text{slot}+1}$) = (3, 4).

**Remark 14.** Recall that given a bound function, the number of regions is $O(|C|!2^{|C|}M_{\max}^{|C|})$ since regions determine an order of the fractional values of clocks, the subsets of clocks that have integer values, and an integral value for each clock [18]. The number of $M^{\gamma}$-regions is $O(|C|!2^{|C|}(M^{\gamma}(t))^{|C|})$, which is doubly exponential in $|C|$ since $M^{\gamma}(t)$ is.

Crucial to our paper, however, is that the set of projections $r_{\downarrow -t}$ of the set of $M^{\gamma}$-regions $r$ has size exponential only. This can be seen as follows: our definition of regions from [18] uses a distinct maximum bound function for each clock. Thus, when constraints on $t$ are eliminated, there only remain constraints on clocks $c \in C \setminus \{t\}$, with maximal constants $M(c)$ as in the original GTA A. We thus fall back to the set of regions of A of size $O(|C|!2^{|C|}M_{\max}^{|C|})$.

## 3.2 Layer-based Algorithm for the DTN Region Automaton

We describe here an algorithm to compute a TA $S(A)$ that recognizes the language $L(A^{\infty})_{\downarrow 1}$. We explain at the end of the section how to generalize the algorithm to compute $L(A^{\infty})_{\downarrow I}$ for an interval $I = [1, a]$ for $a \ge 1$.
1:10 Parameterized Verification of Timed Networks with Clock Invariants

<figure><img src="image_6.png" /><figcaption>Figure 4 An overview of data structures in the paper</figcaption></figure>

► **Assumption 1.** We assume that the given GTA *A* is timelock-free, regardless of location guards. Formally, let *A'* be obtained from *A* by removing all transitions with non-trivial location guards. We require that no configuration of *A'* has a timelock.

Note that this assumption guarantees that $A^n$ will be timelock-free for all $n$. Assuming timelock-freeness is not restrictive since a protocol cannot possibly block the physical time: time will elapse regardless of the restrictions of the design. A network with a timelock is thus a design artifact, and just means the model is incomplete. An incomplete model can be completed by adding a sink location to which processes that would cause a timelock can move, and regarding reachability the resulting model is equivalent to the original one.

<figure><img src="image_7.png" /><figcaption>Figure 3 A GTA with timelock due to location guards.</figcaption></figure>

► **Example 15.** The GTA in Fig. 3 does not satisfy Assumption 1, since $A'$ (where we remove transitions with non-trivial location guards) has a timelock at $(q_1, c = 1)$.

The following assumption simplifies the proofs:

► **Assumption 2.** Each transition of GTA *A* is labeled by a unique label different from $\epsilon$.

Consider a GTA *A*. Our algorithm builds a TA capturing the language $\mathcal{L}(A^\infty)\downarrow_1$. The construction is based on $M'\text{-region}$ states of $UG(A)$; however, not all transitions of the region automaton of $UG(A)$ are to be added since location guards mean that some transitions are not enabled at a given region. Unless otherwise stated, by region states we mean $M'\text{-region}$ states. The steps of the construction are illustrated in Fig. 4. From *A*, we first obtain $UG(A)$, and build the region automaton for $UG(A)$, denoted by $\mathcal{R}_{M'}(UG(A))$. Then Algorithm 1 builds the so-called *DTN region automaton* $\mathcal{D}(A)$ which is a finite automaton. Finally we construct $\mathcal{S}(A)$ which we refer to as the *summary timed automaton*, a timed automaton derived from $\mathcal{D}(A)$ by adding clocks and clock guards to $\mathcal{D}(A)$. Our main result is that $\mathcal{S}(A)$ recognizes the language $\mathcal{L}(A^\infty)\downarrow_1$.

Intuitively, Algorithm 1 computes region states reachable by a single process within the context of a network of arbitrary size. These region states are partitioned according to their slots. More precisely, Algorithm 1 computes (lines 3-4) the sequence $(W_i, E_i)_{i \ge 0}$, where $W_i$ is a set of $M'$-region states of $UG(A)$ having the same slot (written $\text{slot}(W_i)$), and $E_i$ is a set of transitions from region states of $W_i$ to either $W_i$ or $W_{i+1}$. These transitions include $\epsilon$-transitions which correspond to delay transitions: if the slot does not change during the delay transition, then the transition goes to a region-state which is also in $W_i$; otherwise, it leaves to the next slot and the successor is in $W_{i+1}$. During discrete transitions from $W_i$, the slot does not change, so the successor region-states are always inside $W_i$. In order to check if a discrete transition with location guard $\gamma$ must be considered, the algorithm checks if some region-state $(\gamma, r_\gamma)$ was previously added to the *same layer* $W_i$. This means that some (other) process can be at $\gamma$ somewhere at a global time that belongs to $\text{slot}(W_i)$. This is the nontrivial part of the algorithm: the proof will establish that if a process can be at location $\gamma$ at *some time* in a given slot $s$, then it can also be at $\gamma$ at *any time* within $s$.

For two sets $W_i, W_j$ of region states of $UG(A)$, let us define $W_i \approx W_j$ iff $W_j$ can be obtained from $W_i$ by shifting the slot, that is, if there exists $k \in \mathbb{Z}$ such that $(W_i)_{\text{slot}+k} = W_j$.
**Algorithm 1** Algorithm to compute DTN region automaton of GTA A.

input : GTA A = (Q, ˆq, C, Σ, T, Inv) and $\mathcal{R}_{M'}$(UG(A))

output : The DTN region automaton of A

1 Initialize $s \leftarrow [0, 0], W_0 \leftarrow \{(\hat{q}, \hat{r})\}, E_0 \leftarrow \emptyset, l \leftarrow -1$

2 repeat

3 $l \leftarrow l + 1$;

4 Compute $(W_l, E_l)$ by applying the following rules until a fixed point is reached:

■ Rule 1: For any $(q, r) \in W_l$, let $(q, r) \xrightarrow{\text{delay}} (q, r')$ s.t. $\text{slot}(r') = s$, do

$W_l \leftarrow W_l \cup \{(q, r')\}$, and $E_l \leftarrow E_l \cup \{((q, r), \epsilon, (q, r'))\}$.

■ Rule 2: For any $(q, r) \in W_l$ and $\tau = (q, g, C_r, \sigma, \gamma, q')$ s.t. $(q, r) \xrightarrow{\sigma} (q', r')$, if $\gamma = \top$, or if there exists $(\gamma, r_\gamma) \in W_l$,

then do $W_l \leftarrow W_l \cup \{(q', r')\}$, and $E_l \leftarrow E_l \cup \{((q, r), \sigma, (q', r'))\}$
$s \leftarrow \text{next}(s)$;

$W_{l+1} \leftarrow \{(q, r') | (q, r) \in W_l, (q, r) \xrightarrow{\text{delay}} (q, r') \text{ and } \text{slot}(r') = s\}$;

$E_l \leftarrow E_l \cup \{((q, r), \epsilon, (q, r')) | (q, r) \in W_l, (q, r) \xrightarrow{\text{delay}} (q, r') \wedge \text{slot}(r') = s\}$;

5 **until** $\exists i_0 < l : W_l \approx W_{i_0}$, and $\text{slot}(W_{i_0})$ is a singleton;

6 $l_0 \leftarrow l$;

7 $E_{l_0-1} \leftarrow E_{l_0-1} \cap (W_{l_0-1} \times \Sigma \times W_{l_0-1}) \cup$

$$ \left\{ ((q, r), \epsilon, (q, r')) \middle| (q, r') \in W_{i_0}, \exists r'', \exists k \in \mathbb{N}, ((q, r), \epsilon, (q, r'')) \in E_{l_0-1} \cap (W_{l_0-1} \times \Sigma \times W_{l_0}), r'_{\text{slot}+k} = r'' \right\} $$

8 $W \leftarrow \cup_{0 \le i \le l_0-1} W_i$, $E \leftarrow \cup_{0 \le i \le l_0-1} E_i$

9 **return** $(\bar{W}, (\hat{q}, \hat{r}), \Sigma, E)$

Recall that $(W_i)_{\text{slot}+k} = W_j$ means that both sets contain the same regions when projected to the local clocks $C \setminus \{t\}$. This definition is of course symmetric.

Algorithm 1 stops (line 5) when $W_{i_0} \approx W_{l_0}$ for some $i_0 < l_0$ with both layers having singleton slots (this requirement could be relaxed but this simplifies the proofs and only increases the number of iterations by a factor of 2).

The algorithm returns the DTN region automaton $\mathcal{D}(A) = (W, (\hat{q}, \hat{r}), \Sigma, E)$, where W is the set of explored region states, and E is the set of transitions that were added; except that transitions leaving $W_{l_0-1}$ are redirected back to $W_{i_0}$ (lines 7-9). Redirecting such transitions means that whenever $\mathcal{R}_{M'}(\text{UG}(A))$ has a delay transition from $(q, r)$ to $(q, r')$ with $\text{slot}(r) = \text{slot}(W_{l_0-1})$ and $\text{slot}(r') = \text{slot}(W_{l_0})$, then we actually add a transition from $(q, r)$ to $(q, r'')$, where $r''$ is obtained from $r'$ by shifting the slot to that of $\text{slot}(W_{i_0})$; this means that $r' \downarrow_{-t} = r'' \downarrow_{-t}$, so these define the same clock valuations except with a shifted slot. The property $W_{i_0} \approx W_{l_0}$ ensures that $(q, r'') \in W_{i_0}$.

We write $(q, r) \xrightarrow{\sigma} (q', r')$ iff $((q, r), \sigma, (q', r')) \in E$. Paths and computations are defined for the DTN region automaton analogously to region automata.

We now show how to construct the summary timed automaton $\mathcal{S}(A)$ (the step from $\mathcal{D}(A)$ to $\mathcal{S}(A)$ in Fig. 4). We define $\mathcal{S}(A)$ by extending $\mathcal{D}(A)$ with the clocks of A. Moreover, each transition $((q, r), \epsilon, (q, r'))$ has the guard $r' \downarrow_{-t}$ and no reset; and each transition $((q, r), \sigma, (q', r'))$ with $\sigma \neq \epsilon$ has the guard $r \downarrow_{-t}$, and resets the clocks that are equal to 0 in $r'$. The intuition is that $\mathcal{S}(A)$ ensures by construction that any valuation that is to take a discrete transition $(\sigma \neq \epsilon)$ at location $(q, r)$ belongs to $r$. Notice that we omit invariants here. Because transitions are derived from those of $\mathcal{R}_{M'}(\text{UG}(A))$, the only additional behavior we can have in $\mathcal{S}(A)$ due to the absence of invariants is a computation delaying in a location
1:12 Parameterized Verification of Timed Networks with Clock Invariants

450

451

452

$(q, r)$ and reaching outside of $r$ (without taking an $\epsilon$-transition), while no discrete transitions
can be taken afterwards. Because traces end with a discrete transition, this does not add
any trace not possible in $\mathcal{L}\downarrow_1(A^\infty)$.

453

**3.2.1 Properties of Algorithm 1**

454

455

We explain the overview of the correctness argument for Algorithm 1 and some of its
consequences (See Appendix B.2).

456

457

458

Let us first prove the termination of the algorithm, which also yields a bound on the
number of iterations of the main loop (thus on $l_0$ and $i_0$). Recall that for a given $A$, $N_A$
denotes the number of pairs $(q, r)$ where $q \in Q$ and $r$ is an $M$-region (see Section 3.1).

459

460

461

**► Lemma 16.** Let $\mathcal{D}(A)$ be a DTN region automaton returned by Algorithm 1. Then the slots of all region states in $\mathcal{D}(A)$ are bounded. Consequently, the number of iterations of Algorithm 1 is bounded by $2^{N_A+1}$.

462

463

464

465

The region automaton is of exponential size. Each iteration of Algorithm 1 takes
exponential time since one might have to go through all region states in the worst case. By
Lemma 16, the number of iterations is bounded by $2^{N_A}$, which is doubly exponential in $|\mathcal{C}|$.
Theorem 21 will show how to decide the reachability PMCP in exponential space.

466

We now prove the correctness of the algorithm in the following sense.

467

468

**► Theorem 17.** Let $A$ be a GTA, $\mathcal{D}(A) = (W, (\hat{q}, \hat{r}), \Sigma, E)$ its DTN region automaton, $S(A)$ be the summary timed automaton. Then we have $\mathcal{L}(A^\infty)\downarrow_1 = \mathcal{L}(S(A))$.

470

471

472

473

To prove this, we need the following lemma that states a nontrivial property on which
we rely: if a process can reach a given location $q$ at global time $t'$, then it can also reach $q$
at any global time within the slot of $t'$. It follows that the set of global times at which a
location can be occupied by at least one process is a union of intervals. Intuitively, this is
why partitioning the region states by slots is a good enough abstraction in our setting.

474

475

476

477

**► Lemma 18.** Consider a GTA $A$ with bound function $M'$. Let $\rho_r = (q_0, r_0) \xrightarrow{\sigma_0} \dots \xrightarrow{\sigma_{l-1}} (q_l, r_l)$ such that $(q_0, r_0) = (\hat{q}, \hat{r})$ be a computation in $\mathcal{R}_{M'}(\text{UG}(A))$ such that slot$(r_l)$ is bounded. For all $t' \in \text{slot}(r_l)$, there exists a timed computation $(q_0, v_0) \to \dots \to (q_l, v_l)$ in UG$(A)$ such that $v_i \in r_i$ for $0 \le i \le l$, and $v_l(t) = t'$.

478

The following lemma proves one direction of Theorem 17.

479

480

**► Lemma 19.** Consider a trace $tt = (\delta_0, \sigma_0) \dots (\delta_{l-1}, \sigma_{l-1}) \in \mathcal{L}(S(A))$. Let $I$ be the unique interval of the form $[k, k]$ or $(k, k+1)$ with $k \in \mathbb{N}$ that contains $\delta_0 + \dots + \delta_{l-1}$.

481

482

1. For all $t' \in I$, there exists $n \in \mathbb{N}$, and a computation $\pi$ of $A^n$ such that $\text{trace}(\pi)\downarrow_1 = (\delta'_0, \sigma_0) \dots (\delta'_{l-1}, \sigma_{l-1})$ for some $\delta'_i \ge 0$, and $\delta(\pi\downarrow_1) = t'$.

483

2. $tt \in \mathcal{L}(A^\infty)\downarrow_1$.

484

485

486

487

The following lemma establishes the inclusion in the other direction. Given a computation
$\pi$ in $A^n$, we build a timed computation in $S(A)$ on the same trace. Because the total time
delay of $\pi$ can be larger than the bound $2^{N_A}$, we need to carefully calculate the slot in which
they will end when projected to $S(A)$.

488

**► Lemma 20.** For any computation $\pi$ of $A^n$ with $n \in \mathbb{N}$, $\text{trace}(\pi)\downarrow_1 \in \mathcal{L}(S(A))$.

489

490

491

492

**Deciding the Reachability PMCP.** It follows from Algorithm 1 that the reachability
case can be decided in exponential space. This basically consists of running the main loop of
Algorithm 1 without storing the whole list of all $W_i$, but only the last one. The loop needs
to be repeated up to $2^{N_A+1}$ times (or until the target label $\sigma_0$ is found).
► **Theorem 21.** *The reachability PMCP for DTNs is decidable in EXPSPACE.*

493

**Local Properties Involving Several Processes.** The algorithm described above can be extended to compute $\mathcal{L}(A^\infty)\downarrow_{[1,a]}$. We define the product of $k$ timed automata $A_i$, written $\otimes_{1\le i\le k} A_i$, as the standard product of timed automata (see e.g., [15]) applied to $A_i$ after replacing each label $\sigma$ appearing in $A_i$ by $(i, \sigma)$.

494

495

496

497

► **Lemma 22.** *Given GTA A, and interval $I = [1, a]$, let $S(A)$ be the summary automaton computed as above. Then $\mathcal{L}(A^\infty)\downarrow_I = \mathcal{L}(\otimes_{1\le i\le a} S(A))$.*

498

499

**Limitations.** Liveness properties (e.g., checking whether a transition can be taken an infinite number of times) are not preserved by our abstraction; since an infinite loop in the DTN region automaton may not correspond to a concrete computation in any $A^n$. In fact, consider the GTA in Fig. 5. While there is an infinite loop on $\hat{q}$ in the DTN region automaton, no concrete execution takes the loop on $\hat{q}$ indefinitely, as each firing of this loop needs one more process to visit $q_1$, and then to leave it forever, due to the invariant $c \le 0$.

500

501

502

503

504

505

506

507

508

<figure><img src="image_8.png" /><figcaption>■ **Figure 5** An example of GTA for which liveness is not preserved by our abstraction.</figcaption></figure>

## 4 Timed Lossy Broadcast Networks

509

Systems with lossy broadcast (a.k.a. “reconfigurable broadcast networks”, where the underlying network topology might change arbitrarily at runtime) have received attention in the parameterized verification literature [21]. In the setting with finite-state processes, lossy broadcast is known to be at least as powerful as disjunctive guards, but it is unknown if it is strictly more powerful [14, Section 6]. We show that in our timed setting the two models are equally powerful, i.e., they simulate each other. Details are given in Appendix B.3.

510

511

512

513

514

515

**Lossy Broadcast Networks.** Let $\Sigma$ be a set of labels. A lossy broadcast timed automaton (LBTA) $B$ is a tuple $(Q, \hat{q}, \mathcal{C}, \Sigma, \Lambda, \mathcal{T}, \mathit{Inv})$ where $Q, \hat{q}, \mathcal{C}, \mathit{Inv}$ are as for TAs, and a transition is of the form $(q, g, \mathcal{C}_r, \sigma, \lambda, q')$, where $\lambda \in \{a!!, a?? | a \in \Lambda\}$. The synchronization label $\lambda$ is used for defining global transitions. A transition with $\lambda = a!!$ is called a *sending transition*, and a transition with $\lambda = a??$ is called a *receiving transition*.

516

517

518

519

520

521

We also make Assumption 1 and Assumption 2 for LTBAs. The former means that the LBTA is timelock-free when all receiving transitions are removed. The semantics of a network of LBTAs is a timed transition system defined similarly as for NGTAs, except for *discrete transitions* which now induce a sequence of local transitions separated by 0 delays, as follows. Given $n > 0$, configurations of $B^n$ are defined as for DTNs. Let $\mathcal{C} = ((q_1, v_1), \dots, (q_n, v_n))$ be a configuration of $B^n$. Consider indices $1 \le i \le n$ and $J \subseteq \{1, \dots, n\} \setminus \{i\}$, and labels $\sigma, \sigma_j \in \Sigma$ for $j \in J$, such that $i) (q_i, v_i) \xrightarrow{a^{!!}, \sigma} (q'_i, v'_i)$ is a sending transition of $B$, and $ii) \text{ for all } j \in J$: $(q_j, v_j) \xrightarrow{a^{??}, \sigma_j} (q'_j, v'_j)$ is a receiving transition of $B$. Then the timed transition system of $B^n$ contains the transition sequence $\mathcal{C} \xrightarrow{(0,(i,\sigma))} \mathcal{C}' \xrightarrow{(0,(j_1,\sigma_{j_1}))} \mathcal{C}'_1 \xrightarrow{(0,(j_2,\sigma_{j_2}))} \dots \xrightarrow{(0,(j_m,\sigma_{j_m}))} \mathcal{C}'_m$ for all possible sequences $j_1, \dots, j_m$ where $J = \{j_1, \dots, j_m\}$. Non-zero delays only occur outside of these chains of 0-delay transitions. For a given LBTA $B$, the family of systems $B^\infty$ is called a *lossy broadcast timed network* (LBTN).

522

523

524

525

526

527

528

529

530

531

532

533

534

535

536

**Simulating LBTN by DTN (and vice versa).** The following theorem states that LBTAs and GTAs are inter-reducible.

537

538

► **Theorem 23.** *For all GTA A, there exists an LBTA B s.t. $\forall k \ge 1$, $\mathcal{L}(A^\infty)\downarrow_{[1,k]} \equiv \mathcal{L}(B^\infty)\downarrow_{[1,k]}$. For all LBTA B, there exists a GTA A s.t. $\forall k \ge 1$, $\mathcal{L}(A^\infty)\downarrow_{[1,k]} = \mathcal{L}(B^\infty)\downarrow_{[1,k]}$.*

539

540
1:14 Parameterized Verification of Timed Networks with Clock Invariants

537

538

539

**Sketch.** Simulation of disjunctive guards by lossy broadcast is simple: a transition from $q$ to $q'$ with location guard $\gamma$ is simulated in lossy broadcast by the sender taking a self-loop transition on $\gamma$, and the receiver having a synchronizing transition from $q$ to $q'$.

540

541

542

543

544

545

The other direction is where we need the power of clock invariants: to simulate a lossy broadcast where the sender moves from $q$ to $q'$ and a receiver moves from $q_{rcv}$ to $q'_{rcv}$, in the DTN we first let the sender move to an auxiliary location $q_{\sigma}$ (from which it can later move on to $q'$), and have a transition from $q_{rcv}$ to $q'_{rcv}$ that is guarded with $q_{\sigma}$. To ensure that no time passes between the steps of sender and receiver, we add an auxiliary clock $c_{snd}$ that is reset when moving into $q_{\sigma}$, and $q_{\sigma}$ has clock invariant $c_{snd} = 0$.

546

547

In both directions, auxiliary transitions that are only needed for the simulation are labeled with fresh symbols in $\Sigma^{-}$ such that they do not appear in the language of the system. $\quad$

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

548

Because the reduction to DTNs is in linear-time, we get the following.

549

**► Corollary 24.** The reachability PMCP for LBTN is decidable in EXPSPACE.

550

5 Synchronizing Timed Networks and Timed Petri Nets

551

552

553

We first introduce synchronizing timed networks. Our definitions follow [6, 5], except that their model considers systems with a controller process, whereas we assume (like in our previous models) that all processes execute the same automaton.

554

555

556

557

**Synchronizing Timed Network.** A synchronizing timed automaton (STA) $\mathcal{S}$ is a tuple $(Q, \hat{q}, \mathcal{C}, \text{Inv}, \mathcal{R})$ where $Q, \hat{q}, \mathcal{C}, \text{Inv}$ are as for TAs, and $\mathcal{R}$ is a finite set of rules, where each rule $r \in \mathcal{R}$ is of the form $\langle q_{r,1} \xrightarrow{g_{r,1}, \mathcal{C}_{r,1}, \sigma_{r,1}} q'_{r,1}, \dots, q_{r,m} \xrightarrow{g_{r,m}, \mathcal{C}_{r,m}, \sigma_{r,m}} q'_{r,m} \rangle$ for some $m \in \mathbb{N}$ and with $(q_i, g_{r,i}, \mathcal{C}_{r,i}, \sigma_{r,i}, q'_i) \in Q \times \Psi(\mathcal{C}) \times 2^C \times \Sigma \times Q$ for $1 \le i \le m$.

558

559

560

561

562

563

The semantics of a network of STAs (NSTA) is defined as for NGTAs, except for discrete transitions, which now synchronize a subset of all processes in the following way: Let $r \in \mathcal{R}$ be a rule (of the form described above) and $c = ((q_1, v_1), \dots, (q_n, v_n))$ a configuration of $\mathcal{S}^n$. Assume i) there exists an injection $h : \{1, \dots, m\} \to \{1 \dots n\}$ such that for each $1 \le i \le m$, $q_{h(i)} = q_{r,i}$, $q_{h(i)} \xrightarrow{g_{r,i}, \mathcal{C}_{r,i}, \sigma_{r,i}} q'_{h(i)}$ is an element of $r$, $v_{h(i)} \models q_{r,i}$ and $v'_{h(i)} = v_{h(i)}[\mathcal{C}_{r,i} \leftarrow 0]$, and ii) $j \notin \text{range}(h)$, $q'_j = q_j$ and $v'_j = v_j$. Then the timed transition system of $\mathcal{S}^n$ contains the transition sequence $c \xrightarrow{(0,(h(1),\sigma_{r,1}))} c_1 \xrightarrow{(0,(h(2),\sigma_{r,2}))} \dots \xrightarrow{(0,(h(m),\sigma_{r,m}))} c_m$. That is, $m$ distinct processes take individual transitions according to the rule without delay, and the configurations of the non-participating processes remain unchanged.

564

565

566

567

568

569

570

Again, we also make Assumption 1 and Assumption 2 for STAs. The former means here that $\mathcal{S}$ is timelock-free when all transitions of rules with $m > 1$ are removed. All other notions follow in the natural way. Given an STA $\mathcal{S}$, the family of systems $\mathcal{S}^{\infty}$ is called a synchronizing timed network (STN).

571

572

573

574

**► Theorem 25.** For all GTA A with set of locations $Q$, there exists an STA $\mathcal{S}$ with set of locations $Q$ such that for every $q \in Q$: $q$ is reachable in A iff $q$ is reachable in $\mathcal{S}$. For all STA $\mathcal{S}$ with set of locations $Q_{\mathcal{S}}$, there exists a GTA A with set of locations $Q_{A} \supseteq Q_{\mathcal{S}}$ such that for every $q \in Q_{\mathcal{S}}$: $q$ is reachable in A iff $q$ is reachable in $\mathcal{S}$.

575

576

577

**Sketch.** Simulation of disjunctive guards by STAs is simple: a transition from $q$ to $q'$ with location guard $\gamma$ is simulated by a pairwise synchronization, where one process takes a self-loop on $\gamma$, and the other moves from $q$ to $q'$.

578

579

580

Conversely, to simulate a rule $r$ of the STA with $m$ participating processes, we add auxiliary locations $p_{r,i}$, for $1 \le i \le m$, each with a clock invariant (on an additional clock only used for the simulation) that ensures that no time passes during simulation. For each
<table><caption>**Table 1** Existing and new decidability results for location reachability (Reach) and local trace properties (Trace) for DTN, LBTN, and STN with a single (|C| = 1) or multiple clocks (|C| > 1), and with (Inv) or without invariants (Inv). Entries with ✓* need to satisfy Assumption 1.</caption><thead><tr><th rowspan="2"></th><th colspan="3">DTN</th><th colspan="3">LBTN</th><th colspan="3">STN</th></tr><tr><th>|C|=1</th><th>|C|>1</th><th>|C|>1</th><th>|C|=1</th><th>|C|>1</th><th>|C|>1</th><th>|C|=1</th><th>|C|>1</th><th>|C|>1</th></tr></thead><tbody><tr><td></td><td>Inv</td><td>Inv</td><td>Inv</td><td>Inv</td><td>Inv</td><td>Inv</td><td>Inv</td><td>Inv</td><td>Inv</td></tr><tr><td>Reach</td><td>✓[30]</td><td>✓[30]</td><td>✓</td><td>✓[6, 11]</td><td>✓</td><td>✓</td><td>✓[6]</td><td>✓</td><td>✓</td></tr><tr><td>Trace</td><td>✓[30]</td><td>✓[30]</td><td>✓*</td><td>✓</td><td>✓</td><td>✓*</td><td>?</td><td>?</td><td>?</td></tr></tbody></table>

element $q_{r,i} \xrightarrow{g_{r,i}, C_{r,i}, \sigma_{r,i}} q'_{r,i}$ of $r$, we have a transition from $q_{r,i}$ to $p_{r,i}$, and from there to $q'_{r,i}$. A transition to $p_{r,i}$ is guarded with $p_{r,i-1}$ (except when $i = 1$), and with the clock constraint $g_{r,i}$, and all transitions to $q'_{r,i}$ are guarded with $p_{r,m}$. This ensures that any $q'_{r,i}$ is reachable through this construction if and only if the global configuration at the beginning would allow the STA to execute rule $r$. To avoid introducing timelocks, each of the $p_{r,i}$ has an additional transition with a trivial location guard and no clock guard to a new sink location $q_⊥$ that does not have an invariant. I.e., if simulation of a rule is started but cannot be completed (because there are processes in some but not all of the locations $q_{r,i}$), then processes can (and have to) move to $q_⊥$. A full proof can be found in Appendix B.4. ◀

**Corollary 26.** *The reachability PMCP for STN is decidable in EXPSPACE.*

Note that the construction in our proof is in general not suitable for language equivalence, i.e., $\mathcal{L}(A^\infty)\downarrow_{[1,k]}$ might contain traces that are not in $\mathcal{L}(S^\infty)\downarrow_{[1,k]}$.

Abdulla et al. [2] considered the universal safety problem of timed Petri nets — that is, whether a given transition can eventually be fired for any number of tokens in the initial place — and solved it for the case where each token has a single clock. The question whether the problem is decidable for tokens with multiple clocks remained open. This problem, in the multi-clock setting, can be reduced to the PCMP of STNs. The reduction is conceptually straightforward and computable in polynomial time in the size of the input.

**Corollary 27.** *The universal safety problem for timed Petri nets with an arbitrary number of clocks is decidable in EXPSPACE.*

# 6 Conclusion

In this paper, we solved positively the parameterized model checking problem (PMCP) for finite local trace properties of disjunctive timed networks (DTNs) with invariants. We also proved that the PMCP for networks that communicate via lossy broadcast can be reduced to the PMCP for DTNs, and is therefore decidable. Additional results also allowed us to solve positively the open problem from [2] whether the universal safety problem for timed Petri nets with multiple clocks is decidable. Table 1 gives an overview of our results, compared to existing results for the classes of systems we consider.

In addition to the results presented here, we believe that our proof techniques can be extended to support timed networks with more powerful communication primitives, and in some cases to networks with controllers.

Future work will include tightening the complexity bounds for the problems considered here, as well as the development of zone-based algorithms that can be more efficient in practice than a direct implementation of the algorithms presented here.
1:16 Parameterized Verification of Timed Networks with Clock Invariants

References

1 Abdulla, P.A., Atig, M.F., Cederberg, J.: Timed lossy channel systems. In: D’Souza, D., Kavitha, T., Radhakrishnan, J. (eds.) FSTTCS. LIPIcs, vol. 18, pp. 374–386. Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2012). https://doi.org/10.4230/LIPICS.FSTTCS.2012.374

2 Abdulla, P.A., Atig, M.F., Ciobanu, R., Mayr, R., Totzke, P.: Universal safety for timed Petri nets is PSPACE-complete. In: Schewe, S., Zhang, L. (eds.) CONCUR. LIPIcs, vol. 118, pp. 6:1–6:15. Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2018). https://doi.org/10.4230/LIPICS.CONCUR.2018.6

3 Abdulla, P.A., Delzanno, G.: Parameterized verification. International Journal on Software Tools for Technology Transfer **18**(5), 469–473 (2016). https://doi.org/10.1007/s10009-016-0424-3

4 Abdulla, P.A., Delzanno, G., Rezine, O., Sangnier, A., Traverso, R.: Parameterized verification of time-sensitive models of ad hoc network protocols. Theoretical Computer Science **612**, 1–22 (2016). https://doi.org/10.1016/j.tcs.2015.07.048

5 Abdulla, P.A., Deneux, J., Mahata, P.: Multi-clock timed networks. In: LiCS. pp. 345–354. IEEE Computer Society (2004). https://doi.org/10.1109/LICS.2004.1319629

6 Abdulla, P.A., Jonsson, B.: Model checking of systems with many identical timed processes. Theoretical Computer Science **290**(1), 241–264 (2003). https://doi.org/10.1016/S0304-3975(01)00330-9

7 Abdulla, P.A., Sistla, A.P., Talupur, M.: Model checking parameterized systems. In: Clarke, E.M., Henzinger, T.A., Veith, H., Bloem, R. (eds.) Handbook of Model Checking, pp. 685–725. Springer (2018). https://doi.org/10.1007/978-3-319-10575-8_21

8 Alur, R., Dill, D.L.: A theory of timed automata. Theoretical Computer Science **126**(2), 183–235 (Apr 1994). https://doi.org/10.1016/0304-3975(94)90010-8

9 Aminof, B., Kotek, T., Rubin, S., Spegni, F., Veith, H.: Parameterized model checking of rendezvous systems. Distributed Computing **31**(3), 187–222 (2018). https://doi.org/10.1007/s00446-017-0302-6

10 Aminof, B., Rubin, S., Zuleger, F., Spegni, F.: Liveness of parameterized timed networks. In: Halldórsson, M.M., Iwama, K., Kobayashi, N., Speckmann, B. (eds.) ICALP, Part II. Lecture Notes in Computer Science, vol. 9135, pp. 375–387. Springer (2015). https://doi.org/10.1007/978-3-662-47666-6_30

11 André, É., Delahaye, B., Fournier, P., Lime, D.: Parametric timed broadcast protocols. In: Enea, C., Piskac, R. (eds.) VMCAI. Lecture Notes in Computer Science, vol. 11388, pp. 491–512. Springer (2019). https://doi.org/10.1007/978-3-030-11245-5_23

12 André, É., Eichler, P., Jacobs, S., Karra, S.L.: Parameterized verification of disjunctive timed networks. In: Dimitrova, R., Lahav, O. (eds.) VMCAI. Lecture Notes in Computer Science, vol. 14499, pp. 124–146. Springer (2024). https://doi.org/10.1007/978-3-031-50524-9_6

13 Apt, K.R., Kozen, D.: Limits for automatic verification of finite-state concurrent systems. Information Processing Letters **22**(6), 307–309 (1986). https://doi.org/10.1016/0020-0190(86)90071-2

14 Balasubramanian, A.R., Weil-Kennedy, C.: Reconfigurable broadcast networks and asynchronous shared-memory systems are equivalent. In: Ganty, P., Bresolin, D. (eds.) GandALF. EPTCS, vol. 346, pp. 18–34 (2021). https://doi.org/10.4204/EPTCS.346.2

15 Bengtsson, J., Yi, W.: Timed automata: Semantics, algorithms and tools. In: Desel, J., Reisig, W., Rozenberg, G. (eds.) Lectures on Concurrency and Petri Nets, Advances in Petri Nets. Lecture Notes in Computer Science, vol. 3098, pp. 87–124. Springer (2003). https://doi.org/10.1007/978-3-540-27755-2_3

16 Bertrand, N., Fournier, P.: Parameterized verification of many identical probabilistic timed processes. In: Seth, A., Vishnoi, N.K. (eds.) FSTTCS. LIPIcs, vol. 24, pp. 501–513. Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2013). https://doi.org/10.4230/LIPIcs.FSTTCS.2013.501
17 Bloem, R., Jacobs, S., Khalimov, A., Konnov, I., Rubin, S., Veith, H., Widder, J.: Decidability of Parameterized Verification. Synthesis Lectures on Distributed Computing Theory, Morgan & Claypool Publishers (2015). https://doi.org/10.2200/S00658ED1V01Y201508DCT013

18 Bouyer, P., Dufourd, C., Fleury, E., Petit, A.: Are timed automata updatable? In: Emerson, E.A., Sistla, A.P. (eds.) CAV. Lecture Notes in Computer Science, vol. 1855, pp. 464–479. Springer (2000). https://doi.org/10.1007/10722167_35

19 Bouyer, P., Dufourd, C., Fleury, E., Petit, A.: Updatable timed automata. Theoretical Computer Science 321(2-3), 291–345 (Aug 2004). https://doi.org/10.1016/j.tcs.2004.04.003

20 Bouyer, P., Fahrenberg, U., Larsen, K.G., Markey, N., Ouaknine, J., Worrell, J.: Model checking real-time systems. In: Clarke, E.M., Henzinger, T.A., Veith, H., Bloem, R. (eds.) Handbook of Model Checking, pp. 1001–1046. Springer (2018). https://doi.org/10.1007/978-3-319-10575-8_29

21 Delzanno, G., Sangnier, A., Zavattaro, G.: Parameterized verification of ad hoc networks. In: Gastin, P., Laroussinie, F. (eds.) CONCUR. Lecture Notes in Computer Science, vol. 6269, pp. 313–327. Springer (2010). https://doi.org/10.1007/978-3-642-15375-4_22

22 Emerson, E.A., Kahlon, V.: Reducing model checking of the many to the few. In: McAllester, D.A. (ed.) CADE. Lecture Notes in Computer Science, vol. 1831, pp. 236–254. Springer (2000). https://doi.org/10.1007/10721959_19

23 Emerson, E.A., Namjoshi, K.S.: On reasoning about rings. International Journal of Foundations of Computer Science 14(4), 527–550 (2003). https://doi.org/10.1142/S0129054103001881

24 Esparza, J., Finkel, A., Mayr, R.: On the verification of broadcast protocols. In: LiCS. pp. 352–359. IEEE Computer Society (1999). https://doi.org/10.1109/LICS.1999.782630

25 Esparza, J., Jaax, S., Raskin, M.A., Weil-Kennedy, C.: The complexity of verifying population protocols. Distributed Computing 34(2), 133–177 (2021). https://doi.org/10.1007/s00446-021-00390-x

26 Ganty, P., Majumdar, R.: Algorithmic verification of asynchronous programs. ACM Transactions on Programming Languages and Systems 34(1), 6:1–6:48 (2012). https://doi.org/10.1145/2160910.2160915

27 German, S.M., Sistla, A.P.: Reasoning about systems with many processes. Journal of the ACM 39(3), 675–735 (1992). https://doi.org/10.1145/146637.146681

28 Henzinger, T.A., Nicollin, X., Sifakis, J., Yovine, S.: Symbolic model checking for real-time systems. Information and Computation 111(2), 193–244 (1994). https://doi.org/10.1006/inco.1994.1045

29 Herbreteau, F., Kini, D., Srivathsan, B., Walukiewicz, I.: Using non-convex approximations for efficient analysis of timed automata. In: Chakraborty, S., Kumar, A. (eds.) FSTTCS. LIPIcs, vol. 13, pp. 78–89. Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2011). https://doi.org/10.4230/LIPIcs.FSTTCS.2011.78

30 Spalazzi, L., Spegni, F.: Parameterized model checking of networks of timed automata with Boolean guards. Theoretical Computer Science 813, 248–269 (2020). https://doi.org/10.1016/j.tcs.2019.12.026

31 Suzuki, I.: Proving properties of a ring of finite-state machines. Information Processing Letters 28(4), 213–214 (1988). https://doi.org/10.1016/0020-0190(88)90211-6
A **Omitted Formal Definitions**

A.1 Timed automata

We give the formal definition of the trace of a timed path $\rho = (q_0, v_0)^{\delta_0, \sigma_0} \cdots \xrightarrow{\delta_{l-1}, \sigma_{l-1}} (q_l, v_l)$, which is the sequence of pairs of delays and labels, obtained by removing transitions with a label from $\Sigma^-$ and adding the delays of these to the following transition. Formally, if all $\sigma_j$ are from $\Sigma^-$, then the trace is empty. Otherwise, trace($\rho$) = $(\delta'_0, \sigma'_0) \cdots (\delta'_m, \sigma'_m)$ defined as follows. Let $0 \le i_0 < \dots < i_m \le l-1$ be the maximal sequence such that $\sigma_{i_j} \notin \Sigma^-$ for each $j$. Then, $\sigma'_j = \sigma_{i_j}$. Moreover, $\delta'_j = \sum_{i_{j-1} < k \le i_j} \delta_k$ with $\delta_{-1} = -1$.

**Zones and DBMs [28, 15].** A zone is a set of clock valuations that are defined by a clock constraint $\psi$ (as defined in Section 2). In the following we will use the constraint notation and the set (of clock valuations) notation interchangeably. We denote by $\mathcal{Z}$ the set of all zones.

Let $\text{Post}_{\ge 0}(z) = \{v' \mid \exists v \in z, \exists \delta \ge 0, v' = v + \delta\}$ denote the time successors of $z$, and for a transition $\tau = (q, g, C_r, \sigma, q')$, let $\text{Post}_{\tau}(z) = \{v' \mid \exists v \in z, v \models \text{Inv}(q) \wedge g, v' = v[C_r \leftarrow 0], v' \models \text{Inv}(q')\}$ be the immediate successors of $z$ via $\tau$.

For a set $C$ of clocks, we denote by $C_0 = C \cup \{c_0\}$ the set $C$ extended with a special variable $c_0$ with the constant value 0. For convenience we sometimes write 0 to represent the variable $c_0$.

A difference bound matrix (DBM) for a set of clocks $C$ is a $|C_0| \times |C_0|$-matrix $(Z_{cc'})_{c,c' \in C_0}$, in which each entry $Z_{cc'} = (\ll_{cc'}, d_{cc'})$ represents the constraint $c - c' \ll_{cc'} d_{cc'}$ where $d_{cc'} \in \mathbb{Z}$ and $\ll_{cc'} \in \{\langle, \le\}$, or $(\ll_{cc'}, d_{cc'}) = (\langle, \infty\)$.

It is known that a zone $z$ can be represented by a DBM i.e., a valuation $v \in z$ iff $v$ satisfies all the clock constraints represented by the DBM.

We define a total ordering on $(\ll_{cc'} \times \mathbb{Z}) \cup \{\langle, \infty\}\}$ as follows $(\ll_{cc'}, d) < (\langle, \infty)$, $(\ll_{cc'}, d) < (\ll'_{cc'}, d')$ if $d < d'$ and $(\langle, d) < (\le, d)$. A DBM is canonical if none of its constraints can be strengthened (i.e., replacing one or more entries with a strictly smaller entry based on the ordering we defined) without reducing the set of solutions. Given a DBM $(Z_{cc'}), c,c' \in C_0$, we denote by $[(Z_{cc'}), c,c' \in C_0]$, the set of valuations that satisfy all the clock constraints in $(Z_{cc'}), c,c' \in C_0$, which is a zone. Any region and zone can be represented by a DBM. Given two DBMs $(Z_{cc'}), c,c' \in C_0$, $(Z'_{cc'}), c,c' \in C_0$ we write $(Z_{cc'}), c,c' \in C_0 \le (Z'_{cc'}), c,c' \in C_0$ if for all $c, c'$, $Z_{cc'} \le Z'_{cc'}$, if $z = [(Z_{cc'}), c,c' \in C_0]$ and $z' = [(Z'_{cc'}), c,c' \in C_0]$, then we have $(Z_{cc'}), c,c' \in C_0 \le (Z'_{cc'}), c,c' \in C_0$ iff $z \subseteq z'$.

A.2 Networks of TAs

We formally define projections of computations and traces of NGTAs. If $c = ((q_1, v_1), \dots, (q_n, v_n))$ and $\mathcal{I} = \{i_1, \dots, i_k\} \subseteq \{1, \dots, n\}$, then $c \downarrow_{\mathcal{I}}$ is the tuple $((q_{i_1}, v_{i_1}), \dots, (q_{i_k}, v_{i_k}))$, and we extend this notation to computations $\pi \downarrow_{\mathcal{I}}$ by keeping only the discrete transitions of $\mathcal{I}$ and by adding the delays of the removed discrete transitions to the delay of the following discrete transition of $\mathcal{I}$. Formally, given $\mathcal{I} \subseteq \{1, \dots, n\}$ and computation $\pi = c_0 \xrightarrow{\delta_0, (i_0, \sigma_0)} \dots \xrightarrow{\delta_{l-1}, (i_{l-1}, \sigma_{l-1})} c_l$, let $\pi \downarrow_{\mathcal{I}}$ denote the projection of $\pi$ to processes $\mathcal{I}$, defined as follows. Let $0 \le k_0 < \dots < k_m \le l-1$ be a sequence of maximal size such that $i_{k_j} \in \mathcal{I}$ for all $0 \le j \le m$. Then $\pi \downarrow_{\mathcal{I}} = c_0 \downarrow_{\mathcal{I}} \xrightarrow{(\delta'_{k_0}, (i_{k_0}, \sigma_{k_0}))} c_{k_0+1} \downarrow_{\mathcal{I}} \dots c_{k_m} \downarrow_{\mathcal{I}} \xrightarrow{(\delta'_{k_m}, (i_{k_m}, \sigma_{k_m}))} c_{k_m+1} \downarrow_{\mathcal{I}}$, where each $\delta'_{k_j} = \sum_{k_{j-1} < j' \le k_j} \delta_{j'}$ with $k_{-1} = -1$.

We formally define the composition of computations of NGTAs. For timed paths $\pi_1$ of $A^{n_1}$ and $\pi_2$ of $A^{n_2}$ with $\delta(\pi_1) = \delta(\pi_2)$, we denote by $\pi_1 \parallel \pi_2$ their composition into a timed path of $A^{n_1+n_2}$ whose projection to the first $n_1$ processes is $\pi_1$, and whose projection to the
last $n_2$ processes is $\pi_2$. If $\pi_1$ has length 0, then we concatenate the first configuration of $\pi_1$ to $\pi_2$ by extending it to $n_1+n_2$ dimensions; and symmetrically if $\pi_2$ has length 0. Otherwise, for $i \in \{1,2\}$, let $\pi_i = c_0^i \xrightarrow{\delta_0^i, \sigma_0^i} c_1^i \xrightarrow{\delta_1^i, \sigma_0^i} \dots$. Let $i_0 \in \{1,2\}$ be such that $\delta_0^{i_0} \le \delta_0^{3-i_0}$ (and pick $i_0 = 1$ in case of equality). Then the first transition of $\pi_1 \parallel \pi_2$ is $c_0 \xrightarrow{\delta_0^{i_0}, \sigma_0^{i_0}} c_1$, where $c_0$ is obtained by concatenating $c_0^{i_0}$ and $c_1^{3-i_0}$, and $c_1$ is obtained by $c_1^{i_0}$ and $c_0^{3-i_0}$. We define the rest of the path recursively, after subtracting $\delta_0^{i_0}$ from the first delay of $\pi_{3-i_0}$.

# B Omitted Proofs

## B.1 Proofs of Section 3.1

**Proof of Lemma 12.** Consider $r$ represented by a DBM in canonical form. We define $r'_{t,c} = r_{t,c} + k$ and $r'_{c,t} = r_{c,t} - k$, and $r'_{c,c'} = r_{c,c'}$ for all $c, c' \in C \setminus \{t\}$. In addition, if $r'_{t,c} > M^t$, then it is replaced by $\infty$, and if $r'_{c,t} < -M^c$, it is replaced by $-\infty$.

Note that the relations between $c$ and $c'$ remain unchanged for all $c, c' \in C \setminus \{t\}$ since these entries are not modified, and moreover, the canonical form also cannot assign these entries a smaller value. This is because $r_{c,c'} \le r_{c,t} + r_{t,c'}$ by the canonical form of $r$. Moreover,

$$r'_{c,t} + r'_{t,c'} = r_{c,t} + k + r_{t,c'} - k = r_{c,t} + r_{t,c'}$$

So we also have $r'_{c,c'} \le r'_{c,t} + r'_{t,c'}$. So is $r'$ is also in canonical form, and we have $r'_{\downarrow-t} = r_{\downarrow-t}$. $\quad$

## B.2 Proofs of Section 3.2.1

**Proof of Lemma 16.** Note that each $W_i$ is a set of $M^t$-region states of UG($A$) (thus, including the global clock). Moreover, each $W_i_{\downarrow-t}$ is a set of pairs $(q, r)$ where $q$ is a location, and $r$ is a $M$-regions. Recall that $N_A$ is the number of such pairs. Every layer $W_i$ with even index $i$ and with a bounded slot has a singleton slot. So whenever $l_0 \ge 2^{N_A+1}$, there exists $0 \le i < j \le l_0$ such that $W_i \approx W_j$.

Because $M^t(t) = 2^{N_A+1}$, if the algorithm stops at some iteration $l$, then slot($W_l$) is indeed bounded. $\quad$

**Proof of Lemma 18.** Consider a computation $\rho_r = (q_0, r_0) \xrightarrow{\sigma_0} \dots \xrightarrow{\sigma_{l-1}} (q_l, r_l)$ of $\mathcal{R}_{M^t}(\text{UG}(A))$, and assume, w.l.o.g. that it starts with a delay transition, and delays and discrete transitions alternate. By the properties of regions [8], there exists a timed computation $\rho = (q_0, v_0) \to \dots \to (q_l, v_l)$ that follows $\rho_r$, in the sense that $v_i \in r_i$ for all $0 \le i \le l$.

Recall that, by definition, each discrete transition with label $\sigma$ in $\mathcal{R}_{M^t}(\text{UG}(A))$ is built from a transition of UG($A$) with label $\sigma$.

Let $\tau_i = \epsilon$ if $\sigma_i = \text{delay}$, and otherwise, let $\tau_i$ denote the transition $(q_i, g, C_r, \sigma_i, q_{i+1})$ of UG($A$) corresponding to the $i$-th transition of $\rho_r$.

For a set of clock valuations $z$, we define $\text{Post}_{\ge 0}(z) = \{v+d \mid d \ge 0, v \in z\}$, and for a given transition $\tau = (q, g, C_r, \sigma, q')$, $\text{Post}_{\tau}(z) = \{v[C_r \leftarrow 0] \mid v \in z, z \models g\}$. Consider the sequence $(z)_i$ defined by $z_0 = \hat{r}$, and for all $0 \le i \le l-1$,

* $z_{i+1} = \text{Post}_{\ge 0}(z_i) \cap r_{i+1}$, if $\tau_i = \epsilon$ (delay transition);

* $z_{i+1} = \text{Post}_{\tau_i}(z_i) \cap r_i$, if $\tau_i \ne \epsilon$ (discrete transition).

Each $z_i$ is exactly the set of those valuations that are reachable from the initial valuation by visiting $r_i$ at step $i$. In other terms, $z_l$ is the strongest post-condition of $\hat{r}$ via $\rho_r$: it is the set
of states reachable from the initial state in UG($A$), by following the discrete transitions of $\rho_r$, while staying at each step inside $r_i$. We have that $z_l \neq \emptyset$ since there exists the computation $\rho$ mentioned above. We can have however $z_i \subsetneq r_i$ since unbounded regions can contain unreachable valuations.

In this proof, we assume familiarity with DBMs; formal definitions are given in Appendix A.1. The sequence $(z_i)$ can be computed using zones, using difference bound matrices (DBM) [28, 15]. Let $Z, R$ be DBMs in canonical form representing $z_l, r_l$ respectively.

Since, by construction, $z_l \subseteq r_l$, it holds that for every pair of clocks $c, c'$, $Z_{c,c'} \le R_{c,c'}$. In particular $Z_{t,0} \le R_{t,0}$ and $Z_{0,t} \le R_{0,t}$ that is $[-Z_{0,t}, Z_{t,0}] \subseteq [-R_{0,t}, R_{t,0}]$. And we have $\emptyset \neq [-Z_{0,t}, Z_{t,0}]$ since $z_l \neq \emptyset$. But in our case the interval on the right hand side is a slot, and because it is bounded it is either a singleton or an interval of the form $(k, k+1)$. It follows that $[-Z_{0,t}, Z_{t,0}]$ cannot be strictly smaller since it is nonempty.

Now, because $Z$ is in canonical form, for all $t' \in \mathbb{R}_{\ge 0}$ such that $t' \le Z_{t,0}$ and $-t' \le Z_{0,t}$, there exists a valuation $v_l \in [Z]$ and $v_l(t) = t'$ [29, Lemma 1]. Because $v_l \in z_l$, and by definition of $z_l$, there exists a timed computation $(q_0, v_0) \to \dots \to (q_l, v_l)$ such that $(q_0, v_0) = (\hat{q}, \mathbf{0})$ and $v_i \in r_i$ for $i \in \{1 \dots l\}$. $\quad \blacksquare$

**Proof of Lemma 19.** Consider the order in which the transitions $((q, r), \sigma, (q', r'))$ are added to some $E_i$ by the algorithm. The index of transition $((q, r), \sigma, (q', r'))$, denoted by ind($\sigma$), is equal to $i$ if $((q, r), \sigma, (q', r'))$ is the $i$-th transition added by the algorithm. We define the index of a path $\rho_D = (q_0, r_0) \stackrel{\sigma_0}{\implies} \dots \stackrel{\sigma_{l-1}}{\implies} (q_l, r_l)$ in $D(A)$, denoted by ind($\rho_D$), as the maximum of the indices of its transitions (we define the maximum as 0 for a path of length 0). For a computation $\pi$ of $A^n$, ind($\pi$) is the maximum over the computations of all processes.

Let $i_0 < l_0$ be the indices such that the algorithm stopped by condition $W_{l_0} \approx W_{i_0}$ such that $\text{slot}(W_{i_0}) = [k_{i_0}, k_{i_0}]$, $\text{slot}(W_{l_0}) = [k_{l_0}, k_{l_0}]$ for some $k_{i_0}, k_{l_0} \ge 0$.

Notice that in the DTN region automaton, delay transitions from $W_{l_0-1}$ that increment the slots lead to regions with smaller slots in line 7 in Algorithm 1. This was done on purpose to obtain a finite construction. However, we are going to prove the lemma by building timed computations whose total delay belongs to the slot of the regions of a given path of the DTN region automaton, and this is only possible if slots are nondecreasing along delay transitions. We thus show how to fix a given path of the DTN region automaton by shifting the slots appropriately to make them nondecreasing.

Consider a path $\rho_D = (q_0, r_0) \stackrel{\sigma_0}{\implies} \dots \stackrel{\sigma_{l-1}}{\implies} (q_l, r_l)$. for each $0 \le i \le l$, define $\text{period}_{i_0, l_0}(i)$ as the number of times the prefix path $(q_0, r_0) \stackrel{\sigma_0}{\implies} \dots \stackrel{\sigma_{i-1}}{\implies} (q_i, r_i)$ has a transition during which the slot goes from $\text{slot}(W_{l_0-1})$ back to $\text{slot}(W_{i_0})$. Here, we will work with $M'^{\gamma}$-regions where $M'^{\gamma}(t) > \max(M^{\gamma}(t), (k_{l_0} - k_{i_0})\text{period}_{i_0, l_0}(l) + k_{i_0})$, and $M'^{\gamma}(c) = M(c)$ for all $c \in C$. Because all $M^{\gamma}$-regions of $\rho_D$ have bounded slots (Lemma 16), all $r_i$ are $M'^{\gamma}$-regions as well. Having a sufficiently large bound for $t$ in $M'^{\gamma}$ make sure that all shifted slots are bounded in all steps of $\rho_D$ (and not just in the first $2l_0$ steps).

We define fix($\rho_D$) from $\rho_D$ by replacing each $r_i$ by $(r_i)_{\text{slot}+(k_{l_0}-k_{i_0})\text{period}_{i_0,l_0}(i)}$. This simply reverts the effect of looping back to the slot of $W_{i_0}$ and ensures that whenever $\sigma_i = \epsilon$, the $M'^{\gamma}$-region $r_{i+1}$ is a time successor of $r_i$, that is, $(q_i, r_i) \xrightarrow{\text{delay}} (q_{i+1}, r_{i+1})$ in the region automaton $\mathcal{R}_{M'^{\gamma}}(\text{UG}(A))$. We extend the definition of fix($\cdot$) to paths of $S(A)$ by shifting the slots of the regions that appear in the locations as above (without changing the clock valuations or delays).

We first show Claim 1. Given a computation $\rho_D$ of $S(A)$, write fix($\rho_D$) = $((q_0, r_0), v_0) \xrightarrow{\delta_0, \sigma_0} \dots \xrightarrow{\delta_{l-1}, \sigma_{l-1}} ((q_l, r_l), v_l)$. We prove that for all $t' \in \text{slot}(r_l)$, there
exists $n \in \mathbb{N}$ and path $\pi$ of $A^n$ such that $t(\pi) = t'$ and $\text{trace}(\pi)\downarrow_1 = (\delta'_0, \sigma_0) \dots (\delta'_{l-1}, \sigma_{l-1})$ for some $\delta'_0, \dots, \delta'_{l-1}$. We proceed by induction on $\text{ind}(\rho_D)$.

This clearly holds for $\text{ind}(\rho_D) = 0$ since the slot is then $[0, 0]$, and the region path starts in the initial region state and has length 0.

Assume that $\text{ind}(\rho_D) > 0$. Consider $t' \in \text{slot}(r_l)$. Computation $\rho_D$ defines a path in $\mathcal{R}_{M'}(\text{UG}(A))$ to which we apply Lemma 18, which yields a timed computation $\rho = (q_0, v_0) \xrightarrow{\delta_0, \sigma_0} \dots \xrightarrow{\delta_{l-1}, \sigma_{l-1}} (q_l, v_l)$ in $\text{UG}(A)$ such that $v_i \in r_i$ for $0 \le i \le l$, and $v_l(t) = t'$.

This computation has the desired trace but we still need to prove that it is feasible in some $A^n$. We are going to build an instance $A^n$ in which $\rho$ will be the computation of the first process, where all location guards are satisfied.

Let $J$ be the set of steps $j$ such that $\sigma_j$ is a discrete transition with a nontrivial location guard. Consider some $j \in J$, and denote its nontrivial location guard by $\gamma$. Let $t'_j = v_j(t) + \delta_j$ the global time at which the transition is taken. By the properties of $S(A)$, We have $t'_j \in \text{slot}(r_j)$. When the algorithm added the transition $((q_j, r_j), \sigma_j, (q_{j+1}, r_{j+1}))$, some region state $(\gamma, r_\gamma)$ with $\text{slot}(r_\gamma) = \text{slot}(r_j)$ was already present (by Rule 2 on line 4). Therefore, there exists a computation $\pi^j$ in the DTN region automaton that ends in state $(\gamma, r_\gamma)$ with $\text{ind}(\pi^j) < \text{ind}(((q_j, r_j), \sigma_j, (q_{j+1}, r_{j+1})))$. Therefore there exists a computation in $S(A)$ as well visiting the same locations, and ending in the location $(\gamma, r_\gamma)$. By induction, there exists $n_j$, and a computation $\pi^j$ in $A^{n_j}$ with $\text{trace}(\pi^j)\downarrow_1$ ending in $\gamma$ with $t(\pi^j\downarrow_1) = t'_j$.

We arbitrarily extend all $\pi^j$, for $j \in J$, to global time $\delta(\rho)$ (or further), which is possible by Assumption 1. We compose $\rho_{\downarrow-t}$ and all the $\pi^j$ into a single one in $A^{n+1}$ (see composition in Appendix A.2) where the first process follows $\rho_{\downarrow-t}$, and the next $n = \sum_{j \in J} n_j$ follow the $\pi^j$. Thus, when the first process takes a transition with a location guard $\gamma$ at time $t'_j$, there is another process at $\gamma$ precisely at time $t'_j$.

Claim 2 is an application of Claim 1. In fact, we can build a computation in which process 1 follows $\text{fix}(\rho_D)$ by applying Claim 1 to each prefix where a nontrivial location guard is taken.

**Proof of Lemma 20.** We prove, by induction on the length of $\pi$, a slightly stronger statement: for all $n \ge 1$, all computations $\pi$ of $A^n$, and all $1 \le k \le n$, $\text{trace}(\pi)\downarrow_k \in \mathcal{L}(S(A))$.

Let $i_0 < l_0$ be the indices such that the algorithm stopped by condition $W_{l_0} \approx W_{i_0}$ such that $\text{slot}(W_{i_0}) = [k_{i_0}, k_{i_0}]$, $\text{slot}(W_{l_0}) = [k_{l_0}, k_{l_0}]$ for some $k_{i_0}, k_{l_0} \ge 0$. Define function $\text{reduce}(a) = a$ if $a < k_{i_0}$, and otherwise $\text{reduce}(a) = k_{i_0} + ((a - k_{i_0}) \mod (k_{l_0} - k_{i_0}))$. This function simply removes the global time spent during the loops between $W_{i_0}$ and $W_{l_0}$; thus, given any computation of $S(A)$ ending in $((q, r), v)$, we have $\text{reduce}(v(t)) \in \text{slot}(r)$.

If $\pi$ has length 0, then its trace is empty and thus belongs to $\mathcal{L}(S(A))$.

Assume that the length is greater than 0. The proof does not depend on a particular value of $k$, so we show the statement for $k = 1$ (but induction hypotheses will use different $k$). Let $\rho = (q_0, v_0) \xrightarrow{\delta_0, \sigma_0} \dots \xrightarrow{\delta_{l-1}, \sigma_{l-1}} (q_l, v_l)$ be a computation of $\text{UG}(A)$ on the trace $\text{trace}(\pi\downarrow_1)$, and let $\tau_j$ be the transition with label $\sigma_j$ that is taken on the $j$-th discrete transition.

Assume that $\tau_{l-1}$ does not have a location guard. Let $\pi'$ be the prefix of $\pi$ on the trace $(\delta_0, \sigma_0) \dots (\delta_{l-2}, \sigma_{l-2})$ (if $l = 1$, then $\pi' = (q_0, v_0)$). By induction $\text{trace}(\pi')\downarrow_1 \in \mathcal{L}(S(A))$. Consider a computation of $S(A)$ along this trace, that ends in some configuration $((q, r), v)$. By $\pi$, the invariant of $q$ holds at $v + \delta_{l-1}$, so by Rule 1 of Algorithm 1, $S(A)$ contains a region state $(q, r')$ with $r'\downarrow_{-t} = [v + \delta_{l-1}]_M$ that is reachable from $(q, r)$ via $\epsilon$-transitions. Moreover, we know by $\pi$ that the guard of $\tau_{l-1}$ is satisfied at $v + \delta_{l-1}$, and by Rule 2, $S(A)$ has a transition from $(q, r')$ with label $\sigma_{l-1}$. It follows that $\text{trace}(\pi)\downarrow_1 = \text{trace}(\pi')\downarrow_1 \cdot (\delta_{l-1}, \sigma_{l-1}) \in \mathcal{L}(S(A))$.

Assume now that $\tau_{l-1}$ has a nontrivial location guard $\gamma$.
Let $\pi'$ be the prefix of $\pi$ on the trace $(\delta_0, \sigma_0) \dots (\delta_{l-2}, \sigma_{l-2})$. As in the previous case, we have, by induction a computation in $S(A)$ which follows trace $\pi'(\delta_0)\downarrow_1$ and further delays $\delta_{l-1}$. At this point, the clock guard of the transition $\tau_{l-1}$ is also enabled. Following the same notations as above, let $(q, r')$ denote the location of $S(A)$ reached after the additional delay $\delta_{l-1}$. Notice that $\text{reduce}(\delta_0 + \dots + \delta_{l-1}) \in \text{slot}(r')$. To conclude, we just need to justify that a transition from $(q, r')$ with label $\sigma_{l-1}$ exists in $S(A)$. By Algorithm 1, this is the case if, and only if some other region state $(\gamma, s)$ exists in $S(A)$ such that $\text{slot}(s) = \text{slot}(r')$.

In $\pi$, there exists some process $k$ which is at location $\gamma$ at time $\delta_0 + \dots + \delta_{l-1}$ (since the last transition requires a location guard at $\gamma$). Thus process $k$ is at $\gamma$ at the end of $\pi'$, and remains so after the delay of $\delta_{l-1}$. By induction, $\text{trace}(\pi')\downarrow_k \in \mathcal{L}(S(A))$. Thus, there is a computation of $S(A)$ along this trace, that is, with total delay $t(\pi') = \delta_0 + \dots + \delta_{l-1}$, and ending in a location $(\gamma, s)$ for some region $s$. Therefore $\text{reduce}(\delta_0 + \dots + \delta_{l-1}) \in \text{slot}(s)$. But we also have $\text{reduce}(\delta_0 + \dots + \delta_{l-1}) \in \text{slot}(r')$ as seen above. Because slots are disjoint intervals, it follows $\text{slot}(r') = \text{slot}(s')$, which concludes the proof. $\quad$

**Proof of Theorem 21.** By symmetry between processes, a label $\sigma_0$ is reachable in $A^n$ by some process, iff it is reachable by process 1 in $A^n$. By Lemmas 19 and 20, this is the case iff there exists $0 \le i \le 2^{N_A+1}$ and a region $r$ such that $(q, r) \in W_i$ and $((q, r), \sigma_0, (q', r')) \in W_i$ for some $(q', r')$.

Notice also that because $t$ has the same slot in each $W_i$, the size of $W_i$ is bounded by the number of region states for a bound function where $t$ is either equal to 0 (for slots of the form $[k, k]$), or is in the interval $(0, 1)$ (for slots of the form $(k, k+1)$). This is exponential in $|C|$.

Moreover, each $W_i$ can be constructed only using $W_{i-1}$ and $A$, that is, does not require the whole sequence $W_0, W_1, \dots, W_{i-1}$.

The EXPSPACE algorithm basically executes the main loop of Algorithm 1 but only stores $W_i$ at iteration $i$. It has a binary counter to count up to $2^{N_A+1}$. If it encounters the target label $\sigma_0$, it stops and returns yes. Otherwise, it stops after $2^{N_A+1}$ iterations, and returns no. $\quad$

**Proof of Lemma 22.** Consider a trace $tt = (\delta_0, (i_0, \sigma_0)) \dots (\delta_{l-1}, (i_{l-1}, \sigma_{l-1}))$ in $\mathcal{L}(A^\infty)\downarrow_I$ and let $tt_j$ denote its projection to process $j$. By Theorem 17, $tt_j \in \mathcal{L}(S(A))$, so there is a computation $\rho_j$ in $S(A)$ with trace $tt_j$. Due to the labeling of the symbols with indices, there is no synchronization in $\otimes_{1 \le j \le a} S(A)$ between different copies of $S(A)$ (except on time delays), so we can execute each $\rho_j$ in the $j$-th copy in the product, and this yields the a cpmputation with trace $tt$.

Conversely, consider a trace $tt$ of $\otimes_{1 \le j \le a} S(A)$. Similarly, it follows that there is a computation $\rho_j$ in $S(A)$ on trace $tt_j$. By Theorem 17, there exists $n_j \ge 1$ such that $tt_j \downarrow \in \mathcal{L}(A^{n_j})\downarrow_j$. Let $\pi_j$ be the computation in $A^{n_j}$ with a trace whose projection to $j$ is equal to $tt_j$. We compose the computations $\pi_j$, which yields a computation $\pi$ in $A^{n_1+\dots+n_a}$ such that $\pi\downarrow_{[1,a]} = tt$. $\quad$

## B.3 Proofs of Section 4

In order to simulate location guards in the lossy broadcast setting, we use $\Lambda = Q$ and transitions that require a nontrivial location guard $\gamma$ have synchronization label $\gamma??$; we add for each location $\gamma$ a self-loop with synchronization label $\gamma!!$ and with a fresh label $\iota$ from $\Sigma^-$ (such that this transition will not appear in the traces of the system).

The other direction is slightly more involved: given an LTBA $B$, a GTA $A$ is constructed from $B$ starting with the same locations and clock invariants, and adding an auxiliary clock $c_{\text{snd}}$. Then, for every broadcast sending transition $(q, g, C_r, \sigma, a!!, q')$ we do the following:
■ add an auxiliary location $q_\sigma$ with $Inv(q_\sigma) = (c_{\text{snd}} = 0)$ (i.e., it has to be left again without time passing), and transitions $(q, g, \{c_{\text{snd}}\}, \sigma, \top, q_\sigma)$ and $(q_\sigma, \top, C_r, \iota, \top, q')$ for a fresh $\iota \in \Sigma^-$;

■ for every corresponding broadcast receiving transition $(q_{rcv}, g_{rcv}, C_r^{rcv}, \sigma', a??, q'_{rcv})$ we add a disjunctive guarded transition $(q_{rcv}, g_{rcv}, C_r^{rcv}, \sigma', q_\sigma, q'_\sigma)$, i.e., receivers can only take the transition if the sender has moved to $q_\sigma$.

Note that this construction relies on the fact that a label $\Sigma$ uniquely determines the transition (Assumption 2 also applies here).

<figure><img src="image_10.png" /><figcaption>■ **Figure 6 Gadgets for constructing an LBTA B from a GTA A.** The upper half shows the case of a transition with a trivial location guard in the GTA A given on the left, for which we produce a transition in the LBTA B shown on the right. The lower half shows the case of a transition of the GTA A with a non-trivial location guard, given on the left, for which we produce two transitions shown on the right in the LBTA B.</figcaption></figure>

► **Lemma 28.** For every GTA A, there exists an LBTA B such that for every $k \ge 1$, $\mathcal{L}(A^\infty)_{\downarrow[1,k]} \equiv \mathcal{L}(B^\infty)_{\downarrow[1,k]}$.

**Proof.** B is constructed from A by keeping locations and clock invariants, setting $\Lambda = Q$, and modifying the transitions in the following way:

■ each transition $(q, g, C_r, \sigma, \gamma, q')$ of A with $\gamma = \top$ is simulated by a sending transition $(q, g, C_r, \sigma, q??, q')$,

■ each transition $(q, g, C_r, \sigma, \gamma, q')$ of A with $\gamma \neq \top$ is simulated by a receiving transition $(q, g, C_r, \sigma, \gamma??, q')$ together with a sending transition $(\gamma, \top, \emptyset, \iota, \gamma??, \gamma)$,

Fig. 6 shows the idea of the construction.

We prove that $\mathcal{L}(A^\infty)_{\downarrow 1} = \mathcal{L}(B^\infty)_{\downarrow 1}$, the lemma statement follows as for NGTAs in Lemma 22.

First, let $tt = (\delta_0, \sigma_0) \dots (\delta_{l-1}, \sigma_{l-1})$ be the trace of a computation $\rho$ of $A^n$ for some $n$. We prove inductively that there exists a computation $\rho'$ of $B^n$ that has the same trace $tt$ and ends in the same configuration as $\rho$.

Base case: $i=0$. If $(\delta_0, \sigma_0)$ is a trace of $A^n$, then there must exist a transition $c \xrightarrow{\delta, (j, \sigma)} c'$ such that $c$ is the initial configuration of $A$, and after a delay $\delta$ some process $j$ takes a discrete transition on label $\sigma$, which may be guarded by a location $\gamma$. Note that by construction $c$ is also an initial configuration of $B$, and we can take the same delay $\delta$ in $c$. Since the transition on $(j, \sigma)$ is possible after $\delta$ in $A$, there must be a transition $(q, g, C_r, \sigma, \gamma, q')$ of $A$ such that $q = \hat{q}, \mathbf{0} + \delta$ satisfies $g$, and $\gamma$ is either $\hat{q}$ or $\top$. If $\gamma = \top$, then by construction of $B$ there exists a sending transition $(\hat{q}, g, C_r, \sigma, \gamma??, q')$. If $\gamma \neq \top$, then in $B$ there exists a receiving transition $(\hat{q}, g, C_r, \sigma, \gamma??, q')$ and a sending transition $(\gamma, \top, \hat{q}, \iota, \gamma??, \gamma)$. In both cases, one process moves into $q'$ and the transition label $\sigma$ is the same as for the transition in $A$ (and
1:24 Parameterized Verification of Timed Networks with Clock Invariants

the transition of B labeled with $\iota$ does not appear in the trace). Therefore, the resulting configuration and trace is the same as in A.

Step: $i \to i + 1$. Assume that the property holds for the first $i$ steps. Then the inductive argument is the same as above, except that we are not starting from an initial configuration, but equal configurations in $A^n$ and $B^n$ that we get by induction hypothesis.

Now, let $tt = (\delta_0, \sigma_0) \dots (\delta_{l-1}, \sigma_{l-1})$ be the trace of a computation $\rho$ of $B^n$ for some $n$. With the same proof structure above, we can show that there exists a computation $\rho'$ of $A^n$ that has the same trace $tt$ and ends in the same configuration. ◀

<figure><img src="image_11.png" /><figcaption>Figure 7 Gadgets for constructing a GTA A from an LBTA B. Given a sending transition of the B shown on top left, we produce the sequence of transitions in the GTA A as shown on top right. For every receiving transition of the LBTA B with the corresponding label a??, we produce a transition shown on bottom right in the GTA A.</figcaption></figure>

**Lemma 29.** For every LBTA B, there exists a GTA A such that $\mathcal{L}(A^\infty)\downarrow_{[1,k]} = \mathcal{L}(B^\infty)\downarrow_{[1,k]}$.

**Proof.** A is constructed from B by starting with the same locations and clock invariants, and adding an auxiliary clock $c_{\text{snd}}$. Then, for every broadcast sending transition $(q, g, C_r, \sigma, a!!, q')$ we do the following:

■ add an auxiliary location $q_\sigma$ with $\text{Inv}(q_\sigma) = (c_{\text{snd}} = 0)$ (i.e., it has to be left again without time passing), and transitions $(q, g, \{c_{\text{snd}}\}, \sigma, \top, q_\sigma)$ and $(q_\sigma, \top, C_r, \iota, \top, q')$ for a fresh $\iota \in \Sigma^-$;

■ for every corresponding broadcast receiving transition $(q_{\text{rcv}}, g_{\text{rcv}}, C_r^{\text{rcv}}, \sigma', a??, q'_{\text{rcv}})$ we add a disjunctive guarded transition $(q_{\text{rcv}}, g_{\text{rcv}}, C_r^{\text{rcv}}, \sigma', q_\sigma, q'_{\text{rcv}})$, i.e., receivers can only take the transition if the sender has moved to $q_\sigma$.

Fig. 7 shows the idea of the construction. Note that the construction relies on the fact that a label $\Sigma$ uniquely determines the transition (Assumption 2 also applies here).

Like in the proof of Lemma 28, the claim follows from proving inductively that for every computation $\rho$ of $B^n$ with trace $tt$ there exists a computation $\rho'$ of $A^n$ with trace $tt$. In this case the proof relies on the fact that for a lossy broadcast transition, the timed transition system of $B^n$ contains the sequence of steps in any order for the receivers. ◀

Note that [11] claims that location reachability is undecidable for automata with 2 clocks in a model that is very similar (and may be equivalent) to LBTN; we have reasonable doubts regarding that result (which comes without a full proof), but the discrepancy might come from differences in the models as well.

## B.4 Proofs of Section 5

As mentioned in the proof idea of Theorem 25, simulating a GTA by an STA is simple. For the other direction, let us define the GTA that will simulate a given STA. This GTA is
<figure><img src="image_12.png" /><figcaption>Figure 8 On the left-hand side is a rule *r* in an STA *S*. On the right-hand side is the corresponding GTA-gadget, where location guards ensure that *p*<sub>r,m</sub> is only reachable if all *p*<sub>r,i</sub> are reachable, and it follows that all *q*'<sub>i</sub> are reachable if and only if *p*<sub>r,m</sub> is reachable. Furthermore, invariants on *p*<sub>r,i</sub> ensure that there cannot be any delay between the transitions in the gadget. Not displayed are transitions from every *p*<sub>r,i</sub> without any guards to the sink location *q*<sub>⊥</sub> (with fresh labels from Σ<sup>-</sup>).</figcaption></figure>

based on the gadget shown in Fig. 8 (for one rule *r* of the STA), and formally defined in the
following.

► **Definition 30** (Corresponding GTA for a given STA). For a given STA $\mathcal{S} = (Q, \hat{q}, \mathcal{C}, \text{Inv}, \mathcal{R})$, its corresponding GTA is defined as $A_{\mathcal{S}} = (Q_{A_{\mathcal{S}}}, \hat{q}, \mathcal{C} \cup \{c_{\text{sync}}\}, \Sigma, \mathcal{T}, \text{Inv}_{A_{\mathcal{S}}})$, where:

Q_S = Q \dot{\cup} P \dot{\cup} \{q_⊥\}, with P = \{p_{r,i} | r \in \mathcal{R}, 1 \le i \le m \text{ where } r = \langle q_{r,1} \xrightarrow{g_{r,1},C_{r,1},\sigma_{r,1}} q'_{r,1}, \dots, q_{r,m} \xrightarrow{g_{r,m},C_{r,m},\sigma_{r,m}} q'_{r,m} \rangle\}

c_sync is an auxiliary clock that does not appear in C

$\mathcal{T} = \bigcup_{r \in \mathcal{R}} T_{r,1} \cup T_{r,2} \cup T_{r,\perp}$ for $r = \langle q_{r,1} \xrightarrow{g_{r,1},C_{r,1},\sigma_{r,1}} q'_{r,1}, \dots, q_{r,m} \xrightarrow{g_{r,m},C_{r,m},\sigma_{r,m}} q'_{r,m} \rangle$, where:

$$
\begin{align*}
T_{r,1} &= \{(q_{r,1}, g_{r,1}, C_{r,1} \cup \{c_{\text{sync}}\}, \iota_{r,1}, \top, p_{r,1})\} \\
&\quad \cup \bigcup_{2 \le i \le m} \{(q_{r,i}, g_{r,i}, C_{r,i} \cup \{c_{\text{sync}}\}, \iota_{r,i}, p_{r,i-1}, p_{r,i})\} \\
&\qquad \text{(incoming transitions of locations } p_{r,i} \text{ in Fig. 8),}
\end{align*}
$$

$$
\begin{align*}
T_{r,2} &= \bigcup_{1 \le i \le m-1} \{(p_{r,i}, \top, \emptyset, \sigma_{r,i}, p_{r,m}, q'_{r,i})\} \\
&\quad \cup \{(p_{r,m}, \top, \emptyset, \sigma_{r,m}, \top, q'_{r,m})\} \\
&\qquad \text{(outgoing transitions of locations } p_{r,i} \text{ in Fig. 8),}
\end{align*}
$$

$$
\begin{align*}
T_{r,\perp} &= \bigcup_{1 \le i \le m} \{(p_{r,i}, \top, \emptyset, \iota, \top, q_{\perp})\} \\
&\qquad \text{(transitions to sink location, not shown in Fig. 8)}
\end{align*}
$$

Inv<sub>A<sub>S</sub></sub> : Q<sub>A<sub>S</sub></sub> → Ψ(C ∪ {c<sub>sync</sub>}) defined as Inv<sub>A<sub>S</sub></sub>(q) = Inv(q) for every q ∈ Q, Inv<sub>A<sub>S</sub></sub>(p) = c<sub>sync</sub> ≤ 0 for p ∈ P and Inv<sub>A<sub>S</sub></sub>(q<sub>⊥</sub>) = ⊥.

**Definition 31** (Stable and Intermediate Configurations). For an NGTA $A_S^m$ (where $A_S$ is the guarded timed automaton defined above), the set of configurations is partitioned into:

- Stable Configurations: A configuration **c** = ((q<sub>1</sub>, v<sub>1</sub>), ..., (q<sub>m</sub>, v<sub>m</sub>)) is stable if q<sub>i</sub> ∈ Q for all 1 ≤ i ≤ m, i.e., in stable configurations, no process is in a location p<sub>r,i</sub> or in the sink location q<sub>⊥</sub>.

- Intermediate Configurations: A configuration is intermediate if it is not stable.
We say that a stable configuration $c_{AS}$ of $A_S^n$ corresponds to a configuration $c_S$ of $S^n$ if for every configuration $(q, v)$ of $A_S$ we have $(q, v) \in c_{AS}$ if and only if $(q, v \downarrow_{-c_{sync}}) \in c_S$

1019

1020

For the following lemma, we extend the projection $v \downarrow_{-c}$ of a clock valuation $v$ onto the clocks different from a clock $c$ to configurations in the expected way, i.e., for $c = ((q_1, v_1), \dots, (q_n, v_n))$, let $c \downarrow_{-c} = ((q_1, v_1 \downarrow_{-c}), \dots, (q_n, v_n \downarrow_{-c}))$.

1021

1022

1023

**Lemma 32.** *Consider an STA $S = (Q, \hat{q}, C, \text{Inv}, \mathcal{R})$ and its corresponding GTA $A_S = (Q_{AS}, \hat{q}, C \cup \{c_{sync}\}, \Sigma, \mathcal{T}, \text{Inv}_{AS})$. If a configuration $c_S$ is reachable in $S^n$ for some $n \in \mathbb{N}$ then there exists a stable configuration $c_{AS}$ in $A_S^n$ such that $c_{AS} \downarrow_{-c_{sync}} = c_S$ (in particular, $c_{AS}$ corresponds to $c_S$).*

1024

1025

1026

1027

**Proof.** Let $\pi_S$ be a computation of $S^n$ that ends in $c_S$, and $l$ the number of blocks in $\pi_S$, where a block is either a non-zero delay transition or a sequence of discrete transitions that correspond to the execution of a single rule $r \in \mathcal{R}$. The proof is by induction on $l$, the number of blocks of $\pi_S$.

1028

1029

1030

1031

1. **Base case ($l=0$):** Let $c_{S,0}$ and $c_{AS,0}$ be the initial configurations of networks $S^n$ and $A_S^n$ respectively. Since all processes in $c_{AS,0}$ and $c_{S,0}$ start in the initial location and all clocks are initialized to zero, we have $c_{AS,0} \downarrow_{-c_{sync}} = c_{S,0}$.

1032

1033

1034

2. **Induction step ($l \to l+1$):**

1035

1036

1037

We consider two cases: the final block in the computation could be a delay transition or the execution of a rule $r \in \mathcal{R}$.

a. **Delay transition:**

1038

In this case $\pi_S$ is of the form $c_{S,0} \to^* c_{S,pre} \xrightarrow{\delta} c_S$. By induction hypothesis, there is a stable configuration $c_{AS,pre}$ with $c_{AS,pre} \downarrow_{-c_{sync}} = c_{S,pre}$. Because the $c_{AS,pre}$ is stable, $c_{S,pre}$ has the same locations, thus the same invariants as $c_{AS,pre}$, so the same delay $\delta$ is possible from $c_{AS,pre}$ as well. If $c_{AS}$ is the configuration reached by a delay of $\delta$ from $c_{AS,pre}$, then clearly we have $c_{AS} \downarrow_{-c_{sync}} = c_S$.

1039

1040

1041

1042

1043

b. **Execution of rule $r \in \mathcal{R}$:**

1044

In this case $\pi_S$ is of the form $c_{S,0} \to^* c_{S,pre} \to^* c_S$, where the sequence of transitions $c_{S,pre} \to^* c_S$ is an execution of rule $r$. By induction hypothesis, if $c_{S,pre} = ((q_1, v_1), \dots, (q_n, v_n))$ is reachable in $S^n$ then a stable configuration $c_{AS,pre} = ((q_1, u_1), \dots, (q_n, u_n))$ is reachable in $A_S^n$ with $u_i \downarrow_{-c} = v_i$ for $1 \le i \le n$. To show that a stable configuration $c_{AS}$ with the desired property can be reached from $c_{AS,pre}$, we construct a computation $\pi_{pre}$ of the form $\pi_{pre} = c_{AS,pre} \to^* c_{AS, mid} \to^* c_{AS}$, where in the first part $c_{AS,pre} \to^* c_{AS, mid}$ the discrete transitions from $T_{r,1}$ (for the given rule $r$, compare Definition 30 and Fig. 8) are executed without delay, and in the second part $c_{AS, mid} \to^* c_{AS}$ the discrete transitions from $T_{r,2}$ are executed. We analyze the properties of this computation in the following.

1045

1046

1047

1048

1049

1050

1051

1052

1053

1054

**Part 1:** $c_{AS,pre} \to^* c_{AS, mid}$, executing $T_{r,1}$:

1055

1056

Assume w.l.o.g. that the transitions in $c_{S,pre} \to^* c_S$ in $S^n$ are executed by the first $m$ processes, and process $i$ takes element $q_{r,i} \xrightarrow{g_{r,i}, c_{r,i}, \sigma_{r,i}} q'_{r,i}$ of the rule $r$. Then, for $1 \le i \le m$ and $(q_i, v_i) \in c_{S,pre}$ we know that $v_i \models g_{r,i}$. Now consider $c_{AS,pre}$: since $u_i \downarrow_{-c} = v_i$ for $1 \le i \le n$, we have $u_i \models g_{r,i}$ for $1 \le i \le m$, i.e., process $i$ for $1 \le i \le m$ satisfies the clock guard of the $i$th transition in $T_{r,1}$. By taking the transitions in increasing order of $i$, also all location guards are satisfied. In addition, note that the set of clock resets for the $i$th transition in $T_{r,1}$ is the same as for the $i$th element of rule $r$, except for $c_{sync}$ (which is reset on all transitions in $T_{r,1}$). Since $u_i \downarrow_{-c} = v_i$ for $1 \le i \le n$, we get that the clock values in $c_{AS, mid}$ are equal (up to

1057

1058

1059

1060

1061

1062

1063

1064

1065
$c_{\text{sync}}$) to those in $\mathcal{C}_S$. Finally, note that in $\mathcal{C}_{A_S, \text{mid}}$, process $i$ occupies location $p_{r,i}$ for $1 \le i \le m$ (and the other processes have not changed their configuration).

**Part 2:** $\mathcal{C}_{A_S, \text{mid}} \to^* \mathcal{C}_S$, executing $T_{r,2}$:
Starting from $\mathcal{C}_{A_S, \text{mid}}$, each process $i$ for $1 \le i \le m$ takes the $i$th transition in $T_{r,2}$ and moves to $q'_{r,i}$, say in increasing order of $i$. Note that this is possible because the guard location $p_{r,m}$ is occupied in $\mathcal{C}_{r, \text{mid}}$, and will stay occupied until the $m$th process takes the $m$th transition from $T_{r,2}$. In the resulting configuration $\mathcal{C}_{A_S}$, the first $m$ processes will be in locations $q'_{r,i}$ according to rule $r$ and the other processes will be in the same location as in $\mathcal{C}_{A_S, \text{pre}}$ (and therefore the same as in $\mathcal{C}_S$). Therefore, all processes will be in the same location as in $\mathcal{C}_S$. Moreover, since none of these transitions alters clock valuations of any process, we get that $\mathcal{C}_{A_S} \downarrow_{-c_{\text{sync}}} = \mathcal{C}_S$. Finally, observe that $\mathcal{C}_{A_S}$ is a stable configuration, proving the desired property.

We now prove the converse direction. Here, starting from a stable configuration of $A_S^{n_1}$, we will build a corresponding reachable configuration in $S^{n_2}$ for some $n_2$. The reason of this discrepancy is that in STAs, each rule is applied to exactly $m$ processes, while in GTAs, nothing prevents more processes to cross the gadget of Fig. 8.

As a concrete example, consider the STA $S$ on the left side of Fig. 9 and the gadgets for its two rules that appear in $A_S$ on the right side: To reach location $q_3$ in $A_S$, three processes are sufficient—in the gadget for rule $r_1$ (at the right bottom), one process moves from $\hat{q}$ via $p_{r_1,1}$ to $q_1$, and two processes move $\hat{q}$ via $p_{r_1,2}$ to $q_2$, and then these two processes can execute the gadget of $r_2$ (right top) such that one of them arrives in $q_3$. In the STA $S$, at least four processes are needed to make one of them reach $q_3$— upon firing $r_1$ a single time, only one process is in $q_2$ (and another has moved to $q_1$), such that we need two additional processes in $\hat{q}$ to fire $r_1$ a second time, and only after that can $r_2$ be fired and one process reaches $q_3$.

Accordingly, the statement is also weaker: given $\mathcal{C}_{A_S}$, the lemma shows that there exists a reachable configuration $\mathcal{C}_S$ that corresponds to $\mathcal{C}_{A_S}$ (but without necessarily having $\mathcal{C}_{A_S} \downarrow_{-c_{\text{sync}}} = \mathcal{C}_S$). The proof is a bit more involved, and requires a copycat lemma given at the end of this section.

**Lemma 33.** Consider an STA $S = (Q, \hat{q}, C, \text{Inv}, \mathcal{R})$ and its corresponding GTA $A_S = (Q_{A_S}, \hat{q}, C \cup \{c_{\text{sync}}\}, \Sigma, \mathcal{T}, \text{Inv}_{A_S})$. If a stable configuration $\mathcal{C}_{A_S}$ is reachable in $A_S^{n_1}$ for some $n_1 \in \mathbb{N}$, then a configuration $\mathcal{C}_S$ is reachable in $S^{n_2}$ for some $n_2 \in \mathbb{N}$ such that $\mathcal{C}_{A_S}$ corresponds to $\mathcal{C}_S$.

**Proof.** Let $\pi$ be a computation of $A_S^{n_1}$ that ends in a stable configuration $\mathcal{C}_{A_S}$. The proof is by induction on $l$, the number of non-zero delay transitions in $\pi$.

1. **Base case** ($l = 0$): Let $\pi = \mathcal{C}_{A_S, 0} \to^* \mathcal{C}_{A_S}$ be the computation to $\mathcal{C}_{A_S}$ which in general can have multiple discrete but no non-zero delay transitions. Let $TS = \langle \tau_1 \dots \tau_k \rangle$ be the sequence of transitions of $A_S$ that appear on $\pi$, and let $TS\text{-set} = \{\tau_1, \dots, \tau_k\}$ be the set of the transitions in $TS$. For a given rule $r \in \mathcal{R}$ of $S$, let $TG_r = T_{r,1} \cup T_{r,2}$, with $T_{r,1}, T_{r,2}$ as defined in Definition 30.

We distinguish two cases: i) $TS\text{-set} \subseteq TG_r$ for some rule $r = \langle q_{r,1} \xrightarrow{g_{r,1}, C_{r,1}, \sigma_{r,1}} q'_{r,1}, \dots, q_{r,m} \xrightarrow{g_{r,m}, C_{r,m}, \sigma_{r,m}} q'_{r,m} \rangle$, i.e., all the transitions occuring in $TS$ are a part of only one rule. ii) $TS\text{-set} \subseteq \bigcup_{r \in \mathcal{R}'} TG_r$ for some $\mathcal{R}' \subseteq \mathcal{R}$ with $|\mathcal{R}'| > 1$.

a. Case $TS\text{-set} \subseteq TG_r$ for some $r \in \mathcal{R}$:
<figure><img src="image_13.png" /><figcaption>■ **Figure 9** A STA $\mathcal{S}$ template for which atleast 4 processes are required to reach $q_3$ and on the right of the figure are gadgets corresponding to its rules. Note that $q_3$ is reachable in $A_{\mathcal{S}}^3$ where $A_{\mathcal{S}}$ is the corresponding guarded timed automata</figcaption></figure>

We claim that in this case $TS-set = TG_r$, i.e., if some of the transitions of $TG_r$ appear in $TS$, then all of them must appear because of following observations:

- First, note that all transitions in $T_{r,2}$ have $p_{r,m}$ as a location guard, so $p_{r,m}$ has to be occupied to take any of these transitions. So if a transition from $T_{r,2}$ appears in $TS-set$, since $(q_{r,m}, g_{r,m}, C_{r,m} \cup \{c_{sync}\}, l_{r,m}, \{p_{r,m-1}\}, p_{r,m}) \in T_{r,1}$ is the only incoming transition to $p_{r,m}$, then we know that it must also be in $TS-set$. But for every $i > 1$ we have that $(q_{r,i}, g_{r,i}, C_{r,i} \cup \{c_{sync}\}, l_{r,i}, p_{r,i-1}, p_{r,i}) \in T_{r,1}$ has $p_{r,i-1}$ as a location guard, so all elements of $T_{r,1}$ must be in $TS-set$.

- If for some $i \in \{1, \dots, m\}$ a transition $(q_{r,i}, g_{r,i}, C_{r,i} \cup \{c_{sync}\}, l_{r,i}, p_{r,i-1}, p_{r,i}) \in T_{r,1}$ appears in $TS$ then $(p_{r,i}, \top, \emptyset, \sigma_{r,i}, p_{r,m}, q_{r,i}) \in T_{r,2}$ must also appear in $TS$, otherwise the process that takes the former transition would either be stuck in the auxiliary location $p_{r,i}$ or be in the sink location $q_{\perp}$ by the end of $\pi$, contradicting the assumption that $c_{AS}$ is stable.

Thus, if one of the transitions in $TG_r$ appears in $TS$, we can assume that all of them appear. Furthermore, since all transitions are taken without a delay, we know that the initial configuration $c_{AS,0}$ satisfies the clock guards of all transitions in $T_{r,1}$, and therefore all clock guards of rule $r$, i.e., rule $r$ can be fired in $\mathcal{S}$ from $c_{S,0}$. To prove the claim, consider which local configurations can be contained in $c_{AS}$: since the transitions in $TS$ are exactly those from $TG_r$ and we arrive in a stable configuration, $c_{AS}$ must contain $(q'_{r,i}, \mathbf{0})$ for all $1 \le i \le m$. Moreover, note that if $n_1 > m$ then it may contain $(\hat{q}, \mathbf{0})$ (but it does not have to, since every path in the gadget can be taken by an arbitrary number of processes). For both cases, we can find a suitable $n_2$ such that $\mathcal{S}$ reaches a global configuration that contains exactly the same local configurations: if $n_2 = m$, then the resulting $\mathcal{C}_S$ contains exactly all the $(q'_{r,i}, \mathbf{0})$, and if $n_2 > m$, then it additionally contains $(\hat{q}, \mathbf{0})$.

b. Case $TS-set \subseteq \bigcup_{r \in \mathcal{R}'} TG_r$ for some $\mathcal{R}' \subseteq \mathcal{R}$ with $|\mathcal{R}'| > 1$:
For simplicity, consider TS-set $\subseteq TG_{r_1} \cup TG_{r_2}$ for $r_1 \neq r_2 \in \mathcal{R}$. Like in the previous case we can argue that all transitions in $TG_{r_1} \cup TG_{r_2}$ have to appear in TS. To prove the claim, we will reorder the sequence of transitions. Assume w.l.o.g. that $p_{r_1,m_1}$ is reached before $p_{r_2,m_2}$ on $\pi$. We will show that we can reorder the computation such that all transitions from $TG_{r_1}$ are taken before all transitions from $TG_{r_2}$, and we reach the same configuration $c_{AS}$. The overall construction of this proof case is depicted in Fig. 10.

<figure><img src="image_14.png" /><figcaption>■ Figure 10 Constructing a computation of a network of STAs (of possibly a larger size) from a run of a network of corresponding GTA, with an intermediate step of reordering the given run</figcaption></figure>

To see this, we first show that all transitions in $T_{r_1,1}$ are enabled in $c_{AS,0}$, i.e., for every element $q_{r_1,i} \xrightarrow{g_{r_1,i}, c_{r_1,i}, \sigma_{r_1,i}} q'_{r_1,i}$ of $r_1$ we have $(q_{r_1,i}, v_{r_1,i}) \in c_{AS,0}$ with $v_{r_1,i} = g_{r_1,i}$ (and since $c_{AS,0}$ is the initial configuration we know that $v_{r_1,i} = 0$). To see this, remember that $p_{r_1,m_1}$ is reached before $p_{r_2,m_2}$ on $\pi$ and note that none of the transitions of $T_{r_2,2}$ can appear before $p_{r_2,m_2}$ is reached, and therefore none of the $q'_{r_2,i}$ are available when the transitions in $T_{r_1,1}$ are taken. Since moreover $Q \cap P = \emptyset$ (auxiliary locations do not appear in rules $S$) and no time passes in $\pi$, it must be the case that all transitions in $T_{r_1,1}$ are already enabled in $c_{AS,0}$.

Regarding transitions in $T_{r_1,2}$, note that these start in auxiliary locations that are unique to $TG_{r_1}$ and by construction the only location guard is $p_{r_1,m_1}$ (and again, no time passes). Therefore all transitions in $T_{r_1,2}$ are enabled as soon as $p_{r_1,m_1}$ is reached, independently of any transitions from $TG_{r_2}$.

Thus, we can consider a different sequence of transitions $TS' = TS_{\downarrow TG_{r_1}} \cdot TS_{\downarrow TG_{r_2}}$, which is a concatenation of the subsequences obtained by projecting the original sequence onto the transitions in $TG_{r_1}$ or $TG_{r_2}$, respectively. Let $\pi'$ be a computation with $TS'$ its sequence of transitions, and where each transition is taken by the same process as in $\pi$. Therefore, $\pi'$ ends in the same configuration $c_{AS}$.

Note that, since $c_{AS}$ is a stable configuration, we must also reach a stable configuration $c_{AS,1}$ after executing $TS_{\downarrow TG_{r_1}}$ from $c_{AS,0}$ (if $c_{AS,1}$ was not stable, either an auxiliary location of $TG_{r_1}$ or the sink location would be occupied in $c_{AS,1}$, and the same would still be true after executing $TS_{\downarrow TG_{r_2}}$ and reaching $c_{AS}$).

To construct a computation of $S$ that reaches a configuration $c_S$ with the desired property, we show that from a suitably chosen $c_{S,0}$ we can first execute $r_1$ and then $r_2$.
1:30 Parameterized Verification of Timed Networks with Clock Invariants

To this end, first note that by the properties of $c_{A_{S,0}}$ established above we know that $r_1$ can be executed from any initial configuration $c_{S,0}$ that has at least $m_1$ processes. We want to ensure that $c_{A_{S,1}}$ corresponds to the configuration $c_{S,1}$ that is reached after executing $r_1$ in $S$. Similar to what we explained in the first case above, after executing $TS_{\downarrow T_{G_{r_1}}}$ from $c_{A_{S,0}}$, the resulting configuration $c_{A_{S,1}}$ must contain $(q'_{r_1,i}, 0)$ for all $1 \le i \le m_1$, and it may or may not contain $(\hat{q}, 0)$. If it does contain $(\hat{q}, 0)$, then we get to a corresponding $c_{S,1}$ by starting with $m_1 + 1$ processes, otherwise by starting with $m_1$ processes.

To see that $r_2$ can be executed from $c_{S,1}$, first note that $TS_{\downarrow T_{G_{r_2}}}$ can be executed from $c_{A_{S,1}}$ in $A_S$. From this we can conclude that for every element $q_{r_2,i} \xrightarrow{g_{r_2,i}, c_{r_2,i}, \sigma_{r_2,i}} q'_{r_2,i}$ of $r_2$, we have $(q_{r_2,i}, v_{r_2,i}) \in c_{A_{S,1}}$ for some $v_{r_2,i}$ that satisfies $g_{r_2,i}$ (actually, since no time passed, all clock valuations are 0). As $c_{A_{S,1}}$ corresponds to $c_{S,1}$, we have the same property for $c_{S,1}$. However, note that multiple processes occupying the same $(q_{r_2,i}, v_{r_2,i})$ might be necessary to execute $r_2$, e.g., if $q_{r_2,i}$ appears on the left-hand side of multiple elements of $r$. By Lemma 36, for any lower bound on the number of processes required in each local configuration, we can reach a global configuration $c_{S,2}$ that has sufficiently many processes in every local configuration that is needed. As a consequence, we can execute $r_2$ from $c_{S,2}$.

Finally, to ensure that the resulting configuration $c_S$ corresponds to $c_{A_S}$, we need to pick $c_{S,2}$ with the right number of processes in each local configuration by a similar argument as above.

2. Induction step ($l \Rightarrow l+1$):

Let $\pi = c_{A_{S,0}} \to^* c_{A_{S,1}} \xrightarrow{\delta} c_{A_{S,2}} \to^* c_{A_S}$ be a computation with $l+1$ non-zero delay transitions, where the last non-zero delay happens after $c_{A_{S,1}}$, and between $c_{A_{S,2}}$ and $c_{A_S}$ there is a (possibly empty) sequence of discrete transitions with zero delay between them. Note that since we assume that $c_{A_S}$ is stable, also $c_{A_{S,1}}$ and $c_{A_{S,2}}$ need to be stable configurations (since a non-zero delay is not possible if any location from $P$ is occupied, and if the sink location is occupied it will remain occupied forever). Then the timed path $c_{A_{S,0}} \to^* c_{A_{S,1}}$ has only $l$ non-zero delays and by induction hypothesis we get that in $S$ we can reach a configuration $c_{S,1}$ that corresponds to $c_{A_{S,1}}$.

Note that if we can take a delay transition with delay $\delta$ from $c_{A_{S,1}}$, then we can also take it from $c_{S,1}$, and the resulting configuration $c_{S,2}$ will again correspond to $c_{A_{S,2}}$. What remains to be shown is that from $c_{S,2}$ we can reach a configuration $c_S$ that corresponds to $c_{A_S}$. This works essentially in the same way as in the base case, except that now we might need to invoke Lemma 36 even if only a single rule is executed (since in the base case we can freely choose how many processes should be in the initial configuration $c_{S,0}$, whereas here we need to prove that we can bring sufficiently many processes to the local configurations that are needed).

Lemmas 32 and 33 consider reachability of stable configurations of $A_S^n$ that contain given configurations $c_{A_S}$ of $A_S$. We now show that the reachability of stable configurations containing a location $q$ is equivalent to reachability of any configuration containing $q$.

**Lemma 34.** Let $S$ be an STA with set of locations $Q$ and $A_S$ its corresponding GTA. For any $q \in Q$, a configuration $c$ with $q \in c$ is reachable in $A_S$ if and only if a stable configuration $c'$ with $q \in c'$ is reachable in $A_S$.
<figure><img src="image_15.png" /><figcaption>Figure 11 An example of an STA $\mathcal{S}$ for which $\mathcal{L}(S^\infty)\downarrow_{[1,2]} \neq \mathcal{L}(A_S^\infty)\downarrow_{[1,2]}$.</figcaption></figure>

**Proof.** $\Leftarrow$: immediate

1211

1212

1213

1214

1215

1216

1217

1218

1219

1220

1221

⇒: Suppose an intermediate configuration $c$ with $q \in c$ is reachable, and let $\pi = c_0 \to^{*} c_s \to^{*} c$ be the computation that ends in $c$, where $c_s$ is the last stable configuration on $\pi$. Since $c$ is not stable, there are some processes that are in locations $p_{r,i}$ for some $r, i$, or in $q_{\perp}$. For each of these processes, modify the local timed path of the process (i.e., the projection of $\pi$ onto this process) in the following way: Let $p$ be the location that it occupies at the end. At the point in time where the process finally moves to $p$, let the process instead do anything else such that it remains in one of the locations in $Q$. (This is possible since we assumed the absence of timelocks in $\mathcal{S}$)

Then let $\pi'$ be the result of replacing the local timed paths of all these processes with the
modified versions. Note that:

1. $\pi'$ is still a valid computation (as those processes that have been modified cannot be necessary for the steps of other processes after they have moved to their $p$)

1222

1223

2. We did not change the local timed path of the process that occupies $q$ at the end of $\pi$, therefore it also occupies $q$ at the end of $\pi'$

1224

1225

3. $\pi'$ ends in a stable configuration

1226

1227

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

Lemmas 32 to 34 together imply Theorem 25.

1228

Note that our construction is in general not sufficient to prove language equivalence.
Fig. 11 shows an STA $\mathcal{S}$ with three locations and two rules: $r_1$ with $m_1 = 1$, i.e., a single
participating process and $r_2$ with $m_2 = 2$, i.e., two participating processes. An invariant in
location $\hat{q}$ forces any process to take a transition after at most 1 time unit.

1230

1231

1232

1233

1234

1235

1236

1237

However, in the corresponding GTA $A_S$, a process can move from $\hat{q}$ to $p_{r_2,1}$ and from
there to $q_{\perp}$, both without delay and with labels in $\Sigma^{-}$, i.e., that will not appear in the trace.
Therefore, the trace $(1, (1, \sigma_0))$, $(1, (1, \sigma_0))$ is in $\mathcal{L}(A_S^\infty)\downarrow_{[1,2]}$ (where process 2 moves to $q_{\perp}$
and never uses a transition that is visible in the trace), but not in $\mathcal{L}(S^\infty)\downarrow_{[1,2]}$ (where the
second process has to take a visible transition after at most 1 time unit).

**► Definition 35.** For a given configuration $c$ of $S^n$ and a configuration $(q, v)$ of $S$, let $\#(c, (q, v))$ indicate the number of occurrences of $(q, v)$ in $c$.

1238

1239

**► Lemma 36.** *Team Copycat in network of STAs:* In a network of STAs $S^n$, if there is a reachable configuration $c_S$ such that $\#(c_S, (q_i, v_i)) = k_i$ for $1 \le i \le n$, then $\forall 1 \le j \le n$ there exists an $n' \in \mathbb{N}$ and a reachable configuration $c'_S$ in $S^{n'}$ such that $\#(c'_S, (q_i, v_i)) \ge k_i$ for $1 \le i \le n$ and $\#(c'_S, (q_j, v_j)) \ge k_j + 1$.

1240

1241

1242

1243

**Proof.** Let $\pi_S$ be a computation of $S^n$ that ends in $c_S$. In order to prove the lemma, we prove the following *doubling* property: Given a reachable configuration $c_S = ((q_1, v_1) \dots (q_n, v_n))$ in $S^n$, we prove the configuration $c'_S = ((q_1, v_1) \dots (q_n, v_n), (q_{n+1}, v_{n+1}) \dots (q_{2 \cdot n}, v_{2 \cdot n}))$, where $(q_j, v_j) = (q_{j-n}, v_{j-n})$ for $n+1 \le j \le 2 \cdot n$, is reachable in $S^{2 \cdot n}$.

1244

1245

1246

1247

1248
Notice that this property implies there exists a reachable configuration, namely $c'_S$, such that for every $(q, v) \in c_S$, $\#(c'_S, (q, v)) \ge \#(c_S, (q, v)) + 1$ and therefore proving the lemma.

Now we prove the doubling property.

Let $l$ be the number of blocks in $\pi_S$, where a block is either a non-zero delay transition or a sequence of discrete transitions that correspond to the execution of a single rule $r \in \mathcal{R}$. The proof is by induction on $l$, the number of blocks of $\pi_S$.

1. **Base case ($l=0$):** Consider the network of size $2 \cdot n$ and the initial configuration of this new network satisfies the desired property.

2. **Induction step ($l \Rightarrow l+1$):** We consider two cases: the final block in the computation could be a delay transition or the execution of a rule $r \in \mathcal{R}$.

3. **Delay transition:**

In this case $\pi_S$ is of the form $c_{S,0} \to \dots \to c_{S,pre} \xrightarrow{\delta} c_S$. From hypothesis it follows $((q_1, v_1), \dots, (q_m, v_m))'_{S,pre} = ((q_1, v_1), \dots, (q_n, v_n), (q_{n+1}, v_{n+1}), \dots, (q_{2\cdot n}, v_{2\cdot n}))$ where $(q_j, v_j) = (q_{j-n}, v_{j-n})$ for $n+1 \le j \le 2 \cdot n$. Delaying $\delta$ from this configuration results in $c'_S$ which has the desired property.

4. **Execution of rule $r \in \mathcal{R}$:**

In this case $\pi_S$ is of the form $c_{S,0} \to \dots \to c_{S,pre} \to^* c_S$, where the sequence of transitions $c_{S,pre} \to^* c_S$ is an execution of rule $r$, where $r = \langle q_{r,1} \xrightarrow{g_{r,1},c_{r,1},\sigma_{r,1}} q'_{r,1}, \dots, q_{r,m} \xrightarrow{g_{r,m},c_{r,m},\sigma_{r,m}} q'_{r,m} \rangle$.

From hypothesis it follows $c'_{S,pre} = ((q_1, v_1), \dots, (q_n, v_n), (q_{n+1}, v_{n+1}), \dots, (q_{2\cdot n}, v_{2\cdot n}))$ where $(q_j, v_j) = (q_{j-n}, v_{j-n})$ for $n+1 \le j \le 2\cdot n$ is reachable.

Let the computation to $c'_{S,pre}$ be $\pi'_{S,pre} = c_{S,0} \to \dots \to c'_{S,pre}$. We extend $\pi'_{S,pre}$ with two additional blocks each of which correspond to execution of $r$. Let the resulting computation be $\pi'_S = c_{S,0} \to \dots \to c'_{S,pre} \to^* c'_{S,\text{mid}} \to^* c'_S$. More precisely, $c'_S$ is obtained from $c'_{S,pre}$ as follows:

* We first apply the sequence of transitions in $r$ on the configuration $c'_{S,pre}$ (which is of size $2 \cdot n$) during which the processes $1 \dots m$ participate. Note that this is possible because, by assumption $c_{S,pre} \to^* c_S$, and therefore the first $m$ processes (w.l.o.g) satisfy the transitions of $r$. Also the first $m$ configurations of $c'_{S,pre}$ are same as those in $c_{S,pre}$.

* We then apply again the sequence of transitions in $r$, without any delay in between, starting from $c'_{S,\text{mid}}$. Now the processes $n+1, \dots, n+m$ participate (this is possible because the configuration of $j$th process is same as $(j-n)$th process in $c'_{S,pre}$ for $n+1 \le j \le 2 \cdot n$) to finally obtain $c'_S$.

The obtained configuration $c'_S$ has the desired property because in the process of obtaining $c'_S$ from $c'_{S,pre}$ above, both the $k$th and $(k-n)$th, for $n \le k \le n+m$, processes took the same transition from rule $r$ (without any delay in between), while the rest of the processes did not take any transition. Therefore the doubling property is proved, hence proving the lemma.

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