Marco Bernardo

Claudio Antares Mezzina

Towards Bridging Time and Causal Reversibility

des établissements d'enseignement et de recherche français ou étrangers, des laboratoires publics ou privés.

Introduction

The interest into computation reversibility dates back to the 60's, when it was observed that irreversible computations cause heat dissipation into circuits [START_REF] Landauer | Irreversibility and heat generated in the computing process[END_REF]. This suggested that low energy consumption could be achieved by resorting to reversible computing, in which there is no information loss [START_REF] Bennett | Logical reversibility of computations[END_REF]. Nowadays, reversible computing has several applications ranging from biochemical reactions [START_REF] Pinna | Reversing steps in membrane systems computations[END_REF][START_REF] Phillips | A reversible process calculus and the modelling of the ERK signalling pathway[END_REF] and parallel discrete-event simulation [START_REF] Perumalla | Reverse computation for rollback-based fault tolerance in large parallel systems -Evaluating the potential gains and systems effects[END_REF][START_REF] Schordan | Generation of reversible C++ code for optimistic parallel discrete event simulation[END_REF] to robotics [START_REF] Laursen | Modelling reversible execution of robotic assembly[END_REF], control theory [START_REF] Siljak | Distributed antenna selection for massive MIMO using reversing Petri nets[END_REF], fault tolerant systems [START_REF] Danos | Transactions in RCCS[END_REF][START_REF] De Vries | Communicating transactions[END_REF][START_REF] Lanese | Concurrent flexible reversibility[END_REF][START_REF] Vassor | Checkpoint/rollback vs causally-consistent reversibility[END_REF], and program debugging [START_REF] Giachino | Causal-consistent reversible debugging[END_REF][START_REF] Lanese | CauDEr: A causal-consistent reversible debugger for Erlang[END_REF].

In a reversible system, we can observe two directions of computation: a forward one, coinciding with the normal way of computing, and a 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 [START_REF] Barylska | Reversible computation vs. reversibility in Petri nets[END_REF], while in distributed systems it amounts to the capability of returning to a past consistent state [START_REF] Danos | Reversible communicating systems[END_REF]. In contrast, in the performance evaluation field, reversibility is intended as time reversibility and is instrumental to develop efficient analysis methods [START_REF] Kelly | Reversibility and Stochastic Networks[END_REF].

Our focus is on the relationship between causal consistent reversibility and time reversibility, from a process algebraic perspective. On the one hand, quantitative aspects have been disregarded in the setting of causal consistent reversibility. On the other hand, the theory of time reversibility has been applied to concurrent systems without explicitly taking causality into account.

In this paper, instead, we aim at bridging these two theories, by showing how causal consistent reversibility and time reversibility can be jointly obtained. 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 [START_REF] Hillston | A Compositional Approach to Performance Modelling[END_REF], the stochastic process underlying the calculus turns out to be a continuous-time Markov chain (CTMC) [14].

The contribution of this paper is twofold. Firstly, we apply for the first time the technique of [START_REF] Phillips | Reversing algebraic process calculi[END_REF] 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. This is accomplished by importing from the reduction semantics setting of [START_REF] Danos | Reversible communicating systems[END_REF] the notion of concurrent transitions, which is new in the structural operational semantics framework of [START_REF] Phillips | Reversing algebraic process calculi[END_REF].

Secondly, after observing that the CTMC underlying the calculus is stationary, we show that time reversibility can be achieved by using, in the operational semantic rules, backward rates equal to the corresponding forward rates. This is quite different from the approaches followed for example in [START_REF] Harrison | Turning back time in Markovian process algebra[END_REF][START_REF] Marin | Quantitative analysis of concurrent reversible computations[END_REF], where time reversibility is addressed a posteriori, as we instead obtain a calculus in which time reversibility can be guaranteed by construction.

This paper is organized as follows. In Sects. 2 and 3 we recall background information about causal consistent reversibility and time reversibility, respectively. Then, in Sect. [START_REF] Cristescu | A compositional semantics for the reversible π-calculus[END_REF] we provide and illustrate our results about the integration of these two forms of reversibility in the considered stochastic process calculus. Finally, in Sect. 5 we conclude with some directions for future work.

Causal Consistent Reversibility

Reversibility in a system means the possibility of reverting the last performed action. In a sequential system, this is very simple as there exists just one last action. 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 synchronised 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 causal consistent reversibility [START_REF] Danos | Reversible communicating systems[END_REF], 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, there are two reversible variants of CCS [START_REF] Milner | Communication and Concurrency[END_REF]. The first one in time order, RCCS [START_REF] Danos | Reversible communicating systems[END_REF], uses stack-based memories attached to processes to record all the actions executed by the processes themselves. In contrast, [START_REF] Phillips | Reversing algebraic process calculi[END_REF] proposes a general method, of which CCSK is a result, to reverse calculi whose operational semantic rules are expressed in the path format [START_REF] Baeten | A congruence theorem for structured operational semantics with predicates[END_REF]. 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. Note that, since dynamic operators such as prefixing and choice are forgetful by definition, making them static avoids information loss during a reduction.

Despite these two approaches may seem different, they have been shown to be equivalent in terms of labeled transition system isomorphism [START_REF] Lanese | Static versus dynamic reversibility in CCS[END_REF]. The approach of [START_REF] Danos | Reversible communicating systems[END_REF] is more suitable for systems whose operational semantics is given in terms of reduction semantics, hence its application is to be preferred in the case of very expressive calculi [START_REF] Lanese | Reversing higher-order π[END_REF][START_REF] Cristescu | A compositional semantics for the reversible π-calculus[END_REF] as well as programming languages [START_REF] Lienhardt | A reversible abstract machine and its space overhead[END_REF][START_REF] Lanese | A theory of reversibility for Erlang[END_REF]. On the other hand, the approach of [START_REF] Phillips | Reversing algebraic process calculi[END_REF] is very handy when it comes to deal with labeled transition systems and CCS-like calculi, which is the case of this paper.

For example, given the process P + Q, from P α -→ P we derive P + Q α -→ P . If we assume the possibility of reverting action α, i.e., P αr -→ P , we have that P gets back to a state in which the information about the choice operator and Q is lost. To avoid this, in [START_REF] Phillips | Reversing algebraic process calculi[END_REF] + Q is treated as a dead decoration of process P . In this way, the use of explicit memories of [START_REF] Danos | Reversible communicating systems[END_REF] is avoided because the necessary information is syntactically maintained within processes.

Time Reversibility

In the field of performance evaluation, a different notion of reversibility, called time reversibility, is considered. We illustrate it in the specific case of continuoustime Markov chains, which are discrete-state stochastic processes characterized by the memoryless property [14].

A 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 S for t ∈ R ≥0 is a continuous-time Markov chain (CTMC) iff for all n ∈ N, time instants

t 0 < t 1 < • • • < t n < t n+1 ∈ R ≥0 , and states s 0 , s 1 , . . . , s n , s n+1 ∈ S it holds that Pr{X(t n+1 ) = s n+1 | X(t i ) = s i , 0 ≤ i ≤ n} = Pr{X(t n+1 ) = s n+1 | 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 irreducible iff each of its states can be reached from every other state. A state s ∈ S is recurrent iff the CTMC will eventually return to s with probability 1, in which case s is called positive recurrent iff the expected number of steps until the CTMC returns to it is finite. A CTMC is 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 stateindexed 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 time-homogeneous CTMCs, in which conditional probabilities of the form Pr{X(t + t ) = s | X(t) = s} do not depend on t, so that the considered information is simply a positive real number. This is called the 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 ∈ S 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 stationary, which means that (X(t i + t )) 1≤i≤n has the same joint distribution as (X(t i )) 1≤i≤n for all n ∈ N ≥1 and t 1 < • • • < t n , t ∈ R ≥0 . Specifically, X(t) has a unique steady-state probability distribution π that for all s ∈ S fulfills π(s) = lim t→∞ Pr{X(t) = s | X(0) = s } for any s ∈ S. These probabilities can be computed by solving the linear system of global balance equations π • Q = 0 subject to s∈S π(s) = 1 and π(s) ∈ R >0 for all s ∈ S. The infinitesimal generator matrix 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 =s =s q s,s for all s ∈ S so that every row of Q sums up to 0.

Due to state space explosion and numerical stability problems [START_REF] Stewart | Introduction to the Numerical Solution of Markov Chains[END_REF], 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 time reversible iff (X(t i )) 1≤i≤n has the same joint distribution as (X(t -t i )) 1≤i≤n for all n ∈ N ≥1 and t 1 < • • • < t n , t ∈ R ≥0 , in which case X(t) and its reversed version X r (t) = X(t -t) are stochastically identical; in particular, X(t) and X r (t) share the same steady-state probability distribution π if any. In order for a stationary CTMC X(t) to be time reversible, it is necessary and sufficient that the partial balance equations π(s) • q s,s = π(s ) • q s ,s are satisfied for all s, s ∈ S such that s = s or, equivalently, that q s1,s2 • . . . • q sn-1,sn • q sn,s1 = q s1,sn • q sn,sn-1 • . . . • q s2,s1 for all n ∈ N ≥2 and distinct s 1 , . . . , s n ∈ S [START_REF] Kelly | Reversibility and Stochastic Networks[END_REF].

Time reversibility of CTMC-based compositional models of concurrent systems has been investigated in [START_REF] Harrison | Turning back time in Markovian process algebra[END_REF]. 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 [START_REF] Kleinrock | Queueing Systems[END_REF], thus avoiding the need of solving the global balance equation system. More recently, in [START_REF] Marin | Quantitative analysis of concurrent reversible computations[END_REF] similar conditions have been employed to characterize the class of ρ-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.

Integrating Causal and Time Reversibility

In this section, we integrate the two concepts of causal consistent reversibility and time reversibility recalled in the previous two sections. To do so, 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 the approach of [START_REF] Phillips | Reversing algebraic process calculi[END_REF]. Then, we show that the reversibility induced by RMPC is causal consistent by importing the notion of concurrent transitions from [START_REF] Danos | Reversible communicating systems[END_REF]. 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 [START_REF] Harrison | Turning back time in Markovian process algebra[END_REF][START_REF] Marin | Quantitative analysis of concurrent reversible computations[END_REF].

Syntax and Semantics for RMPC

The syntax of RMPC is shown in Table 1. A forward process P can be one of the following: the idle process 0; the prefixed process (a, λ).P , which is able to perform an action a at rate λ and then continues as process P ; the nondeterministic choice P + Q between processes P and Q; or the cooperation P L Q, indicating that processes P and Q execute in parallel and must synchronise only on actions prescribed by the set L.

A reversible process R is built on top of forward processes. As in [START_REF] Phillips | Reversing algebraic process calculi[END_REF], the syntax of reversible processes differs from the one of forward processes by the fact that in the former each prefix (a, λ) can be decorated with a communication key i thus becoming (a, λ) [i]. A process of the form (a, λ)[i].R expresses that in the past the process synchronised with the environment and this synchronisation was identified by key i. Keys are thus attached only to already executed actions.

P, Q ::= 0 | (a, λ).P | P + Q | P L Q R, S ::= P | (a, λ)[i].R | R + S | R L S Table 1. Syntax of RMPC forward/standard/

initial processes and reversible processes

Let A be the set of actions such that a, b ∈ A, R = R >0 be the set of rates such that λ, µ ∈ R, and K be the set of keys such that i, j ∈ K. Let L = A×R×K be the set of labels each formed by an action, a rate, and a communication key. We let and its decorated versions range over L. Moreover, given a forward label = (a, λ)[i], we denote by = (a, λ)[i] the corresponding backward label. Finally, P is the set of processes generated by the production for R in Table 1.

Definition 1 (standard process). Process R ∈ P is standard, written std(R), iff it can be derived from the production for P in Table 1.

Definition 2 (process key). The set of keys of process R ∈ P, written key(R), is inductively defined as follows:

key(P ) = ∅ key((a, λ)[i].R) = {i} ∪ key(R) key(R + S) = key(R) ∪ key(S) key(R L S) = key(R) ∪ key(S)
The semantics for RMPC is defined as a labeled transition system (P, L, -→). Like in [START_REF] Phillips | Reversing algebraic process calculi[END_REF], the transition relation -→ ⊆ P × L × P is given by -→ ∪ , where the forward transition relation -→ and the backward transition relation are the least relations respectively induced by the forward rules in the left part and the backward rules in the right part of Table 2.

Act1 std(R) (a, λ).R (a,λ)[i] ----→ (a, λ)[i].R Act1 • std(R) (a, λ)[i].R (a,λ)[i] (a, λ).R Act2 R (b,µ)[j] ----→ R j = i (a, λ)[i].R (b,µ)[j] ----→ (a, λ)[i].R Act2 • R (b,µ)[j] R j = i (a, λ)[i].R (b,µ)[j] (a, λ)[i].R Cho R (a,λ)[i] ----→ R std(S) R + S (a,λ)[i] ----→ R + S Cho • R (a,λ)[i] R std(S) R + S (a,λ)[i] R + S Par R (a,λ)[i] ----→ R a / ∈ L i / ∈ key(S) R L S (a,λ)[i] ----→ R L S Par • R (a,λ)[i] R a / ∈ L i / ∈ key(S) R L S (a,λ)[i] R L S Coo R (a,λ)[i] ----→ R S (a,µ)[i] ----→ S a ∈ L R L S (a,λ•µ)[i] ------→ R L S Coo • R (a,λ)[i] R S (a,µ)[i] S a ∈ L R L S (a,λ•µ)[i] R L S Table 2.
Structural operational semantic rules for RMPC Rule Act1 deals with prefixed processes of the form (a, λ).P , with P written as R subject to std(R). In addition to transforming the action prefix into a transition label, it generates a fresh key i, which is bound to the action (a, λ) thus yielding the label (a, λ)[i]. As we can note, the prefix is not discarded by the application of the rule, instead it becomes a key-storing decoration in the target process. Rule Act1 • reverts the action (a, λ)[i] of the process (a, λ)[i].R provided that R is a standard process, which ensures that (a, λ)[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 λ of the backward action is calculated. For the time being, we leave it unspecified in Act1 • as the value of this rate is not necessary to prove the causal consistency part of reversibility, but as we will see later on it is important in the proof of time reversibility.

The presence of rules Act2 and Act2 • is motivated by the fact that rule Act1 does not discard the executed prefix from the process it generates. In particular, rule Act2 allows a prefixed process (a, λ)[i].R to execute if R can itself execute, provided that the action performed by R picks a key j different from i. Rule Act2 • simply propagates the execution of backward actions from inner subprocesses that are not standard as long as key uniqueness is preserved.

Unlike the classical rules of the choice operator [START_REF] Milner | Communication and Concurrency[END_REF], rule 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 + S does an action, say (a, λ)[i], and becomes R , then the entire process 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 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 Cho • has precisely the same structure as rule 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 cooperation is inspired by [START_REF] Hoare | Communicating Sequential Processes[END_REF]. Rule Par allows process R within R L S to individually perform an action (a, λ)[i], provided that a / ∈ L. Rule Coo allows R and S to cooperate 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 [START_REF] Hillston | The nature of synchronisation[END_REF]. Rules Par Not all the processes generated by the grammar in Table 1 are meaningful as, e.g., there might be several action prefixes sharing the same key in a sequential process, i.e., a process without occurrences of the cooperation operator. We only consider processes that are initial or reachable in the following sense: Definition 3 (initial and reachable process). Process R ∈ P is initial iff std(R) holds. Process R ∈ P is reachable iff it is initial or can be derived from an initial one via finitely many applications of the rules for -→ in Table 2.

Properties Preliminary to Reversibility

A basic property to satisfy in order for RMPC to be reversible is the so called loop lemma [START_REF] Danos | Reversible communicating systems[END_REF][START_REF] Phillips | Reversing algebraic process calculi[END_REF], 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. Formally: Lemma 1 (loop lemma). Let R ∈ P be a reachable process. Then R

(a,λ)[i] ----→ S iff S (a,λ)[i] R.
Proof. We proceed by induction on the depth of the derivation of R

(a,λ)[i] ----→ S (resp., S (a,λ)[i]
R), by noticing that for each forward (resp., backward) rule there exists a corresponding backward (resp., forward) one.

The lemma generalizes as follows. For any sequence σ of n ∈ N >0 labels

1 , . . . , n , let R σ -→ S be the corresponding forward sequence of transitions R 1 -→ R 1 2 -→ • • • n
-→ S and σ be the corresponding backward sequence such that, for each i occurring in σ, it holds that R i-

1 i -→ R i iff R i i R i-1 .
A direct consequence of the loop lemma is the following:

Corollary 1. Let R ∈ P be a reachable process. Then R σ -→ S iff S σ -→ R.

Causal Consistent Reversibility for RMPC

In order to prove the causal consistent reversibility of RMPC, we borrow some machinery from [START_REF] Danos | Reversible communicating systems[END_REF] that needs to be adapted as the reversing method of [START_REF] Phillips | Reversing algebraic process calculi[END_REF] we are using is different from the one of [START_REF] Danos | Reversible communicating systems[END_REF]. In particular, we import the notion of concurrent transitions.

Given a transition θ : R -→ S with R, S ∈ P reachable processes, we call R the source of θ and S its target. Two transitions are said to be coinitial if they have the same source, and cofinal if they have the same target. A sequence of pairwise composable transitions is called a computation, where composable means that the target of any transition in the sequence is the source of the next transition. We let θ and its decorated variants range over transitions, while ω and its decorated variants range over computations. If θ is a forward transition, i.e., θ : R -→ S, we denote its backward version S R as θ. The notions of source, target, and composability extend naturally to computations. We indicate with R the empty computation whose source is R and with ω 1 ; ω 2 the composition of two composable computations ω 1 and ω 2 .

Before specifying when two transitions are concurrent, we need to define the set of causes -identified by keys -of a given communication key. Definition 4 (causal set). Let R ∈ P be a reachable process and i ∈ key(R). The causal set cau(R, i) is inductively defined as follows for j = i:

cau((a, λ)[i].R, i) = ∅ cau((a, λ)[j].R, i) = {j} ∪ cau(R, i) cau(R + S, i) = cau (R, i) ∪ cau (S, i) cau(R L S, i) = cau (R, i) ∪ cau (S, i) where cau (R, i) = cau(R, i) if i ∈ key(R) and cau (R, i) = ∅ otherwise.
If i ∈ key(R), then cau(R, i) represents the set of keys in R that caused i, with cau(R, i) ⊂ key(R) since i / ∈ 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. We are now in place to define what we mean by concurrent transitions: Definition 5 (concurrent transitions). Two coinitial transitions θ 1 and θ 2 from a reachable process R ∈ P are in conflict iff one of the following holds:

1. θ 1 : R (a,λ)[j] -----→ S 1 and θ 2 : R (b,µ)[i] S 2 with i ∈ cau(S 1 , j). 2. R = R 1 + R 2 with θ k deriving from R k (a k ,λ k )[i k ] -------→ S k for k = 1, 2.
Two coinitial transitions are concurrent when they are not in conflict.

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 1 shows two related examples. In the first case, the process (a, λ)[i].(b, µ).P can perform two transitions: a backward one and a forward one. They meet the first condition of Definition 5 as the backward transition removes the key i that is in the causal set of j. In the second case, we have that process (a, λ).P + (a, λ).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 5.

Remark 1. It is worth noting that in a stochastic process calculus like RMPC the semantic treatment of the choice operator is problematic [START_REF] Hillston | A Compositional Approach to Performance Modelling[END_REF] because a process of the form (a, λ).P + (a, λ).P should produce either a single a-transition whose rate is λ + λ, or two a-transitions each having rate λ 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 1.

(a, λ).(b, µ).P (a, λ)[i].(b, µ).P (a,λ)[i] 5 5 (b,µ)[j] / / (a, λ)[i].(b, µ)[j].P (a, λ).P + (a, λ).P (a,λ)[i] u u (a,λ)[i]
) ) Concurrent transitions can commute, while conflicting ones cannot. Formally:

Lemma 2 (diamond lemma). Let θ 1 : R 1 -→ S 1 and θ 2 : R 2 -→ S 2 be two coinitial transitions from a reachable process R ∈ P. If θ 1 and θ 2 are concurrent, then there exist two cofinal transitions

θ 2 /θ 1 : S 1 2 -→ S and θ 1 /θ 2 : S 2 1 -→ S.
Proof. By case analysis on the form of θ 1 and θ 2 .

We are now in a position to show that reversibility in our framework is causally consistent. Following [START_REF] Lévy | An algebraic interpretation of the λβK-calculus; and an application of a labelled λ-calculus[END_REF], we first define a notion of causal equivalence between computations that abstracts from the order of concurrent transitions. We formalize as the least equivalence relation over computations that is closed under composition and obeys the following rules:

θ 1 ; θ 2 /θ 1 θ 2 ; θ 1 /θ 2 θ; θ source(θ) θ; θ target(θ)
Equivalence states that if we have two concurrent transitions, then the two computations obtained by swapping the order of their execution are the same, and that any computation composed by a transition followed by its inverse is equivalent to the empty computation. The proof of causal consistency relying on follows that of [START_REF] Danos | Reversible communicating systems[END_REF], although the arguments are different due to the fact that the notion of concurrent transitions is formalized differently.

The following lemma says that, up to causal equivalence, one can always reach for the maximum freedom of choice among transitions, meaning that it is possible to undo all the executed actions and then restart.

Lemma 3 (rearranging lemma). For any computation ω there exist two forward computations ω 1 and ω 2 such that ω ω 1 ; ω 2 .

Proof. By induction on the length of ω and on the distance (intended as number of transitions) between the beginning of ω and the earliest pair of consecutive transitions in ω such that the former is forward while the latter is backward. The analysis uses both the loop lemma (Lemma 1) and the diamond lemma (Lemma 2).

The following lemma says that if two computations ω 1 and ω 2 are coinitial and cofinal and ω 2 is made of forward transitions only, then in ω 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. Lemma 4 (shortening lemma). Let ω 1 and ω 2 be coinitial and cofinal computations, with ω 2 forward. Then there exists a forward computation ω 1 of length at most that of ω 1 such that ω 1 ω 1 .

Proof. The proof is by induction on the length of ω 1 , using the diamond lemma (Lemma 2) and the rearranging lemma (Lemma 3). In the proof, the forward computation ω 2 is the main guideline for shortening ω 1 into a forward computation. Indeed, the proof relies crucially on the fact that ω 1 and ω 2 share the same source and the same target and that ω 2 is a forward computation.

Theorem 1 (causal consistency). Let ω 1 and ω 2 be coinitial computations. Then ω 1 ω 2 iff ω 1 and ω 2 are cofinal too.

Proof. The 'if' direction follows by definition of causal equivalence and computation composition. The 'only if' direction exploits the diamond lemma (Lemma 2), the rearranging lemma (Lemma 3), and the shortening lemma (Lemma 4).

With Theorem 1 we have proved that the notion of causal equivalence characterises a space for admissible rollbacks that are (i) consistent in the sense that 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. We can therefore conclude that RMPC is causal consistent reversible.

Time Reversibility for RMPC

The rules in Table 2 associate with any initial process R ∈ P a labeled transition system R = (P, L, -→, R). To investigate time reversibility, we have to derive from R the CTMC M R underlying R and we have to specify how each backward rate λ is obtained from the corresponding forward rate λ.

First of all, we observe that every non-terminal state of R has infinitely many outgoing transitions. The reason is that rules Act1 and 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, λ)-transition in the case of a process like (a, λ).P + (a, λ).P whose overall exit rate is λ + λ; even if the key is the same, two different states (a, λ)[i].P + (a, λ).P and (a, λ).P + (a, λ)[i].P are reached. On the other hand, it requires considering transition bundles to build M R .

We call transition bundle 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. Formally, we denote by ≡ K the least equivalence relation over P induced by (a, λ)[i].S ≡ K (a, λ)[j].S. We then define the CTMC underlying an initial process R ∈ P as the labeled transition system

M R = (P/ ≡ K , A × R, - → K , [R] ≡ K )
where:

-P/ ≡ K is the quotient set of ≡ K over P, i.e., the set of classes of processes that are equivalent to each other according to ≡ K . -[R] ≡ K is the equivalence class of R with respect to ≡ K , which simply is the singleton set {R} as R is initial and hence contains no keys. --→ K ⊆ P/ ≡ K ×(A×R)×P/ ≡ K is the transition relation given by

-→ K ∪ K such that [R] ≡ K (a,λ) ---→ K [R ] ≡ K whenever R (a,λ)[i] ----→ R for some i ∈ K and [R] ≡ K (a,λ) K [R ] ≡ K whenever R (a,λ)[i]
R for some i ∈ K.

When moving from R to M R , individual states are 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 M R turns out to have finitely many outgoing transitions. We also note that M R is an 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 M R is stationary. It holds that M R is even ergodic thanks to the loop lemma.

Lemma 5. Let R ∈ P be an initial process. Then M R is time homogeneous and ergodic.

Proof. The time homogeneity of M R is a straightforward consequence of the fact that its rates simply are positive real numbers, not time-dependent functions. The ergodicity of M R stems from the fact that the graph representation of the considered CTMC is a finite, strongly connected component due to Cor. 1.

We exploit once more the loop lemma to derive that, in the case that λ = λ, the steady-state probability distribution of M R is the uniform distribution, from which time reversibility will immediately follow. Lemma 6. Let R ∈ P be an initial process, S be the set of states of M R , and n = |S|. If every backward rate is equal to the corresponding forward rate, then the steady-state probability distribution π of M R satisfies π(s) = 1/n for all s ∈ S.

Proof. If n = 1, i.e., R is equal to 0 or to the cooperation of several processes whose initial actions have to synchronize but are different from each other, then trivially π(s) = 1/n = 1 for the only state s ∈ S. Suppose now that n ≥ 2. From Lemma 5, it follows that M R has a unique steady-state probability distribution π. Due to Lemma 1, the global balance equation for an arbitrary s ∈ S is as follows:

π(s) • s (a,λ) ---→ K s λ = s (a,λ) ---→ K s π(s ) • λ
Since every backward rate is equal to the corresponding forward rate, the global balance equation for s boils down to:

π(s) • s (a,λ) ---→ K s λ = s (a,λ) ---→ K s π(s ) • λ
Since the two summations have the same number of summands, the equation above is satified when π(s) = π(s ) for all s ∈ S reached by a transition from s.

All global balance equations are thus satisfied when π(s) = 1/n for all s ∈ S.

Theorem 2 (time reversibility). Let R ∈ P be an initial process. If every backward rate is equal to the corresponding forward rate, then M R is time reversible.

Proof. Let S be the set of states of M R and n = |S|. From Lemma 5, it follows that M R has a unique steady-state probability distribution π. To avoid trivial cases, suppose n ≥ 2 and consider s, s ∈ S with s = s connected by a transition. Due to Lemma 1, the partial balance equation for s and s is as follows:

π(s) • s (a,λ) ---→ K s λ = π(s ) • s (a,λ) ---→ K s λ
Since every backward rate is equal to the corresponding forward rate, the partial balance equation for s and s boils down to:

π(s) • s (a,λ) ---→ K s λ = π(s ) • s (a,λ) ---→ K s λ
Since the two summations have the same number of summands and π(s) = π(s ) = 1/n due to Lemma 6, the equation above is satified. The result then follows from the fact that s and s are two arbitrary distinct states connected by a transition.

The main difference between our approach to time reversibility and the ones of [START_REF] Harrison | Turning back time in Markovian process algebra[END_REF][START_REF] Marin | Quantitative analysis of concurrent reversible computations[END_REF] 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 [START_REF] Phillips | Reversing algebraic process calculi[END_REF] 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 [START_REF] Harrison | Turning back time in Markovian process algebra[END_REF] or verifying a posteriori whether a given model is time reversible or not like in [START_REF] Marin | Quantitative analysis of concurrent reversible computations[END_REF].

It is worth noting that these methodological differences do not prevent us from adapting to our setting some results from [START_REF] Harrison | Turning back time in Markovian process algebra[END_REF][START_REF] Marin | Quantitative analysis of concurrent reversible computations[END_REF], although a few preliminary observations about notational differences are necessary.

Both [START_REF] Harrison | Turning back time in Markovian process algebra[END_REF] and [START_REF] Marin | Quantitative analysis of concurrent reversible computations[END_REF] 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 [START_REF] Marin | Quantitative analysis of concurrent reversible computations[END_REF] synchronization is enforced between any active-passive pair of identical actions, whereas in RMPC the cooperation 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 A of all the actions. We can therefore conclude that our cooperation operator is a generalization of those used in [START_REF] Harrison | Turning back time in Markovian process algebra[END_REF][START_REF] Marin | Quantitative analysis of concurrent reversible computations[END_REF], hence the recalled notational differences do not hamper result transferral.

In [START_REF] Harrison | Turning back time in Markovian process algebra[END_REF] the compositionality of a CTMC-based stochastic process calculus is exploited to prove the reversed compound agent theorem (RCAT), 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 [START_REF] Jackson | Jobshop-like queueing systems[END_REF].

In [START_REF] Marin | Quantitative analysis of concurrent reversible computations[END_REF] the notion of ρ-reversibility is introduced for stochastic automata, which are essentially action-labeled CTMCs. Function ρ is a state permutation that ensures (i) for each action the equality of the total exit rate of any state s and ρ(s) and (ii) the conservation of action-related rate products across cycles when considering states in the forward direction and their ρ-counterparts in the backward direction. For any ergodic ρ-reversible automaton, it turns out that π(s) = π(ρ(s)) for every state s. Moreover, the synchronization inspired by [START_REF] Plateau | On the stochastic structure of parallelism and synchronization models for distributed algorithms[END_REF] of two ρ-reversible stochastic automata is still ρ-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 [START_REF] Marin | Quantitative analysis of concurrent reversible computations[END_REF] in terms of ρ-reversibility with ρ being the identity function over states. As a consequence, the following two results stem from Theorem 2 of the present paper and, respectively, Theorems 2 and 3 of [START_REF] Marin | Quantitative analysis of concurrent reversible computations[END_REF]:

Corollary 2 (time reversibility closure). Let R, S ∈ P be initial processes and L ⊆ A. If every backward rate is equal to the corresponding forward rate, then M R L S is time reversible too.

Corollary 3 (product form). Let R, S ∈ P be initial processes and L ⊆ A. If every backward rate is equal to the corresponding forward rate and the set of states S of M R L S is equal to S R × S S where S R is the set of states of M R and S S is the set of states of M S , then π(r, s) = π R (r) • π S (s) for all (r, s) ∈ S R × S S .

The product form result above avoids the calculation of the global balance equations over M R L S , as π(r, s) can simply be obtained by multiplying π R (r) with π S (s). However, the condition S = S R × S S requires to check that every state in the full Cartesian product is reachable from R L S. 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 S = S R × S S implies that M R L S is ergodic over the full Cartesian product of the two original state spaces, which is the condition used in [START_REF] Marin | Quantitative analysis of concurrent reversible computations[END_REF]. Although implicit in the statement of the corollary, the time reversibility of M R L S is essential for the product form result.

Conclusions

Different interpretations of reversibility are present in the literature. In this paper, we have started our research quest towards bridging causal consistent reversibility [START_REF] Danos | Reversible communicating systems[END_REF] -developed in concurrency theory -and time reversibility [START_REF] Kelly | Reversibility and Stochastic Networks[END_REF] -originated in the field of stochastic processes. We have accomplished this by introducing the stochastic process calculus RMPC, whose syntax and semantics follow the approach of [START_REF] Phillips | Reversing algebraic process calculi[END_REF], thus paving the way to concurrent system models that are both causal consistent reversible and time reversible by construction. Based on time reversibility, we have also adapted from [START_REF] Marin | Quantitative analysis of concurrent reversible computations[END_REF] a product form result that enables the efficient calculation of performance measures.

There are several lines of research that we plan to undergo, ranging from the application of our results to examples and case studies modeled with RMPC to the development of further theoretical results. For instance, we would like to investigate other conditions under which time reversibility is achieved, in addition to the one relying on the equality of forward and backward rates.

Moreover, we observe that the syntax of RMPC does not include recursion. From the point of view of the ergodicity of the underlying CTMC, this 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 (a, λ).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 communications keys to keep track of past actions, which may avoid the generation of an infinite state space in the presence of recursion.

  • and Coo • respectively have the same structure as Par and Coo; the symmetric variants of Par and Par • are omitted.

Fig. 1 .

 1 Fig. 1. Examples of conflicting transitions

Acknowledgement. We would like to thank Andrea Marin for the valuable discussions on time reversibility. The second author has been partially supported by the French ANR project DCore ANR-18-CE25-0007 and by the Italian INdAM -GNCS project 2020 Reversible Concurrent Systems: From Models to Languages.