Pith. sign in

REVIEW 3 major objections 4 minor 52 references

Expansion Laws for Forward-Reverse, Forward, and Reverse Bisimilarities via Proved Encodings

T0 review · 3 major / 4 minor · reviewed 2026-08-12 · deepseek-v4-flash

Challenge this review Re-run · record.json Download PDF Read on arXiv ↗ Review JSON

Pith's one-line read Concurrent reversible processes can be axiomatized by expansion laws, provided reverse and forward-reverse bisimilarities annotate every action prefix with the backward ready set of the reached process.

desk verdict Clever observation, broken encoding: the parallel non-initial case in Definition 5.3 makes the main theorems fail as stated. read the letter →

arxiv 2411.14583 v1 pith:4QPRELWH submitted 2024-11-21 cs.LO

Marco Bernardo (University of Urbino) , Andrea Esposito (University of Urbino) , Claudio A. Mezzina (University of Urbino) This is my paper · ORCID
classification cs.LO MSC 68Q85
keywords reversibleprocesscalculibisimilarityexpansionlawsprovedtreesbackwardreadysetstrueconcurrencyaxiomatizationparallelcomposition
verification ladder T0 review T1 audit T2 compute T3 formal

The pith

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The reading

This paper extends a reversible process calculus with parallel composition and asks whether the three standard behavioural equivalences — forward, reverse, and forward-reverse bisimilarity — can be captured by equational axioms. The authors establish that all three have sound and ground-complete axiomatizations, obtained by expansion laws that eliminate parallel composition. For the two truly concurrent equivalences, reverse and forward-reverse bisimilarity, the key new ingredient is that every action prefix in the encoded process must be annotated with the backward ready set of the process reached by that action, that is, the set of actions labelling its incoming transitions. The result matters because it gives a fully equational account of behaviour in reversible concurrent systems, allowing algebraic reasoning about systems that can undo computations.

What carries the argument

The machinery is the proved trees approach, in which every transition is labelled by a proof term — the action preceded by the sequence of operator contexts in whose scope it occurs — and an observation function maps proof terms to whatever the semantics under study should see. The paper instantiates this with three observation functions: $\ell_F(\theta) = act(\theta)$ for forward bisimilarity, and $\ell_R(\theta)_{P'} = \ell_{FR}(\theta)_{P'} = \langle act(\theta), brs(P')\rangle$ for the reverse and forward-reverse cases, where $brs(P')$ is the backward ready set of the reached process. The lifting of $\ell_{brs}$ to a process encoding $\widehat{P}$ annotates every action prefix with the backward ready set of the process reached so far, maintained by an environment-process update function. For parallel compositions where both sides have already executed non-synchronizing actions, the encoding orders the executed actions by a total order $\leq^{\dagger}$ over proof terms, because executed actions cannot both appear on either side of an alternative composition in a well-formed process.

What would settle it

Take the process $a^{\dagger}.0 \parallel_{\emptyset} b^{\dagger}.0$ with $a \neq b$ and compute its $\ell_{brs}$-encoding under two different admissible orders, for instance with $Ua \leq^{\dagger} Tb$ or with $Tb \leq^{\dagger} Ua$. If the two resulting processes are not bisimilar under $\sim_{RB}$ or $\sim_{FRB}$, then the encoding of Theorem 5.7 is not well-defined; if they are bisimilar but not provably equal in $A_R$ or $A_{FR}$, then the completeness theorems would need a proof of order-independence.

Watch

Extended reading notes

Core claim

The central claim is that proving the three bisimilarities equal over concurrent reversible processes reduces to choosing the right process encoding. For forward bisimilarity the observation function is the identity on actions, so the classical interleaving expansion law suffices, yielding the axiom system $A_F$ and Theorem 4.3: $P_1 \sim_{FB:ps} P_2$ iff $A_F \vdash P_1 = P_2$. For reverse and forward-reverse bisimilarities, the paper shows that the original transition labels carry no discriminating information about concurrency, and that the additional information needed is the backward ready set of the reached process: the observation is $\ell_{brs}(\theta)_{P'} = \langle act(\theta), brs(P')\rangle$. The encoding $\widehat{P}$ lifts this observation into action prefixes, and the main theorems state that $\widehat{P_1} \sim_{RB:\ell_{brs}} \widehat{P_2}$ iff $A_R \vdash \widehat{P_1} = \widehat{P_2}$ and $\widehat{P_1} \sim_{FRB:\ell_{brs}} \widehat{P_2}$ iff $A_{FR} \vdash \widehat{P_1} = \widehat{P_2}$. If correct, this gives sound and ground-complete equational characterizations of both truly concurrent reversible equivalences over the full calculus with parallel composition.

Load-bearing premise

The load-bearing premise is that the expansion laws for parallel composition of two non-initial processes use a total order $\leq^{\dagger}$ over proof terms, induced by the trace of actions executed so far; the paper does not give a concrete definition of this order and does not prove the encoding independent of the chosen linearization.

Editorial extensions

If this is right

  • $\sim_{FB:ps}$ over concurrent reversible processes is soundly and ground-completely axiomatized by the system $A_F$, whose single expansion law is the interleaving one.
  • $\sim_{RB}$ and $\sim_{FRB}$ are soundly and ground-completely axiomatized by $A_R$ and $A_{FR}$, whose expansion laws are expressed through the $\ell_{brs}$-encoding with backward ready sets in every action prefix.
  • $P_1 \sim_B P_2$ holds exactly when $\widehat{P_1} \sim_{B:\ell_{brs}} \widehat{P_2}$ for $B \in \{RB, FRB\}$, so the backward ready set is precisely the information needed to tell concurrent from sequential reversible behaviour.
  • All four bisimilarities are congruences with respect to parallel composition, so the axiomatizations compose with the rest of the calculus.
  • A fully equational account of truly concurrent reversible behaviour exists: algebraic derivations can replace bisimulation games for these equivalences.

Reading between the lines

Editorial extensions of the paper, not claims the author makes directly.

  • A natural extension of the paper's closing suggestion is that switching from backward ready sets to backward ready multisets may characterize hereditary history-preserving bisimilarity; counting occurrences of executed actions rather than just their presence would separate $a \parallel a$ from $a$ alone, a distinction the set version collapses.
  • The total order $\leq^{\dagger}$ in the non-initial parallel case is the only non-constructive point in the construction; proving order-independence would make the axiomatization fully syntactic.
  • The same observation-function method should transfer to weak ($\tau$-abstracting) versions of the three bisimilarities, with backward ready sets weakened by $\tau$-closure, giving expansion laws for weak reversible concurrency.
Share X Bluesky LinkedIn Reddit HN

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, and a circularity audit.

Referee Report

3 major / 4 minor

Summary. The paper extends the reversible process calculus of [13] with a CSP-style parallel composition and develops equational axiomatizations of past-sensitive forward bisimilarity (∼FB:ps), reverse bisimilarity (∼RB), and forward-reverse bisimilarity (∼FRB). The method follows the proved-trees approach of Degano and Priami: transitions are labelled with proof terms, observation functions map proof terms to the information relevant to each bisimilarity, and the observation function is lifted to a syntactic encoding eP of processes. For ∼FB:ps the encoding is the identity on action prefixes and the expansion law is interleaving (Section 4). For ∼RB and ∼FRB the paper claims that the needed extra information is the backward ready set brs of the reached process, so prefixes are annotated with such sets, and expansion laws are given in Definition 5.3. The main theorems are Theorem 4.3 (AF is sound and ground-complete for ∼FB:ps), Corollary 5.8 (P1 ∼B P2 iff eP1 ∼B:ℓbrs eP2 for B ∈ {RB, FRB}), and Theorems 5.11 and 5.14 (AR and AFR are sound and ground-complete for the encoded equivalences).

Significance. If correct, the paper would give a uniform, fully equational treatment of a truly concurrent reversible semantics, and it would identify backward ready sets as the discriminating information needed for expansion laws under reverse and forward-reverse bisimilarity. The congruence result for parallel composition (Theorem 2.8), the clean interleaving axiomatization for ∼FB:ps, and the systematic use of proved transitions are valuable components. However, the central construction for the truly concurrent cases is not well-defined as written: it relies on an unspecified total order, and the choice of that order changes the FRB:ℓbrs equivalence class of the encoding. Since Corollary 5.8 and the completeness theorems for AR and AFR depend on the encoding, the paper's main claims for reverse and forward-reverse bisimilarities are not established and, in the form stated, fail.

major comments (3)
  1. [Definition 5.3, fourth case] The expansion law for the both-non-initial parallel case is not well-defined. The text says the sequencing of already executed actions is chosen 'based on a total order ≤† over Θ induced by the trace of actions executed so far', but no definition of ≤† is ever given, and no invariance lemma is proved. The choice matters. For P = a†.0 ∥/0 b†.0 with a ≠ b, the calculation in Example 5.4 with Ua ≤† Tb gives eP = <a†,{a}>.<b†,{a,b}> + <b,{b}>.<a,{a,b}>.0; with the reversed order Tb ≤† Ua the same Definition 5.3 gives eQ = <b†,{b}>.<a†,{a,b}> + <a,{a}>.<b,{a,b}>.0. These two Pbrs processes are not ∼FRB:ℓbrs-equivalent: through the backward clause, eP has an incoming transition labelled (b,{b}) but no incoming transition labelled (a,{a}), whereas eQ has the dual behaviour. Since the original processes a†.0 ∥/0 b†.0 and b†.0 ∥/0 a†.0 are FRB-equivalent (their proved LTSs are isomorphic with the same action labels), any fixed deterministic reading of ≤† makes Corollary 5.8 false. This is a load-bearing defect, not a missing detail: the encoding is not a function of the process up to FRB-equivalence, and the completeness theorems for AR and AFR inherit the problem.
  2. [Corollary 5.8 and Theorems 5.11, 5.14] These results are stated without proof bodies in the submitted text, but more importantly they are not well-formed as consequences of Definition 5.3. Corollary 5.8 asserts P1 ∼B P2 iff eP1 ∼B:ℓbrs eP2; the counterexample above shows that the right-hand side depends on the unspecified order, not only on the FRB-equivalence class of the source process. Theorems 5.11 and 5.14 also quantify over eP1 and eP2, so their statements are indeterminate until the encoding is fixed. The paper needs either a concrete definition of ≤† with a proof that all admissible orders yield provably equivalent encodings, or a redesigned encoding that is canonical (for example, by carrying the full history or by constructing all legal linearizations rather than selecting one). Without such a mechanism, the central claims for reverse and forward-reverse bisimilarities cannot be accepted.
  3. [Proposition 5.6(2)] The paper itself concedes the problematic case. Proposition 5.6(2) states that brs(eP) = brs(P) fails when P has a subprocess P1 ∥L P2 with both components non-initial and different last executed actions outside L, and the subsequent example with a†.0 ∥/0 b†.0 shows brs(eP) = {b} while brs(P) = {a,b}. The explanation that '{a,b} occurs next to the last executed action b†' does not repair the invariance failure: in the bisimulation game on Pbrs the label of an incoming transition is determined by the backward ready set of the target state, and the asymmetric choice of which executed action counts as 'last' is exactly the arbitrary order that is never defined. The mismatch between brs(P) and brs(eP) is thus not a harmless technicality but a symptom of the non-canonicity of the encoding.
minor comments (4)
  1. [Definition 5.1] There is a typo in the phrase 'by induction on the syntactical structural of its first argument'; it should read 'syntactical structure'.
  2. [Table 4] Several axiom names and symbols in Table 4 appear corrupted in the rendered text (e.g., 'Â', 'fl', 'ga', '‡'); these should be typeset uniformly so that axioms AR,1–AR,5 and AFR,1–AFR,5 are readable.
  3. [Section 3] The description of the general expansion law for sequential processes is only a sketch, and the notation for the lifted encoding ℓσ is dense; a short example explicitly showing how the environment process E is threaded through the encoding would substantially improve readability.
  4. [Lemma 4.2 and Lemmas 5.10, 5.13] The proofs of the normal-form lemmas and of Theorems 4.3, 5.11, and 5.14 are omitted from the submitted text; if the version of record has an appendix, it should be included in the submission for refereeing.

Circularity Check

0 steps flagged · score 0.0 of 10

No significant circularity: the bisimilarities are fixed before the encoding, and the expansion laws are proved correct rather than defined to match; the ≤† gap is an ill-formedness issue, not circularity.

full rationale

The paper defines forward, reverse, and forward-reverse bisimilarities externally in Definitions 2.2–2.4 over the proved transition system, before introducing any encoding. The observation function ℓbrs and the encoding eP are then defined in Section 5, and Theorem 5.7 and Corollary 5.8 prove a transition-by-transition correspondence between P and eP rather than assuming it. The expansion axioms in Table 4 are not fitted parameters: they are conventional algebraic laws whose soundness and ground-completeness are established through normal forms and the prior sequential axiomatization [13], which supplies the base case rather than the concurrent result itself. The paper does not invoke a uniqueness theorem from its own authors to forbid alternatives, and it does not rename a known empirical pattern as a new derivation. The most serious weakness is formal, not circular: Definition 5.3 relies on a 'total order ≤† over Θ induced by the trace of actions executed so far' that is never defined, and no invariance lemma shows the encoding is independent of that order. This threatens the well-definedness of the encoding and hence theorems built on it, but it is a correctness and completeness gap, not a case of a conclusion being equivalent to its inputs by construction.

Assumptions & free parameters 1 free parameters · 4 assumptions · 2 invented entities

The central claim rests on the well-formed reversible process semantics and sequential axiomatizations imported from prior work, plus a choice of total order in one expansion subcase. No numerical parameters are fitted.

free parameters (1)
  • Total order ≤† over proof terms = not specified
    Definition 5.3 chooses one of two possible linearizations (Uθ1 ≤† Tθ2 or Tθ2 ≤† Uθ1) when expanding a†.0 ∥/0 b†.0; the paper does not fix a canonical order or prove the axiomatization independent of the choice.
assumptions (4)
  • domain assumption The well-formed process predicate wf and the proved transition system (P, Θ, →) of Section 2.2 are taken as the semantic foundation.
    The paper builds on the reversible CCS-like calculus from [13] with a single symmetric transition relation and loop property; these are assumed, not re-derived (Sections 2.1-2.2).
  • domain assumption Congruence and ground-completeness results for the sequential fragment from [13].
    The axioms AF,1-AF,7 and the base axioms for AR/AFR are imported from [13]; their correctness for sequential processes is assumed. Sections 4 and 5 state 'all the axioms apart from the last one come from [13]'.
  • standard math Classical expansion-law proof method of Hennessy-Milner (normal forms, induction).
    The soundness/completeness proofs (stated without proof bodies) rely on the standard ground-completeness technique introduced in [32].
  • domain assumption Symmetry of transitions and the loop property [26] permit treating backward moves as reverse forward transitions.
    The definitions of ∼RB and ∼FRB in Definitions 2.2-2.4 use outgoing/incoming transitions of a single proved transition relation, following [26,13].
invented entities (2)
  • Pbrs process syntax with action prefixes annotated by backward ready sets (<a, ℶ>.U) independent evidence
    purpose: Encoding target that carries the backward-ready information in the syntax, enabling expansion laws for truly concurrent reversible equivalences.
    Correctness of the encoding is proven in Theorem 5.7 (transition correspondence) and Corollary 5.8 (full abstraction), not merely asserted.
  • Observation functions ℓR and ℓFR (= ℓbrs) mapping proof terms to (action, backward ready set) independent evidence
    purpose: Define bisimilarities that coincide with ∼RB and ∼FRB and lift to process encoding.
    Proposition 2.7 and Theorem 5.7 establish the required properties of ℓbrs.

how reviews work

0 comments
Cite this review

Pith. "Pith review of Expansion Laws for Forward-Reverse, Forward, and Reverse Bisimilarities via Proved Encodings." pith.science (2026). https://pith.science/paper/4QPRELWH

@misc{pith2026241114583,
  author       = {Pith},
  title        = {Pith review of: Expansion Laws for Forward-Reverse, Forward, and Reverse Bisimilarities via Proved Encodings},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/4QPRELWH}},
  note         = {Machine review of arXiv:2411.14583}
}
read the original abstract

Reversible systems exhibit both forward computations and backward computations, where the aim of the latter is to undo the effects of the former. Such systems can be compared via forward-reverse bisimilarity as well as its two components, i.e., forward bisimilarity and reverse bisimilarity. The congruence, equational, and logical properties of these equivalences have already been studied in the setting of sequential processes. In this paper we address concurrent processes and investigate compositionality and axiomatizations of forward bisimilarity, which is interleaving, and reverse and forward-reverse bisimilarities, which are truly concurrent. To uniformly derive expansion laws for the three equivalences, we develop encodings based on the proved trees approach of Degano & Priami. In the case of reverse and forward-reverse bisimilarities, we show that in the encoding every action prefix needs to be extended with the backward ready set of the reached process.

Figures

Figures reproduced from arXiv: 2411.14583 by the authors.

Figure 1
Figure 1. Forward, reverse, and forward-reverse bisimilarities at work: interleaving vs. true concurrency [PITH_FULL_IMAGE:figures/full_fig_p002_1.png] view at source ↗

Discussion (0). Continue with ORCID to comment.

Reference graph

Works this paper leans on

52 extracted references · 30 canonical work pages

  1. [13]

    Bernardo & S

    M. Bernardo & S. Rossi (2023): Reverse Bisimilarity vs. Forward Bisimilarity. In: Proc. of the 26th Int. Conf. on Foundations of Software Science and Computation Structures (FOSSACS 2023), LNCS 13992, Springer, pp. 265–284, doi:10.1007/978-3-031-30829-1 13

    doi:10.1007/978-3-031-30829-1 2023

  2. [1]

    Aubert (2022): Concurrencies in Reversible Concurrent Calculi

    C. Aubert (2022): Concurrencies in Reversible Concurrent Calculi . In: Proc. of the 14th Int. Conf. on Reversible Computation (RC 2022) , LNCS 13354, Springer, pp. 146–163, doi:10.1007/978-3-031-09005- 9 10

    work page doi:10.1007/978-3-031-09005- 2022

  3. [2]

    Aubert & I

    C. Aubert & I. Cristescu (2017): Contextual Equivalences in Configuration Structures and Reversibility . Journal of Logical and Algebraic Methods in Programming86, pp. 77–106, doi:10.1016/j.jlamp.2016.08.004

    work page doi:10.1016/j.jlamp.2016.08.004 2017

  4. [3]

    Aubert & I

    C. Aubert & I. Cristescu (2020): How Reversibility Can Solve Traditional Questions: The Example of Hereditary History-Preserving Bisimulation. In: Proc. of the 31st Int. Conf. on Concurrency Theory (CON- CUR 2020), LIPIcs 171, pp. 7:1–7:23, doi:10.4230/LIPIcs.CONCUR.2020.7

    work page doi:10.4230/lipics.concur.2020.7 2020

  5. [4]

    Baldan & S

    P. Baldan & S. Crafa (2014): A Logic for True Concurrency . Journal of the ACM 61, pp. 24:1–24:36, doi:10.1145/2629638

    work page doi:10.1145/2629638 2014

  6. [5]

    Bednarczyk (1991): Hereditary History Preserving Bisimulations or What Is the Power of the Future Perfect in Program Logics

    M.A. Bednarczyk (1991): Hereditary History Preserving Bisimulations or What Is the Power of the Future Perfect in Program Logics. Technical Report, Polish Academy of Sciences, Gdansk

    work page 1991

  7. [6]

    Bennett (1973): Logical Reversibility of Computation

    C.H. Bennett (1973): Logical Reversibility of Computation. IBM Journal of Research and Development 17, pp. 525–532, doi:10.1147/rd.176.0525

    doi:10.1147/rd.176.0525 1973

  8. [7]

    Bergstra, J.W

    J.A. Bergstra, J.W. Klop & E.-R. Olderog (1988): Readies and Failures in the Algebra of Communicating Processes. SIAM Journal on Computing 17, pp. 1134–1177, doi:10.1137/0217073

    work page doi:10.1137/0217073 1988

Show all 52 references
  1. [8]

    Bernardo & A

    M. Bernardo & A. Esposito (2023): On the Weak Continuation of Reverse Bisimilarity vs. Forward Bisimi- larity. In: Proc. of the 24th Italian Conf. on Theoretical Computer Science (ICTCS 2023), CEUR-WS 3587, pp. 44–58

    2023

  2. [9]

    Bernardo & A

    M. Bernardo & A. Esposito (2023): Modal Logic Characterizations of Forward, Reverse, and Forward- Reverse Bisimilarities. In: Proc. of the 14th Int. Symp. on Games, Automata, Logics, and Formal Verification (GANDALF 2023), EPTCS 390, pp. 67–81, doi:10.4204/EPTCS.390.5

    2023 doi

  3. [10]

    Bernardo & C.A

    M. Bernardo & C.A. Mezzina (2023): Bridging Causal Reversibility and Time Reversibility: A Stochastic Process Algebraic Approach. Logical Methods in Computer Science19(2), pp. 6:1–6:27, doi:10.46298/lmcs- 19(2:6)2023

    2023 doi

  4. [11]

    Bernardo & C.A

    M. Bernardo & C.A. Mezzina (2023): Causal Reversibility for Timed Process Calculi with Lazy/Eager Du- rationless Actions and Time Additivity. In: Proc. of the 21st Int. Conf. on Formal Modeling and Analysis of Timed Systems (FORMATS 2023), LNCS 14138, Springer, pp. 15–32, doi:...

    2023 doi

  5. [12]

    Bernardo & C.A

    M. Bernardo & C.A. Mezzina (2024): Reversibility in Process Calculi with Nondeterminism and Probabili- ties. In: Proc. of the 21st Int. Coll. on Theoretical Aspects of Computing (ICTAC 2024), LNCS, Springer

    2024

  6. [14]

    Bocchi, I

    L. Bocchi, I. Lanese, C.A. Mezzina & S. Yuen (2024): revTPL: The Reversible Temporal Process Language. Logical Methods in Computer Science 20(1), pp. 11:1–11:35, doi:10.46298/lmcs-20(1:11)2024

    2024 doi

  7. [15]

    Boudol & I

    G. Boudol & I. Castellani (1988): Concurrency and Atomicity. Theoretical Computer Science 59, pp. 25–84, doi:10.1016/0304-3975(88)90096-5. 68 Expansion Laws for Forward-Reverse, Forward, and Reverse Bisimilarities via Proved Encodings

    1988 doi

  8. [16]

    Boudol & I

    G. Boudol & I. Castellani (1988): A Non-Interleaving Semantics for CCS Based on Proved Transitions . Fundamenta Informaticae 11, pp. 433–452, doi:10.3233/FI-1988-11406

    1988 doi

  9. [17]

    Boudol & I

    G. Boudol & I. Castellani (1994): Flow Models of Distributed Computations: Three Equivalent Semantics for CCS. Information and Computation 114, pp. 247–314, doi:10.1006/inco.1994.1088

    1994

  10. [18]

    Boudol, I

    G. Boudol, I. Castellani, M. Hennessy & A. Kiehn (1994): A Theory of Processes with Localities . Formal Aspects of Computing 6, pp. 165–200, doi:10.1007/BF01221098

    1994 doi

  11. [19]

    Brookes, C.A.R

    S.D. Brookes, C.A.R. Hoare & A.W. Roscoe (1984): A Theory of Communicating Sequential Processes . Journal of the ACM 31, pp. 560–599, doi:10.1145/828.833

    1984 doi

  12. [20]

    Castellani (1995): Observing Distribution in Processes: Static and Dynamic Localities

    I. Castellani (1995): Observing Distribution in Processes: Static and Dynamic Localities . Foundations of Computer Science 6, pp. 353–393, doi:10.1142/S0129054195000196

    1995 doi

  13. [21]

    Cristescu, J

    I. Cristescu, J. Krivine & D. Varacca (2013): A Compositional Semantics for the Reversible P-Calculus . In: Proc. of the 28th ACM/IEEE Symp. on Logic in Computer Science (LICS 2013) , IEEE-CS Press, pp. 388–397, doi:10.1109/LICS.2013.45

    2013 doi

  14. [22]

    Danos & J

    V . Danos & J. Krivine (2004): Reversible Communicating Systems . In: Proc. of the 15th Int. Conf. on Concurrency Theory (CONCUR 2004), LNCS 3170, Springer, pp. 292–307, doi:10.1007/978-3-540-28644- 8 19

    2004 doi

  15. [24]

    Darondeau & P

    Ph. Darondeau & P. Degano (1989): Causal Trees. In: Proc. of the 16th Int. Coll. on Automata, Languages and Programming (ICALP 1989), LNCS 372, Springer, pp. 234–248, doi:10.1007/BFb0035764

    1989 doi

  16. [25]

    Darondeau & P

    Ph. Darondeau & P. Degano (1990): Causal Trees: Interleaving + Causality . In: Proc. of the LITP Spring School on Theoretical Computer Science: Semantics of Systems of Concurrent Processes , LNCS 469, Springer, pp. 239–255, doi:10.1007/3-540-53479-2 10

    1990 doi

  17. [26]

    De Nicola, U

    R. De Nicola, U. Montanari & F. Vaandrager (1990): Back and Forth Bisimulations . In: Proc. of the 1st Int. Conf. on Concurrency Theory (CONCUR 1990) , LNCS 458, Springer, pp. 152–165, doi:10.1007/BFb0039058

    1990 doi

  18. [27]

    Degano & C

    P. Degano & C. Priami (1992): Proved Trees. In: Proc. of the 19th Int. Coll. on Automata, Languages and Programming (ICALP 1992), LNCS 623, Springer, pp. 629–640, doi:10.1007/3-540-55719-9 110

    1992 doi

  19. [28]

    Fecher (2004): A Completed Hierarchy of True Concurrent Equivalences

    H. Fecher (2004): A Completed Hierarchy of True Concurrent Equivalences. Information Processing Letters 89, pp. 261–265, doi:10.1016/j.ipl.2003.11.008

    2004 doi

  20. [29]

    Fr ¨oschle & S

    S. Fr ¨oschle & S. Lasota (2005): Decomposition and Complexity of Hereditary History Preserving Bisim- ulation on BPP . In: Proc. of the 16th Int. Conf. on Concurrency Theory (CONCUR 2005) , LNCS 3653, Springer, pp. 263–277, doi:10.1007/11539452 22

    2005 doi

  21. [30]

    Giachino, I

    E. Giachino, I. Lanese & C.A. Mezzina (2014): Causal-Consistent Reversible Debugging. In: Proc. of the 17th Int. Conf. on Fundamental Approaches to Software Engineering (FASE 2014) , LNCS 8411, Springer, pp. 370–384, doi:10.1007/978-3-642-54804-8 26

    2014 doi

  22. [31]

    van Glabbeek & U

    R.J. van Glabbeek & U. Goltz (2001): Refinement of Actions and Equivalence Notions for Concurrent Sys- tems. Acta Informatica 37, pp. 229–327, doi:10.1007/s002360000041

    2001 doi

  23. [32]

    Hennessy & R

    M. Hennessy & R. Milner (1985): Algebraic Laws for Nondeterminism and Concurrency . Journal of the ACM 32, pp. 137–162, doi:10.1145/2455.2460

    1985

  24. [33]

    Krivine (2012): A Verification Technique for Reversible Process Algebra

    J. Krivine (2012): A Verification Technique for Reversible Process Algebra. In: Proc. of the 4th Int. Workshop on Reversible Computation (RC 2012), LNCS 7581, Springer, pp. 204–217, doi:10.1007/978-3-642-36315- 3 17

    2012 doi

  25. [34]

    Landauer (1961): Irreversibility and Heat Generation in the Computing Process

    R. Landauer (1961): Irreversibility and Heat Generation in the Computing Process. IBM Journal of Research and Development 5, pp. 183–191, doi:10.1147/rd.53.0183. M. Bernardo, A. Esposito & C.A. Mezzina 69

    1961 doi

  26. [35]

    Lanese, M

    I. Lanese, M. Lienhardt, C.A. Mezzina, A. Schmitt & J.-B. Stefani (2013): Concurrent Flexible Reversibility. In: Proc. of the 22nd European Symp. on Programming (ESOP 2013) , LNCS 7792, Springer, pp. 370–390, doi:10.1007/978-3-642-37036-6 21

    2013 doi

  27. [36]

    Lanese, D

    I. Lanese, D. Medi ´c & C.A. Mezzina (2021): Static versus Dynamic Reversibility in CCS. Acta Informatica 58, pp. 1–34, doi:10.1007/s00236-019-00346-6

    2021 doi

  28. [38]

    Lanese, N

    I. Lanese, N. Nishida, A. Palacios & G. Vidal (2018): CauDEr: A Causal-Consistent Reversible Debugger for Erlang. In: Proc. of the 14th Int. Symp. on Functional and Logic Programming (FLOPS 2018) , LNCS 10818, Springer, pp. 247–263, doi:10.1007/978-3-319-90686-7 16

    2018 doi

  29. [40]

    Laursen, L.-P

    J.S. Laursen, L.-P. Ellekilde & U.P. Schultz (2018): Modelling Reversible Execution of Robotic Assembly . Robotica 36, pp. 625–654, doi:10.1017/S0263574717000613

    2018 doi

  30. [41]

    Milner (1989): Communication and Concurrency

    R. Milner (1989): Communication and Concurrency. Prentice Hall

    1989

  31. [42]

    Olderog & C.A.R

    E.-R. Olderog & C.A.R. Hoare (1986): Specification-Oriented Semantics for Communicating Processes . Acta Informatica 23, pp. 9–66, doi:10.1007/BF00268075

    1986 doi

  32. [43]

    Park (1981): Concurrency and Automata on Infinite Sequences

    D. Park (1981): Concurrency and Automata on Infinite Sequences. In: Proc. of the 5th GI Conf. on Theoret- ical Computer Science, LNCS 104, Springer, pp. 167–183, doi:10.1007/BFb0017309

    1981 doi

  33. [44]

    Perumalla & A.J

    K.S. Perumalla & A.J. Park (2014): Reverse Computation for Rollback-Based Fault Tolerance in Large Parallel Systems – Evaluating the Potential Gains and Systems Effects. Cluster Computing 17, pp. 303–313, doi:10.1007/s10586-013-0277-4

    2014 doi

  34. [45]

    Phillips & I

    I. Phillips & I. Ulidowski (2007): Reversing Algebraic Process Calculi . Journal of Logic and Algebraic Programming 73, pp. 70–96, doi:10.1016/j.jlap.2006.11.002

    2007 doi

  35. [46]

    Phillips & I

    I. Phillips & I. Ulidowski (2007): Reversibility and Models for Concurrency . In: Proc. of the 4th Int. Workshop on Structural Operational Semantics (SOS 2007) , ENTCS 192(1), Elsevier, pp. 93–108, doi:10.1016/j.entcs.2007.08.018

    2007 doi

  36. [47]

    Phillips & I

    I. Phillips & I. Ulidowski (2012): A Hierarchy of Reverse Bisimulations on Stable Configuration Structures. Mathematical Structures in Computer Science 22, pp. 333–372, doi:10.1017/S0960129511000429

    2012 doi

  37. [48]

    Phillips & I

    I. Phillips & I. Ulidowski (2014): Event Identifier Logic . Mathematical Structures in Computer Science 24(2), pp. 1–51, doi:10.1017/S0960129513000510

    2014 doi

  38. [49]

    Phillips, I

    I. Phillips, I. Ulidowski & S. Yuen (2012): A Reversible Process Calculus and the Modelling of the ERK Signalling Pathway. In: Proc. of the 4th Int. Workshop on Reversible Computation (RC 2012), LNCS 7581, Springer, pp. 218–232, doi:10.1007/978-3-642-36315-3 18

    2012 doi

  39. [50]

    Pinna (2017): Reversing Steps in Membrane Systems Computations

    G.M. Pinna (2017): Reversing Steps in Membrane Systems Computations. In: Proc. of the 18th Int. Conf. on Membrane Computing (CMC 2017) , LNCS 10725, Springer, pp. 245–261, doi:10.1007/978-3-319-73359- 3 16

    2017 doi

  40. [51]

    Rabinovich & B.A

    A.M. Rabinovich & B.A. Trakhtenbrot (1988): Behavior Structures and Nets. Fundamenta Informaticae 11, pp. 357–404, doi:10.3233/FI-1988-11404

    1988 doi

  41. [52]

    Schordan, T

    M. Schordan, T. Oppelstrup, D.R. Jefferson & P.D. Barnes Jr. (2018): Generation of Reversible C++ Code for Optimistic Parallel Discrete Event Simulation . New Generation Computing 36, pp. 257–280, doi:10.1007/s00354-018-0038-2

    2018 doi

  42. [53]

    Siljak, K

    H. Siljak, K. Psara & A. Philippou (2019): Distributed Antenna Selection for Massive MIMO Using Reversing Petri Nets. IEEE Wireless Communication Letters 8, pp. 1427–1430, doi:10.1109/LWC.2019.2920128. 70 Expansion Laws for Forward-Reverse, Forward, and Reverse Bisimilarities ...

    2019

  43. [54]

    Vassor & J.-B

    M. Vassor & J.-B. Stefani (2018): Checkpoint/Rollback vs Causally-Consistent Reversibility . In: Proc. of the 10th Int. Conf. on Reversible Computation (RC 2018) , LNCS 11106, Springer, pp. 286–303, doi:10.1007/978-3-319-99498-7 20

    2018 doi

  44. [55]

    de Vries, V

    E. de Vries, V . Koutavas & M. Hennessy (2010): Communicating Transactions. In: Proc. of the 21st Int. Conf. on Concurrency Theory (CONCUR 2010) , LNCS 6269, Springer, pp. 569–583, doi:10.1007/978-3- 642-15375-4 39

    2010 doi

Pith tools

Reviewed August 12, 2026 · model on record in the stance chip above.