On the Weak Continuation of Reverse Bisimilarity vs. Forward Bisimilarity

Abstract

We introduce a process calculus for nondeterministic systems that are reversible, i.e., capable of undoing their actions starting from the last performed one. The considered systems are sequential so as to be neutral with respect to interleaving semantics vs. truly concurrent semantics of parallel composition. As a natural continuation of previous work on strong bisimilarity in this reversible setting, we investigate compositionality properties and equational characterizations of weak variants of forward-reverse bisimilarity as well as of its two components, i.e., weak forward bisimilarity and weak reverse bisimilarity.

1. Introduction

Reversibility in computing started to gain attention since the seminal works of Landauer [ 1 ] and Bennett [ 2 ], where it was shown that reversible computations may achieve lower levels of heat dissipation. Nowadays reversible computing has many applications ranging from computational biochemistry and parallel discrete-event simulation to robotics, control theory, fault tolerant systems, and concurrent program debugging.

In a reversible system, two directions of computation can be observed: a forward one, coinciding with the normal way of computing, and a backward one, along which the efects of the forward one can be undone when needed in a causally consistent way, i.e., by returning to a past consistent state. The latter task is not easy to accomplish in a concurrent system, because the undo procedure necessarily starts from the last performed action and this may not be uniquely identifiable. The usually adopted strategy is that an action can be undone provided that all of its consequences, if any, have been undone beforehand [ 3 ].

In the process algebra literature, two approaches have been developed to reverse computations based on keeping track of past actions: the dynamic one of [ 3 ] and the static one of [ 4 ], later shown to be equivalent in terms of labeled transition systems isomorphism [ 5 ].

The former approach yields RCCS, a variant of CCS [ 6 ] that uses stack-based memories attached to processes so as to record all the actions executed by the processes themselves. A single transition relation is defined, while actions are divided into forward and backward resulting in forward and backward transitions. This approach is suitable when the operational semantics is given in terms of reduction semantics, like in the case of very expressive calculi as well as programming languages.

In contrast, the latter approach proposes a general method, of which CCSK is a result, to reverse calculi, relying on the idea of retaining within the process syntax all executed actions, which are suitably decorated, and all dynamic operators, which are thus made static. A forward transition relation and a backward transition relation are separately defined, which are labeled with actions extended with communication keys so as to remember who synchronized with whom when going backward. This approach is very handy when it comes to deal with labeled transition systems and basic process calculi.

In [ 4 ] forward-reverse bisimilarity was introduced too. Unlike standard bisimilarity [ 7, 6 ], it is truly concurrent as it does not satisfy the expansion law of parallel composition into a choice among all possible action sequencings. The interleaving view can be restored in a reversible setting by employing back-and-forth bisimilarity [ 8 ]. This is defined on computation paths instead of states, thus preserving not only causality but also history as backward moves are constrained to take place along the path followed when going forward even in the presence of concurrency. In the latter setting, a single transition relation is considered, which is viewed as bidirectional, and in the bisimulation game the distinction between going forward or backward is made by matching outgoing or incoming transitions of the considered processes, respectively.

In [ 9 ] forward-reverse bisimilarity and its two components, i.e., forward bisimilarity and reverse bisimilarity, have been investigated in terms of compositionality properties and equational characterizations, both for nondeterministic processes and for Markovian processes. In order to remain neutral with respect to interleaving view vs. true concurrency, the study has been conducted over a sequential processes calculus, in which parallel composition is not admitted so that not even the communication keys of [ 4 ] are needed. Furthermore, a single transition relation viewed as bidirectional and the distinction between outgoing and incoming transitions in the bisimulation game have been adopted like in [ 8 ].

In this paper we extend the work done in [ 9 ] to weak variants of forward-reverse, forward, and reverse bisimilarities over nondeterministic reversible sequential processes, where by weak we mean that the considered equivalences abstract from unobservable actions, traditionally denoted by . As far as compositionality is concerned, compared to [ 9 ] we discover that an initiality condition is necessary not only for forward bisimilarity but also for forward-reverse bisimilarity, which additionally solves the congruence problem with respect to nondeterministic choice afecting all weak variants of bisimilarity [ 6, 10 ]. As for equational characterizations, we retrieve the -laws of weak bisimilarity [ 6 ] and branching bisimilarity [ 10 ] over standard forward-only processes in the case of forward bisimilarity and forward-reverse bisimilarity respectively, along with some variants of those laws in the case of reverse bisimilarity. Together with the results in [ 8, 11 ], this emphasizes once more the connection between forward-reverse bisimilarity and branching bisimilarity.

The paper is organized as follows. In Section 2 we recall syntax and semantics for the calculus of nondeterministic reversible sequential processes as well as the forward, reverse, and forwardreverse bisimilarities introduced in [ 9 ]. In Section 3 we define the weak variants of the three aforementioned bisimilarities. In Section 4 we study their compositionality properties. Finally, in Section 5 we provide sound and ground-complete equational characterizations for the three weak bisimilarities.

2. Background

2.1. Syntax of Nondeterministic Reversible Sequential Processes where: Given a countable set of actions – ranged over by , , – including an unobservable action denoted by , the syntax of reversible sequential processes is as follows [ 9 ]: ::= 0 | . | †. | + • 0 is the terminated process. • . is a process that can execute action and whose continuation is . • † . is a process that executed action and whose continuation is in . • 1 + 2 expresses a nondeterministic choice between 1 and 2 as far as both of them have not executed any action yet.

We syntactically characterize through suitable predicates three classes of processes generated by the grammar above. Firstly, we have initial processes, i.e., processes in which all the actions are unexecuted:

initial(0) initial( . ) ⇐= initial( ) initial(1 + 2) ⇐= initial(1) ∧ initial(2)

Secondly, we have final processes, i.e., processes in which all the actions along a single path have been executed:

ifnal (0) ifnal (†. ) ⇐= final ( ) ifnal (1 + 2) ⇐= (final (1) ∧ initial(2)) ∨ (initial(1) ∧ final (2)) Multiple paths arise only in the presence of alternative compositions, i.e., nondeterministic choices. At each occurrence of +, only the subprocess chosen for execution can move, while the other one, although not selected, is kept as an initial subprocess within the overall process to support reversibility.

Thirdly, we have the processes reachable from an initial one, whose set we denote by P: reachable(0) reachable( . ) ⇐= initial( ) reachable(†. ) ⇐= reachable( ) reachable(1 + 2) ⇐= (reachable(1) ∧ initial(2)) ∨ (initial(1) ∧ reachable(2)) It is worth noting that: • 0 is the only process that is both initial and final as well as reachable. • Every initial or final process is reachable too. • P also contains processes that are neither initial nor final, like e.g. †. . 0. • The relative positions of already executed actions and actions to be executed matter; in particular, an action of the former kind can never follow one of the latter kind. For instance, †. . 0 ∈ P whereas . †. 0 ∈/ P.

(Actf )

initial( ) . →− †. (Chol) 1 →− 1′ initial(2) 1 + 2 →− 1′ + 2 (Actp)

→− ′ †. →− †. ′ (Chor) 2 →− 2′ initial(1) 1 + 2 →− 1 + 2′ 2.2. Operational Semantic Rules According to the approach of [ 4 ], dynamic operators such as action prefix and alternative composition have to be made static by the semantics, so as to retain within the syntax all the information needed to enable reversibility. For the sake of minimality, unlike [ 4 ] we do not generate two distinct transition relations – a forward one →− and a backward one − ⇝ – but a single transition relation, which we implicitly regard as being symmetric like in [ 8 ] to enforce the loop property: each executed action can be undone and each undone action can be redone.

In our setting, a backward transition from ′ to ( ′ − ⇝ ) is subsumed by the corresponding forward transition from to ′ ( →− ′). As will become clear with the definition of bisimulation equivalences, like in [ 8 ] when going forward we view as an outgoing transition of , while when going backward we view as an incoming transition of ′. The semantic rules for →− ⊆ P × × P are defined in Table 1 and generate the labeled transition system (P, , →− ) [ 9 ].

The first rule for action prefix ( Actf where f stands for forward) applies only if is initial and retains the executed action in the target process of the generated forward transition by decorating the action itself with †. The second rule for action prefix ( Actp where p stands for propagation) propagates actions executed by inner initial subprocesses.

In both rules for alternative composition (Chol and Chor where l stands for left and r stands for right), the subprocess that has not been selected for execution is retained as an initial subprocess in the target process of the generated transition. When both subprocesses are initial, both rules for alternative composition are applicable, otherwise only one of them can be applied and in that case it is the non-initial subprocess that can move, because the other one has been discarded at the moment of the selection.

Every state corresponding to a non-final process has at least one outgoing transition, while every state corresponding to a non-initial process has exactly one incoming transition due to the decoration of executed actions. The labeled transition system underlying an initial process turns out to be a tree, whose branching points correspond to occurrences of +. Example 2.1. The labeled transition systems generated by the rules in Table 1 for the two initial processes . 0 and . 0 + . 0 are depicted in Figure 1. As for the one on the right, we observe that, in the case of a standard process calculus, a single -transition from . 0 + . 0 to 0 would have been generated due to the absence of action decorations within processes. 2.3. Strong Forward, Reverse, and Forward-Reverse Bisimilarities While forward bisimilarity considers only outgoing transitions [ 7, 6 ], reverse bisimilarity considers only incoming transitions. Forward-reverse bisimilarity [ 4 ] considers instead both outgoing transitions and incoming ones. Here are their strong versions studied in [ 9 ], where strong means not abstracting from -actions.

Definition 2.2. We say that 1, 2 ∈ P are forward bisimilar, written 1 ∼ FB 2, if (1, 2) ∈ ℬ for some forward bisimulation ℬ. A symmetric relation ℬ over P is a forward bisimulation if for all (1, 2) ∈ ℬ and ∈ :

• Whenever 1 →− 1′ , then 2 →− 2′ with (1′ , 2′ ) ∈ ℬ.

Definition 2.3. We say that 1, 2 ∈ P are reverse bisimilar, written 1 ∼ RB 2, if (1, 2) ∈ ℬ for some reverse bisimulation ℬ. A symmetric relation ℬ over P is a reverse bisimulation if for all (1, 2) ∈ ℬ and ∈ :

• Whenever 1′ →− 1, then 2′ →− 2 with (1′ , 2′ ) ∈ ℬ.

Definition 2.4. We say that 1, 2 ∈ P are forward-reverse bisimilar, written 1 ∼ FRB 2, if (1, 2) ∈ ℬ for some forward-reverse bisimulation ℬ. A symmetric relation ℬ over P is a forward-reverse bisimulation if for all (1, 2) ∈ ℬ and ∈ : • Whenever 1 →− 1′ , then 2 →− 2′ with (1′ , 2′ ) ∈ ℬ.

• Whenever 1′ →− 1, then 2′ →− 2 with (1′ , 2′ ) ∈ ℬ.

∼ FRB ⊊ ∼ FB ∩ ∼ RB with the inclusion being strict because, e.g., the two final processes †. 0 and †. 0 + . 0 are identified by ∼ FB (no outgoing transitions on both sides) and by ∼ RB (only an incoming -transition on both sides), but distinguished by ∼ FRB as in the latter process action is enabled again after undoing (and hence there is an outgoing -transition in addition to an outgoing -transition). Moreover, ∼ FB and ∼ RB are incomparable because for instance: †. 0 ∼ FB 0 but †. 0 ̸∼ RB 0 . 0 ∼ RB 0 but . 0 ̸∼ FB 0 Note that that ∼ FRB = ∼ FB over initial processes, with ∼ RB strictly coarser, whilst ∼ FRB ̸= ∼ RB over final processes because, after going backward, previously discarded subprocesses come into play again in the forward direction.

Example 2.5. The two processes considered in Example 2.1 are identified by all the three equivalences. This is witnessed by any bisimulation that contains the pairs ( . 0, . 0 + . 0), (†. 0, †. 0 + . 0), and (†. 0, . 0 + †. 0).

As observed in [ 9 ], it makes sense that ∼ FB identifies processes with a diferent past and that ∼ RB identifies processes with a diferent future, in particular with 0 that has neither past nor future. However, for ∼ FB this results in a compositionality violation with respect to alternative composition. As an example:

†. . 0 ∼ FB . 0 †. . 0 + . 0 ̸∼ FB . 0 + . 0 because in †. . 0+ . 0 action is disabled due to the presence of the already executed action †, while in . 0 + . 0 action is enabled as there are no past actions preventing it from occurring. Note that a similar phenomenon does not happen with ∼ RB as †. . 0 ̸∼ RB . 0 due to the incoming -transition of †. . 0.

This problem, which does not show up for ∼ RB and ∼ FRB because these two equivalences cannot identify an initial process with a non-initial one, leads to the following variant of ∼ FB that is sensitive to the presence of the past.

Definition 2.6. We say that 1,2 ∈ P are past-sensitive forward bisimilar, written 1∼ FB:ps2, if (1, 2) ∈ ℬ for some past-sensitive forward bisimulation ℬ. A relation ℬ over P is a pastsensitive forward bisimulation if it is a forward bisimulation such that initial(1) ⇐⇒ initial(2) for all (1, 2) ∈ ℬ.

Now ∼ FB:ps is sensitive to the presence of the past:

†. . 0 ̸∼ FB:ps . 0 but can still identify non-initial processes having a diferent past:

†1 . ∼ FB:ps †2 . It holds that ∼ FRB ⊊ ∼ FB:ps ∩ ∼ RB, with ∼ FRB = ∼ FB:ps over initial processes as well as ∼ FB:ps and ∼ RB being incomparable because, e.g., for 1 ̸= 2: †1 . ∼ FB:ps †2 . but †1 . ̸∼ RB †2 .

1 . ∼ RB 2 . but 1 . ̸∼ FB:ps 2 .

In [ 9 ] it has been shown that all the considered bisimilarities are congruences with respect to action prefix, while only ∼ FB:ps, ∼ RB, and ∼ FRB are congruences with respect to alternative composition too, with ∼ FB:ps being the coarsest congruence with respect to + contained in ∼ FB. Sound and ground-complete equational characterizations have also been provided for the three equivalences that are congruences with respect to both operators.

3. Weak Bisimilarity and Reversibility

In this section we introduce weak variants of forward, reverse, and forward-reverse bisimilarities, i.e., variants capable of abstracting from -actions.

In the following definitions, ==⇒* ′ means that ′ = or there exists a nonempty sequence of finitely many -transitions such that the target of each of them coincides with the source of the subsequent one, with the source of the first one being and the target of the last one being ′. Moreover, ==⇒* →− ==⇒* stands for an -transition possibly preceded and followed by finitely many -transitions. We further let ¯ = ∖ { }.

* * weak forward bisimulation if for all (1, 2) ∈ ℬ :

Definition 3.1.

We say that 1, 2 ∈ P are weakly forward bisimilar, written 1 ≈ FB 2, if (1, 2) ∈ ℬ for some weak forward bisimulation ℬ. A symmetric binary relation ℬ over P is a • Whenever 1 →− 1′, then 2 ==⇒ 2′ and (1′, 2′) ∈ ℬ . • Whenever 1 →− 1′ for ∈ ¯, then 2 ==⇒ →− * * ==⇒ 2′ and (1′, 2′) ∈ ℬ . weak reverse bisimulation if for all (1, 2) ∈ ℬ :

Definition 3.2.

We say that 1, 2 ∈ P are weakly reverse bisimilar, written 1 ≈ RB 2, if (1, 2) ∈ ℬ for some weak reverse bisimulation ℬ. A symmetric binary relation ℬ over P is a • Whenever 1′ →− 1, then 2′ ==⇒* 2 and (1′, 2′) ∈ ℬ . • Whenever 1′ →− 1 for ∈ ¯, then 2′ ==⇒* →− * ==⇒ 2 and (1′, 2′) ∈ ℬ .

Definition 3.3.

We say that 1,2 ∈ P are weakly forward-reverse bisimilar, written 1≈ FRB2, over P is a weak forward-reverse bisimulation if for all (1, 2) ∈ ℬ : if (1, 2) ∈ ℬ for some weak forward-reverse bisimulation ℬ. A symmetric binary relation ℬ • Whenever 1 →− 1′, then 2 ==⇒ 2′ and (1′, 2′) ∈ ℬ . • Whenever 1 →− 1′ for ∈ ¯, then 2 ==⇒ →− * * ==⇒ 2′ and (1′, 2′) ∈ ℬ . • Whenever 1′ →− 1, then 2′ ==⇒* 2 and (1′, 2′) ∈ ℬ . • Whenever 1′ →− 1 for ∈ ¯, then 2′ ==⇒* →− * ==⇒ 2 and (1′, 2′) ∈ ℬ .

Each of the three weak bisimilarities is strictly coarser than the corresponding strong one. Similar to the strong case, ≈ FRB ⊊ ≈ FB ∩ ≈ RB with ≈ FB and ≈ RB being incomparable. Unlike the strong case, ≈ FRB ̸= ≈ FB over initial processes. For instance, . . 0 + . 0 + . 0 and . . 0 + . 0 are identified by ≈ FB but told apart by ≈ FRB: if the former performs , the latter responds with followed by and if it subsequently undoes thus becoming †. . 0 + . 0 in which only is enabled, the latter can only respond by undoing thus becoming . . 0 + . 0 + . 0 in which both and are enabled. An analogous counterexample with

4. Congruence Properties

it holds that: In this section we investigate the compositionality of the three weak bisimilarities with respect problem as weak bisimilarity for standard forward-only processes [ 6 ], i.e., for ≈ ∈ {≈ to the considered process operators. Firstly, we observe that ≈ FB sufers from the same problem with respect to alternative composition as ∼ FB. Secondly, ≈ FB and ≈ FRB feature the same . . 0 ≈ . 0 . . 0 + . 0 ̸≈ . 0 + . 0 because if . . 0 + . 0 performs thereby evolving to †. . 0 + . 0 where only is enabled in the forward direction, then . 0 + . 0 can neither move nor idle in the attempt to evolve in such a way to match †. . 0 + . 0.

To solve both problems it is suficient to redefine the two equivalences by making them sensitive to the presence of the past, exactly as in the strong case for forward bisimilarity. By so doing, . . 0 is no longer identified with . 0: if the former performs thereby evolving to †. . 0 and the latter idles, then †. . 0 and . 0 are told apart because they are not both initial or non-initial.

Definition 4.1. We say that 1, 2 ∈ P are weakly past-sensitive forward bisimilar, written 1 ≈ FB:ps 2, if (1, 2) ∈ ℬ for some weak past-sensitive forward bisimulation ℬ. A binary relation ℬ over P is a weak past-sensitive forward bisimulation if it is a weak forward bisimulation such that initial(1) ⇐⇒ initial(2) for all (1, 2) ∈ ℬ.

Definition 4.2. We say that 1, 2 ∈ P are weakly past-sensitive forward-reverse bisimilar, written 1 ≈ FRB:ps 2, if (1, 2) ∈ ℬ for some weak past-sensitive forward-reverse bisimulation ℬ. A binary relation ℬ over P is a weak past-sensitive forward-reverse bisimulation if it is a weak forward-reverse bisimulation such that initial(1) ⇐⇒ initial(2) for all (1, 2) ∈ ℬ.

Observing that ∼ FRB ⊊ ≈ FRB:ps as the former naturally satisfies the initiality condition, we show the following congruence results. When present, side conditions on subprocesses just ensure that the overall processes are reachable.

Theorem 4.3. Let ≈ ∈ {≈ and 1, 2 ∈ P:

FB, ≈ FB:ps, ≈ RB, ≈ FRB, ≈ FRB:ps}, ≈ ′ ∈ {≈ FB:ps, ≈ RB, ≈ FRB:ps}, • If 1 ≈ 2 then for all ∈ : – . 1 ≈ . 2 provided that initial(1) ∧ initial(2).

– †. 1 ≈ †. 2. • If 1 ≈ ′ 2 then for all ∈ P: – 1 + ≈ ′ 2 + and + 1 ≈ ′ + 2 provided that initial( ) ∨ (initial(1) ∧ initial(2)). • ≈ FB:ps is the coarsest congruence with respect to + contained in ≈ FB.

• ≈ FRB:ps is the coarsest congruence with respect to + contained in ≈ FRB.

Like in the non-past-sensitive case, ≈ FRB:ps ̸= ≈ FB:ps over initial processes, as shown by . . 0 + . 0 and . . 0: if the former performs , the latter responds with followed by and if it subsequently undoes thus becoming the non-initial process †. . 0, the latter can only respond by undoing thus becoming the initial process . . 0 + . 0. An analogous counterexample with non-initial -actions is given again by . ( . . 0 + . 0 + . 0) and . ( . . 0 + . 0).

It is worth noting that the aforementioned compositionality problems with respect to alternative composition may not be solved, in this reversible setting, by employing the construction of [ 6 ] for building a weak bisimulation congruence. If we introduced a variant ≈ ′FB of ≈ FB such that, when considering two initial processes, a -transition on either side must be matched by a -transition on the other side – possibly preceded and followed by finitely many -transitions – with the two reached processes being related by ≈ FB, then again †. . 0 ≈ ′FB . 0 but †. . 0 + . 0 ̸≈ ′FB . 0 + . 0 as explained in Section 2.3.

5. Equational Characterizations

In this section we investigate the equational characterizations of ≈ FB:ps, ≈ RB, and ≈ FRB:ps so as to highlight the fundamental laws of these behavioral equivalences. In the following, by deduction system we mean a set comprising the following axioms and inference rules over P – possibly enriched by a set of additional axioms – corresponding to the fact that ≈ FB:ps, ≈ RB, and ≈ FRB:ps are equivalence relations as well as congruences with respect to action prefix and alternative composition as established by Theorem 4.3: • Reflexivity, symmetry, transitivity: = , • .-Substitutivity: 1 = 2 initial(1) ∧ initial(2) . 1 = . 2 2 = 1 1 = 2 1 = 2 2 = 3 ,

.

1 = 3 ,

1 = 2 †. 1 = †. 2 • +-Substitutivity: 1 = 2 initial( ) ∨ (initial(1) ∧ initial(2)) 1 + = 2 + + 1 = + 2 .

.

It is known from [ 9 ] that, for the three strong bisimilarities, alternative composition turns out to be associative and commutative and to admit 0 as neutral element, like in the case of bisimilarity over standard forward-only processes [ 12 ]. The same holds true for ≈ FB:ps, ≈ RB, and ≈ FRB:ps as they are strictly coarser than their strong counterparts. This is formalized by axioms 1 to 3 in Table 2.

Then, we have axioms specific to ∼ FB:ps [ 9 ], which are thus valid for ≈ FB:ps too. Axioms 4 and 5 together establish that the past can be neglected when moving only forward, but the presence of the past cannot be ignored. Axiom 6 states that a previously non-selected alternative can be discarded after starting moving only forward.

Likewise, we have axioms specific to ∼ RB [ 9 ], which are thus valid for ≈ RB too. Axiom 7 means that the future can be completely canceled when moving only backward. Axiom 8 states that a previously non-selected alternative can be discarded when moving only backward. Since there are no constraints on , axiom 8 subsumes axiom 3.

Furthermore, the idempotency of alternative composition in the case of bisimilarity over standard forward-only processes, i.e., + = [ 12 ], changes as follows depending on the considered equivalence [ 9 ]: • For ∼ FB:ps, and hence ≈ FB:ps too, idempotency is explicitly formalized by axiom 9, which is disjoint from axiom 6 where cannot be initial. (1) (2) (3) (8 ) [≈ FRB:ps] †. ( †. (1′ + 2) + 1) = †. (1′ + 2) • For ∼ RB, and hence ≈ RB either, an additional axiom is not needed as idempotency follows from axiom 8 by taking equal to . • For ∼ FRB, and hence ≈ FRB:ps too, idempotency is formalized by axiom 10, where function to_initial brings a process back to its initial version by removing all action decorations: to_initial(0) = 0 to_initial( . ) = . to_initial(†. ) = . to_initial( ) to_initial(1 + 2) = to_initial(1) + to_initial(2) This axiom appeared for the first time in [ 13 ] and subsumes axioms 9 and 6 for ∼ FB:ps and ≈ FB:ps as well as axiom 8 for ∼ RB and ≈ RB.

Let us now focus on axioms specific to ≈ FB:ps, ≈ RB, and ≈ FRB:ps, which are usually called -laws. Axioms 1 to 3 are valid for ≈ FB:ps and coincide with those for weak bisimulation congruence over standard forward-only processes [ 12 ]. A variant of 1 with being decorated, i.e., axiom 4 , is also valid for ≈ FB:ps; note that †. †. = †. is valid too, but it follows from reflexity ( = ), axiom 5 or axiom 4 depending on whether is initial or not ( †. = †. ), and axiom 4 applied to the lefthand side along with transitivity. As far as . = is concerned, which over standard forward-only processes is valid for weak additional axioms below: -law of branching bisimulation congruence [ 10 ]. bisimilarity but not for weak bisimulation congruence [ 12 ], its reverse counterpart holds for ≈ RB, yielding axiom 5 . Axioms 6 , 7 ,

8 are valid for ≈ FRB:ps and are related to the only In the following, we denote by ⊢ the deduction relation and we examine the three sets of • FB:ps = {1, 2, 3, 4, 5, 6, 9, 1 , 2 , 3 ,

4 } for ≈ FB:ps. • RB = {1, 2, 7, 8, 5 } for ≈ RB.

• FRB:ps = {1, 2, 3, 10, 6 , 7 ,

8 } for ≈ FRB:ps.

After proving its soundness, we demonstrate the ground completeness of the equational characterization for each of the three considered weak bisimilarities by introducing as usual equivalence-specific normal forms to which every process is shown to be reducible, so that we then work with normal forms only. For each of the three weak bisimilarities, the normal form comes from the one of the corresponding strong bisimilarity in [ 9 ] and relies on the fact that alternative composition is associative and commutative, hence the binary + can be generalized to the -ary ∑︀ theorems will be by induction on the size of a process, which is inductively defined as follows: ∈ for a finite nonempty index set . The proofs of the ground completeness size(0) size( . ) size(†. ) size(1 + 2) = = = = 1 1 + size( ) 1 + size( ) max(size(1), size(2))

We start with the soundness and ground completeness of FB:ps with respect to ≈ FB:ps. To this purpose, we introduce the following function that extracts the forward behavior from a process by eliminating executed actions and non-selected alternatives:

to_forward( ) to_forward(†. ) to_forward(1 + 2) to_forward(1 + 2) = = = = to_forward( ) to_forward(1) to_forward(2) if initial( ) if ¬initial(1) ∧ initial(2) if ¬initial(2) ∧ initial(1) which yields an initial process and satisfies the following properties.

Proposition 5.1. Let , ′, ′′, ∈ P and ∈ : • to_forward( ) is initial, with to_forward( ) = when initial( ) while to_forward( ) ∼ FB when ¬initial( ). • →−

′ if to_forward( ) →− ′′ with ′ ∼ FB:ps ′′.

cannot execute -actions, else to_forward( ) ≈ FB to_forward().

• If ≈ FB:ps , then to_forward( ) ≈ FB:ps to_forward() when and are initial or Theorem 5.2. Let 1, 2 ∈ P. If FB:ps ⊢ 1 = 2 then 1 ≈ FB:ps 2.

Definition 5.3.

of the following:

We say that ∈ P is in forward normal form, written F-nf, if it is equal to one • 0. • ∑︀∈ . , where each is initial and in F-nf.

• †. ′, where ′ is initial and in F-nf.

Lemma 5.4. For all ∈ P there exists ∈ P in F-nf such that FB:ps ⊢ = .

Following the approach adopted in [ 6 ] for weak bisimulation congruence over standard forward-only processes, for ≈ FB:ps we introduce a saturated normal form where, unlike [ 6 ], two distinct equivalent processes ′ and ′′ come into play instead of a single process due to the presence of action decorations within processes in our reversible setting. This leads to the so-called saturation lemma, which immediately follows the definition below and, unlike [ 6 ], features to_forward( ′) in place of ′ in the final part of its statement.

Definition 5.5. We say that ∈ P is in forward saturated normal form, written F-snf, if it is equal to one of the following: • ∑︀∈ . , where each is initial and in F-snf • †. ′, where ′ is initial and in F-snf and whenever ==⇒* →− ==⇒* ′, then →− ′′ with ′ ≈ FB:ps ′′.

Lemma 5.6. [saturation lemma] Let ∈ P be initial. If ==⇒* →− ==⇒* ′ then FB:ps ⊢ = + . to_forward( ′).

Lemma 5.7. For all ∈ P in F-nf there exists ∈ P in F-snf such that FB:ps ⊢ = . Theorem 5.8. Let 1, 2 ∈ P. If 1 ≈ FB:ps 2 then FB:ps ⊢ 1 = 2.

As for the soundness and ground completeness of RB with respect to ≈ RB, the latter does not require saturation as no choice occurs when going backward.

Theorem 5.9. Let 1, 2 ∈ P. If RB ⊢ 1 = 2 then 1 ≈ RB 2.

Definition 5.10. We say that ∈ P is in reverse normal form, written R-nf, if it is equal to one of the following: • 0.

• †. ′, where ′ is in R-nf.

Lemma 5.11. For all ∈ P there exists ∈ P in R-nf such that RB ⊢ = . Theorem 5.12. Let 1, 2 ∈ P. If 1 ≈ RB 2 then RB ⊢ 1 = 2.

We conclude with the soundness and ground completeness of FRB:ps with respect to Theorem 5.13. Let 1, 2 ∈ P. If FRB:ps ⊢ 1 = 2 then 1 ≈ FRB:ps 2. Definition 5.14. We say that ∈ P is in forward-reverse normal form, written FR-nf, if it is equal to one of the following: ≈ FRB:ps.

• 0. • ∑︀∈ . , where each is initial and in FR-nf. • †. ′, where ′ is in FR-nf.

• †. ′ + ∑︀∈ . , where ′ is in FR-nf and each is initial and in FR-nf. Lemma 5.15. For all ∈ P there exists ∈ P in FR-nf such that FRB:ps ⊢ = . which is:

Similar to branching bisimulation semantics over standard forward-only processes [ 14 ], saturation is unsound for ≈ FRB:ps. In particular, a normal form based on saturation cannot be set up for ≈ FRB:ps. First of all, the backward version of: whenever ==⇒* →− ==⇒* ′, then →− ′′ with ′ ≈ FRB:ps ′′ whenever ′ ==⇒* →− ==⇒* , then ′′ →− with ′ ≈ FRB:ps ′′ can be satisfied only when ′ and ′′ coincide because can have only one incoming transition. Secondly, not even the forward version of saturation works for ≈ FRB:ps: • Consider ≜ . ( . . 0 + . 0) + . 0 + . 0 along with its two transitions: ==⇒* →− ==⇒* †. (†. †. 0 + . 0) + . 0 + . 0 ≜ ′ →− . ( . . 0 + . 0) + †. 0 + . 0 ≜ ′′ Then ′ ̸≈ FRB:ps ′′. Indeed, if ′ undoes with ′′ staying idle and then undoes thus reaching the non-initial process †. ( . . 0 + . 0) + . 0 + . 0, then ′′ can only respond by undoing thus reaching the initial process . • Consider ≜ . . ( . 0 + . 0) + . 0 + . 0 along with its two transitions: ==⇒* →− ==⇒* †. †. ( †. 0 + . 0) + . 0 + . 0 ≜ ′ →− . . ( . 0 + . 0) + †. 0 + . 0 ≜ ′′ Then ′ ̸≈ FRB:ps ′′. Indeed, if ′ undoes thus reaching †. †. ( . 0+ . 0)+ . 0+ . 0 with ′′ staying idle, then in the forward direction the newly reached process can perform whereas ′′ cannot.

To investigate the ground completeness of FRB:ps for ≈ FRB:ps, first of all we develop an alternative characterization of ≈ FRB:ps. This is inspired by the construction employed in [ 6 ] over forward-only processes to define weak bisimulation congruence on the basis of weak bisimulation equivalence. Consider for example . . 0 and . 0, which are identified by ≈ FRB but told apart by ≈ FRB:ps. The reason for distinguishing them is that if . . 0 performs thereby evolving to the non-initial process †. . 0, then the only way for . 0 to respond is idling thus remaining in an initial process. In the weak bisimulation congruence setting of [ 6 ], this would be reformulated in terms of the fact that the latter process has no initial -transition and hence cannot match the initial -transition of the former process.

In our reversible setting, the construction of [ 6 ] needs to be adapted as follows. In the case of two initial processes, every transition of either process must be matched by an identically labeled transition of the other process, with the two reached non-initial processes being related by ≈ FRB. In the case of two non-initial processes, in addition to requiring them to be ≈ FRBequivalent, we also have to make sure that their initial versions are equivalent in the sense above. For instance, the two non-initial processes †. †. 0 and †. 0 are identified by ≈ FRB, but to_initial( †. †. 0) = . . 0 ̸≈ FRB:ps . 0 = to_initial(†. 0), hence †. †. 0 ̸≈ FRB:ps †. 0 too. On the other hand, it is not enough to guarantee that the initial versions are equivalent, as for example to_initial(†. . 0) = . . 0 = to_initial(†. †. 0) but †. . 0 ̸≈ FRB †. †. 0. Definition 5.16. We say that 1, 2 ∈ P are weakly forward-reverse bisimulation congruent, written 1 ≈ FRB:c 2, if: • either 1 and 2 are both initial and, for all ∈ , whenever 1 →− 1′, then 2 →− 2′ and 1′ ≈ FRB 2′, and vice versa; • or 1 and 2 are both non-initial, 1 ≈ FRB 2, and to_initial(1) ≈ FRB:c to_initial(2). Theorem 5.17. Let 1, 2 ∈ P. Then 1 ≈ FRB:c 2 if 1 ≈ FRB:ps 2.

Secondly, we recast in our reversible setting a preliminary result for the completeness of the axiomatization of branching bisimulation congruence provided in [ 15 ]. This yields two lemmas, where the former is about ≈ FRB-equivalent initial processes that are then prefixed by an unexecuted action, while the latter has to do with ≈ FRB-equivalent arbitrary processes that are then prefixed by an executed action. The proof of the former lemma and part of the latter lemma is inspired by the proof of the preliminary result in the aforementioned paper. Each lemma is followed by the corresponding ground completeness result of FRB:ps for ≈ FRB:ps, in which the lemma itself can be employed thanks to the alternative characterization of ≈ FRB:ps. The former completeness result thus deals with ≈ FRB:ps-equivalent initial processes. The latter completeness result instead addresses ≈ FRB:ps-equivalent non-initial processes, with the related lemma exploiting completeness over initial processes.

Lemma 5.18. Let 1, 2 ∈ P be initial and ∈ . If 1 ≈ FRB 2 then FRB:ps ⊢ . 1 = . 2.

Theorem 5.19. Let 1, 2 ∈ P be initial. If 1 ≈ FRB:ps 2 then FRB:ps ⊢ 1 = 2. Lemma 5.20. Let 1, 2 ∈ P and ∈ . If 1 ≈ FRB 2 then FRB:ps ⊢ †. 1 = †. 2. Theorem 5.21. Let 1, 2 ∈ P be not initial. If 1 ≈ FRB:ps 2 then FRB:ps ⊢ 1 = 2. Acknowledgments. This research has been supported by the PRIN 2020 project NiRvAna – Noninterference and Reversibility Analysis in Private Blockchains. We are grateful to Rob van Glabbeek for the valuable discussions on branching bisimilarity and its axiomatization.

References

[1] R. Landauer , Irreversibility and heat generation in the computing process , IBM Journal of Research and Development 5 ( 1961 ) 183 - 191 .

[2] C. H. Bennett , Logical reversibility of computation, IBM Journal of Research and Development 17 ( 1973 ) 525 - 532 .

[3] V. Danos , J. Krivine , Reversible communicating systems , in: Proc. of the 15th Int. Conf. on Concurrency Theory (CONCUR 2004 ), volume 3170 of LNCS , Springer, 2004 , pp. 292 - 307 .

[4] I. Phillips , I. Ulidowski , Reversing algebraic process calculi , Journal of Logic and Algebraic Programming 73 ( 2007 ) 70 - 96 .

[5] I. Lanese , D. Medić , C. A. Mezzina , Static versus dynamic reversibility in CCS , Acta Informatica 58 ( 2021 ) 1 - 34 .

[6] R. Milner , Communication and Concurrency, Prentice Hall, 1989 .

[7] D. Park , Concurrency and automata on infinite sequences , in: Proc. of the 5th GI Conf. on Theoretical Computer Science , volume 104 of LNCS , Springer, 1981 , pp. 167 - 183 .

[8] R. De Nicola , U. Montanari , F. Vaandrager , Back and forth bisimulations , in: Proc. of the 1st Int. Conf. on Concurrency Theory (CONCUR 1990 ), volume 458 of LNCS , Springer, 1990 , pp. 152 - 165 .

[9] M. Bernardo , S. Rossi , Reverse bisimilarity vs. forward bisimilarity , in: Proc. of the 26th Int. Conf. on Foundations of Software Science and Computation Structures (FOSSACS 2023 ), volume 13992 of LNCS , Springer, 2023 , pp. 265 - 284 .

[10] R. J. van Glabbeek , W. P. Weijland , Branching time and abstraction in bisimulation semantics , Journal of the ACM 43 ( 1996 ) 555 - 600 .

[11] M. Bernardo , A. Esposito , Modal logic characterizations of forward, reverse, and forwardreverse bisimilarities , in: Proc. of the 14th Int. Symp. on Games , Automata, Logics, and Formal Verification (GANDALF 2023 ), volume 390 of EPTCS , 2023 , pp. 67 - 81 .

[12] M. Hennessy , R. Milner , Algebraic laws for nondeterminism and concurrency , Journal of the ACM 32 ( 1985 ) 137 - 162 .

[13] I. Lanese , I. Phillips , Forward-reverse observational equivalences in CCSK , in: Proc. of the 13th Int. Conf. on Reversible Computation (RC 2021 ), volume 12805 of LNCS , Springer, 2021 , pp. 126 - 143 .

[14] R. J. van Glabbeek , A complete axiomatization for branching bisimulation congruence of ifnite-state behaviours , in: Proc. of the 18th Int. Symp. on Mathematical Foundations of Computer Science (MFCS 1993 ), volume 711 of LNCS , Springer, 1993 , pp. 473 - 484 .

[15] L. Aceto , R. J. van Glabbeek , W. Fokkink , A. Ingolfsdottir , Axiomatizing prefix iteration with silent steps , Information and Computation 127 ( 1996 ) 26 - 40 .