Clément Aubert
email: aubertc@appstate.edu

Ioana Cristescu
email: ioana.cristescu@pps.univ-paris-diderot.fr

Contextual equivalences in configuration structures and reversibility

Keywords: Formal semantics, Process algebras and calculi, Reversible CCS, Hereditary history preserving bisimulation, Strong barbed congruence, Contextual characterization, 2000 MSC: 68Q85 Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) 2012 MSC: [Theory of computation] -Semantics and reasoning -Program semantics -Algebraic semantics, [Software

Introduction

Reversibility

Being able to reverse a computation is an important feature of computing systems. Reversibility is a key aspect in every system that needs to achieve distributed consensus [START_REF] Bougé | On the existence of symmetric algorithms to find leaders in networks of communicating sequential processes[END_REF] to escape local states where the consensus cannot be found. In such problems, multiple computing agents have to reach a common solution. Allowing independent agents to backtrack and explore the solution space enables them to reach a globally accepted state if given enough time and if a common solution exists. For example, the dining philosophers problem [START_REF] Hoare | Communicating Sequential Processes[END_REF] requires a backtracking mechanism to prevent deadlocks. Rewinding a computation step by step is also a common way to debug programs. In such settings the step by step approach is often more useful than restarting the program from an initial state.

Importantly, the backtracking mechanism can be integrated to the operational semantics of a programming language, instead of adding a tailor-made implementation on top of each program. Constructing a formal model for reversible concurrent systems require to address two challenges. The first one consists in recording the information needed for backtracking: processes carry a memory that keeps track of everything that has been done.

Importantly the needed information to backtrack is recorded in a distributed fashion instead of using a centralized store, which could be a bottleneck for the computation. The second challenge we need to address for designing a reversible models consists in implementing an optimal notion of legitimate backward moves. In a sequential program, one backtracks computations in the opposite order to the execution. However, in a concurrent setting, we do not want to undo the actions precisely in the opposite order than the one in which they were executed, as this order may not materialize. The concurrency relation between actions has to be taken into account. It can be argued that the most liberal notion of reversibility is the one that just respects causality: an action can be undone precisely after all the actions that causally depend on it have also been undone. Then an acceptable backward path is causally consistent with the forward computation.

There are different accounts of reversible operational semantics, RCCS [START_REF] Danos | Reversible communicating systems[END_REF][START_REF] Danos | Self-assembling trees[END_REF] and CCSK [START_REF] Phillips | Reversibility and models for concurrency[END_REF] being the two main propositions for a reversible CCS. In these works, reversibility is embedded into a (classical) process calculus.

Causal models

In interleaving models, the internal relations between different events cannot be observed. In particular, causality is not treated as a primitive concept. On the other hand, non-interleaving semantics have a primitive notion of concurrency between computation events. As a consequence one can also derive a causality relation, generally defined as the complement of concurrency. These models are therefore sometimes called true-concurrent or causal or, if causality is represented as a partial order on events, partial order semantics. 2A causal model is often an alternative representation of an existing interleaving semantics that helps in understanding the relations between computations in the latter. Usually in such models, sets of events are considered computational states. Each set, called a configuration, represents a reachable state in the run of the process. The behaviour of a system is encoded as a collection of such sets. The set inclusion relation between the configurations stands for the possible paths followed by the execution. Concurrency and causality are derivable from set inclusion. In their generality, such models are called configuration structures [START_REF] Van Glabbeek | Configuration structures, event structures and petri nets[END_REF], they are a syntax-free and causal model that can interpret multiple calculi.

Stable families [START_REF] Winskel | Event structures[END_REF] are configuration structures equipped with a set of axioms, that capture the intended behaviour of a CCS process. Morphisms of stable families capture sub-behaviours of processes and form a category of stable families. Process combinators correspond then to universal constructions in this category. The correspondence with CCS is established through an operational semantics defined on stable families, abusively named in that context configuration structures as well.

Behavioural equivalence

Behavioural equivalences are a major motivation in the study of formal semantics. For instance, one wants to verify that the execution of a program satisfies its expected behaviour, or that binaries obtained from the same source code, but with different compilation techniques, behave the same. Thus the interesting equivalences equate terms that behave the same. Moreover the equivalence should be a congruence: two processes are equivalent if they behave similarly in any context. Loosely speaking it aims at identifying process that have a common external behaviour in any environment.

Equivalences defined on reduction semantics are often hard to prove. A proof technique in this case is to define a LTS-based equivalence that is equivalent with the reduction-based one and carry the proofs in LTS semantics.

Behavioural equivalences are defined on the operational semantics and thus cannot access the structure of a term. The observations one does during the execution of a process are called the observables of the relation. For instance one observes whether the process terminates or whether it interacts with the environment [START_REF] Honda | On reduction-based process semantics[END_REF].

Causality and reversibility

Causality and reversibility are tightly connected notions [START_REF] Danos | Reversible communicating systems[END_REF][START_REF] De Nicola | Back and forth bisimulations[END_REF]. Causal consistency is a correctness criterion for reversible computations. Therefore whenever a reversible semantics is proposed, the calculus has to be equipped first with a causal semantics.

Notably the connection between reversibility and causality is useful to define meaningful reversible equivalences. Causal equivalences are more discriminating than the traditional operational ones. However on a reversible operational semantics one defines equivalences of the same expressivity. Causal equivalences have been extensively studied [START_REF] Phillips | A hierarchy of reverse bisimulations on stable configuration structures[END_REF][START_REF] Bednarczyk | Hereditary history preserving bisimulations or what is the power of the future perfect in program logics[END_REF][START_REF] Baldan | A logic for true concurrency[END_REF][START_REF] Vogler | Bisimulation and action refinement[END_REF]. Of particular interest is the hereditary history preserving bisimulation, which was shown to correspond to a LTS-based equivalence for a reversible CCS [START_REF] Phillips | Reversibility and models for concurrency[END_REF].

Equivalences on configuration structures

In CCS, equivalences are defined only on forward transitions and are therefore inappropriate to study reversible processes.

A reversible bisimulation [START_REF] Lanese | Reversing higher-order pi[END_REF] is more adapted but it is not contextual. We introduce a contextual equivalence on RCCS by adapting the notions of contexts and barbs to the reversible setting. The resulting relation, called barbed backand-forth congruence is defined similarly to the barbed congruence of CCS except that the backwards reductions are also observed.

Configuration structures provide a causal semantics for CCS. Equivalences on configuration structures are more discriminating than the ones on the operational setting. It is possible to move up and down in the lattice, whereas in the operational semantics, only forward transitions have to be simulated. As an example, consider the processes a | b and a.b + b.a that are bisimilar in CCS but whose causal relations between events differ.

In particular we are interested in hereditary history preserving bisimulation (HHPB) in Definition 25, which equates configuration structures that simulate each others' forward and backward moves. Phillips and Ulidowski [START_REF] Phillips | A hierarchy of reverse bisimulations on stable configuration structures[END_REF] showed that the back-and-forth bisimulation corresponds to HHPB, that can be defined in an operational setting thanks to reversibility. Allowing both forward and backward transitions gives to the operational world the discriminating power of causal models. We show that HHPB also corresponds to a congruence on RCCS, the barbed back-and-forth congruence. It is the a contextual characterization of HHPB which implies a contextual equivalence in configuration structures.

Outline

We begin by recalling notions on LTS and CCS, as well as their so-called reversible variants (Sect. 1). RCCS (Sect. 1.2) is then proven to be a conservative extension of CCS over the traces: there is a strong bisimulation between a reversible process and a "classical", memory-less, process (Lemma 3). Lastly, we adapt the usual CCS notions of contexts, barbs, and barbed congruence to RCCS (Sect. 1.3), thus introducing the back-and-forth barbed congruence (Definition 14).

We next introduce the encoding of reversible process as configuration structures (Sect. 2). We recall the classical definitions (Sect. 2.1) as well as the encoding of CCS terms as configuration structures (Sect. 2.2). Encoding of RCCS terms is built on top of this previous encoding (Sect. 2.3), and an operational correspondence between reversible processes and their encodings is proven (Lemma 6).

Finally, we introduce a notion of context for configuration structures (Sect. 3.1) and study the relation induced on configuration structures by the barbed backand-forth congruence (Sect. 3.2). In Sect. 3.3 we introduce the hereditary history preserving bisimilarity and provide a characterization by inductive relations. Lastly, we show in Sect. 3.4 that HHPB is a congruence (Proposition 9) and that whenever two configuration structures are barbed back-and-forth congruent, they also are hereditary history preserving bisimilar (Theorem 2).

Our main contribution is proving that barbed congruence in RCCS corresponds to hereditary history preserving bisimulation, which is defined on configuration structures. As a consequence, it provides a contextual characterization of equivalences defined in non-interleaving semantics.

Limitations

Our work is restrained to processes that forbid "auto-concurrency" and "autoconflict" (Definition 26). We do not cover recursion, though a treatment of recursion in configuration structures exists [START_REF] Winskel | Event structures[END_REF]. "Irreversible" action is a feature of RCCS [START_REF] Danos | Reversible communicating systems[END_REF] that is absent of our work.

We tried to stick to canonical notations and to remind of common definitions. However, we consider the reader familiar with the syntax, congruence relation and reduction rules of CCS. If not, a quick glance at a textbook [START_REF] Milner | Communication and Concurrency[END_REF] or handbook [START_REF] Winskel | Models for concurrency[END_REF] should help the reader uneasy with them.

Contextual equivalences in reversibility

Reversibility provides an implicit mechanism to undo computations. Interleaving semantics use a Labeled Transition System (LTS) to represent computations, henceforth referred to as the forward LTS. In a reversible semantics a second LTS is defined that represents the backward moves (Sect. 1.1).

RCCS [START_REF] Danos | Reversible communicating systems[END_REF][START_REF] Danos | Transactions in RCCS[END_REF][START_REF] Krivine | Algèbres de processus réversible -programmation concurrente déclarative[END_REF] (Sect. 1.2) is a reversible variant of CCS, that allows computations to backtrack, hence introducing the notions of forward and backward transitions. Memories attached to processes store the relevant information to eventually do backward steps. Without this memory, RCCS terms are essentially CCS terms (Lemma 3), but their presence forces to be precise when defining contexts and contextual equivalence for the reversible case (Sect. 1.3).

(Reversible) labeled transition systems

A label-led transition system is a multi-graph where the nodes are called states and the edges, transitions. Transitions are labeled by actions and may be fired non-deterministically.

Definition 1 (Labelled Transition System). A labeled transition system is a tuple (→, S, Act) made of a set S of states, a set Act of actions (or labels) and a relation →⊆ S × Act × S. For s, s ∈ S and a, b ∈ Act , we write s a -→ s for (s, a, s ) ∈→ and s → s if s a -→ s for some a ∈ Act.

Elements t : s a -→ s of -→ are called transitions. Two transitions, t and t are composable, written t; t , if the target of t is the source of t .

Definition 2 (Trace). A trace, denoted by σ : t 1 ; . . . ; t n is a sequence of composable transitions. Except for the empty trace, denoted , all traces have a source and a target, and can be decomposed as a transition followed by a trace. Let Act be the set of sequences in Act.

Define -→ ⊆ S × Act × S the reachability relation as follows:

s α1 -→ • • • αn -→ s ⇐⇒ ∃t 1 , .
. . , t n and s 1 , . . . , s n+1 such that

t i : s i αi -→ s i+1 and s 1 = s, s n+1 = s .
We say in that case that s is reachable from s, that s is a derivative of s, and that s is an ancestor of s .

Definition 3 (Reversible LTS). Given (-→, S, Act) and ( , S, Act) two labeled transition systems defined on the same set of states and actions, we define ( , S, Act) a third LTS by taking =-→ ∪ . By convention, a transition s -→ t is said to be forward, whereas a transition t s is said to be backward. In t s, s is an ancestor of t.

A variety of semantically different backtracking mechanisms exists, for instance,

• taking = ∅ models a language with only irreversible moves,

• in a sequential setting, if -→ draws a tree, taking = {(t, α, s) | s α -→ t} forces the backward traces to follow exactly the forward execution.

In concurrency, backward traces are allowed if their source and target are respectively the target and source of a forward trace.

Reversible CCS

A RCCS term, also called a monitored process, is a CCS process equipped with a memory. A thread is a CCS term P guarded by a memory m and denoted m P . Processes can be composed of multiple threads. The memory acts as a stack for the previous computations. Each entry in the memory is called a (memory) event and has a unique identifier. The forward transitions push events to the memories while the backward moves pop them out. Definition 4 (Names, labels and actions). We define N = {a, b, c, . . . } to be the set of names and N = {ā, b, c, . . . } its co-names. The complement of a (co-)name is given by a bijection [•] : N → N, whose inverse is also denoted by [•], so that ā = a.

A synchronization is a pair of names that complement each other, as (a, ā), and that is denoted with the special symbol τ , whose complement is undefined.

Actions are labeled using the set L = N ∪ N ∪ {τ } of (event) labels defined by the following grammar:

N ∪ N : λ, π := a ā . . . (CCS prefixes) L : α, β := τ a ā . . . (Event labels)
As it is common, we will sometimes use a and b to range over names, and call the set of names and co-names simply the set of names.

Transitions in both directions are decorated by the identifier of the associated event. Identifiers on the (partial) events are used to remember their synchronization partners. Thus to combine into a τ , the transitions need complementary labels and the same identifier.

Grammar. Consider the following process constructors, also called combinators or operators: e := i, α, P (memory events) m := ∅ .m e.m (memory stacks)

P, Q := λ.P P | Q λ.P + π.Q P \a 0 (CCS processes) R, S := m P R | S R\a (RCCS processes)
A (memory) event e = i, α, P is made of:

• An event identifier i ∈ I that tags transitions. We may think of them as pid, in the sense that they are a centrally distributed identifier attached to each transition.

• A label α that marks which action has been fired (in the case of a forward transition), or what action should be restored from the memory (in the case of a backward move).

• A backup of the whole process P that has been erased when firing a sum, or 0 otherwise.

In the memory stack, the fork symbol marks a parallel composition. The memory is then copied in two local memories, as depicted in the congruence rule called "distribution memory" in Definition 5).

Notations 1.

• We use N for the set of event identifiers I and let i, j, k range over elements of I. Forward and backward transitions will be tagged with such identifiers, and so we write

• • in:αn R n , then we write R 1 R n .
We sometimes omit the identifier in the transition. Thus we write τ -→ for the transition i:τ -→, for some i.

• As identifiers uniquely tags memory events, we'll use the identifier i to denote the unique memory event e = i, α, P of a process.

• For R a reversible process and m a memory, we denote I(m) (resp. I(R)) the set of identifiers occurring in m (resp. in R).

• The sets nm(R) of names in R, fn(R) of free names in R and bn(R) = nm(R) \ fn(R) of bound (or private) names in R are defined by extending the definition of free names on CCS terms to memories and RCCS terms:

fn(P \a) = fn(P ) \ {a} fn(a.P ) = fn(ā.P ) = {a} ∪ fn(P )

fn(P | Q) = fn(P + Q) = fn(P ) ∪ fn(Q) fn(0) = ∅ (CCS rules) fn(R\a) = fn(R) \ {a} fn(R | S) = fn(R) ∪ fn(S)
fn(m P ) = fn(P )

(RCCS rules)
We can also define the sets of name in a memory, denoted nm(m). All names occurring in a memory are free.

Remark 1 (On recording the past). To store the information needed to backtrack, RCCS attaches local memories to each thread. CCSK [START_REF] Phillips | Reversibility and models for concurrency[END_REF], a variant of CCS, simulates reductions by moving a pointer in the term, that is left unchanged. Reversible higher-order π [START_REF] Lanese | Reversing higher-order pi[END_REF] uses a centralized, global memory to store the process before a reduction. Keys are associated to each reduction, thus reverting a transition with key k consists in restoring the process associated to k from the global memory. The exact mechanism used for recording does not have an impact on the theory except for the structural rules, as we note in Remark 2.

The labeled transition system for RCCS is given by the rules of Figure 1. The null process, denoted 0, cannot perform any transition. We will often omit it, so for example we write a | b instead of a.0 | b.0. The prefix constructor a.P stands for sequential composition, the process interacts on a before continuing with P . Rules In+ (for the input) and Out+ (for the output) consumes a prefix by adding in the memory the corresponding event. The backward moves, described by the rules In-and Out-, remove an event at the top of a memory and restores the prefix and the non-deterministic sum. Those rules are presented with a (guarded) sum, but we consider for instance ∅ a.P 1:a -→ 1, a, 0 .∅ P to be a legal transition, taking a.P + 0 (which is not syntactically correct) to be a.P . Note that we are using guarded sum of two processes, but more general forms of guarded sum (as in RCCS) or even unguarded sum can be supported. We use guarded sum in order to foresee the case of weak bisimulation, which we leave as future work, but also in order to simplify the notations. Parallel composition P | Q employs the four rules of Figure 1b to derive a transition. Rules Com+ and Com-depict two process agreeing to synchronize or to undo a synchronization by providing two dual prefixes, 3 agreeing on the event identifier and triggering the transitions simultaneously. Rules ParL and ParR allow respectively the left or the right process to compute independently of the rest of the process. In those two later rules, the side condition i / ∈ I(S) ensures, in the forward direction, the uniqueness of the event identifiers and it prevents, in the backward direction, a part of a previous synchronization to backtrack alone.

In+ i / ∈ I(m) m a.P + Q i:a -→ i, a, Q .m P Out+ i / ∈ I(m) m ā.P + Q i:ā -→ i, ā, Q .m P In- i / ∈ I(m) i, a, Q .m P i:a m a.P + Q Out- i / ∈ I(m) i, ā, Q .m P i:ā m ā.P + Q (a) Prefix and sum rules R i:α -→ R S i: ᾱ -→ S Com+ R | S i:τ -→ R | S R i:α R ParL i / ∈ I(S) R | S i:α R | S R i:α R S i: ᾱ S Com- R | S i:τ R | S R i:α R ParR i / ∈ I(S) S | R i:α S | R (b) Parallel constructions R i:α R Hide a / ∈ {α, ᾱ} R\a i:α R \a R ≡ R i:α S ≡ S Congr R i:α

S (c) Hiding and congruence

Once the name a is "hidden in P ", that is, made private to the process P , it cannot be used to interact with the environment. This situation is denoted with P \a and illustrated in rule Hide. Whenever the private name a is encountered in the environment, α-renaming of a is done inside P :

P \a = α (P [b/a])\b
where P [b/a] stands for process P in which b substitutes a. We say that the hiding operator is a binder for the private name a. The grammar of reversible processes does not support the sum (R + S) or the prefix constructors (a.R), as we do not have an interpretation for such processes.

The structural congruence, whose definition follows, is applied on terms by the rule Congr. It is built on top of some of the corresponding rules for CCS, and rewrites the terms under the memory or distributes it between two forking processes.

Definition 5 (Structural congruence). Structural congruence on monitored processes is the smallest equivalence relation up to uniform renaming of identifiers generated by the:

m (P + Q) ≡ m (Q + P ) (1)
m

((P + Q) + R) ≡ m (P + (Q + R)) (2)
P = α Q m P ≡ m Q (α-conversion) m (P | Q) ≡ ( .m P | .m Q) (distribution memory)
m P \a ≡ (m P )\a with a / ∈ nm(m) (scope of restriction)

Remark 2 (On reduction semantics). Correctness criteria for reversible semantics mostly relate it with its only-forward counterpart. However one may be interested in defining a reduction semantics for the LTS of Figure 1 if only to relate RCCS with other reversible semantics for CCS. One, then needs a congruence relation on RCCS terms that has the monoid structure for parallel composition and the null process 0. However, due to the fork constructor, the associativity does not hold:

(R 1 |R 2 )|R 3 ≡ R 1 |(R 2 |R 3 ).
3 Notice that since the complement of τ is not defined, only inputs and outputs synchronize.

Other reversible calculi, in particular the reversible higher-order π-calculus [START_REF] Lanese | Reversing higher-order pi[END_REF] fares better: its congruence relation respects associativity, thanks to a mechanism that uses bounded names for forking processes. Then α-renaming can be applied on these forking names. Alternatively, one could use "at distance rewriting" [START_REF] Accattoli | Evaluating functions as processes[END_REF] to bypass the lack of flexibility of our structural congruence.

In RCCS not all syntactically correct processes have an operational meaning. Consider for instance . i, α, 0 .∅ P | ∅ Q.

To make a backward transition, one should first apply the congruence rule called "distribution memory" and then look for a rule of the LTS to apply. But this is impossible, since the memory on the right-hand side of the parallel operator does not contain a fork symbol ( ) at its top. The distributed memory does not agree on a common past, blocking the execution, but this term is correct from a syntactical point of view. In the following, we will consider only the semantically correct terms, called coherent.

Definition 6 (Coherent process). A RCCS process R is coherent if there exists a CCS process P such that ∅ P -→ R.

Coherent terms are also called reachable, as they are obtained by a forward execution from a process with an empty memory. Coherence of terms can equivalently be defined in terms of coherence on memories [5, Definition 1].

Backtracking is non-deterministic because backtracking is possible on different threads. However, it is noetherian and confluent as backward synchronizations are deterministic [START_REF] Danos | Transactions in RCCS[END_REF]Lemma 11].

Lemma 1 (Unique origin). If R is a coherent process, then ∀R such that R ≡ R or R R , then R is also coherent. Up to structural congruence, there exists a unique process P such that R ∅ P .

In the following, we call the origin of R and denote O R the unique process P such that R ∅ P . Lastly, we recall a useful result, that asserts that every reversible trace can be rearranged as a sequence of only-backward moves followed by a sequence of only-forward moves.

Lemma 2 (Parabolic traces, [5, Lemma 10]

). If R • • • S, then there exists R such that R R -→ S.
It is natural to wonder if our reversible syntax is a conservative extension of CCS. We will make sure in the following that the forward rules in the reversible LTS correspond to the LTS of the natural semantics.

Definition 7 (Map from RCCS to CCS). We define inductively a map ε(•) from RCCS terms to CCS terms by erasing the memory:

ε(m P ) = P ε(R|S) = ε(R)|ε(S) ε(R\a) = (ε(R))\a
In the following lemma, we denote α -→ the standard rewriting rule on CCS terms.

Lemma 3 (Correspondence between R and ε(R)). For all R and S, R

i:α -→ S for some i iff ε(R) α -→ ε(S).
Proof. The main elements of the proof are already known [START_REF] Danos | Reversible communicating systems[END_REF], and require an additional function l mapping CCS terms to RCCS terms, i.e., l(P ) = ∅ P . The "if" part is an application of [5, Corollary 4] together with the observation that R and l(ε(R)) can perform the same forward transitions, up to event identifier. The "only if" part is a direct application of [START_REF] Danos | Reversible communicating systems[END_REF]Lemma 4], once we remarked that every CCS term P is such that there exists a RCCS term R with ε(R) = P (just take l(P )).

Lastly, we can define an order relation on memory events, that we call structural causality. Intuitively, the order of events in the memory reflects the causality relations between their respective transitions.

Definition 8 (Structural causality, [23, Definition 2.2.]). Let S 1 i1:α1 -→ S 2 and S 2 i2:α2
-→ S 3 be two composable transitions. We say that the memory event i 1 is a cause of event i 2 in S 3 , denoted i 1 < S3 i 2 iff S 3 contains the process i 2 , α 2 , P 2 . i 1 , α 1 , P 1 .m P 3 for a memory m and three CCS processes P 1 , P 2 and P 3 .

Given a memory and an event identifier, we can uniquely identify a memory event. Therefore, sometimes we use only the event identifier to talk about an event or about the structural causality between two events.

Contextual equivalences

Contextual equivalence for CCS terms [START_REF] Milner | Barbed bisimulation[END_REF] is now standard, but its extension to RCCS is not straightforward, since contexts needs to be properly defined (Definition 12). As usual, reductions are part of the observables, but observing only them results in a too coarse relation, and adding termination is not relevant in concurrency. Barbed congruence (Definition 11) has proven to be the right notion for CCS, and we revisit it for RCCS terms. We begin by recalling definitions of context and observables for CCS.

Definition 9 (Context).

A context is a process with a hole [•] defined formally by the grammar:

C[•] := [•] λ.C[•] P | C[•] C[•]\a P + λ.C[•]
Definition 10 (Barbs). Write P ↓ α if there exists P such that P α -→ P .

We now define a contextual equivalence where reductions and barbs are the observables.

Definition 11 (Barbed congruence). A barbed bisimulation is a symmetric relation R on CCS processes such that whenever P R Q the following holds:

P τ -→ P ⇒ ∃Q s.t. Q τ -→ Q and Q R Q (closed by reduction) P ↓ a ⇒ Q ↓ a (barb preserving)
If there exists a barbed bisimulation between P and Q we write

P • ∼ τ
Q and say that P and Q are barbed bisimilar.

If

∀C[•], C[P ] • ∼ τ C[Q],
we write P ∼ τ Q and say that P and Q are barbed congruent.

An interesting proposition allows to restrict the grammar of contexts in the following.

Proposition 1. ∀a, P 1 , P 2 , Q, λ, a, P 1 • ∼ τ P 2 ⇒      λ.P 1 • ∼ τ λ.P 2 P 1 \a • ∼ τ P 2 \a λ 1 .P 1 + π.Q • ∼ τ λ 2 .P 2 + π.Q Proof. 1. P 1 • ∼ τ P 2 ⇒ λ.P 1 • ∼ τ λ.P 2 . From CCS's grammar, λ = τ , hence P 1 , P 2 such that P τ -→ P 1 or P 2 τ -→ P 2 . The relation {λ.P 1 , λ.P 2 } is trivially a barbed bisimulation. 2. P 1 • ∼ τ P 2 ⇒ P 1 \a • ∼ τ P 2 \a.
Let us denote R 1 the largest barbed bisimulation for P 1 and P 2 . We show that the relation R 2 = {P 1 \a, P 2 \a | P 1 R 1 P 2 } is a barbed bisimulation. We have to show that:

• ∀b such that P 1 \a ↓ b then P 2 \a ↓ b . It follows from P 1 \a ↓ b ⇒ P 1 ↓ b
and b = a.

• P 1 \a τ -→ P 1 implies that P 2 \a τ -→ P 2 and P 1 R 2 P 2 . By structural induction on the transition P 1 \a τ -→ P 1 we have that ∃P 1 such that P 1 τ -→ P 1 and P 1 \a = P 1 . As P 1 R 1 P 2 there exists P 2 such that P 2 τ -→ P 2 and we apply the rule Hide we get P 2 \a τ -→ P 2 \a. Thus there exists P 2 = P 2 \a and P 1 R 2 P 2 .

It follows similarly for the barbs and reductions on P 2 .

P

1 • ∼ τ P 2 ⇒ λ 1 .P 1 + π.Q • ∼ τ λ 1 .P 1 + π.Q.
Let us denote R 1 the largest barbed bisimulation for P 1 and P 2 . We show that the relation R 2 =R 1 ∪{π.Q, π.Q} is a barbed bisimulation. As above, we show that ∀α such that (λ

1 .P 1 + π.Q) ↓ α then (λ 1 .P 1 + π.Q) ↓ α . It follows from the subcases λ 1 .P 1 ↓ α (hence λ 2 .P 2 ↓ α ) or π.Q ↓ α .
It follows similarly for the barbs and reductions on P 2 .

Corollary 1. If a context C[•] does not contain the parallel operator, then for all

P , Q, C[P ] • ∼ τ C[Q] implies P • ∼ τ Q.
Stated differently, this implies that discriminating contexts regarding barbed congruence involve parallel composition. As we will focus on this relation, we will only consider in the following the contexts to be parallel compositions:

C[•] := [•] P | [•]
This is handy to define RCCS context, but some subtleties remain. A context has to become an executable process regardless of the process instantiated with it. We say that a context has a coherent memory if it may backtrack up to the context with an empty memory (similar to the Definition 6 of coherent processes). We distinguish three types of contexts, depending on their memories:

• Contexts with an empty memory.

• Contexts with a non-empty memory that is coherent on its own. 4 The process that we instantiate with it can be incoherent in which case we conjecture that the term obtained after instantiation is also incoherent, coherent on their own in which case it is possible to backtrack the memory of the context up to the empty memory.

Hence, w.l.o.g., we consider contexts without memory and contexts with coherent memories to be equivalent. These are the types of contexts that we use throughout the article. However, a third case remains:

• Contexts that have a non-coherent memory. There exists incoherent terms whose instantiation with an incoherent context is coherent. For instance, C = 1, a, 0 . .∅ P | [•] and R = 1, ā, 0 . .∅ P are incoherent individually, but C[R] is coherent and can backtrack to .∅ a.P | .∅ ā.P . We leave this case as future work.

The "up to minor addition of symbols" comes from a simple consideration on the parallel composition in RCCS. A process with an empty memory compose with a RCCS term if fork symbols are added to reflect the parallel composition. For instance, two processes with an empty memory ∅ P and ∅ P compose and we obtain .∅ P | .∅ P ≡ ∅ (P | P ) instead of ∅ P | ∅ P , an incoherent process.

We define a rewriting function on RCCS processes, that adds a fork symbol at the beginning of a memory. It allows a process with a memory to compose with a context. Definition 12 (RCCS context). Define (R) the operator that adds a fork symbol at the beginning of the memory of each thread in R:

(R 1 | R 2 ) = (R 1 ) | (R 2 ) (R\a) = ( (R))\a (m P ) = m . .∅ P where m = m .∅ (0) = 0 Define C [R] as follows C [R] = R if C[•] = [•] .∅ P | (R) if C[•] = P | [•]
RCCS contexts are basically CCS context with additional fork symbols in the memory of the context and in the memory of the process instantiated. We now verify that C [R] is a coherent process, using the function ε(•) that erases the memories from a term (Definition 7). Recall that the "origin of a process" R,

unique by Lemma 1, is denoted O R . Proposition 2. For all R and C [•], ∅ C[ε(O R )] -→ C [R]. Proof. Let C[•] = P | [•] and O R = ∅ P , we get that ∅ C[ε(O R )] = ∅ P | ε(O R ) = ∅ P | P ≡ ( .∅ P ) | ( .∅ P ) (By distribution memory) = ( .∅ P ) | (O R ) -→ ( .∅ P ) | (R) (Since O R -→ R) = C [R] Example 1. Let R = .m.∅ P 1 | .m.∅ P 2 and C[•] = P | [•]. Let us rewind R to its origin: R = .m.∅ P 1 | .m.∅ P 2 ≡ m.∅ (P 1 | P 2 ) ∅ P = O R
We instantiate the context with O R and redo the execution from the origin of R up to R:

C [O R ] = ( .∅ P ) | ( .∅ P ) -→ ( .∅ P ) | m. .∅ P 1 | m. .∅ P 2 = ( .∅ P ) | (R) = C [R]
Hence we have that

C [O R ] -→ C [R].
Once this delicate notion of context for reversible process is settled, extending the CCS barbs (Definition 10) and barbed congruence (Definition 11) are straightforward. We'll overload the notations ↓ α and • ∼ τ by using them for both RCCS and CCS terms, but, since terms always indicate in which realm we are, we consider this abuse to be harmless.

Definition 13 (RCCS barbs). We write R ↓ α if there exists i ∈ I and R such that

R i:α -→ R .
Definition 14 (Back-and-forth barbed congruence). A back-and-forth bisimulation is a symmetric relation on coherent processes R such that if R R S, then

R τ R ⇒ ∃S s.t. S τ S and R R S ; (back) R τ -→ R ⇒ ∃S s.t. S τ -→ S and R R S ; (forth)
and it is a back-and-forth barbed bisimulation if, additionally,

R ↓ a ⇒ S ↓ a . (barbed)
We write R

• ∼ τ S if there exists R a back-and-forth barbed bisimulation such that R R S.

The back-and-forth barbed congruence, denoted R ∼ τ S, holds if for all context

C [•], C [O R ] • ∼ τ C [O S ].
From the definition of R ∼ τ S, the following lemma trivially holds. Lemma 4. For all R and S, R

∼ τ S ⇒ O R ∼ τ O S .
However, the converse does not hold as R and S can be any derivative of the same origin, as illustrated below.

Example 2. Let R = 1, a, b.Q .∅ P and S = 2, b, a.P .∅ Q, with P • ∼ τ Q. We have that O R ∼ τ O S , as O R = O S , but R ∼ τ S, as P • ∼ τ Q: O R ∼ τ O S 1, a, b.Q .∅ P ∼ τ 2, b, a.P .∅ Q 1 : a 2 : b
Note that even if the context is defined for any reversible process, we instantiate the context with processes with an empty memory in Definition 14. If instead we had defined R ∼ τ S iff for all contexts, there exists R such that

C [R] R C [S]
, then Lemma 4 would not hold. We highlight this in the following example.

Example 3. Let us consider the processes ∅ a.P + Q and ∅ a.P which can do a transition on a to obtain respectively R = 1, a, Q P and S = 1, a P . We have that R and S are back-and-forth barbed bisimular. As we are using contexts without memory, there is no context able to backtrack on a.

O R = ∅ a.P + Q • ∼ τ ∅ a.P = O S R = 1, a, Q P ∼ τ 1, a P = S 1 : a 1 : a
Remark 3 (On backward barbs). Let us informally argue that backward barbs are not an interesting addition to a contextual equivalence. One can always define ad-hoc barbs that potentially change the equivalence relations, however we end up with relations that have no practical meaning. We consider below another definition of barb [25, Definition 2.1.3], which gives an intuitive reading and is not syntax-specific.

Let the tick ( / ∈ N) be a special symbol denoting termination. A barb is an interaction with a context that can do a tick immediately after:

P ↓ α ⇐⇒ P | ᾱ. τ -→ Q | for some Q.
Note that the definition above implies that (i) the barb is an interaction with a context that can terminate immediately after and (ii) the interaction blocks the termination on the context side, i.e., no further transition is possible on that side.

If we try to apply this definition to a backward barb then the tick has to be in the memory of the context and blocked by another action, i.e., the context has to be of the form

C[•] ≡ [•] | ( i, ᾱ, 0 .
.∅ 0). This raises multiple problems:

1. Syntactically, becomes a prefix, rather than a "terminal process", i.e., terms of the form .a.P appear. This contradict the intuition that this symbol stands for termination.

In a situation where C[R]

i:τ R | .∅ 0, the symbol is not observable, and R could continue its computation before is popped from the context's memory. So we would have to add the content of the memory to what is observable. But in that case, one might as well look directly in the process' memory if a label is present.

3. Lastly, defining the backward barb as the capability to do a backward step, and having immediately after the forward barb, seems to be equivalent to any reasonable definition of backward barb.

Thus we argue that the backward barbs are a contrived notion.

Configuration structures as a model of reversibility

Causal models take causality and concurrency between events as primitives. In configuration structures, configurations stands for computational states and the set inclusion represents the executions, so that in each state one can infer a local order on the events based on the set inclusion. We introduce them 5 and their categorical representation modeling operations from process (Sect. 2.1).

One can also obtain a causal semantics of a process calculus, by decorating its LTS. In Sect. 2.2 we briefly show how to interpret CCS terms in configuration structures and how to decorate its LTS to derive causal information from the transitions.

Lastly, we introduce configuration structure for a restricted class of RCCS process, called singly labeled (Definition 26). They are essentially an address in the configuration structure of the underlying, "original" CCS term. We then introduce the LTS of those configuration structures and prove their operational correspondence with the reversible syntax (Lemma 5).

Configuration structures as a causal model

Let E be a set, ⊆ be the usual set inclusion and C be a family of subsets of

E. For X ⊆ C, X is compatible, denoted X↑, if ∃y ∈ C finite such that ∀x ∈ X, x ⊆ y.
Definition 15 (Configuration structures). A configuration structure C is a triple (E, C, ⊆) where E is a set of events, ⊆ is the set inclusion and C ⊆ P(E) is a set of subsets satisfying:

∀x ∈ C, ∀e ∈ x, ∃z ∈ C finite s.t.e ∈ z and z ⊆ x (finiteness) ∀x ∈ C, ∀e, e ∈ x, e = e ⇒ ∃z ∈ C, z ⊆ x e ∈ z ⇐⇒ e / ∈ z (coincidence freeness) ∀X ⊆ C if X↑ then X ∈ C (finite completness) ∀x, y ∈ C if x ∪ y ∈ C then x ∩ y ∈ C (stability)
We denote 0 the configuration structure with E = ∅.

Intuitively, events are the actions occurring during the run of a process, while configurations represents computational states. The first axiom, finiteness, guarantees that for each event the set of causes is finite. Coincidence freeness states that each computation step consists of a single event. Axioms finite completness and stability are more abstract and are better explained on some examples. Consider the structures in Figure 2: the structure 2a does not satisfy the second axiom, as two events occur in a single step. The structure 2b does not satisfy finite completeness. Intuitively, configuration structures cannot capture "pairwise" concurrence. Finally, the structure 2c does not satisfies stability and the intuition is that the causes of event e 3 are either e 1 or e 2 , but not both. From now on, we will only consider configuration structures that are labeled, so we omit that adjective in the following. Now we define morphisms on configuration structures that permits to form a category whose objects are configuration structures. Intuitively, morphisms model the inclusion or refinement relations between processes. Process algebras' operators are then extended to configuration structures, which makes it a modular model.

Definition 17 (Category of configuration structures). A morphism of configuration structures

f : (E 1 , C 1 , 1 ) → (E 2 , C 2 , 2 ) is a partial function on the underlying sets f : E 1 E 2 that is: ∀x ∈ C 1 , f (x) = {f (e) | e ∈ x} ∈ C 2 (configurations preserving) ∀x ∈ C 1 , ∀e 1 , e 2 ∈ x, f (e 1 ) = f (e 2 ) ⇒ e 1 = e 2 (local injective) ∀x ∈ C 1 , ∀e ∈ x, 1 (e) = 2 (f (e)) (label preserving)
An isomorphism on configuration structures is denoted ∼ =.

Definition 18 (Operations on configuration structures). Let

C 1 = (E 1 , C 1 , 1 ), C 2 = (E 2 , C 2 , 2 ) be two configuration structures and set E = E ∪ { }.
Product Let denote undefined for a partial function. Define the product of C 1 and

C 2 as C = C 1 ×C 2 , for C = (E, C, )
, where E = E 1 × E 2 is the product in the category of sets and partial functions6 :

E 1 × E 2 = {(e 1 , ) | e 1 ∈ E 1 } ∪ {( , e 2 ) | e 2 ∈ E 2 } ∪ {(e 1 , e 2 ) | e 1 ∈ E 1 , e 2 ∈ E 2 } with p 1 : E → E 1 ∪ { } and p 2 : E → E 2 ∪ { }. Define the projections π 1 : (E, C) → (E 1 , C 1 ), π 2 : (E, C) → (E 2 , C 2 )
and the configurations x ∈ C such that the following holds:

∀e ∈ E, π 1 (e) = p 1 (e) and π 2 (e) = p 2 (e) (× 1 )

π 1 (x) ∈ C 1 and π 2 (x) ∈ C 2 (× 2 ) ∀e, e ∈ x, if π 1 (e) = π 1 (e ) = or π 2 (e) = π 2 (e ) = then e = e (× 3 ) ∀e ∈ x, ∃z ⊆ x finite s.t. π 1 (x) ∈ C 1 , π 2 (x) ∈ C 2 and e ∈ z (× 4 )
∀e, e ∈ x, e = e ⇒ ∃z ⊆ x s.t.

     π 1 (z) ∈ C 1 , π 2 (z) ∈ C 2 e ∈ z ⇐⇒ e / ∈ z (× 5 )
The labeling function is defined as follows:

(e) =      1 (e 1 )
if π 1 (e) = e 1 and π 2 (e) =

2 (e 2 ) if π 1 (e) = and π 2 (e) = e 2

( 1 (e 1 ), 2 (e 2 )) otherwise

The conditions (× 1 )-(× 5 ) guarantee that C 1 × C 2 is the product in the category of configuration structures, and that the projections π 1 and π 2 are morphisms.

In particular, (× 3 ) ensures that the projections are local injective, (× 4 ) and (× 5 ) enforce finiteness and coincidence-freeness axioms in the resulted configuration structure.

Coproduct Define the coproduct of C 1 and C 2 as

C = C 1 + C 2 , for C = (E, C, ), where E = ({1}×E 1 )∪({2}×E 2 ) and C = {{1}×x | x ∈ C 1 }∪{{2}×x | x ∈ C 2 }.
The labeling function is defined as (e) = i (e i ) when e i ∈ E i and π i (e i ) = e.

Restriction Relabeling Given r : L → L a Relabeling function, define the relabeling of a configuration structure

C 1 = (E 1 , C 1 , 1 ) as r • C 1 = (E 1 , C 1 , r • 1 ).
and

Parallel composition Define parallel composition C = r • (C 1 × C 2 )
E as the application of product, relabeling and restriction, with r and E defined below.

• First, C 1 × C 2 = C 3 is the product with C 3 = (E 3 , C 3 , 3 );
• Then, C = r • C 3 with r : L → L ∪ {⊥} defined as follows:

r • 3 (e) =      3 (e) if 3 (e) ∈ {a; ā} τ if 3 (e) ∈ {(a, ā); (ā, a)} ⊥ otherwise • Finally, C = (E 1 × E 2 , C 3 , r • 3 ) E is the resulted configuration structure, where E = {e ∈ E 3 | r • 3 (e) = ⊥}.
Example 4. Consider the following two configuration structures, respectively

C 1 = (E 1 , C 1 , 1 ) and C 2 = (E 2 , C 2 , 2 ): ∅ {e 1 } 1 (e 1 ) = a ∅ {e 2 } {e 2 } 2 (e 2 ) = ā, 2 (e 2 ) = b
Then we can form their product

C 3 = C 1 × C 2 as ∅ {e 1 × e 2 } {e 1 × } { × e 2 } { × e 2 } {e 1 × e 2 } {e 1 × , × e 2 } {e 1 × , × e 2 } 3 (e 1 × e 2 ) = (a, ā), 3 (e 1 × ) = a 3 ( × e 2 ) = ā, 3 ( × e 2 ) = b 3 (e 1 × e 2 ) = (a, b)
The parallel composition of C 1 and C 2 is built on top of C 3 , by

• removing the configuration {e 1 × e 2 }, since r • 3 (e 1 × e 2 ) = ⊥,
• letting the label for (e 1 × e 2 ) be τ , since r • 3 (e 1 × e 2 ) = r(ā, a) = τ . Definition 19 (Causality). Let x ∈ C and e 1 , e 2 ∈ x for (E, C, ) a configuration structure. Then we say that e 1 happens before e 2 in x or that e 1 causes e 2 in x, written e 1 x e 2 , iff

∀x 2 ∈ C, x 2 ⊆ x, e 2 ∈ x 2 ⇒ e 1 ∈ x 2 .
Morphisms on configuration structures reflect causality. Let f : C 1 → C 2 be a morphism and x ∈ C 1 be a configuration. Then

∀e 1 , e 2 ∈ x, if f (e 1 ) f (x) f (e 2 ) then e 1 x e 2 .
However, morphisms do not preserve causality in general. In the case of a product we can show that all immediate causalities are due to one of the two configuration structures. Stated differently, a context can add but cannot remove causality in the process.

Definition 20 (Immediate causality). Let x be a configuration in a configuration structure, and e, e ∈ x be two events. We say that e is an immediate cause for e in x, and write e → x e , if e < x e and e ∈ x such that e < x e < x e .

The reader should remark that we now have two orders, one on events, that we just defined, and one on memory events (or memory identifiers), the structural causality i 1 < S3 i 2 (Definition 8).

Proposition 3. Let x ∈ C 1 × C 2 . Then e 1 → x e 2 ⇐⇒ either π 1 (e 1 ) < π1(x) π 1 (e 2 ) or π 2 (e 1 ) < π2(x) π 2 (e 2 ).
Proof. The proof [2, Proposition 6] follows by contradiction, using that if x is a configuration in C and if e ∈ x is such that ∀e ∈ x, e < x e , then x \ {e} is a configuration in C.

Operational semantics, correspondence and equivalences

Configuration structures are a causal model for CCS [START_REF] Winskel | Models for concurrency[END_REF] in which the computational states are the configurations and the forward executions are dictated by set inclusion. To show the correspondence with CCS (Lemma 5), one defines an operational semantics on configuration structures (Definition 22) that erases the part of the structure that is not needed in future computations. To define a reversible semantics on configuration structures, a second LTS is introduced (Definition 23), that instead of being defined on configuration structures is defined on the configurations of a configuration structure. Thus forward and backward moves are simply the set inclusion relation and its opposite, respectively.

The soundness of the model is proved by defining an operational semantics on configuration structures and showing an operational correspondence between the two worlds.

Definition 21 (Encoding a CCS term). Given P a CCS term, its encoding [[P ]] as a configuration structure is built inductively, using the operations of Definition 18: Proof. This is just a reformulation of a classical result [START_REF] Boudol | On the semantics of concurrency: Partial orders and transition systems[END_REF]Theorem 2].

[[a.P ]] = a.[[P ]] [[ā.P ]] = ā.[[P ]] [[P | Q]] = [[P ]] | [[Q]] [[P + Q]] = [[P ]] + [[Q]] [[P \a]] = [[P ]] E a [[0]] = 0
The above lemma shows that labeled transitions are in correspondence, but labels are just a tool for compositionality. The main result is that a process and its encoding simulate each others reductions. The following is a direct corollary from the previous lemma. Multiple equivalence relations on configuration structures have been defined and studied [START_REF] De Nicola | Back and forth bisimulations[END_REF][START_REF] Phillips | A hierarchy of reverse bisimulations on stable configuration structures[END_REF][START_REF] Baldan | A logic for true concurrency[END_REF][START_REF] Vogler | Bisimulation and action refinement[END_REF][START_REF] Van Glabbeek | Equivalence notions for concurrent systems and refinement of actions (extended abstract)[END_REF]. Among them, hereditary history preserving bisimulation (HHPB) [START_REF] Bednarczyk | Hereditary history preserving bisimulations or what is the power of the future perfect in program logics[END_REF] equates structures that simulate each others' forward and backward moves and thus connects configuration structures to reversibility. It is considered a canonical equivalence on configuration structures as it respects the causality and concurrency relations between events and admits a categorical representation [START_REF] Joyal | Bisimulation from open maps[END_REF].

Those connections between reversibility and causal models shed a new light on what help are the meaningful equivalences on reversible processes. Consequently, one applies them in the operational setting. We begin by modifying the definition of our LTS on configuration structures to include backward moves as well. The definition of HHPB below uses a label and order preserving bijection defined on two configurations, that is, sets of events equipped with a labeling function and an order relation, i.e., a causality (Definition 19), on events. Label preserving functions are introduced in Definition 17, and we define order preserving functions in a similar manner.

Definition 24 (Order preserving functions). Let x 1 , x 2 be two sets of events, and let x1 and x2 , be order relations on events in x 1 , and x 2 respectively. A function f : x 1 → x 2 is order preserving iff e x1 e ⇒ f (e) x2 f (e ), for all e, e ∈ x 1 such that f (e) and f (e ) are defined.

Definition 25 (HHPB [14, Definition 1.4]). A hereditary history preserving bisimulation on labeled configuration structures is a symmetric relation

R⊆ C 1 × C 2 × P(E 1 × E 2 ) such that (∅, ∅, ∅) ∈ R and if (x 1 , x 2 , f ) ∈ R, then
f is a label and order preserving bijection between x 1 and x 2

∀x 1 s.t. x 1 e1 -→ x 1 ⇒ ∃x 2 ∈ C 2 s.t. x 2 e2 -→ x 2 and f = f x 1 , (x 1 , x 2 , f ) ∈ R ∀x 1 s.t. x 1 e1 x 1 ⇒ ∃x 2 ∈ C 2 s.t. x 2 e2 x 2 and f = f x 2 , (x 1 , x 2 , f ) ∈ R
It is known [START_REF] Phillips | Reversibility and models for concurrency[END_REF] that hereditary history preserving bisimulation corresponds to the back-and-forth bisimulation (Definition 14), in the following sense: CCSK [START_REF] Phillips | Reversing algebraic process calculi[END_REF] is proven to satisfy the "the axioms of reversibility" [31, Definition 4.2]), so that its LTS is prime. Then, this LTS is represented as a process graph, on which the forward-reverse bisimulation [7, Definition 5.1]-our back-and-forth bisimulation (Definition 14)-is defined. Finally, configuration graphs and hereditary historypreserving bisimulation are defined from configuration structures, and both relations are proven to coincide [7, Theorem 5.4, p. 105].

Configuration structures for RCCS

All the possible future behaviours of a process without memory are present in its encoding as a configuration structure. All alike, we want our encoding of processes with memory to record both their past and their future, so that they can evolve in both directions, as reversible processes do. To this end, we encode RCCS terms as a configuration in the configuration structure of their origins (Definition 27). Then, we show an operational correspondence between RCCS terms and their encoding (Lemma 6).

To determine which configuration corresponds to the computational state of the term, we need to uniquely identify a process from its past and future. However, as the following example illustrates, this is not always possible. 1. The process P = a.b + a is interpreted as the configuration structure in Figure 3a. Let us consider the execution ∅ P i:a -→ R, for some i. To determine which of the configurations labeled a correspond to R we have to consider the future of R as well.

2. Hence we choose a configuration that respects the past and the future of R, but such a configuration might not be unique. Let Q = a.b + a.b be a process whose configuration structure is in Figure 3b. For the trace

∅ P i:a
-→ R there is no way to choose between the two configurations labeled a.

The situation of example 5 can be generalized to any process whose reduction may lead to a process of the form a.P | a.Q or a.P + a.Q. The first kind of process is ruled out by forbidding auto-concurrency [32, Definition 9.5], but we need a stronger condition, a sort of auto-conflict, to forbid the second type of process. We then consider a restricted class of processes, defined below. Definition 26 (Singly labeled configuration structures and processes). A configuration structure C is singly labeled, or without auto-concurrency nor auto-conflict if ∀x ∈ C and ∀e, e / ∈ x we have that A CCS process P (resp. a RCCS process R) is singly labeled if

[[P ]] (resp. [[ε(O R )]]) is.
Remark that being singly labeled does not mean that each label has to occurs only once in a process: whereas a | b.a is not singly labeled, since after firing b two transitions labeled a can be fired, a.a and a.b + b are singly labeled. However, a syntactical definition of this restriction cannot be inductively defined, since P and Q might be singly labeled, but not P | Q nor P + Q.

The following encoding, and all the results that use it, require the process to be singly labeled (on top of being coherent, if they are reversible). This restriction could probably be removed at the price of a tagging of the occurrences of names, maybe in the spirit of the localities [START_REF] Boudol | A non-interleaving semantics for CCS based on proved transitions[END_REF].

We are now ready to define the encoding of a singly labeled, coherent, reversible process R as a tuple made of a configuration structure and a configuration. Remember that R has a unique origin O R (Lemma 1), whose empty memory can be removed (Definition 7) to obtain a CCS process that can be encoded as a configuration structure (Definition 21). Hence, we obtain a configuration structure [[ε(O R )]] which contains all the possible computation starting from O R , but doesn't account for the transitions that led to R. However, we know there must exists a configuration

x ∈ [[ε(O R )]] such that • if R i:α -→ S, then there exists y ∈ [[ε(O R )]
] and e such that y = x ∪ {e} and (e) = α.

• if R i:α S, then there exists y ∈ [[ε(O R )]] such that x = y ∪ {e}.
Stated differently, x is the configuration reflecting the future and the past of R, and we're calling it its address. This address is determined by the trace

σ : O R -→ R.
To define the address of a process using its trace from the origin, first remark that if the trace is empty, i.e., R is O R , then the address of R is ∅. Otherwise, we need to follow the trace σ up in the structure. This is the initial step in the following definition (Equation 3). To do so, we need a function called ad [[ε(O R )]] which takes three arguments-the current address x of a process R 1 , a bijection ∂ between events in x and memory events in R 1 , and a trace σ : R 1 -→ R 2 -and returns the corresponding address of R 2 . The bijection ∂ ensures that events in x and R 1 have the same causal order. For example, let m a.b.P | b.P be a process that communicates, first on channel a and then on channel b. To interpret the resulting process, one needs to know which b has been fired, i.e., to know the causal relation between the two communications, on a and b. This information can be retrieved from the memory of a process, using structural causality (Definition 8).

Definition 27 (Encoding RCCS processes in configuration structures). Let R be a singly labeled and coherent process. Let C = [[ε(O R )]] be the encoding (Definition 21) of its "memory-less" origin (Definition 7). The encoding of R as a configuration structure is defined by induction on the trace (Definition 2)

σ : O R -→ R, as [[R]] σ = (C, ad C (∅, ∅, σ)) (3)
Before defining the function ad C , let us remark that for all trace σ : R 1 -→ R 3 , either σ = is the empty trace, and R 1 = R 3 , either there exists R 2 , a transition t : R 1 i:α -→ R 2 and a trace σ : R 2 -→ R 3 such that σ = t; σ .

ad C (x, ∂, ) = x (4) ad C (x, ∂, t; σ ) = ad C (x ∪ {e}, ∂ ∪ {e ↔ i}, σ ) (5)
where

(a) (e) = α (b) x ∪ {e} ∈ C (c) j < R2 i ⇐⇒ ∂(j) < x∪{e} e (d) [[ε(R 2 )]] = C \ (x ∪ {e})
Where ∂ is a bijection between events in a configuration of C and events identifiers in the memory of R 2 . Hence, i and j are event identifiers, uniquely identifying event memories in the memory of R, and compared with the structural causality < R2 (Definition 8). On the other hand, ∂(j) and e are events, compared using the immediate causality order < x∪{e} (Definition 20).

Equation 5 defines a step of computation of the function ad C (x, ∂, σ). Given that the current process in the trace is R 1 with address x and a bijection ∂, the next configuration consists in x ∪ {e}, for some event e, such that x ∪ {e} is a valid configuration (condition (b)). Which event e is chosen depends on the transition t : R 1 i:α -→ R 2 (conditions (a) and (c)). Finally, to handle process as the one in example 5, we also check that the future of R 2 corresponds to the future of x ∪ {e} (condition (d)). The computation stops when we reach the end of the trace (Equation 4).

We show in Proposition 4 that the function is well defined, i.e., for every singly labeled process R and for every trace σ : O R -→ R there exists a unique configuration in [[ε(O R )]] σ defined as above. In the following, we won't name traces and will just write ad C (x, f, R -→ S) instead of the more correct ad C (x, ∂, σ) for σ : R -→ S. Proposition 5 will prove that the encoding is in fact independent of the trace considered. -→ R n+1 there exists a unique configuration

x n+1 ∈ C such that ad C (∅, ∅, O R -→ R n i:α -→ R n+1 ) = x n+1 and [[ε(R n+1 )]] = C \ x n+1 .
We have that

ad C (∅, ∅, O R -→ R n i:α -→ R n+1 ) = ad C (x n , ∂ n , R n i:α -→ R n+1 )
Hence we have to show that there exists a unique e ∈ C such that (e) = α, x n+1 = x n ∪ {e}, ∂ n+1 = ∂ n ∪ {e ↔ i} and we have and

[[ε(R n+1 )]] = C \ (x n ∪ {e}).
However, if such an e exists then e ∈ [[ε(R n )]] and

C \ (x n ∪ {e}) = [[ε(R n )]] \ {e}.

Hence we reason on the transition R

n i:α -→ R n+1 to show that there exists a unique e ∈ [[ε(R n )]] such that [[ε(R n+1 )]] = [[ε(R n )]] \ {e}.
We consider only the case α = a, the rest being similar. Using structural congruence it is possible to rewrite R n and R n+1 as follows

R n ≡ (m a.P 1 | R 2 )\(b 1 . . . b n ) R n+1 ≡ (m P 1 | R 2 )\(b 1 . . . b n ) and hence, for ε(R 2 ) = P 2 , ε(R n ) = (a.P 1 | P 2 )\(b 1 . . . b n ) ε(R n+1 ) = (P 1 | P 2 )\(b 1 . . . b n ).
We have then to show that

[[(P 1 | P 2 )\(b 1 . . . b n )]] = [[(a.P 1 | P 2 )\(b 1 . . . b n )]] \ {e}.
From Lemma 5 such an event exists. To show its uniqueness, we need to consider several cases on R n . We only consider the case where we can rewrite [[(P

R n as R n ≡ m 1 a.P 1 | m 2 a.P 2 | R 2 . Either m 1 = m 2 ,
1 | P 2 )\(b 1 . . . b n )]] = ([[P 1 ]] × [[P 2 ]]) ∪ 1 i n E bi [[(a.P 1 | P 2 )\(b 1 . . . b n )]] = ([[a.P 1 ]] × [[P 2 ]]) ∪ 1 i n E bi If x ∈ ([[P 1 ]] × [[P 2 ]]) ∪ 1 i n E bi then ∀e ∈ x, (e) / ∈ {b i , bi , 0}. (6)
Hence

x ∈ ([[P 1 ]] × [[P 2 ]]
). Let π 1 , π 2 be the two projections defined by the product. Then

π 1 (x) ∈ [[P 1 ]] and π 2 (x) ∈ [[P 2 ]]. (7)
As

π 1 (x) ∈ [[P 1 ]],
and from the definition of [[a.P 1 ]] we have that ∃e 1 , (e 1 ) = a and such that {e

1 } ∪ π 1 (x) ∈ a.[[P 1 ]]. From Equation 7 we have that ∃x 2 ∈ a.[[P 1 ]]×[[P 2 ]] such that π 1 (x 2 ) = {e 1 }∪π 1 (x) and π 2 (x 2 ) = π 2 (x).
Hence ∃!e such that π 1 (e) = e 1 , π 2 (e) = and x 2 = {e} ∪ x. From Equation 6we have that

x 2 ∈ (a.[[P 1 ]] × [[P 2 ]]) ∪ 1 i n E bi . We infer that if x ∪ {e} ∈ (a.[[P 1 ]] × [[P 2 ]]) \ (b 1 . . . b n ) then x ∈ [[(a.P 1 | P 2 ) \ (b 1 . . . b n )]] \ {e}. From [[ε(R)]] = C \ x n , we have that ∀y ∈ [[ε(R)]], y ∪ x n ∈ C. In particular x n ∪ {e} ∈ C.
Let us denote x n+1 = x n ∪ {e}. Remains to show that j < Rn+1 i ⇐⇒ ∂(j) < xn+1 e. We show the implication j < Rn+1 i ⇒ ∂ n (j) < xn+1 e and consider the immediate order for < Rn+1 , as the order is transitive. From j < Rn+1 i, we have that i, a . j, b ∈ R n+1 , hence we retrieve a process R k where b.a.P ∈ R k . Hence the events ∂ n (j) and ∂ n (i) are causally dependent in the configuration structure of [[ε(R k )]], and therefore causally dependent in C. For the other direction ∂ n (j) < xn+1 e ⇒ j < Rn+1 i we show that (∂(j)) and (e) are causal in the origin process P , hence they are causally dependent in the memory of R n+1 .

Hence

ad C (∅, O R -→ R n a -→ R n+1 ) = x n ∪ {e} with [[ε(R n+1 )]] = [[O Rn ]] \ (x n ∪ {e}).
Remark 4 (On encoding RCCS). Another encoding exists [START_REF] Phillips | A hierarchy of reverse bisimulations on stable configuration structures[END_REF], but it is not compositional, since

[[P 1 | P 2 ]] is not defined as an operation on [[P 1 ]] and [[P 2 ]].
Compositionality is important for the definition of contexts in configuration structures, in particular for the definition of congruence (Definition 30).

Let us now define a transition relation on configuration structures, useful in showing the operational correspondence between terms of RCCS and their encoding. We defined in Definition 27 the encoding of a process parametrically on a trace. The following proposition shows that any trace from O R up to R leads to the same encoding.

Proposition 5. For all singly labeled processes R there exists x a configuration in

[[ε(O R )]] such that ∀σ : O R -→ R, [[R]] σ = x holds. Proof. Denote C = [[ε(O R )]] = (E, C, ). From the definition of [[R]] σ it suffices to
show that for any configuration x, y ∈ C such that there exist a label and order preserving bijection f between them and such that C \ x = C \ y, x = y holds.

We prove it by induction on the size of x and y. Suppose that there exist two events e, e such that y = x ∪ {e} and z = x ∪ {e } are configurations of C as well, with f : y ↔ z. Since R is singly labeled (Definition 26), if (e) = (e ), then e = e .

-→ S then [[R]] α -→ [[S]]; 2. ∀α, S and i ∈ I such that R i:α S then [[R]] α [[S]]; 3. ∀e ∈ E, (C, x) (e)
-→ (C, x ∪ {e}) then ∃S, such that for some i ∈ I,

R i:α -→ S and [[S]] = (C, x ∪ {e}). 4. ∀e ∈ E, (C, x) (e) (C, x \ {e}) then ∃S, such that for some i ∈ I, R i:α S and [[S]] = (C, x \ {e}).
Proof. First, we should remark that in item 3 (resp. item 4), (e) = α is enforced, since

[[S]] = (C, x ∪ {e}) (resp. [[S]] = (C, x \ {e})). 1. As R i:α -→ S, O R = O S , we have that [[S]] = (C, x s ), where x S = ad C (∅, ∂, O R -→ S) = ad C (∅, ∂, O R -→ R α -→ S) = x R ∪ {e} by Proposition 4. As [[R]] = (C, x R ) it follows that (C, x R ) α -→ (C, x S ).
2. The proof for the backward direction is similar except that it uses the trace up to R. It uses Proposition 5, which allows us to backtrack on any path from the emptyset and leading to x R .

3. From (C, x)

(e) -→ (C, x ∪ {e}) we have that x ∪ {e} ∈ C. Then {e} ∈ C \ x. From [[R]] = (C, x) we have that C \ x = [[ε(R)]], hence {e} ∈ [[ε(R)]].
We use Lemma 5 and obtain that ∃P such that ε(R) (e) -→ P . Then due to the strong bisimulation between a RCCS term and its corresponding CCS term in Lemma 3, we have that, for some i, R i:α -→ S, where ε(S) = P . That [[S]] = (C, x ∪ {e}) follows from a similar argument to above and from Proposition 5.

4. It is similar to the case above.

Contextual equivalence on configuration structures

In this section we introduce a notion of context for the configuration structures and then adapt the back-and-forth barbed bisimulation to configuration structures (Definition 30). We define hereditary history preserving bisimulation and use two families of relations, denoted F i and B i , to inductively approximate the bisimulation (Lemma 8). We use these relations to show that two processes are barbed congruent whenever their denotations are in the HHPB relation (Theorem 2). Once the HHPB has been proven to be a congruence (Proposition 9), one direction is straightforward, whereas the other is more technical and, as in CCS [START_REF] Milner | Barbed bisimulation[END_REF], follows by contradiction. It uses the relations F i and B i (Definition 34 and Definition 35) to build contexts that discriminate processes that are not bisimilar.

Contexts for configuration structures

Contexts for configuration structures have never been defined as it is not clear what a configuration structure with a hole could be. However, if a structure C has an operational meaning, i.e., if there exists P a process such that C

= [[P ]], we use a CCS context C[•] to build a configuration structure [[C[P ]]].
When analyzing the reductions of a process in context, we need to know the contribution the process and the context have in the reduction. To this aim we associate to the context C[•] instantiated by a process P a projection morphism π C,P :

[[C[P ]]] → [[P ]] that retrieve in [[C[P ]]] the parts of a configuration belonging to [[P ]].

Following Proposition 1, we continue to consider only context made of parallel compositions, but the following definition can be extended to arbitrary contexts [

• if C[•] = C [•] | P then π C,P : [[C [P ] | P ]] → [[P ]] is defined as π C,P (e) = π C ,P (π 1 (e)), where π 1 : [[C [P ] | P ]] → [[C [P ]]]
is the projection morphism defined by the product in Definition 18;

• if C[•] = [•] then π C,P : [[C[P ]]] → [[P ]
] is the identity.

We naturally extend π C,P to configurations, and prove by case analysis that π C,P :

[[C[P ]]] → [[P ]
] is a morphism.

Relation induced by barbed congruence on configuration structures

We define a relation on configuration structures that have an operational meaning and we show it is the relation induced by the barbed congruence in RCCS (Definition 14). We call the relation barbed back-and-forth congruence, to highlight its meaning, though it is not strictly speaking a congruence on configuration structures.

Definition 30 (Back-and-forth barbed congruence on configuration structures).

A back-and-forth barbed bisimulation on configuration structures is a symmetric relation R⊆ C 1 × C 2 such that (∅, ∅) ∈ R, and if (x 1 , x 2 ) ∈ R, then

x 1 e1 x 1 ⇒ ∃x 2 ∈ C 2 s.t. x 2 e2 x 2 , with 1 (e 1 ) = 2 (e 2 ) = τ and (x 1 , x 2 ) ∈ R; (back) x 1 e1 -→ x 1 ⇒ ∃x 2 ∈ C 2 s.t. x 2 e2 -→ x 2 , with 1 (e 1 ) = 2 (e 2 ) = τ and (x 1 , x 2 ) ∈ R; (forth) if ∃e 1 ∈ E 1 s.t. 1 (e 1 ) = τ and x 1 e1 -→ x 1 then ∃x 2 ∈ C 2 s.t. x 2 e2 -→ x 2 , with 1 (e 1 ) = 2 (e 2 ). (barbed) Let C 1 • ∼ τ C 2 if
and only if there exists a back-and-forth barbed bisimulation between C 1 and C 2 .

Define ∼ τ the back-and-forth barbed congruence induced on configuration structures as a symmetric relation on configuration structures that have an operational meaning such that

[[P 1 ]] ∼ τ [[P 2 ]] ⇐⇒ ∀C, [[C[P 1 ]]] • ∼ τ [[C[P 2 ]]].
We now prove that this relation is the relation induced on the encoding of processes by the barbed back-and-forth congruence (Definition 14). We begin by proving it in the non-contextual case. We remind the reader that, as we are going to manipulate encoding of RCCS terms, some restrictions on the terms applies (Definition 26). Proposition 6. For all P and Q, ∅ P

• ∼ τ ∅ Q ⇐⇒ [[P ]] • ∼ τ [[Q]].
Proof. ⇒ Let R CCS be a back-and-forth barbed bisimulation between P and Q.

We show that the following relation

R = {(x 1 , x 2 ) | x 1 ∈ [[P ]], x 2 ∈ [[Q]], ∃R, S s.t. O R = P, O S = Q, R R CCS S and [[R]] = ([[P ]], x 1 ), [[S]] = ([[Q]], x 2 )}
is a back-and-forth barbed bisimulation between

[[P ]] and [[Q]].
We have that (∅, ∅) ∈ R, let (x 1 , x 2 ) ∈ R. We have to show that the conditions in Definition 30 hold. Suppose that x 1

e1 -→ x 1 = x 1 ∪ {e 1 }, for (e 1 ) = τ . x 1 e1 -→ x 1 ⇒ ([[P ]], x 1 ) (e1) -→ ([[P ]], x 1 ) (From Definition 28) ⇒ R i: (e1) -→ R s.t. [[R ]] = ([[P ]], x 1 ) (From Lemma 6) ⇒ S i :τ -→ S (From R R CCS S) ⇒ ([[Q]], x 2 ) (e2) -→ ([[Q]], x 2 ) (From Lemma 6)
with (e 2 ) = τ . We have then (x 1 , x 2 ) ∈ R.

We proceed in a similar manner to show that conditions on the backward transitions and on the barbs hold.

⇐ Let R Conf be a back-and-forth barbed bisimulation between

[[P ]] and [[Q]].
We show that the following relation

R = {(R, S) | ε(O R ) = P, ε(O S ) = Q and [[R]] = ([[P ]], x 1 ), [[S]] = ([[Q]], x 2 ), with (x 1 , x 2 ) ∈ R Conf }
is a back-and-forth barbed bisimulation between P and Q. Let (R, S) ∈ R, the following holds:

R i:τ -→ R ⇒ ([[P ]], x 1 ) (e1)
-→ ([[P ]], x 1 ) (From Lemma 6) ⇒ ([[Q]], x 2 ) (e2) -→ ([[Q]], x 2 ) (From (x 1 , x 2 ) ∈ R Conf ) ⇒ S i :τ -→ S (From Lemma 6)
where

x 1 = x 1 ∪ {e 1 }, x 2 = x 2 ∪ {e 2 } and (e 1 ) = (e 2 ) = τ . We have that O R = P , O S = Q, [[R ]] = ([[P ]], x 1 ), [[S ]] = ([[Q]], x 2 ) and (x 1 , x 2 ) ∈ R Conf . Hence (R , S ) ∈ R.
To prove that the remaining conditions on the pair (R, S) holds as well is similar.

The contextual version of the proposition for reversible processes is straightforward.

Lemma 7. Given two singly labeled processes R and

S, O R ∼ τ O S ⇐⇒ [[ε(O R )]] ∼ τ [[ε(O S )]]. Proof. O R ∼ τ O S ⇐⇒ ∀C[•], C [O R ] • ∼ τ C [O S ] (From Definition 14) ⇐⇒ ∀C[•], ∅ C[ε(O R )] • ∼ τ ∅ C[ε(O S )] (From Definition 12) ⇐⇒ ∀C[•], [[C[ε(O R )]]] • ∼ τ [[C[ε(O S )]]] (From Proposition 6) ⇐⇒ [[ε(O R )]] ∼ τ [[ε(O S )]] (From Definition 30) ∅ {e 1 } {e 1 } 1 (e 1 ) = 1 (e 1 ) = a ∅ {e 2 } {e 2 } 2 (e 2 ) = 2 (e 2 ) = a f 2 f 1

Inductive characterization of HHPB

Similarly to the proof in CCS, the correspondence between a contextual equivalence and a non-contextual one necessitates to approximate HHPB with (a family of) inductive relations defined on configuration structures. If we are interested only in the forward direction (as in CCS), the inductive reasoning starts with the empty set, and constructs the bisimilarity relation by adding pairs of configurations reachable in the same manner from the empty set. However, to approximate HHPB, we need to have an inductive reasoning on the backward transition as well (Definition 35). These relations are of major importance to prove our main theorem (Theorem 2), as they re-introduce the possibility of an inductive reasoning thanks to a stratification of the HHPB relation.

Definition 31 (Hereditary history preserving bisimilarity). The hereditary history preserving bisimilarity, denoted ∼, is the union of all HHPB relations (Definition 25).

Remark 5 (On the uniqueness of hereditary history preserving bisimilarity). Writing C 1 ∼ C 2 is an abuse of notation as hereditary history preserving bisimulations are defined on C 1 × C 2 × P(E 1 × E 2 ). Also the union of all bisimulations may contain triples that do not have "compatible" bijections. For instance, we have two possible bisimulations between the configuration structures of Figure 4:

f 1 = {e 1 ↔ e 2 , e 1 ↔ e 2 } f 2 = {e 1 ↔ e 2 , e 1 ↔ e 2 }
However, the bisimilarity relation contains both tuples ({e 1 , e 2 }, {e 1 , e 2 }, f 1 ) and ({e 1 , e 2 }, {e 1 , e 2 }, f 2 ).

We give an inductive characterization of HHPB by reasoning on the structures up to a level: we ignore the configurations that have greater cardinality than the considered level. HHPB is then the relation obtained when we reach the top level. Hence we are able to detect, whenever two configuration structures are not HHPB, at which level the bisimulation does no longer hold.

In the following, Card(x) denotes the cardinality of a set x.

Definition 32 (Maximal and top configurations). A configuration x ∈ C is maximal if there is no configuration y ∈ C such that x y. If moreover ∀y ∈ C, Card(y) Card(x) then x is a top configuration.

Definition 33 (Cardinality of a configuration structure). The cardinality of a configuration structure C, denoted Card(C), is the maximum cardinality of any of its top configurations:

Card(C) = max{Card(x) | x is a top configuration in C}.
We use two families of relations, denoted F i , for the forward transitions, and B i , for the backward ones. The relations are parametrized by the cardinality of the configurations, that is F i (or B i ) relates configurations of cardinality i, and only of cardinality i. Intuitively, it relates processes that have performed exactly i computation steps. But F i relates processes using their future actions, while the relations B i checks the backwards steps.

Definition 34 (The forward relations

F i ). Given C 1 , C 2 two configuration structures, for all x 1 ∈ C 1 , x 2 ∈ C 2 , i ∈ N, f : x 1 → x 2 ,
we define the family of relations F i as follows:

(x 1 , x 2 , f ) ∈ F i ⇐⇒           
Card(x 1 ) = Card(x 2 ) = i, x 1 and x 2 are maximal, and f is a label preserving bijection or

∀x 1 , ∀e 1 , x 1 e1 -→ x 1 , ∃x 2 , ∃e 2 , x 2 e2 -→ x 2 and f = f x 1 such that 1 (e 1 ) = 2 (e 2 ) and (x 1 , x 2 , f ) ∈ F i+1
The family of relations F i starts by pairing configurations that are maximal, i.e., that cannot do a forward transition. It then moves downward in the structure and relates configurations of cardinality i using the relations defined on configurations of cardinality i + 1. Informally, two configurations are in the relation F i if after one forward transition the resulting configurations are in the relation F i+1 .

Note that the condition of having a label preserving bijection on the maximal configuration already imposes a form of consistent past on the configurations. For any triple (x 1 , x 2 , f ) ∈ F i , f is always a label preserving bijection: if x 1 and x 2 are maximal, then it comes from the definition; otherwise it comes from the fact that f is obtained by restricting a label preserving bijection.

We can describe informally these relations using RCCS processes. Suppose that

[[R 1 ]] = (C 1 , x 1 ), [[R 2 ]] = (C 2 ,
x 2 ) and that (x 1 , x 2 , f ) ∈ F i for some f and i. It implies that there are exactly i events in both traces O R1 -→ R 1 and O R2 -→ R 2 , and that the two traces have the same labels. Any future action of R 1 can be mimicked by R 2 , and their continuations are in the relation F i+1 .

(x 1 , x 2 , f ) ∈ B i ⇐⇒    (x 1 , x 2 , f ) ∈ F i and ∀x 1 , ∀e 1 , x 1 e1 x 1 , ∃x 2 , ∃e 2 , x 2 e2
x 2 and f = f x 1 such that 1 (e 1 ) = 2 (e 2 ) and

(x 1 , x 2 , f ) ∈ B i-1
The relation B i is built on top of F i : it tests that all pairs of configurations that are in a forward bisimulation are also backward bisimilar. Mirroring F i , one builds the families of relations B i starting from the bottom of the structures. Hence B i = F 0 .

It then moves up in the structure with B i built using B i-1 . Two configurations are related by B i if, after one backward step they both end up in B i-1 . The relations are also using a mapping between the events, which is a label preserving bijection, as B i uses F i . Moreover the bijection is also order preserving, as the following proposition shows. Proposition 7. Let C 1 , C 2 be two configuration structures and B i the family of relations defined on them. If for all i, B i = ∅, then for all (x 1 , x 2 , f ) ∈ B i , f is a order preserving bijection.

Proof. We proceed by induction on i. The base case i = 0 is trivial. Let us consider the inductive case.

Let (x 1 , x 2 , f ) ∈ B i . Then for any backward step of x 1 , x 1 e1 x 1 there exists x 2 such that x 2 e2 x 2 and (x 1 , x 2 , f ) ∈ B i . Suppose by contradiction that f is not order preserving. However, by the induction hypothesis f is an order preserving bijection. Hence the only possible case for f not to be order preserving if is there exists e 1 ∈ x 1 and e 2 ∈ x 2 , f (e 1 ) = e 2 and e 1 < x1 e 1 while e 2 < x2 e 2 . Then x 2 can backtrack on e 2 and as (x 1 , x 2 , f ) ∈ B i , x 1 has to backtrack as well on the event corresponding to e 2 , that is on e 1 . However, that contradicts e 1 < x1 e 1 .

Card(x 1 ) = 0. ⇐ By definition, F 0 ∩B 0 = F 0 . Since there exists x 2 ∈ C 2 such that (∅, x 2 , f ) ∈ R, we know that any forward transition made by ∅ can be simulated by a forward transition from x 2 , and that the elements obtained are in the relation R. By an iterated use of this notion, we find top configurations

⇒ x 2 ∈ C 2 s.t. (∅, x 2 , f ) ∈ R
x m 1 ∈ C 1 and x m 2 ∈ C 2 such that (x m 1 , x m 2 , f m ) ∈ R. By Proposition 8, x m
1 and x m 2 have the same cardinality, k, and (x m 1 , x m 2 , f m ) ∈ F k . By just reversing the trace, we go backward and stay in relation F i until i = 0, hence we found the x 2 and f we were looking for.

Card(x 1 ) = k + 1. As Card(x 1 ) > 0, we know there exists x 1 such that x 1 e1 x 1 .

⇒ Let x 2 and f such that (x 1 , x 2 , f ) ∈ B k+1 . We know that

∀x 1 , ∃x 2 and f , x 1 e1 x 1 , x 2 e1 x 2 and (x 1 , x 2 , f ) ∈ B k (By definition of B k ) ∃x 2 , f , (x 1 , x 2 , f ) ∈ R (By induction hypothesis)
And as x 1

e1

-→ x 1 , there exist x 2 and f such that (x 1 , x 2 , f ) ∈ R.

⇐ We prove it by contraposition: suppose that ∃x 2 , f such that (x 1 , x 2 , f ) ∈ R, we prove that ∀x 2 , (x 1 , x 2 , f ) / ∈ B k+1 leads to a contradiction.

As (x 1 , x 2 , f ) ∈ R, we know that there exist x 1 , x 2 and f such that

x 1 e1 x 1 ,
-x 1 e1 x 1 , -x 2 e 2 x 2 , -(x 1 , x 2 , f ) ∈ B k , -(x 1 , x 2 , f ) ∈ F k+1 , -f = f x 1 , -1 (e 1 ) = 2 (e 1 ), since f is label preserving, we have that (x 1 , x 2 , f ) ∈ B k+1 .
From this contradiction we know that we found the right element (x 2 ) that is in relation with x 1 according to B k+1 .

[[P 1 ]] = E 1 , C 1 , 1 x 1 • • e 1 [[P 1 | Q]] = E 1 , C 1 , 1 = ([[P 1 ]] × [[Q]]) E 1 y 1 • y 1 • e = (e 1 , e q ) [[P 2 ]] = E 2 , C 2 , 2 x 2 • x 2 • e 2 [[P 2 | Q]] = E 2 , C 2 , 2 = ([[P 2 ]] × [[Q]]) E 2 y 2 • y 2 • e 2 f c f π 2 π 1 π 1 e = e 1 , e q π1 π2
e = e 1 , e q We also use inductively defined relations to characterize bisimilarity with F i and B i , but would like to highlight four differences: 1. Our relations are defined on (semantic) configuration structures, and not on (syntactic) terms.

2. Our relations takes into account past and future computations, whereas ≈ takes care only of past computation.

3. For all i ∈ N, ≈ i ⊇≈ i+1 , whereas we have a more involved structure: for n the cardinality of the configuration structure under study, we have that Due to the restriction on the contexts we consider (motivated by Proposition 1), we only have to prove that Define

F n ⊇ F n-1 ⊇ • • • ⊇ F 1 ⊇ F 0 = B 0 ⊇ B 1 ⊇ • • • ⊇ B n-1 ⊇ B n 4
∀P 1 , P 2 , [[P 1 ]] ∼ [[P 2 ]] ⇒ ∀Q, [[P 1 |Q]] ∼ [[P 2 |Q]] As [[P 1 ]] ∼ [[P 2 ]],
R c ⊆ C 1 × C 2 × P(E 1 × E 2 ) as follows: (y 1 , y 2 , f c ) ∈ R c ⇐⇒ (π 1 (y 1 ), π 2 (y 2 ), π 1 • f ) ∈ R f c (e) = (π 1 • f (e)), π 2 (e)) ∈ y 2 for all e ∈ y 1 Informally (y 1 , y 2 , f c ) is in the relation R c if there is (x 1 , x 2 , f ) in R such that x i
is the first projection of y i and such that f c satisfies the property: for (e 1 , e q ) ∈ E 1 , f c (e 1 , e q ) = (f (e 1 ), e q ) and (f (e 1 ), e q ) ∈ E 2 .

Let us show that R c is a HHPB between E 1 , C 1 , 1 and E 2 , C 2 , 2 .

• (∅, ∅, ∅) ∈ R c .

• For (y 1 , y 2 , f c ) ∈ R we show that f c is label and order preserving bijection. We have that f c is defined as f c (e) = (π 1 • f (e)), π 2 (e)), for some f label and order preserving bijection such that (π 1 (y 1 ), π 2 (y 2 ),

π 1 • f ) ∈ R.
That f c is a bijection follows from f being a bijection.

Let e ∈ y 1 with π 1 (e) = e 1 , π 2 (e) = e q , then f c (e) = (f (e 1 ), e q ) for some f c s.t. (π(y 1 ), π 2 (y 2 ), f ) ∈ R. We have that 1 (e) = ( 1 (e 1 ), Q (e q )) and

2 (f c (e)) = 2 (f (e 1 ), e q ) = 2 (f (e 1 )), Q (e q )
As f is label preserving we get 2 (f c (e)) = ( 1 (e 1 ), Q (e q )), hence 1 (e) = 2 (f c (e)).

Let us now show that for e, e ∈ y 1 , if e → y1 e then f c (e) y2 f c (e ). We denote π 1 (e) = e 1 , π 2 (e) = e q and π 1 (e ) = e 1 , π 2 (e ) = e q . Then from Proposition 3

e → y1 e ⇒ e 1 π1(y1) e 1 or e q π2(y1) e q

We consider the case where e 1 π1(y1) e 1 . As f is order preserving we have that f (e 1 ) π1(y2) f (e 1 ). Then (f (e 1 ), e q ) x2 (f (e 1 ), e q ), as the projections are order reflecting.

For i ∈ {1, 2}, we have:

[[P i ]] x i • x i • [[C[P i ]]] y i • y i • [[C [P i ]]] z i • π C,Pi π C ,C[Pi] π C,Pi
We start with y 1 ∼ τ y 2 , then prove that z 1 ∼ τ z 2 , to end up with • Let (y 1 , y 2 , f c ) ∈ R c and y 1 e -→ y 1 , y 1 = y 1 ∪ {e }. We consider only the case when π 1 (e ) = e 1 = , π 2 (e ) = e q = as the rest is similar. From the definition of the projections π 1 (y 1 ), π 1 (y 1 ) ∈ C 1 and as π 1 (e ) = e 1 = , we have that π 1 (y 1 ) = π 1 (y 1 ) ∪ {e 1 }. We reason similarly on π 2 (y 1 ) and get

(x 1 , x 2 , f ) ∈ F n ∩ B n .
π 1 (y 1 ) e 1 -→ π 1 (y 1 ) and π 2 (y 1 ) e q -→ π 2 (y 1 ). (8)
From Equation 8and as (π 1 (y 1 ), π 2 (y 2 ), f ) ∈ R, by definition of R c , we have that

∃x 2 s.t. π 1 (y 2 ) e 2 -→ x 2 = x 2 ∪ {e 2 } (9)
and

f = f ∪ {e 1 ↔ e 2 } ( 10
) such that (x 1 , x 2 , f ) ∈ R. Let us show that ∃y 2 ∈ ([[P 2 ]] × [[P Q ]]) with y 2 = y 2 ∪ {e 2 } and π 1 (e 2 ) = e 2 , π 2
(e 2 ) = e q . From Equation 8and Equation 9we have that the projections are defines with π 1 (y 2 ) = x 2 , π 2 (y 2 ) = π 2 (y 1 ). The axioms of finiteness and coincidence freeness on y 2 follows from y 2 being a configuration in

([[P 2 ]] × [[P Q ]]).
Let us show that y 2 / ∈ X 2 . We have that y 1 / ∈ X 1 . As (e 1 ) and (e q ) are compatible, then so are (e 2 ) and (e q ), hence y 2 ∪ {(e 2 , e q )} / ∈ X 2 .

Remains to show

(y 1 , y 2 , f c ) ∈ R, where f c = f c ∪ {e 1 ↔ e 2 }.
We have that (π 1 (y 1 ), π 1 (y 2 ), f ) ∈ R c and from Equation 10 that π 1 • f c = f . Theorem 2. For all singly labeled P 1 and P

2 , [[P 1 ]] ∼ [[P 2 ]] ⇐⇒ [[P 1 ]] ∼ τ [[P 2 ]].
Proof. The left-to-right direction follows from the definition of ∼ (Definition 25) and from Proposition 9.

We prove the other direction by contraposition: let us suppose that [

[P 1 ]] ∼ τ [[P 2 ]] and [[P 1 ]] ∼ [[P 2 ]],
we will find a contradiction. Figure 7 presents the general shape of the configurations at the end of the proof.

As

[[P 1 ]] ∼ [[P 2 ]], by Lemma 8, there exists x 1 ∈ [[P 1 ]] such that ∀x 2 ∈ [[P 2 ]], (x 1 , x 2 , f ) / ∈ B n = F n ∩ B n holds.
Let us consider the largest such x 1 . Note that we consider only x 2 such that Card(x 1 ) = Card(x 2 ) = n, and that we use the projections π C,P (Definition 29) to separate the events of the process P from the events of the context C.

For any

x 1 we define C[•] := ei∈xi ( (e i ) + c ei ) | [•]
where c ei / ∈ nm(P 1 ) ∪ nm(P 2 ), such that the following holds

• ∃y 1 ∈ [[C[P 1 ]]] such that y 1 is closed, π C,P1 (y 1 ) = x 1 and y 1 ↓ ce i for all e i ∈ x 1 ; • We supposed that [[P 1 ]] ∼ τ [[P 2 ]], so [[C[P 1 ]]] • ∼ τ [[C[P 2 ]]].
Hence ∃ R a backand-forth barbed bisimulation and ∃y

2 ∈ [[C[P 2 ]]] such that (y 1 , y 2 ) ∈ R and y 2 ↓ ce i for all e i ∈ x 1 .
Note that B n is defined on top of F n . We proceed as follows:

• we show that there exists f a label and order preserving bijection between

x 1 and π C,P1 (y 2 );

• then we show that (x 1 , π C,P1 (y 2 ), f ) ∈ F n for f defined above;

• similarly we show that (x 1 , π C,P1 (y 2 ), f ) ∈ B n .

We denote π C,P1 (y 2 ) with x 2 . We have by induction on the trace ∅ -→ y 1 that if y 1 is closed then y 2 is closed as well. Moreover we define a bijection g : y 1 → y 2 that is order and label preserving. It follows again from an induction on the trace ∅ -→ y 1 and from y 2 ↓ ce i for all e i ∈ x 1 .

We have that ∀e 1 , e

e 1 < x1 e 1 =⇒ π -1 C,P1 (e 1 ) < y1 π -1 C,P1 (e 1 ) (11)
=⇒ g(π -1 C,P1 (e 1 )) < y2 g(π -1 C,P1 (e 1 )) (12)
Remark that (11) follows from y 2 ↓ ce i and from the fact that if y 1 is closed we can show by contradiction that y 2 is closed as well. Secondly, [START_REF] De Nicola | Back and forth bisimulations[END_REF] follows from the morphisms reflecting causality. Lastly, (13) follows from g being an order preserving bijection between y 1 and y 2 .

For every events in e 1 , e 2 ∈ y 2 such that e 1 → y2 e 2 from Proposition 3, either π C,P2 (e 1 ) π C,P 2 (y2) π C,P2 (e 2 ) or the projection of the two events are causal dependent in the context. However, the context does not induce any causality between the events. As π C,P2 (e 1 ) π C,P 2 (y2) π C,P2 (e 2 ), we have that there exists f a label and order preserving bijection between x 1 and π C,P1 (y 2 ).

Let us now prove that (x 1 , x 2 , f ) ∈ F n+1 . There are two cases: Using a similar argument to above we have that z 2 is closed and that there exists a bijection h between z 1 and z 2 .

∃x 1 , x 1 e1 -→ x 1 , ∃x 2 , x 2 e2 -→ x 2 (14
Let us denote the projection π C ,P2 (z 2 ) as x 2 . We infer using the fact that z 2 is closed and that z 2 ↓ ce 1 that ∃e 2 ∈ x 2 such that (e 2 ) = (e 1 ).

As there exists a label and order preserving bijection h between z 1 and z 2 , and as we forbid auto concurrency and ambiguous non-deterministic sum (Definition 26), we conclude that x 2 \ {e 2 } = x 2 , for π C ,P2 (z 2 ) = x 2 .

Then we have π C ,P1 (z 1 ) = x 1 , π C ,P2 (z 2 ) = x 2 and f ∪ {e 1 ↔ e 2 } a bijection between the two. As we supposed that x 1 is the largest configuration for which the HHPB breaks we get that ∃x 2 such that (x 1 , x 2 , f ) ∈ F n+1 . But such an x 2 is unique since P 2 is singly labeled. Thus we conclude that (x 1 , x 2 , f ∪ {e 1 ↔ e 2 }) ∈ F n .

The proof that (x 1 , x 2 , f ) ∈ B n goes along the line of (and uses) the proof that (x 1 , x 2 , f ) ∈ F n .

Remark 7 (On Theorem 2). Note that Theorem 2 is a result on RCCS processes that have an empty memory. It is a consequence of HHPB and the back-and-forth barbed congruence on configuration structure (Definition 30) being defined on configuration structures, and not on the tuples of configuration structures and configurations (address). However, we need the reversible setting to simulate the back-and-forth behaviour that we acquire when moving to configuration structures. The result above then should be read as: reversible process with an empty memory are barbed congruent if and only if their encodings in configuration structures are in a HHPB relation.

To make the result more general and include any reversible process we need to reformulate it as follows. We leave this as future work.

Conclusions and future work

We showed that, for a restricted class of RCCS processes (coherent, without recursion, auto-concurrency nor auto-conflict (Definition 26)) hereditary history preserving bisimilarity has a contextual characterization in CCS. We used the barbed congruence defined on RCCS as the congruence of reference, adapted it to configuration structures and then showed a correspondence with HHPB. As a proof tool, we defined two inductively relations that approximate HHPB. Consequently we have that adding reversibility into the syntax helps in retrieving some of the discriminating power of configuration structures.

Note that one could prove the main result of the paper by showing that the bisimulation defined on the LTS of RCCS and the barbed congruence (Definition 14) equate the same terms. We chose to use configuration structures instead, as we plan to investigate other equivalences on reversible process algebra and their encodings as configuration structures give interesting insights.

Weak equivalences. This work follows notable efforts [START_REF] Phillips | Reversibility and models for concurrency[END_REF][START_REF] Lanese | Reversing higher-order pi[END_REF] to understand equivalences for reversible processes. There are numerous interesting continuations. A first one is to move to weak equivalences, which ignores silent moves τ and focus on the observable part of a process. This is arguably a more interesting relation than the strong one, in which processes have to mimic exactly each others' silent moves. Even if such a relation on configuration structures exists [START_REF] Vogler | Bisimulation and action refinement[END_REF][START_REF] Fiore | Weak bisimulation and open maps[END_REF] one still has to show that this is indeed the relation we expect.

In configuration structures, the adjective weak has sometimes [START_REF] Phillips | A hierarchy of reverse bisimulations on stable configuration structures[END_REF][START_REF] Van Glabbeek | Equivalence notions for concurrent systems and refinement of actions (extended abstract)[END_REF] a different meaning: it stands for the ability to change the label and order preserving bijection as the relation grows, to modify choices that were made before this step. It would be interesting to understand what "weak" relations in this sense represent for reversible processes.

Insensitiveness to the direction of the transitions and irreversibility. The relations defined so far simulate forward (resp. backward) transitions only with forward (resp. backward) transitions, and only consider forward barb. Ignoring the direction of the transitions could introduce some fruitful liberality in the way processes simulate each other. Depending on the answer, a + τ.b and a + b would be weakly bisimilar or not. A weak bisimulation that ignores the direction of transitions [START_REF] Lanese | Reversing higher-order pi[END_REF] already exists, but it equates a reversible process with all its derivatives. Irreversible moves could play an important role in such equivalences and would help to understand what are the meaningful equivalences in the setting of transactions [START_REF] Danos | Transactions in RCCS[END_REF].

Reversibility is commonly used in transactional systems, i.e., participative computations where a commitment phase is reached whenever a consensus occurs. This has two effects: it forbids the further exploration of the solution space, and prevents all the participants to complete if a participant cancels the transaction [START_REF] Danos | Self-assembling trees[END_REF]. Commitment is modeled as an irreversible action: such a feature is present in RCCS [START_REF] Danos | Reversible communicating systems[END_REF], but absent from our work. It could probably be implemented by adding a mechanism to "update" the origin of a term, and by "cutting" the configuration structure after an irreversible transition (in the spirit of the LTS of Definition 22). However, it remains to prove that those two actions would be equivalent.

Removing the limitations. Context-which plays a key role-raises questions on the memory handling of RCCS : what about a context that could fix the memory of an incoherent process?

Maybe of less interest but important for the generality of these results, one should include infinite processes as well. This needs to modify the relations F i and B i (Definition 34 and Definition 35) used to approximate the HHPB. In configuration structures, however, one usually handles the recursive case by unfolding the process up to a finite level.

One way to retrieve the class of processes with auto-conflict and autoconcurrence could be to define bisimulations that take into account tagged labels. At the price of a verbose syntax, one could imagine being able to discriminate between configurations reached after firing events with the same labels, thus allowing to define configuration structures for arbitrary RCCS terms. Are relations taking into account those "localities" [36], which uniquely determine occurrences of a label, more discriminating than traditional bisimulations?

Lastly, we conjecture that HHPB is equivalent to a congruence relation on terms that do not exhibit auto-conflict. More precisely, we could imagine that congruent processes have isomorphic event structures, and that configuration structures are isomorphic if and only if they are in HHPB relation.

,

  and if there are indices i 1 , . . . , i n and labels α 1 , . . . , α n such that R 1 i1:α1

Figure 1 :

 1 Figure 1: Rules of the RCCS LTS

Notations 2 .

 2 In a configuration C, if x, x ∈ C, e ∈ E, e / ∈ x and x = x ∪ {e}, then we write x e -→ x . ∅ {e 1 , e 2 } (a) ∅ {e 1 } {e 2 } {e 3 } {e 1 , e 2 } {e 1 , e 2 , e 3 } {e 2 , e 3 } (b) ∅ {e 1 } {e 2 } {e 1 , e 2 } {e 1 , e 3 } {e 2 , e 3 } {e 1 , e 2 , e 3 } (c)

Figure 2 :

 2 Figure 2: Structures that are not coincidence free, finite complete and stable, respectively

  Let E ⊆ E and define the restriction of a set of events (E , C , ) as (E, C, ) E where x ∈ C ⇐⇒ x ∈ C and x ⊆ E . The restriction of a name is then (E, C, ) a := (E, C, ) E a where E a = {e ∈ E | (e) ∈ {a, ā}}. For a 1 , . . . , a n a list of names, we define similarly ∪ 1 i n E ai . Prefix Let α be the label of an event and define the prefix operation on configuration structures as α.(E, C, ) = (e ∪ E, C , ), for e / ∈ E where x ∈ C ⇐⇒ ∃x ∈ C, x = x ∪ e and (e) = α, and ∀e = e, (e ) = (e ).

Definition 22 (Lemma 5 (

 225 LTS on configuration structures[27, p. 131]). Let C = (E, C, ) be a configuration structure. Define C \ {e} = (E \ {e}, C , ) where is the restriction of to the set E \ {e} andx ∈ C ⇐⇒ x ∪ {e} ∈ C.We easily make sure that C \ {e} is also a configuration structures.We define a LTS on configuration structures thanks to the relation C e -→ C \ {e}, and we extend the notation to C (e) -→ C \ {e} and to C x -→ C \ x, for x a configuration. Operational correspondence between a process and its encoding). Let P a process and [[P ]] = (E, C, ) its encoding. 1. ∀α, P such that P α -→ P , ∃e ∈ E such that (e) = α and [[P ]]\{e} ∼ = [[P ]]; 2. ∀e ∈ E, if {e} ∈ C then ∃P such that P (e) -→ P and [[P ]] \ {e} ∼ = [[P ]].

Theorem 1 (

 1 Operational correspondence with CCS). Let P a process and [[P ]] = (E, C, ) its encoding. 1. ∀P such that P τ -→ P , ∃{e} ∈ C closed such that [[P ]] \ {e} ∼ = [[P ]]; 2. ∀e ∈ E, {e} ∈ C closed, ∃P such that P τ -→ P and [[P ]] \ {e} ∼ = [[P ]].

Definition 23 (

 23 Reversible LTS on configuration structures). Consider (E, C, ) a configuration structure. For x ∈ C, e ∈ E define x e -→ x iff x = x ∪ {e} and x α -→ x if additionally, (e) = α. The backward moves are defined as x e x and x α x if x = x ∪ {e} and (e) = α. Denote x e x when either x e -→ x or x e x .Such a LTS naturally satisfies elementary criterion that one would expect from a LTS[START_REF] Cristescu | Operational and denotational semantics for the reversible πcalculus[END_REF] Chap. 2]. This notion should not be mistaken with the immediate causality e → x e Definition 20.

∅ {e 1 ∅ {e 2 } {e 2 } {e 2 , e 2 } {e 2 , e 2 }∅ {e 3 } {e 3 } {e 3 , e 3 } {e 3 , e 3 } {e 3 , e 3 , e 3 }

 1222222333333333 } {e 1 } {e 1 , e 1 } (e 1 ) = (e 1 ) = a, (e 1 ) = b (a) a.b + a (e 2 ) = (e 2 ) = a, (e 2 ) = (e 2 ) = b (b) a.b + a.b (e 3 ) = (e 3 ) = a, (e 3 ) = c, (e 3 ) = b (c) a.(a|c) + b

Figure 3 :

 3 Figure 3: Encoding RCCS in configuration structures

  and (e) = (e ) ⇒ e = e .

Example 6 .-→ 2 ,Proposition 4 (

 624 A first simple example is the encoding of a process with an empty memory. Let S = ∅ P , ε(O S ) = P and [[S]] = ([[P ]], ∅). Let us show how to compute the encoding of the process R = 2, a, 0 . . 1, a, b 0 | . 1, a, b c. We backtrack to its origin and obtain O R = ∅ a.(a | c) + b. The term is encoded into the configuration structure in Figure 3c. We apply the function ad C (∅, O R -→ R) on the trace ∅ a.(a | c) + b a, 0 . . 1, a, b 0 | . 1, a, b c = RThe configuration corresponding to R is then {e 3 , e 3 }. Soundness of the RCCS encoding). Let P be a singly labeled process and C = [[P ]] its encoding. Then for any R reachable from ∅ P there exists a unique x ∈ C such that ad C (∅, ∅, ∅ P -→ R) = x.Proof. Remark that ∅ P = O R and that from Lemma 2, we can consider the trace O R -→ R to be only forward. We proceed by induction on the trace O R -→ R. For the inductive case we have the trace O R -→ R n and adC (∅, ∂ n , O R -→ R n ) = x n , for x n ∈ C, ∂ n alabel and order preserving bijection between x n and R n , and such that [[ε(R n )]] = C \ x n . We have to show that for the trace O R -→ R n i:a

  in which case the process exhibits auto-concurrency, either m 1 = m 2 , in which case the condition j < Rn+1 i ⇐⇒ ∂ n (j) < xn∪{e} e from the definition of the encoding (Definition 27), points to either m 1 or m 2 .Let us prove that ∀x ∈ [[(P1 | P 2 )\(b 1 . . . b n )]], x ∈ [[(a.P 1 | P 2 )\(b 1 . . . b n )]] \ {e}.The other direction is similar. Let us unfold the encoding of Definition 21 using the operations on configuration structures of Definition 18.

Definition 28 (

 28 Reversible LTS in configuration structures). Define ([[P ]], x) P ]], x ∪ {e}) for x ∪ {e} ∈ [[P ]]. Similarly to Definition 3 we define ([[P ]], x) (e) ([[P ]], x \ {e}), for some e such that x \ {e} ∈ [[P ]].

Example 7 .

 7 Consider the configuration structure in Figure 3c, encoding the process P = a.(a | c) + b. The process S = 2, a, 0 . . 1, a, b 0 | 3, c, 0 . . 1, a, b 0 can be reached on the trace σ 1 : ∅ P However both traces lead to the same encoding of S.Hence we write[[R]] instead of [[R]] σ .It is an essential property to prove the existence of a bisimulation relation between a process and its encoding. Lemma 6 (Operational correspondence between a R and [[R]]). Let R a process and [[R]] = (C, x) its encoding. 1. ∀α, S and i ∈ I such that R i:α

Definition 29 .

 29 Let C[•] a context, and P a process. The projection π C,P : [[C[P ]]] → [[P ]] is defined on the structure of C as follows:

Figure 4 :

 4 Figure 4: Two possible hereditary history preserving bisimulations

∅ {e 1

 1 } {e 1 } {e 1 , e 1 } 1 (e 1 ) = a, 1 (e 1 ) = b (a) a | b ∅ {e 2 } {e 2 } {e 2 , e 2 } {e 2 , e 2 } 2 (e 2 ) = 2 (e 2 ) = a, 2 (e 2 ) = 2 (e 2 ) = b (b) a.b + b.a

Figure 5 :

 5 Figure 5: Encoding parallel and sum in configuration structures

  follows by the definition of the bisimulation from x 2 = ∅ and f = ∅.

Figure 6 :

 6 Figure 6: Configuration structures by the end of the proof of Proposition 9

Figure 7 :

 7 Figure 7: Configuration structures by the end of the proof of Theorem 2

) ∃x 1 , x 1 e1-→ x 1 , ∀x 2 , x 2 e2-→ x 2 2 e2-→ x 2 -→ y 1 , 1 e1-→ x 1 .

 1112222111 and (x 1 , x 2 , f ) / ∈ F n[START_REF] Baldan | A logic for true concurrency[END_REF] The implication[START_REF] Bednarczyk | Hereditary history preserving bisimulations or what is the power of the future perfect in program logics[END_REF] is easier: if ∃x 2 , x , then, as a context cannot remove transitions from the original process, ∃y 2 , y 2 (e2, ) -→ y 2 . As [[C[P 2 ]]] and a similar argument on the context shows that ∃x 1 , x Hence a contradiction. Proving (15) requires more work. First, let C [•] := C[•] | ( (e 1 ) + c e1 ). By induction hypothesis, there exists z 1 ∈ [[C [P 1 ]]] such that z 1 is closed, π C ,C[P1] (z 1 ) = y 1 and z 1 ↓ ce i and z 1 ↓ ce 1 for all e i ∈ x 1 . By hypothesis, [[P 1 ]] ∼ τ [[P 2 ]], hence there exists R a back-and-forth barbed bisimulation between [[C [P 1 ]]] and [[C [P 2 ]]]. It implies that ∃z 2 such that z 2 ∈ [[C [P 2 ]]] and z 2 ↓ ce i and z 2 ↓ ce 1 for all e i ∈ x 1 .

Conjecture 1 .

 1 If R ∼ τ S such that [[R]] = (C R , x R ) and [[S]] = (C S , x S )then there exists R a HHPB between C R and C S with (x R , x S , f ) ∈ R, for some f .

  x 2 e2 x 2 and (x 1 , x 2 , f ) ∈ R. By induction hypothesis, ∃x 2 and ∃f such that (x 1 , x 2 , f ) ∈ B k , and therefore (x 1 , x 2 , f ) ∈ F k . As -→ x 2 and (x 1 , x 2 , f ) ∈ F k+1 , by definition of F k . By assumption, (x 1 , x 2 , f ) / ∈ B k+1 , but as

	x 1	e1 -→ x 1 , ∃x 2 and ∃f such that x 2	e 2

  . Whereas the starting point ≈ 0 is the universal relation, F n is not, it is the universal relation only on maximal configurations.3.4. Contextual characterization of HHPBProposition 9 (Hereditary history preserving bisimulation is a congruence). For all singly labeled P 1 , P 2 ,[[P 1 ]] ∼ [[P 2 ]] ⇒ ∀C, [[C[P 1 ]]] ∼ [[C[P 2 ]]].Proof. The proof amounts to carefully build a relation between [[C[P 1 ]]] and [[C[P 2 ]]] that reflects the known bisimulation between [[P 1 ]] and [[P 2 ]]. Its uses that causality in a product is the result of the entanglement of the causality of its elements (Proposition 3).

  there exists R a hereditary history preserving bisimulation (HHPB) between [[P 1 ]] and [[P 2 ]]. Figure 6 introduces the variables names and types.

Event and configuration structures were introduced to define domains for concurrency[START_REF] Nielsen | Petri nets, event structures and domains[END_REF]. Causal models are thus often, but inaccurately, called denotational: a denotational interpretation is supposed to be invariant by reductions, a property that event structures do not have.

Up to minor addition of symbols, as explained later on.

Notably, the configuration structures we introduce and work with, are technically called stable families. However, previous works on equivalences of reversible processes have adopted the term configuration structures and we stick to this convention.

The category of sets and partial functions has sets as objects and functions that can take the value as morphisms [26, Appendix A].

Acknowledgment

We would like to warmly thank D. Varacca and J. Krivine for the useful discussions as well as the referees of an earlier version [1] and of this version for their helpful and insightful remarks.

D Thesis [2]. $$ This work was partly supported by the ANR-14-CE25-0005 ELICA and the ANR-11-INSE-0007 REVER.

Example 8. Consider the configuration structures in Figures 3b and3c, the relations F n are enough to discriminate them: 5a and5b, we need the backward moves as well. Let us first build the F n relations:

We first construct the B 0 relation and then move up in the structures. In our example, the B 2 relation breaks the HHPB.

The following proposition states that pairs of configurations are in a bisimulation relation if they have the same cardinality. It follows from the fact that any configuration is reachable from the empty set and that they have to mimic each others' step in the backward direction. Proposition 8. Let C 1 , C 2 be two configuration structures in a hereditary history preserving bisimulation R and x 1 ∈ C 1 , x 2 ∈ C 2 be two configurations.

If ∃f such that (x 1 , x 2 , f ) ∈ {R} then Card(x 1 ) = Card(x 2 ).

Proof. It follows by induction on the trace ∅ -→ x 1 . For every event in x 1 , we have to add an event in x 2 in order to obtain that the pair x 1 and x 2 are in a HHPB relation.

We conjecture that, for Card(C 1 ) = Card(C 2 ) = n (Definition 33), ∪ n B n is the hereditary history preserving bisimularity on C 1 , C 2 . However, for our main result (Theorem 2) we only need the following weaker lemma: Lemma 8. For all C 1 , C 2 , if there exists a hereditary history preserving bisimulation R such that

and ∃f such that (x 1 , x 2 , f ) ∈ R, as (∅, ∅, ∅) ∈ R and all configurations are reachable from the empty set. The reader should notice that the x 2 ∈ C 2 and f on both sides of the ⇐⇒ symbol may be different.

We prove that statement by induction on Card(x 1 ).