Parameterized Verification of Timed Networks
with Clock Invariants

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 [14] 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 [32, 23]. A long line of research has identified classes of systems and properties for which parameterized verification is decidable [23, 28, 24, 25, 22, 18, 9, 26], 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, 17, 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 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) [31, 12]. It combines the expressive formalism of TAs with the relatively weak communication primitive of disjunctive guards [23]: 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. Consider the example in Figure 1 which illustrates a process’s behavior within an asynchronous communication system, where tasks can be dynamically posted and data is read through shared input channels. The transition from $\mathrm{𝗂𝗇𝗂𝗍}$ to $\mathrm{𝗋𝖾𝖺𝖽𝗂𝗇𝗀}$ is guarded by location $\mathrm{𝗉𝗈𝗌𝗍}$: for a process to take this transition, at least one other process must be in $\mathrm{𝗉𝗈𝗌𝗍}$.

Parameterized model checking of DTNs was first studied in [31], 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.

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 Figure 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 [22, 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 [31], where guard locations cannot have invariants. In this case, it is enough to determine for every guard location $q$ the minimal time $\delta$ at which it can be reached: since a process cannot be forced to leave, $q$ can be occupied at any time in $[\delta ,\mathrm{\infty })$, and transitions guarded by $q$ can be assumed to be enabled at any time later than $\delta$. This is already the underlying insight of [31], and in [12] it is embedded into a technique that replaces location guards with clock guards $t\ge \delta$, 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.

Let $𝒞$ be a set of clock variables, also called clocks. A clock valuation is a mapping $v:𝒞\to {ℝ}_{\ge 0}$. For a valuation $v$ and a clock $c$, we denote the fractional and integral parts of $v(c)$ by $\mathrm{𝖿𝗋𝖺𝖼}(v(c))$ and $\lfloor v(c)\rfloor$ respectively. We denote by $\mathrm{𝟎}$ the clock valuation that assigns $0$ to every clock, and by $v+\delta$ for $\delta \in {ℝ}_{\ge 0}$ the valuation s.t. $(v+\delta )(c)=v(c)+\delta$ for all $c\in 𝒞$. Given a subset ${𝒞}_r\subseteq 𝒞$ of clocks and a valuation $v$, $v[{𝒞}_r\leftarrow 0]$ denotes the valuation $v^{\prime }$ such that $v^{\prime }(c)=0$ if $c\in {𝒞}_r$ and $v^{\prime }(c)=v(c)$ otherwise. We call clock constraints $\mathrm{\Psi }(𝒞)$ the terms of the following grammar: $\psi ⩴\top \mid \psi \wedge \psi \mid c\sim d\mid c\sim c^{\prime }+d$ with $d\in \mathbb{N}$, $c,c^{\prime }\in 𝒞$ and

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

TAs were introduced in [8] and clock invariants, also simply called invariants, in [29]. 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). ${\mathrm{\Sigma }}^{-}$ will be used to label silent transitions and unless explicitly specified otherwise (in Sections 4 and 5), we assume that ${\mathrm{\Sigma }}^{-}=\{ϵ\}$.

A configuration of a TA $A$ is a pair $(q,v)$, where $q\in Q$ and $v:𝒞\to {ℝ}_{\ge 0}$ is a clock valuation. A delay transition is of the form $(q,v)\stackrel{𝛿}{\to }(q,v+\delta )$ for some delay $\delta \in {ℝ}_{\ge 0}$ such that $v+\delta \vDash \mathrm{𝐼𝑛𝑣}(q)$. A discrete transition is of the form $(q,v)\stackrel{𝜎}{\to }(q^{\prime },v^{\prime })$, where $\tau =(q,g,{𝒞}_r,\sigma ,q^{\prime })\in 𝒯$, $v\vDash g$, $v^{\prime }=v[{𝒞}_r\leftarrow 0]$ and $v^{\prime }\vDash \mathrm{𝐼𝑛𝑣}(q^{\prime })$. A transition $(q,v)\stackrel{\mathit{ϵ}}{\to }(q^{\prime },v^{\prime })$ is called an $ϵ$-transition. We write $(q,v)\stackrel{\delta ,\sigma }{\to }(q^{\prime },v^{\prime })$ if there is a delay transition $(q,v)\stackrel{𝛿}{\to }(q,v+\delta )$ followed by a discrete transition $(q,v+\delta )\stackrel{𝜎}{\to }(q^{\prime },v^{\prime })$.

A timed path of $A$ is a finite sequence of transitions $\rho =(q_0,v_0)\stackrel{{\delta }_0,{\sigma }_0}{\to }\mathrm{\dots }\stackrel{{\delta }_{l-1},{\sigma }_{l-1}}{\to }(q_l,v_l)$. For a timed path $\rho =(q_0,v_0)\stackrel{{\delta }_0,{\sigma }_0}{\to }\mathrm{\dots }\stackrel{{\delta }_{l-1},{\sigma }_{l-1}}{\to }(q_l,v_l)$, let 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 {ℝ}_{\ge 0}$ s.t. $\delta (\rho )\le b$ for every timed path $\rho$ starting in $(q,v)$. We write $(q_0,v_0){\to }^{\ast }(q_l,v_l)$ if there is a timed path $\rho =(q_0,v_0)\stackrel{{\delta }_0,{\sigma }_0}{\to }\mathrm{\dots }\stackrel{{\delta }_{l-1},{\sigma }_{l-1}}{\to }(q_l,v_l)$; $\rho$ is a computation if $q_0=\widehat{q}$ and $v_0=\mathrm{𝟎}$.

The trace of the timed path $\rho$ is the sequence of pairs of delays and labels obtained by removing transitions with a label from ${\mathrm{\Sigma }}^{-}$ and adding the delays of these to the following transition. The language of $A$, denoted $ℒ(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.

Intuitively, a transition $\tau =(q,g,{𝒞}_r,\sigma ,\gamma ,q^{\prime })\in 𝒯$ takes the automaton from location $q$ to $q^{\prime }$; $\tau$ can only be taken if clock guard $g$ and location guard $\gamma$ are both satisfied, and it resets all clocks in ${𝒞}_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 $\mathrm{𝐼𝑛𝑣}(q)=\top$.

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 $𝔠$ of an NGTA $A^n$ is a tuple $((q_1,v_1),\mathrm{\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 $(ℭ,\widehat{𝔠},T)$, where $ℭ$ denotes the set of all configurations of $A^n$, $\widehat{𝔠}$ is the unique initial configuration ${(\widehat{q},\mathrm{𝟎})}^n$, and the transition relation $T$ is the union of the following delay and discrete transitions:

delay transition

$((q_1,v_1),\mathrm{\dots },(q_n,v_n))\stackrel{𝛿}{\to }((q_1,v_1+\delta ),\mathrm{\dots },(q_n,v_n+\delta ))$ if $\forall i\in \{1,\mathrm{\dots },n\}:v_i+\delta \vDash \mathrm{𝐼𝑛𝑣}(q_i)$, i.e., we can delay $\delta \in {ℝ}_{\ge 0}$ units of time if all clock invariants are satisfied at the end of the delay.

discrete transition

$((q_1,v_1),\mathrm{\dots },(q_n,v_n))\stackrel{(i,\sigma )}{\to }((q_1^{\prime },v_1^{\prime }),\mathrm{\dots },(q_n^{\prime },v_n^{\prime }))$ for some $i\in \{1,\mathrm{\dots },n\}$ if

1. 1)

   $(q_i,v_i)\stackrel{𝜎}{\to }(q_i^{\prime },v_i^{\prime })$ is a discrete transition of $A$ with $\tau =(q_i,g,{𝒞}_r,\sigma ,\gamma ,q_i^{\prime })$,

2. 2)

   $\gamma =\top$ or $q_j=\gamma$ for some $j\in \{1,\mathrm{\dots },n\}\setminus \{i\}$, and

3. 3)

   $q_j^{\prime }=q_j$ and $v_j^{\prime }=v_j$ for all $j\in \{1,\mathrm{\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 $𝔠\stackrel{\delta ,(i,\sigma )}{\to }{𝔠}^{\prime \prime }$ for a delay transition $𝔠\stackrel{𝛿}{\to }{𝔠}^{\prime }$ followed by a discrete transition ${𝔠}^{\prime }\stackrel{(i,\sigma )}{\to }{𝔠}^{\prime \prime }$. Then, a timed path of $A^n$ is a finite sequence $\pi ={𝔠}_0\stackrel{{\delta }_0,(i_0,{\sigma }_0)}{\to }\mathrm{\cdots }\stackrel{{\delta }_{l-1},(i_{l-1},{\sigma }_{l-1})}{\to }{𝔠}_l$.

For a timed path $\pi ={𝔠}_0\stackrel{{\delta }_0,(i_0,{\sigma }_0)}{\to }\mathrm{\cdots }\stackrel{{\delta }_{l-1},(i_{l-1},{\sigma }_{l-1})}{\to }{𝔠}_l$, let 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 ${𝔠}_0=\widehat{𝔠}$. Its length is equal to $2l$.

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

The trace of the timed path $\pi$ is a sequence $\mathrm{𝗍𝗋𝖺𝖼𝖾}(\pi )=({\delta }_0^{\prime },(i_0^{\prime },{\sigma }_0^{\prime }))\mathrm{\dots }({\delta }_{l-1}^{\prime },(i_{l-1}^{\prime },{\sigma }_{l-1}^{\prime }))$ obtained by removing all discrete transitions $(j,{\sigma }_j)$ of $\pi$ with ${\sigma }_j\in {\mathrm{\Sigma }}^{-}$, and adding all delays of these transitions to the following discrete transition, yielding the ${\delta }_j^{\prime }$. The language of $A^n$, denoted $ℒ(A^n)$, is the set of traces of all of its computations.

We will also use projections of these global objects onto subsets of the processes. That is, if $𝔠=((q_1,v_1),\mathrm{\dots },(q_n,v_n))$ and $ℐ=\{i_1,\mathrm{\dots },i_k\}\subseteq \{1,\mathrm{\dots },n\}$, then $𝔠{\downarrow }_{ℐ}$ is the tuple $((q_{i_1},v_{i_1}),\mathrm{\dots },(q_{i_k},v_{i_k}))$, and we extend this notation to computations $\pi {\downarrow }_{ℐ}$ by keeping only the discrete transitions of $ℐ$ and by adding the delays of the removed discrete transitions to the delay of the following discrete transition of $ℐ$.

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 $\mathrm{𝖴𝖦}(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)\stackrel{({\delta }_{k_0}^{\prime },{\sigma }_{k_0})}{\to }\mathrm{\dots }\stackrel{({\delta }_{k_m}^{\prime },{\sigma }_{k_m})}{\to }(q_{m+1},v_{m+1})$. We also extend this to traces; that is, $\mathrm{𝗍𝗋𝖺𝖼𝖾}(\pi ){\downarrow }_a=({\delta }_{k_0}^{\prime },{\sigma }_{k_0})\mathrm{\dots }({\delta }_{k_m}^{\prime },{\sigma }_{k_m})$, which is a trace of $\mathrm{𝖴𝖦}(A)$. For a set of traces $L$, and set $ℐ$ of processes, we write $L{\downarrow }_{ℐ}=\{tt{\downarrow }_{ℐ}\mid tt\in L\}$.

Note that the projection of a computation is not necessarily a computation itself, since location guards may not be satisfied.

A prefix of a computation $\pi ={𝔠}_0\stackrel{{\delta }_0,(i_0,{\sigma }_0)}{\to }\mathrm{\cdots }\stackrel{{\delta }_{l-1},(i_{l-1},{\sigma }_{l-1})}{\to }{𝔠}_l$, is a sequence ${𝔠}_0\stackrel{{\delta }_0,(i_0,{\sigma }_0)}{\to }\mathrm{\cdots }\stackrel{{\delta }_{l^{\prime }},(i_{l^{\prime }},{\sigma }_{l^{\prime }})}{\to }{𝔠}_{l^{\prime }}$ with $l^{\prime }\le l-1$. If $\pi$ is a timed path and $d\in {ℝ}_{\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$.