Dieses Kapitel untersucht die Charakterisierung erbgeschichtserhaltender Doppelgleisigkeiten, ein entscheidendes Konzept im Bereich wahrhaft gleichzeitiger Doppelgleisigkeiten. Es beginnt mit einer Überprüfung der grundlegenden Prinzipien geschichtserhaltender und erbgeschichtserhaltender Unterschiede, wobei ihre Bedeutung für die Erhaltung von Kausalität, Verzweigung und das Zusammenspiel dieser Elemente hervorgehoben wird. Anschließend stellt der Text alternative Charakterisierungen erbgeschichtserhaltender Doppelgleisigkeit vor, wobei der Schwerpunkt auf hin und her sowie vorwärts und rückwärts gerichteter Doppelgleisigkeit liegt, und diskutiert ihre Implikationen in Ermangelung autoconcurrency. Es wird ein neuartiger Ansatz vorgestellt, der den Fokus von der eindeutigen Identifizierung identisch bezeichneter Ereignisse auf deren Zählung verlagert und so die Notwendigkeit von Zwischentönen zwischen den Ereignissen vermeidet. Dieser Ansatz wird durch die Definition rückwärts bereiter Multisets ausgearbeitet, die verwendet werden, um die Vorwärts-Rückwärts-Doppelähnlichkeit zu erweitern. Das Kapitel enthält auch eine detaillierte Beschreibung der Vorgänge auf der Grundlage einer Variante der reversiblen Prozesskalkulation, die Beweiserklärungen zur Formalisierung von Ereignissen enthält. Es schließt mit einer Diskussion über die Beziehungen zwischen verschiedenen logischen Rahmenwerken und schlägt Richtungen für zukünftige Forschung vor, was es zu einer unverzichtbaren Lektüre für diejenigen macht, die sich für die fortgeschrittene Erforschung gleichzeitiger Systeme interessieren.
KI-Generiert
Diese Zusammenfassung des Fachinhalts wurde mit Hilfe von KI generiert.
Abstract
We provide two alternative characterizations of hereditary history-preserving bisimilarity: a denotational one, on stable configuration structures, and an operational one, on a reversible process calculus. The characterizing equivalence is forward-reverse bisimilarity extended with a check for backward ready multiset equality. Unlike previous approaches, the focus is thus on counting identically labeled events rather than uniquely identifying them. We also investigate the relationships between event identifier logic, characterizing the former bisimilarity, and backward ready multiset logic, characterizing the latter bisimilarity.
1 Introduction
In the spectrum of truly concurrent bisimilarities [19, 23, 32], there are two equivalences that are particularly important: history-preserving bisimilarity [34] and hereditary history-preserving bisimilarity [6]. They are the coarsest equivalence and the finest equivalence, respectively, that are preserved under action refinement and are capable of respecting causality, branching, and their interplay while abstracting from choices between identical alternatives [23]. Moreover, hereditary history-preserving bisimilarity can be obtained as a special case of a categorical definition of bisimilarity over concurrency models [25].
History-preserving and hereditary history-preserving bisimilarities are defined over truly concurrent models such as event structures [35] or their variants, in particular configuration structures [24]. A configuration is a finite set of non-conflicting events that is downward-closed with respect to a causality relation over events. The bisimulation game compares configuration transitions. While history-preserving bisimilarity considers only outgoing transitions, hereditary history-preserving bisimilarity takes into account also incoming transitions. In other words, the former stepwise matches only forward computations, whereas the latter examines backward computations too. Both equivalences rely on ternary bisimulation relations, where the third component is a labeling- and causality-preserving bijection from the set of events executed so far in the first structure to the set of events executed so far in the second structure.
Anzeige
Logical characterizations of both equivalences have been provided in [4, 33]. Furthermore, an axiomatization for hereditary history-preserving bisimilarity has been developed over forward-only processes in [21]. Finally, history-preserving bisimilarity is known to coincide with causal bisimilarity [15, 16], hence the latter offers a characterization and an axiomatization [18] for the former. In this paper, we concentrate on characterizations of hereditary history-preserving bisimilarity.
The first alternative characterization of hereditary history-preserving bisimilarity has appeared in [6] for configuration graphs of prime event structures. The characterizing equivalence is called back-and-forth bisimilarity – not to be confused with the homonymous one in [17], which retrieves an interleaving semantics by constraining backward computations to take place along the corresponding forward computations even in the presence of concurrency. The main difference between hereditary history-preserving bisimilarity and back-and-forth bisimilarity is that the latter relies on binary bisimulation relations, hence no labeling- and causality-preserving bijection is stepwise built during the bisimulation game. The characterization result holds under the assumption of no autoconcurrency, i.e., the absence of configurations from which it is possible to execute two identically labeled, distinct events that are not in conflict with each other.
Fig. 1.
Configuration graphs: autoconcurrency (a), autocausation (b), and autoconflict
In Figures 1(a) and (b) we show the configuration graphs respectively associated with the following two processes for a given action a:
Autoconcurrency on a, which is expressed as \(a \mathop {\Vert } a\) where \(\mathop {\Vert }\) stands for parallel composition. There are two equally labeled, non-conflicting events, denoted by
and
, that can be executed in any order.
Autocausation on a, which is expressed as \(a \, . \, a\) where dot represents action prefix. There are two equally labeled, non-conflicting events, denoted by a and .a, such that the former has to be executed before the latter.
These two configuration graphs are back-and-forth bisimilar as witnessed by the symmetric binary relation that contains the pairs of configurations
,
, and
. However, they are not hereditary history-preserving bisimilar because, with respect to the last pair, there is no (labeling- and) causality-preserving bijection that maps the two independent events
and
to the two causally-related events a and .a.
Anzeige
The second alternative characterization of hereditary history-preserving bisimilarity has been given in [31]. The characterizing equivalence is the forward-reverse bisimilarity – very close in spirit to the back-and-forth bisimilarity of [6] – originally defined in [30] for a reversible variant of CCS [29] called CCSK. The operational semantics of CCSK produces labeled transition systems based on a forward transition relation and a backward one ensuring the loop property [13]. Each transition label comprises an action and a communication key; the latter is necessary when building backward transitions so as to know who synchronized with whom in the forward direction. In [31] forward-reverse bisimilarity has been generalized to configuration graphs of prime event structures and shown to coincide with hereditary history-preserving bisimilarity in the absence of repeated, identically labeled events along forward computations, which implies the absence of autoconcurrency (and autocausation), i.e., the assumption made in [6].
In [32] it has been shown, by working on stable configuration structures, how to relax the conditions under which the two characterization results of [6] and [31] hold. Specifically, it is sufficient to require the absence of equidepth autoconcurrency, i.e., the absence of identically labeled events occurring at the same depth within a configuration; the depth of an event is defined as the length of the longest causal chain of events up to and including the considered event.
The third alternative characterization of hereditary history-preserving bisimilarity has been provided in [3] and, unlike the previous two, does not need any restrictive assumption. Based on earlier work [2] – in which hereditary history-preserving bisimilarity was shown to coincide with back-and-forth barbed bisimulation congruence over singly-labeled processes, i.e., processes with no autoconcurrency and autoconflict (see Figure 1(c)) – it has been developed in the setting of a different reversible variant of CCS called RCCS [13, 14, 27]. While in CCSK all executed actions and discarded alternative subprocesses are kept within the syntax of processes so as to enable reversibility, in RCCS the same information is stored into stack-based memories attached to processes; the two approaches have been proven to be equivalent in [28]. The idea in [3] is to import hereditary history-preserving bisimilarity in the RCCS setting by encoding memories, i.e., the past behavior, as identified configuration structures. These are stable configuration structures enriched with unique event identifiers, used in transition labels and exploited when undoing synchronizations. The characterizing equivalence, called back-and-forth bisimilarity and defined over RCCS processes, relies on ternary bisimulation relations in which the third component is a bijection from the set of identifiers of the actions executed so far in the first process to the set of identifiers of the actions executed so far in the second process.
Having to reintroduce a third component in the bisimulation relations in order to exactly characterize hereditary history-preserving bisimilarity amounts to certifying that “reversibility is not just back and forth” [3], i.e., the forward and backward bisimulation games alone are not enough. The question then becomes whether and to what extent a systematic event identification is really necessary.
This question also arises from the fact that, in the aforementioned bisimulation games, CCSK transition labels such as a[i] and a[j] are deemed to be different if the two keys i and j are different [30] – which results in the absence of repeated, identically labeled events along forward computations [31] – while identified RCCS transition labels like i:a and j:a are viewed as compatible even if i and j are different [3]. On the one hand, in CCSK the two processes \(a \mathop {\Vert } a\) and \(a \, . \, a\) are told apart by forward-reverse bisimilarity because the former evolves to \(a[i] \mathop {\Vert } a[j]\), which can undo a[i] and a[j] in any order, while the latter evolves to \(a[i] \, . \, a[j]\), from which only a[j] can be undone, hence undoing a[i] cannot be matched by undoing a[j]. On the other hand, in identified RCCS the same two processes are distinguished by back-and-forth bisimilarity because, although undoing i:a can be matched by undoing j:a, it is not possible to establish a suitable bijection from a distributed memory containing i:a in a location and j:a in another location to a centralized memory containing j:a on top of i:a.
In this paper we propose a totally different approach to exactly characterize hereditary history-preserving bisimilarity. Rather than the unique identification of identically labeled events, the focus is on counting them. Let us consider again Figures 1(a) and (b). If we look at the two top (resp. bottom) configurations, we note that the one on the left has two outgoing (resp. incoming) transitions, while the one on the right has only one. As for the top configuration on the left, in principle we may not know whether the branch is due to the fact that the two events are concurrent or conflicting. However, for the bottom configuration on the left we can certainly say that the two events are concurrent, as the models we are considering are truly concurrent and hence the configuration graph of process \(a \, . \, a + a \, . \, a\) where \(+\) stands for nondeterministic choice (see Figure 1(d)) cannot be isomorphic to the one of \(a \mathop {\Vert } a\) because it must have two different bottom configurations (\(\{ \mathop {. \!\! +} \!a, \mathop {. \!\! +} \!. a \}\) and \(\{ \mathop {+ \!\! .} a, \mathop {+ \!\! .} . a \}\)) instead of a single one.
As an extension of the notion of backward ready set exploited in [8] to axiomatize forward-reverse bisimilarity over reversible concurrent processes, we define the backward ready multiset of a configuration or process to be the multiset of labels of its incoming transitions. After recalling in Section 2 the definitions of stable configuration structure [24], hereditary history-preserving bisimilarity [6], and event identifier logic [33], we provide the following contributions:
In Section 3 we exhibit a denotational characterization on stable configuration structures: hereditary history-preserving bisimilarity turns out to coincide with forward-reverse bisimilarity extended with a clause for checking the equality of the backward ready multisets of matching configurations.
In Section 4 we exhibit an operational characterization based on a variant of the reversible process calculus of [8, 9] where executed action identification is limited to synchronizations. After revising its proved operational semantics inspired by [18] so as to faithfully account for causality and concurrency, we set up a backward-ready-multiset variant of forward-reverse bisimilarity and devise a backward ready multiset logic characterizing it. Then we define a denotational semantics based on stable configuration structures in which events are formalized as proof terms [10, 11], so as to import the notion of hereditary history-preserving bisimilarity. We show that the stable configuration structures associated with two processes are hereditary history-preserving bisimilar iff the two processes are equated by the backward-ready-multiset variant of forward-reverse bisimilarity.
In Section 5 we start the investigation of the relationships between the event identifier logic of [33] and our backward ready multiset logic.
Section 6 concludes the paper with directions for future work.
2 Hereditary History-Preserving Bisimilarity
In this section we recall hereditary history-preserving bisimilarity [6] over stable configuration structures [24] along with its logical characterization based on event identifier logic [33].
In the following two definitions taken from [23], \(\mathcal {P}_\textrm{fin}(\mathcal {E})\) denotes the set of finite subsets of set \(\mathcal {E}\) while \(f \upharpoonright X\) denotes the restriction of function f to set X.
Definition 1
A configuration structure is a quadruple \(\textsf {C} = (\mathcal {E}, \mathcal {C}, \mathcal {A}, l)\) where:
\(\mathcal {E}\) is a set of events.
\(\mathcal {C}\subseteq \mathcal {P}_\textrm{fin}(\mathcal {E})\) is a set of configurations.
\(\mathcal {A}\) is a countable set of labels.
\(l : \bigcup _{X \in \mathcal {C}} X \rightarrow \mathcal {A}\) is a labeling function.
\(\textsf {C}\) is said to be stable iff it is:
Rooted: \(\emptyset \in \mathcal {C}\).
Connected: \(\forall X \in \mathcal {C}\setminus \{ \emptyset \} .\exists e \in X .X \setminus \{ e \} \in \mathcal {C}\).
Closed under bounded unions and intersections: \(\forall X, Y, Z \in \mathcal {C}.X \cup Y \subseteq Z \Longrightarrow X \cup Y, X \cap Y \in \mathcal {C}\).
The causality relation over \(X \in \mathcal {C}\) is defined by letting \(e_{1} \le _{X} e_{2}\) for \(e_{1}, e_{2} \in X\) iff \(e_{2} \in Y\) implies \(e_{1} \in Y\) for all \(Y \in \mathcal {C}\) such that \(Y \subseteq X\); we write \(e_{1} <_{X} e_{2}\) when \(e_{1} \le _{X} e_{2}\) and \(e_{1} \ne e_{2}\). Two events \(e_{1}, e_{2} \in X\) are concurrent in X iff \(e_{1} \not <_{X} e_{2}\) and \(e_{2} \not <_{X} e_{1}\). We write \(X \, {\mathop {\longrightarrow }\limits ^{a}}_{\textsf {C}} \, X'\) for \(X, X' \in \mathcal {C}\) and \(a \in \mathcal {A}\) iff \(X \subseteq X'\), \(X' \setminus X = \{ e \}\), and \(l(e) = a\). \(\blacksquare \)
Definition 2
We say that two stable configuration structures \(\textsf {C}_{i} = (\mathcal {E}_{i}, \mathcal {C}_{i}, \mathcal {A}, l_{i})\), \(i \in \{ 1, 2 \}\), are hereditary history-preserving bisimilar, written \(\textsf {C}_{1} \sim _\textrm{HHPB} \textsf {C}_{2}\), iff there exists a hereditary history-preserving bisimulation between \(\textsf {C}_{1}\) and \(\textsf {C}_{2}\), i.e., a relation \(\mathcal {B}\subseteq \mathcal {C}_{1} \times \mathcal {C}_{2} \times \mathcal {P}(\mathcal {E}_{1} \times \mathcal {E}_{2})\) such that:
\(f \subseteq \mathcal {E}_{1} \times \mathcal {E}_{2}\) is a bijection from \(X_{1} \in \mathcal {C}_{1}\) to \(X_{2} \in \mathcal {C}_{2}\) that preserves:
\(*\) Labeling: \(l_{1}(e) = l_{2}(f(e))\) for all \(e \in X_{1}\).
\(*\) Causality: \(e \le _{X_{1}} e' \Longleftrightarrow f(e) \le _{X_{2}} f(e')\) for all \(e, e' \in X_{1}\).
For each \(X_{1} \, {\mathop {\longrightarrow }\limits ^{a}}_{\textsf {C}_{1}} \, X'_{1}\) there exist \(X_{2} \, {\mathop {\longrightarrow }\limits ^{a}}_{\textsf {C}_{2}} \, X'_{2}\) and \(f' \subseteq \mathcal {E}_{1} \times \mathcal {E}_{2}\) such that \((X'_{1}, X'_{2}, f') \in \mathcal {B}\) and \(f' \upharpoonright X_{1} = f\), and vice versa.
For each \(X'_{1} \, {\mathop {\longrightarrow }\limits ^{a}}_{\textsf {C}_{1}} \, X_{1}\) there exist \(X'_{2} \, {\mathop {\longrightarrow }\limits ^{a}}_{\textsf {C}_{2}} \, X_{2}\) and \(f' \subseteq \mathcal {E}_{1} \times \mathcal {E}_{2}\) such that \((X'_{1}, X'_{2}, f') \in \mathcal {B}\) and \(f \upharpoonright X'_{1} = f'\), and vice versa. \(\blacksquare \)
Since there is a single transition relation, similar to [6, 17] in the bisimulation game above a distinction is made between the outgoing transitions of \(X_{1}\) and \(X_{2}\) (\(X_{1} \, {\mathop {\longrightarrow }\limits ^{a}}_{{{{\textsf {\textit{C}}}}}_{1}} \, X'_{1}\) and \(X_{2} \, {\mathop {\longrightarrow }\limits ^{a}}_{{{{\textsf {\textit{C}}}}}_{2}} \, X'_{2}\) in the forward direction) and their incoming transitions (\(X'_{1} \, {\mathop {\longrightarrow }\limits ^{a}}_{{{{\textsf {\textit{C}}}}}_{1}} \, X_{1}\) and \(X'_{2} \, {\mathop {\longrightarrow }\limits ^{a}}_{{{{\textsf {\textit{C}}}}}_{2}} \, X_{2}\) in the backward direction).
Hereditary history-preserving bisimilarity is characterized by event identifier logic [33]. The set \(\mathcal {L}_\textrm{EI}\) of its formulas is generated by the following syntax:
where \(a \in \mathcal {A}\) and \(x \in \mathcal {I}\), with \(\mathcal {I}\) being a countable set of identifiers. The unary operators \(\langle x : a \rangle \! \rangle \_\) and \((x : a) \_\) act as binders for the identifiers inside them. Therefore, the set of identifiers that occur free in \(\phi \in \mathcal {L}_\textrm{EI}\) is defined by induction on the syntactical structure of \(\phi \) as follows:
where we say that \(\phi \) is closed if \(\textit{fi}(\phi ) = \emptyset \), open otherwise.
In order to assign meaning to open formulas, environments are employed to indicate what events the free identifiers are bound to. Given a configuration structure \({{{\textsf {\textit{C}}}}} = (\mathcal {E}, \mathcal {C}, \mathcal {A}, l)\), an environment is a partial function \(\rho : \mathcal {I}\rightharpoonup \mathcal {E}\). Given \(X \in \mathcal {C}\) and \(\phi \in \mathcal {L}_\textrm{EI}\), we say that \(\rho \) is a permissible environment for X and \(\phi \) iff \(\rho \) maps every free identifier in \(\phi \) to an event in X. Denoting with \(\textit{dom}(\rho )\) the domain of \(\rho \), \(\textit{rge}(\rho )\) the codomain of \(\rho \), and \(\rho _{\phi }\) the restriction \(\rho \upharpoonright \textit{fi}(\phi )\), permissibility is formalized as \(\textit{fi}(\phi ) \subseteq \textit{dom}(\rho )\) and \(\textit{rge}(\rho _{\phi }) \subseteq X\). The set of permissible environments for X and \(\phi \) is indicated by \(\textit{pe}(X, \phi )\).
The satisfaction relation \(\models \, \subseteq (\mathcal {C}\times \mathcal {E}^{\mathcal {I}}) \times \mathcal {L}_\textrm{EI}\), with \(\mathcal {E}^{\mathcal {I}}\) being the set of functions from \(\mathcal {I}\) to \(\mathcal {E}\), i.e., the set of environments, is defined by induction on the syntactical structure of \(\phi \in \mathcal {L}_\textrm{EI}\) as follows:
$${\begin{array}{rclcl} X & \models _{\rho } & \textsf{true}& \\ X & \models _{\rho } & \lnot \phi ' & \, \text {iff} \, & X \not \models _{\rho } \phi ' \\ X & \models _{\rho } & \phi _{1} \wedge \phi _{2} & \text {iff} & X \models _{\rho } \phi _{1} \text { and } X \models _{\rho } \phi _{2} \\ X & \models _{\rho } & \langle x : a \rangle \! \rangle \phi ' & \text {iff} & \text {there is } X \, {\mathop {\longrightarrow }\limits ^{l(e)}}_{{{{\textsf {\textit{C}}}}}} \, X' \text { such that } l(e) = a \text { and } X' \models _{\rho [x \mapsto e]} \phi ' \\ X & \models _{\rho } & (x : a) \phi ' & \text {iff} & \text {there is } e \in X \text { such that } l(e) = a \text { and } X \models _{\rho [x \mapsto e]} \phi ' \\ X & \models _{\rho } & \langle \! \langle x \rangle \phi ' & \text {iff} & \text {there is } X' \, {\mathop {\longrightarrow }\limits ^{l(e)}}_{{{{\textsf {\textit{C}}}}}} \, X \text { such that } \rho (x) = e \text { and } X' \models _{\rho } \phi ' \\ \end{array}}$$
where it is understood that the environment in the subscript of every occurrence of \(\models \) is permissible for the configuration on the left and the formula on the right. Moreover, \(\rho [x \mapsto e]\) is \(\rho \setminus \{ (x, \rho (x)) \} \cup \{ (x, e) \}\) if \(x \in \textit{dom}(\rho )\), \(\rho \cup \{ (x, e) \}\) otherwise.
Let \(\mathcal {L}_\textrm{EI}^\textrm{c}\) be the set of closed formulas of \(\mathcal {L}_\textrm{EI}\). Given \(\phi \in \mathcal {L}_\textrm{EI}^\textrm{c}\), we write \(X \models \phi \) as a shorthand for \(X \models _{\emptyset } \phi \) and \({{{\textsf {\textit{C}}}}} \models \phi \) as a shorthand for \(\emptyset \models \phi \). Image finiteness means no configuration has infinitely many transitions with the same label.
3 Characterization on Stable Configuration Structures
The first characterization that we provide for \(\sim _\textrm{HHPB}\) is on stable configuration structures. From a ternary bisimulation relation we move to a binary one where, instead of stepwise building a labeling- and causality-preserving bijection between the events of matching configurations – which are the events executed so far in both stable configuration structures – we just count the identically labeled incoming transitions of matching configurations. Given a configuration X, its backward ready multiset is defined as \(\textit{brm}(X) = \{ \! | \,a \in \mathcal {A}\mid X' \, {\mathop {\longrightarrow }\limits ^{a}}_{{{{\textsf {\textit{C}}}}}} \, X \, | \! \}\) where \(\{ \! | \,\) and \(\, | \! \}\) are multiset delimiters. We thus decorate the resulting forward-reverse bisimilarity with the acronym brm, standing for backward ready multiset.
Definition 3
We say that two stable configuration structures \(\textsf {C}_{i} = (\mathcal {E}_{i}, \mathcal {C}_{i}, \mathcal {A}, l_{i})\), \(i \in \{ 1, 2 \}\), are brm-forward-reverse bisimilar, written \(\textsf {C}_{1} \sim _\mathrm{FRB:brm} \textsf {C}_{2}\), iff there exists a brm-forward-reverse bisimulation between \(\textsf {C}_{1}\) and \(\textsf {C}_{2}\), i.e., a relation \(\mathcal {B}\subseteq \mathcal {C}_{1} \times \mathcal {C}_{2}\) such that \((\emptyset , \emptyset ) \in \mathcal {B}\) and, whenever \((X_{1}, X_{2}) \in \mathcal {B}\), then:
For each \(X_{1} \, {\mathop {\longrightarrow }\limits ^{a}}_{\textsf {C}_{1}} \, X'_{1}\) there exists \(X_{2} \, {\mathop {\longrightarrow }\limits ^{a}}_{\textsf {C}_{2}} \, X'_{2}\) such that \((X'_{1}, X'_{2}) \in \mathcal {B}\), and vice versa.
For each \(X'_{1} \, {\mathop {\longrightarrow }\limits ^{a}}_{\textsf {C}_{1}} \, X_{1}\) there exists \(X'_{2} \, {\mathop {\longrightarrow }\limits ^{a}}_{\textsf {C}_{2}} \, X_{2}\) such that \((X'_{1}, X'_{2}) \in \mathcal {B}\), and vice versa.
Let \(\textsf {C}_{i} = (\mathcal {E}_{i}, \mathcal {C}_{i}, \mathcal {A}, l_{i})\), \(i \in \{ 1, 2 \}\), be two stable configuration structures. Then \(\textsf {C}_{1} \sim _\textrm{HHPB} \textsf {C}_{2}\) iff \(\textsf {C}_{1} \sim _\mathrm{FRB:brm} \textsf {C}_{2}\). \(\blacksquare \)
4 Operational Characterization
The second characterization that we provide for \(\sim _\textrm{HHPB}\) is operational. More precisely, we present a variant of the syntax (Section 4.1) and the proved operational semantics (Section 4.2) of the reversible process calculus of [8, 9], followed by a redefinition of brm-forward-reverse bisimilarity on that variant along with a modal logic characterization (Section 4.3). Then we develop a denotational semantics for the modified calculus based on stable configuration structures (Section 4.4), so as to import the notion of hereditary history-preserving bisimilarity. Finally, we prove that the stable configuration structures associated with two processes are hereditary history-preserving bisimilar iff the two processes are brm-forward-reverse bisimilar (Section 4.5).
4.1 Syntax of Reversible Concurrent Processes
In the representation of a process, we are used to describe only its future behavior. However, in order to support reversibility in the style of [30], we need to equip the syntax with information about the past, in particular the actions that have already been executed. Taking inspiration from CCS [29] and CSP [12], given a countable set \(\mathcal {A}\) of actions including an unobservable action denoted by \(\tau \), we extend as follows the syntax for reversible concurrent processes of [8, 9]:
where \(a \in \mathcal {A}\), \(L \subseteq \mathcal {A}\setminus \{ \tau \}\), \(\varepsilon \) is the empty string, \(\theta \) is a proof term (its syntax will be provided in Section 4.2), and:
\(\underline{0}\) is the terminated process.
\(a \, . \, P\) is a process that can execute action a and whose forward continuation is P (unexecuted action prefix).
\(a^{\dag \xi } . \, P\) is a process that executed action a and whose forward continuation is inside P, which can undo action a after all executed actions within P have been undone (executed action prefix).
\(P_{1} + P_{2}\) expresses a nondeterministic choice between \(P_{1}\) and \(P_{2}\) as far as neither has executed any action yet, otherwise only the one that was selected in the past can move (past-sensitive alternative composition).
\(P_{1} \mathop {\Vert _{L}} P_{2}\) expresses that \(P_{1}\) and \(P_{2}\) proceed independently of each other on actions in \(\overline{L} = \mathcal {A}\setminus L\), while they have to synchronize on every action in L (parallel composition).
We can characterize two important classes of processes via as many predicates. Firstly, we define initial processes, in which all actions are unexecuted and hence no \(\dag \)-decoration appears:
Secondly, we define well-formed processes, whose set we denote by \(\mathcal {P}\), in which both unexecuted and executed actions can occur in certain circumstances:
Well formedness not only imposes that every unexecuted action is followed by an initial process, but also that in every alternative composition at least one subprocess is initial. Multiple paths may arise in the presence of both alternative and parallel compositions. However, at each occurrence of the former, only the subprocess chosen for execution can move. Although not selected, the other subprocess is kept as an initial subprocess within the overall process, in the same way as executed actions are kept inside the syntax [11, 30], so as to support reversibility. As an example, in \(a^{\dag } . \, b \, . \, \underline{0}+ c \, . \, d \, . \, \underline{0}\) the subprocess \(c \, . \, d \, . \, \underline{0}\) cannot move because a was selected in the choice between a and c.
It is worth noting that:
\(\underline{0}\) is both initial and well-formed.
Any initial process is well-formed too.
\(\mathcal {P}\) also contains processes that are not initial like, e.g., \(a^{\dag } . \, b \, . \, \underline{0}\), which can either do b or undo a.
In \(\mathcal {P}\) the relative positions of already executed actions and actions to be executed matter. Precisely, an action of the former kind can never occur after one of the latter kind. For instance, \(a^{\dag } . \, b \, . \, \underline{0}\in \mathcal {P}\) whereas \(b \, . \, a^{\dag } . \, \underline{0}\notin \mathcal {P}\).
In \(\mathcal {P}\) the subprocesses of an alternative composition can be both initial, but cannot be both non-initial. For example, \(a \, . \, \underline{0}+ b \, . \, \underline{0}\in \mathcal {P}\) while \(a^{\dag } . \, \underline{0}+ b^{\dag } . \, \underline{0}\notin \mathcal {P}\).
Sometimes we will need to bring a process back to its initial version. This is accomplished by removing all \(\dag \)-decorations through function \(\textit{to}\_\textit{init}: \mathcal {P}\rightarrow \mathcal {P}_\textrm{init}\) with \(\mathcal {P}_\textrm{init}\) being the set of initial processes of \(\mathcal {P}\), which is defined as follows:
According to [30] dynamic operators such as action prefix and alternative composition have to be made static in the operational semantic rules, so as to retain within the syntax all the information needed to enable reversibility. Unlike [30] we do not generate a forward transition relation and a backward one, but a single transition relation that we deem to be symmetric in order to enforce the loop property [13]: every executed action can be undone and every undone action can be redone. A backward transition from \(P'\) to P is subsumed by the corresponding forward transition t from P to \(P'\). As already done in Sections 2 and 3 as well as in [6, 17], we will view t as an outgoing transition of P when going forward, while we will view t as an incoming transition of \(P'\) when going backward.
Following [8] we provide an operational semantics based on [18], which is very concrete as every transition is labeled with a proof term [10, 11]. This is an action preceded by the sequence of operator symbols in the scope of which the action occurs inside the source process of the transition. In the case of a binary operator, the corresponding symbol also specifies whether the action occurs to the left or to the right. The syntax that we adopt for the set \(\varTheta \) of proof terms is the following where \(a \in \mathcal {A}\) and \(L \subseteq \mathcal {A}\setminus \{ \tau \}\):
The proved operational semantic rules are in Table 1 and generate the proved labeled transition system \((\mathcal {P}, \varTheta , \! \, {\mathop {\longrightarrow }\limits } \, \!)\) where \( \, {\mathop {\longrightarrow }\limits } \, \! \subseteq \mathcal {P}\times \varTheta \times \mathcal {P}\) is the proved transition relation. We denote by \(\mathbb {P}\subsetneq \mathcal {P}\) the set of processes that are reachable from an initial one via \( \, {\mathop {\longrightarrow }\limits } \, \!\). Not all well-formed processes are reachable; for example, \(a^{\dag } . \, \underline{0}\mathop {\Vert _{\{ a \}}} \underline{0}\) is not reachable from \(a \, . \, \underline{0}\mathop {\Vert _{\{ a \}}} \underline{0}\) as action a on the left cannot synchronize with any action on the right. From now on we consider only \(\mathbb {P}\) and denote by \(\mathbb {P}_\textrm{init}\) the subset of its initial processes. Every process in \(\mathbb {P}\) may have several outgoing transitions and, if it is not initial, has at least one incoming transition.
Table 1.
Proved operational semantic rules for reversible concurrent processes
Dummy
The first rule for action prefix (Act\(_\textrm{f}\) where f stands for forward) applies only if P is initial and retains the executed action in the target process of the generated forward transition by decorating the action itself with \(\dag \). The second rule (Act\(_\textrm{p}\) where p stands for propagation) propagates actions of inner initial subprocesses by putting an a-dot before them in the label for each outer executed a-action prefix that is encountered.
In both rules for alternative composition (Cho\(_\textrm{l}\) and Cho\(_\textrm{r}\) where l stands for left and r stands for right), the subprocess that has not been selected for execution is retained as an initial subprocess in the target process of the generated transition. When both subprocesses are initial, both rules for alternative composition are applicable, otherwise only one of them can be applied and in that case it is the non-initial subprocess that can move, because the other one has been discarded at the moment of the selection. The symbol \(\mathop {. \!\! +} \!\) or \(\mathop {+ \!\! .} \) is added at the beginning of the proof term.
Due to the \(\dag \)-decorations of executed actions inside the process syntax, over the set \(\mathbb {P}_\textrm{seq}\) of sequential processes – in which there are no occurrences of parallel composition – every non-initial process has exactly one incoming transition, proved labeled transition systems turn out to be trees, and well formedness coincides with reachability [9].
Example 1
The proved labeled transition system underlying the initial sequential process \(a \, . \, \underline{0}\) has a single transition \(a \, . \, \underline{0}\, {\mathop {\longrightarrow }\limits ^{a}} \, a^{\dag } . \, \underline{0}\). In contrast, the proved labeled transition system underlying the initial sequential process \(a \, . \, \underline{0}+ a \, . \, \underline{0}\) has the two transitions \(a \, . \, \underline{0}+ a \, . \, \underline{0}\, {\mathop {\longrightarrow }\limits ^{\mathop {. \!\! +} \!a}} \, a^{\dag } . \, \underline{0}+ a \, . \, \underline{0}\) and \(a \, . \, \underline{0}+ a \, . \, \underline{0}\, {\mathop {\longrightarrow }\limits ^{\mathop {+ \!\! .} a}} \, a \, . \, \underline{0}+ a^{\dag } . \, \underline{0}\). Note that the two target processes are different from each other due to the presence of action decorations, whereas a single a-transition from \(a \, . \, \underline{0}+ a \, . \, \underline{0}\) to \(\underline{0}\) would be generated in the setting of a forward-only process calculus. \(\blacksquare \)
The three rules for parallel composition use partial function \(\textit{act}: \varTheta \rightharpoonup \mathcal {A}\) to extract an action from a proof term \(\theta \). This function, which will be used throughout the paper, is defined by induction on the syntactical structure of \(\theta \) as follows:
In the first two rules (Par\(_\textrm{l}\) and Par\(_\textrm{r}\)), a single subprocess proceeds by performing an action not belonging to L, with
or
being placed at the beginning of the proof term. In the third rule (Syn), both subprocesses synchronize on an action in L and the resulting proof term contains both individual proof terms. If \(L = \emptyset \) or \(L = \mathcal {A}\setminus \{ \tau \}\), then the two subprocesses are fully independent or fully synchronized, respectively, on observable actions.
The natural target process \(P'_{1} \mathop {\Vert _{L}} P'_{2}\) of a synchronization has to be suitably manipulated in rule Syn to correctly reflect causality and concurrency. More precisely, the \(\dag \)-decoration of every executed action participating in the synchronization has to be enriched with a proof term of the form \(\langle \theta _{1}, \theta _{2} \rangle _{L}\). This is accomplished by taking \(\textit{enr}(P'_{1} \mathop {\Vert _{L}} P'_{2}, \langle \theta _{1}, \theta _{2} \rangle _{L}) = \textit{enr}'(P'_{1} \mathop {\Vert _{L}} P'_{2}, \langle \theta _{1}, \theta _{2} \rangle _{L}, \langle \theta _{1}, \theta _{2} \rangle _{L})\) as target process, where partial function \(\textit{enr}' : \mathbb {P}\times \varTheta \times \varTheta \rightharpoonup \mathbb {P}\) is defined by induction on the syntactical structure of its first argument \(P \in \mathbb {P}\) as follows:
Example 2
The proved labeled transition system underlying the initial process \((a \, . \, \underline{0}\mathop {\Vert _{\emptyset }} a \, . \, \underline{0}) \mathop {\Vert _{\{ a \}}} a \, . \, a \, . \, \underline{0}\), which is the synchronization of autoconcurrency with autocausation, has the following two maximal transition sequences:
Note that the target processes of the two sequences are different thanks to the different additional decorations of the pairs of synchronizing executed actions. Without those decorations, the two sequences would end up in the same process \((a^{\dag } . \, \underline{0}\mathop {\Vert _{\emptyset }} a^{\dag } . \, \underline{0}) \mathop {\Vert _{\{ a \}}} a^{\dag } . \, a^{\dag } . \, \underline{0}\) – thus yielding a diamond-shaped transition system – which would not reflect the fact that the two executed a-actions in \(a^{\dag } . \, a^{\dag } . \, \underline{0}\) cannot be undone in any order as the first one causes the second one. \(\blacksquare \)
Example 3
The proved labeled transition system underlying the initial process \((a \, . \, \underline{0}\mathop {\Vert _{\emptyset }} a \, . \, \underline{0}) \mathop {\Vert _{\{ a \}}} (a \, . \, \underline{0}\mathop {\Vert _{\emptyset }} a \, . \, \underline{0})\), which is the synchronization of autoconcurrency with itself, has the following four maximal transition sequences:
While the target processes of the first (resp. last) two sequences are equal, the target process of the first two sequences is different from the one of the last two sequences due to the different additional decorations of the pairs of synchronizing executed actions. This results in a double-diamond-shaped transition system like the one of \((a \, . \, \underline{0}\mathop {\Vert _{\emptyset }} a \, . \, \underline{0}) + (a \, . \, \underline{0}\mathop {\Vert _{\emptyset }} a \, . \, \underline{0})\). Without those decorations, the four sequences would end up in the same process \((a^{\dag } . \, \underline{0}\mathop {\Vert _{\emptyset }} a^{\dag } . \, \underline{0}) \mathop {\Vert _{\{ a \}}} (a^{\dag } . \, \underline{0}\mathop {\Vert _{\emptyset }} a^{\dag } . \, \underline{0})\), thus yielding a single-diamond-shaped transition system. \(\blacksquare \)
4.3 Forward-Reverse Bisimilarity and Backward Ready Multisets
We now redefine brm-forward-reverse bisimilarity over \(\mathbb {P}\). Unlike stable configuration structures, for processes we can syntactically construct their (finite) backward ready multisets, intended as the multisets of actions occurring in the labels of their incoming transitions. In the following we use \(\oplus \) for multiset union, which adds multiplicities of identical elements, and \(\otimes \) for multiset intersection, which multiplies the multiplicities of those elements. The backward ready multiset of \(P \in \mathbb {P}\) is inductively defined as follows where \(\overline{L} = \mathcal {A}\setminus L\):
The first two clauses stated below are the same as the ones of forward-reverse bisimilarity \(\sim _\textrm{FRB}\) over a single transition relation defined in [8, 9]. Note the use of function \(\textit{act}\) to abstract from operator symbols inside transition labels.
Definition 4
We say that \(P_{1}, P_{2} \in \mathbb {P}\) are brm-forward-reverse bisimilar, written \(P_{1} \sim _\mathrm{FRB:brm} P_{2}\), iff \(P_{1}\) and \(P_{2}\) are related by a brm-forward-reverse bisimulation, i.e., a symmetric relation \(\mathcal {B}\) over \(\mathbb {P}\) such that, whenever \((Q_{1}, Q_{2}) \in \mathcal {B}\), then:
For each \(Q_{1} \, {\mathop {\longrightarrow }\limits ^{\theta _{1}}} \, Q'_{1}\) there exists \(Q_{2} \, {\mathop {\longrightarrow }\limits ^{\theta _{2}}} \, Q'_{2}\) such that \(\textit{act}(\theta _{1}) = \textit{act}(\theta _{2})\) and \((Q'_{1}, Q'_{2}) \in \mathcal {B}\).
For each \(Q'_{1} \, {\mathop {\longrightarrow }\limits ^{\theta _{1}}} \, Q_{1}\) there exists \(Q'_{2} \, {\mathop {\longrightarrow }\limits ^{\theta _{2}}} \, Q_{2}\) such that \(\textit{act}(\theta _{1}) = \textit{act}(\theta _{2})\) and \((Q'_{1}, Q'_{2}) \in \mathcal {B}\).
\(a \, . \, \underline{0}\mathop {\Vert _{\emptyset }} a \, . \, \underline{0}\not \sim _\mathrm{FRB:brm} a \, . \, a \, . \, \underline{0}\) as in the forward bisimulation game they respectively reach \(a^{\dag } . \, \underline{0}\mathop {\Vert _{\emptyset }} a^{\dag } \, . \, \underline{0}\) and \(a^{\dag } . \, a^{\dag } . \, \underline{0}\) after performing two a-transitions, where \(\textit{brm}(a^{\dag } . \, \underline{0}\mathop {\Vert _{\emptyset }} a^{\dag } \, . \, \underline{0}) = \{ \! | \,a, a \, | \! \}\ne \{ \! | \,a \, | \! \}= \textit{brm}(a^{\dag } . \, a^{\dag } . \, \underline{0})\). Likewise, \((a \, . \, \underline{0}\mathop {\Vert _{\emptyset }} a \, . \, \underline{0}) \mathop {\Vert _{\{ a \}}} a \, . \, a \, . \, \underline{0}\not \sim _\mathrm{FRB:brm} (a \, . \, \underline{0}\mathop {\Vert _{\emptyset }} a \, . \, \underline{0})\). In contrast, \((a \, . \, \underline{0}\mathop {\Vert _{\emptyset }} a \, . \, \underline{0}) \mathop {\Vert _{\{ a \}}} (a \, . \, \underline{0}\mathop {\Vert _{\emptyset }} a \, . \, \underline{0}) \sim _\mathrm{FRB:brm} (a \, . \, \underline{0}\mathop {\Vert _{\emptyset }} a \, . \, \underline{0}) + (a \, . \, \underline{0}\mathop {\Vert _{\emptyset }} a \, . \, \underline{0}) \sim _\mathrm{FRB:brm} a \, . \, \underline{0}\mathop {\Vert _{\emptyset }} a \, . \, \underline{0}\). \(\blacksquare \)
An axiomatization of \(\sim _\mathrm{FRB:brm}\) can be derived from the one of \(\sim _\textrm{FRB}\) in [8] by using backward ready multisets instead of backward ready sets when extending action prefixes at process encoding time. We conclude this section by developing a modal logic characterization for \(\sim _\mathrm{FRB:brm}\) inspired by the one of \(\sim _\textrm{FRB}\) in [7].
The set \(\mathcal {L}_\textrm{BRM}\) of formulas of the backward ready multiset logic is generated by the following syntax:
where \(M : \mathcal {A}\rightarrow \mathbb {N}\) and \(a \in \mathcal {A}\). The satisfaction relation \(\models \, \subseteq \mathbb {P}\times \mathcal {L}_\textrm{BRM}\) is defined by induction on the syntactical structure of \(\phi \in \mathcal {L}_\textrm{BRM}\) as follows:
$${\begin{array}{rclcl} P & \models & \textsf{true}& \\ P & \models & M & \, \text {iff} \, & \textit{brm}(P) = M \\ P & \models & \lnot \phi ' & \text {iff} & P \not \models \phi ' \\ P & \models & \phi _{1} \wedge \phi _{2} & \text {iff} & P \models \phi _{1} \text { and } P \models \phi _{2} \\ P & \models & \langle a \rangle \phi ' & \text {iff} & \text {there exists } P \, {\mathop {\longrightarrow }\limits ^{\theta }} \, P' \text { such that } \textit{act}(\theta ) = a \text { and } P' \models \phi ' \\ P & \models & \langle a^\dag \rangle \phi ' & \text {iff} & \text {there exists } P' \, {\mathop {\longrightarrow }\limits ^{\theta }} \, P \text { such that } \textit{act}(\theta ) = a \text { and } P' \models \phi ' \\ \end{array}}$$
Note that every \(P \in \mathbb {P}\) is image finite, i.e., it has finitely many outgoing (and incoming) transitions labeled with proof terms containing the same action.
4.4 Denotational Semantics on Stable Configuration Structures
To enable a comparison between hereditary history-preserving bisimilarity over stable configuration structures and brm-forward-reverse bisimilarity over processes, we proceed with the introduction of a denotational semantics for \(\mathbb {P}\) based on stable configuration structures. The first step consists of redefining the process operators of Section 4.1 over stable configuration structures. Taking inspiration from [11], we do this by using proof terms in \(\varTheta \) to formalize events:
The terminated stable configuration structure \(\textsf {N}\) is defined as \((\emptyset , \{ \emptyset \}, \mathcal {A}, \emptyset )\).
Let \(a \in \mathcal {A}\) and \({{{\textsf {\textit{C}}}}} = (\mathcal {E}, \mathcal {C}, \mathcal {A}, l)\) be a stable configuration structure such that \(\mathcal {E}\subseteq \varTheta \). The action prefix \(a \, . \, {{{\textsf {\textit{C}}}}}\) is defined as \((\mathcal {E}', \mathcal {C}', \mathcal {A}, l')\) where:
\(l' \, = \, \{ (a, a) \} \cup \{ (._{a} \theta , \textit{act}(._{a} \theta )) \mid \exists X \in \mathcal {C}.\theta \in X \}\).
Let \({{{\textsf {\textit{C}}}}}_{i} = (\mathcal {E}_{i}, \mathcal {C}_{i}, \mathcal {A}, l_{i})\) be a stable configuration structure such that \(\mathcal {E}_{i} \subseteq \varTheta \) for \(i \in \{ 1, 2 \}\). The alternative composition \({{{\textsf {\textit{C}}}}}_{1} + {{{\textsf {\textit{C}}}}}_{2}\) is defined as \((\mathcal {E}, \mathcal {C}, \mathcal {A}, l)\) where:
.
.
.
Let \({{{\textsf {\textit{C}}}}}_{i} = (\mathcal {E}_{i}, \mathcal {C}_{i}, \mathcal {A}, l_{i})\) be a stable configuration structure such that \(\mathcal {E}_{i} \subseteq \varTheta \) for \(i \in \{ 1, 2 \}\) and \(L \subseteq \mathcal {A}\setminus \{ \tau \}\). The parallel composition \({{{\textsf {\textit{C}}}}}_{1} \mathop {\Vert _{L}} {{{\textsf {\textit{C}}}}}_{2}\) is defined as \((\mathcal {E}, \mathcal {C}, \mathcal {A}, l)\) where:
.
with projections being defined as follows:
\(*\)
.
\(*\)
.
.
Then with each process \(P \in \mathbb {P}\) we denotationally associate a stable configuration structure semantics in a way similar to [3, 35], with the notable difference that we represent events via proof terms. More precisely, each process is given a pair formed by a stable configuration structure, built by using the operators above, and a configuration of that structure. The idea is that all processes reachable from the same initial process share the same configuration structure. In contrast, the designated configuration uniquely identifies the specific process through the proof terms labeling a sequence of proved transitions by means of which the considered process is reached from the initial one.
Note that such a sequence is empty if P is initial – which corresponds to the empty configuration – and unique if P is sequential. In the case that P is neither initial nor sequential, if there are several transition sequences reaching it – meaning that non-synchronizing actions of different parallel subprocesses have been executed – then they result in the same configuration [11], because independent actions can be executed in any order and the order of the elements within a configuration – which is a set – does not matter.
Definition 5
The stable configuration structure semantics of \(P \in \mathbb {P}\) is the pair \(\llbracket P \rrbracket = (\textsf {C}_{P}, X_{P})\) where:
\(\textsf {C}_{P} = \textit{scs}(\textit{to}\_\textit{init}(P))\), with the stable configuration structure \(\textit{scs}(Q)\) associated with an initial process \(Q \in \mathbb {P}\) being defined by induction on the syntactical structure of Q as follows:
\(X_{P} = \emptyset \) if P is initial, otherwise \(X_{P} = \{ \theta _{i} \mid 1 \le i \le n \}\) for some \(n \in \mathbb {N}_{\ge 1}\) such that there exists \(P_{i - 1} \, {\mathop {\longrightarrow }\limits ^{\theta _{i}}} \, P_{i}\) for all \(1 \le ~\hbox {i} \le n\) with \(P_{0} = \textit{to}\_\textit{init}(P)\) and \(P_{n} = P\). \(\blacksquare \)
Example 5
\(\llbracket a \, . \, \underline{0}\mathop {\Vert _{\emptyset }} a \, . \, \underline{0}\rrbracket \) comprises (see Figure 1(a)):
The two events
and
.
The four configurations \(\emptyset \),
,
, and
.
The two maximal computations
.
In contrast, \(\llbracket a \, . \, a \, . \, \underline{0}\rrbracket \) comprises (see Figure 1(b)):
The two events a and \(._{a} a\).
The three configurations \(\emptyset \), \(\{ a \}\), and \(\{ a, ._{a} a \}\).
The only maximal computation \(\emptyset \, {\mathop {\longrightarrow }\limits ^{a}}_{{{{\textsf {\textit{C}}}}}_{a \, . \, a \, . \, \underline{0}}} \, \{ a \} \, {\mathop {\longrightarrow }\limits ^{a}}_{{{{\textsf {\textit{C}}}}}_{a \, . \, a \, . \, \underline{0}}} \, \{ a, ._{a} a \}\).
Therefore, \(\llbracket a \, . \, \underline{0}\mathop {\Vert _{\emptyset }} a \, . \, \underline{0}\rrbracket \not \sim _\textrm{HHPB} \llbracket a \, . \, a \, . \, \underline{0}\rrbracket \) because a causally precedes \(._{a} a\) while
and
are independent of each other and hence no (labeling- and) causality-preserving bijection would relate the former two events to the latter two. \(\blacksquare \)
4.5 Operational Characterization Result
We start by establishing a connection between proved transitions of processes and transitions of stable configuration structures associated with processes.
Lemma 1
Let \(P, P' \in \mathbb {P}\) and \(\theta \in \varTheta \). Then \(P \, {\mathop {\longrightarrow }\limits ^{\theta }} \, P'\) iff \(X_{P} \, {\xrightarrow {\textit{act}(\theta )}}_{\textsf {C}_{P}} \, X_{P'}\). \(\blacksquare \)
We are now in a position of proving our operational characterization result.
5 Relationships between \(\mathcal {L}_\textrm{EI}\) and \(\mathcal {L}_\textrm{BRM}\)
From Theorems 4, 3, and 1 it follows that two processes satisfy the same formulas of \(\mathcal {L}_\textrm{BRM}\) iff their associated stable configuration structures satisfy the same formulas of \(\mathcal {L}_\textrm{EI}\). It is therefore interesting to investigate the relationships between the two logics. On the one hand, we show how to reinterpret \(\mathcal {L}_\textrm{EI}\) over processes (Section 5.1) and \(\mathcal {L}_\textrm{BRM}\) over stable configuration structures (Section 5.2). On the other hand, we discuss how to translate \(\mathcal {L}_\textrm{BRM}\) into \(\mathcal {L}_\textrm{EI}\) (Section 5.3) and vice versa (Section 5.4).
5.1 Reinterpreting \(\mathcal {L}_\textrm{EI}\) over \(\mathbb {P}\)
The only non-trivial case is the one of the binder (x : a). The process analogous of an event in a configuration that is labeled with a certain action is a subprocess starting with an executed occurrence of that action. Indicating with \(\textit{sp}(P)\) the set of all subprocesses of P, let \(\textit{apt}(a^{\dag } . \, P', P)\) be the proof term associated with the execution of action a of the subterm \(a^{\dag } . \, P'\) of P. Formally, \(\textit{apt}(a^{\dag } . \, P', P) = \theta \) iff \(a^{\dag } . \, P' \in \textit{sp}(P)\) and there exist \(P'', P''' \in \mathbb {P}\) such that \(a \, . \, \textit{to}\_\textit{init}(P') \in \textit{sp}(P'')\), \(P'' \, {\mathop {\longrightarrow }\limits ^{\theta }} \, P'''\), \(\textit{act}(\theta ) = a\), and \(a^{\dag } . \, \textit{to}\_\textit{init}(P') \in \textit{sp}(P''')\).
The satisfaction relation \(\models \, \subseteq (\mathbb {P}\times \varTheta ^{\mathcal {I}}) \times \mathcal {L}_\textrm{EI}\) is defined by induction on the syntactical structure of \(\phi \in \mathcal {L}_\textrm{EI}\) as follows:
$${\begin{array}{rclcl} P & \models _{\rho } & \textsf{true}& \\ P & \models _{\rho } & \lnot \phi ' & \, \text {iff} \, & P \not \models _{\rho } \phi ' \\ P & \models _{\rho } & \phi _{1} \wedge \phi _{2} & \text {iff} & P \models _{\rho } \phi _{1} \text { and } P \models _{\rho } \phi _{2} \\ P & \models _{\rho } & \langle x : a \rangle \! \rangle \phi ' & \text {iff} & \text {there is } P \, {\mathop {\longrightarrow }\limits ^{\theta }} \, P' \text { such that } \textit{act}(\theta ) = a \text { and } P' \models _{\rho [x \mapsto \theta ]} \phi ' \\ P & \models _{\rho } & (x : a) \phi ' & \text {iff} & \text {there is } a^{\dag } . \, P' \in \textit{sp}(P) \text { such that } P \models _{\rho [x \mapsto \textit{apt}(a^{\dag } . \, P', P)]} \phi \\ P & \models _{\rho } & \langle \! \langle x \rangle \phi ' & \text {iff} & \text {there is } P' \, {\mathop {\longrightarrow }\limits ^{\theta }} \, P \text { such that } \rho (x) = \theta \text { and } P' \models _{\rho } \phi ' \\ \end{array}}$$
where it is understood that the environment in the subscript of every occurrence of \(\models \) is permissible for the configuration identifying (in the associated denotational semantics) the process on the left – e.g., \(X_{P}\) in the case of process P – and the formula on the right.
To prove that, consequently, \(\mathcal {L}_\textrm{EI}\) reinterpreted over \(\mathbb {P}\) characterizes \(\sim _\mathrm{FRB:brm}\), we follow [33] and hence first show that any substitution of the variables freely occurring in a formula requires a modification of the permissible environment.
Lemma 2
Let \(P \in \mathbb {P}\), \(\phi \in \mathcal {L}_\textrm{EI}\), and \(\rho \in \textit{pe}(X_{P}, \phi )\). Given a substitution \(\sigma \) that – not necessarily injectively – maps \(\textit{fi}(\phi )\) to a set of fresh identifiers that do not occur either free or bound in \(\phi \), let \(\sigma (\phi )\) be the formula obtained from \(\phi \) by replacing each occurrence of \(x \in \textit{fi}(\phi )\) with \(\sigma (x)\) and let \(\rho ^{\sigma } \in \textit{pe}(X_{P}, \sigma (\phi ))\) be the environment obtained from \(\rho \) by replacing each \(x \in \textit{fi}(\phi )\) with \(\sigma (x)\). Then \(P \models _{\rho } \phi \) iff \(P \models _{\rho ^{\sigma }} \sigma (\phi )\). \(\blacksquare \)
Corollary 1
Let \(P_{1}, P_{2} \in \mathbb {P}\). Then \(P_{1} \sim _\mathrm{FRB:brm} P_{2}\) iff \(\exists f_{1, 2} .\forall \phi \in \mathcal {L}_\textrm{EI} .\forall \rho \in \textit{pe}(X_{P_{1}}, \phi ) .P_{1} \models _{\rho } \phi \Longleftrightarrow P_{2} \models _{f_{1, 2} \circ \rho } \phi \) where \(f_{1, 2}\) is a label-preserving bijection from \(X_{P_{1}}\) to \(X_{P_{2}}\). \(\blacksquare \)
5.2 Reinterpreting \(\mathcal {L}_\textrm{BRM}\) over Stable Configuration Structures
Let us denote by \(\llbracket \mathbb {P}\rrbracket \) the set of all stable configuration structures – whose events are proof terms – that turn out to be the denotational semantics of some \(P \in \mathbb {P}\). Recalling that \(\llbracket P \rrbracket = ({{{\textsf {\textit{C}}}}}_{P}, X_{P})\), when writing \(\llbracket P \rrbracket \models \phi \) we mean \(X_{P} \models \phi \).
The satisfaction relation \(\models \, \subseteq \llbracket \mathbb {P}\rrbracket \times \mathcal {L}_\textrm{BRM}\) is defined by induction on the syntactical structure of \(\phi \in \mathcal {L}_\textrm{BRM}\) as follows:
$${\begin{array}{rclcl} \llbracket P \rrbracket & \models & \textsf{true}& \\ \llbracket P \rrbracket & \models & M & \, \text {iff} \, & \{ \! | \,a \in \mathcal {A}\mid X_{P'} \, {\mathop {\longrightarrow }\limits ^{a}}_{{{{\textsf {\textit{C}}}}}_{P'}} \, X_{P} \, | \! \}= M \\ \llbracket P \rrbracket & \models & \lnot \phi ' & \text {iff} & \llbracket P \rrbracket \not \models \phi ' \\ \llbracket P \rrbracket & \models & \phi _{1} \wedge \phi _{2} & \text {iff} & \llbracket P \rrbracket \models \phi _{1} \text { and } \llbracket P \rrbracket \models \phi _{2} \\ \llbracket P \rrbracket & \models & \langle a \rangle \phi ' & \text {iff} & \text {there exists } X_{P} \, {\mathop {\longrightarrow }\limits ^{a}}_{{{{\textsf {\textit{C}}}}}_{P}} \, X_{P'} \text { such that } \llbracket P' \rrbracket \models \phi ' \\ \llbracket P \rrbracket & \models & \langle a^\dag \rangle \phi ' & \text {iff} & \text {there exists } X_{P'} \, {\mathop {\longrightarrow }\limits ^{a}}_{{{{\textsf {\textit{C}}}}}_{P'}} \, X_{P} \text { such that } \llbracket P' \rrbracket \models \phi ' \\ \end{array}}$$
Every process and its associated stable configuration structure satisfy the same formulas of \(\mathcal {L}_\textrm{BRM}\). As a consequence, \(\mathcal {L}_\textrm{BRM}\) reinterpreted over stable configuration structures characterizes \(\sim _\textrm{HHPB}\).
Theorem 6
Let \(P \in \mathbb {P}\). Then \(\forall \phi \in \mathcal {L}_\textrm{BRM} .P \models \phi \Longleftrightarrow \llbracket P \rrbracket \models \phi \). \(\blacksquare \)
5.3 Translating \(\mathcal {L}_\textrm{BRM}\) into \(\mathcal {L}_\textrm{EI}\)
The main difficulty is the encoding of multisets, as they are not present in \(\mathcal {L}_\textrm{EI}\). In the translation function we thus introduce two additional parameters:
The first one is a finite set A of actions, e.g., those occurring in a process P. Since \(P \models M\) iff \(\textit{brm}(P) = M\), the \(\mathcal {L}_\textrm{EI}\) formula corresponding to M has to express the fact that every action in the support of M, i.e., \(\textit{supp}(M) = \{ a \in \mathcal {A}\mid M(a) > 0 \}\), can be undone a number of times equal to its multiplicity, while any action in \(A \setminus \textit{supp}(M)\) cannot be undone at all. We assume that \(\textit{supp}(M)\) is finite to avoid infinite conjunctions in the translation.
The second one is a finite sequence \(\varrho _{n}: \{ 1, \dots , n \} \rightarrow \mathcal {I}\times \mathcal {A}\) of pairs each formed by an identifier and an action. It acts like a stack-based memory that keeps track of executed actions, bound to variables via \(\langle x : a \rangle \! \rangle \) and (x : a).
The translation function \(\mathcal {T}_\textrm{BE} : \mathcal {L}_\textrm{BRM} \times \mathcal {P}_\textrm{fin}(\mathcal {A}) \times \{ \varrho _{n} \mid n \in \mathbb {N}_{\ge 1} \} \rightarrow \mathcal {L}_\textrm{EI}\) is defined by induction on the syntactical structure of \(\phi \in \mathcal {L}_\textrm{BRM}\) as follows:
where in the translation of M the finite sequence \(\varrho _{n}\) is such that:
\((x_{i, k}, a_{i}) \in \textit{rge}(\varrho _{n})\), with \(x_{i, k} \ne x_{i, k'}\) for \(k \ne k'\) and all the identifiers \(x_{i, k}\) being taken starting from the end of \(\varrho _{n}\), i.e., the top of the stack.
\(\sharp (a_{i}, \varrho _{n})\) is the number of occurrences of \(a_{i}\) in \(\varrho _{n}\).
\((z_{i, h}, a_{i}) \in \textit{rge}(\varrho _{n})\), with \(z_{i, h} \notin \{ x_{i, k} \mid 1 \le k \le M(a_{i}) \}\) and \(z_{i, h} \ne z_{i, h'}\) for \(h \ne h'\).
Theorem 7
Let \(P \in \mathbb {P}\), \(\phi \in \mathcal {L}_\textrm{BRM}\), and \(\textit{act}(P)\) be the set of actions in P. Then \(P \models \phi \) iff \(\exists \varrho _{n} .\exists \rho \in \textit{pe}(P, \mathcal {T}_\textrm{BE}(\phi , \textit{act}(P), \varrho _{n})) .P \models _{\rho } \mathcal {T}_\textrm{BE}(\phi , \textit{act}(P), \varrho _{n})\). \(\blacksquare \)
5.4 Translating \(\mathcal {L}_\textrm{EI}\) into \(\mathcal {L}_\textrm{BRM}\)
The challenge is the encoding of formulas of the form \((x : a) \phi \), because identifiers are not present in \(\mathcal {L}_\textrm{BRM}\) and the satisfaction of these formulas is not necessarily related to actions to be done or undone in this moment. Rather, it is generically related to executed actions. On the other hand, it is not clear how multisets would come into play. The study of this translation is left for future work.
6 Conclusions
In this paper we have proposed an entirely new approach to characterize hereditary history-preserving bisimilarity, both denotationally and operationally, even in the presence of autoconcurrency, autocausation, and autoconflict. Unlike [3], the focus is on counting identically labeled events rather than uniquely identifying them, thus avoiding bijections between events altogether. Moreover, on the operational side, it has turned out that proof terms naturally lend themselves to identification purposes; in a reversible setting like ours, they have been used for the first time in [1]. Finally, we have logically characterized backward-ready-multiset forward-reverse bisimilarity with backward ready multiset logic and investigated the relationships of the latter with event identifier logic [33].
The operational characterization is particularly important for several reasons. Firstly, in addition to the equational characterization over forward-only processes developed in [21], hereditary history-preserving bisimilarity can be axiomatized over reversible processes by resorting to the approach of [18] as applied in [8], provided that backward ready multisets are considered in place of backward ready sets. Secondly, in addition to the logics of [4, 33], hereditary history-preserving bisimilarity can be characterized also in terms of backward ready multiset logic. The latter is simpler as it does not make use of variables and binders, but the former contain fragments that have been proven to characterize various behavioral equivalences in the true concurrency spectrum [19, 23, 32].
As for future work, we would like to complete the investigation of the relationships between backward ready multiset logic and event identifier logic, as well as to extend it to the logic of [4]. Another direction to pursue is whether our results apply to configuration structures that are not stable, i.e., in which it is not necessarily the case that causality among events can be always represented in terms of partial orders, possibly defined locally to each configuration. Hereditary history-preserving bisimilarity has been defined over non-stable models in [5, 22] and a logical characterization for it has been provided in [5], which is a conservative extension of the one in [4].
Finally, we plan to study backward-ready-multiset forward-reverse bisimilarity checking by taking into account, as far as hereditary history-preserving bisimilarity is concerned, the undecidability result over finite labeled transition systems extended with an independence relation between transitions of [26] and the polynomial-time algorithm over basic parallel processes of [20].
Acknowledgments
We are grateful to Rob van Glabbeek for bringing to our attention the process examined in Example 2 as well as the anonymous reviewers for their comments and suggestions. This research has been supported by the PRIN 2020 project NiRvAna – Noninterference and Reversibility Analysis in Private Blockchains, the PRIN 2022 project DeKLA – Developing Kleene Logics and Their Applications, and the INdAM-GNCS 2024 project MARVEL – Modelli Composizionali per l’Analisi di Sistemi Reversibili Distribuiti.
Open Access This chapter is licensed under the terms of the Creative Commons Attribution 4.0 International License (http://creativecommons.org/licenses/by/4.0/), which permits use, sharing, adaptation, distribution and reproduction in any medium or format, as long as you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons license and indicate if changes were made.
The images or other third party material in this chapter are included in the chapter's Creative Commons license, unless indicated otherwise in a credit line to the material. If material is not included in the chapter's Creative Commons license and your intended use is not permitted by statutory regulation or exceeds the permitted use, you will need to obtain permission directly from the copyright holder.
and
, that can be executed in any order.
,
, and
. However, they are not hereditary history-preserving bisimilar because, with respect to the last pair, there is no (labeling- and) causality-preserving bijection that maps the two independent events
and
to the two causally-related events a and .a.
or
being placed at the beginning of the proof term. In the third rule (Syn), both subprocesses synchronize on an action in L and the resulting proof term contains both individual proof terms. If \(L = \emptyset \) or \(L = \mathcal {A}\setminus \{ \tau \}\), then the two subprocesses are fully independent or fully synchronized, respectively, on observable actions.
.
.
.
.
with projections being defined as follows:
.
.
.
and
.
,
, and
.
.
and
are independent of each other and hence no (labeling- and) causality-preserving bijection would relate the former two events to the latter two. \(\blacksquare \)
