$[{\mu^{\prime}(\mathtt{x}^{\mathtt{p}})}]=[{\mu(\mathtt{x}^{\mathtt{p}})}+\lfloor\delta\rfloor+1]=[{\mu(\mathtt{x}^{\mathtt{p}})}]+\lfloor\delta\rfloor+1=\lambda(\mathtt{x}^{\mathtt{p}})+\lfloor\delta\rfloor+1=\lambda^{\prime}(\mathtt{x}^{\mathtt{p}})$.
Case 2) is analogous.

Now consider $n^{\prime}$, and we need to show
$n^{\prime}(\mathtt{n}^{\mathtt{qr}})=\lfloor\mu^{\prime}(\mathtt{x}^{\mathtt{r}}_{0})-\mu^{\prime}(\mathtt{x}^{\mathtt{q}}_{0})\rfloor$
for every channel $\mathtt{qr}\in\mathtt{C}$. For every channel $\mathtt{qr}$
not mentioning $\mathtt{p}\not\in\left\\{\mathtt{q},\mathtt{r}\right\\}$, the
claim is immediate since
$n^{\prime}(\mathtt{n}^{\mathtt{qr}})=n(\mathtt{n}^{\mathtt{qr}})$ by the
definition of $n^{\prime}$, and $\mu^{\prime},\mu$ take the same value on
clocks $\mathtt{x}^{\mathtt{r}}_{0}$ and, resp.,
$\mathtt{x}^{\mathtt{q}}_{0}$. For every counter
$\mathtt{n}^{\mathtt{qp}}\in\mathtt{N}_{\textrm{yes}}^{+}$ corresponding to an
incoming channel $\mathtt{qp}$, by definition of
$\mathtt{N}_{\textrm{yes}}^{+}$, $n^{\prime}$, and $n^{\prime\prime}$ we have
$\lfloor\mu^{\prime}(\mathtt{x}^{\mathtt{p}}_{0})-\mu^{\prime}(\mathtt{x}^{\mathtt{q}}_{0})\rfloor=\lfloor\mu(\mathtt{x}^{\mathtt{p}}_{0})-\mu(\mathtt{x}^{\mathtt{q}}_{0})\rfloor+\lfloor\delta\rfloor+1=n(\mathtt{n}^{\mathtt{qp}})+\lfloor\delta\rfloor+1=n^{\prime}(\mathtt{n}^{\mathtt{qp}})$,
as required. If
$\mathtt{n}^{\mathtt{qp}}\in\mathtt{N}^{+}\setminus\mathtt{N}_{\textrm{yes}}^{+}$,
then
$\lfloor\mu^{\prime}(\mathtt{x}^{\mathtt{p}}_{0})-\mu^{\prime}(\mathtt{x}^{\mathtt{q}}_{0})\rfloor=\lfloor\mu(\mathtt{x}^{\mathtt{p}}_{0})-\mu(\mathtt{x}^{\mathtt{q}}_{0})\rfloor+\lfloor\delta\rfloor=n(\mathtt{n}^{\mathtt{qp}})+\lfloor\delta\rfloor=n^{\prime}(\mathtt{n}^{\mathtt{qp}})$.
The two cases $\mathtt{n}^{\mathtt{pq}}\in\mathtt{N}_{\textrm{yes}}^{-}$ and
$\mathtt{n}^{\mathtt{pq}}\in\mathtt{N}^{-}\setminus\mathtt{N}_{\textrm{yes}}^{-}$
are similar.

(3) If $\mathsf{op}={\mathsf{test}(\varphi)}$ is a test transition on local
$\mathtt{p}$-clocks, then $\mu^{\prime}=\mu$ and $\mu\models\varphi$. Take
$\lambda^{\prime}=\lambda$, $n^{\prime}=n$, $r^{\prime}=r$, and thus
$c^{\prime}\approx d^{\prime}$. It remains to establish
$d\xrightarrow{\mathsf{op}^{\prime}}d^{\prime}$. There are two cases to
consider.

  1. (1)

In the first case, $\varphi$ is a non-diagonal inequality or modular
constraint. By the definition of $\approx$, the unary class of $\mu$ is
$[\mu]=\lambda$, and, by the definition of unary equivalence,
$\lambda\models\varphi$, and thus the constraint can be checked by reading the
local control state. By the definition of $\mathcal{R}$,
$d\xrightarrow{\mathsf{op}^{\prime}}d^{\prime}$ with
$\mathsf{op}^{\prime}=\mathsf{nop}$.

  2. (2)

In the second case,
$\varphi=\mathtt{x}^{\mathtt{p}}\leq\mathtt{y}^{\mathtt{p}}$ is a fractional
constraint with $\mathtt{x}^{\mathtt{p}},\mathtt{y}^{\mathtt{p}}:\mathbb{I}$
fractional clocks. By assumption,
$\left\\{\mu(\mathtt{x}^{\mathtt{p}})\right\\}\leq\left\\{\mu(\mathtt{y}^{\mathtt{p}})\right\\}$
holds. By (13), $r(\hat{\mathtt{x}}^{\mathtt{p}}_{0})\ominus
r(\hat{\mathtt{x}}^{\mathtt{p}})\leq
r(\hat{\mathtt{x}}^{\mathtt{p}}_{0})\ominus r(\hat{\mathtt{y}}^{\mathtt{p}})$.
By the definition of $K_{0}$, it holds that
$K_{0}(r(\hat{\mathtt{y}}^{\mathtt{p}}),r(\hat{\mathtt{x}}^{\mathtt{p}}),r(\hat{\mathtt{x}}^{\mathtt{p}}_{0}))$;
cf. (6). Thus $d\xrightarrow{\mathsf{op}^{\prime}}d^{\prime}$ with
$\mathsf{op}^{\prime}={\mathsf{test}(K_{0}(\hat{\mathtt{y}}^{\mathtt{p}},\hat{\mathtt{x}}^{\mathtt{p}},\hat{\mathtt{x}}^{\mathtt{p}}_{0})}$.

(4) If $\mathsf{op}={\mathsf{reset}(\mathtt{x}^{\mathtt{p}})}$ is a reset
transition, then $\mu^{\prime}=\mu[\mathtt{x}^{\mathtt{p}}\mapsto 0]$. We
update the unary class as
$\lambda^{\prime}=\lambda[\mathtt{x}^{\mathtt{p}}\mapsto 0]$. Counters are
unchanged $n^{\prime}=n$. There are two cases to consider.

  1. (1)

If $\mathtt{x}^{\mathtt{p}}:\mathbb{N}$ is an integral clock, then also
registers are unchanged $r^{\prime}=r$ and we directly have
$d\xrightarrow{\mathsf{nop}}d^{\prime}$ with $c^{\prime}\approx d^{\prime}$.

  2. (2)

If $\mathtt{x}^{\mathtt{p}}:\mathbb{I}$ is a fractional clock, then we need to
update its corresponding register $\hat{\mathtt{x}}^{\mathtt{p}}$ by taking
$r^{\prime}=r[\hat{\mathtt{x}}^{\mathtt{p}}\mapsto
r(\hat{\mathtt{x}}^{\mathtt{p}}_{0})]$. We execute
$\mathsf{op}^{\prime}=({\mathsf{guess}(\hat{\mathtt{x}}^{\mathtt{p}})};{\mathsf{test}(\hat{\mathtt{x}}^{\mathtt{p}}=\hat{\mathtt{x}}^{\mathtt{p}}_{0})})$
as per the definition of $\mathcal{R}$, and we have
$d\xrightarrow{\mathsf{op}^{\prime}}d^{\prime}$. After the transitions, (13)
is satisfied since
$0=\left\\{\mu^{\prime}(\mathtt{x}^{\mathtt{p}})\right\\}=r^{\prime}(\hat{\mathtt{x}}^{\mathtt{p}})\ominus
r^{\prime}(\hat{\mathtt{x}}^{\mathtt{p}}_{0})=r(\hat{\mathtt{x}}^{\mathtt{p}}_{0})\ominus
r(\hat{\mathtt{x}}^{\mathtt{p}}_{0})=0$.

(5) If
$\mathsf{op}=({\mathsf{send}(\mathtt{pq},\mathtt{m}:\psi^{\mathtt{p}})};{\mathsf{receive}(\mathtt{pq},\mathtt{m}:\psi^{\mathtt{q}})})$
is a send-receive pair, then
${\mathsf{op}^{\mathtt{p}}={\mathsf{send}(\mathtt{pq},\mathtt{m}:\psi^{\mathtt{p}})}}$,
${\mathsf{op}^{\mathtt{q}}={\mathsf{receive}(\mathtt{qp},\mathtt{m}:\psi^{\mathtt{q}})}}$,
and clocks are unchanged $\mu^{\prime}=\mu$. Thus, the unary abstraction
$\lambda^{\prime}=\lambda$, counters $n^{\prime}=n$, and registers
$r^{\prime}=r$ are also unchanged. It is clear that $c^{\prime}\approx
d^{\prime}$. It remains to establish
$d\xrightarrow{\mathsf{op}^{\prime}}d^{\prime}$ for a suitable choice of
$\mathsf{op}^{\prime}$.

By the definition of rendezvous semantics, there exists a valuation for clock
channels ${\mu^{\mathtt{pq}}\in\mathbb{Q}_{\geq
0}^{\mathtt{X}^{\mathtt{pq}}}}$ s.t.
${(\mu,\mu^{\mathtt{pq}})\models\psi^{\mathtt{p}}}$ and
${(\mu,\mu^{\mathtt{pq}}+\delta)\models\psi^{\mathtt{q}}}$ with
$\delta=\mu(\mathtt{x}^{\mathtt{q}}_{0})-\mu(\mathtt{x}^{\mathtt{p}}_{0})$. By
(14) and (15),

$\displaystyle\lfloor\delta\rfloor=n(\mathtt{n}^{\mathtt{pq}})\qquad\textrm{
and }\qquad\left\\{\delta\right\\}=r(\hat{\mathtt{x}}^{\mathtt{q}}_{0})\ominus
r(\hat{\mathtt{x}}^{\mathtt{p}}_{0}).$ (19)

There are now three cases to consider.

  1. (5a)

In the first case, $\psi^{\mathtt{p}}\equiv\mathtt{x}^{\mathtt{pq}}=0$,
$\psi^{\mathtt{q}}\equiv\mathtt{x}^{\mathtt{pq}}\sim k$, and thus
$\mu^{\mathtt{pq}}(\mathtt{x}^{\mathtt{pq}})=0$ and $\lfloor\delta\rfloor\sim
k$. By (19), $n(\mathtt{n}^{\mathtt{pq}})\sim k$. We take
$\mathsf{op}^{\prime}={\mathsf{test}(\mathtt{n}^{\mathtt{pq}}\sim k)}$.

  2. (5b)

In the second case, $\psi^{\mathtt{p}}\equiv\mathtt{x}^{\mathtt{pq}}=0$,
$\psi^{\mathtt{q}}\equiv\mathtt{x}^{\mathtt{pq}}\equiv_{M}k$, and thus
$\mu^{\mathtt{pq}}(\mathtt{x}^{\mathtt{pq}})=0$ and
$\lfloor\delta\rfloor\equiv_{M}k$. By (19),
$n(\mathtt{n}^{\mathtt{pq}})\equiv_{M}k$. we take
$\mathsf{op}^{\prime}={\mathsf{test}(\mathtt{n}^{\mathtt{pq}}\equiv_{M}k)}$.

  3. (5c)

In the third case, $\psi^{\mathtt{p}}\equiv\mathtt{x}^{\mathtt{pq}}=0$,
$\psi^{\mathtt{q}}\equiv\mathtt{x}^{\mathtt{pq}}\leq\mathtt{x}^{\mathtt{q}}$
for fractional clocks
$\mathtt{x}^{\mathtt{pq}},\mathtt{x}^{\mathtt{q}}:\mathbb{I}$, and thus
$\mu^{\mathtt{pq}}(\mathtt{x}^{\mathtt{pq}})=0$ and
$\left\\{\delta\right\\}\leq\left\\{\mu(\mathtt{x}^{\mathtt{q}})\right\\}$. By
(13) and (19), this is the same as
${r(\hat{\mathtt{x}}^{\mathtt{q}}_{0})\ominus
r(\hat{\mathtt{x}}^{\mathtt{p}}_{0})\leq
r(\hat{\mathtt{x}}^{\mathtt{q}}_{0})\ominus r(\hat{\mathtt{x}}^{\mathtt{q}})}$
which by (5) is equivalent to
$K_{0}(r(\hat{\mathtt{x}}^{\mathtt{q}}),r(\hat{\mathtt{x}}^{\mathtt{p}}_{0}),r(\hat{\mathtt{x}}^{\mathtt{q}}_{0}))$.
We take
${\mathsf{op}^{\prime}={\mathsf{test}(K_{0}(\hat{\mathtt{x}}^{\mathtt{q}},\hat{\mathtt{x}}^{\mathtt{p}}_{0},\hat{\mathtt{x}}^{\mathtt{q}}_{0}))}}$.

#### Proof of the back property.

Let $d\to^{*}d^{\prime}$ be a minimal sequence of transitions. By minimality,
no intermediate configuration when going from $d$ to $d^{\prime}$ is of the
form
$d^{\prime}=\left\langle\left\langle(\ell^{\prime\mathtt{p}})_{\mathtt{p}\in\mathtt{P}},\lambda^{\prime}\right\rangle,n^{\prime},r^{\prime}\right\rangle$.
By inspection of the definition of $\mathcal{R}$, we need to consider five
distinct cases.

(1) In the first case, $\mathcal{R}$ is simulating a $\mathsf{nop}$ transition
$\ell^{\mathtt{p}}\xrightarrow{\mathsf{nop}}\\!\\!\mbox{}^{\mathtt{p}}\mathcalligra{r}^{\mathtt{p}}$
of $\mathcal{S}$, and thus by minimality
$d\xrightarrow{\mathsf{nop}}d^{\prime}$ in just one step, with
$\lambda^{\prime}=\lambda$, $n^{\prime}=n$, and $r^{\prime}=r$. Consequently,
$c\xrightarrow{\mathsf{nop}}c^{\prime}$ in
$\left\ldbrack\mathcal{S}\right\rdbrack$ with
$c^{\prime}=\left\langle(\ell^{\prime\mathtt{p}})_{\mathtt{p}\in\mathtt{P}},\mu\right\rangle$
where $\ell^{\prime\mathtt{q}}=\ell^{\mathtt{q}}$ for every
$\mathtt{q}\in\mathtt{P}\setminus\left\\{\mathtt{p}\right\\}$, and thus
$c^{\prime}\approx d^{\prime}$ as required.

(2) In the second case, $\mathcal{R}$ is simulating a local $\mathsf{elapse}$
transition
$\ell^{\mathtt{p}}\xrightarrow{\mathsf{elapse}}\\!\\!\mbox{}^{\mathtt{p}}\mathcalligra{r}^{\mathtt{p}}$
of process $\mathtt{p}$. This is the most involved case. By the definition of
$\mathcal{R}$ and by minimality, transitions in $d\to^{*}d^{\prime}$ decompose
as follows:

$\displaystyle
d=\left\langle\left\langle(\ell^{\mathtt{p}})_{\mathtt{p}\in\mathtt{P}},\lambda\right\rangle,n,r\right\rangle\xrightarrow{\mathsf{nop}}$
$\displaystyle\left\langle\bullet_{\lambda},n,r\right\rangle\xrightarrow{(\mathtt{N}^{+}\texttt{++};\mathtt{N}^{-}\texttt{-}\texttt{-})^{\lfloor\delta\rfloor}}\left\langle\bullet_{\lambda^{\prime\prime}},n^{\prime\prime},r\right\rangle\xrightarrow{\quad}$
$\displaystyle\xrightarrow{{\mathsf{guess}(\hat{x}^{\mathtt{p}}_{1})};{\mathsf{test}(\hat{\mathtt{x}}^{\mathtt{p}}_{1}=\hat{\mathtt{x}}^{\mathtt{p}}_{0})}}$
$\displaystyle\left\langle\bullet_{\lambda^{\prime\prime}}^{1},n^{\prime\prime},r^{\prime\prime}\right\rangle\xrightarrow{{\mathsf{guess}(\hat{x}^{\mathtt{p}}_{0})}}\left\langle\bullet_{\lambda^{\prime\prime}}^{2},n^{\prime\prime},r^{\prime}\right\rangle\xrightarrow{\quad}$
$\displaystyle\xrightarrow{{\mathsf{test}(\varphi)};(\mathtt{N}_{\textrm{yes}}^{+})\texttt{++};(\mathtt{N}_{\textrm{yes}}^{-})\texttt{-}\texttt{-}}$
$\displaystyle\left\langle\bullet_{\lambda^{\prime}}^{3},n^{\prime},r^{\prime}\right\rangle\xrightarrow{\mathsf{nop}}\left\langle\left\langle(\ell^{\prime\mathtt{p}})_{\mathtt{p}\in\mathtt{P}},\lambda^{\prime}\right\rangle,n^{\prime},r^{\prime}\right\rangle=d^{\prime}$

where $\delta\in\mathbb{Q}_{\geq 0}$ it the total elapsed timed that is
simulated, split into its discrete and fractional part
$\delta=\lfloor\delta\rfloor+\left\\{\delta\right\\}$,
$\lambda^{\prime\prime}=\lambda[\mathtt{X}^{\mathtt{p}}\mapsto\mathtt{X}^{\mathtt{p}}+\lfloor\delta\rfloor]$,
$n^{\prime\prime}=n[\mathtt{N}^{+}\mapsto\mathtt{N}^{+}+\lfloor\delta\rfloor,\mathtt{N}^{-}\mapsto\mathtt{N}^{-}-\lfloor\delta\rfloor]$,
$r^{\prime\prime}=r[\hat{x}^{\mathtt{p}}_{1}\mapsto
r(\hat{x}^{\mathtt{p}}_{0})]$,
$r^{\prime}=r^{\prime\prime}[\hat{x}^{\mathtt{p}}_{0}\mapsto
r(\hat{x}^{\mathtt{p}}_{0})\oplus\left\\{\delta\right\\}]$,
$r^{\prime}\models\varphi$,
$\lambda^{\prime}=\lambda^{\prime\prime}[\mathtt{X}^{\mathtt{p}}_{\textrm{yes}}\mapsto\mathtt{X}^{\mathtt{p}}_{\textrm{yes}}+1]$,
and
$n^{\prime}=n^{\prime\prime}[\mathtt{N}_{\textrm{yes}}^{+}\mapsto\mathtt{N}_{\textrm{yes}}^{+}+1,\mathtt{N}_{\textrm{yes}}^{-}\mapsto\mathtt{N}_{\textrm{yes}}^{-}-1]$.
This is simulated in $\mathcal{S}$ by letting process $\mathtt{p}$ elapse
$\delta$ time units and thus go to
$c^{\prime}=\left\langle(\ell^{\prime\mathtt{p}})_{\mathtt{p}\in\mathtt{P}},\mu^{\prime}\right\rangle$,
with $\ell^{\prime\mathtt{q}}=\ell^{\mathtt{q}}$ for every
$\mathtt{q}\in\mathtt{P}\setminus\left\\{\mathtt{p}\right\\}$, where
$\mu^{\prime}=\mu[\forall\mathtt{x}^{\mathtt{p}}\in\mathtt{X}^{\mathtt{p}}{\;\cdot\;}\mathtt{x}^{\mathtt{p}}\mapsto\mu(\mathtt{x}^{\mathtt{p}})+\delta]$
(including the reference clock $\mathtt{x}^{\mathtt{p}}_{0}$). We need to show
that the time elapse transition above is legal in $\mathcal{S}$, which by the
desynchronised semantics amounts to establish that for every channel
$\mathtt{qr}\in\mathtt{C}$,
$\mu^{\prime}(\mathtt{x}^{\mathtt{q}}_{0})\leq\mu^{\prime}(\mathtt{x}^{\mathtt{r}}_{0})$.
Since the value of $\mathtt{x}^{\mathtt{p}}_{0}$ increased during the time
elapse transition,
$\mu(\mathtt{x}^{\mathtt{q}}_{0})=\mu^{\prime}(\mathtt{x}^{\mathtt{q}}_{0})\leq\mu^{\prime}(\mathtt{x}^{\mathtt{p}}_{0})=\mu(\mathtt{x}^{\mathtt{p}}_{0})+\delta$
is immediately satisfied for incoming channels $\mathtt{qp}\in\mathtt{C}$
since $\mu(\mathtt{x}^{\mathtt{q}}_{0})\leq\mu(\mathtt{x}^{\mathtt{p}}_{0})$
follows from the fact that $c$ is a legal configuration in
$\left\ldbrack\mathcal{S}\right\rdbrack$. Let $\mathtt{pq}\in\mathtt{C}$ be an
outgoing channel and we need to establish
$\mu^{\prime}(\mathtt{x}^{\mathtt{q}}_{0})-\mu^{\prime}(\mathtt{x}^{\mathtt{p}}_{0})\geq
0$. The latter inequality will follow immediately from establishing (14) and
(15) for $n^{\prime},r^{\prime},\mu^{\prime}$. For fractional parts, we have

$\displaystyle\left\\{\mu^{\prime}(\mathtt{x}^{\mathtt{q}}_{0})-\mu^{\prime}(\mathtt{x}^{\mathtt{p}}_{0})\right\\}$
$\displaystyle=\left\\{\mu(\mathtt{x}^{\mathtt{q}}_{0})-(\mu(\mathtt{x}^{\mathtt{p}}_{0})+\delta)\right\\}=\left\\{\mu(\mathtt{x}^{\mathtt{q}}_{0})-\mu(\mathtt{x}^{\mathtt{p}}_{0})\right\\}\ominus\delta=$
(by (15)) $\displaystyle=(r(\hat{\mathtt{x}}^{\mathtt{q}}_{0})\ominus
r(\hat{\mathtt{x}}^{\mathtt{p}}_{0}))\ominus\delta=(r^{\prime}(\hat{\mathtt{x}}^{\mathtt{q}}_{0})\ominus(r^{\prime}(\hat{\mathtt{x}}^{\mathtt{p}}_{0})\ominus\delta))\ominus\delta=$
$\displaystyle=r^{\prime}(\hat{\mathtt{x}}^{\mathtt{q}}_{0})\ominus
r^{\prime}(\hat{\mathtt{x}}^{\mathtt{p}}_{0}),$

and thus (15) is again satisfied for $r^{\prime},\mu^{\prime}$. For integral
parts, we consider two cases, depending on whether the channel is incoming or
outgoing.

  1. (1)

For an outgoing channel $\mathtt{pq}$,

$\displaystyle\lfloor\mu^{\prime}(\mathtt{x}^{\mathtt{q}}_{0})-\mu^{\prime}(\mathtt{x}^{\mathtt{p}}_{0})\rfloor=\
\lfloor\mu(\mathtt{x}^{\mathtt{q}}_{0})-(\mu(\mathtt{x}^{\mathtt{p}}_{0})+\delta)\rfloor=$
$\displaystyle=\ $
$\displaystyle\lfloor\mu(\mathtt{x}^{\mathtt{q}}_{0})-\mu(\mathtt{x}^{\mathtt{p}}_{0})-\delta\rfloor=$
$\displaystyle=\ $
$\displaystyle\lfloor\mu(\mathtt{x}^{\mathtt{q}}_{0})-\mu(\mathtt{x}^{\mathtt{p}}_{0})\rfloor-\lfloor\delta\rfloor-\mathbbm{1}_{\left\\{\mu(\mathtt{x}^{\mathtt{q}}_{0})-\mu(\mathtt{x}^{\mathtt{p}}_{0})\right\\}<\left\\{\delta\right\\}?}=$
(by (14), (15)) $\displaystyle=\ $ $\displaystyle
n(\mathtt{n}^{\mathtt{pq}})-\lfloor\delta\rfloor-\mathbbm{1}_{r(\hat{\mathtt{x}}^{\mathtt{q}}_{0})\ominus
r(\hat{\mathtt{x}}^{\mathtt{p}}_{0})<\left\\{\delta\right\\}?}=$ (by the def.
of $\delta$) $\displaystyle=\ $ $\displaystyle
n(\mathtt{n}^{\mathtt{pq}})-\lfloor\delta\rfloor-\mathbbm{1}_{r(\hat{\mathtt{x}}^{\mathtt{q}}_{0})\ominus
r(\hat{\mathtt{x}}^{\mathtt{p}}_{0})<r^{\prime}(\hat{\mathtt{x}}^{\mathtt{p}}_{0})\ominus
r(\hat{\mathtt{x}}^{\mathtt{p}}_{0})?}=$ (by the def. of $r^{\prime}$)
$\displaystyle=\ $ $\displaystyle
n(\mathtt{n}^{\mathtt{pq}})-\lfloor\delta\rfloor-\mathbbm{1}_{r^{\prime}(\hat{\mathtt{x}}^{\mathtt{q}}_{0})\ominus
r^{\prime}(\hat{\mathtt{x}}^{\mathtt{p}}_{1})<r^{\prime}(\hat{\mathtt{x}}^{\mathtt{p}}_{0})\ominus
r^{\prime}(\hat{\mathtt{x}}^{\mathtt{p}}_{1})?}=$ (by the def. of $K_{2}$)
$\displaystyle=\ $ $\displaystyle
n(\mathtt{n}^{\mathtt{pq}})-\lfloor\delta\rfloor-\mathbbm{1}_{K_{2}(r^{\prime}(\hat{\mathtt{x}}^{\mathtt{p}}_{1}),r^{\prime}(\hat{\mathtt{x}}^{\mathtt{q}}_{0}),r^{\prime}(\hat{\mathtt{x}}^{\mathtt{p}}_{0}))?}=$
(by the def. of $n^{\prime}$) $\displaystyle=\ $ $\displaystyle
n^{\prime}(\mathtt{n}^{\mathtt{pq}}),$

thus showing that (14) is again satisfied for $n^{\prime},\mu^{\prime}$ for
outgoing channels $\mathtt{pq}$.

  2. (2)

For an incoming channel $\mathtt{qp}$,

$\displaystyle\lfloor\mu^{\prime}(\mathtt{x}^{\mathtt{p}}_{0})-\mu^{\prime}(\mathtt{x}^{\mathtt{q}}_{0})\rfloor=\lfloor\mu(\mathtt{x}^{\mathtt{p}}_{0})+\delta-\mu(\mathtt{x}^{\mathtt{q}}_{0})\rfloor=$
$\displaystyle=\ $
$\displaystyle\lfloor\mu(\mathtt{x}^{\mathtt{p}}_{0})-\mu(\mathtt{x}^{\mathtt{q}}_{0})\rfloor+\lfloor\delta\rfloor+\mathbbm{1}_{\left\\{\mu(\mathtt{x}^{\mathtt{p}}_{0})-\mu(\mathtt{x}^{\mathtt{q}}_{0})\right\\}+\left\\{\delta\right\\}\geq
1?}=$ (by (14), (15)) $\displaystyle=\ $ $\displaystyle
n(\mathtt{n}^{\mathtt{qp}})+\lfloor\delta\rfloor+\mathbbm{1}_{r(\hat{\mathtt{x}}^{\mathtt{p}}_{0})\ominus
r(\hat{\mathtt{x}}^{\mathtt{q}}_{0})+\left\\{\delta\right\\}\geq 1?}=$ (by the
def. of $\delta$) $\displaystyle=\ $ $\displaystyle
n(\mathtt{n}^{\mathtt{qp}})+\lfloor\delta\rfloor+\mathbbm{1}_{(r(\hat{\mathtt{x}}^{\mathtt{p}}_{0})\ominus
r(\hat{\mathtt{x}}^{\mathtt{q}}_{0}))+(r^{\prime}(\hat{\mathtt{x}}^{\mathtt{p}}_{0})\ominus
r(\hat{\mathtt{x}}^{\mathtt{p}}_{0}))\geq 1?}=$ $\displaystyle=\ $
$\displaystyle
n(\mathtt{n}^{\mathtt{qp}})+\lfloor\delta\rfloor+\mathbbm{1}_{r(\hat{\mathtt{x}}^{\mathtt{p}}_{0})\ominus
r(\hat{\mathtt{x}}^{\mathtt{q}}_{0})\geq
r(\hat{\mathtt{x}}^{\mathtt{p}}_{0})\ominus
r^{\prime}(\hat{\mathtt{x}}^{\mathtt{p}}_{0})?}=$ (by the def. of
$r^{\prime}$) $\displaystyle=\ $ $\displaystyle
n(\mathtt{n}^{\mathtt{qp}})+\lfloor\delta\rfloor+\mathbbm{1}_{r^{\prime}(\hat{\mathtt{x}}^{\mathtt{p}}_{1})\ominus
r^{\prime}(\hat{\mathtt{x}}^{\mathtt{q}}_{0})\geq
r^{\prime}(\hat{\mathtt{x}}^{\mathtt{p}}_{1})\ominus
r^{\prime}(\hat{\mathtt{x}}^{\mathtt{p}}_{0})?}=$ (by the def. of $K_{1}$)
$\displaystyle=\ $ $\displaystyle
n(\mathtt{n}^{\mathtt{qp}})+\lfloor\delta\rfloor+\mathbbm{1}_{K_{1}(r^{\prime}(\hat{\mathtt{x}}^{\mathtt{p}}_{1}),r^{\prime}(\hat{\mathtt{x}}^{\mathtt{q}}_{0}),r^{\prime}(\hat{\mathtt{x}}^{\mathtt{p}}_{0}))?}=$
(by def. of $n^{\prime}$) $\displaystyle=\ $ $\displaystyle
n^{\prime}(\mathtt{n}^{\mathtt{pq}}).$

thus showing that (14) is again satisfied for $n^{\prime},\mu^{\prime}$ for
incoming channels $\mathtt{qp}$.

Also (13) holds:

$\displaystyle\left\\{\mu^{\prime}(\mathtt{x}^{\mathtt{p}})\right\\}$
$\displaystyle=\left\\{\mu(\mathtt{x}^{\mathtt{p}})+\delta\right\\}=\left\\{\mu(\mathtt{x}^{\mathtt{p}})\right\\}\oplus\delta=$
(by (13)) $\displaystyle=(r(\hat{\mathtt{x}}^{\mathtt{p}}_{0})\ominus
r(\hat{\mathtt{x}}^{\mathtt{p}}))\oplus\delta=(r(\hat{\mathtt{x}}^{\mathtt{p}}_{0})\oplus\delta)\ominus
r(\hat{\mathtt{x}}^{\mathtt{p}})=$
$\displaystyle=r^{\prime}(\hat{\mathtt{x}}^{\mathtt{p}}_{0})\ominus
r^{\prime}(\hat{\mathtt{x}}^{\mathtt{p}}).$

Finally, also (12) holds:

$\displaystyle[{\mu^{\prime}(\mathtt{x}^{\mathtt{p}})}]=\ $
$\displaystyle[{\mu(\mathtt{x}^{\mathtt{p}})+\delta}]=$ $\displaystyle=\ $
$\displaystyle[{\mu(\mathtt{x}^{\mathtt{p}})}]+\lfloor\delta\rfloor+\mathbbm{1}_{\left\\{\mu(\mathtt{x}^{\mathtt{p}})\right\\}+\left\\{\delta\right\\}\geq
1?}=$ (by (12), (13)) $\displaystyle=\ $
$\displaystyle\lambda(\mathtt{x}^{\mathtt{p}})+\lfloor\delta\rfloor+\mathbbm{1}_{r(\hat{\mathtt{x}}^{\mathtt{p}}_{0})\ominus
r(\hat{\mathtt{x}}^{\mathtt{p}})+\left\\{\delta\right\\}\geq 1?}=$ (by the
def. of $\delta$) $\displaystyle=\ $
$\displaystyle\lambda(\mathtt{x}^{\mathtt{p}})+\lfloor\delta\rfloor+\mathbbm{1}_{(r(\hat{\mathtt{x}}^{\mathtt{p}}_{0})\ominus
r(\hat{\mathtt{x}}^{\mathtt{p}}))+(r^{\prime}(\hat{\mathtt{x}}^{\mathtt{p}}_{0})\ominus
r(\hat{\mathtt{x}}^{\mathtt{p}}_{0}))\geq 1?}=$ (by the def. of $r^{\prime}$)
$\displaystyle=\ $
$\displaystyle\lambda(\mathtt{x}^{\mathtt{p}})+\lfloor\delta\rfloor+\mathbbm{1}_{(r^{\prime}(\hat{\mathtt{x}}^{\mathtt{p}}_{1})\ominus
r^{\prime}(\hat{\mathtt{x}}^{\mathtt{p}}))+(r^{\prime}(\hat{\mathtt{x}}^{\mathtt{p}}_{0})\ominus
r^{\prime}(\hat{\mathtt{x}}^{\mathtt{p}}_{1}))\geq 1?}=$ $\displaystyle=\ $
$\displaystyle\lambda(\mathtt{x}^{\mathtt{p}})+\lfloor\delta\rfloor+\mathbbm{1}_{r^{\prime}(\hat{\mathtt{x}}^{\mathtt{p}}_{1})\ominus
r^{\prime}(\hat{\mathtt{x}}^{\mathtt{p}})\geq
r^{\prime}(\hat{\mathtt{x}}^{\mathtt{p}}_{1})\ominus
r^{\prime}(\hat{\mathtt{x}}^{\mathtt{p}}_{0})?}=$ (by the def. of $K_{1}$)
$\displaystyle=\ $
$\displaystyle\lambda(\mathtt{x}^{\mathtt{p}})+\lfloor\delta\rfloor+\mathbbm{1}_{K_{1}(r^{\prime}(\hat{\mathtt{x}}^{\mathtt{p}}_{1}),r^{\prime}(\hat{\mathtt{x}}^{\mathtt{p}}),r^{\prime}(\hat{\mathtt{x}}^{\mathtt{p}}_{0}))?}=$
(by def. of $\lambda^{\prime}$) $\displaystyle=\ $
$\displaystyle\lambda^{\prime}(\mathtt{x}^{\mathtt{p}}).$

Altogether, this establishes that the transition
$c\xrightarrow{\delta}c^{\prime}$ is legal and that $c^{\prime}\approx
d^{\prime}$, as required.

(3) In the third case, $\mathcal{R}$ is simulating a test transition
$\ell^{\mathtt{p}}\xrightarrow{{\mathsf{test}(\varphi)}}\\!\\!\mbox{}^{\mathtt{p}}\mathcalligra{r}^{\mathtt{p}}$.
By minimality, $d\xrightarrow{\mathsf{op}}d^{\prime}$ with
$d^{\prime}=\left\langle\left\langle(\ell^{\prime\mathtt{p}})_{\mathtt{p}\in\mathtt{P}},\lambda\right\rangle,n,r\right\rangle$
where $\ell^{\prime\mathtt{q}}=\ell^{\mathtt{q}}$ for every
$\mathtt{q}\in\mathtt{P}\setminus\left\\{\mathtt{p}\right\\}$. Accordingly, we
take
$c^{\prime}=\left\langle(\ell^{\prime\mathtt{p}})_{\mathtt{p}\in\mathtt{P}},\mu\right\rangle$
and thus $c^{\prime}\approx d^{\prime}$ follows immediately from $c\approx d$.
We need to show that $c\xrightarrow{{\mathsf{test}(\varphi)}}c^{\prime}$.
Following the definition of $\mathcal{R}$, we proceed by a case analysis on
$\mathsf{op}$.

  1. (1)

If $\mathsf{op}=\mathsf{nop}$, then $\varphi\equiv\mathtt{x}^{\mathtt{p}}\sim
k$ or $\varphi\equiv\mathtt{x}^{\mathtt{p}}\equiv_{m}k$ and it holds that
$\lambda\models\varphi$. In the first case, this means that
$\lambda(\mathtt{x}^{\mathtt{p}})\sim k$ holds. By (12),
$\lambda(\mathtt{x}^{\mathtt{p}})=[{\mu(\mathtt{x}^{\mathtt{p}})}]$ and since
the unary equivalence is sound when computed w.r.t. the maximal constant,
$\lfloor\mu(\mathtt{x}^{\mathtt{p}})\rfloor\sim k$ holds. Since
$\mathtt{x}^{\mathtt{p}}:\mathbb{N}$ is an integral clock, $\mu\models\varphi$
holds, as required. The reasoning for the second case is analogous.

  2. (2)

If
$\mathsf{op}={\mathsf{test}(K_{0}(\hat{\mathtt{y}}^{\mathtt{p}},\hat{\mathtt{x}}^{\mathtt{p}},\hat{\mathtt{x}}^{\mathtt{p}}_{0}))}$,
then $\varphi\equiv\mathtt{x}^{\mathtt{p}}\leq\mathtt{y}^{\mathtt{p}}$ for
fractional clocks
$\mathtt{x}^{\mathtt{p}},\mathtt{y}^{\mathtt{p}}:\mathbb{I}$. Thus
$K_{0}(r(\hat{\mathtt{y}}^{\mathtt{p}}),r(\hat{\mathtt{x}}^{\mathtt{p}}),r(\hat{\mathtt{x}}^{\mathtt{p}}_{0}))$
holds. By (6), $r(\hat{\mathtt{x}}^{\mathtt{p}}_{0})\ominus
r(\hat{\mathtt{x}}^{\mathtt{p}})\leq
r(\hat{\mathtt{x}}^{\mathtt{p}}_{0})\ominus r(\hat{\mathtt{y}}^{\mathtt{p}})$.
By (13),
$\left\\{\mu(\mathtt{x}^{\mathtt{p}})\right\\}\leq\left\\{\mu(\mathtt{y}^{\mathtt{p}})\right\\}$,
and thus $\mu\models\varphi$ holds, as required.

(4) In the fourth case, $\mathcal{R}$ is simulating a reset transition
$\ell^{\mathtt{p}}\xrightarrow{{\mathsf{reset}(\mathtt{x}^{\mathtt{p}})}}\\!\\!\mbox{}^{\mathtt{p}}\mathcalligra{r}^{\mathtt{p}}$
for a clock $\mathtt{x}^{\mathtt{p}}$ of process $\mathtt{p}$. By minimality,
$d\xrightarrow{\mathsf{op}}d^{\prime}$ with
$d^{\prime}=\left\langle\left\langle(\ell^{\prime\mathtt{p}})_{\mathtt{p}\in\mathtt{P}},\lambda^{\prime}\right\rangle,n,r^{\prime}\right\rangle$
where $\ell^{\prime\mathtt{q}}=\ell^{\mathtt{q}}$ for every
$\mathtt{q}\in\mathtt{P}\setminus\left\\{\mathtt{p}\right\\}$. We take
$c^{\prime}=\left\langle(\ell^{\prime\mathtt{p}})_{\mathtt{p}\in\mathtt{P}},\mu^{\prime}\right\rangle$
with $\mu^{\prime}=\mu[\mathtt{x}^{\mathtt{p}}\mapsto 0]$. Clearly,
$c\xrightarrow{{\mathsf{reset}(\mathtt{x}^{\mathtt{p}})}}c^{\prime}$ holds. In
order to show that (12), (13) hold again for
$\lambda^{\prime},r^{\prime},\mu^{\prime}$, we do a case analysis on
$\mathsf{op}$.

  1. (1)

In the first case, $\mathsf{op}=\mathsf{nop}$. By the definition of
$\mathcal{R}$, $\mathtt{x}^{\mathtt{p}}:\mathbb{N}$ is an integral clock and
$\lambda^{\prime}=\lambda[\mathtt{x}^{\mathtt{p}}\mapsto 0]$ and
$r^{\prime}=r$. Obviously
$\lambda^{\prime}(\mathtt{x}^{\mathtt{p}})=[0]=[{\mu^{\prime}(\mathtt{x}^{\mathtt{p}})}]$,
and for every other clock
$\mathtt{x}^{\mathtt{q}}\neq\mathtt{x}^{\mathtt{p}}$,
$\lambda^{\prime}(\mathtt{x}^{\mathtt{p}})=\lambda(\mathtt{x}^{\mathtt{p}})=\textrm{(by\leavevmode\nobreak\
\eqref{eq:unary})}=[{\mu(\mathtt{x}^{\mathtt{q}})}]=[{\mu^{\prime}(\mathtt{x}^{\mathtt{q}})}]$.
Thus, (12) holds again for $\lambda^{\prime},\mu^{\prime}$. (That (13) holds
is trivial since $r^{\prime}=r$ and
$\mu^{\prime}(\mathtt{x}^{\mathtt{q}})=\mu(\mathtt{x}^{\mathtt{q}})$ for
fractional clocks $\mathtt{x}^{\mathtt{q}}:\mathbb{I}$.)

  2. (2)

In the second case,
$\mathsf{op}=({\mathsf{guess}(\hat{\mathtt{x}}^{\mathtt{p}})};{\mathsf{test}(\hat{\mathtt{x}}^{\mathtt{p}}=\hat{\mathtt{x}}^{\mathtt{p}}_{0})})$.
Consequently, $r^{\prime}=r[\hat{\mathtt{x}}^{\mathtt{p}}\mapsto
r(\hat{\mathtt{x}}^{\mathtt{p}}_{0})]$. Therefore,
$r^{\prime}(\hat{\mathtt{x}}^{\mathtt{p}}_{0})\ominus
r^{\prime}(\hat{\mathtt{x}}^{\mathtt{p}})=r(\hat{\mathtt{x}}^{\mathtt{p}}_{0})\ominus
r(\hat{\mathtt{x}}^{\mathtt{p}}_{0})=0=\left\\{\mu^{\prime}(\mathtt{x}^{\mathtt{p}})\right\\}$.
Thus, (13) holds again for $r^{\prime},\mu^{\prime}$. (That (12) holds is
trivial since $\lambda^{\prime}=\lambda$ and
$\mu^{\prime}(\mathtt{x}^{\mathtt{q}})=\mu(\mathtt{x}^{\mathtt{q}})$ for
integral clocks $\mathtt{x}^{\mathtt{q}}:\mathbb{N}$.)

(5) In the fifth, and last case, $\mathcal{R}$ simulates a send-receive pair
of transitions
${\ell^{\mathtt{p}}\xrightarrow{\mathsf{op}^{\mathtt{p}}}\\!\\!\mbox{}^{\mathtt{p}}\mathcalligra{r}^{\mathtt{p}}}$
of $\mathtt{p}$ with
$\mathsf{op}^{\mathtt{p}}={\mathsf{send}(\mathtt{pq},m:\psi^{\mathtt{p}})}$
and
${\ell^{\mathtt{q}}\xrightarrow{\mathsf{op}^{\mathtt{q}}}\\!\\!\mbox{}^{\mathtt{q}}\mathcalligra{r}^{\mathtt{q}}}$
of $\mathtt{q}$ with
$\mathsf{op}^{\mathtt{q}}={\mathsf{receive}(\mathtt{pq},m:\psi^{\mathtt{q}})}$.
By the definition of $\mathcal{R}$ and by minimality,
$d\xrightarrow{{\mathsf{test}(()}\varphi)}d^{\prime}$ with
$d^{\prime}=\left\langle\left\langle(\ell^{\prime\mathtt{p}})_{\mathtt{p}\in\mathtt{P}},\lambda\right\rangle,n,r\right\rangle$
where $\ell^{\prime\mathtt{r}}=\ell^{\mathtt{r}}$ for every
$\mathtt{r}\in\mathtt{P}\setminus\left\\{\mathtt{p},\mathtt{q}\right\\}$. We
take
$c^{\prime}=\left\langle(\ell^{\prime\mathtt{p}})_{\mathtt{p}\in\mathtt{P}},\mu\right\rangle$
and we need to argue that in
$\left\ldbrack\mathcal{S}\right\rdbrack^{\textsf{rv}}$ we can take the
rendezvous transition
$c\xrightarrow{(\mathsf{op}^{\mathtt{p}},\mathsf{op}^{\mathtt{q}})}c^{\prime}$.
Let
$\delta=\mu(\mathtt{x}^{\mathtt{q}}_{0})-\mu^{(}\mathtt{x}^{\mathtt{p}}_{0})\geq
0$ be the desynchronisation between sender and receiver. Following the
definition of desynchronised semantics, we need to show that there exists a
valuation for clock channels ${\mu^{\mathtt{pq}}\in\mathbb{Q}_{\geq
0}^{\mathtt{X}^{\mathtt{pq}}}}$ s.t.
${(\mu,\mu^{\mathtt{pq}})\models\psi^{\mathtt{p}}}$ and
${(\mu,\mu^{\mathtt{pq}}+\delta)\models\psi^{\mathtt{q}}}$. We proceed by a
case analysis on the condition $\varphi$.

  1. (5a)

In the first case, $\varphi\equiv\mathtt{n}^{\mathtt{pq}}\sim k$ is an
inequality counter constraint, and thus $n(\mathtt{n}^{\mathtt{pq}})\sim k$
holds. Then, $\psi^{\mathtt{p}}\equiv\mathtt{x}^{\mathtt{pq}}=0$ and
$\psi^{\mathtt{q}}\equiv\mathtt{x}^{\mathtt{pq}}\sim k$ with
$\mathtt{x}^{\mathtt{pq}}:\mathbb{N}$ an integral clock. Take
$\mu^{\mathtt{pq}}(\mathtt{x}^{\mathtt{pq}})=0$. Clearly
${(\mu,\mu^{\mathtt{pq}})\models\psi^{\mathtt{p}}}$ is satisfied. By (14),
$n(\mathtt{n}^{\mathtt{pq}})=\lfloor\mu(\mathtt{x}^{\mathtt{q}}_{0})-\mu(\mathtt{x}^{\mathtt{p}}_{0})\rfloor=\lfloor\delta\rfloor$
and thus
$\lfloor\delta\rfloor=\lfloor\mu^{\mathtt{pq}}(\mathtt{x}^{\mathtt{pq}})+\delta\rfloor\sim
k$ holds. Since $\mathtt{x}^{\mathtt{pq}}:\mathbb{N}$ is an integral clock,
the latter is equivalent to
$\mu^{\mathtt{pq}}(\mathtt{x}^{\mathtt{pq}})+\delta\models\mathtt{x}^{\mathtt{pq}}\sim
k$, thus showing
${(\mu,\mu^{\mathtt{pq}}+\delta)\models\mathtt{x}^{\mathtt{pq}}\sim k}$, as
required.

  2. (5b)

In the second case, $\varphi\equiv\mathtt{n}^{\mathtt{pq}}\equiv_{M}k$ is a
modular counter constraint, and we reason as above.

  3. (5c)

In the last case, $\varphi\equiv
K_{0}(\hat{\mathtt{x}}^{\mathtt{q}},\hat{\mathtt{x}}^{\mathtt{p}}_{0},\hat{\mathtt{x}}^{\mathtt{q}}_{0})$
is a register constraint; thus
$K_{0}(r(\hat{\mathtt{x}}^{\mathtt{q}}),r(\hat{\mathtt{x}}^{\mathtt{p}}_{0}),r(\hat{\mathtt{x}}^{\mathtt{q}}_{0}))$
holds. Then, ${\psi^{\mathtt{p}}\equiv\mathtt{x}^{\mathtt{pq}}=0}$ and
${\psi^{\mathtt{q}}\equiv\mathtt{x}^{\mathtt{pq}}\leq\mathtt{x}^{\mathtt{q}}}$
with $\mathtt{x}^{\mathtt{pq}},\mathtt{x}^{\mathtt{q}}:\mathbb{I}$ two
fractional clocks. Take $\mu^{\mathtt{pq}}(\mathtt{x}^{\mathtt{pq}})=0$.
Clearly ${(\mu,\mu^{\mathtt{pq}})\models\psi^{\mathtt{p}}}$ is satisfied. By
the definition of $K_{0}$, $r(\hat{\mathtt{x}}^{\mathtt{q}}_{0})\ominus
r(\hat{\mathtt{x}}^{\mathtt{p}}_{0})\leq
r(\hat{\mathtt{x}}^{\mathtt{q}}_{0})\ominus r(\hat{\mathtt{x}}^{\mathtt{q}})$
(cf. (7)). By (15), $r(\hat{\mathtt{x}}^{\mathtt{q}}_{0})\ominus
r(\hat{\mathtt{x}}^{\mathtt{p}}_{0})=\left\\{\delta\right\\}$, and by (13),
$r(\hat{\mathtt{x}}^{\mathtt{q}}_{0})\ominus
r(\hat{\mathtt{x}}^{\mathtt{q}})=\left\\{\mu(\mathtt{x}^{\mathtt{q}})\right\\}$.
Thus,
$\left\\{\delta\right\\}\leq\left\\{\mu(\mathtt{x}^{\mathtt{q}})\right\\}$,
that is
$(\mu,\mu^{\mathtt{pq}}+\delta)\models\mathtt{x}^{\mathtt{pq}}\leq\mathtt{x}^{\mathtt{q}}$,
as required.

###  A.6. Missing proofs for Sec. 3

######  Proof A.6 (Proof of the “if” direction of Theorem 1).

Let $\mathcal{S}$ be a tca over a polyforest topology, where in each polytree
there is at most one channel with integral inequality tests. By Lemma 5 the
standard semantics $\left\ldbrack\mathcal{S}\right\rdbrack$ is equivalent to
the desynchronised one $\left\ldbrack\mathcal{S}\right\rdbrack^{\textsf{de}}$,
which in turn is equivalent to the rendezvous one
$\left\ldbrack\mathcal{S}\right\rdbrack^{\textsf{rv}}$ by Lemma 6. By the
transformations of Sec. 4 we an assume that the tca is simple. This allows us
to apply the construction of this section in order to build a rac
$\left\ldbrack\mathcal{R}\right\rdbrack$ s.t. the rendezvous semantics
$\left\ldbrack\mathcal{S}\right\rdbrack^{\textsf{rv}}$ is equivalent to
$\left\ldbrack\mathcal{R}\right\rdbrack$ by Lemma 8. Suppose the topology
$\mathcal{T}$ decomposes into $n$ disjoint polytrees
$\mathcal{T}_{1},\dots,\mathcal{T}_{n}$, where by assumption in each of the
$\mathcal{T}_{i}$’s there is at most one channel with integral inequality
tests. We obtain a rac $\mathcal{R}$ with counters of which $n$ have threshold
tests, and thus unless $n=1$ we cannot apply immediately Theorem 7 to obtain
decidability of the non-emptiness problem. With a small modification of the
construction of $\mathcal{R}$ instead of simulating all polytrees
$\mathcal{T}_{1},\dots,\mathcal{T}_{n}$ in parallel, we can simulate them
sequentially by running $\mathcal{T}_{1}$ first, followed by
$\mathcal{T}_{2}$, …, till $\mathcal{T}_{n}$ (cf. [19, Theorem 3]). In order
for the sequential simulation to be faithful, we need to ensure that the same
total amount of time elapses when simulating any of the $\mathcal{T}_{i}$’s.
For the integral part of the elapsed time, we can add an extra counter
$\mathtt{n}_{\mathcal{T}_{i}}$ for each component which is increased by one
every time some fixed process $\mathtt{p}$ therein elapses 1 time unit; at the
end of all simulations, we additionally check that
$\mathtt{n}_{\mathcal{T}_{1}}=\cdots=\mathtt{n}_{\mathcal{T}_{n}}$ by
decreasing all such counters by $1$ until they all hit $0$. (Notice that at
the end of the simulation of $\mathcal{T}_{i}$ all processes therein elapse
the same amount of time since we require all counters
$\mathtt{n}^{\mathtt{pq}}$ to be $0$ at the end of the run.) For the
fractional part of the elapsed time no additional check is needed, since
reference registers $\hat{\mathtt{x}}^{\mathtt{p}}_{0}=0$ at the end of the
run by construction. In this way it suffices to have only one counter with
threshold tests which is reused in the subsequent simulations, and we obtain
decidability by Theorem 7.