Towards a categorical representation of reversible event structures (Q2423742)

The paper is devoted to a mathematical model of concurrent computations obtained from event structures using the inversion of some events. Reversible versions of various kinds of event structures were introduced in [\textit{I. Phillips} et al., Lect. Notes Comput. Sci. 7948, 141--154 (2013; Zbl 1406.68029)]. The aim of the paper under review is to interpret them as objects in appropriate categories and study functors between them, as a foundation for using reversible event structures to give true concurrency semantics of reversible process calculi. In Section 2, the definitions of (forward-only) event structures and configurations are recalled. An event structure (ES) [\textit{G. Winskel}, Lect. Notes Comput. Sci. 255, 325--392 (1987; Zbl 0626.68022)] is a triple \( \mathcal{E}= (E, \text{Con}, \vdash)\), where \(E\) is a set of events, \(\text{Con}\subseteq_{\mathrm{\mathrm{fin}}} 2^E\) is the consistency relation, \(\vdash\,\subseteq \text{Con}\times E\) is the enabling relation, and 1. if \(X\in \text{Con}\) and \(Y\subseteq X\) then \(Y\in \text{Con}\); 2. if \(X\vdash e\) and \(X\subseteq Y\in \text{Con}\) then \(Y\vdash e\). Given an ES \( \mathcal{E}=(E, \text{Con}, \vdash)\), a configuration of \( \mathcal{E}\) is a set \(X\subseteq E\) such that 1. for all \(X'\subseteq_{\mathrm{\mathrm{fin}}} X\), \(X'\in \text{Con}\); 2. for all \(e\in X\), there exists a sequence \(e_0, \ldots, e_n\) such that \(e_n=e\) and for all \(0\leq i\leq n\), \(\{e_0, \ldots, e_{i-1}\}\vdash e_i\). Reversible models are defined in the opposite direction. First, reversible configurations are introduced, and then reversible event structures. A configuration system (CS) [\textit{I. Phillips} and \textit{I. Ulidowski}, J. Log. Algebr. Methods Program. 84, No. 6, 781--805 (2015; Zbl 1330.68213)] is a quadruple \( \mathcal{C}=(E,F, \text{C}, \to)\) where \(E\) is a set of events, \(F\subseteq E\) is a set of reversible events, \(\text{C}\subseteq 2^E\) is the set of configurations, and \(\to~\subseteq \text{C}\times 2^{E\cup \underline{F}}\times \text{C}\) is a labelled transition relation such that if \(X \overset{A\cup \underline{B}}{\longrightarrow} Y\) then: 1. \(A\cap B=\emptyset\); 2. \(B\subseteq X\cap F\); 3. \(Y= (X\setminus B)\cup A\); 4. for all \(A'\subseteq A\) and \(B'\subseteq B\), we have \(X \overset{A'\cup \underline{B'}}{\longrightarrow} Z \overset{(A\setminus A')\cup (\underline{B\setminus B'})}\longrightarrow Y \) (where \(Z= (X\setminus B')\cup A' \in \text{C}\)). The reversible (general) event structure differs from the general event structure not only by allowing the reversal of events, but also by including a preventing set in the enabling relation so that \(X\varobslash Y \vdash e\) means \(e\) is enabled in configurations that include all the events of \(X\) but none of the events of \(Y\). Definition 6.1. A reversible event structure (shortly RES) is a quadruple \( \mathcal{E}= (E, F, \text{Con}, \vdash)\) where \(E\) is the set of events, \(F\subseteq E\) is the set of reversible events, \(\text{Con}\subseteq_{\mathrm{fin}} 2^E\) is the consistency relation, which is downwards closed, \(\vdash\, \subseteq \text{Con}\times 2^E\times (E\cup \underline{F})\) is the enabling relation, and 1. if \(X\varobslash Y\vdash e^*\) then \((X\cup \{e\})\cap Y= \emptyset\); 2. if \(X\varobslash Y \vdash \underline{e}\) then \(e\in X\); 3. (weakening) if \(X\varobslash Y\vdash e^*\), \(X\subseteq X'\in \text{Con}\), and \(X'\cap Y=\emptyset\) then \(X'\varobslash Y\vdash e^*\). The functor \(C_r: \text{RES} \to \text{CS}\) is introduced in Definition 6.10. Definition 6.11. A CS \( \mathcal{C}=(E, F, \text{C}, \to)\) is called to be finitely enabled if 1. \(\text{C}\) is downwards closed; 2. \(X\in\text{C}\) if and only if for all \(X'\subseteq_{\mathrm{fin}} X\), \(X'\in\text{C}\); 3. whenever \(X \overset{e^*}\rightarrow\), there exists a finite configuration \(X'\subseteq_{\mathrm{fin}}X\) such that \(X'' \overset{e^*}\rightarrow\) for all \(X''\) such that \(X'\subseteq X''\subseteq X\). The morphisms in the category FCS are defined as CS morphisms. \(C_r: \text{RES}\to \text{FCS}\) is a functor (Proposition 6.12). A functor \(R: \text{FCS}\to \text{RES}\) is constructed (Definition 6.14 and Proposition 6.15). The following theorem states that \(C_r\) and \(R\) are inverses of each other for CSs for which the set of configurations is downwards closed and derived from the set of finite configurations, and no transitions start from infinite configurations which are not part of a larger transition going through a finite configuration: Theorem 6.16. Given an FCS \( \mathcal{C}=(E, F, \text{C}, \to)\), we have \(C_r(R( \mathcal{C}))= \mathcal{C}\) if whenever \(X \overset{A\cup \underline{B}}\longrightarrow\), there exists \(X'\) such that \(X' \overset{A'\cup \underline{B'}}\longrightarrow\), where \(X'\setminus B'\) is finite, \(A\subseteq A'\), \(X\cup A \subseteq X'\cup A'\) and \(B\subseteq B'\). Theorem 6.17 states that the functor \(R: \text{FCS}\to \text{RES}\) is left adjoint to the functor \(C_r: \text{RES}\to \text{FCS}\). No functor is known from asymmetric event structures to general event structures such that a general event structure maps to the same domain as an asymmetric one. Nevertheless, in this paper a functor is constructed from the category of reversible asymmetric event structures to reversible general event structures and the correspondence between them is shown (Theorem 6.23). The paper provides a large number of examples of models associated with event structures. The authors prove a large number of properties of the categories whose objects these models are, as well as properties of the functors between the categories of these models.