Reversibility, allowing one to execute a program not only forwards as usual, but also backwards, has emerged as a fundamental concept in computing, with applications ranging from debugging and fault tolerance to biological and quantum systems. CCSK, a reversible extension of CCS, is a paradigmatic model of reversible concurrent computation. In this paper, we investigate the encodability of CCSK into classical forward-only concurrent models. We establish a separation theorem showing that there is no basic, success-sensitive encoding of CCSK into CCS or the π-calculus, highlighting the strong impact of reversibility on expressive power. We then present an encoding of CCSK processes with only top-level parallel composition into the internal π-calculus, correct up to strong bisimilarity. We also identify a fundamental limitation: no parallel-preserving encoding of CCSK (with arbitrary parallel composition) into the π-calculus can be correct up to strong bisimilarity. Finally, we provide a parallel-preserving encoding correct under a weaker behavioural correspondence: weak mutual simulation. Our findings extend the literature of encodability results to reversible process calculi.

Undoing computations of a concurrent system is beneficial in many situations, such as in reversible debugging of multi-threaded programs and in recovery from errors due to optimistic execution in parallel discrete event simulation. A number of approaches have been proposed for how to reverse formal models of concurrent computation, including process calculi such as CCS, languages like Erlang, and abstract models such as prime event structures and occurrence nets. However, it has not been settled as to what properties a reversible system should enjoy, nor how the various properties that have been suggested, such as the parabolic lemma and the causal-consistency property, are related. We contribute to a solution to these issues by using a generic labelled transition system equipped with a relation capturing whether transitions are independent to explore the implications between various reversibility properties. In particular, we show how all properties we consider are derivable from a set of axioms. Our intention is that when establishing properties of some formalism, it will be easier to verify the axioms rather than proving properties such as the parabolic lemma directly. We also introduce two new properties related to causal-consistent reversibility, namely causal liveness and causal safety, stating, respectively, that an action can be undone if (causal liveness) and only if (causal safety) it is independent from all of the following actions. These properties come in three flavours: defined in terms of independent transitions, independent events, or via an ordering on events. Both causal liveness and causal safety are derivable from our axioms.

Abstract Undoing computations of a concurrent system is beneficial in many situations, e.g., in reversible debugging of multi-threaded programs and in recovery from errors due to optimistic execution in parallel discrete event simulation. A number of approaches have been proposed for how to reverse formal models of concurrent computation including process calculi such as CCS, languages like Erlang, prime event structures and occurrence nets. However it has not been settled what properties a reversible system should enjoy, nor how the various properties that have been suggested, such as the parabolic lemma and the causal-consistency property, are related. We contribute to a solution to these issues by using a generic labelled transition system equipped with a relation capturing whether transitions are independent to explore the implications between these properties. In particular, we show how they are derivable from a set of axioms. Our intention is that when establishing properties of some formalism it will be easier to verify the axioms rather than proving properties such as the parabolic lemma directly. We also introduce two new notions related to causal consistent reversibility, namely causal safety and causal liveness, and show that they are derivable from our axioms.

In this paper we introduce Event Identifier Logic (EIL), which extends Hennessy–Milner logic by the addition of: (1) reverse as well as forward modalities; and (2) identifiers to keep track of events. We show that this logic corresponds to hereditary history-preserving (HH) bisimulation equivalence within a particular true-concurrency model, namely, stable configuration structures. We also show how natural sublogics of EIL correspond to coarser equivalences. In particular, we provide logical characterisations of weak-history- preserving (WH) and history-preserving (H) bisimulation. Logics corresponding to HH and H bisimulation have been given previously, but none, as far as we are aware, corresponding to WH bisimulation (when autoconcurrency is allowed). We also present characteristic formulas that characterise individual structures with respect to history-preserving equivalences.

Van Glabbeek and Goltz (and later Fecher) have investigated the relationships between various equivalences on stable configuration structures, including interleaving bisimulation (IB), step bisimulation (SB), pomset bisimulation and hereditary history-preserving (H-H) bisimulation. Since H-H bisimulation may be characterised by the use of reverse as well as forward transitions, it is of interest to investigate these and other forms of bisimulations where both forward and reverse transitions are allowed. Bednarczyk asked whether SB with reverse steps is as strong as H-H bisimulation. We answer this question negatively. We give various characterisations of SB with reverse steps, showing that forward steps do not add power. We strengthen Bednarczyk's result that, in the absence of auto-concurrency, reverse IB is as strong as H-H bisimulation, by showing that we need only exclude auto-concurrent events at the same depth in the configuration. We consider several other forms of observations of reversible behaviour and define a wide range of bisimulations by mixing the forward and reverse observations. We investigate the power of these bisimulations and represent the relationships between them as a hierarchy with IB at the bottom and H-H at the top.