*This paper is a revised and extended version of [BLMY22].

[a] [b] [c] [d]

#  $\mathtt{revTPL}$: The Reversible Temporal Process Language*

Laura Bocchi0000-0002-7177-9395  ,  Ivan Lanese0000-0003-2527-9995  ,  Claudio
Antares Mezzina0000-0003-1556-2623  and  Shoji Yuen0000-0003-2642-0647  School
of Computing, University of Kent, UK<EMAIL_ADDRESS>Focus Team,
University of Bologna/INRIA, Italy<EMAIL_ADDRESS>Dipartimento di
Scienze Pure e Applicate, Università di Urbino, Italy
<EMAIL_ADDRESS>Graduate School of Informatics, Nagoya University,
Japan<EMAIL_ADDRESS>
###### Abstract.

Reversible debuggers help programmers to find the causes of misbehaviours in
concurrent programs more quickly, by executing a program backwards from the
point where a misbehaviour was observed, and looking for the bug(s) that
caused it. Reversible debuggers can be founded on the well-studied theory of
causal-consistent reversibility, which only allows one to undo an action
provided that its consequences, if any, are undone beforehand. Causal-
consistent reversibility yields more efficient debugging by reducing the
number of states to be explored when looking backwards. Till now, causal-
consistent reversibility has never considered time, which is a key aspect in
real-world applications. Here, we study the interplay between reversibility
and time in concurrent systems via a process algebra. The Temporal Process
Language (TPL) by Hennessy and Regan is a well-understood extension of CCS
with discrete-time and a timeout operator. We define $\mathtt{revTPL}$, a
reversible extension of TPL, and we show that it satisfies the properties
expected from a causal-consistent reversible calculus. We show that,
alternatively, $\mathtt{revTPL}$ can be interpreted as an extension of
reversible CCS with time.

###### Key words and phrases:

Reversible computing; timed systems; process calculi; operational semantics

This work has been partially supported by the BehAPI project funded by the EU
H2020 RISE under the Marie Sklodowska-Curie action (No: 778233), by EPSRC
project EP/T014512/1 (STARDUST), by MIUR PRIN project NiRvAna, by French ANR
project DCore ANR-18-CE25-0007, by INdAM – GNCS 2022 project _Proprietà
qualitative e quantitative di sistemi reversibili_ and GNCS 2023 project
_Reversibilità In SIstemi COncorrenti: analisi quantitative e funzionali
(RISICO)_ , code CUP_E53C22001930001, and by JSPS KAKENHI Grant Number
JP21H03415. We thank the anonymous referees of this paper and of its
conference version for their helpful comments and suggestions.

## Introduction

Recent studies [Viz20, BJCC13] show that reversible debuggers ease the
debugging phase, and help programmers to quickly find the causes of a
misbehaviour. Reversible debuggers can be built on top of a causal-consistent
reversible semantics [GLM14, LNPV18, FLS21, LLS+22], and this approach is
particularly suited to deal with concurrency bugs, which are hard to find
using traditional debuggers [Gra86]. By exploiting causality information,
causal-consistent reversible debuggers allow one to undo just the steps which
led (that is, are causally related) to a visible misbehaviour, reducing the
number of steps/spurious causes and helping to understand the root cause of
the misbehaviour. More precisely, one can explore backwards the tree of causes
of a visible misbehaviour, possibly spread among different processes, looking
for the bug(s) causing it. In the last years several reversible semantics for
concurrency have been developped, see, e.g., [DK04, PU07, CKV13, LMS16, MMU19,
GLMT17, LM20, BM20, MMPY20, MMP21a]. However, none of them takes into account
time111The notion of time reversibility addressed in [BM20] is not aimed at
studying programming languages with constructs to support hard or soft time
constraints, but at performance evaluation via (time-reversible) Markov
chains.. Time-dependent behaviour is an intrinsic and important feature of
real-world concurrent systems and has many applications: from the engineering
of highways [MP20], to the manufacturing schedule [GZT20] and to the
scheduling problem for real-time operating systems [Ber05].

Time is instrumental for the functioning of embedded systems where some events
are triggered by the system clock. Embedded systems are used for both real-
time and soft real-time applications, frequently in safety-critical scenarios.
Hence, before being deployed or massively produced, they have to be heavily
tested, and hence possibly debugged. Actually, debugging occurs not only upon
testing, but in almost all the stages of the life-cycle of a software system:
from the early stages of prototyping to the post-release maintenance (e.g.,
updates or security patches). Concurrency is important in embedded systems
[FGP12], and concurrency bugs frequently happen in these systems as well
[Koo10]. To debug such systems, and deal with time-dependent bugs in
particular, it is crucial that debuggers can handle both concurrency and time.

In this paper, we study the interplay between time and reversibility in a
process algebra for concurrency. In the literature, there exists a variety of
timed process algebras for the analysis and specification of concurrent timed
systems [NS91]. We build on the Temporal Process Language (TPL) [HR95], a CCS-
like process algebra featuring an _idling_ prefix (modelling a delay) and a
_timeout_ operator. The choice of TPL is due to its simplicity and its well-
understood theory. We define $\mathtt{revTPL}$, a reversible extension of TPL,
and we show that it satisfies the properties expected from a causal-consistent
reversible calculus. Alternatively, $\mathtt{revTPL}$ can be interpreted as an
extension of reversible CCS (in particular CCSK [PU07]) with time.

A reversible semantics in a concurrent setting is frequently defined following
the causal-consistent approach [DK04, LMT14] (other approaches are also used,
e.g., to model biological systems [PUY12, PP18]). Causal-consistent
reversibility states that any action can be undone, provided that its
consequences, if any, are undone beforehand. Hence, it strongly relies on a
notion of causality. To prove the reversible semantics of $\mathtt{revTPL}$
causal-consistent, we exploit the theory in [LPU20], whereby causal-
consistency follows from three key properties:

Loop Lemma:

any action can be undone by a corresponding backward action;

Square Property:

concurrent actions can be executed in any order;

Parabolic Lemma:

backward computations do not introduce new states.

The application of causal-consistent reversibility to timed systems is not
straightforward, since time heavily changes the causal semantics of the
language. In untimed systems, causal dependencies are either _structural_
(e.g., via sequential composition) or determined by _synchronisations_. In
timed systems further dependencies between parallel processes can be
introduced by time, even when processes do not actually interact, as
illustrated in the following example.

######  Example 1 (Motivating example).

Consider the following Erlang code.

⬇

1process_A() ->

2 receive

3 X -> handleMsg()

4 after 200 ->

5 handleTimeout()

6 end

7end.

⬇

8process_B(Pid) ->

9 timer:sleep(500),

10 Pid! Msg

11end.

12

13PidA=spawn(?MODULE,process_A,[]),

14spawn(?MODULE,process_B,[PidA]).

Process A (lines $1-7$) waits for a message; if a message is received within
200 ms, then process A calls function handleMsg(), otherwise it calls function
handleTimeout(). Process B (lines $8-11$) sleeps for 500ms and then sends a
message to Pid, where Pid is a parameter of the function executed by process B
(line $8$). The code in line $13$ spawns an instance of process A and uses its
process identifier PidA as a parameter to spawn an instance of process B (line
$14$). The two process instances are supposed to communicate, but the timeout
in process A (line $4$) triggers after 200 ms, while process B will only send
the message after 500 ms (lines $9-10$). In this example, the timeout rules
out the execution where process A communicates with process B, which would be
possible in the untimed scenario. Namely, an execution can become unviable
because of a time dependency, without any actual interaction between the two
involved processes.  $\diamond$

From a technical point of view, the semantics of TPL does not fit the formats
for which a causal-consistent reversible semantics can be derived
automatically [PU07, LM20], and also the generalisation of the approaches
developed in the literature for untimed models [DK04, CKV13, LMS16] is not
straightforward and is the objective of this work.

The rest of the paper is structured as follows. Section 1 gives an informal
overview of TPL and reversibility. Section 2 introduces the syntax and
semantics of the reversible Temporal Process Language ($\mathtt{revTPL}$). In
Section 3, we relate $\mathtt{revTPL}$ to TPL and CCSK, while Section 4
studies the reversibility properties of $\mathtt{revTPL}$. Section 5 concludes
the paper and discusses related and future work. A formal background on CCS,
TPL and CCSK (for the readers that wish a more rigorous overview than the
informal one in Section 1), as well as longer proofs and additional technical
details are collected in Appendix.

This paper is an extended and revised version of [BLMY22]. The semantics has
been revised since the one in [BLMY22] failed to capture some time
dependencies when going back and forward (cf. Example 4.10). We now also
provide a better characterisation of the causality model of $\mathtt{revTPL}$
(cf. Proposition 8 and Theorem 12). Further technical improvements include the
formulation of the correspondences between $\mathtt{revTPL}$, $\mathtt{TPL}$,
CCSK and CCS in terms of (bi)simulations (Theorems 2 and 4). We now also
provide full proofs of all results as well as additional explanations and
examples. Finally, the whole presentation has been carefully refined.

##  1\. Informal Overview of TPL and Reversibility

In this section we give an informal overview of Hennessy & Regan’s TPL
(Temporal Process Language) [HR95] and introduce a few basic concepts of
causal-consistent reversibility [DK04, LPU20]. For a more rigorous
introduction, the interested reader can find the syntax and semantics of TPL
in Appendix A.3 and the syntax and semantics of the reversible calculus CCSK
[PU07] in Appendix A.2. The syntax and semantics of CCS, which is at the basis
of both TPL and CCSK, is in Appendix A.1.

###  1.1. Overview of TPL

Process $\lfloor pid.P\rfloor(Q)$ models a timeout: it can either immediately
do action $pid$ followed by $P$ or, in case of delay, continue as $Q$. In
transition (1) the timeout process is in parallel with co-party
$\overline{pid}.0$ that can immediately synchronise with action $pid$, and
hence the timeout process continues as $P$.

$\overline{pid}.0\parallel\lfloor pid.P\rfloor(Q)\xrightarrow{\tau}0\parallel
P$ (1)

In transition (2), $\lfloor pid.P\rfloor(Q)$ is in parallel with process
$\sigma.\overline{pid}.0$ that can synchronise only after a delay of one time
unit $\sigma$ ($\sigma$ is called a time action). Because of the delay, the
timeout process continues as $Q$:

$\sigma.\overline{pid}.0\parallel\lfloor
pid.P\rfloor(Q)\xrightarrow{\sigma}\overline{pid}.0\parallel Q$ (2)

The processes on the left-hand side of transition (2) describe the interaction
structures of the Erlang program in Example 1. More precisely, the timeout of
$200$ time units in process A can be encoded using nested timeouts:

$A(0)=Q\quad A(n+1)=\lfloor pid.P\rfloor(A(n))\quad(n\in\mathbb{N})$

while process B can be modelled as the sequential composition of $500$ actions
$\sigma$ followed by action $\overline{pid}$, as follows:

$B(0)=\overline{pid}\quad B(n+1)=\sigma.{B(n)}\quad(n\in\mathbb{N})$

Using the definition above, $\lfloor pid.P\rfloor(A(200))$ models a process
that executes $pid$ and continues as $P$ if a co-party is able to synchronise
within $200$ time units, otherwise executes $Q$. Hence, Example 1 is rendered
as follows:

$\lfloor pid.P\rfloor(A(200))\parallel B(500)$

The design of TPL is based on (and enjoys) three properties [HR95]: time-
determinism, patience, and maximal progress. _Time-determinism_ means that
time actions from one state can never reach distinct states, formally: if
$P\xrightarrow{\sigma}Q$ and $P\xrightarrow{\sigma}Q^{\prime}$ then
$Q=Q^{\prime}$. A consequence of time-determinism is that choices can only be
decided via communication actions and not by time actions, for example
$\alpha.P+\beta.Q$ can change state by action $\alpha$ or $\beta$, but not by
time action $\sigma$. Process $\alpha.P+\beta.Q$ can make an action $\sigma$,
by a property called patience, but this action would not change the state, as
shown in transition (3).

$\alpha.P+\beta.Q\xrightarrow{\sigma}\alpha.P+\beta.Q$ (3)

_Patience_ ensures that communication processes like $\alpha.P$ can
indefinitely delay communication $\alpha$ with $\sigma$ actions (without
changing state) until a co-party is available. For example, by patience,
process $\alpha.P$ in (4) can delay the communication on $\alpha$ until the
other process $\sigma.\overline{\alpha}.Q$ is ready to communicate:

$\alpha.P\parallel\sigma.\overline{\alpha}.Q\xrightarrow{\sigma}\alpha.P\parallel\overline{\alpha}.Q\xrightarrow{\tau}P\parallel
Q$ (4)

_Maximal progress_ states that (internal/synchronisation) $\tau$ actions
cannot be delayed, formally: if $P\xrightarrow{\tau}Q$ then there is no
$Q^{\prime}$ such that $P\xrightarrow{\sigma}Q^{\prime}$. Namely, a delay can
only be attained either via explicit $\sigma$ prefixes or because
synchronisation is not possible. Basically, patience allows for time actions
when communication is not possible, and maximal progress disallows time
actions when communication is possible:

$\begin{array}[]{lll}\alpha.P\xrightarrow{\sigma}&\text{ (by patience)}\\\
\alpha.P\parallel\overline{\alpha}.Q\not\xrightarrow{\sigma}\text{ because
}\alpha.P\parallel\overline{\alpha}.Q\xrightarrow{\tau}&\text{ (by maximal
progress)}\end{array}$

###  1.2. Overview of causal-consistent reversibility.

Before presenting $\mathtt{revTPL}$, we discuss the _reversing technique_ we
adopt. In the literature, two approaches to define a causal-consistent
extension of a given calculus or language have been proposed: _dynamic_ and
_static_ [LMM21]. The dynamic approach (as in [DK04, CKV13, LMS16]) makes
explicit use of memories to keep track of past events and causality relations,
while the static approach (originally proposed in [PU07]) is based on two
ideas: making all the operators of the language static so that no information
is lost and using communication keys to keep track of which events have been
executed. In the dynamic approach, constructors of processes disappear upon
transitions (as in standard calculi).

For example, in the following CCS transition:

$a.P\xrightarrow{a}P$

the action $a$ disappears as an effect of the transition. The dynamic approach
prescribes to use memories to keep track of the discarded items. In static
approaches, such as [PU07], actions are syntactically maintained, and process
$a.P$ can perform the transition below

$a.P\xrightarrow{a[i]}{\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color<EMAIL_ADDRESS>
where $P$ is decorated with the executed action $a$ and a unique key $i$. The
term
${\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color<EMAIL_ADDRESS>acts like $P$ in forward transitions, while the coloured part decorating $P$
is used to define backward transitions, e.g.,

${\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color<EMAIL_ADDRESS>
Keys are important to correctly revert synchronisations. Consider the process
below. It can take two forward synchronisations with keys $i$ and $j$,
respectively:

$a.P_{1}\parallel\overline{a}.P_{2}\parallel
a.Q_{1}\parallel\overline{a}.Q_{2}\xrightarrow{\tau[i]}\xrightarrow{\tau[j]}{\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}a[i].}P_{1}\parallel{\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}\overline{a}[i].}P_{2}\parallel{\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}a[j].}Q_{1}\parallel{\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color<EMAIL_ADDRESS>
From the reached state, there are two possible backward actions: $\tau[i]$ and
$\tau[j]$. The keys are used to ensure that a backward action, say $\tau[i]$,
only involves parallel components that have previously synchronised and not,
for instance,
${\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color<EMAIL_ADDRESS>and
${\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color<EMAIL_ADDRESS>When looking at the choice operator, in the following CCS transition:

$a.P+b.Q\xrightarrow{a}P$

both the choice operator “+” and the discarded branch $b.Q$ disappear as an
effect of the transition. In static approaches, the choice operator and the
discarded branch are syntactically maintained, and process $a.P+b.Q$ can
perform the transition below:

$a.P+b.Q\xrightarrow{a[i]}{\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}a[i].}P{\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color<EMAIL_ADDRESS>
where
${\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}a[i].}P{\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color<EMAIL_ADDRESS>acts like $P$ in forward transitions, while the coloured part allows one to
undo $a[i]$ and then possibly proceed forward with an action $b[j]$.

In this paper, we adopt the static approach since it is simpler, while the
dynamic approach is more suitable to complex languages such as the
$\pi$-calculus, see the discussion in [LMM21, LP21].

##  2\. The Reversible Temporal Process Language

In this section we define $\mathtt{revTPL}$, an extension of Hennessy & Regan
TPL (Temporal Process Language) [HR95] with causal-consistent reversibility
following the static approach in the style of [PU07].

###  2.1. Syntax of $\mathtt{revTPL}$.

We denote with $\mathcal{X}$ the set of all the configurations generated by
the grammar in Figure 1.

(Processes) $\displaystyle P=\,\pi.P\;\;|\;\;\lfloor
P\rfloor(Q)\;\;|\;\;P+Q\;\;|\;\;P\parallel Q\;\;|\;\;P\setminus
a\;\;|\;\;A\;\;|\;\;\mathbf{0}$ (Configurations) $\displaystyle X=\rho[\hskip
0.56905pt{\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}i}\hskip
0.56905pt].X\;\;|\;\;\lfloor
X\rfloor[{\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}\underrightarrow{i}}](Y)\;\;|\;\;\lfloor
X\rfloor[{\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}\underleftarrow{i}}](Y)\mid
X+Y\;\;|\;\;$ $\displaystyle\,\qquad X\parallel Y\;\;|\;\;X\setminus
a\;\;|\;\;P$ (Communication actions)
$\displaystyle\alpha=\,a\;\;|\;\;\overline{a}\;\;|\;\;\tau$ (Prefixes)
$\displaystyle\pi=\,\alpha\;\;|\;\;\sigma$ (Runtime prefixes)
$\displaystyle\rho=\,\pi\;\;|\;\;\sigma_{\bot}$ Figure 1. Syntax of
$\mathtt{revTPL}$

Processes ($P,Q,\ldots$) describe timed interactions following [HR95]. We let
$\mathcal{A}$ be the set of action names $a$, $\overline{\mathcal{A}}$ the set
of action conames $\overline{a}$. We use $\alpha$ to range over $a$,
$\overline{a}$ and internal actions $\tau$. We assume
$\overline{\overline{a}}=a$. In process $\pi.P$, prefix $\pi$ can be a
communication action $\alpha$ or a time action $\sigma$, and $P$ is the
continuation. Timeout $\lfloor P\rfloor(Q)$ executes either $P$ (if possible)
or $Q$ (in case of timeout). $P+Q$, $P\parallel Q$, $P\setminus a$, $A$, and
$\mathbf{0}$ are the usual choice, parallel composition, name restriction,
recursive call, and terminated process from CCS. For each recursive call $A$
we assume a recursive definition $A\stackrel{{\scriptstyle def}}{{=}}P$. We
also assume recursion to be guarded, hence recursive variables can only occur
under prefix.

Configurations ($X,Y,\ldots$) describe states via annotation of executed
actions with keys following the static approach. We let $\mathcal{K}$ be the
set of all keys ($k,i,j,\ldots$). Configurations are processes with (possibly)
some computational history (i.e., prefixes marked with keys): $\pi[\hskip
0.56905pt{\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}i}\hskip
0.56905pt].X$ is the configuration that has already executed $\pi$, and the
execution of such $\pi$ is identified by key $i$. Configuration $\lfloor
X\rfloor[{\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}\underleftarrow{i}}](Y)$
is executing the main branch $X$ whereas $\lfloor
X\rfloor[{\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}\underrightarrow{i}}](Y)$
is executing $Y$. Some TPL processes, namely patient processes like $\alpha.P$
illustrated earlier in (4), allow time to pass without changing their own
structure. This is an issue in $\mathtt{revTPL}$, since it may lead different
parallel components to have a different understanding of the passage of time,
while we want time to pass at the same pace for each parallel component. For
this reason, to record that time has passed for a patient process, we use a
special prefix $\sigma_{\bot}[\hskip
0.56905pt{\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}i}\hskip
0.56905pt].X$. Namely, $\sigma_{\bot}[\hskip
0.56905pt{\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}i}\hskip
0.56905pt].X$ is the configuration which has patiently registered the passage
of time along with key $i$. Prefix $\sigma_{\bot}[\hskip
0.56905pt{\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}i}\hskip
0.56905pt]$ differs from $\sigma[\hskip
0.56905pt{\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}i}\hskip
0.56905pt]$ since the former is only for the current execution (patient delays
_may_ happen but do not always have to), while the latter requires time to
pass in each possible execution (see Example 2). We will discuss this issue in
more detail in Section 4. We use $\rho$ to denote either $\pi$ or
$\sigma_{\bot}$.

A configuration can be thought of as a context with actions that have already
been executed, each associated to a key, containing a process $P$, with
actions yet to execute and hence with no keys. Notably, keys are distinct but
for actions happening together: an action and a co-action that synchronise, or
the same time action traced by different processes, e.g., by two parallel
delays. A configuration $P$ can be thought of as the initial state of a
computation, where no action has been executed yet. We call such
configurations _standard_. Definition 1 formalises this notion via function
$\mathtt{keys}(X)$ that returns the set of keys of a given configuration.

[Standard configuration] The set of keys of a configuration $X$, written
$\mathtt{keys}(X)$, is inductively defined as follows:

$\begin{array}[]{llllll}&\mathtt{keys}(P)=\emptyset&&\quad\mathtt{keys}(\rho[\hskip
0.56905pt{\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}i}\hskip
0.56905pt].X)=\\{i\\}\cup\mathtt{keys}(X)&&\quad\mathtt{keys}(X\setminus
a)=\mathtt{keys}(X)\\\ &\lx@intercol\mathtt{keys}(\lfloor
Y\rfloor[{\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}\underrightarrow{i}}](X))=\mathtt{keys}(\lfloor
X\rfloor[{\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}\underleftarrow{i}}](Y))=\\{i\\}\cup\mathtt{keys}(X)\hfil\lx@intercol\\\
&\lx@intercol\mathtt{keys}(X+Y)=\mathtt{keys}(X\parallel
Y)=\mathtt{keys}(X)\cup\mathtt{keys}(Y)\hfil\lx@intercol\\\ \end{array}$

A configuration $X$ is _standard_ , written $\mathtt{std}(X)$, if
$\mathtt{keys}(X)=\emptyset$. Basically, a standard configuration is a
process. To handle the delicate interplay between time-determinism and
reversibility of time actions, it is useful to distinguish the class of
configurations that have not executed any _communication_ action (but may have
executed time actions). We call these configurations _not-acted_ and
characterise them formally using the predicate $\mathtt{nact}(\cdot)$ below.

[Not-acted configuration] The not-acted predicate $\mathtt{nact}(\cdot)$ is
inductively defined as:

$\begin{array}[]{ll}&\mathtt{nact}(\mathbf{0})=\mathtt{nact}(A)=\mathtt{nact}(\lfloor
X\rfloor(Y))=\mathtt{nact}(\pi.X)=\mathtt{tt}\\\ &\mathtt{nact}(\alpha[\hskip
0.56905pt{\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}i}\hskip
0.56905pt].X)=\mathtt{nact}(\lfloor
X\rfloor[{\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}\underleftarrow{i}}](Y))=\mathtt{ff}\\\
&\mathtt{nact}(\sigma[\hskip
0.56905pt{\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}i}\hskip
0.56905pt].X)=\mathtt{nact}(\sigma_{\bot}[\hskip
0.56905pt{\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}i}\hskip
0.56905pt].X)=\mathtt{nact}(X\setminus a)=\mathtt{nact}(\lfloor
Y\rfloor[{\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}\underrightarrow{i}}](X))=\mathtt{nact}(X)\\\
&\mathtt{nact}(X\parallel
Y)=\mathtt{nact}(X+Y)=\mathtt{nact}(X)\wedge\mathtt{nact}(Y)\end{array}$

A configuration $X$ is _not-acted_ (resp. _acted_) if
$\mathtt{nact}(X)=\mathtt{tt}$ (resp. $\mathtt{nact}(X)=\mathtt{ff}$). Basic
standard configurations are always not-acted (first line of Definition 1).
Indeed, it is not possible to reach a configuration $\pi.X$ where $X$ is
acted. In the second line, a configuration that has executed communication
actions is acted. In particular, we will see that $\lfloor
X\rfloor[{\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}\underleftarrow{i}}](Y)$
is only reachable via a communication action. The configurations in the third
line are not-acted if their continuations are not-acted. For parallel
composition and choice, $\mathtt{nact}(\cdot)$ is defined as a conjunction.
For example $\mathtt{nact}(\alpha[\hskip
0.56905pt{\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}i}\hskip
0.56905pt].P\parallel\beta.Q)=\mathtt{ff}$ and $\mathtt{nact}(\alpha[\hskip
0.56905pt{\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}i}\hskip
0.56905pt].P+\beta.Q)=\mathtt{ff}$. Note that in a choice configuration $X+Y$,
at most one between $X$ and $Y$ can be acted. Whereas $\mathtt{std}(X)$
implies $\mathtt{nact}(X)$, the opposite implication does not hold. For
example, $\mathtt{std}(\sigma[\hskip
0.56905pt{\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}i}\hskip
0.56905pt].\mathbf{0})=\mathtt{ff}$ but $\mathtt{nact}(\sigma[\hskip
0.56905pt{\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}i}\hskip
0.56905pt].\mathbf{0})=\mathtt{tt}$.

###  2.2. Semantics of $\mathtt{revTPL}$.

We denote with $\mathcal{A}^{t}$ the set
$\mathcal{A}\cup\overline{\mathcal{A}}\cup\\{\tau,\sigma\\}$ of actions and
let $\pi$ to range over the set $\mathcal{A}^{t}$. We define the set of all
the labels $\mathcal{L}=\mathcal{A}^{t}\times\mathcal{K}$. The labels
associate each $\pi\in\mathcal{A}^{t}$ to a key $i$. The key is used to
associate the forward occurrence of an action with its corresponding reversal.
Also, instances of actions occurring together (synchronising action and co-
action or the effect of time passing in different components of a process)
have the same key, otherwise keys are distinct.

PAct $\displaystyle\displaystyle{\alpha.P\xrightarrow{\sigma[\hskip
0.56905pt{\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}i}\hskip
0.56905pt]}\sigma_{\bot}[\hskip
0.56905pt{\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}i}\hskip
0.56905pt].\alpha.P}$ RAct
$\displaystyle\displaystyle{\pi.P\xrightarrow{\pi[\hskip
0.56905pt{\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}i}\hskip
0.56905pt]}\pi[\hskip
0.56905pt{\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}i}\hskip
0.56905pt].P}$ Idle
$\displaystyle\displaystyle{\mathbf{0}\xrightarrow{\sigma[\hskip
0.56905pt{\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}i}\hskip
0.56905pt]}\sigma_{\bot}[\hskip
0.56905pt{\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}i}\hskip
0.56905pt].\mathbf{0}}$ Act $\displaystyle\displaystyle{\hbox{\hskip
41.47719pt\vbox{\hbox{\hskip-41.47717pt\hbox{\hbox{$\displaystyle\displaystyle{X\xrightarrow{\pi[\hskip
0.56905pt{\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}j}\hskip
0.56905pt]}X^{\prime}}$}\hskip
20.00003pt\hbox{\hbox{$\displaystyle\displaystyle{j\neq
i}$}}}}\vbox{}}}\over\hbox{\hskip
40.63501pt\vbox{\vbox{}\hbox{\hskip-40.635pt\hbox{\hbox{$\displaystyle\displaystyle{\rho[\hskip
0.56905pt{\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}i}\hskip
0.56905pt].X\xrightarrow{\pi[\hskip
0.56905pt{\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}j}\hskip
0.56905pt]}\rho[\hskip
0.56905pt{\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}i}\hskip
0.56905pt].X^{\prime}}$}}}}}}$ STout $\displaystyle\displaystyle{\hbox{\hskip
62.68585pt\vbox{\hbox{\hskip-62.68584pt\hbox{\hbox{$\displaystyle\displaystyle{X\not\xrightarrow{\tau}}$}\hskip
20.00003pt\hbox{\hbox{$\displaystyle\displaystyle{\mathtt{std}(X)}$}\hskip
20.00003pt\hbox{\hbox{$\displaystyle\displaystyle{\mathtt{std}({Y})}$}}}}}\vbox{}}}\over\hbox{\hskip
50.23726pt\vbox{\vbox{}\hbox{\hskip-50.23724pt\hbox{\hbox{$\displaystyle\displaystyle{\lfloor
X\rfloor(Y)\xrightarrow{\sigma[\hskip
0.56905pt{\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}i}\hskip
0.56905pt]}\lfloor
X\rfloor[{\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}\underrightarrow{i}}](Y)}$}}}}}}$
SWait $\displaystyle\displaystyle{\hbox{\hskip
40.43555pt\vbox{\hbox{\hskip-40.43553pt\hbox{\hbox{$\displaystyle\displaystyle{Y\xrightarrow{\pi[\hskip
0.56905pt{\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}j}\hskip
0.56905pt]}Y^{\prime}}$}\hskip
20.00003pt\hbox{\hbox{$\displaystyle\displaystyle{j\neq
i}$}}}}\vbox{}}}\over\hbox{\hskip
57.66989pt\vbox{\vbox{}\hbox{\hskip-57.66988pt\hbox{\hbox{$\displaystyle\displaystyle{\lfloor
X\rfloor[{\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}\underrightarrow{i}}](Y)\xrightarrow{\pi[\hskip
0.56905pt{\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}j}\hskip
0.56905pt]}\lfloor
X\rfloor[{\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}\underrightarrow{i}}](Y^{\prime})}$}}}}}}$
Tout $\displaystyle\displaystyle{\hbox{\hskip
45.2046pt\vbox{\hbox{\hskip-45.2046pt\hbox{\hbox{$\displaystyle\displaystyle{X\xrightarrow{\alpha[\hskip
0.56905pt{\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}i}\hskip
0.56905pt]}X^{\prime}}$}\hskip
20.00003pt\hbox{\hbox{$\displaystyle\displaystyle{\mathtt{std}({Y})}$}}}}\vbox{}}}\over\hbox{\hskip
53.0796pt\vbox{\vbox{}\hbox{\hskip-53.0796pt\hbox{\hbox{$\displaystyle\displaystyle{\lfloor
X\rfloor(Y)\xrightarrow{\alpha[\hskip
0.56905pt{\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}i}\hskip
0.56905pt]}\lfloor
X^{\prime}\rfloor[{\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}\underleftarrow{i}}](Y)}$}}}}}}$
Wait $\displaystyle\displaystyle{\hbox{\hskip
41.47719pt\vbox{\hbox{\hskip-41.47717pt\hbox{\hbox{$\displaystyle\displaystyle{X\xrightarrow{\pi[\hskip
0.56905pt{\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}j}\hskip
0.56905pt]}X^{\prime}}$}\hskip
20.00003pt\hbox{\hbox{$\displaystyle\displaystyle{j\neq
i}$}}}}\vbox{}}}\over\hbox{\hskip
61.13171pt\vbox{\vbox{}\hbox{\hskip-61.1317pt\hbox{\hbox{$\displaystyle\displaystyle{\lfloor
X\rfloor[{\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}\underleftarrow{i}}](Y)\xrightarrow{\pi[\hskip
0.56905pt{\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}j}\hskip
0.56905pt]}\lfloor
X^{\prime}\rfloor[{\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}\underleftarrow{i}}](Y)}$}}}}}}$
SynW $\displaystyle\displaystyle{\hbox{\hskip
85.08563pt\vbox{\hbox{\hskip-85.08563pt\hbox{\hbox{$\displaystyle\displaystyle{X\xrightarrow{\sigma[\hskip
0.56905pt{\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}i}\hskip
0.56905pt]}X^{\prime}\qquad Y\xrightarrow{\sigma[\hskip
0.56905pt{\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}i}\hskip
0.56905pt]}Y^{\prime}\qquad(X\parallel
Y)\not\xrightarrow{\tau}}$}}}\vbox{}}}\over\hbox{\hskip
37.39694pt\vbox{\vbox{}\hbox{\hskip-37.39694pt\hbox{\hbox{$\displaystyle\displaystyle{X\parallel
Y\xrightarrow{\sigma[\hskip
0.56905pt{\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}i}\hskip
0.56905pt]}X^{\prime}\parallel Y^{\prime}}$}}}}}}$ Par
$\displaystyle\displaystyle{\hbox{\hskip
58.03827pt\vbox{\hbox{\hskip-58.03825pt\hbox{\hbox{$\displaystyle\displaystyle{X\xrightarrow{\alpha[\hskip
0.56905pt{\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}i}\hskip
0.56905pt]}X^{\prime}}$}\hskip
20.00003pt\hbox{\hbox{$\displaystyle\displaystyle{i\not\in\mathtt{keys}(Y)}$}}}}\vbox{}}}\over\hbox{\hskip
36.9684pt\vbox{\vbox{}\hbox{\hskip-36.96838pt\hbox{\hbox{$\displaystyle\displaystyle{X\parallel
Y\xrightarrow{\alpha[\hskip
0.56905pt{\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}i}\hskip
0.56905pt]}X^{\prime}\parallel Y}$}}}}}}$ Syn
$\displaystyle\displaystyle{\hbox{\hskip
49.47455pt\vbox{\hbox{\hskip-49.47455pt\hbox{\hbox{$\displaystyle\displaystyle{X\xrightarrow{\alpha[\hskip
0.56905pt{\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}i}\hskip
0.56905pt]}X^{\prime}\qquad Y\xrightarrow{\overline{\alpha}[\hskip
0.56905pt{\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}i}\hskip
0.56905pt]}Y^{\prime}}$}}}\vbox{}}}\over\hbox{\hskip
36.72565pt\vbox{\vbox{}\hbox{\hskip-36.72565pt\hbox{\hbox{$\displaystyle\displaystyle{X\parallel
Y\xrightarrow{\tau[\hskip
0.56905pt{\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}i}\hskip
0.56905pt]}X^{\prime}\parallel Y^{\prime}}$}}}}}}$ ChoW
$\displaystyle\displaystyle{\hbox{\hskip
59.49017pt\vbox{\hbox{\hskip-59.49017pt\hbox{\hbox{$\displaystyle\displaystyle{X\xrightarrow{\sigma[\hskip
0.56905pt{\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}i}\hskip
0.56905pt]}X^{\prime}\qquad Y\xrightarrow{\sigma[\hskip
0.56905pt{\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}i}\hskip
0.56905pt]}Y^{\prime}\qquad}$}}}\vbox{}}}\over\hbox{\hskip
40.17473pt\vbox{\vbox{}\hbox{\hskip-40.17473pt\hbox{\hbox{$\displaystyle\displaystyle{X+Y\xrightarrow{\sigma[\hskip
0.56905pt{\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}i}\hskip
0.56905pt]}X^{\prime}+Y^{\prime}}$}}}}}}$ Cho
$\displaystyle\displaystyle{\hbox{\hskip
82.0522pt\vbox{\hbox{\hskip-82.05219pt\hbox{\hbox{$\displaystyle\displaystyle{X\xrightarrow{\alpha[\hskip
0.56905pt{\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}i}\hskip
0.56905pt]}X^{\prime}}$}\hskip
20.00003pt\hbox{\hbox{$\displaystyle\displaystyle{\mathtt{nact}(Y)}$}\hskip
20.00003pt\hbox{\hbox{$\displaystyle\displaystyle{i\notin\mathtt{keys}(Y)}$}}}}}\vbox{}}}\over\hbox{\hskip
39.74619pt\vbox{\vbox{}\hbox{\hskip-39.74617pt\hbox{\hbox{$\displaystyle\displaystyle{X+Y\xrightarrow{\alpha[\hskip
0.56905pt{\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}i}\hskip
0.56905pt]}X^{\prime}+Y}$}}}}}}$ Hide $\displaystyle\displaystyle{\hbox{\hskip
53.11317pt\vbox{\hbox{\hskip-53.11317pt\hbox{\hbox{$\displaystyle\displaystyle{X\xrightarrow{\pi[\hskip
0.56905pt{\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}i}\hskip
0.56905pt]}X^{\prime}}$}\hskip
20.00003pt\hbox{\hbox{$\displaystyle\displaystyle{\pi\not\in\\{a,\overline{a}\\}}$}}}}\vbox{}}}\over\hbox{\hskip
36.65591pt\vbox{\vbox{}\hbox{\hskip-36.6559pt\hbox{\hbox{$\displaystyle\displaystyle{X\setminus
a\xrightarrow{\pi[\hskip
0.56905pt{\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}i}\hskip
0.56905pt]}X^{\prime}\setminus a}$}}}}}}$ Const
$\displaystyle\displaystyle{\hbox{\hskip
47.33275pt\vbox{\hbox{\hskip-47.33275pt\hbox{\hbox{$\displaystyle\displaystyle{A\stackrel{{\scriptstyle
def}}{{=}}P}$}\hskip
20.00003pt\hbox{\hbox{$\displaystyle\displaystyle{P\xrightarrow{\pi[\hskip
0.56905pt{\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}i}\hskip
0.56905pt]}X}$}}}}\vbox{}}}\over\hbox{\hskip
18.70427pt\vbox{\vbox{}\hbox{\hskip-18.70425pt\hbox{\hbox{$\displaystyle\displaystyle{A\xrightarrow{\pi[\hskip
0.56905pt{\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}i}\hskip
0.56905pt]}X}$}}}}}}$

The set of rules also includes symmetric versions of rules [Par] and [Cho].

Figure 2. $\mathtt{revTPL}$ forward LTS

[Semantics] The operational semantics of $\mathtt{revTPL}$ is given by two
Labelled Transition Systems (LTSs) defined on the same set of all
configurations $\mathcal{X}$, and the set of all labels $\mathcal{L}$: a
forward LTS ($\mathcal{X}$, $\mathcal{L}$, $\xrightarrow{}$) and a backward
LTS ($\mathcal{X}$, $\mathcal{L}$, $\xhookrightarrow{}$). We define
$\xmapsto{}=\xrightarrow{}\cup\xhookrightarrow{}$, where $\xrightarrow{}$ and
$\xhookrightarrow{}$ are the least transition relations induced by the rules
in Figure 2 and Figure 3, respectively.

Given a relation $\mathcal{R}$, we indicate with $\mathcal{R}^{*}$ its
reflexive and transitive closure. We use notation $X\not\xrightarrow{\tau}$
(resp. $X\not\xhookrightarrow{\tau}$) when there are no configuration
$X^{\prime}$ and key $i$ such that $X\xrightarrow{\tau[i]}X^{\prime}$ (resp.
$X\xhookrightarrow{\tau[i]}X^{\prime}$).

We now discuss the rules of the forward semantics (Figure 2). Rule [PAct]
describes patient actions: in TPL process $\alpha.P$ can make a time step to
itself. This kind of actions allows a process to wait indefinitely until it
can communicate (by patience [HR95]). However, in $\mathtt{revTPL}$ we need to
track passage of time, hence rule [PAct] adds a $\sigma_{\bot}[\hskip
0.56905pt{\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}i}\hskip
0.56905pt]$ prefix in front of the configuration, with a key
${\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}i}$.
Rule [RAct] executes actions $\alpha[\hskip
0.56905pt{\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}i}\hskip
0.56905pt]$ or $\sigma[\hskip
0.56905pt{\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}i}\hskip
0.56905pt]$ on a prefix process. Observe that, unlike patient time actions on
$\alpha.P$, a time action on $\sigma.P$ corresponds to a deliberate and
planned time consuming action and, therefore, it executes the $\sigma$ prefix,
hence no $\sigma_{\bot}$ prefix needs to be added. Rule [Idle] registers
passage of time on a $\mathbf{0}$ configuration by adding a
$\sigma_{\bot}[\hskip
0.56905pt{\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}i}\hskip
0.56905pt]$ prefix to it. Rule [Act] lifts actions of the continuation $X$ on
configurations where prefix $\rho[\hskip
0.56905pt{\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}i}\hskip
0.56905pt]$ has already been executed. Side condition
${\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}j}\neq{\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}i}$
ensures freshness of
${\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}j}$
is preserved. Rules [STout] and [SWait] model timeouts. In rule [STout], if
$X$ is not able to make $\tau$ actions then $Y$ is executed; this rule models
a timeout that triggers only if the main configuration $X$ is stuck. The
negative premise on [Stout] can be encoded into a decidable positive one as
shown in Appendix B. In rule [Tout] instead the main configuration can execute
and the timeout does not trigger. Rule [SWait] (resp. [Wait]) models
transitions inside a timeout configuration where the $Y$ (resp. $X$) branch
has been previously taken. The semantics of timeout construct becomes clearer
in the larger context of parallel configurations, when looking at rule [SynW].
Rule [SynW] models time passing for parallel configurations. The negative
premise ensures that, in case $X$ or $Y$ is a timeout configuration, timeout
can trigger only if no synchronisation may occur, that is if the
configurations are stuck. [SynW] requires time to pass in the same way (an
action $\sigma$ is taken by both components, with the same key
${\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}i}$)
for the whole system. Rules [Par] (and symmetric) and [Syn] are as usual for
communication actions and allow parallel configurations to either proceed
independently or to synchronise. In the latter case, the keys need to
coincide. Defining the semantics of choice configuration $X+Y$ requires
special care to ensure time-determinism (recall, choices are only decided via
communication actions). Also, we need to record time actions to be able to
reverse them correctly (cfr. Loop Lemma, discussed later on in Lemma 6). Rule
[ChoW] describes the passage of time along a choice configuration $X+Y$. Since
time does not decide a choice, both branches have to execute the same time
action with the same key. Rule [Cho] allows one to take one branch, or
continue executing a previously taken branch. The choice construct is
syntactically preserved, to allow for reversibility, but the one branch that
is not taken remains non-acted (i.e., $\mathtt{nact}(Y)$). This ensures that
choices can be decided by a communication action only. Let us note that even
in case of a decided choice, that is a choice configuration in which one of
the two branches has performed a communication action, time actions are
registered by both configurations. For example, the configuration
$a.\mathbf{0}+\sigma.\mathbf{0}$ can execute the following transitions:

$a.\mathbf{0}+\sigma.\mathbf{0}\xrightarrow{a[\hskip
0.56905pt{\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}i}\hskip
0.56905pt]}a[\hskip
0.56905pt{\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}i}\hskip
0.56905pt].\mathbf{0}+\sigma.\mathbf{0}\xrightarrow{\sigma[\hskip
0.56905pt{\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}j}\hskip
0.56905pt]}a[\hskip
0.56905pt{\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}i}\hskip
0.56905pt].\sigma_{\bot}[\hskip
0.56905pt{\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}j}\hskip
0.56905pt].\mathbf{0}+\sigma[\hskip
0.56905pt{\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}j}\hskip
0.56905pt].\mathbf{0}$

After the $a[\hskip
0.56905pt{\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}i}\hskip
0.56905pt]$ action, even if the left branch of the choice has been selected,
both branches participate to the time action $\sigma[\hskip
0.56905pt{\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}j}\hskip
0.56905pt]$. Rules [Hide] and [Const] are standard.

The rules of the backward semantics, in Figure 3, undo communication and time
actions executed under the forward semantics. Backward rules are symmetric to
the forward ones.

Now that we have introduced both the forward and the backward rules we can
clarify the difference between $\sigma_{\bot}$ and $\sigma$.

######  Example 2.

Let us consider the patient process $a.P$. We can have the following
derivation:

$a.P\xrightarrow{\sigma[\hskip
0.56905pt{\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}i}\hskip
0.56905pt]}\sigma_{\bot}[\hskip
0.56905pt{\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}i}\hskip
0.56905pt].a.P\xhookrightarrow{\sigma[\hskip
0.56905pt{\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}i}\hskip
0.56905pt]}a.P\xrightarrow{a[\hskip
0.56905pt{\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}j}\hskip
0.56905pt]}a[\hskip
0.56905pt{\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}j}\hskip
0.56905pt].P$ (5)

where $a.P$ executes forwards in two different ways: first by letting time
pass, later on by interacting on $a$. Notice that for these interactions to be
possible in a larger context we need the context to have changed as well.

We can try to have a similar derivation using process $\sigma.a.P$ instead,
but the final outcome is not the same:

$\sigma.a.P\xrightarrow{\sigma[\hskip
0.56905pt{\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}i}\hskip
0.56905pt]}\sigma[\hskip
0.56905pt{\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}i}\hskip
0.56905pt].a.P\xhookrightarrow{\sigma[\hskip
0.56905pt{\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}i}\hskip
0.56905pt]}\sigma.a.P$ (6)

Indeed, at this stage $\sigma.a.P$ cannot interact on $a$. In general,
$\sigma$ requires time to pass in every possible computation, while
$\sigma_{\bot}$ does not.  $\diamond$

Pact $\displaystyle\displaystyle{\sigma_{\bot}[\hskip
0.56905pt{\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}i}\hskip
0.56905pt].\alpha.P\xhookrightarrow{\sigma[\hskip
0.56905pt{\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}i}\hskip
0.56905pt]}\alpha.P}$ Ract $\displaystyle\displaystyle{\pi[\hskip
0.56905pt{\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}i}\hskip
0.56905pt].P\xhookrightarrow{\pi[\hskip
0.56905pt{\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}i}\hskip
0.56905pt]}\pi.P}$ Idle $\displaystyle\displaystyle{\sigma_{\bot}[\hskip
0.56905pt{\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}i}\hskip
0.56905pt].\mathbf{0}\xhookrightarrow{\sigma[\hskip
0.56905pt{\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}i}\hskip
0.56905pt]}\mathbf{0}}$ Act $\displaystyle\displaystyle{\hbox{\hskip
42.86607pt\vbox{\hbox{\hskip-42.86607pt\hbox{\hbox{$\displaystyle\displaystyle{X\xhookrightarrow{\pi[\hskip
0.56905pt{\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}j}\hskip
0.56905pt]}X^{\prime}\qquad j\not=i}$}}}\vbox{}}}\over\hbox{\hskip
38.135pt\vbox{\vbox{}\hbox{\hskip-38.135pt\hbox{\hbox{$\displaystyle\displaystyle{\rho[\hskip
0.56905pt{\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}i}\hskip
0.56905pt].X\xhookrightarrow{\pi[\hskip
0.56905pt{\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}j}\hskip
0.56905pt]}\rho[\hskip
0.56905pt{\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}i}\hskip
0.56905pt].X^{\prime}}$}}}}}}$ STout $\displaystyle\displaystyle{\hbox{\hskip
62.68585pt\vbox{\hbox{\hskip-62.68584pt\hbox{\hbox{$\displaystyle\displaystyle{X\not\xrightarrow{\tau}}$}\hskip
20.00003pt\hbox{\hbox{$\displaystyle\displaystyle{\mathtt{std}(X)}$}\hskip
20.00003pt\hbox{\hbox{$\displaystyle\displaystyle{\mathtt{std}({Y})}$}}}}}\vbox{}}}\over\hbox{\hskip
47.73724pt\vbox{\vbox{}\hbox{\hskip-47.73724pt\hbox{\hbox{$\displaystyle\displaystyle{\lfloor
X\rfloor[{\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}\underrightarrow{i}}](Y)\xhookrightarrow{\sigma[\hskip
0.56905pt{\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}i}\hskip
0.56905pt]}\lfloor X\rfloor(Y)}$}}}}}}$ SWait
$\displaystyle\displaystyle{\hbox{\hskip
41.82443pt\vbox{\hbox{\hskip-41.82443pt\hbox{\hbox{$\displaystyle\displaystyle{Y\xhookrightarrow{\pi[\hskip
0.56905pt{\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}j}\hskip
0.56905pt]}Y^{\prime}\qquad j\not=i}$}}}\vbox{}}}\over\hbox{\hskip
55.16988pt\vbox{\vbox{}\hbox{\hskip-55.16988pt\hbox{\hbox{$\displaystyle\displaystyle{\lfloor
X\rfloor[{\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}\underrightarrow{i}}](Y)\xhookrightarrow{\pi[\hskip
0.56905pt{\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}j}\hskip
0.56905pt]}\lfloor
X\rfloor[{\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}\underrightarrow{i}}](Y^{\prime})}$}}}}}}$
Tout $\displaystyle\displaystyle{\hbox{\hskip
42.7046pt\vbox{\hbox{\hskip-42.70459pt\hbox{\hbox{$\displaystyle\displaystyle{X\xhookrightarrow{\alpha[\hskip
0.56905pt{\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}i}\hskip
0.56905pt]}X^{\prime}\qquad\mathtt{std}({Y})}$}}}\vbox{}}}\over\hbox{\hskip
50.5796pt\vbox{\vbox{}\hbox{\hskip-50.57959pt\hbox{\hbox{$\displaystyle\displaystyle{\lfloor
X\rfloor[{\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}\underleftarrow{i}}](Y)\xhookrightarrow{\alpha[\hskip
0.56905pt{\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}i}\hskip
0.56905pt]}\lfloor X^{\prime}\rfloor(Y)}$}}}}}}$ Wait
$\displaystyle\displaystyle{\hbox{\hskip
38.97717pt\vbox{\hbox{\hskip-38.97717pt\hbox{\hbox{$\displaystyle\displaystyle{X\xhookrightarrow{\pi[\hskip
0.56905pt{\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}j}\hskip
0.56905pt]}X^{\prime}}$}\hskip
20.00003pt\hbox{\hbox{$\displaystyle\displaystyle{j\neq
i}$}}}}\vbox{}}}\over\hbox{\hskip
58.6317pt\vbox{\vbox{}\hbox{\hskip-58.6317pt\hbox{\hbox{$\displaystyle\displaystyle{\lfloor
X\rfloor[{\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}\underleftarrow{i}}](Y)\xhookrightarrow{\pi[\hskip
0.56905pt{\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}j}\hskip
0.56905pt]}\lfloor
X^{\prime}\rfloor[{\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}\underleftarrow{i}}](Y)}$}}}}}}$
SynW $\displaystyle\displaystyle{\hbox{\hskip
77.58562pt\vbox{\hbox{\hskip-77.5856pt\hbox{\hbox{$\displaystyle\displaystyle{X\xhookrightarrow{\sigma[\hskip
0.56905pt{\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}i}\hskip
0.56905pt]}X^{\prime}\qquad Y\xhookrightarrow{\sigma[\hskip
0.56905pt{\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}i}\hskip
0.56905pt]}Y^{\prime}\qquad(X\parallel
Y)\not\xhookrightarrow{\tau}}$}}}\vbox{}}}\over\hbox{\hskip
34.89694pt\vbox{\vbox{}\hbox{\hskip-34.89693pt\hbox{\hbox{$\displaystyle\displaystyle{X\parallel
Y\xhookrightarrow{\sigma[\hskip
0.56905pt{\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}i}\hskip
0.56905pt]}X^{\prime}\parallel Y^{\prime}}$}}}}}}$ Par
$\displaystyle\displaystyle{\hbox{\hskip
55.53825pt\vbox{\hbox{\hskip-55.53825pt\hbox{\hbox{$\displaystyle\displaystyle{X\xhookrightarrow{\alpha[\hskip
0.56905pt{\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}i}\hskip
0.56905pt]}X^{\prime}\qquad
i\not\in\mathtt{keys}(Y)}$}}}\vbox{}}}\over\hbox{\hskip
34.46838pt\vbox{\vbox{}\hbox{\hskip-34.46838pt\hbox{\hbox{$\displaystyle\displaystyle{X\parallel
Y\xhookrightarrow{\alpha[\hskip
0.56905pt{\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}i}\hskip
0.56905pt]}X^{\prime}\parallel Y}$}}}}}}$ Syn
$\displaystyle\displaystyle{\hbox{\hskip
44.47453pt\vbox{\hbox{\hskip-44.47453pt\hbox{\hbox{$\displaystyle\displaystyle{X\xhookrightarrow{\alpha[\hskip
0.56905pt{\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}i}\hskip
0.56905pt]}X^{\prime}\qquad Y\xhookrightarrow{\overline{\alpha}[\hskip
0.56905pt{\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}i}\hskip
0.56905pt]}Y^{\prime}}$}}}\vbox{}}}\over\hbox{\hskip
34.22565pt\vbox{\vbox{}\hbox{\hskip-34.22563pt\hbox{\hbox{$\displaystyle\displaystyle{X\parallel
Y\xhookrightarrow{\tau[\hskip
0.56905pt{\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}i}\hskip
0.56905pt]}X^{\prime}\parallel Y^{\prime}}$}}}}}}$ ChoW
$\displaystyle\displaystyle{\hbox{\hskip
54.49016pt\vbox{\hbox{\hskip-54.49016pt\hbox{\hbox{$\displaystyle\displaystyle{X\xhookrightarrow{\sigma[\hskip
0.56905pt{\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}i}\hskip
0.56905pt]}X^{\prime}\qquad Y\xhookrightarrow{\sigma[\hskip
0.56905pt{\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}i}\hskip
0.56905pt]}Y^{\prime}\qquad}$}}}\vbox{}}}\over\hbox{\hskip
37.67473pt\vbox{\vbox{}\hbox{\hskip-37.67471pt\hbox{\hbox{$\displaystyle\displaystyle{X+Y\xhookrightarrow{\sigma[\hskip
0.56905pt{\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}i}\hskip
0.56905pt]}X^{\prime}+Y^{\prime}}$}}}}}}$ Cho
$\displaystyle\displaystyle{\hbox{\hskip
82.88553pt\vbox{\hbox{\hskip-82.88553pt\hbox{\hbox{$\displaystyle\displaystyle{X\xhookrightarrow{\alpha[\hskip
0.56905pt{\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}i}\hskip
0.56905pt]}X^{\prime}}$}\hskip
20.00003pt\hbox{\hbox{$\displaystyle\displaystyle{\mathtt{nact}(Y)}$}\hskip
20.00003pt\hbox{\hbox{$\displaystyle\displaystyle{i\not\in\mathtt{keys}(Y)}$}}}}}\vbox{}}}\over\hbox{\hskip
37.24617pt\vbox{\vbox{}\hbox{\hskip-37.24617pt\hbox{\hbox{$\displaystyle\displaystyle{X+Y\xhookrightarrow{\alpha[\hskip
0.56905pt{\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}i}\hskip
0.56905pt]}X^{\prime}+Y}$}}}}}}$ Hide $\displaystyle\displaystyle{\hbox{\hskip
50.61317pt\vbox{\hbox{\hskip-50.61316pt\hbox{\hbox{$\displaystyle\displaystyle{X\xhookrightarrow{\pi[\hskip
0.56905pt{\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}i}\hskip
0.56905pt]}X^{\prime}}$}\hskip
20.00003pt\hbox{\hbox{$\displaystyle\displaystyle{\pi\not\in\\{a,\overline{a}\\}}$}}}}\vbox{}}}\over\hbox{\hskip
34.1559pt\vbox{\vbox{}\hbox{\hskip-34.1559pt\hbox{\hbox{$\displaystyle\displaystyle{X\setminus
a\xhookrightarrow{\pi[\hskip
0.56905pt{\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}i}\hskip
0.56905pt]}X^{\prime}\setminus a}$}}}}}}$ Const
$\displaystyle\displaystyle{\hbox{\hskip
44.83275pt\vbox{\hbox{\hskip-44.83273pt\hbox{\hbox{$\displaystyle\displaystyle{A\stackrel{{\scriptstyle
def}}{{=}}P}$}\hskip
20.00003pt\hbox{\hbox{$\displaystyle\displaystyle{X\xhookrightarrow{\pi[\hskip
0.56905pt{\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}i}\hskip
0.56905pt]}P}$}}}}\vbox{}}}\over\hbox{\hskip
16.20425pt\vbox{\vbox{}\hbox{\hskip-16.20425pt\hbox{\hbox{$\displaystyle\displaystyle{X\xhookrightarrow{\pi[\hskip
0.56905pt{\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}i}\hskip
0.56905pt]}A}$}}}}}}$

The set of rules also includes symmetric versions of rules [Par] and [Cho].

Figure 3. $\mathtt{revTPL}$ backward LTS

[Reachable configurations] A configuration $X$ is reachable if there exist a
process $P$ and a derivation $P\xmapsto{}^{*}X$. Basically, a configuration is
reachable if it can be obtained via forward and backward actions from a
standard configuration.

##  3\. Relations with TPL and reversible CCS

We can consider $\mathtt{revTPL}$ as a reversible extension of TPL, but also
as an extension of reversible CCS (in particular CCSK [PU07]) with time.
First, if we consider the forward semantics only, then we have a tight
correspondence with TPL. To show this we define a forgetful map which discards
the history information of a configuration.

[History forgetting map] The _history forgetting map_
$\phi^{\mathtt{h}}:\mathcal{X}\rightarrow\mathcal{P}$ is inductively defined
as follows:

$\begin{array}[]{ll}\phi^{\mathtt{h}}(P)=P&\phi^{\mathtt{h}}(\rho[\hskip
0.56905pt{\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}i}\hskip
0.56905pt].X)=\phi^{\mathtt{h}}(X)\\\\[5.69054pt] \phi^{\mathtt{h}}(\lfloor
X\rfloor[{\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}\underleftarrow{i}}](Y))=\phi^{\mathtt{h}}(X)&\phi^{\mathtt{h}}(\lfloor
X\rfloor[{\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}\underrightarrow{i}}](Y))=\phi^{\mathtt{h}}(Y)\\\\[5.69054pt]
\phi^{\mathtt{h}}(X\parallel
Y)=\phi^{\mathtt{h}}(X)\parallel\phi^{\mathtt{h}}(Y)&\phi^{\mathtt{h}}(X\setminus
a)=\phi^{\mathtt{h}}(X)\setminus a\\\\[5.69054pt]
\lx@intercol\phi^{\mathtt{h}}(X+Y)=\left\\{\begin{array}[]{ll}\phi^{\mathtt{h}}(X)&\text{
if }\neg\mathtt{nact}(X)\wedge\mathtt{nact}(Y)\\\ \phi^{\mathtt{h}}(Y)&\text{
if }\neg\mathtt{nact}(Y)\wedge\mathtt{nact}(X)\\\
\phi^{\mathtt{h}}(X)+\phi^{\mathtt{h}}(Y)&\text{
otherwise}\end{array}\right.\hfil\lx@intercol\end{array}$

The definition above deletes all the information about history from a
configuration $X$, hence it is the identity on standard configuration $P$.
Even more, each configuration is mapped into a standard one. Notice that in a
non-standard timeout, only the chosen branch is taken. In TPL time cannot
decide choices. This is reflected into the definition of
$\phi^{\mathtt{h}}(X+Y)$, where a branch disappears only if the other one did
at least a communication action.

Notably, the restriction of $\phi^{\mathtt{h}}$ to untimed configurations
(namely configurations containing neither timeouts nor $\sigma$ prefixes nor
$\sigma_{\bot}$ prefixes) is a map from CCSK [PU07] to CCS. Following the
notation of Appendix A, we will indicate with $\rightarrow_{\mathtt{t}}$ the
semantics of TPL [HR95], reported in Appendix A.3, and with
$\mapsto_{\mathtt{k}}$ the semantics of CCSK [PU07], reported in Appendix A.2.

######  Proposition 1 (Embedding of TPL).

Let $X$ be a reachable $\mathtt{revTPL}$ configuration:

  1. (1)

if $X\xrightarrow{\pi[\hskip
0.56905pt{\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}i}\hskip
0.56905pt]}Y$ then
$\phi^{\mathtt{h}}(X)\xrightarrow{\pi}_{\mathtt{t}}\phi^{\mathtt{h}}(Y)$;

  2. (2)

if $\phi^{\mathtt{h}}(X)\xrightarrow{\pi}_{\mathtt{t}}Q$ then for any
$i\in\mathcal{K}\setminus\mathtt{keys}(X)$ there is $Y$ such that
$X\xrightarrow{\pi[\hskip
0.56905pt{\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}i}\hskip
0.56905pt]}Y$ with $\phi^{\mathtt{h}}(Y)=Q$.

######  Proof 3.1.

(1):

by induction on the derivation $X\xrightarrow{\pi[\hskip
0.56905pt{\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}i}\hskip
0.56905pt]}Y$, with a case analysis on the last applied rule. We detail a few
sample rules.

If the move is by rule [PAct] then we have $Y=\sigma_{\bot}[\hskip
0.56905pt{\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}i}\hskip
0.56905pt].\alpha.X_{1}$, with $\phi^{\mathtt{h}}(X)=\phi^{\mathtt{h}}(Y)$,
and in TPL we have a corresponding state-preserving move with label $\sigma$
derived using rule Act2 in Figure 12.

In the case of rule [Act], $X=\rho[\hskip
0.56905pt{\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}i}\hskip
0.56905pt].Z$ and $Y=\rho[\hskip
0.56905pt{\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}i}\hskip
0.56905pt].Z^{\prime}$ with $Z\xrightarrow{\pi[\hskip
0.56905pt{\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}j}\hskip
0.56905pt]}Z^{\prime}$. By inductive hypothesis, in TPL
$\phi^{\mathtt{h}}(Z)\xrightarrow{\pi}_{\mathtt{t}}\phi^{\mathtt{h}}(Z^{\prime})$.
Since $\phi^{\mathtt{h}}(X)=\phi^{\mathtt{h}}(Z)$ and
$\phi^{\mathtt{h}}(Y)=\phi^{\mathtt{h}}(Z^{\prime})$ we are done. The cases
for [Const] and [Hide] are similar by induction. The cases for [SynW] and
[ChoW] follow by induction as well.

If the last applied rule is [Cho], then we have that $X=X_{1}+X_{2}$ with
$X_{1}\xrightarrow{\alpha[\hskip
0.56905pt{\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}i}\hskip
0.56905pt]}X^{\prime}_{1}$ and $\mathtt{nact}(X_{2})$. Also,
$Y=X^{\prime}_{1}+X_{2}$ with $X^{\prime}_{1}$ acted. Hence,
$\phi^{\mathtt{h}}(Y)=\phi^{\mathtt{h}}(X^{\prime}_{1}+X_{2})=\phi^{\mathtt{h}}(X^{\prime}_{1})$.
We consider the case $\mathtt{nact}(X_{1})$, the other one is simpler. By
definition, we have that
$\phi^{\mathtt{h}}(X_{1}+X_{2})=\phi^{\mathtt{h}}(X_{1})+\phi^{\mathtt{h}}(X_{2}).$
Since $X_{1}\xrightarrow{\alpha[\hskip
0.56905pt{\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}i}\hskip
0.56905pt]}X^{\prime}_{1}$, by applying the inductive hypothesis we also have
that
$\phi^{\mathtt{h}}(X_{1})\xrightarrow{\alpha}_{\mathtt{t}}\phi^{\mathtt{h}}(X^{\prime}_{1})$.
Also, since the label is not a $\sigma$ action, in TPL we can use rule Sum1 in
Figure 12 that from
$\phi^{\mathtt{h}}(X_{1})\xrightarrow{\alpha}_{\mathtt{t}}\phi^{\mathtt{h}}(X^{\prime}_{1})$
allows one to derive
$\phi^{\mathtt{h}}(X_{1})+\phi^{\mathtt{h}}(X_{2})\xrightarrow{\alpha}\phi^{\mathtt{h}}(X^{\prime}_{1})$,
as desired.

If the last applied rule is [STout] then $\lfloor
X_{1}\rfloor(X_{2})\xrightarrow{\sigma[\hskip
0.56905pt{\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}i}\hskip
0.56905pt]}\lfloor
X_{1}\rfloor[{\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}\underrightarrow{i}}](X_{2})$
with $X_{1}$ and $X_{2}$ standard, and $X_{1}$ that can not perform $\tau$
steps. By inductive hypothesis $\phi^{\mathtt{h}}(X_{1})$ can not perform
$\tau$ steps in TPL, hence in TPL we can use rule THEN2 in Figure 12 to derive
$\phi^{\mathtt{h}}(\lfloor X_{1}\rfloor(X_{2}))=\lfloor
X_{1}\rfloor(X_{2})\xrightarrow{\sigma}_{\mathtt{t}}X_{2}=\phi^{\mathtt{h}}(\lfloor
X_{1}\rfloor[{\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}\underrightarrow{i}}](X_{2}))$
as desired.

(2):

by induction on the definition of $\phi^{\mathtt{h}}(X)$ (structural induction
on $X$). Let us first assume $X$ standard, hence $\phi^{\mathtt{h}}(X)=X$. Let
us consider $X=\alpha.P$. In TPL, $\alpha.P$ can make a state preserving
transition $\sigma$ and the corresponding $\mathtt{revTPL}$ configuration can
match it: $X\xrightarrow{\sigma[\hskip
0.56905pt{\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}i}\hskip
0.56905pt]}\sigma_{\bot}[\hskip
0.56905pt{\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}i}\hskip
0.56905pt].X$, with $\phi^{\mathtt{h}}(\sigma_{\bot}[\hskip
0.56905pt{\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}i}\hskip
0.56905pt].X)=X$. Alternatively, in TPL,
$\alpha.P\xrightarrow{\alpha}_{\mathtt{t}}P$. The thesis follows since
$\alpha.P\xrightarrow{\alpha[\hskip
0.56905pt{\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}i}\hskip
0.56905pt]}\alpha[\hskip
0.56905pt{\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}i}\hskip
0.56905pt].P$ with $\phi^{\mathtt{h}}(\alpha[\hskip
0.56905pt{\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}i}\hskip
0.56905pt].P)=P$. The other cases are similar, but using the induction
hypothesis.

Let us now assume $X$ non standard. The most interesting case is when
$X=X_{1}+X_{2}$. Let us consider $X_{1}$ acted (the case where $X_{2}$ is
acted is symmetric). In this case
$\phi^{\mathtt{h}}(X_{1}+X_{2})=\phi^{\mathtt{h}}(X_{1})$ hence the thesis
follows by inductive hypothesis using rule [ChoW] for $\sigma$ actions and
[Cho] for communication actions. If both $X_{1}$ and $X_{2}$ are not acted,
then
$\phi^{\mathtt{h}}(X_{1}+X_{2})=\phi^{\mathtt{h}}(X_{1})+\phi^{\mathtt{h}}(X_{2})$.
We now have two cases, either $\pi=\sigma$ or $\pi=\alpha$. If $\pi=\sigma$ we
have that by rule SUM3 in Figure 12
$\phi^{\mathtt{h}}(X_{1})\xrightarrow{\sigma}_{\mathtt{t}}Z_{1}$ and
$\phi^{\mathtt{h}}(X_{2})\xrightarrow{\sigma}_{\mathtt{t}}Z_{2}$ allow one to
derive
$\phi^{\mathtt{h}}(X_{1})+\phi^{\mathtt{h}}(X_{2})\xrightarrow{\sigma}_{\mathtt{t}}Z_{1}+Z_{2}$.
By inductive hypotheses we have that there exist $X^{\prime}_{1}$ and
$X^{\prime}_{2}$ such that $X_{1}\xrightarrow{\sigma[\hskip
0.56905pt{\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}i}\hskip
0.56905pt]}X^{\prime}_{1}$ and $X_{2}\xrightarrow{\sigma[\hskip
0.56905pt{\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}i}\hskip
0.56905pt]}X^{\prime}_{2}$ with $\phi^{\mathtt{h}}(X^{\prime}_{1})=Z_{1}$ and
$\phi^{\mathtt{h}}(X^{\prime}_{2})=Z_{2}$. We can then apply rule [ChoW] to
derive $X_{1}+X_{2}\xrightarrow{\sigma[\hskip
0.56905pt{\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}i}\hskip
0.56905pt]}X^{\prime}_{1}+X_{2}^{\prime}$. Since $X^{\prime}_{1}$ and
$X^{\prime}_{2}$ are still not-acted we can conclude by noticing that
$\phi^{\mathtt{h}}(X^{\prime}_{1}+X^{\prime}_{2})=\phi^{\mathtt{h}}(X^{\prime}_{1})+\phi^{\mathtt{h}}(X^{\prime}_{2})=Z_{1}+Z_{2}$.
The case for $\pi=\alpha$ is similar.

We can describe the above correspondence between $\mathtt{revTPL}$ and TPL in
a more abstract way by adapting the notion of (strong) timed bisimulation
[LY97] to relate configurations from two calculi. [Timed bisimulation] A
binary relation $\mathcal{R}$ on $\mathcal{X}\times\mathcal{P}$ is a strong
timed bisimulation between $\mathtt{revTPL}$ and TPL if $(X,P)\in\mathcal{R}$
implies that

  1. (1)

if $X\xrightarrow{\pi[\hskip
0.56905pt{\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}i}\hskip
0.56905pt]}Y$, then there exists $Q$ such that
$P\xrightarrow{\pi}_{\mathtt{t}}Q$ and $(Y,Q)\in\mathcal{R}$;

  2. (2)

if $P\xrightarrow{\pi}_{\mathtt{t}}Q$, then there exist $Y$ and $i$ such that
$X\xrightarrow{\pi[\hskip
0.56905pt{\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}i}\hskip
0.56905pt]}Y$ and $(Y,Q)\in\mathcal{R}$.

The largest strong timed bisimulation is called strong timed equivalence,
denoted $\sim$.

We can now relate $\mathtt{revTPL}$ and TPL as follows:

######  Theorem 2.

For each reachable $\mathtt{revTPL}$ configuration $X$ we have that
$X\sim\phi^{\mathtt{h}}(X)$.

######  Proof 3.2.

It is sufficient to show that the relation
$\mathcal{R}=\\{(X,P)\mid\phi^{\mathtt{h}}(X)=P\\}$ is a strong timed
bisimulation. Let us check the conditions. If $X\xrightarrow{\pi[\hskip
0.56905pt{\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}i}\hskip
0.56905pt]}Y$ then thanks to Proposition 1 we have that
$\phi^{\mathtt{h}}(X)\xrightarrow{\pi}_{\mathtt{t}}\phi^{\mathtt{h}}(Y)$ with
$\phi^{\mathtt{h}}(Y)=Q$, and we have that $(Y,Q)\in\mathcal{R}$. If
$P\xrightarrow{\pi}_{\mathtt{t}}Q$, thanks to Proposition 1 we have that
$X\xrightarrow{\pi[\hskip
0.56905pt{\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}i}\hskip
0.56905pt]}Y$ with $\phi^{\mathtt{h}}(Y)=Q$, and we have that
$(Y,Q)\in\mathcal{R}$, as desired.

Also, TPL is a conservative extension of CCS. This is stated in [HR95], albeit
not formally proved. Hence, we can define a _forgetful_ map which discards all
the temporal operators of a TPL term and get a CCS one. We can obtain a
stronger result and relate $\mathtt{revTPL}$ with CCSK [PU07]. That is, if we
consider the untimed part of $\mathtt{revTPL}$ what we get is a reversible CCS
which is exactly CCSK. To this end, we define a time forgetting map
$\phi^{\mathtt{t}}$. We denote with $\mathcal{X}^{k}$ the set of untimed
reversible configurations of $\mathtt{revTPL}$, which coincides with the set
of all CCSK configurations (which is defined in Appendix A.2). The set
inclusion $\mathcal{X}^{k}\subset\mathcal{X}$ holds.

[Time forgetting map] The _time forgetting map_
$\phi^{\mathtt{t}}:\mathcal{X}\rightarrow\mathcal{X}^{k}$ is inductively
defined as follows:

$\begin{array}[]{lll}\phi^{\mathtt{t}}(\mathbf{0})=\mathbf{0}&&\phi^{\mathtt{t}}(A)=A\\\
\phi^{\mathtt{t}}(\alpha.P)=\alpha.\phi^{\mathtt{t}}(P)&&\phi^{\mathtt{t}}(\alpha[\hskip
0.56905pt{\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}i}\hskip
0.56905pt].X)=\alpha[\hskip
0.56905pt{\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}i}\hskip
0.56905pt].\phi^{\mathtt{t}}(X)\\\
\phi^{\mathtt{t}}(X+Y)=\phi^{\mathtt{t}}(X)+\phi^{\mathtt{t}}(Y)&&\phi^{\mathtt{t}}(X\parallel
Y)=\phi^{\mathtt{t}}(X)\parallel\phi^{\mathtt{t}}(Y)\\\
\phi^{\mathtt{t}}(X\setminus a)=\phi^{\mathtt{t}}(X)\setminus
a&&\phi^{\mathtt{t}}(\lfloor
X\rfloor(Y){})=\phi^{\mathtt{t}}(X)+\phi^{\mathtt{t}}(Y)\\\
\phi^{\mathtt{t}}(\sigma.P)=\phi^{\mathtt{t}}(P)&&\phi^{\mathtt{t}}(\sigma[\hskip
0.56905pt{\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}i}\hskip
0.56905pt].X)=\phi^{\mathtt{t}}(\sigma_{\bot}[\hskip
0.56905pt{\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}i}\hskip
0.56905pt].X)=\phi^{\mathtt{t}}(X)\\\ \phi^{\mathtt{t}}(\lfloor
X\rfloor[{\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}\underleftarrow{i}}](Y))=\phi^{\mathtt{t}}(X)+\phi^{\mathtt{t}}(Y)&&\phi^{\mathtt{t}}(\lfloor
X\rfloor[{\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}\underrightarrow{i}}](Y))=\phi^{\mathtt{t}}(X)+\phi^{\mathtt{t}}(Y)\end{array}$

Notably, the restriction of $\phi^{\mathtt{t}}$ to standard configurations is
a map from TPL to CCS.

The most interesting aspect in the definition above is that the timeout
operator $\lfloor X\rfloor(Y)$ is rendered as a sum. This also happens for the
decorated configurations $\lfloor
X\rfloor[{\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}\underleftarrow{i}}](Y)$
and $\lfloor
X\rfloor[{\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}\underrightarrow{i}}](Y)$.
We will further discuss this design decision after Proposition 3. Also, since
we are relating a timed semantics with an untimed one (CCSK), the $\sigma$
actions performed by the timed semantics are not reflected in CCSK.

######  Proposition 3 (Embedding of CCSK [PU07]).

Let $X$ be a reachable $\mathtt{revTPL}$ configuration. We have:

  1. (1)

if $X\xrightarrow{\alpha[\hskip
0.56905pt{\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}i}\hskip
0.56905pt]}Y$ then $\phi^{\mathtt{t}}(X)\xrightarrow{\alpha[\hskip
0.56905pt{\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}i}\hskip
0.56905pt]}_{\mathtt{k}}\phi^{\mathtt{t}}(Y)$;

  2. (2)

if $X\xhookrightarrow{\alpha[\hskip
0.56905pt{\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}i}\hskip
0.56905pt]}Y$ then $\phi^{\mathtt{t}}(X)\xhookrightarrow{\alpha[\hskip
0.56905pt{\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}i}\hskip
0.56905pt]}_{\mathtt{k}}\phi^{\mathtt{t}}(Y)$;

  3. (3)

if $X\xmapsto{\sigma[\hskip
0.56905pt{\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}i}\hskip
0.56905pt]}Y$ then $\phi^{\mathtt{t}}(X)=\phi^{\mathtt{t}}(Y)$.

######  Proof 3.3.

(1):

by induction on the derivation $X\xrightarrow{\alpha[\hskip
0.56905pt{\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}i}\hskip
0.56905pt]}Y$, with a case analysis on the last applied rule. The proof goes
along the lines of the proof of Proposition 1, using the rules reported in
Figures 8 and 9 in Appendix A.2.

(2):

similar to the case above, using $X\xhookrightarrow{\alpha[\hskip
0.56905pt{\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}i}\hskip
0.56905pt]}Y$ instead of $X\xrightarrow{\alpha[\hskip
0.56905pt{\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}i}\hskip
0.56905pt]}Y$.

(3):

by induction on the derivation of $X\xrightarrow{\sigma[\hskip
0.56905pt{\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}i}\hskip
0.56905pt]}Y$ (the case of backward transitions is analogous), with a case
analysis on the last applied rule. Basic cases are (i) rules [Pact] and
[Idle], creating a $\sigma_{\bot}$, (ii) $\sigma$ prefixes, and (iii)
timeouts. In case (i) we have $Y=\sigma_{\bot}[\hskip
0.56905pt{\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}i}\hskip
0.56905pt].X$, hence $\phi^{\mathtt{t}}(Y)=\phi^{\mathtt{t}}(X)$. In case (ii)
we have $\sigma.P\xrightarrow{\sigma[\hskip
0.56905pt{\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}i}\hskip
0.56905pt]}\sigma[\hskip
0.56905pt{\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}i}\hskip
0.56905pt].P$, hence
$\phi^{\mathtt{t}}(\sigma.P)=P=\phi^{\mathtt{t}}(\sigma[\hskip
0.56905pt{\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}i}\hskip
0.56905pt].P)$. In case (iii) we have $\lfloor
X_{1}\rfloor(X_{2})\xrightarrow{\sigma[\hskip
0.56905pt{\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}i}\hskip
0.56905pt]}\lfloor
X_{1}\rfloor[{\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}\underrightarrow{i}}](X_{2})$
with $\phi^{\mathtt{t}}(\lfloor
X_{1}\rfloor(X_{2}))=\phi^{\mathtt{t}}(X_{1})+\phi^{\mathtt{t}}(X_{2})=\phi^{\mathtt{t}}(\lfloor
X_{1}\rfloor[{\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}\underrightarrow{i}}](X_{2}))$
as desired. Inductive cases follow by inductive hypothesis.

Notably, it is not always the case that transitions of the underlying untimed
configuration can be matched in a timed setting. Think, e.g., of the Erlang
program in Example 1 (and its formalisation in Section 1.1), for a
counterexample. Indeed, in the example, the communication between the two
processes A and B is allowed in the underlying untimed model, but ruled out by
incompatible timing constraints. Also, let us consider the simple process
$X=\lfloor a\rfloor(b)$ and its untimed version $\phi^{\mathtt{t}}(X)=a+b$.
The untimed process can execute the right branch as follows

$\phi^{\mathtt{t}}(X)\xrightarrow{b[\hskip
0.56905pt{\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}i}\hskip
0.56905pt]}a+b[\hskip
0.56905pt{\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}i}\hskip
0.56905pt]$

To match this action, $X$ has first to perform a time action and only
afterwards it can take the $b$ action, as follows:

$X\xrightarrow{\sigma[\hskip
0.56905pt{\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}j}\hskip
0.56905pt]}\lfloor
a\rfloor[{\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}\underrightarrow{j}}](b)\xrightarrow{b[\hskip
0.56905pt{\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}i}\hskip
0.56905pt]}\lfloor
a\rfloor[{\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}\underrightarrow{j}}](b[\hskip
0.56905pt{\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}i}\hskip
0.56905pt])$

Moreover, there are also cases where actions cannot be matched, not even after
time actions. Indeed, the timeout operator $\lfloor P\rfloor(Q)$ acts as a
choice with left priority. For example, let us consider the process
$X=\lfloor(a\parallel\overline{a})\rfloor(b)$. We have that
$\phi^{\mathtt{t}}(X)$ can perform the $b$ action as follows

$\phi^{\mathtt{t}}(X)=(a\parallel\overline{a})+b\xrightarrow{b[\hskip
0.56905pt{\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}i}\hskip
0.56905pt]}(a\parallel\overline{a})+b[\hskip
0.56905pt{\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}i}\hskip
0.56905pt]$

but this action can never be matched by $X$, as $\mathtt{revTPL}$ maximal
progress forces the internal synchronisation over time passage. Hence we can
only apply rule STout in Figure 2:

$\lfloor(a\parallel\overline{a})\rfloor(b)\xrightarrow{\tau[\hskip
0.56905pt{\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}i}\hskip
0.56905pt]}\lfloor a[\hskip
0.56905pt{\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}i}\hskip
0.56905pt]\parallel\overline{a}[\hskip
0.56905pt{\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}i}\hskip
0.56905pt]\rfloor[{\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}\underleftarrow{i}}](b)$

and the resulting configuration cannot execute $b$.

Due to the examples above, we cannot characterise the relation between $X$ and
$\phi^{\mathtt{t}}(X)$ as a bisimulation, as for $\phi^{\mathtt{h}}$, but we
can only prove that $\phi^{\mathtt{t}}(X)$ simulates $X$. As before, we need
to modify notions of simulation for reversible configurations from the
literature (e..g, [NMV90, LP21]) to relate configurations from two calculi,
and to keep time into account.

[Back and forward simulation] A binary relation $\mathcal{R}$ on
$\mathcal{X}\times\mathcal{X}^{k}$ is a back and forward simulation if
$(X,R)\in\mathcal{R}$ implies that

  1. (1)

if $X\xrightarrow{\alpha[\hskip
0.56905pt{\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}i}\hskip
0.56905pt]}Y$, then there exists $S$ such that $R\xrightarrow{\alpha[\hskip
0.56905pt{\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}i}\hskip
0.56905pt]}_{\mathtt{k}}S$ and $(Y,S)\in\mathcal{R}$;

  2. (2)

if $X\xhookrightarrow{\alpha[\hskip
0.56905pt{\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}i}\hskip
0.56905pt]}Y$, then there exists $S$ such that
$R\xhookrightarrow{\alpha[\hskip
0.56905pt{\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}i}\hskip
0.56905pt]}_{\mathtt{k}}S$ and $(Y,S)\in\mathcal{R}$;

  3. (3)

if $X\xmapsto{\sigma[\hskip
0.56905pt{\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}i}\hskip
0.56905pt]}Y$, then $(Y,R)\in\mathcal{R}$.

The largest back and forward simulation is denoted by $\precsim$.

######  Theorem 4.

For each reachable $\mathtt{revTPL}$ configuration $X$ we have that
$X\precsim\phi^{\mathtt{t}}(X)$.

######  Proof 3.4.

It is sufficient to show that the relation
$\mathcal{R}=\\{(X,R)\mid\phi^{\mathtt{t}}(X)=R\\}$ is a back and forward
simulation. It is easy to check the conditions of Definition 3.3 using
Proposition 3.

$\textstyle{\mathtt{revTPL}\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\phi^{\mathtt{t}}}$$\scriptstyle{Prop.~{}\ref{prop:rtpl_to_ccsk}}$$\scriptstyle{\phi^{\mathtt{h}}}$$\scriptstyle{Prop.~{}\ref{prop:totpl}}$$\textstyle{CCSK\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\phi^{\mathtt{h}}}$$\scriptstyle{Prop.~{}\ref{prop:totpl}}$$\textstyle{TPL\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\phi^{\mathtt{t}}}$$\scriptstyle{Prop.~{}\ref{prop:rtpl_to_ccsk}}$$\textstyle{CCS}$
Figure 4. Forgetting maps.

Figure 4 summarises our results: if we remove the timed behaviour from a
$\mathtt{revTPL}$ configuration we get a CCSK term, with the same behaviour
apart for timed aspects, thanks to Proposition 3. On the other side, if from
$\mathtt{revTPL}$ we remove history information we get a TPL term (matching
its forward behaviour thanks to Proposition 1). Note that the same forgetful
maps (and properties) justify the arrows in the bottom part of the diagram, as
discussed above. This is in line with Theorem 5.21 of [PU07], showing that by
removing reversibility and history information from CCSK we get CCS. Notably
the two forgetting maps commute.

######  Proposition 5.

For each reachable $\mathtt{revTPL}$ configuration $X$ we have
$\phi^{\mathtt{h}}(\phi^{\mathtt{t}}(X))=\phi^{\mathtt{t}}(\phi^{\mathtt{h}}(X))$.

######  Proof 3.5.

By structural induction on $X$.

##  4\. Reversibility in $\mathtt{revTPL}$

In a fully reversible calculus any computation can be undone. This is a
fundamental property of reversibility [DK04, LPU20], called the Loop Lemma,
and $\mathtt{revTPL}$ enjoys it. Formally:

######  Lemma 6 (Loop Lemma).

If $X$ is a reachable $\mathtt{revTPL}$ configuration, then
$X\xrightarrow{\pi[\hskip
0.56905pt{\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}i}\hskip
0.56905pt]}X^{\prime}\iff X^{\prime}\xhookrightarrow{\pi[\hskip
0.56905pt{\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}i}\hskip
0.56905pt]}X$

######  Proof 4.1.

We have two directions. The forward one trivially holds, since for each
forward rule of Figure 2 there exists a symmetric one backwards in Figure 3.
The backward case requires more attention, and we proceed by induction on
$X\xhookrightarrow{\pi[\hskip
0.56905pt{\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}i}\hskip
0.56905pt]}Y$, with a case analysis on the last applied rule. We can further
distinguish the cases according to whether $\pi=\sigma$, $\pi=\tau$ or
$\pi=\alpha$. We will just consider one instance of each case, the others are
similar.

$\pi=\sigma$:

using rule [ChoW] we have that $X=X_{1}+X_{2}$,
$X_{1}\xhookrightarrow{\sigma{[\hskip
0.56905pt{\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}i}\hskip
0.56905pt]}}X^{\prime}_{1}$, $X_{2}\xhookrightarrow{\sigma{[\hskip
0.56905pt{\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}i}\hskip
0.56905pt]}}X^{\prime}_{2}$. Since by reachability of $X$ we have the
reachability of $X_{1}$ and $X_{2}$, by inductive hypothesis we have that
$X^{\prime}_{1}\xrightarrow{\sigma{[\hskip
0.56905pt{\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}i}\hskip
0.56905pt]}}X_{1}$ and $X^{\prime}_{2}\xrightarrow{\sigma{[\hskip
0.56905pt{\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}i}\hskip
0.56905pt]}}X_{2}$, so we can apply the forward version of rule [ChoW], as
desired.

$\pi=\tau$:

using rule [Syn] by hypothesis we have that $X=X_{1}\parallel X_{2}$ with
$X_{1}\xhookrightarrow{\alpha[\hskip
0.56905pt{\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}i}\hskip
0.56905pt]}X^{\prime}_{1}$ and $X_{2}\xhookrightarrow{\overline{\alpha}[\hskip
0.56905pt{\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}i}\hskip
0.56905pt]}X^{\prime}_{2}$. By applying the inductive hypothesis we get
$X^{\prime}_{1}\xrightarrow{\alpha[\hskip
0.56905pt{\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}i}\hskip
0.56905pt]}X_{1}$ and $X^{\prime}_{2}\xrightarrow{\overline{\alpha}[\hskip
0.56905pt{\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}i}\hskip
0.56905pt]}X_{2}$, and we can derive $X^{\prime}_{1}\parallel
X^{\prime}_{2}\xrightarrow{\tau[\hskip
0.56905pt{\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}i}\hskip
0.56905pt]}X_{1}\parallel X_{2}$, as desired.

$\pi=\alpha$:

using rule [Cho] by hypothesis we have that $X=X_{1}+X_{2}$,
$X_{1}\xhookrightarrow{\alpha[\hskip
0.56905pt{\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}i}\hskip
0.56905pt]}X^{\prime}_{1}$ and $\mathtt{nact}(X_{2})$. By applying the
inductive hypothesis we have that $X^{\prime}_{1}\xrightarrow{\alpha[\hskip
0.56905pt{\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}i}\hskip
0.56905pt]}X^{\prime}_{1}$ and we can derive
$X^{\prime}_{1}+X_{2}\xrightarrow{\alpha[\hskip
0.56905pt{\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}i}\hskip
0.56905pt]}X_{1}+X_{2}$ as desired.

Another fundamental property of causal-consistent reversibility is the so-
called causal-consitency [DK04, LPU20], which essentially states that we store
the correct amount of causal information. In order to discuss it, we now
borrow some definitions from [DK04]. We use $t,t^{\prime},s,s^{\prime}$ to
range over transitions. In a transition $t:X\xmapsto{\pi[\hskip
0.56905pt{\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}i}\hskip
0.56905pt]}Y$ we call $X$ the _source_ of the transition, and $Y$ the _target_
of the transition. Two transitions are said to be _coinitial_ if they have the
same source, and _cofinal_ if they have the same target. Given a transition
$t$, we indicate with $\underline{t}$ its reverse, that is if
$t:X\xrightarrow{\pi[\hskip
0.56905pt{\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}i}\hskip
0.56905pt]}Y$ (resp., $t:X\xhookrightarrow{\pi[\hskip
0.56905pt{\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}i}\hskip
0.56905pt]}Y$) then $\underline{t}:Y\xhookrightarrow{\pi[\hskip
0.56905pt{\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}i}\hskip
0.56905pt]}X$ (resp., $\underline{t}:Y\xrightarrow{\pi[\hskip
0.56905pt{\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}i}\hskip
0.56905pt]}X$). The notions of source, target, coinitiality, and cofinality
naturally extend to paths. We let $\chi,\omega$ to range over sequences of
transitions, which we call _paths_ , and with $\epsilon_{X}$ we indicate the
empty sequence starting and ending at $X$. We denote as $|\chi|$ the number of
transitions in path $\chi$. Moreover, we indicate with $\chi_{1}\chi_{2}$ the
composition of the two paths $\chi_{1}$ and $\chi_{2}$ when they are
composable, that is when the target of $\chi_{1}$ coincides with the source of
$\chi_{2}$.

[Causal Equivalence] Let $\asymp$ be the smallest equivalence on paths closed
under composition and satisfying:

  1. (1)

if $t:X\xmapsto{\pi_{1}[\hskip
0.56905pt{\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}i}\hskip
0.56905pt]}Y_{1}$ and $s:X\xmapsto{\pi_{2}[\hskip
0.56905pt{\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}j}\hskip
0.56905pt]}Y_{2}$ are independent, and
$s^{\prime}:Y_{1}\xmapsto{\pi_{2}[\hskip
0.56905pt{\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}j}\hskip
0.56905pt]}Z$, $t^{\prime}:Y_{2}\xmapsto{\pi_{1}[\hskip
0.56905pt{\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}i}\hskip
0.56905pt]}Z$ then $ts^{\prime}\asymp st^{\prime}$;

  2. (2)

$t\underline{t}\asymp\epsilon$ and $\underline{t}t\asymp\epsilon$

Intuitively, paths are causal equivalent if they differ only for swapping
independent transitions (we will discuss independence below) and for adding
do-undo or undo-redo pairs of transitions.

[Causal Consistency (CC)] An LTS is causal consistent if for any coinitial and
cofinal paths $\chi$ and $\omega$ we have $\chi\asymp\omega$. Intuitively, if
coinitial paths are cofinal then they have the same causal information and can
reverse in the same ways: we want only causal equivalent paths to reverse in
the same ways.

###  4.1. Independence

We now define a notion of independence between $\mathtt{revTPL}$ coinitial
transitions, based on a causality preorder (inspired by [LP21]) on keys.
Intuitively, independent transitions can be executed in any order (we will
formalise this as Property 1), while transitions which are not independent
represent a choice: either one is executed, or the other.

[Partial order on keys] The function $\mathtt{po}(\cdot):\mathcal{X}\mapsto
2^{(\mathcal{K}\times\mathcal{K})}$ is inductively defined below. It takes a
configuration $X\in\mathcal{X}$ and computes a set of ordered pairs of keys
which is the set of causal relations among the keys in $X$.

$\begin{array}[]{l}\mathtt{po}(P)=\emptyset\qquad\qquad\mathtt{po}(X\setminus
a)=\mathtt{po}(X)\\\ \mathtt{po}(X\parallel
Y)=\mathtt{po}(X+Y)=\mathtt{po}(\lfloor
X\rfloor(Y))=\mathtt{po}(X)\cup\mathtt{po}(Y)\\\ \mathtt{po}(\rho[\hskip
0.56905pt{\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}i}\hskip
0.56905pt].X)=\mathtt{po}(\lfloor
X\rfloor[{\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}\underleftarrow{i}}](Y))=\mathtt{po}(\lfloor
Y\rfloor[{\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}\underrightarrow{i}}](X))=\\{i<j\mid
j\in\mathtt{keys}(X)\\}\cup\mathtt{po}(X)\end{array}$

The partial order $\leq_{X}$ on $\mathtt{keys}(X)$ is the reflexive and
transitive closure of $\mathtt{po}(X)$. Let us note that function
$\mathtt{po}$ computes a partial order relation, namely a set of pairs
$(i,j)$, denoted $i<j$ to stress that they form a partial order. In
particular, $i<j$ means that key $i$ causes key $j$. This takes into account
both structural causality given by the structure of a configuration (e.g., a
prefix causes its continuation) and causality raising from synchronisation and
time, since synchronising actions and time actions corresponding to the same
point in time have the same key.

######  Example 4.2.

Let us compute the partial order on keys in

$\lfloor
a\rfloor[{\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}\underrightarrow{i}}](b[\hskip
0.56905pt{\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}j}\hskip
0.56905pt].P)\parallel\sigma_{\bot}[\hskip
0.56905pt{\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}i}\hskip
0.56905pt].c[\hskip
0.56905pt{\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}k}\hskip
0.56905pt].d[\hskip
0.56905pt{\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}w}\hskip
0.56905pt].Q\parallel\sigma_{\bot}[\hskip
0.56905pt{\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}i}\hskip
0.56905pt].\overline{c}[\hskip
0.56905pt{\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}k}\hskip
0.56905pt].R$

We have:

$\begin{array}[]{llll}\mathtt{po}(\lfloor
a\rfloor[{\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}\underrightarrow{i}}](b[\hskip
0.56905pt{\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}j}\hskip
0.56905pt].P))&=\\{i<j\\}\cup\mathtt{po}(P)=\\{i<j\\}\cup\emptyset=\\{i<j\\}\\\
\mathtt{po}(\sigma_{\bot}[\hskip
0.56905pt{\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}i}\hskip
0.56905pt].c[\hskip
0.56905pt{\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}k}\hskip
0.56905pt].d[\hskip
0.56905pt{\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}w}\hskip
0.56905pt].Q)&=\\{i<k\\}\cup\\{i<w\\}\cup\mathtt{po}(c[\hskip
0.56905pt{\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}k}\hskip
0.56905pt].d[\hskip
0.56905pt{\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}w}\hskip
0.56905pt].Q)\\\ &=\\{i<k\\}\cup\\{i<w\\}\cup\\{k<w\\}\cup\mathtt{po}(d[\hskip
0.56905pt{\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}w}\hskip
0.56905pt].Q)\\\
&=\\{i<k\\}\cup\\{i<w\\}\cup\\{k<w\\}\cup\emptyset\cup\mathtt{po}(Q)\\\
&=\\{i<k\\}\cup\\{i<w\\}\cup\\{k<w\\}\\\ \mathtt{po}(\sigma_{\bot}[\hskip
0.56905pt{\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}i}\hskip
0.56905pt].\overline{c}[\hskip
0.56905pt{\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}k}\hskip
0.56905pt].R)&=\\{i<k\\}\cup\mathtt{po}(R)=\\{i<k\\}\end{array}$

and hence, looking at the parallel composition:

$\begin{array}[]{l}\mathtt{po}(\lfloor
a\rfloor[{\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}\underrightarrow{i}}](b[\hskip
0.56905pt{\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}j}\hskip
0.56905pt].P)\parallel\sigma_{\bot}[\hskip
0.56905pt{\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}i}\hskip
0.56905pt].c[\hskip
0.56905pt{\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}k}\hskip
0.56905pt].d[\hskip
0.56905pt{\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}w}\hskip
0.56905pt].Q\parallel\sigma_{\bot}[\hskip
0.56905pt{\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}i}\hskip
0.56905pt].\overline{c}[\hskip
0.56905pt{\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}k}\hskip
0.56905pt].R)=\\\
\\{i<j\\}\cup\\{i<k\\}\cup\\{i<w\\}\cup\\{k<w\\}\cup\\{i<k\\}=\\{i<j,\,i<k,\,i<w,\,k<w\\}\end{array}$

$\diamond$

We also need to understand whether two forward communication transitions are
in conflict since either they involve a same prefix or they involve different
branches of a choice.

[Forward communication conflict] Two forward communication transitions
$t_{1}:X\xrightarrow{\alpha_{1}[\hskip
0.56905pt{\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}i}\hskip
0.56905pt]}Y$ and $t_{2}:X\xrightarrow{\alpha_{2}[\hskip
0.56905pt{\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}j}\hskip
0.56905pt]}Z$ with $i\neq j$ are in forward communication conflict iff the
$\mathtt{fcc}(Y,Z)$ predicate defined below holds:

$\begin{array}[]{lcl}\mathtt{fcc}(\alpha[\hskip
0.56905pt{\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}i}\hskip
0.56905pt].P,\alpha[\hskip
0.56905pt{\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}j}\hskip
0.56905pt].P)&=&True\\\ \mathtt{fcc}(P,P)&=&False\\\
\mathtt{fcc}(Y_{1}\parallel Y_{2},Z_{1}\parallel
Z_{2})&=&\mathtt{fcc}(Y_{1},Z_{2})\lor\mathtt{fcc}(Y_{2},Z_{2})\\\
\mathtt{fcc}(Y_{1}+Y_{2},Z_{1}+Z_{2})&=&(Y_{1}\neq Z_{1}\land Y_{2}\neq
Z_{2})\lor\mathtt{fcc}(Y_{1},Z_{1})\lor\mathtt{fcc}(Y_{2},Z_{2})\\\
\mathtt{fcc}(Y_{1}\setminus a,Z_{1}\setminus a)&=&\mathtt{fcc}(Y_{1},Z_{1})\\\
\mathtt{fcc}(\rho[\hskip
0.56905pt{\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}i}\hskip
0.56905pt].Y_{1},\rho[\hskip
0.56905pt{\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}i}\hskip
0.56905pt].Z_{1})&=&\mathtt{fcc}(Y_{1},Z_{1})\\\ \mathtt{fcc}(\lfloor
Y_{1}\rfloor[{\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}\underleftarrow{i}}](Y_{2}),\lfloor
Z_{1}\rfloor[{\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}\underleftarrow{j}}](Z_{2}))&=&\mathtt{fcc}(Y_{1},Z_{1})\\\
\mathtt{fcc}(\lfloor
Y_{1}\rfloor[{\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}\underleftarrow{i}}](Y_{2}),\lfloor
Z_{1}\rfloor[{\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}\underleftarrow{i}}](Z_{2}))&=&\mathtt{fcc}(Y_{1},Z_{1})\\\
\mathtt{fcc}(\lfloor
Y_{1}\rfloor[{\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}\underrightarrow{i}}](Y_{2}),\lfloor
Z_{1}\rfloor[{\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}\underrightarrow{i}}](Z_{2}))&=&\mathtt{fcc}(Y_{2},Z_{2})\\\
\end{array}$

For simplicity, the $\mathtt{fcc}$ predicate above is defined only for pairs
of configurations which may arise from a same configuration. Notice that in
the clause for choice, the only way for the two branches to be pairwise
different, is that $Y$ has chosen one of them, and $Z$ the other. In this case
the two actions are in conflict. However, in this case $\mathtt{fcc}$ may not
be defined on the components. To avoid this issue, we consider the $\lor$
operator to be a short circuit operator.

######  Example 4.3.

Let us consider the configuration $X_{1}=a[\hskip
0.56905pt{\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}i}\hskip
0.56905pt].b.P$ and the two transitions

  * •

$t_{1}:X_{1}\xrightarrow{b[\hskip
0.56905pt{\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}j}\hskip
0.56905pt]}a[\hskip
0.56905pt{\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}i}\hskip
0.56905pt].b[\hskip
0.56905pt{\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}j}\hskip
0.56905pt].P=Y_{1}$ and

  * •

$t_{2}:X_{1}\xrightarrow{b[\hskip
0.56905pt{\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}z}\hskip
0.56905pt]}a[\hskip
0.56905pt{\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}i}\hskip
0.56905pt].b[\hskip
0.56905pt{\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}z}\hskip
0.56905pt].P=Z_{1}$.

We have that

$\displaystyle\mathtt{fcc}(a[\hskip
0.56905pt{\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}i}\hskip
0.56905pt].b[\hskip
0.56905pt{\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}j}\hskip
0.56905pt].P,a[\hskip
0.56905pt{\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}i}\hskip
0.56905pt].b[\hskip
0.56905pt{\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}z}\hskip
0.56905pt].P)=\mathtt{fcc}(b[\hskip
0.56905pt{\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}j}\hskip
0.56905pt].P,b[\hskip
0.56905pt{\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}z}\hskip
0.56905pt].P)=True$

Let us consider the configuration $X_{2}=\lfloor
a.\mathbf{0}\rfloor[{\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}\underrightarrow{i}}](b[\hskip
0.56905pt{\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}j}\hskip
0.56905pt].(a.P+b.Q))$ and the two transitions

  * •

$t_{3}:X_{2}\xrightarrow{a[\hskip
0.56905pt{\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}z}\hskip
0.56905pt]}\lfloor
a.\mathbf{0}\rfloor[{\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}\underrightarrow{i}}](b[\hskip
0.56905pt{\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}j}\hskip
0.56905pt].(a[\hskip
0.56905pt{\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}z}\hskip
0.56905pt].P+b.Q))=Y_{2}$ and

  * •

$t_{4}:X_{2}\xrightarrow{a[\hskip
0.56905pt{\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}w}\hskip
0.56905pt]}\lfloor
a.\mathbf{0}\rfloor[{\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}\underrightarrow{i}}](b[\hskip
0.56905pt{\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}j}\hskip
0.56905pt].(a.P+b[\hskip
0.56905pt{\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}w}\hskip
0.56905pt].Q))=Z_{2}$.

We have that

$\displaystyle\mathtt{fcc}\big{(}\lfloor
a.\mathbf{0}\rfloor[{\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}\underrightarrow{i}}](b[\hskip
0.56905pt{\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}j}\hskip
0.56905pt].(a[\hskip
0.56905pt{\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}z}\hskip
0.56905pt].P+b.Q)),\lfloor
a.\mathbf{0}\rfloor[{\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}\underrightarrow{i}}](b[\hskip
0.56905pt{\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}j}\hskip
0.56905pt].(a.P+b[\hskip
0.56905pt{\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}w}\hskip
0.56905pt].Q))\big{)}=$ $\displaystyle\mathtt{fcc}\big{(}b[\hskip
0.56905pt{\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}j}\hskip
0.56905pt].(a[\hskip
0.56905pt{\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}z}\hskip
0.56905pt].P+b.Q),b[\hskip
0.56905pt{\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}j}\hskip
0.56905pt].(a.P+b[\hskip
0.56905pt{\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}w}\hskip
0.56905pt].Q)\big{)}=\mathtt{fcc}\big{(}a[\hskip
0.56905pt{\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}z}\hskip
0.56905pt].P+b.Q,a.P+b[\hskip
0.56905pt{\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}w}\hskip
0.56905pt].Q\big{)}=True$

$\diamond$

######  Lemma 7.

Function $\mathtt{fcc}$ above is total for each $Y$ and $Z$ obtained via
communication actions from a common $X$.

######  Proof 4.4.

We proceed by structural induction on $X$, with a case analysis on the rules
used to derive the two transitions.

$X=\pi.P$:

the only possibility here is that the prefix is executed, with two different
keys, this case is covered by the first clause;

$X=\lfloor P\rfloor(Q)$:

here the only possibility is that the first component is executed, this case
is covered by the first clause for timeout;

$X=X_{1}+X_{2}$:

this case is covered by the fourth clause;

$X=X_{1}\parallel X_{2}$:

this case is covered by the third clause;

$X=X_{1}\setminus a$:

this case is covered by the fifth clause;

$X=A$:

constant $A$ has a definition $A\stackrel{{\scriptstyle def}}{{=}}P$, hence
the proof for $P$ applies. Note that in this case termination by structural
induction is not granted, but termination is ensured anyway since recursion is
guarded;

$X=\mathbf{0}$:

since $X$ cannot take any communication action, this case never applies;

$X=\rho[\hskip
0.56905pt{\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}i}\hskip
0.56905pt].X_{1}$:

this case is covered by the sixth clause;

$X=\lfloor
X_{1}\rfloor[{\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}\underleftarrow{i}}](X_{2})$:

this case is covered by the one but last clause;

$X=\lfloor
X_{1}\rfloor[{\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}\underrightarrow{i}}](X_{2})$:

this case is covered by the last clause.

We now define a notion of conflict, and independence as its negation.

[Conflict and independence] Given a reachable $\mathtt{revTPL}$ configuration
$X$, two coinititial transitions $t:X\xmapsto{\pi_{1}[\hskip
0.56905pt{\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}i}\hskip
0.56905pt]}Y$ and $s:X\xmapsto{\pi_{2}[\hskip
0.56905pt{\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}j}\hskip
0.56905pt]}Z$ are conflicting, if and only if one of the following conditions
holds:

  1. (1)

$t:X\xrightarrow{\sigma[\hskip
0.56905pt{\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}i}\hskip
0.56905pt]}Y$ and $s:X\xrightarrow{\alpha[\hskip
0.56905pt{\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}j}\hskip
0.56905pt]}Z$ or vice versa;

  2. (2)

$t:X\xrightarrow{\pi_{1}[\hskip
0.56905pt{\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}i}\hskip
0.56905pt]}Y$ and $s:X\xrightarrow{\pi_{2}[\hskip
0.56905pt{\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}j}\hskip
0.56905pt]}Z$ are in forward communication conflict;

  3. (3)

$t:X\xrightarrow{\pi_{1}[\hskip
0.56905pt{\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}i}\hskip
0.56905pt]}Y$ and $s:X\xhookrightarrow{\pi_{2}[\hskip
0.56905pt{\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}j}\hskip
0.56905pt]}Z$ with
${\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}j}\leq_{Y}{\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}i}$
or vice versa;

  4. (4)

$t:X\xrightarrow{\pi_{1}[\hskip
0.56905pt{\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}i}\hskip
0.56905pt]}Y$ and $s:X\xrightarrow{\pi_{2}[\hskip
0.56905pt{\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}j}\hskip
0.56905pt]}Z$ with
${\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}i}={\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}j}$.

Transitions $t$ and $s$ are _independent_ , written $t\,\mathcal{I}\,s$, if
they are not conflicting. Note that the conflict relation is reflexive and
symmetric, hence independence is irreflexive and symmetric. The first clause
of Definition 4.4 tells us that a delay cannot be swapped with a communication
action. Consider configuration $\lfloor b.\mathbf{0}\rfloor(\mathbf{0})$:

Transitions $\sigma[\hskip
0.56905pt{\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}i}\hskip
0.56905pt]$ and $b[\hskip
0.56905pt{\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}j}\hskip
0.56905pt]$ are in conflict: they cannot be swapped since action $b$ is no
longer possible after action $\sigma$, and vice versa.

The second case of Definition 4.4 forbids either a same prefix or prefixes in
different branches of a same choice operator to be consumed by the two
transitions. For example let us consider the configuration
$a.\mathbf{0}\parallel\overline{a}.\mathbf{0}$. The left configuration could
execute an action $a[\hskip
0.56905pt{\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}i}\hskip
0.56905pt]$ while the entire configuration could synchronise by doing a
$\tau[\hskip
0.56905pt{\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}j}\hskip
0.56905pt]$, as depicted below:

It is clear, from the example above, that the two actions cannot commute.

Another example of conflicting transitions captured by case 2 of Definition
4.4 is when transitions consume prefixes in different branches of a same
choice operator. For example, let us consider the configuration
$a.\mathbf{0}+b.\mathbf{0}$. The left branch can do an action $a[\hskip
0.56905pt{\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}i}\hskip
0.56905pt]$ while the right one an action $b[\hskip
0.56905pt{\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}j}\hskip
0.56905pt]$, as follows:

and again it is clear that these two transitions cannot commute.

The third clause of Definition 4.4 dictates that two transitions are in
conflict when a reverse step eliminates some causes of a forward step. For
example, the configuration $a[\hskip
0.56905pt{\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}j}\hskip
0.56905pt].b.\mathbf{0}$ can do a forward step with label $b[\hskip
0.56905pt{\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}i}\hskip
0.56905pt]$ going to $a[\hskip
0.56905pt{\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}j}\hskip
0.56905pt].b[\hskip