Relating Reversible Petri Nets and Reversible Event Structures, categorically
Hern\'an Melgratti, Claudio Antares Mezzina, G. Michele Pinna
TL;DR
This paper explores the categorical relationships between reversible Petri nets with asymmetric conflicts and reversible event structures, extending causal nets to better model concurrent, distributed, and reversible systems.
Contribution
It introduces a categorical framework for reversible causal nets with asymmetric conflicts and relates them to reversible asymmetric event structures.
Findings
Extended causal nets to include asymmetric conflicts
Established categorical relationships between nets and event structures
Provided a formal foundation for reversible concurrent systems
Abstract
Causal nets (CNs) are Petri nets where causal dependencies are modelled via inhibitor arcs. They play the role of occurrence nets when representing the behaviour of a concurrent and distributed system, even when reversibility is considered. In this paper we extend CNs to account also for asymmetric conflicts and study (i) how this kind of nets, and their reversible versions, can be turned into a category; and (ii) their relation with the categories of reversible asymmetric event structures.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsPetri Nets in System Modeling · Distributed systems and fault tolerance · Access Control and Trust
stix@largesymbols”0E stix@largesymbols”0F
[a]
[b]
[c]
Relating Reversible Petri Nets and Reversible Event Structures,
categorically
Hernán Melgratti\lmcsorcid0000-0003-0760-0618
,
Claudio Antares Mezzina\lmcsorcid0000-0003-1556-2623
and
G. Michele Pinna\lmcsorcid0000-0001-8911-1580
ICC - Universidad de Buenos Aires - Conicet, Argentina
Dipartimento di Scienze Pure e Applicate, Università di Urbino, Italy
Università di Cagliari, Italy
Abstract.
Causal nets (CNs) are Petri nets where causal dependencies are modelled via inhibitor arcs. They play the role of occurrence nets when representing the behaviour of a concurrent and distributed system, even when reversibility is considered. In this paper we extend CNs to account also for asymmetric conflicts and study (i) how this kind of nets, and their reversible versions, can be turned into a category; and (ii) their relation with the categories of reversible asymmetric event structures.
Key words and phrases:
Petri Nets and Event Structures and Concurrency and Categories.
This work has been supported by the Italian MUR PRIN 2020 project NiRvAna, the French ANR project ANR-18-CE25-0007 DCore, the INdAM-GNCS project CUP_E55F22000270001 Proprietà Qualitative e Quantitative di Sistemi Reversibili, and the European Union - NextGenerationEU program Research and Innovation Program PE00000014 SEcurity and RIghts in the CyberSpace (SERICS), projects Secure and TRaceable Identities in Distributed Environments (STRIDE) and Securing softWare frOm first PrincipleS (SWOPS), the EU H2020 RISE programme under the Marie Marie Skłodowska-Curie grant agreement 778233, UBACyT projects 20020170100544BA and 20020170100086BA
1. Introduction
Event structures (eses) [38] are a denotational formalism to describe the behaviour of concurrent systems as a set of event occurences and constraints on such events, regulating how such events can happen. Prime event structures () are the simplest form of event structures. A Prime event structure describes a computational process as a set of events whose occurrence is constrained by two relations: causality and (symmetric) conflicts. A simple pes is depicted in Fig. 1(a), where causality () is drawn with straight lines (to be read from bottom to top) and conflicts () with curly lines. In this case, causally depends on (i.e., ) meaning that cannot occur if does not occur first; additionally, and are in conflict (i.e., ) meaning that and are mutually exclusive and cannot occur in the same execution of the process. The behaviour of a pes can be understood in terms of a transition system defined over configurations (i.e., sets of events), as illustrated in Fig. 1(b). For instance, the transition indicates that the initial state (i.e., no event has been executed yet) may evolve to by concurrently executing and . Neither nor are configurations because cannot occur without ; and and cannot happen in the same run.
In order to accommodate asymmetries that may arise, e.g., in shared-memory concurrency, Asymmetric Event Structures (aeses) relax the notion of conflicts by considering instead weak causality. Intuitively, an event weakly causes the event (written ) if can happen after but cannot happen after . This can be considered as an asymmetric conflict because forbids to take place, but not the other way round. Let us consider the following shared memory scenario:
[TABLE]
in which two variables and are shared among two threads. Let us suppose, for simplicity, that the two variables are initialised to [math]. Assuming strong consistency, the actions of the two threads can be scheduled into two different ways leading to two different final configurations: either and or both variables are equal to . If we represent the behaviour of the above snippet as an event structure, we can identify two relevant events: the assignment of to and the increment of . Let us call such events and . We can observe that if happens then can happen, while if happens, then cannot. And this means that the weakly causes , that is .
However, symmetric conflicts can be recovered by making a pair of conflicting events to weakly cause each other. For instance, the pes in Fig. 1(a) can be rendered as the aes in Fig. 1(c), where weak causality is depicted with red, dashed arrows. Now the conflict between and is represented as and (the additional weak causal dependency is required by consistency with the causality relation). Unsurprisingly, the transition system associated with coincides with that of in Fig. 1(b). Differently, the aes relaxes the conflict between and by making it asymmetric: we keep but drop . Hence, can be added to the configuration but cannot be added to , as rendered in the transition system in Fig. 1(e).
Since their introduction [38], eses have played a central role in the development of denotational semantics for concurrency models; in particular, for Petri nets (pns). It is well-known that different classes of eses correspond to different classes of pns [38, 3, 4]. Moreover, different relations in eses translate into different operational mechanisms of pns. Causality and conflicts are typically modelled in nets via places shared among transitions. However, shared places fall short when translating other kinds of dependencies, such as weak causality, which requires contextual arcs [3].
Reversible computing has been studied in the 70’s for its promise of achieving low-energy computation [15]. Lately [1, 25] is gaining interests for its application in different fields: from modelling bio-chemical reactions, to improve parallel discrete events simulation, to model fault tollerant primitives and finally to debugging. In a model of reversible computation we can distinguish two different flows of computation, i.e., in addition to the description of the standard forward execution, there is a backward flow that expresses the way in which the effects of the forward computation can be undone. If in a sequential setting it is pretty clear what is the backward flow of a computation (i.e. it is the exact inverse of the forward one), and the only challenge is on how to record computational history [14, 40]. In a concurrent setting it is more complicated. Different proposal have arisen in the last years trying to cope with different models: causal-consistent reversibility [7] has been shown to be the right notion to model primitives for fault-handling systems such as transactions [8, 16] or roll-back recovery schemas [36, 26, 37], or to reverse-debug concurrent systems; while out-of-causal order reversibility [32] has been shown as being able to model bio-chemical reactions and compensations. Different models of concurrent computation [1] are available today: RCCS [7], CCSK [33], rho [18], R [6], reversible Petri nets [24], reversible event structures [31], to name a few. As expected, the attention has turned to the question of how these models relate to each other (see e.g. [17, 20, 21, 22, 12]). This work addresses such goal by revisiting, in the context of reversibility, the connection between Event Structures (eses) [38] and Petri Nets (pns) established by Winskel [28].
On the event structure side, we focus on the reversible Asymmetric Event Structures (raeses) introduced in [31], which are a reversible counterpart of Asymmetric Event Structures (aeses) [3], which in turn are a generalisation of Prime Event Structures (peses) [28].
In raeses, the backward flow is described in terms of a set of reversing events, each of them representing the undoing of some event of the forward flow. For the aes in Fig. 1(d), with we indicate that and are reversible, while is not. Two relations, dubbed reverse causation () and prevention (), describe the backward flow and regulate the way in which reversing events occur: prescribes the events required for the undoing while stipulates those that preclude it. The raes in Fig. 1(f) consists of the forward flow defined by extended with a backward flow represented by blue arrows: solid arrows correspond to reverse causation and dashed ones to prevention. Then, says that can be executed (meaning can be undone) only when has occurred (the pair is analogous). The prevention arc states that can be reversed only if has not occurred. The transition system associated with is in Fig. 1(g): transitions corresponding to the forward flow (i.e., the ones in black mimicking those in Fig. 1(e)) add events to configurations; on the contrary, reversing transitions (in blue) remove events from configurations. For instance, the transition accounts for the fact that is reversible and can always be undone. Note that can be reversed both in and but not in since the prevention relation (i.e., ) forbids to be reversed if has already occurred. Interestingly, can be reversed in leading to the configuration , which is not reachable by the forward flow (black arrows). This is known as out-of-causal order reversibility [32].
Reversible eses have introduced further questions about the required features of their operational counterpart, suggesting that shared places are not always a suitable choice ([29, 30, 21]). It has been recently shown that the operational model behind (reversible) peses can be recovered as a subclass of contextual Petri nets, called (reversible) Causal Nets (rcns), in which causality is modelled via inhibitor arc [21] rather than relying on a shared place in which one transition produces a token to be consumed by another one. Inhibitor arcs neither produce nor consume tokens but check for the absence of them. This idea is rendered by the nets in Fig. 2. We recall that a pn gives an operational description of a computation in terms of transitions (depicted as boxes) that consume and produce tokens (bullets) in different places (circles). According to the black arrows in Fig. 2(a), the transition consumes a token from producing a token in ; similarly the transition consumes from , and producing in . Note that and are in mutual exclusion (i.e., conflict) because they both compete for the shared resource (i.e., token) in . The arc connecting to indicates that cannot be fired if does not contains any token; consequently, can happen only after has produced the token in . The causal relation between and arises because of . in Fig. 2(a) is the classical operational counterpart of the es in Fig. 1(a). However, we note that both the causalities and conflicts in can be alternatively represented by using inhibitor arcs instead of shared places, as shown in Fig. 2(b). The inhibitor arc (depicted as a red line ending with a circle) between and models , whereas the inhibitor arcs and represent the symmetric conflict between and . The net in Fig. 2(b) can be made reversible by adding a reversing transition for each reversible event, as shown in Fig. 2(c) (in gray). The added transitions and respectively reverse the effects of and : each of them consumes (produces) the tokens produced (resp., consumed) by the associated forward transition. Inhibitor arcs are also used for modelling reverse causation and prevention as, e.g., the inhibitor arc connecting with stands for .
In this paper we generalise the ideas presented in [21] so to be able to deal with raeses (and not just with the subclass of reversible peses). This is achieved by using inhibitor arcs to represent, not only causal dependencies, but also (symmetric) conflicts. In this way, all the dependencies between transitions are modelled uniformly by using inhibitor arcs. Concretely, we identify a subclass of rcnes, dubbed reversible Asymmetric Causal Nets (racnes), which are the operational counterpart of raeses. We show that the correspondence is tight by following the long tradition of comparing concurrency models in categorical terms [28, 38, 39]. To do so we first turn raeses and racnes into categories by providing suitable notions of morphisms, then we introduce two functors relating these categories and finally we show that the functor that associates raeses to racnes is the left adjoint of the one that that give racnes out of raeses. Besides establishing a correspondence between raeses and racnes, this allows us to reinterpret the results in [21] categorically.
This paper is an extended and enhanced version of [23]. In this presentation, we have refined the concept of morphisms for causal nets, specifically by relaxing the requirements on inhibitor arcs that capture causality when conflicting transitions are collapsed in the morphism’s image. Additionally, we include technical details omitted in the conference paper, and we furnish complete proofs of the results. Additional examples and explanations have been added. Also, Section 5 is completely new. Finally, the whole presentation has been thoroughly refined and improved.
Structure of the paper
This paper is structured as follows: in Section 2 we recall Asymmetric Event Structures and their reversible variants, along with their corresponding categories. In Section 3 Asymmetric Causal Nets, reversible Asymmetric Causal Nets and their categories are presented. The main results about categorical connection are showns in Section 4. Section 5 discusses about some applications of our results. Finally, Section 6 concludes the paper.
2. Reversible Asymmetric Event Structures
In this section we recall the basics of Asymmetric Event Structures (aeses) [3] and their reversible version introduced in [31, 11].
2.1. Asymmetric Event Structures
An aes consists of a set of events and two relations: causality () and weak causality or precedence (). If weakly causes , written , then cannot occur after ; i.e., if both events occur in a computation, then precedes . In this case we say that is in an asymmetric conflict with . Events and are in (symmetric) conflict, written , iff and ; intuitively, they cannot take place in the same computation.
{defi}
An Asymmetric Event Structure (aes) is a triple where
- (1)
is a countable set of events; 2. (2)
is an irreflexive partial order, called causality, defined such that . is finite; and 3. (3)
, called weak causality, is defined such that for all :
- (a)
; 2. (b)
is acyclic; and 3. (c)
if and then .
Each event can be attributed to a finite set of causes, as specified in Condition 2. Moreover, weak causality is consistent with causality: if is a cause of , then is also a weak cause of (as stated in Condition 3a). Additionally, circular dependencies among the causes of an event are precluded by Condition 3b. Finally, (symmetric) conflicts () must be inherited along causality, as required by Condition 3c.
{exa}
Consider the aes depicted in Figure 3(a), where the set of events is , the causality relation is defined such that and , and the weak causality is such that , , and . The set is finite, and hence countable (Condition 1). It is straightforward to check that is an irreflexive partial order and also that each event possesses a finite set of causes (Condition 2), being , , and . Additionally, we have that and ; and also and , in accordance with Condition 3a. It is immediate to check that is acyclic on and (Condition 3b). Moreover, the conflict relation is empty, and hence Condition 3c is trivially satisfied.
In the aes of Fig. 3(b), the causality relation contains just and the weak causality is . In this case induces a symmetric conflict among and and one among and , hence and , and also the inheritance of conflicts along the causality relation is verified (Condition 3c).
In the aes illustrated in Fig. 3(b), the causality relation comprises only , while weak causality is defined by , , , , and . In this case, results in a symmetric conflict between and , as well as one between and . As a result, and , satisfying the inheritance of conflicts along causality (Condition 3c).
{defi}
A configuration of an aes is a set of events such that
- (1)
is well-founded on ; 2. (2)
; and 3. (3)
the set is finite.
The set of configurations of is denoted by .
A configuration comprises a set of events representing a potential partial execution of . Condition 1 ensures that events in are not in conflict, as circular weak-causal dependencies are forbidden. In accordance with Condition 2, contains all the causes of its constituent events: an event may occur only if its causes have already occurred. While a configuration may be infinite, as in a non-terminating execution, each event within a configuration has a finite set of weak causes (Condition 3).
For any pair of sets where , we say that extends if, for all and , there is no weak-causal dependency (). In the context of configurations, if and are configurations, then is considered reachable from .
{exa}
The sets of configurations of the aeses and introduced in Section 2.1 are shown in Figs. 3(c) and 3(d) respectively. The arrows represent the extends relation. Straightforwardly configurations satisfy the conditions in Definition 2.1.
A (finite) configuration of an aes is reachable whenever the events in can be ordered in such a way that for each extends and each .
A morphism between aeses is a (possibly partial) mapping of events that preserves computations (i.e., configurations).
{defi}
Let and be aeses. An aes-morphism, denoted as , is defined as a partial function such that for all
- (1)
if then ; and 2. (2)
if then
- (a)
implies ; and 2. (b)
and imply .
An aes-morphism preserves the causes of each mapped event (Condition 1) and reflects its weak causes (Condition 2a). Additionally, it allows the mapping of two distinct events to the same event only when those events are in conflict (Condition 2b). The aforementioned conditions collectively guarantee that morphisms preserve computations, or configurations, as stated below.
Proposition 1** ([3, Lemma 3.6]).**
Let be an aes-morphism and a configuration of , i.e., . Then, .
Since aes-morphisms compose [3], aeses and aes-morphisms turn into a category, which we denote by .
2.2. Reversible aeses
We now provide a summary of reversible aeses, introduced in [31, 11] as the reversible counterparts ofaeses. Given a set of events and , we write for the undoing of , and for the set of undoings of .
{defi}
A Reversible Asymmetric Event Structure (raes) is a sextuple where is the set of events, is the set of reversible events, and
- (1)
, called weak causality; 2. (2)
, called prevention; 3. (3)
, called causation, is an irreflexive relation defined such that for all , is finite and () is acyclic on ; 4. (4)
, called reverse causation, is defined such that
- (a)
for all ; 2. (b)
for all , is finite and () is acyclic on ; 5. (5)
for all ); and 6. (6)
with is an aes.
An raes is defined in terms of a set of events , with those in being reversible.
Causation () and weak causality () delineate the forward flow, while reverse causation (, depicted as solid blue arrows) and prevention (, represented by dashed blue arrows) describe the backward flow. Weak causality serves the same role as in aeses, wherein asserts that event cannot occur after event . Prevention, on the other hand, governs the undoing of events: indicates that event cannot be undone if event has occurred. Similar to causality in aeses, causation indicates causal dependencies. Consistent with aeses, each event has the finite set of causes , and these sets do not contain cyclic dependencies induced by causation and weak causality (Condition 3). The acyclicity of implies that for all , if , then . Reverse causation specifies the causes for the undoing of each event: states that can be undone only if has occurred. Hence, condition 4a simply states that an event can be undone only if it has occurred. Condition 4b, which is analogous to Condition 3, establishes that each undoing has a finite set of causes. Reverse causation precisely states the causes for undoing each event: asserts that event can be undone only if event has occurred. Therefore, Condition 4a straightforwardly defines that an event can be undone only if it has occurred. Condition 4b, akin to Condition 3, establishes that each undoing has a finite set of causes. Just as causation and weak causality demand consistency, wherein an event cannot have precedence over some of its causes (as defined in Condition 3), a similar requirement is imposed on the backward flow by Condition 5. Specifically, reverse causation must align with prevention: a cause of the undoing of (i.e., ) cannot prevent the undoing, i.e., . The final condition is the most intricate. It’s noteworthy that the definition of raes does not mandate to be an aes, particularly because conflicts may not be inherited along causation. This flexibility is crucial for accommodating out-of-causal-order reversibility (see the example below). Condition 5 considers instead the relation , dubbed sustained causation. The sustained causation is derived by excluding from causation all pairs where event can be undone even when has occurred (i.e., does not hold). It’s worth noting that coincides with when ; thus, indeed constitutes an aes.
{exa}
Consider as depicted in Figure 4(a). The (forward) events are , where is the only reversible one (). Causation is defined such that and , and weak causality states . Reverse causation is such that and , and prevention is . Note that is caused by and , with weakly causing (or being in asymmetric conflict with ). Moreover, can be reversed only when is present and has not been executed. In this case, sustained causation coincides with causation because the only reversible event cannot be reversed if (which causally depends on ) is present. It is routine to check that is an aes, and is an raes.
Consider shown in Fig. 4(b), which has the same set of events, causation, and weak causality as but also takes as reversible (i.e., ). Reverse causation is extended with the pairs , , and . Observe that can be reversed even if the event (which depends on ) has occurred. This is known as out-of-causal-order reversibility. In this case, sustained causation consists only of , i.e., the pair is removed because can be reversed despite (which causally depends on ) having occurred. It can be checked that is an aes, and is an raes.
{rems}
For the sake of the presentation, Section 2.2 deviates in style from the original definition in [31], where causation and reverse causation are merged, and weak causality and prevention are combined in a single relation. Additionally, we explicitly stipulate that must constitute an aes, eliminating the need to restate conditions. Further discussion is available in the Appendix.
The definition of configurations in raeses has an operational flavor grounded in the concept of enabling. Consider as an raes, and let be a set of events such that is acyclic on . For and , we say that is enabled at if , , is acyclic on , and
- (1)
for every , if then and if then ; and 2. (2)
for every , if then and if then .
The first condition ensures that contains all the causes of the events to be added (i.e., those in ) but none of their preventing events. The second condition asserts that includes the reverse causes of the events to be undone (i.e., those in ) but none of the preventing ones. If is enabled at , then can be reached from , denoted as . The initial condition above can be restated as follows: and extends . {defi} Let be an raes and a set of events that is well-founded with respect to . Then, is a (reachable) configuration if there exist two sequences of sets and , for , such that
- (1)
and for all , and 2. (2)
for all , and and .
The set of configurations of is denoted by .
{exa}
The configurations of the raeses in Example 2.2 (along with the steps to reach them) are illustrated in Figures 4(c) and 4(d). Notice that —a configuration of but not of —is reached from the configuration by undoing .
{defi}
Let with be two raeses. An raes-morphism is an aes-morphism such that
- (1)
; 2. (2)
for all , if then ; and 3. (3)
for all and , if then .
Observe that and are not necessarily aeses, but here it is enough that works on causation and weak causality as an aes-morphism. Notice that raes-morphisms preserve the causes (and the reverse causes) of each event (resp., reversing event), and reflect preventions.
Proposition 2**.**
Let be an raes-morphism and let . Then .
Proof 2.1**.**
It suffices to demonstrate that, given such that is acyclic on , if is enabled at (with and ), and (with ), then is enabled at . Observe that since and due to . We now prove that is acyclic on by contradiction. Suppose there exists a sequence of events in such that , with , and . However, as is an aes-morphism, we have for all , and , contradicting the acyclicity of on .
Now consider such that is defined and take such that is defined. As is an aes-morphism, if , then , and if , we have , implying that . Therefore, .
Finally, consider and assume is defined. Take . If is defined, and since , we have that because . Now, consider , which implies because implies and . Hence . Observing that configurations are subsets of events reachable from the empty one, we establish the thesis.
As shown in [11], raes-morphisms compose; hence raeses and raes-morphisms are a category, denoted with . Moreover, is a full and faithful subcategory of .
2.3. Constructions
We conclude the section showing a categorical construction for raes. The category of raeses has coproduct, as shown in [11]. We recall here the construction adapting it to our definition of raes which is equivalent to the one in [31] and [11], as we discuss in the appendix.
Proposition 3**.**
Let and be two raeses. Then where
- •
;
- •
;
- •
* whenever and ;*
- •
* whenever either and or ;*
- •
* whenever and ; and*
- •
* whenever either and or ,*
is their coproduct and defined as are the injections.
Proof 2.2**.**
* is clearly a raes. To show that it is indeed a coproduct, we consider any other raes together with two morphisms . We now show that the mapping defined as is a raes-morphism and it is unique. Clearly as is a raes-morphism, moreover if and are defined and we have two cases: either and then , and is because , or , but in this case by construction we have . Assume now that and are defined and equal. There are two cases: if then and , and if then we have again and which implies . Turning to the reverse part, clearly , and being a raes-morphism, and for the reasoning goes as for , hence , as required. Uniqueness follows from the fact that the events are a coproduct in the category of sets and partial mapping.*
A direct construction of the product in the category of is not available.
3. Reversible Asymmetric Causal Nets
We now introduce Asymmetric Causal Nets as a subclass of nets with inhibitor arcs, wherein standard notions of causality and conflicts among transitions are modelled via inhibitor arcs.
Firstly, we revisit the notion of nets with inhibitor arcs and subsequently introduce asymmetric causal nets along with their reversible versions. We develop appropriate notions of morphisms, turning asymmetric causal nets and reversible asymmetric causal nets into categories.
3.1. Nets with inhibitor arcs
We summarise the basics of Petri net with inhibitor arcs along the lines of [27, 2]. We write for the set of natural numbers. A multiset over a set is a function . We assume the usual operations of union () and difference () on multisets, and write if for all . We will use when enumerating the elements of a multiset. The multiset is defined such that if and otherwise. We often confuse a multiset with the set when . In such cases, denotes , and signifies that implies for all . The underlying set of a multiset , namely the one formed by the elements with , is precisely . Additionally, we will employ standard set operations like , , or . The set of all multisets over is denoted as ; the symbol stands for the unique multiset defined such that .
{defi}
A Petri net with inhibitor arcs (ipt for short) is a tuple , where is a set of places, is a set of transitions such that , is the flow relation, is the inhibiting relation, and is the initial marking.
Given an ipt and , the pre- and postset of are respectively defined as the (multi)sets and . If then and ; analogously, if then and . The inhibitor set of a transition is the (multi)set . The definition of generalise straightforwardly to multisets of transitions.
{exa}
Figure 5 introduces some ipts. The ipt in Figure 5(a) has six places (named ) and three transitions , , and . The initial marking is . For instance, the transition consumes a token from and produces a token in and it is inhibited by , meaning its pre-, post-, and inhibiting sets are , , and , respectively.
A (multiset of) transition(s) is enabled at a marking , written , if , and . Intuitively, is enabled at if contains the tokens to be consumed by () and none of the transitions in is inhibited in (). The last condition avoids cases in which a transition in produces tokens that inhibit other transition in . Observe that the multiset is enabled at every marking. If is enabled at , then it can fire and its firing produces the marking , which is written . Hereafter, we assume that each transition is defined such that , i.e., it cannot fire spontaneously without consuming tokens.
A marking is reachable if there exists a sequence of firings originated in the initial marking and leading to ; stands for the set of reachable markings of . An ipt is safe if every reachable marking is a set, i.e., . From now on, we will only consider safe ipts.
{exa}
Consider the ipt in Figure 5(d). Both and are enabled at marking . On the contrary, is not enabled because it is inhibited by the token in the place . The firing of on produces the marking , i.e. . The transition is enabled at while is disabled and cannot be fired because of the token in . The firing of on produces . The reachable markings of are and .
3.2. Asymmetric Causal Nets
In this section, we introduce Asymmetric Causal Nets, a class of ipts that generalises the concept of Causal Nets introduced in [21] to accommodate asymmetric conflicts. Broadly speaking, we focus on ipts where dependencies between transitions arise solely from inhibitor arcs. Similar to causal nets, the property holds for all transitions and . This means that if a place appears in the preset of a transition, it does not appear in the postset of any transition, and vice versa. Consequently, the flow relation induces an empty causal relation. However, causality can be recovered through inhibitor arcs. Intuitively, a transition connected via an inhibitor arc to some place in the preset of another transition cannot be fired before if we assume that the preset of is marked. This is exemplified by transitions and in Figure 5(d), where can only be fired after . The induced (immediate) causality relation is defined by if and only if , signifying that the firing of consumes (at least) one of the tokens inhibiting the firing of .
Additionally, asymmetric causal nets impose that places should not be shared between the presets and postsets of transitions. Formally, implies for all transitions and . This ensures that the flow relation does not introduce forward or backward conflicts, which need to be recovered from inhibitor arcs. Note that a transition inhibited by some place in the postset of another transition cannot be fired if has been fired, i.e., prevents . This is exemplified by transitions and in Figure 5(b), where cannot be fired after (i.e., is prevented by ). Therefore, the induced prevention relation
is defined by t{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\ \mbox{\reflectbox{\leadsto}}\ }t^{\prime} if and only if . We use {\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\leadsto} to denote the inverse of
. It is important to note that {\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\leadsto} is analogous to the weak causality of aeses: if t^{\prime}\ {\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\leadsto}\ t, then , indicating that cannot be fired if has been fired; however, can be fired after . Similar to AES, symmetric conflicts are retrieved from prevention. That is, transitions and are in symmetric conflict, denoted as , whenever t{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\ \mbox{\reflectbox{\leadsto}}\ }t^{\prime} and t\ {\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\leadsto}\ t^{\prime}.
{defi}
Let be an ipt. is a pre asymmetric causal net (pacn) if the following conditions hold:
- (1)
; 2. (2)
. ; ; and ; 3. (3)
is a partial order; 4. (4)
is finite and ({\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\leadsto}\cup\lessdot) is acyclic on ; and 5. (5)
if then and if then .
The first condition asserts that causal dependencies in a pacn are not established through the flow relation. The second condition stipulates that a place may appear in the preset or postset of at most one transition, and places that are either isolated or part of the presets of all transitions are initially marked.The condition on inhibitor arcs, denoted as , specifies that these arcs should not link transitions to isolated places. This is because their purpose is to represent dependencies between transitions that are associated via the flow relation to those places. Since is meant to model causal dependencies, the third condition requires its transitive closure to form a partial order. The fourth condition mandates that each transition has a finite set of causes, ensuring that is a well-founded partial order. By enforcing the acyclicity of ({\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\leadsto}\cup\lessdot) on the causes of every transition , we ensure that causes of each transition can be ordered to satisfy both causality and prevention. This constraint excludes situations where (i) prevention contradicts causality (e.g., and t^{\prime}{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\leadsto}t), (ii) circular chains of prevention exist (i.e., t_{0}{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\leadsto}t_{1}{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\leadsto}\ldots{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\leadsto}t_{n}{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\leadsto}t_{0}), where symmetric conflicts are a particular case, and (iii) self-blocked transitions occur (i.e., needs to be irreflexive, implying for all transitions ). The last condition simply says that a transition cannot depends on one that prevents it.
{defi}
A pacn is an asymmetric causal net (acn) if
- (1)
for all . implies ; 2. (2)
for all . implies t\ {\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\leadsto}\ t^{\prime}; and 3. (3)
for all , imply .
The additional conditions imposed on acns entails that all dependencies among transitions must be explicitly represented in the structure of the net; in other words, causality is saturated (Condition 1) and that all conflicts must be explicitly represented in the net’s structure, ensuring the presence of inhibitor arcs for all inherited symmetric conflicts (Condition 3). Condition 2 simply states that it then . The inhibitor arc with is somehow superflous, but it follow the intuition that in an aes causality implies weak causality.
{exa}
The ipts depicted in Figure 5 satisfy the conditions of acns. The first two conditions of section 3.2 are met by all four nets, as transitions do not share places in their pre and postsets. Additionally, the places in the presets of all transitions are the only ones initially marked. For (Figure 5(a)), we observe that and , making a total order, and causality is saturated with the inclusion of . Furthermore,
is empty (as no transitions have inhibitor arcs connected to the postset of other transitions), thus satisfying the fourth condition. In the case of the net (Figure 5(b)), the causality relation is empty, while prevention contains the sole pair a{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\ \mbox{\reflectbox{\leadsto}}\ }b: cannot be fired after , but can be executed after . Figure 5(c) presents a similar net where and are in symmetric conflict (), meaning the execution of one prevents the other. Finally, Figure 5(d) illustrates a net where , , and , with conflicts being inherited along the causality relation .
3.3. Configurations of a (pre) Asymmetric Causal Nets
We introduce additional concepts and findings related to (pre) acnes, in line with our previous work in [21].
Given a function , the domain of is defined as . A sequence of elements in is a (possibly partial) mapping defined such that implies for all . Its length, denoted by , is defined as the cardinality of its domain, i.e., . We say that is finite when its length is so (i.e., ). We often write a sequence as where . Note that all elements in a sequence are distinct if the the mapping is injective.
A firing sequence (abbreviated as fs ) of an ipt is a sequence of markings defined such that for each there is a multiset of transitions enabled at and . A fs is written as . Additionally, indicates its initial marking . If is finite, designates its final marking . We say that starts at a marking if , and let denote the set of all firing sequences of the ipt that start at . A marking is reachable in if there exists an fs such that . The set of all reachable markings of is .
{defi}
Let be a pacn. A set of transitions is a configuration of if
- (1)
. (i.e., is left closed with respect to ); and 2. (2)
{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\leadsto}\cup\lessdot is acyclic on .
The set of configurations of a pacn is denoted by .
The conditions imposed in the definition of acn ensure that {\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\leadsto}={\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\ \mbox{\reflectbox{\leadsto}}\ }. In such case, the second condition can be alternatively expressed as .
If , then the transitions of can be partially ordered with respect to \lessdot\cup\ {\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\ \mbox{\reflectbox{\leadsto}}\ }. This means that there exists a sequence of the transitions in such that or t_{i}\ {\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\leadsto}\ t_{j} imply .
Lemma 4**.**
Let be an pacn and let a configuration of . Then can be partially ordered with respect to {\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\leadsto}\cup\lessdot.
Proof 3.1**.**
Take . As is acyclic with respect to {\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\leadsto}\cup\lessdot, then we have that ({\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\leadsto}\cup\lessdot)^{\ast}\cap(X\times X) is a partial order and then we have the thesis.
It is important to note a close correspondence between the configurations of a acn and its reachable markings: any reachable marking corresponds to a configuration of the net, and conversely.
Proposition 5**.**
Let be an pacn. Then,
- (1)
if then ; and 2. (2)
if is a reachable configuration then .
Proof 3.2**.**
- (1)
If , then there exists a firing sequence such that . We prove by induction on the length of the firing sequence that .
- •
Base case* (. Then, and , which is a configuration in .*
- •
Inductive step* (). Then, with . By inductive hypothesis on , . Define . From , we conclude that , because transitions cannot be fired twice in a pacn. Also, for all and , we have that because (otherwise would not be enabled at ). This implies that is left-closed with respect to , i.e., .*
It remains to show that {\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\leadsto}\cup\lessdot is acyclic on . Since is a configuration, its transitions can be partially ordered according to {\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\leadsto}\cup\lessdot. Moreover, , . Hence, implies \neg(t^{\prime}{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\leadsto}t) for all (otherwise, would not be enabled at ). Since is enabled, for all , neither t{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\leadsto}t^{\prime} nor t{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\leadsto}t^{\prime}, because enabled ensures that . Consequently, {\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\leadsto}\cup\lessdot is also acyclic on .
Therefore, we conclude that implies . 2. (2)
Let be a reachable configuration. By Lemma 4, the elements of can be partially ordered. That is, there exists a sequence of the elements of such that or t_{i}\ {\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\leadsto}\ t_{j} imply . We prove by induction on the size of that with is a firing sequence and , and .
- •
Base case* (). Hence, . Then, the firing sequence is empty, with . Moreover, and also .*
- •
Inductive step* (). By inductive hypothesis, there exists a firing sequence such that and . Since is a configuration, . This implies that . Additionally, if t^{\prime}{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\leadsto}t_{k+1} then (otherwise, would not be a configuration). Hence, . Then, we can conclude that is a reachable marking. Moreover, (where the last equality holds because transitions do not share places). Also, implies that because and .*
We emphasize that the previous results remain valid even if the nets are acn, as the inheritance of conflicts along the relation does not play any role in the proofs above.
3.4. Morphisms for (pre) Asymmetric Causal Nets
We introduce a suitable notion of morphisms for pacns, which takes into account that inhibitor arcs correspond to two distinct types of dependencies: causality and prevention. In particular, inhibitor arcs representing prevention demand a specific treatment of markings when compared to classical notions of morphisms for nets [38, 39].
{defi}
Let and be pacns. An acn-morphism is a pair consisting of a relation and a partial function defined such that
- (1)
for all if then
- (a)
and ; 2. (b)
.
- (i)
if then . ; 2. (ii)
if then . . 2. (2)
if then . 3. (3)
implies or ; 4. (4)
.
The initial two conditions adhere to the standard criteria for morphisms between safe nets: the preservation of presets and postsets (Condition 1a), and the reflection of inhibitor arcs (Conditions 1(b)i and 1(b)ii). The inhibitor arcs modeling causality have to be reflected by finding a witness of the causality, whereas those representing preventions have to be reflected in every possible instance. Notably, Condition 1b implies that . Furthermore, only conflicting transitions can be identified, as stipulated by Condition 2.
In contrast to conventional requirements, Condition 3 permits to actively identify places in the preset of different transitions. This might raise concerns, as a place in the target of the morphism could represent different tokens in the source, potentially evolving independently. However, under the constraints of Condition 3, is only allowed to identify places connected to transitions that are in (symmetric) conflict. Moreover, the initial markings corresponds via the relation (Condition 4). It is worth noting that the notion of morphisms remains unaffected by the inheritance of symmetric conflicts along the causality relation, making these conditions applicable to acnes as well.
{exa}
Examine the acns and illustrated in Figure 6. The morphism is defined as follows. For transitions, the mapping is defined by , , and , thereby identifying the conflicting transitions and . The relationship on places is established as expected, specifically for , , and . The inhibitor arc in is reflected by the arc in . It is noteworthy that the mapping does not preserve the remaining arcs of .
The following result is instrumental for the following developments, and ensures that any place in the preset of a transition (in the target of an acn-morphisms) possesses a corresponding pre-image within the morphism.
Lemma 6**.**
Let and be pacns, and an acn-morphism. Then, for all , if , then .
Proof 3.3**.**
By contradiction. Assume . Hence, there does does not exists such that . Hence, ; and consequently, , which contradicts the hypothesis that is an acn-morphism (Section 3.4(4)).
In connection with a previous lemma, it is noteworthy that this property does not hold for transitions, which do not have a guaranteed pre-image. Additionally, places in the postset of transitions that are outside of the image of the morphism, may not necessarily be within the image of the morphism.
Now, our focus is on demonstrating that acn-morphisms preserve the token game; specifically, a firing () in the source net is correspondingly translated to a firing in the target net. It is noteworthy that not every marking is meaningful in a acn. For instance, we anticipate that a marking should not simultaneously contain tokens for both the pre- and postset of the same transition. Similarly, a valid marking is not expected to place tokens in the postset of conflicting transitions. The upcoming definition introduces the concept of markings that are coherent for acns.
{defi}
Given a acn , we say is a coherent marking for if ,
- (1)
for all , iff . 2. (2)
for all , and implies .
Another important consideration is that an acn-morphism may collapse different conflicting transitions in the source into a single transition in the target. In other words, two conflicting transitions and may be mapped to the same transition in the target, denoted as . Consequently, and . Therefore, a coherent marking in the source that includes and corresponds to an execution where the conflict has been resolved–— has been fired, and subsequently, is precluded. When mapping such a marking to the target, the conventional approach in morphisms for Petri nets, applying to the marking, would include both and in the target marking. Since , this would result in a marking that is not coherent for the net in the target of the morphism. Therefore, when mapping a marking, it is imperative to account for conflicts that have already been resolved. Specifically, tokens in the preset of transitions that were in conflict with others that have been fired must be disregarded. This is formally addressed by the next definition, which defines the relevant information of a marking.
The next results establish the correspondence among firing between acns related via a morphism.
{defi}
Let be an acn-morphism, and a coherent marking of . The relevant information of is
Proposition 7**.**
Let be an acn-morphism, and a coherent marking of . Then, implies coherent and .
Proof 3.4**.**
Assume . Since is enabled at , we have (i) , (ii) , and (iii) . Firstly, we show that . Suppose the contrary, i.e., . Since, is a set, then all transitions in are different, otherwise would not be enabled at . Since is an acns, each of its transitions has just one place in its preset; i.e., for all , is a singleton. Consequently, there should be two different transitions whose preset is mapped to the same place, i.e., . Since is a pacn morphism, by Section 3.4(2), which contradicts the assumption that is enabled at . Hence, . From (i), we conclude that . By contradiction, we show that implies . Suppose there is , , and . Hence, there exist and such that , and . But this implies is not enabled at , contradicting (ii). Hence, . Since is a pacn morphism, ; and consequently, .
Secondly, we show that . We proceed by contradiction. Assume that there exist and such that inhibits , i.e., . We have two cases:
- •
: Since , we conclude . Hence, there exists such that and , because inhibitor arcs are reflected by Section 3.4(1(b)i). Since is an acn, there exists exactly one transition such that . There are two cases:
- –
: Hence, we have and , ; which is in contradiction with (ii).
- –
. Since , there should exist such that . Let be the transition such that . Since is an acn-morphism, (Section 3.4(3)). Hence, . Since is a coherent marking, implies . Since and , by definition of relevant information of a marking, we conclude that , which contradicts the assumption .
- •
. Since , then there exist such that . By Section 3.4(1(b)ii), inhibitor arcs are reflected, and hence , which contradicts (ii).
Finally, we show that . If this were not the case, then there would exist such that and . Since is a pacn morphism, there would exists such that and and , which contradicts (iii). Consequently, is enabled at . Moreover, as .
The next results shows that acn-morphisms are closed under composition.
Lemma 8**.**
Let and be two acn-morphisms. Then is a acn-morphism as well.
Proof 3.5**.**
We check the conditions of Section 3.4.
- (1)
Take if then
- (a)
Since and define morphisms, we have that . By analogous reasoning, we deduce that . 2. (b)
Consider .
- (i)
Assume , and . By the definition of , there exists . . Furthermore . Again by definition of , we have again that there is an such that . We can conclude that if and if then we have that there exists , . 2. (ii)
Assume . By the definition of , for all . . Furthermore . Again by definition of , we have that for all we have . We can conclude that if , then for all we have . 2. (2)
Assume . There are two cases:
- •
. Then, because is an acn morphism.
- •
* and . Since, is an acn morphism, . By definition of symmetric conflicts, and . Since pacn are defined such that the postset of every transition is a singleton, we have that and . Since is a pacn-morphism, we have that and , by Section 3.4(1b). Consequently, .* 3. (3)
We check that , either or . Therefore, either there exists a place such that both and belong to , or there are two places and in and and are both in . In the first case or holds as is an acn-morphism; in the second case we have or as is a acn-morphism. Since, conflicts are reflected, also or holds. 4. (4)
Condition straightforwardly follows by the definitions of and that ensure and .
We designate the category of pacns and acn-morphisms as . Within this category, there exists a full and faithful subcategory denoted as , wherein the objects are acns. This subcategory, , is the specific category of interest.
3.4.1. Morphisms and configurations:
We conclude this part by noticing that morphisms preserve configurations, a fact established through the lemma presented below.
Lemma 9**.**
Let be an acn-morphism. Then
- (1)
for all , if then ; and 2. (2)
for all such that , if f_{T}(t_{0}){\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\ \mbox{\reflectbox{\leadsto}}\ }_{1}\ f_{T}(t_{0}^{\prime}) then t_{0}{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\ \mbox{\reflectbox{\leadsto}}\ }_{0}\ t_{0}^{\prime}.
Proof 3.6**.**
- (1)
Take such that . For each we have that either or there exists transitions such that . Since is a acn-morphism, this leads to either a place with , and , or the existence of such that , and . This implies . Thus, the inclusion is established. 2. (2)
Assume f_{T}(t_{0}){\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\ \mbox{\reflectbox{\leadsto}}\ }_{1}\ f_{T}(t_{0}^{\prime}), then and , but then for all we have and there must be an . But then t_{0}{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\ \mbox{\reflectbox{\leadsto}}\ }_{0}\ t_{0}^{\prime}.
Proposition 10**.**
Let be an acn-morphism. If , then .
Proof 3.7**.**
Take . Hence, for every , there exists such that . By Proposition 9 . Then, it follows that . It remains to show that {\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\leadsto}_{1}\cup\lessdot_{1} is acyclic on . We proceed by contradiction. Assume that {\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\leadsto}_{1}\cup\lessdot_{1} has a cycle on . Since both relations are induced by inhibitor arcs, which are reflected by acn-morphisms, this implies that {\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\leadsto}_{0}\cup\lessdot_{0} has a cycle on , which contradicts the assumption that is a configuration. Therefore, {\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\leadsto}_{1}\cup\lessdot_{1} is acyclic on and .
Corollary 11**.**
Let be an acn-morphism and be two acnes. If then .
3.5. Reversible Asymmetric Causal Nets
In this section, we introduce the concept of Reversible Asymmetric Causal Nets, following the approach outlined in [21]. We extend acns by incorporating backward transitions, responsible for undoing or reversing the effects of previously executed forward transitions, i.e., ordinary transitions. We assume that the set of transitions in a net is divided into two sets: for forward transitions and for backward transitions. Furthermore, each backward transition is designed to undo the effect of precisely one forward transition . Nonetheless, there may be forward transitions that are irreversible. For simplicity, we will use to refer to the forward transition and to denote its associated reversing transition, when applicable.
{defi}
An ipt is a reversible Asymmetric Causal Net (racn) if there exists a partition of (where represents the forward transitions, and denotes the backward transitions) satisfying the following conditions:
- (1)
is a pacn net; 2. (2)
such that , , and ; 3. (3)
. is finite and {\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\leadsto} acyclic on ; 4. (4)
if then ; 5. (5)
with being the transitive closure of .
Sometimes we use to represent a racn with the set of backward transitions.
In accordance with Condition 1, the underlying net , encompassing solely the forward transitions of , is a pacn. The insistence on it being a pacn rather than an acn stems from the fact that the conflict relation is not always inherited along , which serves as the causation relationship. This deviation is due to the fact that reversing transitions may allow potentially conflicting transitions to be executed. Condition 2 stipulates that each backward transition unequivocally reverses one and only one forward transition . Consequently, consumes the tokens produced by () and generates the tokens consumed by (). The requirement in Condition 2 signifies that the reversal of (i.e., ) can only occur if has been executed. In other words, a transition can only be reversed if it has been fired. Condition 3 requires a finite set of causes for undoing each transition; in essence, encompasses all the forward transitions that enable the execution of . Condition 4 asserts that if a backward transition causally depends on the forward transition (i.e., ), then cannot be prevented by the same transition (), as otherwise, it would be blocked. Condition 5 introduces the relation , which is analogous to the sustained causation in raes. This relation coincides with causality, except in cases in which a cause can be reversed even after a causally-dependent transition has been fired. Note that conflicts should be inherited along rather than along the relation.
The inhibitor arcs of an racn induce four distinct relations. Two of these pertain to the forward flow, defined on , and correspond to those found in pacns, namely and {\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\leadsto}. Additionally, two relations concern the backward flow. These are reverse causation , characterized by if and only if , and prevention , defined by if and only if .
{exa}
Verifying that the ipt in Figure 7(a) is an racn is straightforward. Note that causally depends on and due to the inhibitor arcs connecting with the presets of and . Moreover, and are in asymmetric conflict: the inhibitor arc linking and indicates that is prevented by . The sole reversible transition is , and its associated undoing causally depends on both and and is prevented by . In other words, the reversal of can only occur after the firing of and , but only if has not taken place.
The net in Figure 7(b) is obtained by eliminating the transition along with the connected inhibitor arcs from . It is immediate that is a acn.
The net in Figure 7(c) by extending with the reversal of , i.e., . If and along with their associated inhibitor arcs are removed from , we obtain the acn depicted in Fig. 7(b).
{exa}
Consider the net in Fig. 6. Note that the removal of the reversing transition does not yield a acn, as the conflict between and is not inherited along . It is noteworthy that the following represents a valid execution of : initiating with , followed by , and then reversing (performing ), enabling the subsequent execution of . The ability to execute after the firing and reversal of would be forbidden if the conflict between and were inherited along .
3.6. Configurations of racnes
We now introduce the concept of configuration for racns. In contrast to the configuration for standard nets, which is typically defined in terms of causality, a configuration of racn is simply required reachable via a firing sequence.
{defi}
Let be a racn. A configuration of is any subset of forward transitions such that there exists a firing sequence with .
{exa}
Consider the net in Fig. 7(c); one of its configuration is , obtained by executing first, followed by , then and subsequently undoing (executing ). This configuration is only reachable by undoing since, given that is a cause of , the presence of is necessary to execute .
3.7. Morphisms for Reversible Asymmetric Causal Nets
The notion of morphisms for racns is given below.
{defi}
Let and be two racns. A racn-morphism is a pair consisting of a relation and a partial function satisfying the following conditions
- (1)
and ; 2. (2)
is an acn-morphism, 3. (3)
if then
- (a)
and ; and 2. (b)
.
- (i)
if , implies . ; and 2. (ii)
if , . .
The first condition stipulates that forward and backward transitions are respectively mapped to forward and backward transitions. According to Condition 2, when considering forward transitions only (i.e., the restriction of to ) we have an acn-morphism on the underlying and (i.e., the nets consisting only of forward transitions). Condition 3a ensures that the transition , responsible for reversing , must be mapped to the transition , which, in turn, reverses . Finally, Condition 3(b)i prevents the merging of inhibitor arcs, meaning that the distinction between various causes that might prevent the reversal of a transition is preserved, whereas Condition 3(b)ii assures that is a prevention is present in the target then all the reverse images of this prevention must be present in the origin. We have to restrict our attention to as we have to consider the relations induced by the inhibitor arcs in this case that are either reverse causation or reverse prevention, and these are defined among forward transitions and backward ones.
{exa}
An racn-morphism for the racns and in Fig. 8 is as follows. Consider the multirelation on places, as detailed in Section 3.4, and define the mapping on transitions such that it mirrors the one in Section 3.4 for forward transitions. On the reversing transition , set . It is evident that . The other conditions are straightforwardly satisfied.
The following two results state that racn-morphisms preserve behaviours and that they are closed under composition.
We first need to specialize the notion of coherent marking for racn. The idea is that we have to focus on forward transitions only. Therefore given a marking of the racn , is coherent if it is coherent in (recall that the places in and are the same). Similarly let be an racn-morphism, and let be a coherent marking of . The relevant information of are the relevant information of the marking in .
Proposition 12**.**
Let be a racn-morphism. Let be a coherent marking of . Then, implies coherent and .
Proof 3.8**.**
We notice that conditions 3a and 3b of Section 3.7 are essentially the same of a acn-morphism, thus without distinguish among reverse transitions and forward ones, we have that a racn-morphism is a acn-morphism. Consequently, the tokens game is preserved.
Lemma 13**.**
Let and be two racn-morphisms. Then is a racn-morphism as well.
Proof 3.9**.**
The proof follows the same lines as the one in Proposition 8.
Therefore, racns and racn-morphisms constitute a category, which is denoted by .
3.7.1. Configurations and morphisms:
We show that morphisms preserve configurations.
Proposition 14**.**
Let be a racn-morphism and a configuration, i.e., . Then, .
Proof 3.10**.**
It is sufficient to observe that configurations in racn are characterized by reachable markings, and racn-morphisms preserve them.
3.8. Constructions
Similarly to what we have done for raes, we have a coproduct also in the category of racn.
Proposition 15**.**
Let and be two racns. Then where
- •
;
- •
;
- •
* whenever and ;*
- •
* whenever either and or ; and*
- •
**
is their coproduct and defined as and are the injections.
Proof 3.11**.**
* is clearly an racn. It remains to prove that is indeed a coproduct in the category . Consider an racn and two morphisms and , we show that there exists a unique morphisms . Define as the relation comprising the pairs if either or and the mapping on transitions equal to if and to if . We check first that this is indeed an racn-morphism. Consider such that is defined. Then we have that if and if and as and are morphisms we have that either or and similarly for or . Consider now and . If and then and if then by construction. The case is the same. Assume now and are both defined and equal. If then and if we have as well as each transition of the first one is prevented by the happening of a transition of the second one and vice versa. Condition 3 of Section 3.4 is proven similarly to the previous one, and the same argument is used to show that fact that . Observing that forward transitions are mapped to forward ones and backward transitions are mapped to backward ones, and if and is defined we have that is defined and as and are morphisms. The racn-morphism is unique as is unique and there is just one satisfying the requirements.*
Also the category does not have products.
4. Relating models
In this section, we explore the interplay between the categories of (reversible) asymmetric causal nets and (reversible) asymmetric event structures. We establish functors and demonstrate the emergence of an adjunction.
We delve into the connection between raeses and racnes. The following definition outlines the process of recovering an raes from the flow and inhibitor arcs of an racn.
As expected, the relations induced by an raes —–namely (causality), {\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\leadsto} (weak causality), (reverse causality), (prevention), and (sustained causation)—play a crucial role in defining the relations of the corresponding raes.
{defi}
Let be an racn, and let , {\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\leadsto}, , and denote the causation, weak causality, reverse causality, prevention and sustained causation induced by and . Then, the corresponding structure is the tuple (\overline{{T}},U,\lessdot,{\lll}\cup{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\leadsto}}, , where represents the reversible events.
The following result ensures that the above construction generates an raes.
Theorem 16**.**
Let be an racn. Then is an raes.
Proof 4.1**.**
We show that the conditions in Section 2.2 are satisfied:
- (1)
Weak causality is set to {\lll}\cup{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\leadsto}}. By definition, both and {\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\leadsto} are relations over . Hence, ({\lll}\cup{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\leadsto}})\subseteq\overline{{T}}\times\overline{{T}}. 2. (2)
Prevention corresponds to , which, by definition satisfies . 3. (3)
Firstly, causation is set to , which, by definition, satisfies . Moreover, since is an racn*, is an acn by Section 3.5(1). Hence, is irreflexive because of Section 3.2(4). By Section 3.2(4), is finite and ({\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\leadsto}\cup\lessdot) is acyclic on . By Section 3.5(5), , hence ({\lll}\cup{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\leadsto}}\cup{\lessdot})=({{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\leadsto}}\cup{\lessdot}). Therefore, ({{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\leadsto}}\cup{\lessdot}) acyclic on implies ({\lll}\cup{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\leadsto}}\cup{\lessdot}) acyclic on .* 4. (4)
Reverse causation is set to , which is by definition .
- (a)
By Section 3.5(2), , . Hence, . 2. (b)
By Section 3.5(3), for all , is finite and {\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\leadsto} acyclic on . Note that . Hence, is finite. It remains to show that {\lll}\cup{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\leadsto}}\cup\lessdot is acyclic on . As in the previous item, ({\lll}\cup{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\leadsto}}\cup\lessdot)=({{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\leadsto}}\cup\lessdot). Hence, we need to show that ({{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\leadsto}}\cup\lessdot) is acyclic on . We know that {\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\leadsto} is acyclic on , and is a partial order since is a racn*. Hence, acyclicity on can only be violated if, for any two , we have t^{\prime}{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\leadsto}t^{\prime\prime} and . However, this implies that and , which contradicts the fact that is an racn.* 5. (5)
for all . ). Note that implies that . Consequently, , indicating that . 6. (6)
We need to show that (\overline{{T}},\prec\!\!\prec,{\lll}\cup{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\leadsto}}) with is an aes. We now check the conditions of Section 2.1. First note that by the definition of .
- (a)
We need to show that is an irreflexive partial order defined such that . is finite. The fact that irreflexive and antisymmetric because and is an irreflexive partial order. Transitivity follows from the definition of (Section 3.5(5)).
* is finite because and is finite (Section 3.2(4)).* 2. (b)
({\lll}\cup{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\leadsto}})\subseteq\overline{{T}}\times\overline{{T}}* by definition. We need to show that for all :*
- (i)
t\lll t^{\prime}\ \Rightarrow\ t\ ({\lll}\cup{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\leadsto}})\ t^{\prime}; which immediately follows because {\lll}\subseteq{(\lll\cup{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\leadsto})}. 2. (ii)
({\lll}\cup{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\leadsto}})\cap(\lfloor t\rfloor_{\prec\!\!\prec}\times\lfloor t\rfloor_{\prec\!\!\prec})* is acyclic. Note that ({\lll}\cup{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\leadsto}})\cap(\lfloor t\rfloor_{\prec\!\!\prec}\times\lfloor t\rfloor_{\prec\!\!\prec})=({\lll}\cup{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\leadsto}})\cap(\lfloor t\rfloor_{\lll}\times\lfloor t\rfloor_{\lll})=(\lfloor t\rfloor_{\lll}\times\lfloor t\rfloor_{\lll})\subseteq(\lfloor t\rfloor_{\lessdot}\times\lfloor t\rfloor_{\lessdot}), which is acyclic because is an acn (Section 3.2(4)).* 3. (iii)
if and then . It follows from Section 3.5(5).
We can conclude that is indeed an raes.
{exa}
Consider the racn Figure 7. The corresponding raes is defined as in Section 2.2. In fact, within , causality is characterized by and due to the conditions and . Moreover, weak causality includes as a consequence of b\ {\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\leadsto}\ a, and also encompasses and induced by the sustained causation, which coincides with . On the other hand, reverse causality encompasses and , while prevention is limited to .
Recall that an racn lacking reversing transitions (i.e., ) is essentially an acn. Consequently, the construction outlined in Section 4 is applicable to acnes as well.
Corollary 17**.**
Let be an acn. Then is an aes.
extends to a functor by observing that an racn-morphism induces an raes-morphism .
Proposition 18**.**
* is a well-defined functor.*
The construction linking a net to an event structure adheres to the conventional intuition, where places represent appropriate subsets of events, and transitions are connected to places based on the relations specified in the event structure. In our context, the event subsets have a cardinality of at most one, meaning they are either the empty set or a singleton. To streamline notation, we will use the symbol to represent the singleton set and, consequently, avoid the use of braces.
{defi}
Let be an raes. Then, the associated net is defined as where
[TABLE]
Events in are mapped to the forward transitions of the net. For each event , two associated places are considered: signifies that the event has not occurred, while indicates its execution. As a result, the preset of the forward transition is , and its postset is . A transition corresponds to the undoing of the forward transition . This transition consumes tokens from and produces them in . The inclusion of the special place serves no operational purpose; its motivation is purely technical. Its significance will become clearer when demonstrating that the mapping extends to a functor, as explained in the subsequent discussion. The inhibitor arcs in model both causality (forward or backward) and precedence (forward or backward). Additionally, all places not appearing in the postset of forward transitions are initially marked.
Theorem 19**.**
If is a raes, then is an racn.
Proof 4.2**.**
Consider the raes and as defined in Section 4. Initially, we show that the net , where and are the restrictions of and to the transitions in , is a pacn. The first three conditions of Section 3.2 follow through a straightforward examination of the definition of . The fourth condition is a consequence of being an raes, satisfying Section 2.2(3), which translates to Condition 4 in Section 3.2. The final condition is implied by the fact that constitutes an aes with .
For each transition in , there is precisely one corresponding transition in , represented by , as dictated by being an raes. Condition 3 in Section 3.5—–asserting that is finite—stems from being finite in an raes. For the same reason, causation and weak causality are acyclic on such sets. Hence, Condition 4 is also satisfied by construction. The condition 5 of Section 3.5 is verified as it mimic the requirement of sustained causality of the raes . The final condition depends again on the analogous one in raes. We can conclude that indeed is an racn.
{exa}
Consider the raes from Section 2.2. The places are , , , , , and . The corresponding transitions are (forward ones) and (reversing ones). The flow arcs adhere to the specifications outlined in Section 4, while the inhibitor arcs are determined by the relations within . The resulting net bears resemblance to the one depicted in Figure 7(c), with distinct place labels and the exclusion of the isolated place .
Corollary 20**.**
If is an aes, then is an acn.
We establish the extension of the mapping to a functor by demonstrating that any raes-morphism induces a racn-morphism .
{defi}
Let be raes-morphism. Assume for . We define as follows:
- (1)
where
[TABLE] 2. (2)
is defined as follows:
[TABLE]
According to Condition (1), the relation is established to associate the place in the source with its counterpart in the target. Additionally, it is linked to all the places in the target, where is not in the image of the morphism . This connection is crucial to guarantee that the definition satisfies the condition regarding the initial markings of acn-morphisms (Section 3.4(4)). Each place in the source, denoted as , which corresponds to the preset of the event , is paired with the place in the target representing the preset of the corresponding event ; denoted as . Similarly, each place in the source, denoted as , indicating the postset of the event , is associated with its counterpart in the target representing the postset of the corresponding event ; designated as . The mapping for transitions is straightforward. A transition representing a forward event is mapped to a transition representing the corresponding event . Reversing transitions are similarly mapped to reversing transitions.
The following result ensures that the construction above actually gives an racn-morphism.
Proposition 21**.**
If is an raes-morphism, then is a well-defined racn-morphism.
Proof 4.3**.**
We verify that constitutes an racn-morphism from to by checking the conditions of Section 3.7. Assume for . By definition of , note that and .
- (1)
By definition of , . Similarly, . 2. (2)
We need to show that is an acn-morphism. Hence, we check the conditions of Section 3.4.
- (a)
for all if then
- (i)
We show that and
[TABLE]
Analogously, . 2. (ii)
Assume now . We distinguish two cases, either or .
In the first case, if we have nothing to prove, thus assume that By Section 4, if , then there are two cases:
- •
* and : Since is an raes-morphism, it is also an aes-morphism. Consequently, it preserves causes (Section 2.1(1)). Therefore, it should hold that . Since , there must be such that . Then, it suffices to consider . It is immediate that because . Moreover, because (Section 4).*
- •
* and . As , we can consider all such that . Since is an raes-morphism, it reflects weak causality (Section 2.1(2a)). Hence, for all such that , we have that . Hence, by Section 4.* 2. (b)
We show that if then . Since is an raes*-morphism, implies , i.e., and . Then, by Section 4, and . Hence, .* 3. (c)
We show that implies or . We proceed by case analysis on the shape of .
- •
* or and . Then, is a singleton by Section 4; hence, the thesis follows vacuously.*
- •
* with for some . Then, there exist such that and and . Since is an raes-morphism, . Therefore, and . By Section 4, both and are in . Hence, . Therefore, .*
- •
* with for some . By reasoning analogously to the previous case, it is shown that .* 4. (d)
We show that . By Section 3.2(2), . By Section 4,
[TABLE]
Consequently,
[TABLE]
By Section 4(1),
[TABLE]
Then,
[TABLE]
Note that the first set on the right-hand-side contains all places with that are in the image of , while the second one contains all places with that are not in the image in of . Hence, they cover all the elements of . Hence,
[TABLE] 3. (3)
We check that . If , then with . Then, the corresponding forward transition is with . If then by Section 4(2).
- (a)
By Section 4(2), . Since , by Section 4. Hence, . 2. (b)
Consider now , we have again to distinguish two cases:
- •
* and . Since is an raes-morphism, by Section 2.2(2), . Consequently, there exists such that . Then, take and note that by Section 4.*
- •
* and . By Section 4, . Since is an raes-morphism , , by Section 2.2(3). Then, , by Section 4.*
Proposition 22**.**
* is a well-defined functor.*
Proposition 23**.**
Let be an raes, then .
Proof 4.4**.**
Consider the and the associated racn as defined in Section 4. Let . We now show that the elements coincides:
- •
: By Section 4, with . By Section 4, .
- •
: By Section 4, . By Section 4, . By substituting and , . Hence, .
- •
: By Section 4, . Recall that iff . By inspecting the definition of and , implies , with and . Hence, .
- •
: By Section 4, . We now show that iff . Assume that . Then, , by Section 4. Hence, . Therefore, . On the contrary, assume . Then, either or . If , then . By Section 4, . In case , we recall that is the transitive closure of . Hence, implies . Therefore, . Then, . By inspecting Section 4, . Since is an raes*, implies (Section 2.1(3a)).*
- •
: Then, . Therefore, implies . Then, . By inspecting Section 4, we conclude that .
- •
: Then, . Therefore, implies . Then, . By inspecting Section 4, we conclude that .
The main result is that there is a precise relation between and , namely the functor is the left adjoint of .
Theorem 24**.**
The functor is the left adjoint of the functor .
Proof 4.5**.**
Let be an raes and the associated racn. By Proposition 23, we have that and we have the obvious identity mapping . To prove the result, we show that for any racn , and any raes-morphism , there exists a unique morphism such that the following diagram commutes.
\mathsf{H}$$\mathcal{E}_{r}(\mathcal{N}_{r}(\mathsf{H}))$$\mathcal{E}_{r}(V)$$g$$id$$\mathcal{E}_{r}(h)
We begin by establishing the existence of the morphism. Let be defined as follows:
[TABLE]
and and if .
We verify that is an racn-morphism from to by checking the conditions of Section 3.7. By definition of , note that and .
- (1)
By definition of , . Since is an raes*-morphism, . Similarly, . Since is an raes-morphism, .* 2. (2)
We need to show that is an acn-morphism. Hence, we check the conditions of Section 3.4.
- (a)
for all if then
- (i)
We show that and
[TABLE]
Analogously, . 2. (ii)
We now check that inhibitor arcs are reflected. Consider now and such that .
- (A)
Case . By Proposition 6, . Hence, there exists such that . Moreover, and . As implies that , i.e., . As is an raes*-morphisms, . Consequently, ;* 2. (B)
Case . For any such that , it should be and . As implies that ; hence . As is an raes*-morphisms, . Consequently, ;* 2. (b)
We show that if then . Note that implies , by the definition of . Since is an raes*-morphism, implies , i.e., and . Then, by Section 4, is defined such that and . Hence, .* 3. (c)
We show that implies or . We proceed by case analysis on (according to the definition of ):
- •
: Hence, is the singleton . Therefore, thesis follows vacuously.
- •
. Then, there exist such that and and . Since is an raes*-morphism, . Therefore, and . By Section 4, both and are in . Hence, . Therefore, .*
- •
. As in the previous case, there exist such that and and . Since is an raes*-morphism, . Therefore, and . By Section 4, both and are in . Hence, . Therefore, .* 4. (d)
We prove that . By Section 4,
[TABLE]
Consequently,
[TABLE]
By the definition of ,
[TABLE]
Note that both multisets on the right-hand-side are actually sets. Moreover, their union covers all places in . Hence,
[TABLE] 3. (3)
. If , then with . Then, the corresponding forward transition is with . If then by the definition of .
- (a)
By the definition of , . 2. (b)
Consider .
- (i)
Case . If then there exists a and . Since, , it implies . Since is a raes*-morphism, . Therefore, * 2. (ii)
Case . Take . Hence, and . Since, , it implies . Since is a raes*-morphism, . Therefore, .*
The uniqueness of the mapping is established by assuming the existence of another . As makes the diagram commutative, we can conclude . Consequently, must be the relation , concluding the proof.
Denoting with and the functors defined as and but acting on objects that are either acnes or aeses, i.e. if we restrict our attentions to the two full and faithful subcategories of and , we have that the same relation the between them exists.
Theorem 25**.**
The functor is the left adjoint of the functor .
5. Applications
Reversible Debugging
One of the successful applications of reversibility is causal-consistent reversible debugging [9, 19]. Reversible debuggers extend the classical ones with the possibility to get back in the execution of a program, so to find the source of a bug in an effective way. Causal-consistent reversible debuggers improve on reversible ones by exploiting causal information while undoing computations. So far this technique has been applied to message passing concurrent systems (e.g., actor-like languages), but not to shared-memory based concurrency. Consider the next code snippet consisting of a two-threaded program that accesses dynamically allocated memory.
1pthread_mutex_t m = PTHREAD_MUTEX_INITIALIZER;
2int *x;
3
4void thread(void *arg)
5{
6 pthread_mutex_lock(&m);
7 if(x != NULL)
8 doSomething(x);
9 pthread_mutex_unlock(&m);
10}
11int main()
12{
13 x= malloc(sizeof(int));
14 pthread_t t;
15 pthread_create(&t, NULL, thread, NULL);
16 pthread_mutex_lock(&m);
17 free(x);
18 pthread_mutex_unlock(&m);
19 return 0;
20}
The behaviour of the program can be thought in terms of events. Take as the event corresponding to the initialisation of at line , for the instruction at line and for the one at line . It is clear that both and causally depend on ( and ); while can happen after , cannot happen after , that is . Moreover, the reversal of a complete execution of the program should ensure that is reversed (i.e., the memory is allocated) before is reversed, hence . Consider instead a version of the program in which is executed outside a critical section (e.g., without acquiring and releasing the lock). In this case, the execution may raise a segmentation fault error. When debugging such a faulty execution, the programmer would observe that the execution violates because happened after . On the hand, an execution can be visualised in terms of events, i.e., the programmer can be provided with a high-level description of the current state of the system (a configuration of the event structure) along with the relevant dependencies. On the other hand, the instrumented execution of the program and of its reversal can be handled by the underlying operational model (i.e., a reversible causal net). Also, one could think of the undoing of an event as a backward breakpoint. That is, one could trigger the undoing of an event from the net and then the debugger will execute all the necessary backward steps in the code, to undo such event. The seamless integration of raes and racn with causal-consistent reversible debuggers can be a nice exploitation of our results, which we will consider in future work.
Another way to exploit our results is to generate directly a reversible semantics for languages for shared memory [5, 13]. In these works, weak memory models are interpreted as event structures. By exploiting our results, we could use to interpret such models and give them a reversible debugging tool in terms of corresponding Petri net. For example, let us consider a simple snippet (taken from [5])
[TABLE]
where is a thread-local variable (e.g., a register) while and are global shared variables, and all the variables are initialised to [math]. The interpretation of such a snippet in terms of event structures is depicted in Figure 9(a), where the assignment of to (event ), causes the first thread to read the value (event ). On the other hand, if the first thread reads the value [math], then the assignment of to happens. The event of the third thread (i.e., the assignment of to ) is independent of the others, hence it has no conflict neither causes. This interpretation works fine when considering just the normal forward flow of computation, but it turns out to be too strict if one wants to reverse debug such a snippet, since sequencing is seen as causation. If we want to reverse debug such a snippet, we could reason as follows: the event can be reversed at any time since it has no causes, neither it is caused by another event. Also, the undoing of should cause the undoing of the event . But then, the undoing of should not cause the undoing of , since the second event is not a consequence of the first one. Hence, the right interpretation for reversible debugging should be the aes depicted in Figure 9(b). Again, we leave as future work the adaptation of the results in [5, 13] for reversible systems.
A speculative scenario
We now show how our framework can be used to model a speculative scenario borrowed from [34]. In this scenario, value speculation is used as a mechanism to boost parallelism by predicting values of data dependencies between tasks. Whenever a value prediction is incorrect, corrective actions must be taken in order to re-execute the data consumer code with the correct data value. In this regard, as shown in [10] for a shared-memory setting, reversible execution can permit to relieve programmers from the burden of properly undoing the actions subsequent to an incorrect prediction. For simplicity, our scenario will involve a producer and a consumer. The producer produces a value on which the consumer has to perform some calculation. Since the production of such a value may require some time, the consumer can try to guess (e.g. speculate) the value and launch a computation on the predicted value. At the end of the computation, the consumer compares the predicted value with the real one, and if it has done a wrong guess then it reverts its computation and redoes the calculation with the actual value. If the guess was right, then nothing has to be reverted. Hence we can model such a scenario with the where:
[TABLE]
The sef of forward events includes the following events: (indicating the production of the value), (indicating that the consumer decided to wait for the real value), (indicating that the consumer predicts the value and hence speculates), (the predicted value coincides with the one generated by the producer) and (the predicted value is wrong). The only reversible events (set ) are and , as the computation has to be reverted just in case of a wrong prediction. The causality relation is as expected: predicting the value causes its comparison with the real one. About conflicts, we have that and . Also we have that the consumer may decide to predict the value and afterwards the producer produces the value. The opposite cannon happen, as it is worthless to speculate if the value has been already generated. Hence, . Reverse causation is as expected. The prevention relation allows for preventing the undoing of the prediction if the prediction was right, hence , and in case the prediction was wrong to revert first the comparison and then the prediction (). The net corresponding to the is depicted in Figure 10, where some inhibitor arcs (those induced by the weak causality of forward events) are omitted.
6. Conclusions
In this paper we complete previous efforts [29, 30, 21] aimed at relating classes of reversible event structures with classes of Petri nets: Firstly, we account for the full class of raeses instead of proper subclasses (being raeses the most general reversible event structures considered in the literature). Secondly, the correspondence is established according to the standard technique of exhibiting a coreflection between suitable categories. Regarding the philosophy behind our nets, it may be asked whether we adhere to the individual token philosophy or the collective token philosophy, as defined in [35]. In the individual token philosophy, each place can be uniquely marked, whereas in the collective token philosophy, there can be multiple ways to place a token in a given place. If we only consider the forward flow of our nets, they adhere to the individual token philosophy. However, asymmetric conflicts suggest that the past of the transition putting a token in a given place may not be unique. Moreover, when considering the reversing flow, things become more complex, particularly with out-of-causal order reversibility, as a forward transition may only be executed because some reversing transition has been executed. To settle this question, it may be necessary to seek a different definition for the individual token philosophy, perhaps by focusing on the forward dependencies of the pre-asymmetric causal net in the racn, rather than considering the entire racn.
Besides the theoretical relevance of establishing a correspondence between these two different models, such connection may be exploited in concrete scenarios as discussed in the previous Section.
Appendix A Appendix
In this appendix we prove that the notions of raes and acn we used are consistent to what is established in literature ([21], [31] and [11])
We start fixing notation and introducing auxiliary definitions concerning nets that will be useful in the following. Given an fs , is the set of all sequences of multisets of transitions that agree with , namely the set , and for the set of multisets of transitions associated to an fs. Each multiset of is a state of the net and write for the set of states of the net , and is an execution of the net.
A.1. Causal Nets and Asymmetric Causal Nets
In [21] we introduced the notion of causal net to show that it was the proper kind of net corresponding to reversible prime event structures of [31]. In that paper we proved that each occurrence nets, the classical counterpart of prime event structures in net terms, could be seen as a causal net. Here we show that each causal net can be seen as an asymmetric causal nets, and this implies that the tight correspondence between causal nets and reversible prime event structures can be transferred to racn. In that paper we did not considered causal nets in categorical terms.
We first recall the definition of causal net from [21].
{defi}
Let be an ipt. is a causal net (cn) if the following conditions are satisfied:
- (1)
; 2. (2)
; 3. (3)
, 4. (4)
. is finite; 5. (5)
is an irreflexive partial order; 6. (6)
; 7. (7)
; and 8. (8)
and .
The requirement that . is finite implies that is finite and is analogous to the requirement that the inverse prevention relation and the causality one are acyclic on .
Proposition 26**.**
Let be a cn and let be the shared places, i.e. . Define be the ipt where
- (1)
; 2. (2)
; 3. (3)
; and 4. (4)
.
Then is an acn and .
Proof A.1**.**
* is a acn as . finite means that is finite and requiring that does not contain conflicting transitions account to prescribe that the reverse prevention and the causality are acyclic on the set of transitions . The other requirements are trivial.*
To show that it is enough to observe that each transition can be executed just once and that, given any marking and any multiset of transitions such that there exists a marking such that . Given a marking , the associated marking is . Now consider such that , we have to show . Clearly and this implies that , now assume that there is a transition such that there exists a place such that . This implies that for all and , hence . It is straightforward to observe that if then . Consider now a marking and a step such that , we show that there exists a marking such that . Consider , the transitions executed to reach that marking are such that for each . . Define where . It is easy to see that if then reasoning as above, and observing that we have that . Observing that all the steps in a cn (and in a acn) are indeed execution of set of transitions and that each transition is fired just once, we can conclude that .
As we have a precise correspondence between reachable markings of a cn and of the associated acn and the states coincide, we can conclude that acnes are a proper generalisation of cns.
A.2. Equivalence of the definitions of raeses
The definition of reversible asymmetric event structure given in [31] and [11] has just two relations which, as we already said, comprises both the forward and the reverse causality and prevention. To avoid confusion we call them standard reversible asymmetric event structures.
{defi}
A standard reversible asymmetric event structures (sraes) is the quadruple where is the set of events and
- (1)
is the set of reversible events; 2. (2)
is an irreflexive causation relation; 3. (3)
is an irreflexive precedence relation such that for all is finite and acyclic with respect to ; 4. (4)
; 5. (5)
for all and , if then not ; and 6. (6)
the relation , defined as when and if , with , then , is such that
- •
implies ;
- •
it is a transitive relation; and
- •
if and then , where .
In this definition comprises the forward causality (which we called causation) and the reverse causality, and comprises the weak causality (forward relation) and the prevention involving the undoing of events. Just observing that the relations on subsets of events reduces always to the part concerning forward relations, and that the last condition of the previous definition can be rewritten just requiring that, when restricted to forward events only, sustained causation and the restriction of the prevention to these events is an aes, it is straightforward to see that the two proposition below hold.
Proposition 27**.**
Let be an sraes, then is an raes, where , , and .
Proposition 28**.**
Let be an raes, then is an sraes.
The proofs of both propositions are trivial and omitted.
The reference list from the paper itself. Each links out to its DOI / PubMed record.
- 1[1] B. Aman, G. Ciobanu, R. Glück, R. Kaarsgaard, J. Kari, M. Kutrib, I. Lanese, C. A. Mezzina, L. Mikulski, R. Nagarajan, I. C. C. Phillips, G. M. Pinna, L. Prigioniero, I. Ulidowski, and G. Vidal. Foundations of reversible computation. In I. Ulidowski, I. Lanese, U. P. Schultz, and C. Ferreira, editors, Reversible Computation: Extending Horizons of Computing - Selected Results of the COST Action IC 1405 , volume 12070 of Lecture Notes in Computer Science , pages 1–40. Springer, 202
- 2[2] P. Baldan, N. Busi, A. Corradini, and G. M. Pinna. Domain and event structure semantics for Petri nets with read and inhibitor arcs. Theor. Comput. Sci. , 323(1-3):129–189, 2004.
- 3[3] P. Baldan, A. Corradini, and U. Montanari. Contextual Petri nets, asymmetric event structures, and processes. Inf. Comput. , 171(1):1–49, 2001.
- 4[4] G. Boudol. Flow event structures and flow nets. In Semantics of Systems of Concurrent Processes, LITP Spring School on Theoretical Computer Science , volume 469 of Lecture Notes in Computer Science , pages 62–95. Springer, 1990.
- 5[5] S. Castellan. Weak memory models using event structures. In J. Signoles, editor, Vingt-septièmes Journées Francophones des Langages Applicatifs (JFLA 2016) , Saint-Malo, France, Jan. 2016.
- 6[6] I. Cristescu, J. Krivine, and D. Varacca. A compositional semantics for the reversible π 𝜋 \pi -calculus. In 28th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS , pages 388–397, 2013.
- 7[7] V. Danos and J. Krivine. Reversible communicating systems. In CONCUR 2004 - Concurrency Theory, 15th International Conference , volume 3170 of Lecture Notes in Computer Science , pages 292–307. Springer, 2004.
- 8[8] V. Danos and J. Krivine. Transactions in RCCS. In CONCUR 2005 , volume 3653 of Lecture Notes in Computer Science , pages 398–412. Springer, 2005.