Comparative Transition System Semantics for Cause-Respecting Reversible Prime Event Structures

TL;DR

This paper explores two different transition system semantics for cause-respecting reversible prime event structures, proving their bisimilarity and thus establishing a formal connection between the two approaches in reversible computing.

Contribution

It provides a formal comparison and proof of bisimilarity between configuration-based and residual-based transition semantics for cause-respecting reversible prime event structures.

Findings

Bisimilarity of the two semantics is established.

Step semantics are incorporated into the bisimilarity proof.

The work links configuration and residual approaches in reversible event structures.

Abstract

Reversible computing is a new paradigm that has emerged recently and extends the traditional forwards-only computing mode with the ability to execute in backwards, so that computation can run in reverse as easily as in forward. Two approaches to developing transition system (automaton-like) semantics for event structure models are distinguished in the literature. In the first case, states are considered as configurations (sets of already executed events), and transitions between states are built by starting from the initial configuration and repeatedly adding executable events. In the second approach, states are understood as residuals (model fragments that have not yet been executed), and transitions are constructed by starting from the given event structure as the initial state and deleting already executed (and conflicting) parts thereof during execution. The present paper focuses on an investigation of how the two approaches are interrelated for the model of prime event structures extended with cause-respecting reversibility. The bisimilarity of the resulting transition systems is proved, taking into account step semantics of the model under consideration.