
\section{Forward and Backward Markovian Bisimilarity}
\label{sec:bisim}

\noindent
Behavioral equivalences provide a means to identify structurally different systems that expose the same
observable behavior. A central notion for stochastic process calculi is Markovian
bisimilarity~\cite{Hillston96}. It equates systems capable of stepwise mimicking each other's functional and
performance behavior and enjoys nice properties in terms of compositional reasoning and equational and
logical characterizations. For the sake of uniformity, in this section we work at the state space level,
rather than at the linguistic level, by considering an action-labeled CTMC $(\cals, \Act \times \Rate,
\rightarrow)$, where $\Act$ is a set of actions while $\Rate = \realns_{> 0}$ is a set of rates, which in
the case of RMPC is obtained by collecting transitions into bundles as formalized in
Definition~\ref{def:underl_ctmc}.

	\begin{defi}[\emph{Markovian bisimilarity}]\label{def:mb}
An equivalence relation $\bisim$ over the set of states $\cals$ is a Markovian bisimulation iff, whenever
$(s_1, s_2) \in \bisim$, then for all actions $a \in \Act$ and equivalence classes $C \in \cals / \bisim$:
\cws{0}{\rate(s_1, a, C) \: = \: \rate(s_2, a, C)}
where $\rate(s, a, C) = \sum \{ \lambda \in \Rate \st \exists s' \in C \ldotp s \xrightarrow{(a, \lambda)}
s' \}$. Two states $s_1, s_2 \in \cals$ are Markovian bisimilar, written $s_1 \mb s_2$, iff there exists a
Markovian bisimulation $\bisim$ such that $(s_1, s_2) \in \bisim$.
\fullbox

	\end{defi}

Following~\cite{ccsk}, we may adapt Markovian bisimilarity to our reversible calculus by means of two
conditions like the one in the definition above, with the former referring to forward transitions and the
latter referring to backward transitions. By so doing, we would end up with a very restrictive equivalence,
as for instance $(a, \lambda) . \nil \coop{\emptyset} (b, \mu) . \nil$ and $(a, \lambda) . (b, \mu) . \nil +
(b, \mu) . (a, \lambda) . \nil$ would be told apart. The reason is that in the former process from $(a,
\lambda)[i] . \nil \coop{\emptyset} (b, \mu)[j] . \nil$ both a backward $a$-transition and a backward
$b$-transition are enabled, whilst in the latter process from $(a, \lambda)[i] . (b, \mu)[j] . \nil + (b,
\mu) . (a, \lambda) . \nil$ only a backward $b$-transition is enabled as well as from $(a, \lambda) . (b,
\mu) . \nil + (b, \mu)[i] . (a, \lambda)[j] . \nil$ only a backward $a$-transition is enabled. In other
words, the so-called expansion law~\cite{Milner89}, which transforms a parallel composition into a choice
among all of its possible interleaved computations, would not hold, because the two transitions in the
former process are concurrent and hence when going backward there is no obligation to follow the path
traversed in the forward direction, whereas this is not the case with the latter process.

As recognized in~\cite{DeNicolaMV90}, in order to set up a more useful equivalence, it is necessary to
enforce that, when going backward, a process can only move along the path representing the history that
brought the process to the current state. To accomplish this, bisimilarity has to be defined as a relation
over paths, not over states, hence we start by adapting the notation of the nondeterministic setting
of~\cite{DeNicolaMV90} to our stochastic setting. In particular, we suitably extend the notion of
transition.

	\begin{defi}[\emph{path}]
A sequence $\xi = (s_0, (a_1, \lambda_1), s_1) (s_1, (a_2, \lambda_2), s_2) \dots (s_{n - 1}, (a_n,
\lambda_n), s_n) \linebreak \in \, \rightarrow^*$ is called a path from state $s_0$ of length $n$. We let
$\first(\xi) = s_0$ and $\last(\xi) = s_n$; the empty path is indicated with $\epsilon$. We denote by
$\pt(s)$ the set of paths from state $s$.
\fullbox

	\end{defi}

	\begin{defi}[\emph{run}]
A pair $\rho = (s, \xi)$ is called a run from state $s$ iff $\xi \in \pt(s)$, in which case we let
$\pt(\rho) = \xi$, $\first(\rho) = \first(\xi)$, $\last(\rho) = \last(\xi)$, with $\first(\rho) =
\last(\rho) = s$ when $\xi = \epsilon$. We denote by $\rn(s)$ the set of runs from state $s$. Given $\rho =
(s, \xi) \in \rn(s)$ and $\rho' = (s', \xi') \in \rn(s')$, their composition $\rho \rho' = (s, \xi \xi') \in
\rn(s)$ is defined iff $\last(\rho) = \first(\rho')$. We write $\rho \xrightarrow{(a, \lambda)} \rho'$ iff
there exists $\rho'' = (s, (s, (a, \lambda), s'))$ with $s = \last(\rho)$ such that $\rho' = \rho \rho''$.
\fullbox

	\end{defi}

In the following, for the action-labeled CTMC $(\cals, \Act \times \Rate, \rightarrow)$ we consider the set
$\calu$ of its runs in lieu of~$\cals$. Furthermore, we view the transition relation $\rightarrow$ as being
symmetric with respect to source and target states, so that every transition can be traversed in both
directions. In the setting of RMPC, this amounts to considering only the forward transition relation thanks
to Lemma~\ref{lm:loop}. Given a run $\rho$, an action $a$, and a bisimulation equivalence class $C$, based
on~\cite{DeNicolaMV90} we distinguish between the total rate of \emph{outgoing} and \emph{incoming} run
transitions, respectively, when moving between $\rho$ and $C$ via $a$. Forward and backward Markovian
bisimilarity thus relies on checking both outgoing rate equality and incoming rate equality.

	\begin{defi}[\emph{forward and backward Markovian bisimilarity}]\label{def:fbmb}
An equivalence relation $\bisim$ over the set of runs $\calu$ is a forward and backward Markovian
bisimulation iff, whenever $(\rho_1, \rho_2) \in \bisim$, then for all actions $a \in \Act$ and equivalence
classes $C \in \calu / \bisim$:
\cws{0}{\begin{array}{rcl}
\rateo(\rho_1, a, C) & = & \rateo(\rho_2, a, C) \\
\ratei(\rho_1, a, C) & = & \ratei(\rho_2, a, C) \\
\end{array}}
where $\rateo(\rho, a, C) = \sum \{ \lambda \in \Rate \mid \exists \rho' \in C \ldotp \rho \xrightarrow{(a,
\lambda)} \rho' \}$ and $\ratei(\rho, a, C) = \sum \{ \lambda \in \Rate \mid \linebreak \exists \rho' \in C
\ldotp \rho' \xrightarrow{(a, \lambda)} \rho \}$. Two states $s_1, s_2 \in \cals$ are forward and backward
Markovian bisimilar, written $s_1 \fbmb s_2$, iff there exists a forward and backward Markovian bisimulation
$\bisim$ such that $((s_1, \epsilon), (s_2, \epsilon)) \in \bisim$.
\fullbox

	\end{defi}

	\begin{thm}\label{thm:fbmb}
Let $s_1, s_2 \in \cals$. Then $s_1 \fbmb s_2 \: \Longrightarrow \: s_1 \mb s_2$.

		\begin{proof}
Suppose that $s_1 \fbmb s_2$, with $\bisim$ being a forward and backward Markovian bisimulation on $\calu$
such that $((s_1, \epsilon), (s_2, \epsilon)) \in \bisim$. We show that $\bisim' = \{ (\last(\rho_1),
\last(\rho_2)) \st (\rho_1, \rho_2) \in \bisim \}$ is a Markovian bisimulation on $\cals$, from which $s_1
\mb s_2$ will follow. \\
Consider $(\last(\rho_1), \last(\rho_2)) \in \bisim'$. By definition of $\bisim'$, we have that $(\rho_1,
\rho_2) \in \bisim$. Since $\bisim$ is a forward and backward Markovian bisimulation, for all $a \in \Act$
and $C \in \calu / \bisim$ it holds in particular that $\rateo(\rho_1, a, C) = \rateo(\rho_2, a, C)$. Since
$\rho_k \xrightarrow{(a, \lambda)} \rho'_k$ iff $\last(\rho_k) \xrightarrow{(a, \lambda)} \last(\rho'_k)$
for $k \in \{ 1, 2 \}$ and -- provided that function $\last$ is lifted from runs to sets of runs -- any
equivalence class $C' \in \cals / \bisim'$ is of the form $[\last(\rho)]_{\bisim'} = \{\last(\rho') \in
\cals \st (\last(\rho), \last(\rho')) \in \bisim' \} = \last(\{ \rho' \in \calu \st (\rho, \rho') \in \bisim
\}) = \last([\rho]_{\bisim})$, i.e., $C' = \last(C)$ for some equivalence class $C \in \calu / \bisim$, it
follows that for all $a \in \Act$ and $C' \in \cals / \bisim$ such that $C' = \last(C)$ for $C \in \calu /
\bisim$ it holds that $\rate(\last(\rho_1), a, C') = \rateo(\rho_1, a, C) = \rateo(\rho_2, a, C) =
\rate(\last(\rho_2), a, C')$.
		\end{proof}

	\end{thm}

The behavioral equivalence $\fbmb$ is strictly finer than $\mb$. Indeed, it turns out to be exceedingly
discriminating. For example, a CTMC with the only two transitions $s_{1} \xrightarrow{(a, \lambda)} s'_{1}$
and $s_{1} \xrightarrow{(a, \mu)} s''_{1}$ would be distinguished from a CTMC having only transition $s_{2}
\xrightarrow{(a, \lambda + \mu)} s'_{2}$. \linebreak Observing that in terms of runs the considered
transitions are reformulated as $\rho_{1} \xrightarrow{(a, \lambda)} \rho'_{1}$, $\rho_{1} \xrightarrow{(a,
\mu)} \rho''_{1}$, and $\rho_{2} \xrightarrow{(a, \lambda + \mu)} \rho'_{2}$ where $\rho_{1} = (s_{1},
\epsilon)$ and $\rho_{2} = (s_{2}, \epsilon)$, the reflexive, symmetric, and transitive closure of the
relation $\{ (\rho_{1}, \rho_{2}), (\rho'_{1}, \rho'_{2}), (\rho''_{1}, \rho'_{2}) \}$ would work well when
moving forward, as for instance $\rateo(\rho_1, a, C) = \lambda + \mu = \rateo(\rho_2, a, C)$ for $C = \{
\rho'_{1}, \rho''_{1}, \rho'_{2} \}$, whereas this would not be the case when moving backward, as for
instance $\ratei(\rho'_1, a, C) = \lambda$, $\ratei(\rho''_1, a, C) = \mu$, $\ratei(\rho'_2, a, C) = \lambda
+ \mu$ for $C = \{ \rho_{1}, \rho_{2} \}$.

This example suggests that rate-based quantitative aspects may be neglected when going backward. Indeed,
summing up rates when considering transitions departing from the same state is consistent with the fact that
the sojourn time in that state is exponentially distributed with rate given by the sum of the rates of the
outgoing transitions. Operationally, this can be interpreted as if there were a race among those transitions
to decide which one will be executed, with each transition having a winning probability proportional to its
rate. This race interpretation no longer applies in the backward direction, as we sum up rates of
transitions that may depart from different states. We therefore consider a time-abstract variant of $\fbmb$
when going backward. It is worth noting that, if it abstracted from time also when going forward, then we
would precisely obtain the strong back and forth bisimilarity of~\cite{DeNicolaMV90}.

	\begin{defi}[\emph{forward and time-abstract backward Markovian bisimilarity}]\label{def:ftabmb}
An equivalence relation $\bisim$ over the set of runs $\calu$ is a forward and time-abstract backward
Markovian bisimulation iff, whenever $(\rho_1, \rho_2) \in \bisim$, then for all actions $a \in \Act$ and
equivalence classes $C \in \calu / \bisim$:
\cws{0}{\begin{array}{rcl}
\rateo(\rho_1, a, C) & = & \rateo(\rho_2, a, C) \\
\transi(\rho_1, a, C) & = & \transi(\rho_2, a, C) \\
\end{array}}
where $\transi(\rho, a, C) = 1$ if there exist $\rho' \in C$ and $\lambda \in \Rate$ such that $\rho'
\xrightarrow{(a, \lambda)} \rho$, $\transi(\rho, a, C) \linebreak = 0$ otherwise. Two states $s_1, s_2 \in
\cals$ are forward and time-abstract backward Markovian bisimilar, written $s_1 \ftabmb s_2$, iff there
exists a forward and time-abstract backward Markovian bisimulation $\bisim$ such that $((s_1, \epsilon),
(s_2, \epsilon)) \in \bisim$.
\fullbox

	\end{defi}

We conclude by showing that $\ftabmb$ -- which is defined on runs, compares for any action both outgoing
total rates and the existence of incoming transitions, and preserves history when going backward even in the
presence of concurrent transitions -- coincides with the standard $\mb$ -- which is defined on states and
compares for any action only outgoing total rates -- thus generalizing the first result
of~\cite{DeNicolaMV90} in our stochastic setting. As a consequence, the former equivalence inherits the
compositionality properties and the equational and logical characterizations of the latter, including in
particular the expansion law as well as the stochastic variant of idempotency according to which $(a,
\lambda) . P + (a, \mu) . P$ is identified with $(a, \lambda + \mu) . P$.

	\begin{thm}\label{thm:ftabmb}
Let $s_1, s_2 \in \cals$. Then $s_1 \ftabmb s_2 \iff s_1 \mb s_2$.

		\begin{proof}
The proof is divided into two parts:

			\begin{itemize}

\item The proof of $s_1 \ftabmb s_2 \: \Longrightarrow \: s_1 \mb s_2$ is identical to the proof of
Theorem~\ref{thm:fbmb} as only outgoing total rates are considered.

\item Suppose that $s_1 \mb s_2$. Let $\ct$ be the mapping that associates with each path $\xi$ its colored
trace, i.e., the path obtained from $\xi$ by replacing each state with its Markovian bisimulation
equivalence class:
\cws{0}{\hspace*{-0.6cm}\begin{array}{l}
\ct((s_0, (a_1, \lambda_1), s_1) (s_1, (a_2, \lambda_2), s_2) \dots (s_{n - 1}, (a_n, \lambda_n), s_n)) = \\
\hspace*{1.0cm} ([s_{0}]_{\mb}, (a_1, \lambda_1), [s_{1}]_{\mb}) ([s_{1}]_{\mb}, (a_2, \lambda_2),
[s_{2}]_{\mb}) \dots ([s_{n-1}]_{\mb}, (a_n, \lambda_n), [s_{n}]_{\mb}) \\
\end{array}}
Let $\bisim = \{ (\rho_1, \rho_2) \st \rho_1 \in \run(s_1), \rho_2 \in \run(s_2), \ct(\pt(\rho_1)) =
\ct(\pt(\rho_2)) \}$, which contains in particular $((s_1, \epsilon), (s_2, \epsilon))$. We show that its
reflexive, symmetric, and transitive closure $\bisim'$ is a forward and time-abstract backward Markovian
bisimulation. \\
Given $(\rho_1, \rho_2) \in \bisim$, i.e., $\rho_1 \in \run(s_1)$ and $\rho_2 \in \run(s_2)$ such that
$\ct(\pt(\rho_1)) = \ct(\pt(\rho_2))$, with $l$ being the length of $\pt(\rho_1)$ and $\pt(\rho_2)$, let us
examine the forward and backward directions respectively:

				\begin{itemize}

\item By virtue of $\ct(\pt(\rho_1)) = \ct(\pt(\rho_2))$, it holds in particular that $\last(\rho_1) \mb
\last(\rho_2)$, hence for all $a \in \Act$ and $C \in \cals / \! \mb$ we have that $\rate(\last(\rho_1), a,
C) = \rate(\last(\rho_2), a, C)$. Since $\last(\rho_k) \xrightarrow{(a, \lambda)} \last(\rho'_k)$ iff
$\rho_k \xrightarrow{(a, \lambda)} \rho'_k$ for $k \in \{ 1, 2 \}$, with $\rho'_k$ still belonging to
$\run(s_k)$, and any equivalence class $C' \in (\run(s_1) \cup \run(s_2)) / \bisim'$ is made of runs with
paths of the same length that traverse the same sequence of Markovian bisimulation equivalence classes of
states and perform the same sequence~of exponentially timed actions, it follows that for all $a \in \Act$
and $C' \in (\run(s_1) \cup \run(s_2)) / \bisim'$:

					\begin{itemize}

\item if the length of all the runs of $C'$ is less than $l + 1$, then it trivially holds that
$\rateo(\rho_1, a, C') = 0 = \rateo(\rho_2, a, C')$;

\item otherwise, assuming that the states reached after $l + 1$ transitions by all of the runs of $C'$
belong to some $C \in \cals / \! \mb$, it holds that $\rateo(\rho_1, a, C') = \rate(\last(\rho_1), a, C) =
\rate(\last(\rho_2), a, C) = \rateo(\rho_2, a, C')$.

					\end{itemize}

\item Since $\ct(\pt(\rho_1)) = \ct(\pt(\rho_2))$, it cannot be the case that $\pt(\rho_1) = \epsilon$ and
$\pt(\rho_2) \neq \epsilon$, or vice versa. If $\pt(\rho_1) = \pt(\rho_2) = \epsilon$, then for all $a \in
\Act$ and $C' \in (\run(s_1) \cup \run(s_2)) / \bisim'$ it trivially holds that $\transi(\rho_1, a, C') = 0
= \transi(\rho_2, a, C')$. \\
Suppose that $\pt(\rho_1) \neq \epsilon \neq \pt(\rho_2)$, with $\rho_k = \rho'_k \rho''_k$ and $\rho''_k =
(s'_k, (s'_k, (a, \lambda), s''_k))$, so that $s'_k \xrightarrow{(a, \lambda)} s''_k$ is the last transition
in $\pt(\rho_k)$ and hence $\rho'_k \xrightarrow{(a, \lambda)} \rho_k$ with $\rho'_k$ still belonging to
$\run(s_k)$, for $k \in \{ 1, 2 \}$. From $\ct(\pt(\rho_1)) = \ct(\pt(\rho_2))$, it follows in particular
that $s'_1 \mb s'_2$. As a consequence, for all $a \in \Act$ and $C' \in (\run(s_1) \cup \run(s_2)) /
\bisim'$:

					\begin{itemize}

\item if the length of all the runs of $C'$ is less than $l$, then it trivially holds that $\transi(\rho_1,
a, C') \linebreak = 0 = \transi(\rho_2, a, C')$;

\item otherwise, assuming that the states reached after $l - 1$ transitions by all of the runs of $C'$
belong to some $C \in \cals / \! \mb$, it holds that $\transi(\rho_1, a, C') = 1 = \transi(\rho_2, a, C')$
or $\transi(\rho_1, a, C') = 0 = \transi(\rho_2, a, C')$ depending on whether $s'_1, s'_2 \in C$ or $s'_1,
s'_2 \notin C$.
\qedhere

					\end{itemize}

				\end{itemize}

			\end{itemize}
 
		\end{proof}

	\end{thm}

	\begin{cor}
Let $R_1, R_2 \in \calp$ be two reachable processes. Then $R_1 \ftabmb R_2 \iff R_1 \mb R_2$.
\fullbox

	\end{cor}

\section{Causal Consistent Reversibility}
\label{sec:causal_rev}

\noindent
Reversibility in a computing system implies the possibility of reverting the last performed action. In a
sequential system, this is very simple as there exists just one last action. Hence, the only challenge is
how to store the information needed to reverse this last action. Since Bennett~\cite{Bennett73}, several
techniques have been developed to reverse the computations of a sequential
program~\cite{Leeman86,YokoyamaG07,HaySchmidtGCH21,PalaciosV15}.

In a concurrent system, the situation is more complex as there is no clear definition of last action.
Indeed, there might be several concurrent last actions. One could resort to timestamps to decide which
action is the last one, but having synchronized clocks in a distributed system is rather difficult. A good
approximation is to consider as last action each action that has not caused any other action yet. This is
at the basis of the so called \emph{causal consistent reversibility}~\cite{rccs}, which relates
reversibility with causality. Intuitively, the definition says that, in a concurrent system, any action can
be undone provided that all of its consequences, if any, are undone beforehand. 

In the process algebra literature, specifically for CCS~\cite{Milner89}, two approaches have been developed
to reverse a computation and to keep track of past actions: the \emph{dynamic} approach of~\cite{rccs} and
the \emph{static} approach of~\cite{ccsk}. The former relies on RCCS~\cite{rccs}, a variant of CCS that uses
stack-based memories attached to processes to record all the actions executed by the processes themselves.
In contrast, \cite{ccsk} proposes a general method, of which CCSK is a result, to reverse calculi whose
operational semantic rules are expressed in the path format of~\cite{BaetenV93}. The basic idea of this
method is to make all the operators of the calculus static and to univocally identify each executed action
with a communication key.

Despite these two approaches are quite different, they have been recently shown to be equivalent in terms of
labeled transition system isomorphism~\cite{LaneseMM21}. On the application side, the dynamic approach
of~\cite{rccs} is more suitable for systems whose operational semantics is given in terms of reduction
semantics, hence it is to be preferred in the case of very expressive
calculi~\cite{LaneseMS10,CristescuKV13,LaneseM20} as well as programming
languages~\cite{LienhardtLMS12,LaneseNPV18b}. On the other hand, the static approach of~\cite{ccsk} is very
handy when it comes to deal with labeled transition systems and CCS-like calculi, which is the case of this
paper.

As mentioned above, since dynamic process algebraic operators -- like for instance action prefix ``.'' and
choice ``+'' -- disappear after a reduction thus causing information loss, in~\cite{ccsk} all of them are
made static. For example, in the following CCS reduction:
\[ a . P + b . Q \: \xrightarrow{a} \: P \]
both the information about $a$ and the right branch $+ \, b . Q$ are lost after performing the reduction.
Hence, in order to get back to the initial state, the system has to remember both the executed prefix $a$
and the discarded process $b . Q$. In~\cite{ccsk} the dynamic operators are syntactically maintained in the
term, so that the process $a . P + b . Q$ reduces as follows:
\[ a . P + b . Q \: \xrightarrow{a\decor{[i]}} \: \decor{a[i]} . P \decor{\, + \, b . Q} \]
where $\decor{a[i]}.P \decor{\, + \, b . Q}$ behaves like $P$ in further forward reductions, while the
colored parts can be seen as decorations of $P$ to be used only in backward reductions. Alternatively,
$\decor{a[i]} . P \decor{\, + \, b . Q}$ can be seen as $\calc[P]$, where $P$ is the active part and $\calc
= a[i] . \bullet \, + \, b . Q$ is its decorated context. In this way, the use of explicit memories
of~\cite{rccs} is avoided because the necessary information is syntactically maintained within processes.
Note that action $a$ is decorated with key $\decor{[i]}$ so as to distinguish among several actions executed
in the past that have the same name.

\section{Conclusions}
\label{sec:concl}

\noindent
Since the work of Landauer~\cite{Landauer61}, reversible computing has attracted a growing attention mainly
for the possibility of building energy efficient circuits. Nowadays, the interest has spread into many
application areas and hence reversible computing requires a deep investigation of its theoretical
foundations from a software science perspective. There exist different interpretations of reversibility in
the literature. In this paper, we have addressed our research quest towards bridging causal consistent
reversibility~\cite{rccs} -- developed in concurrency theory -- and time reversibility~\cite{Kelly79} --
originated in the field of stochastic processes for efficient analysis purposes.

We have accomplished this by introducing the stochastic process calculus RMPC, whose syntax and semantics
follow the approach of~\cite{ccsk}, with the aim of paving the way to concurrent system models that are
causal consistent reversible and time reversible \emph{by construction}. Causal consistent reversibility has
been proved by exploiting the technique of~\cite{LanesePU20} after importing in the setting of~\cite{ccsk}
some notions coming from~\cite{rccs}. Thanks to time reversibility, we have inherited from~\cite{MarinR15} a
product form result that enables the efficient calculation of performance measures. Finally, we have
developed two forward and backward variants of Markovian bisimilarity~\cite{Hillston96} inspired
by~\cite{DeNicolaMV90}, with the former preserving the expansion law and the latter additionally preserving
a stochastic variant of the idempotency law.

There are several lines of research that we plan to undergo, ranging from the application of our results to
case studies modeled with RMPC to the development of further theoretical results. For instance, we would
like to investigate further conditions under which time reversibility is achieved, in addition to the one
relying on the equality of forward and backward rates, as well as further properties of forward and backward
variants of Markovian bisimilarity. As another example, we would like to add recursion to the syntax of
RMPC. From the point of view of the ergodicity of the underlying CTMC, the absence of recursion is not a
problem because every forward transition has the corresponding backward transition by construction. However,
there might be situations in which recursion is necessary to appropriately describe the behavior of a
system. Because of the use of communication keys, a simple process of the form $P \triangleq (a, \lambda) .
P$, whose standard labeled transition system features a single state with a self-looping transition,
produces a sequence of infinitely many distinct states even if we resort to transition bundles. Our claim is
that the specific cooperation operator that we have considered may require a mechanism lighter than
communication keys to keep track of past actions, which may avoid the generation of an infinite state space
in the presence of recursion.

\section*{Acknowledgement}
This research has been supported by the MUR PRIN project NiRvAna -- Noninterference and Reversibility
Analysis in Private Blockchains.

\section{Introduction}
\label{sec:intro}

\noindent
The interest into computation reversibility dates back to the 60’s, when Landauer observed that irreversible
computations cause heat dissipation into circuits~\cite{Landauer61}. More precisely, Landauer's principle
says that any logically irreversible manipulation of information, such as the erasure of a bit or the
merging of two computation paths, must be accompanied by a corresponding entropy increase in
non-information-bearing degrees of freedom of the information processing apparatus or its
environment~\cite{Bennet03}. Hence, according to this principle, which has been recently
verified in~\cite{BerutAPCDL12} and given a physical foundation in~\cite{Frank18}, any logically-reversible
computation, in which no information (e.g., bits) is erased, may be potentially carried out without
releasing any heat. This suggested that low energy consumption could be achieved by resorting to
\emph{reversible computing}, in which there is no information loss~\cite{Bennett73}. Nowadays, reversible
computing has several applications ranging from modelling biochemical reactions~\cite{Pinna17,PhillipsUY12}
and parallel discrete-event simulation~\cite{PerumallaP14,SchordanOJB18} to robotics~\cite{LaursenES18},
control theory~\cite{SiljakPP19}, fault tolerant systems~\cite{DanosK05,deVriesKH10,LaneseLMSS13,VassorS18},
and program debugging~\cite{GiachinoLM14,LaneseNPV18a}.

In a reversible system, we can observe two directions of computation: a \emph{forward} one, coinciding with
the normal way of computing, and a \emph{backward} one, which is able to undo the effects of the forward
one. In the literature, there exist different meanings of reversibility. For instance, in a Petri net model
reversibility means that one can always reach the initial marking~\cite{BarylskaKMP18}, while in distributed
systems it amounts to the capability of returning to a past consistent state~\cite{rccs}. In contrast, in
the performance evaluation field, reversibility is intended as time reversibility and is instrumental to
develop efficient analysis methods~\cite{Kelly79}.
 
Our focus is on the relationship between \emph{causal consistent reversibility} and \emph{time
reversibility}, from a process algebraic perspective. Causal consistent reversibility stands for the
capability of going back to a past state that is consistent with the computational history of a system; in
this setting, quantitative aspects have been totally disregarded. On the other hand, the theory of time
reversibility studies the conditions under which the stochastic behavior of a system remains the same when
the direction of time is reversed; unfortunately, it has been applied to concurrent systems without
explicitly taking causality into account. In this paper, we aim at bridging these two theories by showing
how causal consistent reversibility and time reversibility can be jointly achieved. To this purpose, we
consider a stochastic process calculus in which every action is equipped with a positive real number
expressing the rate at which the action is executed. As is well known in the literature~\cite{Hillston96},
the stochastic process underlying the calculus turns out to be a continuous-time Markov chain
(CTMC)~\cite{KemenyS60}.

The contribution of this paper is threefold. Firstly, we apply for the first time the technique
of~\cite{ccsk} to a stochastic process calculus. In particular, we provide forward and backward operational
semantic rules -- featuring forward and backward actions and rates -- and then we show that the resulting
calculus is causal consistent reversible. The latter is accomplished by importing from the reduction
semantics setting of~\cite{rccs} the notion of concurrent transitions, which is new in the structural
operational semantics framework of~\cite{ccsk} and is then managed by following the approach
of~\cite{LanesePU20}.

Secondly, after observing that the CTMC underlying the calculus is stationary, we prove that time
reversibility can be obtained by using, in the operational semantic rules, backward rates equal to the
corresponding forward rates. This is quite different from the approach adopted for example
in~\cite{Harrison03,MarinR15}, where time reversibility is verified a posteriori, as we instead produce a
calculus in which time reversibility can be guaranteed by construction. The difference in the approach does
not prevent us from importing compositionality results of those works in our setting.

Thirdly, we address behavioral equivalences for our reversible stochastic process calculus, in order to
provide a means to identify systems possessing the same functional and performance properties. In
particular, we focus on Markovian bisimilarity~\cite{Hillston96}, which equates systems capable of stepwise
mimicking each other's functional and performance behavior. We extend a result of~\cite{DeNicolaMV90} to our
stochastic setting by showing that a variant of Markovian bisimilarity on computations accounting for both
forward and backward directions coincides with Markovian bisimilarity on states, thus inheriting the nice
properties of the latter.

This paper, which is a revised and enriched version of~\cite{BernardoM20}, is organized as follows. In
Sections~\ref{sec:causal_rev} and~\ref{sec:time_rev} we recall background information about causal
consistent reversibility and time reversibility, respectively. In Section~\ref{sec:rmpc_integration} we
develop our proposal of integration for these two forms of reversibility in the setting of a Markovian
process calculus, which is then equipped in Section~\ref{sec:bisim} with a forward and backward Markovian
bisimilarity. Finally, in Section~\ref{sec:concl} we conclude with some directions for future work.


\section{Integrating Causal and Time Reversibility}
\label{sec:rmpc_integration}

\noindent
In this section, we integrate the two concepts of causal consistent reversibility and time reversibility
recalled in the previous two sections. We start with a simple calculus called RMPC -- Reversible Markovian
Process Calculus, in which actions are paired with rates, whose syntax and semantics are inspired
by~\cite{ccsk}. Then, we show that the reversibility induced by RMPC is causal consistent by using the
notion of concurrent transitions of~\cite{rccs} and the technique of~\cite{LanesePU20}. Finally, we exhibit
the conditions under which time reversibility is achieved too and we compare our setting, in which time
reversibility is ensured by construction, with those of~\cite{Harrison03,MarinR15}, from which we import a
product form result.


\subsection{Syntax and Semantics for RMPC}
\label{sec:integr_calculus}

\noindent
The syntax of RMPC is shown in Table~\ref{tab:syntax}. A \emph{forward process} $P$ can be one of the
following: the idle process~$\nil$; the prefixed process $(a, \lambda) . P$, which is able to perform an
action $a$ at rate $\lambda$ -- called an exponentially timed action as its duration follows an exponential
distribution of parameter $\lambda$ -- and then continues as process~$P$; the nondeterministic choice $P +
Q$ between processes $P$ and $Q$; or the parallel composition $P \coop{L} Q$, indicating that processes $P$
and $Q$ execute in parallel and must synchronize only on actions prescribed by the set $L$.

	\begin{table}[t]

\[\begin{array}{|rcl|}
\hline
\: P, Q & \sdef & \nil \ou (a, \lambda) . P \ou P + Q \ou P \coop{L} Q \\[0.1cm]
R, S & \sdef & P \ou (a, \lambda)[i] . R \ou R + S \ou R \coop{L} S \:\: \\
\hline
\end{array}\]

\caption{Syntax of RMPC forward/standard/initial processes and reversible processes}
\label{tab:syntax}

	\end{table}

A \emph{reversible process} $R$ is built on top of forward processes. As in~\cite{ccsk}, the syntax of
reversible processes differs from the one of forward processes by the fact that in the former each prefix
$(a, \lambda)$ can be decorated with a \emph{communication key} $i$ thus becoming $(a, \lambda)[i]$. A
process of the form $(a, \lambda)[i] . R$ expresses that in the past the process synchronized with the
environment and this synchronization was identified by key $i$. Keys are thus attached only to already
executed actions.

Let $\Act$ be a set of actions (ranged over by $a, b$), $\Rate = \realns_{> 0}$ be a set of rates (ranged
over by $\lambda, \mu$), and $\Key$ be a set of keys (ranged over by $i, j$). Let $\Lbl = \Act \times \Rate
\times \Key$ be a set of labels each formed by an action, a rate, and a communication key. We let $\ell$ and
its decorated version range over $\Lbl$. Moreover, given a forward label $\ell = (a, \lambda)[i]$, we denote
by $\past{\ell} = (a, \past{\lambda})[i]$ the corresponding backward label. Finally, $\Procs$ is the set of
processes generated by the production for $R$ in Table~\ref{tab:syntax}.

	\begin{defi}[\emph{standard process}]
Process $R \in \Procs$ is standard, written $\std(R)$, iff it can be derived from the production for $P$ in
Table~\ref{tab:syntax}.
\fullbox

	\end{defi}

	\begin{defi}[\emph{process key set}]
The set of keys of process $R \in \Procs$, written $\key(R)$, is inductively defined as follows:
\cws{10}{\begin{array}{rcl}
\key(P) & = & \emptyset \\
\key((a,\lambda)[i].R) & = & \{i\} \cup \key(R) \\
\key(R + S) & = & \key(R) \cup \key(S) \\
\key(R \coop{L} S) & = & \key(R) \cup \key(S) \\
\end{array}}
\fullbox

	\end{defi}

	\begin{table}[t]

\[\begin{array}{|c|}
\hline
\inferrule*[left=Act1]{\std(R)}{(a,\lambda).R \fw{(a,\lambda)[i]} (a,\lambda)[i].R} \quad
\inferrule*[left=Act1$^\rev$]{\std(R)}{(a,\lambda)[i].R \bk{(a,\past{\lambda})[i]} (a,\lambda).R} \\[0.3cm]
\inferrule*[left=Act2]{R \fw{(b,\mu)[j]} R' \quad j \neq i}{(a,\lambda)[i].R \fw{(b,\mu)[j]}
(a,\lambda)[i].R'} \quad
\inferrule*[left=Act2$^\rev$]{R \bk{(b,\past{\mu})[j]} R' \quad j \neq i}{(a,\lambda)[i].R
\bk{(b,\past{\mu})[j]} (a,\lambda)[i].R'} \\[0.3cm]
\inferrule*[left=Cho]{R \fw{(a,\lambda)[i]} R' \and \std(S)}{R+S \fw{(a,\lambda)[i]} R'+S} \quad
\inferrule*[left=Cho$^\rev$]{R \bk{(a,\past{\lambda})[i]} R' \and \std(S)}{R+S \bk{(a,\past{\lambda})[i]}
R'+S} \\[0.3cm]
\inferrule*[left=Par]{R \fw{(a,\lambda)[i]} R' \quad a \notin L \quad i \notin \key(S)}{R \coop{L} S
\fw{(a,\lambda)[i]} R' \coop{L} S} \quad
\inferrule*[left=Par$^\rev$]{R \bk{(a,\past{\lambda})[i]} R' \quad a \notin L \quad i \notin \key(S)}{R
\coop{L} S \bk{(a,\past{\lambda})[i]} R' \coop{L} S} \\[0.3cm]
\: \inferrule*[left=Coo]{R \fw{(a,\lambda)[i]} R' \quad S \fw{(a,\mu)[i]} S' \quad a \in L}{R \coop{L} S
\fw{(a,\lambda\cdot\mu)[i]} R' \coop{L} S'} \quad
\inferrule*[left=Coo$^\rev$]{R \bk{(a,\past{\lambda})[i]} R' \,\,\, S \bk{(a,\past{\mu})[i]} S' \,\,\,
a \in L}{R \coop{L} S \bk{(a,\past{\lambda}\cdot\past{\mu})[i]} R' \coop{L} S'} \: \\
\hline
\end{array}\]

\caption{Structural operational semantic rules for RMPC}
\label{tab:sem}

	\end{table}

The semantics for RMPC is defined as a labeled transition system $(\Procs, \Lbl, \reduction{})$. Like
in~\cite{ccsk}, the transition relation $\reduction{} \, \subseteq \Procs \times \Lbl \times \Procs$ is
given by $\fw{\;\;} \cup \bk{\;\;\;}$, where the \emph{forward transition relation} $\fw{\;\;}$ and the
\emph{backward transition relation} $\bk{\;\;\;}$ are the least relations respectively induced by the
forward rules in the left part of Table~\ref{tab:sem} and the backward rules in the right part of the same
table.

Rule \textsc{Act1} deals with prefixed processes of the form $(a,\lambda).P$, with $P$ written as $R$
subject to $\std(R)$. In addition to transforming the action prefix into a transition label, it generates a
key $i$ that is bound to the action $(a,\lambda)$ thus yielding the label $(a,\lambda)[i]$. As can be noted,
the prefix is not discarded by the application of the rule, instead it becomes a key-storing decoration in
the target process. Rule \textsc{Act1}$^\rev$ reverts the action $(a,\lambda)[i]$ of the process
$(a,\lambda)[i].R$ provided that $R$ is a standard process, which ensures that $(a,\lambda)[i]$ is the only
past action that is left to undo. One of the main design choices of the entire framework is how the rate
$\past{\lambda}$ of the backward action is calculated. For the time being, we leave it unspecified in
\textsc{Act1}$^\rev$ as the value of this rate is not necessary to prove the causal consistency part of
reversibility; we will see later on that it is important in the proof of time reversibility.

The presence of rules \textsc{Act2} and \textsc{Act2}$^\rev$ is motivated by the fact that rule
\textsc{Act1} does not discard the executed prefix from the process it generates. In particular, rule
\textsc{Act2} allows a prefixed process $(a,\lambda)[i].R$ to execute if $R$ can itself execute provided
that the action performed by $R$ picks a key $j$ different from~$i$, so that all action prefixes in a
sequence are decorated with distinct keys. Rule \textsc{Act2}$^\rev$ simply propagates the execution of
backward actions from inner subprocesses that are not standard as long as key uniqueness is preserved, so
that past actions are overall undone from the most recent one to the least recent one.

Unlike the classical rules of the choice operator~\cite{Milner89}, rule \textsc{Cho} does not discard the
context, i.e., the part of the process that has not contributed to the action. More in detail, if the
process $R$ does an action, say $(a,\lambda)[i]$, and becomes $R'$, then the entire process $R + S$ becomes
$R' + S$. In this way, the information about $+ \, S$ is preserved. Furthermore, since $S$ is a standard
process because of the premise $\std(S)$, it will never execute even if it is present in the process $R' +
S$. Hence, the $+ \, S$ can be seen as a decoration, or a dead context, of process~$R$. Note that, in order
to apply rule \textsc{Cho}, at least one of the two processes has to be standard, meaning that it is
impossible for two non-standard processes to execute if they are composed by a choice operator. Rule
\textsc{Cho}$^\rev$ has precisely the same structure as rule \textsc{Cho}, but uses the backward transition
relation. For both rules, we omit their symmetric variants in which it is $S$ to move.

The semantics of parallel composition is inspired by~\cite{Hoare85}. Rule \textsc{Par} allows process~$R$
within $R \coop{L} S$ to individually perform an action $(a,\lambda)[i]$ provided that $a \notin L$. It is
also checked that the executing action is bound to a fresh key, thus ensuring the uniqueness of
communication keys across parallel composition too. Rule \textsc{Coo} allows $R$ and $S$ to synchronize
through any action in the set $L$, provided that the communication key is the same on both sides. For the
sake of simplicity, the rate of the cooperation action is assumed to be the product of the rates of the two
involved actions~\cite{Hillston94}. Rules \textsc{Par}$^\rev$ and \textsc{Coo}$^\rev$ respectively have the
same structure as \textsc{Par} and \textsc{Coo}; the symmetric variants of \textsc{Par} and
\textsc{Par}$^\rev$ are omitted.

Not all the processes generated by the grammar in Table~\ref{tab:syntax} are meaningful, i.e., respectful of
communication key uniqueness enforced by the rules in Table~\ref{tab:sem}. Therefore, in the rest of the
paper we only consider processes that are initial or reachable in the following sense.

	\begin{defi}[\emph{initial process}]
Process $R \in \Procs$ is initial iff $\std(R)$ holds.
\fullbox

	\end{defi}

	\begin{defi}[\emph{reachable process}]
Process $R \in \Procs$ is reachable iff it is initial or can be derived from an initial one via finitely
many applications of the rules for $\fw{\;\;}$ in Table~\ref{tab:sem}.
\fullbox

	\end{defi}


\subsection{Preliminary Reversibility Properties}
\label{sec:integr_prelim}

\noindent
A basic property to satisfy in order for RMPC to be reversible is the so called \emph{loop
lemma}~\cite{rccs,ccsk}, which will be exploited to establish both causal consistent reversibility and time
reversibility. This property states that each transition of a reachable process can be undone, as formalized
below.

	\begin{lem}[\emph{loop lemma}]\label{lm:loop}
Let $R \in \Procs$ be a reachable process. Then $R \fw{(a,\lambda)[i]} S$ iff $S \bk{(a,\past{\lambda})[i]}
R$.

		\begin{proof}
It is easily proved by induction on the depth of the derivation of $R \fw{(a,\lambda)[i]} S$ (resp., $S
\bk{(a,\past{\lambda})[i]} R$), by noting that for each forward (resp., backward) rule there exists a
corresponding backward (resp., forward) one.  
		\end{proof}

	\end{lem}

Given a sequence $\sigma$ of $n \in \natns_{> 0}$ labels $\ell_1, \dots, \ell_n$, let $R \fw{\sigma} S$ be
the corresponding forward sequence of transitions $R \fw{\ell_1} R_1 \fw{\ell_2} \cdots \fw{\ell_n} S$ and
$\past{\sigma}$ be the corresponding backward sequence such that, for each $\ell_i$ occurring in $\sigma$,
it holds that $R_{i-1} \fw{\ell_i} R_i$ iff $R_i \bk{\past{\ell_i}} R_{i-1}$. The loop lemma generalizes as
follows.
 
	\begin{cor}\label{cor:loop}
Let $R \in \Procs$ be a reachable process. Then $R \reduction{\sigma} S$ iff $S \reduction{\past{\sigma}}
R$.
\fullbox

	\end{cor}


\subsection{Causal Consistent Reversibility for RMPC}
\label{sec:integr_causal_rev}
 
\noindent
In order to prove the causal consistent reversibility of RMPC, we borrow some machinery from~\cite{rccs}
that needs to be adapted as the reversing method of~\cite{ccsk} we are using is different from the one
of~\cite{rccs}. In particular, we import the notion of \emph{concurrent transitions}.

Given a transition $\theta : R \reduction{\ell} S$ with $R, S \in \Procs$ reachable processes, we call $R$
the \emph{source} of~$\theta$ and $S$ its \emph{target}. If $\theta$ is a forward transition, i.e., $\theta
: R \fw{\ell} S$, we denote the corresponding backward transition $S \bk{\, \past{\ell}} R$ as
$\past{\theta}$. Two transitions are said to be \emph{coinitial} if they have the same source, and
\emph{cofinal} if they have the same target. A sequence of pairwise composable transitions is called a
\emph{computation}, where \emph{composable} means that the target of any transition in the sequence is the
source of the next transition. We let $\trace$ and its decorated version range over computations, with
$|\trace|$ denoting the length of $\trace$ expressed as the number of transitions constituting it. The
notions of source, target, and composability extend naturally to computations. We indicate with $\et$ the
empty computation and with $\trace_1 \trace_2$ the composition of the two computations $\trace_1$ and
$\trace_2$ when they are composable.

Before specifying when two transitions are concurrent, we need to define the set of causes -- identified by
keys -- that lead to a given communication key along with the notion of process context.

	\begin{defi}[\emph{causal set}]
Let $R \in \Procs$ be a reachable process and $i \in \key(R)$. The causal set $\cau(R,i)$ is inductively
defined as follows for $j \neq i$:
\cws{0}{\begin{array}{rcl}
\cau((a,\lambda)[i].R,i) & = & \emptyset \\
\cau((a,\lambda)[j].R,i) & = & \{j\} \cup \cau(R,i) \\
\cau(R + S, i) & = & \cau'(R,i) \cup \cau'(S,i) \\
\cau(R \coop{L} S, i) & = & \cau'(R,i) \cup \cau'(S,i) \\
\end{array}}
where $\cau'(R,i) = \cau(R,i)$ if $i \in \key(R)$ and $\cau'(R,i) = \emptyset$ otherwise.
\fullbox

	\end{defi}

If $i \in \key(R)$, then $\cau(R, i)$ represents the set of keys in $R$ that caused $i$, with $\cau(R, i)
\subset \key(R)$ because $i \notin \cau(R, i)$ and keys not causally related to $i$ are not considered. A
key $j$ causes $i$ if it appears syntactically before $i$ in $R$ or, said otherwise, $i$ is inside the scope
of $j$. 

	\begin{defi}[\emph{process context}]
A process context $\calc$ is a process with a hole $\bullet$ generated by the grammar $\calc \: \sdef \:
\bullet \,\ou\, (a,\lambda)[i].\calc \,\ou\, R + \calc \,\ou\, \calc + R \,\ou\, R \coop{L} \calc \,\ou\,
\calc \coop{L} R$.
\fullbox

	\end{defi}

We are now in a position to define what we mean by concurrent transitions.

	\begin{defi}[\emph{concurrent transitions}]\label{def:conf}
Two coinitial transitions $\theta_1$ and $\theta_2$ from a reachable process $R \in \Procs$ are in conflict
iff one of the following two conditions holds:

		\begin{enumerate}

\item $\theta_1 : R \fw{(a, \lambda)[i]} S_1$ and $\theta_2 : R \bk{(b, \past{\mu})[j]} S_2$ with $j \in
\cau(S_1, i)$.

\item $R = \calc[P_1 + P_2]$ with $\theta_k$ deriving from $P_k \fw{(a_k, \lambda_k)[i_k]} S_k$ for $k = 1,
2$.

		\end{enumerate}

\noindent
Two coinitial transitions are concurrent when they are not in conflict.
\fullbox

	\end{defi}

The first condition above just tells that a forward transition is in conflict with a backward one whenever
the latter tries to undo a cause of the key of the former. The second condition deems as conflictual two
transitions respectively generated by the two subprocesses of a choice operator. Figure~\ref{fig:conf_tr}
shows two related examples. In the former, the process $(b, \mu)[j] . (a, \lambda) . P$ can perform two
transitions: a backward one and a forward one. They meet the first condition of Definition~\ref{def:conf} as
the backward transition removes the key $i$ that is in the causal set of $j$. In the latter, we have that
process $(a,\lambda).P+(a,\lambda).P$ is able to trigger two forward transitions. Since they arise from the
same choice operator, they are in conflict according to the second condition of Definition~\ref{def:conf}.

	\begin{rem}
It is worth noting that in a stochastic process calculus like RMPC the semantic treatment of the choice
operator is problematic~\cite{Hillston96} because a process of the form $(a,\lambda).P + (a,\lambda).P$
should produce either a single $a$-transition whose rate is $\lambda + \lambda$, or two $a$-transitions each
having rate $\lambda$ that do not collapse into a single one. In our reversible framework, two distinct
transitions are generated thanks to the fact that the key associated with the executed action is stored into
the derivative process too, as shown in the bottom part of Figure~\ref{fig:conf_tr}.
\fullbox

	\end{rem}

	\begin{figure}

\[
\xymatrix{
	&(b,\mu).(a,\lambda).P\\
	(b,\mu)[j].(a,\lambda).P \ar@{~>}^{(b,\past{\mu})[j]} [ur] \ar@{->} ^{(a,\lambda)[i]}[r] & 
(b,\mu)[j].(a,\lambda)[i].P\\
&(a,\lambda).P + (a,\lambda).P \ar@{->}_{(a,\lambda)[i]} [dl] \ar@{->}^{(a,\lambda)[i]} [dr]\\
	(a,\lambda)[i].P+(a,\lambda).P&& (a,\lambda).P+ (a,\lambda)[i].P
	}
\]

\caption{Examples of conflicting transitions}
\label{fig:conf_tr}

	\end{figure}

Concurrent transitions can commute, as formally stated below by the \emph{diamond property}, while
conflicting ones cannot.

	\begin{lem}[\emph{diamond property}]\label{lm:diamond}
Let $\theta_1 : R \reduction{\ell_1} S_1$ and $\theta_2 : R \reduction{\ell_2} S_2$ be two coinitial
transitions from a reachable process $R \in \Procs$. If $\theta_1$ and $\theta_2$ are concurrent, then there
exist two cofinal transitions $\theta_2/\theta_1 : S_1 \reduction{\ell_2} S$ and $\theta_1/\theta_2: S_2
\reduction{\ell_1} S$.

		\begin{proof}
The proof is by case analysis on the direction of $\theta_1$ and $\theta_2$. We distinguish three cases
according to whether the two transitions are both forward, both backward, or one forward and the other
backward. Suppose that $\ell_1 = (a,\lambda)[i]$ and $\ell_2 = (b,\mu)[j]$, with $i \neq j$ otherwise
$\theta_1$ and $\theta_2$ would be generated by the two subprocesses of a choice operator and hence could
not be concurrent:

			\begin{itemize}

\item Suppose that $\theta_1$ and $\theta_2$ are both forward. Since $\theta_1$ and $\theta_2$ are
concurrent, by virtue of Definition~\ref{def:conf} the two transitions cannot originate from a choice
operator. They must thus be generated by a parallel composition, but not through the \textsc{Coo} rule
because $\theta_1$ and $\theta_2$ have different keys and hence cannot synchronize. Without loss of
generality, we can assume that $R = R_1 \coop{L} R_2$ with $R_1 \fw{(a,\lambda)[i]} S_1$ and $R_2
\fw{(b,\mu)[j]} S_2$ and $a,b \not\in L$. By applying the \textsc{Par} rule, we have that $R_1 \coop{L} R_2
\fw{(a,\lambda)[i]} S_1 \parallel_{L} R_2 \fw{(b,\mu)[j]} S_1 \parallel_{L} S_2$ as well as $R_1 \coop{L}
R_2 \fw{(b,\mu)[j]} R_1 \parallel_{L} S_2 \fw{(a,\lambda)[i]} S_1 \parallel_{L} S_2$.

\item The case in which $\theta_1$ and $\theta_2$ are both backward is similar to the previous one.

\item Suppose that $\theta_1$ is forward and $\theta_2$ is backward. Since $\theta_1$ and $\theta_2$ are
concurrent, by virtue of Definition~\ref{def:conf} the backward transition cannot remove a cause of the
forward one. Since either subprocess of a choice operator or a parallel composition cannot perform a forward
transition and a backward transition without preventing the backward one from removing a cause of the
forward one, and in the case of the choice operator only one of the two subprocesses can perform
transitions, without loss of generality we can assume that $R = R_1 \coop{L} R_2$ with $R_1
\fw{(a,\lambda)[i]} S_1$ and $R_2 \bk{(b,\mu)[j]} S_2$ as well as $a,b \not\in L$ so as to preserve causes.
By applying the \textsc{Par} rule, we have that $R_1 \coop{L} R_2 \fw{(a,\lambda)[i]} S_1 \parallel_{L} R_2
\bk{(b,\mu)[j]} S_1 \parallel_{L} S_2$ as well as $R_1 \coop{L} R_2 \bk{(b,\mu)[j]} R_1 \parallel_{L} S_2
\fw{(a,\lambda)[i]} S_1 \parallel_{L} S_2$.
\qedhere

			\end{itemize}

		\end{proof}

	\end{lem} 
 
We finally show that reversibility is causally consistent in our concurrent framework. This can be done in
two ways: either by adapting the original proof of~\cite{rccs}, as we did in~\cite{BernardoM20}, or by using
the general technique provided by~\cite{LanesePU20}. We opt for the latter, according to which causal
consistency stems from the diamond property, \emph{backward transition independence} -- which generalizes
the concept of backward determinism used for reversible sequential languages~\cite{YokoyamaG07} -- and
\emph{past well foundedness} -- which ensures that reachable processes have a finite past.
Following~\cite{Levy76}, we first define a notion of \emph{causal equivalence} over computations, which
abstracts from the order of concurrent transitions, so that computations obtained by swapping the order of
their concurrent transitions are identified with each other and the composition of a computation with its
inverse is identified with the empty computation.

	\begin{defi}[\emph{causal equivalence}]
Causal equivalence is the smallest equivalence $\ceq$ on computations closed under composition and
satisfying:
		\begin{enumerate}

\item If $\theta_1: R \reduction{\ell_1} R_1$, $\theta_2: R \reduction{\ell_2} R_2$ are concurrent and
$\theta'_2: R_1 \reduction{\ell_2} S$, $\theta'_1: R_2 \reduction{\ell_1} S$, then $\theta_1\theta'_2 \ceq
\theta_2\theta'_1$.

\item $\theta\past{\theta} \ceq \et$ and $\past{\theta} \theta\ceq \et$.
\fullbox

		\end{enumerate}

	\end{defi}

	\begin{lem}[\emph{backward transition independence}]
Given a reachable process $R \in \calp$, any two coinitial backward transitions $\theta_1: R
\bk{(a,\past{\lambda})[i]} S_1$ and $\theta_2: R \bk{(b,\past{\mu})[j]} S_2$ are concurrent.

		\begin{proof}
Since by Definition~\ref{def:conf} there is no case in which two backward transitions are conflicting, the
property trivially holds.
		\end{proof}

	\end{lem}

	\begin{prop}[\emph{past well foundedness}]
Let $R_0 \in \calp$ be a reachable process. Then there is no infinite sequence such that $R_i \bk{\ell_i}
R_{i+1}$ for all $i \in \natns$.

		\begin{proof}
It can be easily proved by induction on $|\key(R_0)|$ by observing that a backward transition decreases by
one the total number of keys of $R_0$, with this number being finite.
		\end{proof}

	\end{prop}

The further property below, called \emph{parabolic lemma} in~\cite{LanesePU20}, says that if two
computations $\trace_1$ and $\trace_2$ are coinitial and cofinal and $\trace_2$ is made of forward
transitions only, then in $\trace_1$ there are some transitions that are later undone. This computation is
thus causally equivalent to a forward one in which the undone transitions do not take place at all. Another
way to see this lemma is that backward transitions do not add new states.

	\begin{lem}[\emph{parabolic lemma}]
For any computation $\omega$, there exist two forward-only computations $\omega_1, \omega_2$ such that
$\omega \ceq \past{\omega_1};\omega_2$ and $|\omega_1| + |\omega_2| \leq |\omega|$.

		\begin{proof}
It follows from the diamond property and backward transition independence thanks to~\cite{LanesePU20}.
		\end{proof}

	\end{lem}

	\begin{thm}[\emph{causal consistency}]\label{thm:causal_cons_rev}
Let $\trace_1$ and $\trace_2$ be coinitial computations. Then $\trace_1 \ceq \trace_2$ iff $\trace_1$ and
$\trace_2$ are cofinal too.

		\begin{proof}
It follows from past well foundedness and the parabolic lemma thanks to~\cite{LanesePU20}.
		\end{proof}

	\end{thm}

Theorem~\ref{thm:causal_cons_rev} shows that the notion of causal equivalence characterizes a space for
admissible rollbacks that are (i)~consistent as they do not lead to previously unreachable states and
(ii)~flexible enough to allow undo operations to be rearranged. This implies that the states reached by a
backward computation could be reached by performing forward computations only. Therefore, we conclude that
RMPC is causal consistent reversible.


\subsection{Time Reversibility for RMPC}
\label{sec:integr_time_rev}

\noindent
The rules in Table~\ref{tab:sem} associate with any initial process $R \in \Procs$ a labeled transition
system $\lsp R \rsp = (\Procs, \Lbl, \reduction{}, R)$. To investigate time reversibility, we have to derive
from $\lsp R \rsp$ the CTMC $\calm \lsp R \rsp$ underlying $R$ and we have to specify how each backward rate
$\past{\lambda}$ is obtained from the corresponding forward rate $\lambda$.

First of all, we observe that every non-terminal state of $\lsp R \rsp$ has infinitely many outgoing
transitions. The reason is that rules \textsc{Act1} and \textsc{Act2} generate a transition for each
possible admissible key, with the key being part of both the label and the derivative process term. On the
one hand, this is useful for avoiding the generation of a single $(a, \lambda)$-transition in the case of a
process like $(a, \lambda) . P + (a, \lambda) . P$ whose overall exit rate is $\lambda + \lambda$; even if
the key is the same, two different states $(a, \lambda)[i] . P + (a, \lambda) . P$ and $(a, \lambda) . P +
(a, \lambda)[i] . P$ are reached. On the other hand, it requires considering transition bundles to build
$\calm \lsp R \rsp$, where a \emph{transition bundle} is a set of transitions departing from the same state
and labeled with the same action/rate but different keys, whose target states are syntactically identical up
to keys.

	\begin{defi}[\emph{underlying CTMC}]\label{def:underl_ctmc}
Let $\equiv_{\calk}$ be the least equivalence relation over $\Procs$ induced by $(a, \lambda)[i] . S
\equiv_{\calk} (a, \lambda)[j] . S$. The CTMC underlying an initial process $R \in \Procs$ is defined as the
labeled transition system $\calm \lsp R \rsp = (\Procs / \! \equiv_{\calk}, \cala \times \calr,
\reduction{}_{\calk}, [R]_{\equiv_{\calk}})$ where:

		\begin{itemize}

\item $\Procs / \! \equiv_{\calk}$ is the quotient set of $\equiv_{\calk}$ over $\Procs$, i.e., the set of
classes of processes that are equivalent to each other according to $\equiv_{\calk}$, representing the set
of states.

\item $[R]_{\equiv_{\calk}}$ is the equivalence class of $R$ with respect to $\equiv_{\calk}$, which simply
is the singleton set $\{ R \}$ as $R$ is initial and hence contains no keys, representing the initial state.

\item $\reduction{}_{\calk} \, \subseteq \Procs / \! \equiv_{\calk} \! \times (\cala \times \calr) \times
\Procs / \! \equiv_{\calk}$ is the transition relation given by $\fw{\;\;}_{\calk} \cup \bk{\;\;\;}_{\calk}$
such that:

			\begin{itemize}

\item $[S]_{\equiv_{\calk}} \fw{(a, \lambda)}_{\calk} [S']_{\equiv_{\calk}}$ whenever $S \fw{(a,
\lambda)[i]} S'$ for some $i \in \calk$.

\item $[S]_{\equiv_{\calk}} \bk{(a, \past{\lambda})}_{\calk} [S']_{\equiv_{\calk}}$ whenever $S \bk{(a,
\past{\lambda})[i]} S'$ for some $i \in \calk$.
\fullbox

			\end{itemize}

		\end{itemize}

	\end{defi}

When moving from $\lsp R \rsp$ to $\calm \lsp R \rsp$, individual states are thus replaced by classes of
states that are syntactically identical up to keys in the same positions; moreover, keys are removed from
transition labels. As a consequence, every state of $\calm \lsp R \rsp$ turns out to have finitely many
outgoing transitions. We also note that $\calm \lsp R \rsp$ is an \emph{action-labeled} CTMC, as each of its
transitions is labeled with both a rate and an action.

As a preliminary step towards time reversibility, we have to show that $\calm \lsp R \rsp$ is stationary. It
holds that $\calm \lsp R \rsp$ is even ergodic thanks to the loop lemma.

	\begin{lem}\label{lm:ergodicity}
Let $R \in \Procs$ be an initial process. Then $\calm \lsp R \rsp$ is time homogeneous and ergodic.

		\begin{proof}
The time homogeneity of $\calm \lsp R \rsp$ is a straightforward consequence of the fact that its rates
simply are positive real numbers, not time-dependent functions. The ergodicity of $\calm \lsp R \rsp$ stems
from the fact that the graph representation of $\calm \lsp R \rsp$ is a finite, strongly connected component
due to Corollary~\ref{cor:loop}.
		\end{proof}

	\end{lem}

We exploit once more the loop lemma to derive that, under $\past{\lambda} = \lambda$, the steady-state
probability distribution of $\calm \lsp R \rsp$ is the uniform distribution, from which time reversibility
will immediately follow.

	\begin{lem}\label{lm:unif_stat_distr}
Let $R \in \Procs$ be an initial process, $\cals$ be the set of states of $\calm \lsp R \rsp$, and $n =
|\cals|$. If every backward rate is equal to the corresponding forward rate, then the steady-state
probability distribution $\bfpi$ of $\calm \lsp R \rsp$ satisfies $\pi(s) = 1 / n$ for all $s \in \cals$.

		\begin{proof}
If $n = 1$, i.e., $R$ is equal to $\nil$ or to the parallel composition of several processes whose initial
actions have to synchronize but are different from each other, then trivially $\pi(s) = 1 / n = 1$ for the
only state $s \in \cals$. \\
Suppose now that $n \ge 2$. From Lemma~\ref{lm:ergodicity}, it follows that $\calm \lsp R \rsp$ has a unique
steady-state probability distribution $\bfpi$. Due to Lemma~\ref{lm:loop}, the global balance equation for
an arbitrary $s \in \cals$ is as follows:
\cws{0}{\pi(s) \cdot \sum\limits_{s \reduction{(a, \lambda)}_{\calk} s'} \lambda \: = \: \sum\limits_{s'
\reduction{(a, \past{\lambda})}_{\calk} s} \pi(s') \cdot \past{\lambda}}
Since every backward rate is equal to the corresponding forward rate, the global balance equation for $s$
boils down to:
\cws{0}{\pi(s) \cdot \sum\limits_{s \reduction{(a, \lambda)}_{\calk} s'} \lambda \: = \: \sum\limits_{s'
\reduction{(a, \lambda)}_{\calk} s} \pi(s') \cdot \lambda}
Since the two summations have the same number of summands, the equation above is satified when $\pi(s) =
\pi(s')$ for all $s' \in \cals$ reached by a transition from $s$. All global balance equations are thus
satisfied when $\pi(s) = 1 / n$ for all $s \in \cals$.
		\end{proof}

	\end{lem}

	\begin{thm}[\emph{time reversibility}]\label{thm:time_rev}
Let $R \in \Procs$ be an initial process. If every backward rate is equal to the corresponding forward rate,
then $\calm \lsp R \rsp$ is time reversible.

		\begin{proof}
Let $\cals$ be the set of states of $\calm \lsp R \rsp$ and $n = |\cals|$. From Lemma~\ref{lm:ergodicity},
it follows that $\calm \lsp R \rsp$ has a unique steady-state probability distribution $\bfpi$. To avoid
trivial cases, suppose $n \ge 2$ and consider $s, s' \in \cals$ with $s \neq s'$ connected by a transition.
The proof resembles the one of Lemma~\ref{lm:unif_stat_distr}, but focuses on partial balance equations
rather than on global ones. \\
Due to Lemma~\ref{lm:loop}, the partial balance equation for $s$ and $s'$ is as follows:
\cws{0}{\pi(s) \cdot \sum\limits_{s \reduction{(a, \lambda)}_{\calk} s'} \lambda \: = \: \pi(s') \cdot
\sum\limits_{s' \reduction{(a, \past{\lambda})}_{\calk} s} \past{\lambda}}
Since every backward rate is equal to the corresponding forward rate, the partial balance equation for $s$
and~$s'$ boils down to:
\cws{0}{\pi(s) \cdot \sum\limits_{s \reduction{(a, \lambda)}_{\calk} s'} \lambda \: = \: \pi(s') \cdot
\sum\limits_{s' \reduction{(a, \lambda)}_{\calk} s} \lambda}
Since the two summations have the same number of summands and $\pi(s) = \pi(s') = 1 / n$ due to
Lemma~\ref{lm:unif_stat_distr}, the equation above is satified. The result then follows from the fact that
$s$ and $s'$ are two arbitrary distinct states connected by transitions.
		\end{proof}

	\end{thm}

The main difference between our approach to time reversibility and previous ones in the field of formal
methods, in particular those of~\cite{Harrison03,MarinR15} is twofold. Firstly, our approach is part of a
more general framework in which also causal consistent reversibility is addressed. Secondly, our approach is
inspired by the idea of~\cite{ccsk} of developing a formalism in which it is possible to express models
whose reversibility is guaranteed by construction, instead of building a posteriori the time-reversed
version of a certain model like in~\cite{Harrison03} or verifying a posteriori whether a given model is time
reversible or not like in~\cite{MarinR15}.

It is worth noting that these methodological differences do not prevent us from adapting to our setting some
results from~\cite{Harrison03,MarinR15}, although a few preliminary observations about notational
differences are necessary.

Both~\cite{Harrison03} and~\cite{MarinR15} make a distinction between active actions, each of which is given
a rate, and passive actions, each of which is given a weight, with the constraint that, in case of
synchronization, the rate of the active action is multiplied by the weight of the corresponding passive
action. In RMPC there is no such distinction, however the same operation, i.e., multiplication, is applied
to the rates of two synchronizing actions. A passive action can thus be rendered as an action with rate $1$,
while a set of alternative passive actions can be rendered as a set of actions whose rates sum up to $1$.
Moreover, in~\cite{MarinR15} synchronization is enforced between any active-passive pair of identical
actions, whereas in RMPC the parallel composition operator is enriched with an explicit synchronization set
$L$, which yields as a special case the aforementioned synchronization discipline when $L$ is equal to the
set $\Act$ of all the actions. We can therefore conclude that our parallel composition operator is a
generalization of those used in~\cite{Harrison03,MarinR15}, hence the recalled notational differences do not
hamper result transferral.

In~\cite{Harrison03} the compositionality of a CTMC-based stochastic process calculus is exploited to prove
RCAT, the reversed compound agent theorem, which establishes the conditions under which the time-reversed
version of the cooperation of two processes is equal to the cooperation of the time-reversed versions of
those two processes. The application of RCAT leads to product-form solution results from stochastic process
algebraic models, including a new different proof of Jackson theorem for product-form queueing
networks~\cite{Jackson63}.

In~\cite{MarinR15} the notion of $\rho$-reversibility is introduced for stochastic automata, which are
essentially action-labeled CTMCs. Function $\rho$ is a state permutation that ensures (i)~for each action
the equality of the total exit rate of any state~$s$ and $\rho(s)$ and (ii)~the conservation of
action-related rate products across cycles when considering states in the forward direction and their
$\rho$-counterparts in the backward direction. For any ergodic $\rho$-reversible automaton, it turns out
that $\pi(s) = \pi(\rho(s))$ for every state $s$. Moreover, the synchronization inspired by~\cite{Plateau85}
of two $\rho$-reversible stochastic automata is still $\rho$-reversible and, in case of ergodicity, under
certain conditions the steady-state probability of any compound state is the product of the steady-state
probabilities of the two constituent states.

Our time reversibility result for RMPC can be rephrased in the setting of~\cite{MarinR15} in terms of
$\rho$-reversibility with $\rho$ being the identity function over states. As a consequence, the following
two results stem from Theorem~\ref{thm:time_rev} of the present paper and, respectively, Theorems~$2$
and~$3$ of~\cite{MarinR15}.

	\begin{cor}[\emph{time reversibility closure}]\label{cor:closure}
Let $R_{1}, R_{2} \in \Procs$ be two initial processes and $L \subseteq \Act$. If every backward rate is
equal to the corresponding forward rate, then $\calm \lsp R_{1} \coop{L} R_{2} \rsp$ is time reversible too.
\fullbox

	\end{cor}

	\begin{cor}[\emph{product form}]\label{cor:product_form}
Let $R_{1}, R_{2} \in \Procs$ be two initial processes and $L \subseteq \Act$. If every backward rate is
equal to the corresponding forward rate and the set of states $\cals$ of $\calm \lsp R_{1} \coop{L} R_{2}
\rsp$ is equal to $\cals_{R_{1}} \times \cals_{R_{2}}$ where $\cals_{R_{1}}$ is the set of states of $\calm
\lsp R_{1} \rsp$ and $\cals_{R_{2}}$ is the set of states of $\calm \lsp R_{2} \rsp$, then $\pi(s_{1},
s_{2}) = \pi_{R_{1}}(s_{1}) \cdot \pi_{R_{2}}(s_{2})$ for all $(s_{1}, s_{2}) \in \cals_{R_{1}} \times
\cals_{R_{2}}$.
\fullbox

	\end{cor}

The product form result above avoids the calculation of the global balance equations over $\calm \lsp R_{1}
\coop{L} R_{2} \rsp$, as $\pi(s_{1}, s_{2})$ can simply be obtained by multiplying $\pi_{R_{1}}(s_{1})$ with
$\pi_{R_{2}}(s_{2})$. However, the condition $\cals = \cals_{R_{1}} \times \cals_{R_{2}}$ requires to check
that every state in the full Cartesian product is reachable from $R_{1} \coop{L} R_{2}$. This means that no
compound state is such that its constituent states enable some action but none of the enabled actions can be
executed due to the constraints imposed by the synchronization set $L$. The condition $\cals = \cals_{R_{1}}
\times \cals_{R_{2}}$ implies that $\calm \lsp R_{1} \coop{L} R_{2} \rsp$ is ergodic over the full Cartesian
product of the two original state spaces, which is the condition used in~\cite{MarinR15}. Although implicit
in the statement of the corollary, the time reversibility of $\calm \lsp R_{1} \coop{L} R_{2} \rsp$ is
essential for the product form result.

\section{Time Reversibility}
\label{sec:time_rev}

\noindent
In the performance evaluation field, a different notion of reversibility, called \emph{time reversibility},
is considered. We illustrate it in the specific case of continuous-time Markov chains, which are
discrete-state stochastic processes characterized by the \emph{memoryless property}~\cite{KemenyS60}.

A \emph{stochastic process} describes the evolution of some random phenomenon over time through a set of
random variables, one for each time instant. A stochastic process $X(t)$ taking values into a discrete state
space $\cals$ for $t \in \realns_{\ge 0}$ is a \emph{continuous-time Markov chain (CTMC)} iff for all $n \in
\natns$, time instants $t_{0} < t_{1} < \dots < t_{n} < t_{n + 1} \in \realns_{\ge 0}$, and states $s_{0},
s_{1}, \dots, s_{n}, s_{n + 1} \in \cals$ it holds that $\Pr \{ X(t_{n + 1}) = s_{n + 1} \mid X(t_{i}) =
s_{i}, 0 \le i \le n \} = \Pr \{ X(t_{n + 1}) = s_{n + 1} \mid X(t_{n}) = s_{n} \}$, i.e., the probability
of moving from one state to another does not depend on the particular path that has been followed in the
past to reach the current state, hence that path can be forgotten.

A CTMC is \emph{irreducible} iff each of its states is reachable from every other state. A state $s \in
\cals$ is \emph{recurrent} iff the CTMC will eventually return to $s$ with probability $1$, in which case
$s$ is called \emph{positive recurrent} iff the expected number of steps until the CTMC returns to it is
finite. A CTMC is \emph{ergodic} iff it is irreducible and all of its states are positive recurrent;
ergodicity coincides with irreducibility in the case that the CTMC has finitely many states.

A CTMC can be represented as a labeled transition system or as a state-indexed matrix. In the first case,
each transition is labeled with some probabilistic information describing the evolution from its source
state to its target state. In the second case, the same information is stored into an entry, indexed by
those two states, of a matrix. The value of this probabilistic information is, in general, a function of the
time at which the state change takes place.

For the sake of simplicity, we restrict ourselves to \emph{time-homogeneous} CTMCs, in which conditional
probabilities of the form $\Pr \{ X(t + t') = s' \mid X(t) = s \}$ do not depend on $t$, so that the
considered information is simply a positive real number. This is called the \emph{rate} at which the CTMC
moves from state $s$ to state~$s'$ and uniquely characterizes the exponentially distributed time taken by
the considered move. It can be shown that the sojourn time in any state $s \in \cals$ is exponentially
distributed with rate given by the sum of the rates of the moves of~$s$. The average sojourn time in $s$ is
the inverse of such a sum and the probability of moving from $s$ to $s'$ is proportional to the
corresponding rate.

Every time-homogeneous, ergodic CTMC $X(t)$ is \emph{stationary}, which means that $(X(t_{i} + t'))_{1 \le i
\le n}$ has the same joint distribution as $(X(t_{i}))_{1 \le i \le n}$ for all $n \in \natns_{\ge 1}$ and
$t_{1} < \dots < t_{n}, t' \in \realns_{\ge 0}$. Specifically, $X(t)$ has a unique \emph{steady-state
probability distribution} $\bfpi$ that for all $s \in \cals$ fulfills $\pi(s) = \lim_{t \rightarrow \infty}
\Pr \{ X(t) = s \mid X(0) = s' \}$ for any $s' \in \cals$. These probabilities can be computed by solving
the linear system of \emph{global balance equations} $\bfpi \cdot \mathbf{Q} = \mathbf{0}$ subject to
$\sum_{s \in \cals} \pi(s) = 1$ and $\pi(s) \in \realns_{> 0}$ for all $s \in \cals$. The
\emph{infinitesimal generator matrix} $\mathbf{Q}$ contains for each pair of distinct states the rate of the
corresponding move, which is $0$ in the absence of a direct move between them, with $q_{s, s} = - \sum_{s'
\neq s} q_{s, s'}$ for all $s \in \cals$ so that every row of $\mathbf{Q}$ sums up to $0$.

Due to state space explosion and numerical stability problems~\cite{Stewart94}, the calculation of the
solution of the global balance equation system is not always feasible. However, it can be tackled in the
case that the behavior of the considered CTMC remains the same when the direction of time is reversed. A
CTMC $X(t)$ is \emph{time reversible} iff $(X(t_{i}))_{1 \le i \le n}$ has the same joint distribution as
$(X(t' - t_{i}))_{1 \le i \le n}$ for all $n \in \natns_{\ge 1}$ and $t_{1} < \dots < t_{n}, t' \in
\realns_{\ge 0}$, in which case $X(t)$ and its reversed version $X^{\textrm{r}}(t) = X(t' - t)$ are
stochastically identical; in particular, $X(t)$ and $X^{\textrm{r}}(t)$ share the same steady-state
probability distribution $\bfpi$ if any. \linebreak In order for a stationary CTMC $X(t)$ to be time
reversible, it is necessary and sufficient that the \emph{partial balance equations} $\pi(s) \cdot q_{s, s'}
= \pi(s') \cdot q_{s', s}$ are satisfied for all $s, s' \in \cals$ such that $s \neq s'$ or, equivalently,
that $q_{s_{1}, s_{2}} \cdot \ldots \cdot q_{s_{n - 1}, s_{n}} \cdot q_{s_{n}, s_{1}} = q_{s_{1}, s_{n}}
\cdot q_{s_{n}, s_{n - 1}} \cdot \ldots \cdot q_{s_{2}, s_{1}}$ for all $n \in \natns_{\ge 2}$ and distinct
$s_{1}, \dots, s_{n} \in \cals$~\cite{Kelly79}.

Time reversibility of CTMC-based compositional models of concurrent systems has been investigated
in~\cite{Harrison03}. More precisely, conditions relying on the conservation of total exit rates of states
and of rate products around cycles are examined, which support the hierarchical and compositional reversal
of stochastic process algebra terms. These conditions also lead to the efficient calculation of steady-state
probability distributions in a product form typical of queueing theory~\cite{Kleinrock75}, thus avoiding the
need of solving the global balance equation system. More recently, in~\cite{MarinR15} similar conditions
have been employed to characterize the class of $\rho$-reversible stochastic automata. Under certain
constraints, the joint steady-state probability distribution of the composition of two such automata is the
product of the steady-state probability distributions of the two automata.
