Clément Aubert
email: caubert@augusta.edu

Ioana Cristescu
email: ioana-domnina.cristescu@inria.fr

History-Preserving Bisimulations on Reversible Calculus of Communicating Systems

Keywords: 2012 ACM Subject Classification Theory of computation → Program semantics; Computing methodologies → Concurrent programming languages Formal semantics, Process algebras and calculi, Configuration structures, Distributed and reversible computation, Auto-concurrency

History-and hereditary history-preserving bisimulation (HPB and HHPB) are classical equivalences relations for denotational models of concurrency that are meaningful to study reversible computation. Finding their counterpart in process algebras is an open problem, with some partial successes: there exists in Calculus of Communicating Systems (CCS) an equivalence based on causal trees that corresponds to HPB. In Reversible CSS (RCCS), there are bisimulations corresponding to HHPB, but they consider only restricted classes of process. We propose equivalences on RCCS processes that correspond to HPB and HHPB on all processes. The equivalences exploit not only reversibility but also the memory mechanism of RCCS, and our development shows why both are needed.

Introduction

Reversing Concurrent Computation Reversible systems have the possibility of backtracking to return to some previous state. Implementing reversibility in a programming language often requires a mechanism to record the history of the execution. Ideally, this history should be complete, so that every forward step can be backtracked, and minimal, so that only the relevant information is saved. Concurrent programming languages have additional requirements: the history should be distributed, to avoid centralization, and should prevent steps that required a sychronization with other parts of the program to backtrack without undoing this synchronization. To fulfill those requirements, Reversible Calculus of Communicating Systems (RCCS) [START_REF] Danos | Reversible communicating systems[END_REF][START_REF] Danos | Transactions in RCCS[END_REF] uses memories attached to the threads of a process.

Equivalences for Reversible Processes

A theory of reversible concurrent computation relies not only on a syntax, but also on "meaningful" behavioral equivalences. This paper studies behavioral equivalences defined on configuration structures [START_REF] Winskel | Petri Nets: Central Models and Their Properties, Advances in Petri Nets[END_REF], a classical denotational model for concurrency. In configuration structures, an event represents an execution step, and a configuration-a set of events that occurred-represents a state. A forward transition is then represented as moving from a configuration to one of its supersets. Backward transitions have a "built-in" representation: it suffices to move from a configuration to one of its subset. Multiple behavioral equivalences have been defined for configuration structures ; some of them, like history-and hereditary history-preserving bisimulations (HPB and HHPB) [START_REF] Baldan | Hereditary history-preserving bisimilarity: Logics and automata[END_REF][START_REF] Marek | Hereditary history preserving bisimulations or what is the power of the future perfect in program logics[END_REF][START_REF] Fröschle | On plain and hereditary history-preserving bisimulation[END_REF][START_REF] Phillips | A logic with reverse modalities for history-preserving bisimulations[END_REF][START_REF] Van Glabbeek | History preserving process graphs[END_REF], use that "built-in" notion of reversibility.

memories, and state some properties about them. Finally, Sect. 4.3 uses this encoding to define relations on RCCS processes that are then proven to correspond to HPB and HHPB on configuration structures and connects them to our back-and-forth bisimulation, and Sect. 5 concludes with an interesting connection to our previous formalism. Sect. 2 is compact and serves more as a reminder than as an actual introduction to the topic at stake, but the relations under study as well as RCCS are introduced in great detail and with numerous examples that should guide the reader. As it is common in the study of concurrent computation [START_REF] Winskel | Event structure semantics for CCS and related languages[END_REF][START_REF] Winskel | Models for concurrency[END_REF], we use category theory as a "common language". Only the notion of isomorphism, that is recalled in the body of our work, is really needed, but the curious reader can find a more rigorous development in Appendix A. All the proofs and some auxiliary results are gathered in Appendix B, but we tried to give insights and intuitions on how, and why, the results hold.

Preliminary Definitions

We recall the definitions of configuration structures and some of their restrictions (Sect. 2.1), and how to encode CCS processes into configuration structures (Sect. 2.2). Reversible CCS is recalled last (Sect. 2.3). We write ⊆ the set inclusion, P the power set, \ the set difference, A → B (resp. A B) the set of (resp. partial) functions between A and B, f C the restriction of f : A → B to C ⊆ A, f ∪ {a → b} the function defined as f : A → B on A that additionally maps a / ∈ A to b, and inversely we write f \ {a → b} if f : A → B and f (a) = b for f A\{a} .

Let N = {a, b, c, . . . } be a set of names and N = {a, b, c, . . . } its set of co-names. The complement of a (co-)name is given by a bijection • : N → N, whose inverse is also written •. We write -→ a for a list of names a 1 , • • • , a n . We define the set of labels L = N ∪ N ∪ {τ }, and use α (resp. λ, ν, µ) to range over L (resp. L\{τ }).

Configuration Structures

Definition 1 (Configuration structure). A configuration structure C is a tuple (E, C, L, ) where E is a set of events, L is a set of labels, : E → L is a labeling function and C ⊆ P(E) is a set of subsets satisfying:

∀x ∈ C, ∀e ∈ x, ∃z ∈ C finite, e ∈ z, z ⊆ x (Finiteness) ∀x ∈ C, ∀d, e ∈ x, d = e ⇒ ∃z ∈ C, z ⊆ x, d ∈ z ⇐⇒ e / ∈ z (Coincidence Freeness) ∀X ⊆ C, ∃y ∈ C finite, ∀x ∈ X, x ⊆ y ⇒ X ∈ C (Finite Completeness) ∀x, y ∈ C, x ∪ y ∈ C ⇒ x ∩ y ∈ C (Stability)
We denote 0 the configuration structure with E = ∅, and write x --→ e y and y ¬¬ → e

x for x, y ∈ C such that x = y ∪ {e}.

For the rest of this paper, let x, y, z range over configurations, d, e range over events, and assume that we are always given C = (E, C, L, ) and Example 4. Consider the configuration structures of Fig. 2, where we make the abuse of notation of writing the events as their labels (with a subscript if multiple events have the same label), and where the sets of events, of configurations and of labels can be read from the diagram. Note that two events with complementary names can happen at the same time (Fig. 2c), in which case they are labeled with τ , as is usual in CCS. In Fig. 2c, we have a < b and τ < b; and in Fig. 2b, a 1 and a 2 are concurrent in the configuration {a 1 , a 2 }. A configuration structure can have one (Fig. 2b) or multiple (Fig. 2a and2c) maximal configurations. Finally, we grayed out {a, a} ↓ in Fig. 2c.

C i = (E i , C i , L i , i ), for i = 1, 2.
We now recall how process algebra constructors are defined on configuration structures [START_REF] Winskel | Event structure semantics for CCS and related languages[END_REF]. The definition below may seem technical, but the encoding of CCS processes into configuration structures (Definition 8) will make it clear that it captures the right notions. Product, relabeling and restriction are needed only to define parallel composition.

This definition uses the product (× , p 1 , p 2 ) of the category which has sets as objects and partial functions as morphisms [17, Appendix A]: letting denote undefined for a partial function and C = C ∪ { } for a set C, we define, for two sets A and B,

A × B = {(a, ) | a ∈ A} ∪ {( , b) | b ∈ B} ∪ {(a, b) | a ∈ A, b ∈ B} with p 1 : A × B → A and p 2 : A × B → B the two projections.
Definition 5 (Operations on configuration structures [START_REF] Aubert | Contextual equivalences in configuration structures and reversibility[END_REF][START_REF] Vladimiro Sassone | Models for concurrency: Towards a classification[END_REF]).

The product of C 1 and C 2 is C 1 × C 2 = (E 1 × E 2 , C, L, ). Define the projections π i : C → C i and the configurations x ∈ C such that: ∀e ∈ E, π i (e) = p i (e), π i ( i (e)) = i (π i (e)) π i (x) ∈ C i , with π i (x) = {e i | π i (e) = e i = and e ∈ x} ∀e, e ∈ x, π 1 (e) = π 1 (e ) = or π 2 (e) = π 2 (e ) = ⇒ e = e ∀e ∈ x, ∃z ⊆ x finite, π 1 (x) ∈ C 1 , π 2 (x) ∈ C 2 , e ∈ z ∀e, e ∈ x, e = e ⇒ ∃z ⊆ x, π i (z) ∈ C i , e ∈ z ⇐⇒ e / ∈ z
The labeling function :

E 1 × E 2 → L = L 1 ∪ L 2 ∪ (L 1 × L 2 ) is (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 relabeling of C 1 along r :

E 1 → L is r • C 1 = (E 1 , C 1 , L, r).

The restriction of a set of events

A ⊆ E 1 in C 1 is C 1 A = (E 1 \ A, C, L, 1 E1\A ), where x ∈ C ⇐⇒ x ∈ C 1 and x ∩ A = ∅, and L = {α | ∃e ∈ A, 1 (e) = α}. The restriction of a name a in C 1 is C 1 a = C 1 E a 1 where E a 1 = {e ∈ E 1 | (e) ∈ {a, a}}. For - → a = a 1 , . . . , a n a list of names, we define similarly C 1 - → a = C 1 E - → a 1 for E - → a 1 = {e ∈ E 1 | (e) ∈ {a 1 , a 1 , . . . , a n , a n }}. The parallel composition of C 1 and C 2 is C 1 | C 2 = r • (C 1 × C 2 ) E ⊥ 3 , with C 1 × C 2 = C 3 = (E 3 , C 3 , L 3 , 3 ) is the product; r • C 3 with r : E 3 → L 1 ∪ L 2 ∪ {⊥} defined as follows: r(e) =      3 (e) if 3 (e) ∈ N ∪ N τ if 3 (e) ∈ {(a, a), (a, a), τ | a ∈ N} ⊥ otherwise (r • C 3 ) E ⊥ 3 , where E ⊥ 3 = {e ∈ E 3 | r(e) = ⊥}. The coproduct of C 1 and C 2 is C 1 + C 2 = 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, for π 1 (e) = i, as (e) = i (π 2 (e)) and L = L 1 ∪ L 2 . The prefixing of C 1 by the name λ is λ.C 1 = (e ∪ E 1 , C, L 1 ∪ {λ}, ), for e / ∈ E 1 , where x ∈ C ⇐⇒ x = ∅ ∨ ∃x ∈ C 1 , x = x ∪ e ; (e) = λ and ∀e = e, (e ) = 1 (e ).
As detailed in Appendix A, configuration structures and "structure-preserving" functions form a category. This development can be omitted, except for the notion of isomorphisms:

Definition 6. We write C 1 ∼ = C 2 if there exists an isomorphism f = (f E , f L , f C ); a bijection such that f E : E 1 → E 2 preserves labels, 2 (f E (e)) = f L ( 1 (e)), for f L : L 1 → L 2 ; and f C : C 1 → C 2 is defined as f C (x) = {f E (e) : e ∈ x}.
Some constraints were used in showing equivalences between process algebra and configuration structures:

C \ z = (E \ z, {z | z ∪ z ∈ C}, E\z ), then C is singly labeled [1, Definition 26].

CCS and its Encoding in Configuration Structures

The set of CCS processes is inductively defined:

P, Q := P | Q λ.P + ν.Q P \a 0 (CCS Processes)
We often omit 0, and write e. Definition 8 (Encoding a CCS process [START_REF] Winskel | Models for concurrency[END_REF]). Given a CCS process P , its encoding P as a configuration structure is built inductively: 3, where the grayed out parts are {c, τ, b} ↓ and {c, a} ↓.

λ.P + ν.Q = λ.P + ν.Q λ.P = λ. P P \a = P a P | Q = P | Q 0 = 0 Example

Definition 10 (Restrictions on CCS processes).

A process P is non-repeating (resp. without auto-concurrency, singly labeled) if P is (Definition 7).

Example 11. Every non-repeating configuration is without auto-concurrency, but the other pairs of restrictions are independent, as suggested below:

Non-repeating Without auto-concurrency Singly labeled a a.a

X (a.b) | a X X a + a X a.(a + a) X X a | (a.(b + b)) X X X

Reversible CCS

Let I be a set of identifiers, and i, j range over its elements: an identifier can be anything, but a reasonable implementation would use integers or Linux's pid_t datatype. The set of reversible processes R is built on top of the set of CCS processes by adding memory stacks to the threads: We will treat CCS and "memory-less" reversible processes to be the same, i.e. we will sometimes treat P as being identical to ∅ P : we come back to this in Definition 15.

i /

∈ I(m) act. (m λ.P + Q) ---→ i:λ i, λ, Q .m P R ---→ i:λ R S ---→ i:λ S syn. R | S ---→ i:τ R | S i / ∈ I(m) act. * i, λ, Q .m P ¬¬¬ → i:λ m (λ.P + Q) R ¬¬¬ → i:λ R S ¬¬¬ → i:λ S syn. * R | S ¬¬¬ → i:τ R | S R ---→ → i:α R i / ∈ I(S) par. R | S ---→ → i:α R | S R ---→ → i:α R a / ∈ α res. R\a ---→ → i:α R \a R 1 ≡ R ---→ → i:α R ≡ R 1 ≡ R 1 ---→ → i:α R 1
m (λ.P + ν.Q) ≡ m (ν.Q + λ.P ) (Sum Symmetry) m ((λ.P + ν.Q) + µ.R) ≡ m (λ.P + (ν.Q + µ.R)) (Sum Associativity) P = α Q m P ≡ m Q (α-Conversion) m (P | Q) ≡ ( .m P | .m Q) (Distribution of Memory)
m P \a ≡ (m P )\a with a / ∈ nm(m) (Scope of Restriction)

The labeled transition system for RCCS is given by the rules of Fig. 4. We use ---→ → i:α

for the union of ---→ i:α (forward) and ¬¬¬ → i:α (backward transition), and if there are indices i 1 , . . . , i n and labels α 1 , . . . , α n such that R 1 ----→ →

i1:α1 • • • ----→ → in:αn R n , then we write R 1 --→ → R n .
Note that those rules are presented with the guarded sum of CCS for concision and clarity, but we will consider for instance ∅ a.P ---→ 1:a 1, a, 0 .∅ P to be a legal transition. Example 14. An example of valid (forward-only) execution, or trace, is:

∅ (a.b | c.a) ≡ ( .∅ a.b) | ( .∅ c.a) (Distribution of Memory) ---→ 1:c ( .∅ a.b) | ( 1, c, 0 . .∅ a) (act.) ---→ 2:τ ( 2, a, 0 . .∅ b) | ( 2, a, 0 . 1, c, 0 . .∅ 0) (syn.) ---→ 3:b ( 3, b, 0 . 2, a, 0 . .∅ 0) | ( 2, a, 0 . 1, c, 0 . .∅ 0) (act.)
Reading it from end to beginning and replacing ---→

_:_ with ¬ ¬ ¬ → _ : _
gives a backward-only execution. Of course, an execution can be a mix of forward and backward transitions.

Definition 15 (Reachable [1, Lemma 1]). If there is a CCS term P such that ∅ P --→ → R, we say that R is reachable, that P is the origin of R and write P = O R .

An important result [5, Lemma 10] furthermore states that this transition ∅ P --→ → R can always be taken to be forward-only. Also, note that multiple RCCS terms can have the same origin, but that a reachable RCCS term has one unique origin (up to structural

∅ {a} {a, b 1 } {a, b 2 } (a) a.(b + b) ∅ {a 1 } {a 2 } {a 1 , b 1 } {a 2 , b 2 } (b) (a.b) + (a.b) ∅ {a 1 } {b} {a 1 , b} {a 1 , a 2 } {a 1 , a 2 , b} (c) (a.a) | b ∅ {a 1 } {a 2 } {b} {a 1 , a 2 } {a 1 , b} {a 2 , b} {a 1 , a 2 , b} (d) a | a | b Figure 5
Examples of configuration structures that are or not in HPB and HHPB relations equivalence). We consider only reachable terms: unreachable terms are "dysfunctional", since their memory is not coherent [START_REF] Danos | Transactions in RCCS[END_REF] and they can not be "rewinded" back to an origin process.

Definition 16 (Restrictions on RCCS processes).

A process R is non-repeating (resp. without auto-concurrency, singly labeled) if O R is (Definition 7).

Reversible Bisimulations

In this section we introduce bisimulations on configuration structures (Sect. 3.1) and on RCCS (Sect. 3.2), which aim at capturing reversibility.

History-Preserving Bisimulations in Configuration Structures

History-preserving bisimulation (HPB) [START_REF] Baldan | Hereditary history-preserving bisimilarity: Logics and automata[END_REF][START_REF] Phillips | A logic with reverse modalities for history-preserving bisimulations[END_REF][START_REF] Rabinovich | Behavior structures and nets[END_REF] and hereditary history-preserving bisimulation (HHPB) [START_REF] Baldan | Hereditary history-preserving bisimilarity: Logics and automata[END_REF][START_REF] Marek | Hereditary history preserving bisimulations or what is the power of the future perfect in program logics[END_REF] are equivalences on configuration structures that use label-and order-preserving bijections between the events of the two configuration structures.

Definition 17 (Label-and order-preserving functions). A function f :

x 1 → x 2 , for x i ∈ C i , i ∈ {1, 2} is label-preserving if 1 (e) = 2 (f (e))
for all e ∈ x 1 . It is order-preserving if e 1 x1 e 2 ⇒ f (e 1 ) x2 f (e 2 ), for all e 1 , e 2 ∈ x 1 .

Definition 18 (HPB and HHPB

). A relation R ⊆ C 1 × C 2 × (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 and (1) and (2) (resp. [START_REF] Aubert | Contextual equivalences in configuration structures and reversibility[END_REF][START_REF] Baldan | Hereditary history-preserving bisimilarity: Logics and automata[END_REF][START_REF] Marek | Hereditary history preserving bisimulations or what is the power of the future perfect in program logics[END_REF][START_REF] Boudol | Permutation of transitions: An event structure semantics for CCS and SCCS[END_REF]) hold is called a history-(resp. hereditary history-) preserving bisimulation (HPB, resp. HHPB) between C 1 and C 2 .

∀y 1 , x 1 --→ e1 y 1 ⇒ ∃y 2 , g, x 2 --→ e2 y 2 , g x1 = f, (y 1 , y 2 , g) ∈ R (1)
∀y 2 , x 2 --→ e2 y 2 ⇒ ∃y 1 , g, x 1 --→ e1 y 1 , g x1 = f, (y 1 , y 2 , g) ∈ R (2)
∀y 1 , x 1 ¬¬ → e1 y 1 ⇒ ∃y 2 , g, x 2 ¬¬ → e2 y 2 , g = f y1 , (y 1 , y 2 , g) ∈ R (3)
∀y 2 , x 2 ¬¬ → e2 y 2 ⇒ ∃y 1 , g, x 1 ¬¬ → e1 y 1 , g = f y1 , (y 1 , y 2 , g) ∈ R (4)
We write that C 1 and C 2 are (H)HPB if there exists a (H)HPB relation between them.

Example 19. Note that HPB and HHPB are two different relations, and that HHPB is not the structural congruence of CCS: the classical example [START_REF] Van Glabbeek | Refinement of actions and equivalence notions for concurrent systems[END_REF] of processes whose encodings are HPB but not HHPB is (a

| (b + c)) + (a | b) + ((a + c) | b) and (a | (b + c)) + ((a + c) | b).
The two processes a.(b + b) and (a.b) + (a.b) are not structurally congruent in CCS, but their encodings, presented in Fig. 5a and5b, are HHPB.

F-R bisimulation (Definition 20) on non-repeating CCS processes (Definition 10)

corresponds to HHPB on their encoding [START_REF] Phillips | Reversibility and models for concurrency[END_REF].

Back-and-forth barbed congruence on singly labeled CCS processes (Definition 10)

corresponds to HHPB on their encoding [START_REF] Aubert | Contextual equivalences in configuration structures and reversibility[END_REF]. 3. Back-and-forth bisimulation (Definition 20) and Hereditary history-preserving bisimulation (resp. history-preserving bisimulation) (Definition 32) on all CCS processes correspond to HHPB (resp. HPB) on their encoding (Theorem 36, Corollary 38).

Back-and-forth Bisimulations in Reversible CCS

Let us now review the preliminary attempts to capture HHPB as a relation on process algebra terms [START_REF] Aubert | Contextual equivalences in configuration structures and reversibility[END_REF][START_REF] Phillips | Reversibility and models for concurrency[END_REF], and present the relation we will be using. We use the setting of RCCS to present these results, and synthesize them, along with our new result, in Fig. 6.

Definition 20 (B&F, SB&F, FR bisimulations). A relation R ⊆ R × R × (I I) such that (∅ P 1 , ∅ P 2 , ∅) ∈ R and if (R 1 , R 2 , f ) ∈ R, then f is a bijection between I(R 1 ) and I(R 1 )
and [START_REF] Danos | Reversible communicating systems[END_REF][START_REF] Danos | Transactions in RCCS[END_REF][START_REF] Darondeau | Causal trees: Interleaving + causality[END_REF][START_REF] Fröschle | On plain and hereditary history-preserving bisimulation[END_REF] hold is called a back-and-forth-bisimulation (B&F bisim) between R 1 and R 2 .

∀S 1 , R 1 ---→ i:α S 1 ⇒ ∃S 2 , g, R 2 ---→ j:α S 2 , g = f ∪ {i → j}, (S 1 , S 2 , g) ∈ R (5)
∀S 2 , R 2 ---→ i:α S 2 ⇒ ∃S 1 , g, R 1 ---→ j:α S 1 , g = f ∪ {i → j}, (S 1 , S 2 , g) ∈ R (6)
∀S 1 , R 1 ¬¬¬ → i:α S 1 ⇒ ∃S 2 , f, R 2 ¬¬¬ → j:α S 2 , g = f \ {i → j}, (S 1 , S 2 , g) ∈ R (7)
∀S 2 , R 2 ¬¬¬ → i:α S 2 ⇒ ∃S 1 , g, R 1 ¬¬¬ → j:α S 1 , g = f \ {i → j}, (S 1 , S 2 , g) ∈ R (8)
If f = id, we call R a forward-reverse bisimulation (FR bisim), and if we remove the requirements on f , we call R a simple back-and-forth bisimulation (SB&F bisim). We write that R 1 and R 2 (resp. P 1 and P 2 ) are B&F bisim if there exists a B&F bisim relation between them (resp. between ∅ P 1 and ∅ P 2 ), and similarly for FR bisim and SB&F bisim.

FR bisim [START_REF] Phillips | Reversing algebraic process calculi[END_REF][START_REF] Phillips | Reversibility and models for concurrency[END_REF] was used to get the first result on capturing HHPB:

Theorem 21 ([10, Theorem 5.4]). Two CCS processes with non-repeating events are in FR bisim iff their encoding are HHPB.

However, back-and-forth bisimulations do not use in a meaningful way the identifiers when restricted to non-repeating processes, which are trivially without auto-concurrency: Theorem 22. On the class of processes without auto-concurrency, B&F bisim and SB&F bisim are the same relations.

The intuition behind this theorem is that since two concurrent transitions sharing the same label can not be fired at the same time, the process being without auto-concurrency, the identifiers do not add any information. The proof is easy for the forward transitions, and uses an order on the transitions enforced by causality for the backward traces.

Example 23. Observe that the bisimulation relation obtained from Definition 20 by only considering ( 5) and ( 6) and ignoring the identifiers is the "standard" bisimulation of CCS. The processes (a.a) | b and a | a | b are in this "standard" bisimulation, but their encodings, presented in Fig. 5c and5d, are not HPB. Also note that those two processes are SB&F bisim but that their encodings are not HHPB. This example shows that SB&F bisim does not characterize HHPB on processes with auto-concurrency, and supports that both the bijection on identifiers and the backward transitions are necessary to capture HHPB.

A second attempt [START_REF] Aubert | Contextual equivalences in configuration structures and reversibility[END_REF] to capture HHPB used a back-and-forth barbed congruence on RCCS processes which was proven to correspond to HHPB on their encoding for the class of singly-labeled processes (Definition 10). Even if this restriction may seem lighter than forbidding not non-repeating structures and easier to justify (it is a restriction relative to "the future" of the configurations), it is actually an orthogonal restriction to being non-repeating, and forbid processes as simple as a+a (Example 11). We lift both restrictions in the following, by proving that B&F bisim captures HHPB on all processes.

Lifting the Restrictions

To prove that B&F bisim corresponds to HHPB on all processes (Corollary 38), we first define bisimulations on RCCS (Sect. 4.3) that are then proven to correspond to (H)HPB (Theorem 36). The relation that characterizes HHPB coincides with B&F bisim (Theorem 37). Those relations on RCCS use identified configuration structures (Sect. 4.1) to encode the memories of reversible processes (Sect. 4.2).

Identified Configuration Structures

Identified configuration structures arise from the observation that events can carry, on top of a label, an identifier reflecting the history of a reversible process, as recorded by its memory.

Definition 24 (Identified configuration structure). An identified configuration structure, or For the rest of this paper, we assume always given I = (E, C, L, , I, m) and

I-structure, I = (E, C, L, , I, m) is a configuration structure C = (E, C, L, )
I i = (E i , C i , L i , i , I i , m i ), for i = 1, 2.
Using Definition 5, we define the following operations: Definition 25 (Operations on I-structures). The product of I 1 and I 2 is

I 1 × I 2 = (E, C, L, , I, m): (E 1 , C 1 , L 1 , 1 )×(E 2 , C 2 , L 2 , 2 ) = (E, C, L, ) is the product of configuration structures with projections π i : (E, C, L, ) → (E i , C i , L i , i ); I = (I 1 ∪ {m }) × (I 2 ∪ {m }), for m / ∈ I 1 ∪ I 2 ; m : E 1 × E 2 → I is defined as m(e) =      (m 1 (π 1 (e)), m ) if π 2 (e) = (m , m 2 (π 2 (e))) if π 1 (e) = (m 1 (π 1 (e)), m 2 (π 2 (e))) otherwise
with the projections θ i : I → I i ∪ {m } and θ i (j 1 , j 2 ) = j i . Define the projections γ i :

I 1 × I 2 → I i as the pair (π i , θ i ). The relabeling of I 1 along r : E 1 → L is r • I 1 = (E 1 , C 1 , L, r, I 1 , m 1 ).

The restriction of a set of events

A ⊆ E 1 in I 1 is I 1 A = (E 1 , C 1 , L 1 , 1 ) A ⊕ (m 1 E1\A ).
Similarly we define the restriction of a name.

The parallel composition of I 1 and I 2 is

I 1 | I 2 = (E, C, L, , I, m), with I 1 × I 2 = I 3 = (E 3 , C 3 , L 3 , 3 , I 3 , m 3 ) is the product of I-structures. r • I 3 , with r : E 3 → L ∪ {⊥} defined as follows, r(e) =                                  ⊥ if π 1 (e) = e 1 = ∧ π 2 (e) = e 2 = ∧ m 1 (e 1 ) = m 2 (e 2 ) or if π 1 (e) = e 1 = ∧ π 2 (e) = ∧ ∃e 2 ∈ E 2 , m 1 (e 1 ) = m 2 (e 2 ) or if π 2 (e) = e 2 = ∧ π 1 (e) = ∧ ∃e 1 ∈ E 1 , m 1 (e 1 ) = m 2 (e 2 )) τ if π 1 (e) = e 1 = ∧ π 2 (e) = e 2 = ∧ m 1 (e 1 ) = m 2 (e 2 ) ∧ 3 (e) = (α, α) α if π 1 (e) = e 1 = ∧ π 2 (e) = e 2 = ∧ m 1 (e 1 ) = m 2 (e 2 )
∧ 3 (e) = (α, α)

3 (e) otherwise (Err. 1)

(Err. 2) (Err. 3) (Sync.) (Fork) (r • I 3 ) F = (E, C, L, , I, m ), where F = {e ∈ E 3 | r(e) = ⊥}; m is defined as m(e) = i for m (e) = (i, m ) or m (e) = (m , i), or if m (e) = (i, j)
and i = j. The postfixing of the memory event i, λ, P to I 1 , is defined if i is not already an identifier in I 1 as L,,I,m) where

I 1 • i, λ, P = (E, C,
E = E 1 ∪ {e}, for e / ∈ E 1 , C = C 1 ∪ {x ∪ {e} | x ∈ C 1 is maximal}, L = L 1 ∪ {λ}, = 1 ∪ {e → λ}, I = I 1 ∪ {i}, m(e ) = m 1 (e ) if e = e,
and m(e) = i otherwise.

In parallel compositions, r detects the wrong synchronization (or fork) pairs: if two events occur at the same time, then they must have the same identifier. In the case where an event occurs alone, then no other event can occur with the same identifier. The last step of the parallel composition consists in removing the spurious m from the events identifiers. Definition 27 will detail how those operations correspond to the encoding of a memory.

As detailed in Appendix A, I-structures and "structure-preserving" functions form a category. This development supports the interest and validity of studying I-structures, but can be omitted, except for the notion of isomorphism, that echoes Definition 6: Definition 26. We write I 1 ∼ = I 2 if there exists an isomorphism q = (f, f m ), i.e., an isomorphism f = (f E , f L , f C ) between F(I 1 ) and F(I 2 ) endowed with a function f m :

I 1 → I 2 that preserves identifiers: f m (m 1 (e)) = m 2 (f E (e)).

Encoding the Memory of Reversible Processes

We show and illustrates in this section how I-structures can encode memories, and highlight some properties of this encoding that will be useful in proving our main results.

Definition 27 (Encoding a RCCS memory). The encoding of the memory of a RCCS process in a I-structure is defined by induction on the process and on the memory:

m P = m R 1 | R 2 = R 1 | R 2 R\a = R i, λ, P .m = m • i, λ, P .m = m ∅ = 0
The memories of any RCCS process could be encoded into I-structures, but we will consider only reachable processes (Definition 15), and thus coherent memories.

For the rest of this paper, we assume given reachable reversible processes R, R 1 , R 2 and S, we write O R for the origin of R, R as (E R , C R , R , I R , m R ) and similarly for S.

The underlying configuration of R is included in O R . We come back on this observation in Sect. 5, but we can observe that it is suggested by the following examples.

Example 28. Looking back at the transition detailed in Example 14, we can observe that:

( 3, b, 0 . 2, a, 0 . .∅ 0) | ( 2, a, 0 . 1, c, 0 . .∅ 0) = 3, b, 0 . 2, a, 0 . .∅ 0 | 2, a, 0 . 1, c, 0 . .∅ 0 = 3, b, 0 . 2, a, 0 . .∅ | 2, a, 0 . 1, c, 0 . .∅
We can let L = {a, a, b, c}, (x) = x for x ∈ L, I = {1, 2, 3}, and have:

3, b, 0 . 2, a, 0 . .∅ = ({a, b}, {∅, {a}, {a, b}}, L, , I, {a → 2, b → 3} 2, a, 0 . 1, c, 0 . .∅ = ({c, a}, {∅, {c}, {c, a}}, L, , I, {c → 1, a → 2})
whose underlying structures are in Fig. 3a and3b. The product of those two configurations gives the following set of events (where we keep naming the events after their label):

(a, ) (ev. 1) (b, ) (ev. 2) ( , c) (ev. 3) ( , a) (ev. 4) (a, c) (ev. 5) (a, a) (ev. 6) (b, c) (ev. 7) (b, a) (ev. 8)
When doing the parallel composition, the relabeling step labels with ⊥ events ev. 5, ev. 7 and ev. 8, since the event identifiers do not match in the pair, as well as ev. 1 and ev. 4, since they have the same identifier but occur unsynchronized. The relabeling also changes the labels of events ev. 2, ev. 3 and ev. 6 into b, c and τ , respectively. Hence, we obtain the I-structure whose underlying structure is the gray part of Fig. 3c, with m( , c) = m(c) = 1, m(a, a) = m(τ ) = 2 and m(b, ) = m(b) = 3. Observe that the structure underlying the encoding of the memory is just a particular "path" in that configuration structure.

Example 29. The encoding of the memory resulting from the (partial) execution

∅ (a.b | c) ---→ 1:c ---→ 2:a ( 2, a, 0 . .∅ b) | ( 1, c, 0 . .∅ 0)
has for underlying structure the gray part in Fig. 3d, with m(c) = 1 and m(a) = 2.

I-structures resulting from the encoding of processes have interesting properties:

Lemma 30. For all e 1 , e 2 ∈ E R , m R (e 1 ) = m R (e 2 ) implies e 1 = e 2 .
In particular, all memory events in R are either causally linked or concurrent, therefore the encoding of the memory of R results in a partially ordered set with one maximal element (Definition 2), linked by the subset relation. This was illustrated by the previous two examples and is proved by induction on the RCCS process.

Lemma 31. R is a partially ordered set (poset) with one maximal configuration.

(Hereditary) History-Preserving Bisimulations on CCS

Our main task now is to define relations on CCS, that we named HPB and HHPB (Definition 32), and then to prove that those relations correspond to their counterparts on the encoding of terms (Theorem 36) and that HHPB corresponds to B&F bisim on all processes (Corollary 38). This requires a notion of maximal event that relates to the operational semantics of RCCS (Lemma 34), and to prove that isomorphisms between I-structures and label-and order-preserving bijections on the configurations are the same concept (Lemma 35). [START_REF] Phillips | Reversibility and models for concurrency[END_REF] and [START_REF] Phillips | Reversing algebraic process calculi[END_REF] (resp. [START_REF] Phillips | Reversibility and models for concurrency[END_REF][START_REF] Phillips | Reversing algebraic process calculi[END_REF][START_REF] Phillips | A logic with reverse modalities for history-preserving bisimulations[END_REF][START_REF] Rabinovich | Behavior structures and nets[END_REF]) hold is called a history-(resp. hereditary history-) preserving bisimulation between R 1 and R 2 .

Definition 32 (HPB and HHPB on RCCS

). A relation R ⊆ R × R × (E 1 E 2 ) such that (∅ O R1 , ∅ O R , ∅) ∈ R and if (R 1 , R 2 , f ) ∈ R then f is an isomorphism between R 1 and R 2 and
∀S 1 , R 1 ---→ i:α S 1 ⇒ ∃S 2 , g, R 2 ---→ j:α S 2 , g R1 = f, (S 1 , S 2 , g) ∈ R (10)
∀S 2 , R 2 ---→ i:α S 2 ⇒ ∃S 1 , g, R 1 ---→ j:α S 1 , g R1 = f, (S 1 , S 2 , g) ∈ R (11) ∀S 1 , R 1 ¬¬¬ → i:α S 1 ⇒ ∃S 2 , f, R 2 ¬¬¬ → j:α S 2 , g = f S1 , (S 1 , S 2 , g) ∈ R (12) ∀S 2 , R 2 ¬¬¬ → i:α S 2 ⇒ ∃S 1 , g, R 1 ¬¬¬ → j:α S 1 , g = f S1 , (S 1 , S 2 , g) ∈ R (13)
If there exists a (H)HPB relation between R 1 and R 2 (resp. between ∅ P 1 and ∅ P 2 ), we say that R 1 and R 2 (resp. P 1 and P 2 ) are (H)HPB.

Note that the definitions above reflect Definition 18: the condition (∅ O R1 , ∅ O R , ∅) ∈ R is intuitively the counterpart to the condition that (∅, ∅, ∅) has to be included in the relation on configuration structures. Also, f shares similarity with the label-and order-preserving bijection (this will be made formal in Lemma 35).

Definition 33 (Maximal event).

An event e is maximal in I if there is no event e such that e < x m e , for x m a maximal configuration of I.

Note that by Lemma 31, the encoding of a memory has at most one maximal configuration, but that does not prevent it from having multiple maximal events: Fig. 3d is an I-structure resulting from the encoding of a memory with two maximal events, labeled a and c.

The following lemma shows the operational correspondence between a RCCS process and its encoding in I-configuration structure.

Lemma 34. 1. For all transitions R ---→ i:α S, R ∼ = S {e} with e maximal in S and m S (e) = i.

For all transitions R ¬¬¬ →

i:α S, S ∼ = R {e} with e maximal in R and m R (e) = i.

3.

For any maximal event e in R , there is a transition R ¬¬¬¬¬¬¬¬ → m R (e): R (e) S with S ∼ = R {e} .

The proof, for 1, shows that the transition triggered the creation of a maximal event with the same identifier, and nothing else, and that this event can be "traced" in S . It uses intermediate lemma showing how maximal events are preserved by certain operations on I-structures. Part 2 follows easily, but 3 is more involved: it requires to show that e can be mapped to a particular transition in the trace from O R to R, and, using a notion of trace equivalence, that this particular transition can be "postponed" and done last, so that R can backtrack on it.

Lemma 35. Letting x m

1 and x m 2 be the unique maximal configuration in R 1 and R 2 , R 1 ∼ = R 2 iff there exists a label-and order-preserving bijection between x m 1 and x m 2 .

Theorem 36. P 1 and P 2 are HHPB (resp. HPB) iff P 1 and P 2 are.

In the definition of (H)HPB on configuration structures (Definition 18), removing the condition that the bijection f on events must be preserved from one step to the next gives the definition of weak-HPB and weak-HHPB [START_REF] Marek | Hereditary history preserving bisimulations or what is the power of the future perfect in program logics[END_REF][START_REF] Phillips | A logic with reverse modalities for history-preserving bisimulations[END_REF]. The same loosening can be done on the definition of (H)HPB on RCCS (Definition 32), and a theorem similar to Theorem 36 regarding those "weak" relations can easily be proven.

Theorem 37. HHPB and B&F bisim coincide on all CCS processes.

The proofs of those two results are relatively easy, once we have all the intermediate lemmas, and use one relation to define the other. Theorem 36 (resp. Theorem 37) uses our operational correspondence between RCCS processes (resp. RCCS memories) and their encodings as configuration structures [1, Lemma 6] (resp. as I-structure (Lemma 34)) to transition between the semantic and syntactic worlds.

Corollary 38 (Main result). P 1 and P 2 are B&F bisim iff P 1 and P 2 are HHPB.

Proof. This is an immediate corollary of Theorem 37 and Theorem 36.

Concluding Remarks

As we stressed, this work offers a "definitive" answer to the question of finding a relation for process algebras that corresponds to (H)HPB on their encodings for all processes. It uses the memory mechanism of RCCS, or, more precisely, the encoding of this memory into an "enriched" configuration structure, called identified configuration structure. This observation echoes our previous formalism [START_REF] Aubert | Contextual equivalences in configuration structures and reversibility[END_REF] in an interesting way: as mentioned in Sect. 1, we offered to encode a reversible process R as a pair ( O R , x R ) made of the configuration structure encoding the origin of R, and a configuration x R in it, called the address of R. The intuition was that we could "match" a partially executed process with a configuration. We can go further, and observe that the encoding of the memory of R has the same underlying configuration structure as the structure generated by its address, x R ↓ (Definition 3). This lemma is actually used to prove Theorem 36, and it reads:

Lemma 39. The underlying configuration structure of R is isomorphic to x R ↓.

We can now come back to the intuitions of Fig. 1 using Example 29: the encoding of the memory of ( 2, a, 0 . .∅ b) | ( 1, c, 0 . .∅ 0) corresponds the "past" of the process, whose underlying structure is grayed out in Fig. 3d. What is left to execute, b | 0, corresponds to the "future" of that process, and is represented by the configuration {c, a, b} in Fig. 3d. Note that the configuration {a, b} is not part of the past nor of the future of this process, as reaching this configuration would require to undo c first.

Different versions of the back-and-forth bisimulation have been previously proposed for reversible processes and with the adequate restrictions on the class of processes, these versions coincide. But to capture HHPB on all process, B&F bisim uses both the reversibility and the memory mechanisms of RCCS. As we show with Example 23, using only the backward transitions does not capture HHPB on processes with auto-concurrency.

As future work, we plan to investigate the versions of HPB and HHPB where the τ transitions are ignored. We would also like to identify a criteria to determine what the "right" structural equivalence for RCCS is: as of now, our equivalence excludes e.g. R | 0 ≡ R for technical reasons that should be overcome.

A Category Theory

Configuration structures often use the insights provided by the categorical framework [START_REF] Aubert | Contextual equivalences in configuration structures and reversibility[END_REF][START_REF] Vladimiro Sassone | Models for concurrency: Towards a classification[END_REF][START_REF] Winskel | Event structure semantics for CCS and related languages[END_REF]. We regroup in this appendix the categorical treatment related to the configuration structures and to the identified configuration structures.

Definition 40 (Category of configuration structures). We define C the category of configuration structures, where an object is a configuration structure, and a morphism f :

C 1 → C 2 is a triple (f E , f L , f C ) such that f E : E 1 → E 2 preserves labels: 2 (f E (e)) = f L ( 1 (e)), for f L : L 1 → L 2 ; f C : C 1 → C 2 is defined as f C (x) = {f E (e) : e ∈ x}. If there exists an isomorphism f : C 1 → C 2 , then we write C 1 ∼ = C 2 .
Observe that C has 0 for initial object. For simplicity, we often assume that L 1 = L 2 , i.e., that all the configuration structures use the same set of labels, take f L to be the identity and remove it from the notation.

Definition 41 (Category of I-structures). We define D the category of identified configuration structures, where objects are I-structures, and a morphism f :

I 1 → I 2 is a tuple q = (f, f m ) such that f = (f E , f C ) is a morphism in C between the underlying structures of I 1 and I 2 , f m : I 1 → I 2 preserves identifiers: f m (m 1 (e)) = m 2 (f E (e))
. If there exists an isomorphism q : I 1 → I 2 , then we write

I 1 ∼ = I 2 .
Observe that D as for initial object 0, and that C is a subcategory of D. In both C and D, composition is written • and defined componentwise.

Lemma 42. Identified configuration structures and their morphisms form a category.

Proof. Identity For every I-structure I = (E, C, , I, m), id I : I → I is defined to be the identity on the underlying configuration structure id : (E, C, ) → (E, C, ) from C, that trivially preserves identifiers. For any morphism f :

I 1 → I 2 , f • id I1 = f = id I2 •f is trivial. Associativity for f : I 1 → I 2 , g : I 2 → I 3 and h : I 3 → I 4 , h • (g • f ) = (h • g) • f is
inherited from the associativity in C, and since f , g and h all preserves identifiers. Hence D is a category.

Unsurprisingly, a forgetful functor and an enrichment functor can be defined between those two categories. The only assumption is that we need to suppose that every configuration structure can be endowed with a total ordering on its events.

Lemma 43. The forgetful functor

F : D → C, defined by F(E, C, , I, m) = (E, C, ) F(f E , f C , f m ) = (f E , f C ) and S : C → D,
) : (E 1 , C 1 , 1 ) → (E 2 , C 2 , 2 ), S(f E , f C ) = (f E , f C , f m ), where we let f m (m 1 (e)) = m 2 (f E (e 2 )).
are functors.

Proof. Proving that F is a functor is immediate. Proving that S(C) is a I-structure is immediate, since our construction of m trivially insures Collision Freeness. For (f E , f C ) : C 1 → C 2 , proving that S(f E , f C ) is a morphism between S(C 1 ) and S(C 2 ) is also immediate. For the preservation of the identity, we compute:

S(id C ) = S(id E , id C ) = (id E , id C , f m )
where f m (m(e)) = m(id E (e)) = m(e), hence f m = id I :

I → I, = (id E , id C , id I ) = id S(C)
For the composition of morphisms, given

f = (f C , f E ) : C 1 → C 2 and g = (g C , g E ) : C 2 → C 3 , we write S(C i ) = (E i , C i , i , I i , m i )
and we compute:

S(g) • S(f ) = (g C , g E , g m ) • (f C , f E , f m ) = (g C • f C , g E • f E , g m • f m )
where, for all e ∈ E 1 , we compute:

(g m • f m )(m 1 (e)) = g m (f m (m 1 (e)) = g m (m 2 (f E (e))) (Since f m preserves identifiers) = m 3 (g E (f E (e)))
(Since g m preserves identifiers)

Hence we can conclude:

S(g) • S(f ) = S(g • f )
Remark 44. In D, every morphism f = (f E , f L , f C , f m ) from I 1 to I 2 is actually fully determined by f E whenever f L = id. Indeed, given f E : E 1 → E 2 , then we can define for all

x ∈ C 1 , f C (x) = {f E (e) | e ∈ x} and f m as f m (m 1 (e)) = m 2 (f E (e)
). We will often make the abuse of notation of writing f E for f and reciprocally.

Lemma 45. The product of I-structures is the product in D.

Proof. First note that I 1 × I 2 is an I-structure as it is a configuration structure endowed with an m function, where by definition every event in a configuration has a unique label. Secondly, it is easy to show that the projections γ i : I 1 × I 2 → I i are morphisms, since they are defined as the pair (π i , θ i ). Lastly to show that the structure I 1 × I 2 has the universal property, we proceed in two steps:

the underlying configuration structure is the product of the underlying configuration structures, by definition of the product in configuration structure:

F(I 1 × I 2 ) = F(I 1 ) × F(I 2 );
for any I which projects into I 1 and I 2 , then F(I ) projects into F(I 1 ) and F(I 2 ) and therefore there exists a unique morphism h : F(I ) → F(I 1 × I 2 ). It is easy to show that since the projections preserve identifiers, then so does h which concludes our proof. This lemma also follows from [START_REF] Winskel | Models for concurrency[END_REF]Proposition 85].

B Proofs and Auxiliary Lemmas

In this section we detail the proofs missing from the main text, as well as introducing some intermediate results that are necessary for the proofs.

B.1 Proof for Sect. 3.2

Theorem 22. On the class of processes without auto-concurrency, B&F bisim and SB&F bisim are the same relations.

Proof. Let R 1 , R 2 be two reversible processes without auto-concurrency. We want to show that 1. (R 1 , R 2 ) ∈ R for R a SB&F bisim implies that there exists f a bijection between I(R 1 )

and

I(R 2 ) such that (R 1 , R 2 , f ) ∈ R is a B&F bisim. 2. (R 1 , R 2 , f ) ∈ R for R a B&F bisim implies that (R 1 , R 2 ) ∈ R for R a SB&F bisim.
For 1, we first note that there exists forward-only traces from ∅ O R1 to R 1 [5, Lemma 10]. We pick one, θ 1 , and construct the bijection f between I(R 1 ) and I(R 2 ) using it. We start by letting

(∅ O R1 , ∅ O R2 , ∅) ∈ R . Then, assuming θ 1 starts with ∅ O R1 ---→ i:α R 1 , since (R 1 , R 2 )
∈ R, we know there are R 2 and j such that

∅ O R2 ---→ j:α R 2 and (R 1 , R 2 ) ∈ R,
and we let (R 1 , R 2 , {i → j}) ∈ R . We iterate this construction until we obtain the bijection

f such (R 1 , R 2 , f ) ∈ R .
That this bijection can be extended in case of forward transitions from R 1 or R 2 is obvious, using R. The more difficult part of the proof is to show that f is "right", i.e., that if R 1 or R 2 does a backward transition to a term S, and if S is paired with S in R, then it is the case that the identifiers of the transitions leading to S and S are "matched", i.e., in bijection in f . Stated formally, we want to show that for any (R 1 , R 2 ) ∈ R with f constructed as above, then for all R 1 ¬¬¬ → i:α S 1 and R 2 ¬¬¬ → j:α S 2 such that (S 1 , S 2 ) ∈ R, {i → j} ∈ f . We show it by contradiction: let us then take (R 1 , R 2 ) ∈ R and f : I(R 1 ) → I(R 2 ). We want to show that (R 1 , R 2 , f ) ∈ R is a valid relation, and for this we must show that it can accommodate the backward transitions. Suppose that we have two pairs of indexes {i → j}, {i → j } in f , and that R 1 ¬¬¬ → i :α S 1 and that R 2 ¬¬¬ → j:α S 2 such that (S 1 , S 2 ) ∈ R.

First, observe that all four indexes, i, i , j and j , are associated to the same label α: due to the way f was constructed, following R, it cannot be the case that two transitions with different labels have their identifiers paired. Secondly, since R 2 ¬¬¬ → j:α S 2 and {i → j} is in f , it must be the case that there is a transition in θ 1 with the identifier i by construction of f . Let us denote

t i : S 1 ---→ i:α R 1 and t i : S 1 ---→ i :α R 1 .
The following paragraphs are necessary for the proof but are more general and can also be read as standalone.

Interlude: Concurrency in a Trace and Trace Equivalence

Concurrency on events corresponds to a notion of concurrency on transitions in a trace. We introduce here the concepts needed for this proof, as they are defined in [START_REF] Danos | Reversible communicating systems[END_REF]Definition 7 and Lemma 8].

Two transitions

t 1 = R ----→ i1:α1 R 1 and t 2 = R ----→ i2:α2 R 2 are composable if R 1 = R ,
and doing t 1 , then t 2 is written as the composition t 1 ; t 2 . Given n composable transitions t i : R i ---→ i:αi R i+1 and their composition t 1 ; . . . ; t n , we say that t i is a direct cause of t k for 1 i < k n and write t i < t k (or, for short, i < k) if there is a memory stack m in R i+1 and a memory stack m in R k+1 such that m < m , where the order on memory stacks is given by prefix ordering.

Let R ---→ i:α S be a transition. If α = τ , we write m R/S = {m} where

R =(• • • ((R 3 | ((R 1 | (m P )) | R 2 )\ - → b 1 ) | R 4 )\ - → b 2 • • • | R n )\ -→ b m S =(• • • ((R 3 | ((R 1 | i, a, Q .m P ) | R 2 )\ - → b 1 ) | R 4 )\ - → b 2 • • • | R n )\ -→ b m
for some R i any of which could be missing and for some -→ b j , possibly missing as well. If α = τ , then m R/S will contain the pair of memory stacks that has been changed by the transition. Intuitively, the notation m R/S is useful below to extract the memory stack(s) modified by a forward transition from R to S.

Two transitions are coinitial if they have the same source process and cofinal if they have the same target process. We say that two coinitial transitions t 1 = R ----→ i1:α1 S 1 and

t 2 = R ----→ i2:α2 S 2 are concurrent if m R/S1 ∩ m R/S2 = ∅, that is, if the transitions modify disjoint memories in R.
The square lemma [5, Lemma 8] says that moreover, given two such concurrent transitions, there exists two cofinal and concurrent transitions

t 1 = S 1 ----→ i2:α2 S and t 2 = S 2 ----→ i1:α1 S.
The name of the lemma comes from this picture:

R S 1 S 2 S t 1 t 2 t 1 t 2
Moreover, the traces θ 1 = t 1 ; t 1 and θ 2 = t 2 ; t 2 are equivalent [START_REF] Danos | Reversible communicating systems[END_REF]Definition 9]. This allows one to define equivalence classes on transitions: t 1 in θ 1 is equivalent to t 2 in θ 2 if θ 1 is equivalent to θ 2 and t 1 and t 2 have the same index. Then in the trace t 1 ; t 1 we are now allowed to say that t 1 is concurrent to t 1 .

In a trace t 1 ; t 2 we have that t 1 is concurrent to t 2 iff t 1 is not a cause of t 2 . This follows from a case analysis using the definitions of concurrency and causality. Thanks to trace equivalence, we also have that in a trace t 1 ; . . . ; t n either t 1 is a cause of t n or the two transitions are concurrent. We refer the reader to [START_REF] Boudol | Permutation of transitions: An event structure semantics for CCS and SCCS[END_REF] for the complete treatment of concurrency and causality in the trace of a CCS process.

The definitions of concurrency for forward coinitial traces and of causality for forward traces can easily be "flipped" into definitions of concurrency for backward cofinal traces, and of causality for backward traces. Also, the concurrency and causality relations between transitions can be "lifted" to one between indexes in a trace. We will use them below.

Back to our Proof

Observe that i and i cannot be concurrent in θ 1 . If they were, then in the encoding of R 1 , there would be two events-the one introduced by t i and the one introduced by t j -that are concurrent, with the same label, but that is not possible since R 1 is without auto-concurrency. Since two transitions are either concurrent or causal, it follows that either i < i or i < i.

As the cause cannot backtrack before the effect it follows that the case i < i is not possible. Then i < i . We now reason by cases on j < j or j < j.

If j < j then R 1 must have already backtracked on j , which implies that the there is no j in f as we assumed.

The case j < j is not possible. Note that i < i implies an order in which the pair of indexes are added to the bijection, in this case the pair {i → j} occurs before {i → j } and therefore it cannot be that j < j.

From this reasoning, we get that for any R 1 ¬¬¬ → i:α S 1 and R 2 ¬¬¬ → j:α S 2 such that (S 1 , S 2 ) ∈ R, {i → j} ∈ f . We still need to show that (S 1 , S 2 , f \{i → j}) ∈ R is a "valid" relation. We only need to show that f \{i → j} matches the "right" indices in case of a backward transition, but we can simply iterate the previous reasoning until we reach (∅ O R1 , ∅ O R2 , ∅) ∈ R . This concludes this direction of the proof. For 2, there is nothing to prove, since we are dropping a requirement, the existence of the bijection.

B.2 Operations on Identified Configurations Preserve Them (Sect. 4.1)

Our main goal here is to prove that the operations of Definition 25 preserve I-structures (Lemma 48), and that requires the following intermediate lemma:

Lemma 46. For every reversible thread m P of a reachable process R, and for all i ∈ I(m), i occurs once in m.

Proof. We prove it by induction on the structure of m.

if m = ∅, then it is obvious. if m = .m , then by induction hypothesis, for all i ∈ I(m ), i occurs only once in m , and since no identifier occur in , i occurs only once in m. if m = j, λ, Q .m then there exists S such that m S ---→ j:λ j, λ, Q .m P since R is reachable. By induction we know that for all i ∈ I(m ), i occurs once in m . We reason on the derivation tree of the transition that add the memory event j, λ, Q and we have that for any such transition, the rule act. of Fig. 4 is applied as axiom at the top of the derivation tree. By the side condition of the rule act., we know that j / ∈ I(m ), hence that for all i ∈ I(m), i occurs once in m.

Remark 47. Note that the property above holds for reversible threads, and not for RCCS processes in general: we actually want memory events to sometimes share the same identifiers. Indeed, two memory events need to have the same identifiers if they result from a synchronization (i.e., the application of the syn. rule of Fig. 4) or a fork (i.e., the application of the Distribution of Memory rule of structural equivalence, Definition 13).

Lemma 48. The operations of Definition 25 (product, relabeling, restriction, parallel composition and postfixing) preserve I-structures.

Proof. Let us note that (i) the product, relabeling, restriction, and parallel composition on configuration structures from Definition 5 preserve configuration structures, as their are adaptations from [START_REF] Winskel | Event structure semantics for CCS and related languages[END_REF][START_REF] Winskel | Petri Nets: Central Models and Their Properties, Advances in Petri Nets[END_REF], and that (ii) any configuration structure endowed with a valid identifier function (i.e., such that no two events in the same configuration have the same identifier, cf. Collision Freeness) is a valid I-structure.

For the product, it follows trivially from Lemma 45. Relabeling does not change anything but the labels, so we have nothing to prove. The restriction only removes events in configurations and keeps the identifier function intact. Hence if the initial structure has a valid identifier function, then the identifier function of the new structure is a valid one by assumption.

Let us now consider the parallel composition of two I-structures, denoted E,C,L,,I,m). Proving that the identifier function m is valid follows from a case analysis. Given a configuration x ∈ C and two events e, e ∈ x, these are the possible cases: π 2 (e) = and π 2 (e ) = . In this case, looking at the definition of the product in I-structures, m(e) = (m 1 (π 1 (e)), m ) and m(e ) = (m 1 (π 1 (e )), m ). If m(e) = m(e ), then m 1 (π 1 (e)) = m 1 (π 1 (e )) in the configuration π 1 (x) in I 1 . But that's a contradiction, since π 1 (e) and π 1 (e ) are in the same configuration and the identifier function of I 1 is valid. π 1 (e) = and π 1 (e ) = . This case is similar as the previous one, except that it uses that the identifier function of I 2 is valid. π 1 (e) = and π 2 (e ) = (with either π 1 (e ) = or π 1 (e ) = ). If m(e) = m(e ), then m i (π i (e)) = m i (π i (e )) for i = 1, 2. Then in this case, either one of them, say, e, is a synchronization or a fork: in this case, m 1 (π 1 (e)) = m 2 (π 2 (e)) = m 2 (π 2 (e )), and e was relabeled ⊥ at the relabeling stage of the parallel composition, and then removed during the restriction. Hence a contradiction: e and e cannot be two events in the same configuration. or none of them is a synchronization, in which case both events were removed by the restriction. Hence, again, a contradiction: e and e cannot be two events in the same configuration. The symmetric case (where π 2 (e) = and π 1 (e ) = ) is similar.

I 1 | I 2 = (
For the postfixing operation, we have to first prove that the underlying configuration of I 1 • i, λ, P , written (E, C, L, ), is a valid configuration structure. Finiteness is satisfied because the underlying configuration of I 1 , written (E 1 , C 1 , L 1 , 1 ), is a configuration structure, and every configuration in {x ∪ {e} | x ∈ C 1 is maximal} is finite. For Coincidence Freeness, we also only have to check the configurations in {x ∪ {e} | x ∈ C 1 is maximal}. Given y ∈ {x ∪ {e} | x ∈ C 1 is maximal}, there exists y such that y = y ∪ {e}. Given two events e 1 , e 2 in y such that e 1 = e 2 , if e 1 = e or e 2 = e, then y is the configuration we are looking for. Otherwise, it follows from y being a configuration in the configuration structure (E 1 , C 1 , L 1 , 1 ). Finite Completeness and Stability trivially follow from the fact that (E 1 , C 1 , L 1 , 1 ) is a configuration structure. Hence, I 1 • i, λ, P has a configuration structure underlying, and we just need to prove that the identifier function is valid. That follows from the fact that i is not an identifier in the codomain of m i , and hence I 1 • i, λ, P is an I-structure.

B.3 Properties of Memory Encodings (Sect. 4.2)

Remember that we assume given coherent reversible processes R, R 1 , R 2 and S (without any restriction), and that we write O R for the origin of R, and R as (E R , C R , R , I R , m R ) and similarly for S. Proof. We proceed by induction on R.

If R is m P , we prove that m P is a poset with one maximal element by induction on m. The base case, if m is ∅, is trivial, since ∅ = 0 is a poset with one maximal element, ∅. If m is .m , then it follows by induction hypothesis, since .m = m . If m is i, α, P .m , then by induction hypothesis, m is a poset with one maximal element, and the postfixing construction used to define i, α, P .m , detailed in Definition 25, preserves that property.

If R is R \a, then it trivially follows by induction hypothesis.

Finally, if R is R 1 | R 2 ,
then by induction hypothesis we get that R 1 and R 2 are both posets with a maximal configuration. We also know by Lemma 30 that events in each structure have disjoint identifiers (however the two structures can share identifiers with each other). Looking at the definition of parallel composition for I-structures (Definition 25), we may

observe that R = R 1 | R 2 = R 1 | R 2 consists of the structure r • ( R 1 × R 2 ) F with a different m function.
We show that there exists more than one maximal configurations in R 1 × R 2 and that all but one are removed by the restriction.

We show this by first showing that there exists more than one maximal configurations in F( R 1 ) × F( R 2 ), denoted here with C. From the definition of product (Definition 5), we have that there exists y 1 , . . . , y n maximal configurations in C such that π 1 (y i ) and π 2 (y i ) are maximal in C 1 and C 2 , respectively. As

R 1 × R 2 = (F( R 1 ) × F( R 2 )) ⊕ m it follows that the maximal configurations of C are preserved in R 1 × R 2 .
A second step is then to show that the restriction keeps only one maximal configuration. Let y i , y j be two maximal configurations. As they are maximal it implies that y i ∪ y j / ∈ C, for i = j n. In turn, this implies that there exists e i ∈ y i and e j ∈ y j such that π 1 (e i ) = π 1 (e j ) and e i = e j , as otherwise y i ∪ y j would be defined. Here we assume that π 1 (e i ) = π 1 (e j ) but we could also take π 2 (e i ) = π 2 (e j ) and the argument still holds.

Let us now take d an event in C 1 and take e 1 , . . . , e m the subset of events in E where π 1 (e i ) = d. The restriction in the parallel composition of R 1 | R 2 keeps only one such event e i and removes the rest. Therefore, from all maximal configurations y 1 , . . . , y m such that e i ∈ y i , i m, only one remains.

By applying the argument above to all events in R 1 (and R 2 ), we have that the restriction removes all but one y i , which is then the maximal configuration in R 1 | R 2 .

B.4 Lemmas and Proofs for Sect. 4.3 and Sect. 5

Our goal here is to prove Theorems 36 and 37, and we use the following organization: first (Sect. B.4.1), we show that there is an operational correspondence between R and R (Lemma 34), and this requires intermediate lemmas (Lemmas 49, 50, 51) about the encoding of memories and their relation to maximal events. Then (Sect. B.4.2), we use this result to identify isomorphisms of I-structures with label-and order-preserving functions (Lemma 35), and to connect our previous formalism with the encoding of memories (Lemma 39). Finally, Sect. B.4.3 concludes by proving our two main theorems.

B.4.1 Operational Correspondence

Lemma 49. If R ≡ S then R ∼ = S .
Proof. Looking back at Definition 13, there are only limited ways for R and S to be structurally equivalent (i.e., in the ≡ relation), and we review them one by one.

In Sum Symmetry, Sum Associativity and α-Conversion, it should be noted that the memory is left untouched, so their encodings are equal.

For For Scope of Restriction, we have that have m (P \a) = m = (m P )\a .

Lemma 50. The event introduced in the postfixing of a memory event to an identified structure is maximal in the resulting identified structure.

Proof. The proof is immediate: the event introduced occurs only in the maximal configurations of the identified structure, and hence there cannot be any other event that causes it.

Furthermore, the maximality of an event can be "preserved" by parallel composition: Lemma 51. For all identified structure

I 1 = (E 1 , C 1 , L 1 , 1 , I 1 , m 1
) with e 1 ∈ E 1 a maximal event in it, and for all identified configuration

I 2 = (E 2 , C 2 , L 2 , 2 , I 2 , m 2 ) such that m 1 (e 1 ) / ∈ I 2 , (e 1 , ) is maximal in I 1 | I 2 .
Proof. The definition of parallel composition of identified configuration structure (Definition 25) should make it clear that the only event in I 1 | I 2 whose first projection is e 1 is (e 1 , ), since m 1 (e 1 ) / ∈ I 2 : all the other pairings of events from E 2 with e 1 resulting in Err. 1. Now, suppose for the sake of contradiction that (e 1 , ) is not maximal in I 1 | I 2 . It means that there is a maximal configuration x in I 1 | I 2 and an event e ∈ x such that (e 1 , ) < x e.

By Definition 5, π 1 (x) ∈ C 1 , and we prove that π 1 (x) is maximal in C 1 by contradiction. Suppose π 1 (x) is not maximal in C 1 , then there exists z ∈ C 1 such that π 1 (x) z. Assume z is maximal in C 1 (if it is not, then take z the maximal configuration such that z ⊆ z , which always exists, and note that e 1 ∈ z, since e 1 ∈ π 1 (x) and π 1 (x) ⊂ z. By Stability, since z ∪ π 1 (x) = z is a configuration in C 1 , z ∩ π 1 (x) = z \ π 1 (x) also is, and note that for all events e in z \ π 1 (x), we have that e 1 z\π1(x) e . Since e ∈ z \ π 1 (x), e ∈ z and e 1 z e , we have that z is a maximal configuration in I 1 where e 1 is not maximal: a contradiction. Hence, we know that π 1 (x) is maximal in C 1 . Now, we prove that π 1 (e) = . For the sake of contradiction, suppose that π 1 (e) = . Then, observe that the underlying configuration structure F(I 1 | I 2 ) also have this configuration x with (e 1 , ) < x e. Without loss of generality, we can assume that e is a an immediate cause of (e 1 , ) [1, Definition 20], that is, that there is no e in x such that (e 1 , ) < x e < x e. We can now use [START_REF] Aubert | Contextual equivalences in configuration structures and reversibility[END_REF]Proposition 3] to get that it must be the case that either π 1 (e 1 , ) < π1(x) π 1 (e) or π 2 (e 1 , ) < π2(x) π 2 (e). But since π 2 (e 1 , ) = / ∈ π 2 (x), and since we assumed π 1 (e) = / ∈ π 1 (x), both scenario are impossible, so we reached a contradiction, and it must be the case that π 1 (e) = .

Since π 1 (x) is maximal in C 1 , and since π 1 (e), e 1 ∈ π 1 (x), we reached a contradiction: π 1 (e) is not caused by e 1 , but that cannot be since e 1 is not maximal. Hence, there is no such e ∈ x, and (e 1 , ) is maximal in

I 1 | I 2 .
Lemma 34. 1. For all transitions R ---→ i:α S, R ∼ = S {e} with e maximal in S and m S (e) = i.

For all transitions R ¬¬¬ →

i:α S, S ∼ = R {e} with e maximal in R and m R (e) = i.

3.

For any maximal event e in R , there is a transition R ¬¬¬¬¬¬¬¬ → m R (e): R (e) S with S ∼ = R {e} .

Proof. We prove the three items separately.

item 1

We proceed by case on α in the transition R ---→ i:α S:

If α = a For the transition R ---→ i:α S to take place, it must be the case that R contains a thread T = m a.P + Q for some m, P and Q, and that T ---→ i:α i, a, Q .m P . Additionally, the par., res. and ≡ rules of Fig. 4, gives us that it must be the case that

R ≡ ((R n-1 • • • ((R 3 | ((R 1 | T ) | R 2 )\ - → b 1 ) | R 4 )\ - → b 2 • • • ) | R n )\ -→ b m
for some R i any of which (and its corresponding | constructor) could be missing and for some -→ b j , any of which (along with their \ constructor) could be missing as well. Hence, the transition can be written as

R ---→ i:a ((R n-1 • • • ((R 3 | ((R 1 | i, a, Q .m P ) | R 2 )\ - → b 1 ) | R 4 )\ - → b 2 • • • ) | R n )\ -→ b m

=S

with S ≡ S. By Lemma 50, we know that there is a maximal event e 1 in i, a, Q .m P that has for identifier i. We show that this event can be "traced through" S , using four arguments: From the par. rule in Fig. 4 we have that i / ∈ I(R 1 ). Using Lemma 51, it follows that there exists a maximal event e 2 in R 1 | i, a, Q .m P such that π 2 (e 2 ) = e 1 , and from Definition 25 that its identifier is i. We can use the same reasoning to prove that there is a maximal event e 3 in (R 1 | i, a, Q .m P ) | R 2 such that π 1 (e 3 ) = e 2 and such that its identifier is i.

Since R 3 | ((R 1 | i, a, Q .m P ) | R 2 )\ - → b 1 = R 3 | ((R 1 | i, a, Q .m P ) | R 2 )
, it is trivial that e 3 is a maximal event with identifier i in it. Using those three arguments repeatedly, and "skipping" them if a parallel composition or a restriction is "missing", we can "trace" the maximal event with identifier i in

((R n-1 • • • ((R 3 | ((R 1 | i, a, Q .m P ) | R 2 )\ - → b 1 ) | R 4 )\ - → b 2 • • • ) | R n )\ -→ b m
. But we still need to find a maximal event whose identifier is i in S . Since

((R n-1 • • • ((R 3 | ((R 1 | i, a, Q .m P ) | R 2 )\ - → b 1 ) | R 4 )\ - → b 2 • • • ) | R n )\ -→ b m ≡ S Lemma 49 gives us that ((R n-1 • • • ((R 3 | ((R 1 | i, a, Q .m P ) | R 2 )\ - → b 1 ) | R 4 )\ - → b 2 • • • ) | R n )\ -→ b m ∼ = S .
Let us write f this isomorphism, we want to prove that f (e) is maximal in S . To do so, let us use the "if" part of the upcoming Lemma 35 (this part of the lemma is not proved using the lemma we are currently proving, but the "and only if" part does, hence the choice of postponing it after this current lemma) and suppose that f (e) is not maximal in S . Then, there exists a maximal configuration x m in S and an event e in x m such that f (e) < xm e . But since f is an isomorphism, and since f preserves the order in maximal configurations according to the first part of Lemma 35, we have that it must be the case that e < f -1 (xm) f -1 (e ), which contradicts the maximality of e in ((R n-1

• • • ((R 3 | ((R 1 | i, a, Q .m P ) | R 2 )\ - → b 1 ) | R 4 )\ - → b 2 • • • ) | R n )\ -→ b m .
Since f is by definition label-preserving, we have that f (e) is a maximal event in S such that m S (e) = i. It is obvious that this event is the only one that was added to the encoding of R, so that R = S {e} . If α = τ Then it must be the case that R has two threads, T = m a.P + Q and T = m ā.P + Q for some m, m , a, P, P and Q, Q , and that

R = (• • • (R 3 | (((R 1 | T ) | R 2 )\ - → b 1 | R 4 ))\ - → b 2 • • • | ((R 1 | T ) | R 2 )\ - → c 1 • • • | R n )\ -→ b m
for some R i , R i any of which (and its corresponding | constructor) could be missing and for some -→ b j , -→ c k , any of which (along with their \ constructor) could be missing as well. Then the transition becomes

R ---→ i:τ (• • • ((R 3 | (R 1 | ( i, a, Q .m P ) | R 2 ))\ - → b 1 | R 4 )\ - → b 2 • • • (R 1 | (( i, ā, Q .m P ) | R 2 )\ - → c 1 • • • | R n )\ -→ b m = S.
We use the same reasoning as in the first case above to deduce that there is a maximal event in ( i, a, Q .m P , let us name it e 1 , and one in i, ā, Q .m P , let us name it e 1 , that both have identifier i. Using the same argument as the first case of the proof, we can "trace" in parallel e 1 and e 1 , until the I-structures that hold their "descendants" are put in parallel: at that point, by Definition 25, it should be clear that a single maximal event resulting from their composition will emerge, that it will be labeled τ and have identifier i. Finally, using again the same argument as in the first case, this event resulting from the synchronization of our two maximal events will still be maximal in S , and hence we can conclude that there exists a maximal event in S labeled τ whose identifier is i.

item 3

For any reachable process R, from Definition 15 and [5, Lemma 10], we have that there exists a forward-only trace O R --→ → R. We consider without loss of generality the following trace:

∅ O R = R 0 ----→ 1:α1 R 1 • • • ----→ k:α k R k = R,
for some k, α 1 , . . . , α k .

Given two processes S 1 , S 2 such that S 1 = S 2 {e} for some event e, we write for simplicity that S 2 = S 1 + e. Using item 1, we have then that R j = R j-1 + e j , for j k and m(e j ) = j. Therefore we can construct a bijection h between events e j in R and transitions t j : R j-1 ----→ j:αj R j with m(e j ) = j.

Let e be a maximal event in R and let h(e) = R j-1 ----→ j:αj R j , where

R 0 ----→ 1:α1 R 1 • • • R j-1 ----→ j:αj R j -------→ j+1:αj+1 R j+1 • • • R k-1 ----→ k:α k R k = R
As e is maximal, by Definition 33, there exists no event e in R such that e < e . From R i+1 = R i + e i+1 , for i k, we have that R i ⊆ R i+1 and by induction, R i ⊆ R k , for all i k. Then R j+i ⊆ R k and we have that e i e, for all j + 1 i k. It implies that e i is concurrent with e, for all j + 1 i k.

We use here concurrency in a trace and trace equivalence, that have been introduced in the proof of Theorem 22. Consider two consecutive transitions t j = R j -------→ j+1:αj+1 R j+1 and t j+1 = R j+1 -------→ j+2:αj+2 R j+2 . Using the bijection h defined above between transitions and events, we have that there exists two event e j , e j+1 in R j+2 such that h(e j ) = t j and h(e j+1 ) = t j+1 . Suppose that e j is concurrent to e j+1 . By an induction on the structure of memories in R j+2 , we have that m Rj /Rj+1 ∩ m Rj+1/Rj+2 = ∅ which implies that there exists a transition t j = R j -------→ j+2:αj+2 R j+2 such that t j is concurrent with t j .

Recall that e i is concurrent with e, for all j + 1 i k in our trace. We can now use the trace equivalence of [START_REF] Danos | Reversible communicating systems[END_REF]Definition 9], and use the previous remark repeatedly to re-organize

Definition 2 (Figure 2

 22 Figure 2 Examples of configuration structures encoding CCS processes

Definition 7 (

 7 Constraints on configuration structures). If ∀x ∈ C, ∀e 1 , e 2 ∈ x, (e 1 ) = (e 2 ) implies e 1 = e 2 , then C is non-repeating [10, Definition 3.5]. ∀e 1 , e 2 ∈ x, e 1 co x e 2 and (e 1 ) = (e 2 ) implies e 1 = e 2 , then C is without autoconcurrency [16, Definition 9.5]. ∀e, e / ∈ x, x --→ e y, x --→ e y , (e) = (e ) and C \ y ∼ = C \ y implies e = e , where

Figure 3 (

 3 Figure 3 (Identified) Configurations structures of Examples 9 and 28.

9 .

 9 In addition to the examples of Fig. 2, the encoding of the processes a.b, c.a, and their parallel composition (a.b) | (c.a), as well as a.b | c, are given in Fig.

Figure 4

 4 Figure 4 Rules of the labeled transition system

Figure 6

 6 Figure 6 Syntactical characterizations of HHPB

  endowed with a set of identifiers I and a function m : E → I such that ∀x ∈ C, ∀e 1 , e 2 ∈ x, m(e 1 ) = m(e 2 ). (Collision Freeness) We call C the underlying configuration structure of I, write F(I) = C, I = C ⊕ m, (I being the domain of m), and write 0 for the identified configuration structure with E = ∅.

Lemma 30 .

 30 For all e 1 , e 2 ∈ E R , m R (e 1 ) = m R (e 2 ) implies e 1 = e 2 .Proof. We proceed by structural induction on R. From Lemma 46 the only interesting case is the parallel composition, i.e. R = R 1 | R 2 . From the definition of parallel composition in I-structures (Definition 25), it follows that m R (e 1 ) = m R (e 2 ) implies e 1 = e 2 .Lemma 31. R is a partially ordered set (poset) with one maximal configuration.

  Distribution of Memory, we have that m (P | Q) = m , and ( .m P ) | ( .m Q) = ( .m P ) | ( .m Q) = .m | .m = m | m . The construction of the isomorphism between m and m | m is trivial: let e be an event in m . Note that the only event e in m | m such that π 1 (e ) = e is (e, e). Indeed, suppose (e, e ) is in m | m , for e = e. Then, by Lemma 30, m(e) = m(e ), since they are both events in m . But by the definition of parallel composition, (e, e ) should have triggered Err. 1. Similarly, (e, ) can not be an event in m | m , since it should have triggered Err. 2. Hence, we can map e in m and (e, e) in m | m and obtain our isomorphism.

item 2 If

 2 R ¬¬¬ → i:α S, then by the Loop Lemma [5, Lemma 6], S ---→ i:α R. By item 1, we have that S ∼ = R {e} with e maximal in R and m R (e) = i, which is what we wanted to show.

For the reader familiar with event structures, a configuration x defines an event structure (x, x, ). The construction here mirrors the transformation from an event structure to a configuration structure[START_REF] Winskel | Models for concurrency[END_REF].

our original trace as follows:

The core idea being that we can "postpone" the transition that will create the event e in the encoding of R, by flipping it with the other transitions, and have it become the last transition that leads to the same R.

We can use now the Loop Lemma [5, Lemma 6], and have that R ¬¬¬¬ → j:αj R k . Using item 2 on this transition, we have that R k = R {e} .

B.4.2 On Connecting Formalisms

Lemma 35. Letting x m 1 and x m 2 be the unique maximal configuration in R 1 and R 2 , R 1 ∼ = R 2 iff there exists a label-and order-preserving bijection between x m 1 and x m 2 .

Proof. Let f : R 1 → R 2 be an isomorphism: using Remark 44, we will take f to be fully determined by its function between events f E , that we also write f . Then f : x m 1 → x m 2 is by definition a label-preserving bijection. For two events e, e in R 1 , if e < x m 1 e it follows that for all x 1 in R 1 such that e ∈ x 1 then e ∈ x 1 . From f an isomorphism we have that f -1 : R 2 → R 1 is a well defined morphism. As f -1 preserves configurations it follows that for all x 2 in R 2 , there exists x 1 in R 1 such that f (x 1 ) = x 2 . Then for all x 2 , such that f (e ) ∈ x 2 it implies that e ∈ f -1 (x 2 ) and e ∈ f -1 (x 2 ) and finally, f (e) ∈ x 2 . Then f (e) < x m 2 f (e ), as for all x 2 , x 2 ⊆ x m 2 . Similarly we proceed for the concurrent events, and obtain that f is an order-preserving bijection on top of being label-preserving.

For the reverse direction, let f : x m 1 → x m 2 be a label-and order-preserving bijection. All events in R 1 are present in x m 1 , and therefore f : R 1 → R 2 is a bijection on events. Remains to show that f preserves configurations, that is, for all

In other words, f (x 1 ) = x 2 must satisfies the properties of Definition 1.

Finiteness follows from the fact that all configurations in the encoding of an RCCS memory are finite.

For Coincidence Freeness let us first note that there is a unique and finite maximal configuration x m 2 in which all distinct events are either causal or concurrent. Let us consider e 2 = e 2 two events in x 2 . Since e 2 = e 2 then either (i)e 2 x m 2 e 2 (or e 2 x m 2 e 2 but this is similar) or (ii)e 2 co x m 2 e 2 . As x m 2 is the unique maximal configuration, the relations above hold for x 2 as well. In the case (i), as e 2 = e 2 then e 2 x2 e 2 . We apply the definition of causality (Definition 2) to obtain the configuration z ⊆ x 2 where e 2 ∈ z and e 2 / ∈ z as required by Coincidence Freeness. In the case (ii), we use the definition of concurrency, which implies that e 2 x2 e 2 and e 2 x2 e 2 . Then there exists z ⊆ x 2 such that e 2 ∈ z and e 2 / ∈ z and moreover, there exists z ⊆ x 2 such that e 2 ∈ z and e 2 / ∈ z. To show Finite Completeness, it suffices to note that there exists a unique maximal configuration x m 2 which can be an upper bound for any subset of configurations in R 2 . To show Stability we first note that because there is a single maximal configuration, the condition ∀x 2 , x 2 ∈ C 2 , x 2 ∪ x 2 ∈ C 2 always holds. Then we have to show that for all configurations x 2 , x 2 , x 2 ∩ x 2 is a configuration. We will show that x 2 ∩ x 2 = f (x 1 ∩ x 1 ) is a configuration in R 2 by exploiting the causality and concurrency relations in x 1 ∩ x 1 . From the second item of Lemma 34 we have that there exists a maximal event e 1 1 in x 1 and from S {e 1 1 } ⊂ R , x 1 \ e 1 is a configuration in R 1 . We use the same reasoning for x 1 \ e 1 in S {e 1 1 } with e 2 1 maximal and S {e 1

1 ,e 2 1 } ⊂ S {e 1 1 } ⊂ R . We have then a sequence of events e 1 1 ,

Let us consider e 2 = e 2 two events in x 2 and as f is a bijection, let e 1 = e 1 be two events in f -1 (x 2 ) = x 1 such that f -1 (e 2 ) = e 1 and f -1 (e 2 ) = e 1 . If e 2 = e 2 then either e 2 x m 2 e 2 or e 2 co x m 2 e 2 . It follows that either e 1 x m 1 e 1 or e 1 co x m 1 e 1 , respectively, since f -1 is label-and order-preserving as well. As x m 1 , x m 2 are the unique maximal configurations the relations above hold for x 2 and x 1 as well. We therefore have that f (e 1 1 ) is the maximal event in x 2 . Again we use the second item of Lemma 34 and as above we obtain the sequence of events f (e 1 1 ),

Lemma 39. The underlying configuration structure of R is isomorphic to x R ↓.

Proof. Let us abuse the notation by writing

This encoding is based on the following result : as R is reachable there exists a forwardonly trace [5, Lemma 10]

αn R, such that for any transition in θ there exists a corresponding event in x [1, Lemma 1].

We reason then by induction on the trace θ. As the base case is similar, we only treat the inductive case.

Suppose that the result holds for R, that is let h : F( R ) → x R ↓ be an isomorphism. Remember that F is the identity on events. We use an argument similar to Lemma 35 to show that instead of an isomorphism, we can reason on h : x m → x R as a label-and orderpreserving bijection, where x m is the maximal configuration of R . Indeed, from Definition 3, x R is the maximal configuration in x R ↓ and we can easily derive an identified structure S(x R ↓) (Lemma 43).

Let R ---→ i:α S be an RCCS transition. Then by the operational correspondence between R and ( O R , x) [1, Lemma 6] there exists e an event in O R such that

with (e) = α and S = ( O R , x R ∪ {e}). By the operational correspondence between R and R (Lemma 34) there exists a memory event e such that R = S {e } with e maximal in S and m S (e ) = i. As there is only one maximal configuration in S and as R = S {e } , it follows that x m ∪ {e } is the maximal configuration in S .

We have then to show that if h : x m → x R is label-and order-preserving bijection then so is h = h ∪ {e → e } : x m ∪ {e } → x R ∪ e. We do this by exploiting the correspondence with RCCS and following a reasoning similar to the one in Theorem 37.

B.4.3 Proofs of Theorems 36 and 37

Theorem 36. P 1 and P 2 are HHPB (resp. HPB) iff P 1 and P 2 are.

Proof. Let us prove the HHPB case, the other case being similar, and actually simpler. ⇒ Let R RCCS be a HHPB between P 1 and P 2 (Definition 32). We show that the following relation

is a HHPB between P 1 and P 2 . We first show that for any tuple (x 1 , x 2 , f ) ∈ R, f : x 1 → x 2 is a label-and orderpreserving bijection. For a tuple (R

History-Preserving Bisimulations on RCCS isomorphism, we have that F : x m 1 → x m 2 , the isomorphism restricted to the maximal configurations x m 1 , x m 2 , with F a label-and order-preserving bijection, by Lemma 35. The functor F maps isomorphisms on identified structures to isomorphisms on configuration structures, by Lemma 43, and therefore f = F(F ) : F(x m 1 ) → F(x m 2 ). Moreover, x 1 and x 2 are the maximal configurations in x 1 ↓ and x 2 ↓, by Definition 3. By Lemma 39, F( R i ) ∼ = x i ↓ which implies that F(x m i ) = x i , for i ∈ {1, 2}. Thus f = F(F ) is well defined and indeed, a label-and order-preserving bijection. The rest of the proof follows the same structure as in [1, Proposition 6]. Note that (∅, ∅, ∅) ∈ R: indeed (∅ P 1 , ∅ P 2 , ∅) ∈ R RCCS and ∅ P i = ( P i , ∅), for i ∈ {1, 2}. Let us suppose that (x 1 , x 2 , f ) ∈ R for R i = ( P i , x i ), for i ∈ {1, 2} and f : x 1 → x 2 a label-and order-preserving bijection. Note that F( R i ) ∼ = x i ↓, from Lemma 39, and that R i ∼ = x i ↓ ⊕m, for some function m, from Definition 24. To show that R is a HHPB we have to show that if x 1 --→ e1 y 1 (or x 1 ¬¬ → e1 y 1 ) then there exists y 2 such that x 2 --→ e1 y 2 (or x 2 ¬¬ → e2 y 2 respectively) and such that (y

Let x 1 --→ e1 y 1 , hence by definition, y 1 = x 1 ∪ {e 1 }. From the correspondence between RCCS and their encodings (from [1, Lemma 6]), it follows that R 1 ---→ i:α S 1 such that

, it follows that there exists a transition

Again from the correspondence between R 2 and R 2 we have that x 2 --→ e2 y 2 such that

Note that, again using Lemma 35, we can consider F : x m 1 → x m 2 and F : y m 1 → y m 2 to be label-and order-preserving bijections on the maximal configurations of R 1 , R 2 and S 1 , S 2 , respectively. From the definition of postfixing and parallel composition, in Definition 25, we have that

} by which we conclude. We treat similarly the cases where x 2 does a transition, or when the transitions are backwards. ⇐ Let R CONF be a HHPB between P 1 and P 2 . We show that the following relation

x 2 a label-and order-preserving bijection, and for two functions m 1 :

then there exists a unique function f m :

, for all e ∈ x 1 . This follows from Collision Freeness in the definition of identified structures and from f being a bijection. We write then

. Moreover, as in the first case, we derive that x 1 , x 2 are maximal in R 1 , R 2 , respectively. We use Lemma 35 to conclude that

order-preserving.

To show that R is a HHPB we have to show that if R 1 ---→ i:α S 1 (or R 1 ¬¬¬ → i:α S 1 ) then there exists S 2 such that R 2 ---→ j:α S 2 (or R 2 ¬¬¬ → j:α S 2 respectively) and such that (S 1 , S 2 , F ) ∈ R for some F . Let R 1 ---→ i:α S 1 . We use again the correspondence between RCCS and their encodings [1, Lemma 6] from which we have that there exists e 1 and y 1 = x 1 ∪ {e 1 } such that x 1 --→ e1 y 1

and S 1 = ( P 1 , y 1 ). As (x 1 , x 2 , f ) ∈ R CONF it implies that there exists e 2 , y 2 and

Again, from the correspondence between RCCS and configuration structures we have that, from x 2 --→ e2 y 2 , there exists S 2 such that R 2 ---→ j:α S 2 with S 2 = ( P 2 , y 2 ). From

We conclude therefore that (S 1 , S 2 , F ) ∈ R.

Similarly we show the cases where R 1 does a backward transition, or if R 2 does a forward or backward transition.

Theorem 37. HHPB and B&F bisim coincide on all CCS processes.

Proof.

Let P 1 , P 2 be two processes and let R be a B&F bisim relation between them as in Definition 20. Then for any (R 1 , R 2 , f ) ∈ R, R 1 , R 2 are two RCCS processes and f : I(R 1 ) → I(R 2 ) is a bijection on their identifiers. Letting R i = (E i , C i , L i , i , I i , m i ), for i ∈ {1, 2}, we show that the relation

is a HHPB relation as in Definition 32. We do this by induction on the processes R 1 and R 2 , as any process reachable from P 1 has to be in R (and in S) and vice versa. Remember Remark 44: to define F : R 1 → R 2 = (f E , f C , f m ), it is enough to define f E , and we write F for f E in the following. The base case (∅ P 1 , ∅ P 2 , ∅) ∈ S is trivial. Suppose that for (R 1 , R 2 , f ) ∈ R, we have that (R 1 , R 2 , F ) ∈ S. Now let R 1 ---→ i:α S 1

for which we have that R 2 ---→ j:α S 2 and g : I(S 1 ) → I(S 2 ) is a bijection defined as f on I(R 1 ) ⊂ I(S 1 ) and g(i) = j. Let e 1 ∈ S 1 such that m 1 (e 1 ) = i and e 2 ∈ S 2 such that m 2 (e 2 ) = j. Then G = F ∪ {e 1 → e 2 } is defined by g(m 1 (e 1 )) = m 2 (e 2 ), and thus (S 1 , S 2 , G) ∈ S.

We show now that G is an isomorphism between S 1 and S 2 . G preserves identifiers by definition; it preserves labels as 1 (e 1 ) = 2 (e 2 ) = α. Lastly we have to show that it preserves configurations. We can use Lemma 35 to show instead that G :

is a label-and order-preserving function, where x m 1 , x m 2 are the maximal configurations in S 1 and S 2 , respectively. Also by Lemma 35 we have that F : y m 1 → y m 2 is a label-and order-preserving function on y m 1 , y m 2 maximal configurations in R 1 and R 2 , respectively. From Lemma 34, x m 1 \ {e 1 } ∈ R 1 and using Lemma 31 we have that

2 is a label-and order-preserving function on all events e = e 1 . Let us suppose, by contradiction, that there exists e such that e 1 co x m 1 e but that e 2 co x m 2 F (e) does not hold. Take the maximal event e with such a property. Moreover, let F (e) = e < x m 2 e 2 without loss of generality. There exists at least one sequence of events e 1 ≤ • • • e n such that e x m 1 e 1 and such that e n is maximal. For simplicity we suppose that there is only one such sequence (the general case uses the same reasoning). From Lemma 34, we have that S 1 ¬¬¬¬¬¬¬¬ → m(e n ): (e n ) S 1 .

We have F (e) < F (e 1 ) < • • • < F (e n ) and F (e n ) maximal, since F is label-and orderpreserving on all these events. As (S 1 , S 2 , g) ∈ R, we have also (S 1 , S 2 , g ) ∈ R, where g is defined as g. We apply this reasoning until we reach the process T 1 where e is maximal. Then there exists T 2 such that (T 1 , T 2 , g ) and g is defined as g on the identifiers i, j and m(e).

Then e is maximal however e is not and we reach a contradiction: from Lemma 34 S 1 ¬¬¬¬¬¬¬ → m(e): (e) S 1 but S 2 cannot backtrack on e . It implies then that G : x m 1 → x m 2 is a label-and order-preserving function on all events in x m 1 . Let P 1 , P 2 be two processes and let R be a HHPB relation between them as defined in Definition 32. Then for any R 1 , R 2 two RCCS processes and f : R 1 → R 2 an isomorphism such that (R 1 , R 2 , f ) ∈ R, f is also a bijection on the event identifiers of the memories of R 1 , R 2 . The relation