Reversible Causal Nets and Reversible Event Structures

TL;DR

This paper introduces reversible causal nets, establishing a precise correspondence with a subclass of reversible prime event structures, thereby advancing the modeling of reversible computation in concurrency theory.

Contribution

It defines reversible causal nets and proves their equivalence with causal reversible prime event structures, bridging a gap in reversible concurrency models.

Findings

Reversible causal nets generalize reversible unfolding.

Reversible causal nets correspond exactly to causal reversible prime event structures.

The work enhances modeling capabilities for reversible computation in concurrency theory.

Abstract

One of the well-known results in concurrency theory concerns the relationship between event structures and occurrence nets: an occurrence net can be associated with a prime event structure, and vice versa. More generally, the relationships between various forms of event structures and suitable forms of nets have been long established. Good examples are the close relationship between inhibitor event structures and inhibitor occurrence nets, or between asymmetric event structures and asymmetric occurrence nets. Several forms of event structures suited for the modelling of reversible computation have recently been developed; also a method for reversing occurrence nets has been proposed. This paper bridges the gap between reversible event structures and reversible nets. We introduce the notion of reversible causal net, which is a generalisation of the notion of reversible unfolding. We show that reversible causal nets correspond precisely to a subclass of reversible prime event structures, the causal reversible prime event structures.