The Category-Theoretic Characterization of Transition Systems Semantics for Cause-Respecting Reversible Prime Event Structures

Reversible computing, which has been widely studied in recent years, is an unconventional form of computing that can be performed in both directions: forward and backward. Any sequence of actions performed by the system can be later canceled for any reason (for example, in case of an error), allowing one to restore the system to its previous state, as if the canceled actions had never performed. Event structures are a fundamental model in concurrency theory, allowing us to comprehend the behavior of concurrent systems by describing system events and their relations. In the literature, there are two main approaches to constructing the semantics of transition systems for event structure models. One approach is based on configurations, i.e. sets of already executed events, and the other relies on residuals, i.e. model fragments that have not yet been executed. Configuration-based transition systems are mainly used to represent semantics and equivalences of concurrent models. Residual-based transition systems are actively involved to demonstrate the consistency between the operational and denotational semantics of algebraic calculi for concurrent processes, as well as to visualize the behavior of models. This article provides a category-theoretic characterization of these types of transition systems semantics for cause-respecting reversible prime event structures, and establishes the relationship between the semantics, which can be useful in constructing algebraic descriptions of the composition of reversible concurrent processes.