*Programming, 18th International Colloquium, ICALP91, Madrid, Spain, July 8-12, 1991, Proceedings*, volume 510 of Lecture Notes in Computer Science, pages 217-228. Springer, 1991.
doi:10.1007/3-540-54233-7_136.

[ZFH01] Armin Zimmermann, Jörn Freiheit, and Günter Hommel. Discrete time stochastic Petri nets for the modeling and evaluation of real-time systems. In *Proceedings of the 15th International Parallel & Distributed Processing Symposium (IPDPS-01)*, page 100. IEEE Computer Society, 2001. doi:10.1109/IPDPS.2001.925065.

## APPENDIX A. BACKGROUND: CCS, CCSK AND TPL

In this section we present the full syntax and semantics of CCS, TPL and CCSK, taken respectively from [Mil80], [HR95] and [PU07].

### A.1. CCS: Calculus of Communicating Systems.
The Calculus of Communicating Systems is a process calculus introduced by Milner [Mil80]. We let $\mathcal{A}$ be the set of action names $a, \bar{\mathcal{A}}$ the set of action conames $\bar{a}$. We use $\alpha$ to range over $a, \bar{a}$ and internal actions $\tau$. We assume $\bar{\alpha} = a$. We let $\mathcal{A}^{\tau} = \mathcal{A} \cup \bar{\mathcal{A}} \cup \{\tau\}$. The syntax of CCS is reported in Figure 5. A process can be an action *prefix* $\alpha.P$, that can perform an action $\alpha$ and continue as $P$, a non-deterministic *choice* $P + Q$ among two processes, a *parallel* composition $P \parallel Q$ of two processes, the *restriction* $P \setminus a$, which acts as the process $P$, but actions on $a$ are forbidden, the constant *identifier* $\mathcal{A}$ and the *inactive* process 0. The semantics of CCS is given by the labelled transition system (LTS) $(\mathcal{P}, \mathcal{A}^{\tau}, \to_t)$, where $\mathcal{P}$ is the set of all CCS processes, $\mathcal{A}^{\tau}$ is the set of labels and $\to_t$ is the least transition relation induced by the rules in Figure 6.

### A.2. CCSK: CCS with communication keys.
CCS with communication keys (CCSK) is a reversible extension of CCS obtained by applying to CCS the approach in [PU07]. The key idea of this approach is to make all the dynamic operators (such as prefix and non-deterministic choice) static and to decorate prefixes with freshly created identifiers, dubbed communication keys, when they are executed. The syntax of CCSK is reported in Figure 7, where the addition with respect to the syntax of CCS (Figure 5) is enclosed in grey boxes. With respect to CCS, in CCSK a prefix $\alpha$ can be decorated with a communication key $i$, to indicate the fact that the prefix has been executed. As one can see, CCSK (reversible) configurations are built on top of CCS processes.

The semantics of CCSK is given by two LTSs, the *forward* one $(\mathcal{X}^k, \mathcal{A}^\tau \times \mathcal{K}, \to_k)$ and the *backward* one $(\mathcal{X}^k, \mathcal{A}^\tau \times \mathcal{K}, \leftarrow_k)$, where $\mathcal{X}^k$ is the set of CCSK configurations, $\mathcal{K}$ is the set of keys and $\to_k$ and $\leftarrow_k$ are the least transition relations induced by the rules in Figure 8 and Figure 9, respectively. Since CCSK is reversible, for each forward rule there exists a corresponding backward one. The two LTSs use two functions, `std(X)` and `keys(X)`. Intuitively, function `std(X)` states that a configuration X has no decorated prefixes (i.e., it does not contain any history information hence it is a CCS process), while function `keys(X)` returns the set of keys of a given configuration.
*Programming, 18th International Colloquium, ICALP91, Madrid, Spain, July 8-12, 1991, Proceedings*, volume 510 of *Lecture Notes in Computer Science*, pages 217-228. Springer, 1991.
doi:10.1007/3-540-54233-7_136.

[ZFH01] Armin Zimmermann, Jörn Freiheit, and Günter Hommel. Discrete time stochastic Petri nets for the modeling and evaluation of real-time systems. In *Proceedings of the 15th International Parallel & Distributed Processing Symposium (IPDPS-01)*, page 100. IEEE Computer Society, 2001. doi:10.1109/IPDPS.2001.925065.

## APPENDIX A. BACKGROUND: CCS, CCSK AND TPL

In this section we present the full syntax and semantics of CCS, TPL and CCSK, taken respectively from [Mil80], [HR95] and [PU07].

### A.1. CCS: Calculus of Communicating Systems.
The Calculus of Communicating Systems is a process calculus introduced by Milner [Mil80]. We let $\mathcal{A}$ be the set of action names $a, \bar{\mathcal{A}}$ the set of action conames $\bar{a}$. We use $\alpha$ to range over $a, \bar{a}$ and internal actions $\tau$. We assume $\bar{\alpha} = a$. We let $\mathcal{A}^{\tau} = \mathcal{A} \cup \bar{\mathcal{A}} \cup \{\tau\}$. The syntax of CCS is reported in Figure 5. A process can be an action *prefix* $\alpha.P$, that can perform an action $\alpha$ and continue as $P$, a non-deterministic *choice* $P + Q$ among two processes, a *parallel* composition $P \parallel Q$ of two processes, the *restriction* $P \setminus a$, which acts as the process $P$, but actions on $a$ are forbidden, the constant *identifier* $\mathcal{A}$ and the *inactive* process 0. The semantics of CCS is given by the labelled transition system (LTS) $(\mathcal{P}, \mathcal{A}^{\tau}, \to_t)$, where $\mathcal{P}$ is the set of all CCS processes, $\mathcal{A}^{\tau}$ is the set of labels and $\to_t$ is the least transition relation induced by the rules in Figure 6.

### A.2. CCSK: CCS with communication keys.
CCS with communication keys (CCSK) is a reversible extension of CCS obtained by applying to CCS the approach in [PU07]. The key idea of this approach is to make all the dynamic operators (such as prefix and non-deterministic choice) static and to decorate prefixes with freshly created identifiers, dubbed communication keys, when they are executed. The syntax of CCSK is reported in Figure 7, where the addition with respect to the syntax of CCS (Figure 5) is enclosed in grey boxes. With respect to CCS, in CCSK a prefix $\alpha$ can be decorated with a communication key $i$, to indicate the fact that the prefix has been executed. As one can see, CCSK (reversible) configurations are built on top of CCS processes.

The semantics of CCSK is given by two LTSs, the *forward* one $(\mathcal{X}^k, \mathcal{A}^\tau \times \mathcal{K}, \to_k)$ and the *backward* one $(\mathcal{X}^k, \mathcal{A}^\tau \times \mathcal{K}, \leftarrow_k)$, where $\mathcal{X}^k$ is the set of CCSK configurations, $\mathcal{K}$ is the set of keys and $\to_k$ and $\leftarrow_k$ are the least transition relations induced by the rules in Figure 8 and Figure 9, respectively. Since CCSK is reversible, for each forward rule there exists a corresponding backward one. The two LTSs use two functions, `std(X)` and `keys(X)`. Intuitively, function `std(X)` states that a configuration X has no decorated prefixes (i.e., it does not contain any history information hence it is a CCS process), while function `keys(X)` returns the set of keys of a given configuration.
$$ (\text{Processes}) \quad P = \alpha.P \mid P+Q \mid P \parallel Q \mid P \setminus a \mid A \mid \mathbf{0} $$

<caption>Figure 5: Syntax of CCS</caption>

$$ \begin{array}{l @{\quad} l @{\quad} l @{\quad} l @{\quad} l @{\quad} l} \text{(ACT)} & \alpha.P \xrightarrow{\alpha} {}_t P & \text{(SUM}_1\text{)} & \displaystyle \frac{P \xrightarrow{\alpha} {}_t P'}{P+Q \xrightarrow{\alpha} {}_t P'+Q} & \text{(SUM}_2\text{)} & \displaystyle \frac{Q \xrightarrow{\alpha} {}_t Q'}{P+Q \xrightarrow{\alpha} {}_t P+Q'} \\[1.5ex] \text{(COM}_1\text{)} & \displaystyle \frac{P \xrightarrow{\alpha} {}_t P'}{P \parallel Q \xrightarrow{\alpha} {}_t P' \parallel Q} & \text{(COM}_2\text{)} & \displaystyle \frac{Q \xrightarrow{\alpha} {}_t Q'}{P \parallel Q \xrightarrow{\alpha} {}_t P \parallel Q'} & \text{(COM}_3\text{)} & \displaystyle \frac{P \xrightarrow{\alpha} {}_t P'}{P \parallel Q \xrightarrow{\tau} {}_t P' \parallel Q'} \\[1.5ex] \text{(RES)} & \displaystyle \frac{P \xrightarrow{\alpha} {}_t P'}{P \setminus a \xrightarrow{\tau} {}_t P' \setminus a} & \text{(REC)} & \displaystyle \frac{A \stackrel{\text{def}}{=} P}{A \xrightarrow{\alpha} {}_t P'} & \displaystyle \frac{P \xrightarrow{\alpha} {}_t P'}{A \xrightarrow{\alpha} {}_t P'} \end{array} $$

<caption>Figure 6: Semantics of CCS</caption>

$$ \begin{array}{l @{\quad} l @{\quad} l @{\quad} l @{\quad} l @{\quad} l} \text{(Processes)} & P = \alpha.P \mid P+Q \mid P \parallel Q \mid P \setminus a \mid A \mid \mathbf{0} & & & & \\[1.5ex] \text{(Configurations)} & X = \boxed{\alpha[i].X} \mid X+Y \mid X \parallel Y \mid X \setminus a \mid P & & & & \end{array} $$

<caption>Figure 7: Syntax of CCSK</caption>

### A.3. TPL: Timed Process Language.
TPL [HR95] is an extension of CCS with time. Its syntax is reported in Figure 10, where the novelties w.r.t. CCS are enclosed in grey boxes. TPL adds to CCS two constructs to deal with time: the idling prefix $\sigma.P$ and the timeout operator $\lceil P \rceil(Q)$. The process $\sigma.P$ acts as $P$ after having waited one time unit, while the timeout $\lceil P \rceil(Q)$ executes $P$ (if possible) or $Q$ (in case of a timeout). We indicate with $A^t$ the set $A \cup \bar{A} \cup \{\tau, \sigma\}$. The semantics of TPL is given via an LTS and two set of rules: rules for actions (Figure 11, similar to the CCS rules with the addition of rule THEN), and rules for time (Figure 12), which regulate the behaviour of the temporal operators $\sigma.P$ and $\lceil P \rceil(Q)$ and the passage of time in the system (e.g., in a parallel composition). Hence, the semantics of TPL is given by the LTS $(\mathcal{P}^t, A^t, \to_t)$, where $\mathcal{P}^t$ is the set of TPL processes and $\to_t$ is the least relation induced by the rules in Figures 11 and 12.

## APPENDIX B. ENCODING OF NEGATIVE PREMISES

In this section we show that there exists an encoding of the negative premises in the rules of Figure 2 and Figure 3 into decidable positive premises. To do so we compute all the enabled forward prefixes (i.e., barbs) of a configuration and form all the possible pairs of prefixes on the two sides of a parallel operator. We then check whether there exists a pair containing both an action and the corresponding co-action. The operator $\gamma$ is inductively defined as follows:
$$ (\text{Processes}) \quad P = \alpha.P \mid P+Q \mid P \parallel Q \mid P \setminus a \mid A \mid \mathbf{0} $$

<caption>Figure 5: Syntax of CCS</caption>

$$ \begin{array}{l @{\quad} l @{\quad} l @{\quad} l @{\quad} l @{\quad} l} \text{(ACT)} & \alpha.P \xrightarrow{\alpha} {}_t P & \text{(SUM}_1\text{)} & \displaystyle\frac{P \xrightarrow{\alpha} {}_t P'}{P+Q \xrightarrow{\alpha} {}_t P'+Q} & \text{(SUM}_2\text{)} & \displaystyle\frac{Q \xrightarrow{\alpha} {}_t Q'}{P+Q \xrightarrow{\alpha} {}_t P+Q'} \\[1.5em] \text{(COM}_1\text{)} & \displaystyle\frac{P \xrightarrow{\alpha} {}_t P'}{P \parallel Q \xrightarrow{\alpha} {}_t P' \parallel Q} & \text{(COM}_2\text{)} & \displaystyle\frac{Q \xrightarrow{\alpha} {}_t Q'}{P \parallel Q \xrightarrow{\alpha} {}_t P \parallel Q'} & \text{(COM}_3\text{)} & \displaystyle\frac{P \xrightarrow{\alpha} {}_t P'}{P \parallel Q \xrightarrow{\tau} {}_t P' \parallel Q'} \\[1.5em] \text{(RES)} & \displaystyle\frac{P \xrightarrow{\alpha} {}_t P'}{P \setminus a \xrightarrow{\tau} {}_t P' \setminus a} & \text{(REC)} & \displaystyle\frac{A \stackrel{\text{def}}{=} P}{A \xrightarrow{\alpha} {}_t P'} & & \\[1.5em] \end{array} $$

<caption>Figure 6: Semantics of CCS</caption>

$$ \begin{array}{l @{\quad} l @{\quad} l @{\quad} l @{\quad} l @{\quad} l} \text{(Processes)} & P = \alpha.P \mid P+Q \mid P \parallel Q \mid P \setminus a \mid A \mid \mathbf{0} & & & & \\[1.5em] \text{(Configurations)} & X = \boxed{\alpha[i].X} \mid X+Y \mid X \parallel Y \mid X \setminus a \mid P & & & & \\[1.5em] \end{array} $$

<caption>Figure 7: Syntax of CCSK</caption>

### A.3. TPL: Timed Process Language.
TPL [HR95] is an extension of CCS with time. Its syntax is reported in Figure 10, where the novelties w.r.t. CCS are enclosed in grey boxes. TPL adds to CCS two constructs to deal with time: the idling prefix $\sigma.P$ and the timeout operator $\lfloor P \rfloor(Q)$. The process $\sigma.P$ acts as $P$ after having waited one time unit, while the timeout $\lfloor P \rfloor(Q)$ executes $P$ (if possible) or $Q$ (in case of a timeout). We indicate with $A^t$ the set $A \cup \bar{A} \cup \{\tau, \sigma\}$. The semantics of TPL is given via an LTS and two set of rules: rules for actions (Figure 11, similar to the CCS rules with the addition of rule THEN), and rules for time (Figure 12), which regulate the behaviour of the temporal operators $\sigma.P$ and $\lfloor P \rfloor(Q)$ and the passage of time in the system (e.g., in a parallel composition). Hence, the semantics of TPL is given by the LTS $(\mathcal{P}^t, A^t, \to_t)$, where $\mathcal{P}^t$ is the set of TPL processes and $\to_t$ is the least relation induced by the rules in Figures 11 and 12.

## APPENDIX B. ENCODING OF NEGATIVE PREMISES

In this section we show that there exists an encoding of the negative premises in the rules of Figure 2 and Figure 3 into decidable positive premises. To do so we compute all the enabled forward prefixes (i.e., barbs) of a configuration and form all the possible pairs of prefixes on the two sides of a parallel operator. We then check whether there exists a pair containing both an action and the corresponding co-action. The operator $\gamma$ is inductively defined as follows:
<figure><img src="image_13.png" /><figcaption>Figure 8: Forward LTS of CCSK</figcaption></figure>

**Definition B.1 (Synchronisation Operator).**

$$
\begin{align*}
\gamma(\alpha.P) &= \{\{\alpha\}\} & \gamma(\rho[i].X) &= \gamma(X) \\
\gamma(X \parallel Y) &= \gamma(X) \oplus \gamma(Y) & \gamma(X \setminus a) &= \gamma(X) \setminus \{a\} \\
\gamma(X + Y) &= \gamma(X) \cup \gamma(Y) & \gamma(X + Y) &= \gamma(X) \cup \gamma(Y) \\
\gamma(X + Y) &= \gamma(X) & \gamma(X + Y) &= \gamma(Y) \\
\gamma(\lfloor X \rfloor(Y)) &= \gamma(X) & \gamma(\lfloor X \rfloor_{\leftarrow i}(Y)) &= \gamma(X) \\
\gamma(\lfloor X \rfloor_{\leftarrow i}(Y)) &= \gamma(Y) & \gamma(A) &= \gamma(P) \text{ if } A \stackrel{def}{=} P \\
\gamma(\mathbf{0}) &= \emptyset & \gamma(\sigma.P) &= \emptyset
\end{align*}
$$

where $A \oplus B$ is defined as follows:

$$
\{A_i \mid i \in I\} \oplus \{B_j \mid j \in J\} = \bigcup_{i \in I, j \in J} \{A_i \cup B_j\}
$$

We can then define $X \xrightarrow{\mathcal{F}}$ as:

$$
X \xrightarrow{\mathcal{F}} = \forall C \in \gamma(X). \forall c_i, c_j \in C. \overline{c_i} \neq c_j
$$

The intuition behind the $\gamma(\cdot)$ operator is that for sequential processes (i.e., processes which have no top level $\parallel$) it computes a set of singletons of prefixes. Such a set represents the list of all the enabled forward prefixes, which could synchronise in a parallel composition. This is rendered by the rule $\gamma(X \parallel Y) = \gamma(X) \oplus \gamma(Y)$. In this case, via the operator $\oplus$, we compute all the possible pairs of such singletons. Let us note that if we have more than one
<figure><img src="image_13.png" /><figcaption>Figure 8: Forward LTS of CCSK</figcaption></figure>

**Definition B.1 (Synchronisation Operator).**

$$
\begin{align*}
\gamma(\alpha.P) &= \{\{\alpha\}\} & \gamma(\rho[i].X) &= \gamma(X) \\
\gamma(X \parallel Y) &= \gamma(X) \oplus \gamma(Y) & \gamma(X \setminus a) &= \gamma(X) \setminus \{a\} \\
\gamma(X + Y) &= \gamma(X) \cup \gamma(Y) & \gamma(X + Y) &= \gamma(X) \cup \gamma(Y) \\
\gamma(X + Y) &= \gamma(X) & \gamma(X + Y) &= \gamma(Y) \\
\gamma(\lfloor X \rfloor(Y)) &= \gamma(X) & \gamma(\lfloor X \rfloor_{\leftarrow i}(Y)) &= \gamma(X) \\
\gamma(\lfloor X \rfloor_{\leftarrow i}(Y)) &= \gamma(Y) & \gamma(A) &= \gamma(P) \text{ if } A \stackrel{def}{=} P \\
\gamma(\mathbf{0}) &= \emptyset & \gamma(\sigma.P) &= \emptyset
\end{align*}
$$

where $A \oplus B$ is defined as follows:

$$
\{A_i \mid i \in I\} \oplus \{B_j \mid j \in J\} = \bigcup_{i \in I, j \in J} \{A_i \cup B_j\}
$$

We can then define $X \xrightarrow{\mathcal{F}}$ as:

$$
X \xrightarrow{\mathcal{F}} = \forall C \in \gamma(X). \forall c_i, c_j \in C. \overline{c_i} \neq c_j
$$

The intuition behind the $\gamma(\cdot)$ operator is that for sequential processes (i.e., processes which have no top level $\parallel$) it computes a set of singletons of prefixes. Such a set represents the list of all the enabled forward prefixes, which could synchronise in a parallel composition. This is rendered by the rule $\gamma(X \parallel Y) = \gamma(X) \oplus \gamma(Y)$. In this case, via the operator $\oplus$, we compute all the possible pairs of such singletons. Let us note that if we have more than one
<figure><img src="image_14.png" /><figcaption>Figure 9: Backward LTS of CCSK</figcaption></figure>

$$ (\text{Processes}) \quad P = \pi.P \mid \lfloor P \rfloor(Q) \mid P+Q \mid P \parallel Q \mid P \setminus a \mid A \mid \mathbf{0} \quad (\pi = \alpha \mid \sigma) $$

<caption>Figure 10: Syntax of TPL</caption>

top level $\parallel$, say $n$, we will have a set of $(n+1)$-uples. Also, since we are using set-based operators, repetitions of prefixes will be dropped.

The $\gamma$ operator just collects all the available prefixes, discarding the ones already executed, and the discarded branches. For example, let us consider the process $P = a + \bar{a}$ we have that $\gamma(P) = \{\{a\}, \{\bar{a}\}\}$. Synchronisation is induced by the parallel operator $\parallel$, hence when the $\gamma$ operator meets a parallel composition, it computes all the possible pairs via the $\oplus$ operator. We then have a possible synchronisation if there is a pair of the form $\{\alpha, \bar{\alpha}\}$. For example, if we take the process $P$ above and we put it in parallel with $a$, the synchronisation operator will compute the following pairs

$$ \gamma((a + \bar{a}) \parallel a) = \gamma(a + \bar{a}) \oplus \gamma(a) = \{\{a\}, \{\bar{a}\}\} \oplus \{\{a\}\} = \{\{a, \bar{a}\}, \{a, a\}\} $$

We can see that there exists one synchronisation pair. Furthermore, if we consider the process $(b + \bar{a}) \parallel a \parallel \bar{b}$ we have:

$$ \begin{aligned} \gamma((b + \bar{a}) \parallel a \parallel \bar{b}) = & \gamma(b + \bar{a}) \oplus \gamma(a) \oplus \gamma(\bar{b}) = \{\{b\}, \{\bar{a}\}\} \oplus \{\{a\}\} \oplus \{\{\bar{b}\}\} = \\ & \{\{b, a\}, \{\bar{a}, a\}\} \oplus \{\{\bar{b}\}\} = \{\{b, a, \bar{b}\}, \{\bar{a}, a, \bar{b}\}\} \end{aligned} $$

where there are two synchronisation pairs.

**Lemma B.2.** Given a reachable revTPL configuration $X$, then $X \not\to \bar{X}$ is decidable.
<figure><img src="image_14.png" /><figcaption>Figure 9: Backward LTS of CCSK</figcaption></figure>

$$ (\text{Processes}) \quad P = \pi.P \mid \lfloor P \rfloor(Q) \mid P+Q \mid P \parallel Q \mid P \backslash a \mid A \mid \mathbf{0} \quad (\pi = \alpha \mid \sigma) $$

<caption>Figure 10: Syntax of TPL</caption>

top level $\parallel$, say $n$, we will have a set of $(n+1)$-uples. Also, since we are using set-based operators, repetitions of prefixes will be dropped.

The $\gamma$ operator just collects all the available prefixes, discarding the ones already executed, and the discarded branches. For example, let us consider the process $P = a + \bar{a}$ we have that $\gamma(P) = \{\{a\}, \{\bar{a}\}\}$. Synchronisation is induced by the parallel operator $\parallel$, hence when the $\gamma$ operator meets a parallel composition, it computes all the possible pairs via the $\oplus$ operator. We then have a possible synchronisation if there is a pair of the form $\{\alpha, \bar{\alpha}\}$. For example, if we take the process $P$ above and we put it in parallel with $a$, the synchronisation operator will compute the following pairs

$$ \gamma((a + \bar{a}) \parallel a) = \gamma(a + \bar{a}) \oplus \gamma(a) = \{\{a\}, \{\bar{a}\}\} \oplus \{\{a\}\} = \{\{a, \bar{a}\}, \{a, a\}\} $$

We can see that there exists one synchronisation pair. Furthermore, if we consider the process $(b + \bar{a}) \parallel a \parallel \bar{b}$ we have:

$$ \begin{aligned} \gamma((b + \bar{a}) \parallel a \parallel \bar{b}) = & \gamma(b + \bar{a}) \oplus \gamma(a) \oplus \gamma(\bar{b}) = \{\{b\}, \{\bar{a}\}\} \oplus \{\{a\}\} \oplus \{\{\bar{b}\}\} = \\ & \{\{b, a\}, \{\bar{a}, a\}\} \oplus \{\{\bar{b}\}\} = \{\{b, a, \bar{b}\}, \{\bar{a}, a, \bar{b}\}\} \end{aligned} $$

where there are two synchronisation pairs.

**Lemma B.2.** Given a reachable revTPL configuration $X$, then $X \not\to \bar{X}$ is decidable.
<figure><img src="image_15.png" /><figcaption>Figure 11: LTS of TPL: rules for actions</figcaption></figure>

<figure><img src="image_16.png" /><figcaption>Figure 12: LTS of TPL: rules for time</figcaption></figure>

*Proof.* By a simple induction on the structure of X. □

## APPENDIX C. ADDITIONAL PROOFS OF SECTION 4

**Property 4.11 (Square Property - SP).** Given a reachable revTPL configuration X and two coininitial transitions $t: X \xrightarrow{\pi_1[i]} Y$ and $s: X \xrightarrow{\pi_2[j]} Z$ with $t \in \mathcal{I}s$ there exist two cofinal transitions $t': Y \xrightarrow{\pi_2[j]} W$ and $s': Z \xrightarrow{\pi_1[i]} W$.

*Proof.* The proof is by case analysis on the direction of the two transitions. We distinguish three cases according to whether the two transitions are both forwards, both backwards, or one forwards and the other backwards.

**t and s forwards:** first we look at the case where the two actions are both communication actions. The proof is by induction on the structure of the common source configuration X. From **0** no transition is possible hence this case can never happen. For a standard
<figure><img src="image_15.png" /><figcaption>Figure 11: LTS of TPL: rules for actions</figcaption></figure>

<figure><img src="image_16.png" /><figcaption>Figure 12: LTS of TPL: rules for time</figcaption></figure>

*Proof.* By a simple induction on the structure of X.

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

## APPENDIX C. ADDITIONAL PROOFS OF SECTION 4

**Property 4.11 (Square Property - SP).** Given a reachable revTPL configuration X and two coininitial transitions $t: X \xrightarrow{\pi_1[i]} Y$ and $s: X \xrightarrow{\pi_2[j]} Z$ with $t \in \mathcal{I}s$ there exist two cofinal transitions $t': Y \xrightarrow{\pi_2[j]} W$ and $s': Z \xrightarrow{\pi_1[i]} W$.

*Proof.* The proof is by case analysis on the direction of the two transitions. We distinguish three cases according to whether the two transitions are both forwards, both backwards, or one forwards and the other backwards.

**t and s forwards:** first we look at the case where the two actions are both communication actions. The proof is by induction on the structure of the common source configuration X. From **0** no transition is possible hence this case can never happen. For a standard
prefix, a single transition is possible, but for the choice of the key. Two transitions with
the same key are not independent due to condition 4 in Definition 4.9, hence there is
nothing to prove. The cases of non-standard prefixes, timeout (both standard and non
standard), hiding and constants follow by inductive hypothesis. If the configuration
is a parallel composition then either we apply rule [PAR] and its symmetric, or we
apply rule [PAR] and rule [SYN], or two [SYN]. In the case of two applications of rule
[PAR], if the same parallel component acts in both the cases, then the thesis follows
from inductive hypothesis. Otherwise we have $X = X_1 \parallel X_2 \xrightarrow{\alpha_1[i]} Y_1 \parallel X_2 = Y$
and $X_1 \parallel X_2 \xrightarrow{\alpha_2[j]} X_1 \parallel Z_2 = Z$ with premises $X_1 \xrightarrow{\alpha_1[i]} Y_1$ and $X_2 \xrightarrow{\alpha_2[j]} Z_2$
(note that $i \neq j$ by case 4 of Definition 4.9). By applying rule [PAR] again we have
$Y = Y_1 \parallel X_2 \xrightarrow{\alpha_2[j]} Y_1 \parallel Z_2$ and $Z = X_1 \parallel Z_1 \xrightarrow{\alpha_1[i]} Y_1 \parallel Z_2$, as desired. In the case of
two applications of rule [SYN] we proceed by induction on the two components. In the
case of one [PAR] and one [SYN] we proceed by induction on the component which
acts in [PAR].

In the case of choice, if the two transitions concern the same component then
the thesis follows by inductive hypothesis. If the two transitions concern different
components then they are not independent as they are in forward communication
conflict, according to condition 2 in Definition 4.9.

In the case $\pi_1 = \sigma$ and $\pi_2 = \sigma$ there is nothing to prove since then $Y = Z$ and $t = s$
by time determinism.

Finally, note that the case $\pi_1 = \alpha$ and $\pi_2 = \sigma$ is ruled out by Definition 4.9 (first
clause).

**t and s backwards:** the case of two communication actions is similar to the previous
one, noticing however that backward transitions are never in conflict according to
Definition 4.9. Indeed, keys ensure that each component can take part in a single
transition.

The case of two $\sigma$ actions follows since time determinism holds also in the backward
direction, since time actions are required on all components, and they need to have
the same key.

The case of a $\sigma$ action and a communication action follows from Proposition 4.10.

**t forwards and s backwards:** the case of communication actions is similar to the previous
one: actions either are in conflict by condition 3 of Definition 4.9 or they are generated
by parallel components, hence can take place also in the opposite order. Two time
transitions from the same configuration are always in conflict by condition 3 of
Definition 4.9, since time actions are recorded in each component. The case $\pi_1 = \alpha$
and $\pi_2 = \sigma$ (or vice versa) is analogous to the previous one. $\square$
prefix, a single transition is possible, but for the choice of the key. Two transitions with the same key are not independent due to condition 4 in Definition 4.9, hence there is nothing to prove. The cases of non-standard prefixes, timeout (both standard and non standard), hiding and constants follow by inductive hypothesis. If the configuration is a parallel composition then either we apply rule [PAR] and its symmetric, or we apply rule [PAR] and rule [SYN], or two [SYN]. In the case of two applications of rule [PAR], if the same parallel component acts in both the cases, then the thesis follows from inductive hypothesis. Otherwise we have $X = X_1 \parallel X_2 \xrightarrow{\alpha_1[i]} Y_1 \parallel X_2 = Y$ and $X_1 \parallel X_2 \xrightarrow{\alpha_2[j]} X_1 \parallel Z_2 = Z$ with premises $X_1 \xrightarrow{\alpha_1[i]} Y_1$ and $X_2 \xrightarrow{\alpha_2[j]} Z_2$ (note that $i \neq j$ by case 4 of Definition 4.9). By applying rule [PAR] again we have $Y = Y_1 \parallel X_2 \xrightarrow{\alpha_2[j]} Y_1 \parallel Z_2$ and $Z = X_1 \parallel Z_1 \xrightarrow{\alpha_1[i]} Y_1 \parallel Z_2$, as desired. In the case of two applications of rule [SYN] we proceed by induction on the two components. In the case of one [PAR] and one [SYN] we proceed by induction on the component which acts in [PAR].

In the case of choice, if the two transitions concern the same component then the thesis follows by inductive hypothesis. If the two transitions concern different components then they are not independent as they are in forward communication conflict, according to condition 2 in Definition 4.9.

In the case $\pi_1 = \sigma$ and $\pi_2 = \sigma$ there is nothing to prove since then $Y = Z$ and $t = s$ by time determinism.

Finally, note that the case $\pi_1 = \alpha$ and $\pi_2 = \sigma$ is ruled out by Definition 4.9 (first clause).

**t and s backwards:** the case of two communication actions is similar to the previous one, noticing however that backward transitions are never in conflict according to Definition 4.9. Indeed, keys ensure that each component can take part in a single transition.

The case of two $\sigma$ actions follows since time determinism holds also in the backward direction, since time actions are required on all components, and they need to have the same key.

The case of a $\sigma$ action and a communication action follows from Proposition 4.10.

**t forwards and s backwards:** the case of communication actions is similar to the previous one: actions either are in conflict by condition 3 of Definition 4.9 or they are generated by parallel components, hence can take place also in the opposite order. Two time transitions from the same configuration are always in conflict by condition 3 of Definition 4.9, since time actions are recorded in each component. The case $\pi_1 = \alpha$ and $\pi_2 = \sigma$ (or vice versa) is analogous to the previous one. $\square$