key: cord-0047281-xjgrl97q authors: Melgratti, Hernán; Mezzina, Claudio Antares; Phillips, Iain; Pinna, G. Michele; Ulidowski, Irek title: Reversible Occurrence Nets and Causal Reversible Prime Event Structures date: 2020-06-17 journal: Reversible Computation DOI: 10.1007/978-3-030-52482-1_2 sha: 37667eeae3bc1439cfe300a0397c73b26c80bb59 doc_id: 47281 cord_uid: xjgrl97q One of the well-known results in concurrency theory concerns the relationship between event structures and occurrence nets: an occurrence net can be associated with a prime event structure, and vice versa. More generally, the relationships between various forms of event structures and suitable forms of nets have been long established. Good examples are the close relationship between inhibitor event structures and inhibitor occurrence nets, or between asymmetric event structures and asymmetric occurrence nets. Several forms of event structures suited for the modelling of reversible computation have recently been developed; also a method for reversing occurrence nets has been proposed. This paper bridges the gap between reversible event structures and reversible nets. We introduce the notion of reversible occurrence net, which is a generalisation of the notion of reversible unfolding. We show that reversible occurrence nets correspond precisely to a subclass of reversible prime event structures, the causal reversible prime event structures. Event structures and nets are closely related. Since the seminal papers by Nielsen, Plotkin and Winskel [21] and Winskel [29] , the relationship among nets and event structures has been considered as a pivotal characteristic of concurrent systems. The ingredients of an event structure are a set of events and a number of relations that are used to express which events can be part of a configuration (the snapshot of a concurrent system), modelling a consistency predicate, and how events can be added to reach another configuration, modelling the dependencies among the events. On the net side, the ingredients boil down to constraints on how transitions may be executed, and usually have a structural flavour. Since the introduction of event structures there has been a flourish of investigations into the possible relations among events, giving rise to a number of different definitions of event structures. We first mention the classical prime event structures [29] where the dependency between events, called causality, is given by a partial order and the consistency is determined by a conflict relation. Flow event structures [6] drop the requirement that the dependency should be a partial order, and bundle event structures [18] are able to represent OR-causality by allowing each event to be caused by a member of a bundle of events. Asymmetric event structures [3] introduce the notion of weak causality that can model asymmetric conflicts. Inhibitor event structures [2] are able to faithfully capture the dependencies among events which arise in the presence of read and inhibitor arcs. In [4] event structures, where the causality relation may be circular, are investigated, and in [1] the notion of dynamic causality is considered. Finally, we mention the quite general approach presented in [27] , where there is a unique relation, akin to a deduction relation. To each of the aforementioned event structures a particular class of nets corresponds. To prime event structures we have occurrence nets, to flow event structures we have flow nets, to bundle event structures we have unravel nets [7] , to asymmetric and inhibitor event structures we have contextual nets [2, 3] , to event structures with circular causality we have lending nets [4] , to those with dynamic causality we have inhibitor unravel nets [8] and finally to the ones presented in [27] 1-occurrence nets are associated. Recently a new type of event structure tailored to model reversible computation has been proposed [24, 26] . In particular, in [24] , reversible prime event structures have been introduced. In this kind of event structure two relations are added: the reverse causality relation and the prevention relation. The first one is a standard dependency relation: in order to reverse an event some other events must be present. The second relation, on the contrary, identifies those events whose presence prevents the event being reversed. This kind of event structure is able to model both causal-consistent reversibility [9, 15, 23] and out-of-causal-order reversibility [13, 25] . Causal-consistent reversibility relates reversibility with causality: an event can be undone provided that all of its effects have been undone first. This allows the system to get back to a past state, which was possible to reach by just the normal (forward) computation. This notion of reversibility is natural in reliable distributed systems since when an error occurs the system tries to go back to a past consistent state. Examples of application of causal-consistent reversibility to model reliable systems include transactions [10, 14] and rollback protocols [28] . Also, there are applications in program analysis and debugging [12, 17] . The out-of-causal-order reversibility does not preserve causes, and this feature makes it suitable to model biochemical reactions where, for example, a bond can be undone 'out-of-order' thus leading to a new state that was not present before. Reversibility in Petri nets has been studied in [19, 22] with two different approaches. In [22] reversibility in an acyclic Petri net is obtained by adding a new kind of tokens, called bonds, that keep track of the execution history. Bonds are rich enough to permit modelling of both the causal-consistent and out-ofcausal order reversibility. In [19] a notion of unfolding of a P/T (place/transition) net, where all the transitions can be reversed, has been proposed. By resorting to standard notions of the Petri net theory [19] provides a causal-consistent reversible semantics for P/T nets. This exploits the well-known unfolding of P/T nets into occurrence nets [29] , and is done by adding for each transition its reversible counterpart. We also note that a problem of making a Petri net reversible (meaning every computation is able to reach back to the initial state) has been solved by showing how to add a minimal number of additional transitions [5] . In this paper we study what kind of nets can be associated with reversible prime event structures. To this aim we introduce reversible occurrence nets, which are occurrence nets enriched with additional transitions (called reversing transitions) that undo the effects of executing the ordinary transitions. Each reversing transition (event in the occurrence net dialect) is associated with a unique transition that produces the effects that the reversing transition undoes. A reversing event associated with an event e can be executed in a reversible occurrence net only when all the events caused by e have been previously reversed. If this is not possible then the reversing event cannot be executed. This means that some events in a reversible event structure may prevent the occurrence of a reversing event. A reversible occurrence net where the reversing events have been removed is just an occurrence net. This discussion suggests a natural way of relating reversible occurrence nets and reversible prime event structures: the causality relation is the one induced by the occurrence net while the prevention relation is induced by the inverse of causality: a reversing event associated with e is prevented by any event that causally depends on e. In this way we associate a reversible occurrence net with a causal reversible prime event structure [24, 26] , which is a subclass of reversible prime event structures. We also show how to obtain a reversible occurrence net from a causal reversible prime event structure. The ingredients that are used are just the causality relation and the set of reversible events. We prove that the two formalisms have the same configurations. Hence, this gives us the precise correspondence between causal reversible prime event structures and reversible occurrence nets. We do not consider non-causal reversible prime event structures here; however, we hint at how this can be done in Sect. 5. Structure of the Paper. Section 2 reviews some preliminary notions for nets and event structures, including reversible prime event structures. Section 3 recalls the well-known relationship between prime event structures and occurrence nets. The core of the paper is Sect. 4 where we first introduce reversible occurrence nets and then we show how to obtain a reversible occurrence net from an occurrence net. We then show how to associate a causal reversible prime event structure with a reversible occurrence net, and vice versa. Section 5 concludes the paper. We denote with N the set of natural numbers. Let A be a set, a multiset of A is a function m : A → N. The set of multisets of A is denoted by μA. We assume the usual operations on multisets such as union + and difference −, and k · m stands for the scalar multiplication of m by k, i.e., (k · m)(a) = k · m(a) for all a ∈ A. Furthermore we use the standard set operations like ∩, ∪ or \. Given a set A and a relation < ⊆ A × A, we say that < is an irreflexive partial order whenever it is irreflexive and transitive. We shall write ≤ for the reflexive closure of a partial order <. We review the notion of Petri net along with some auxiliary notions. Given a net N = S, T, F, m and x ∈ S ∪ T , we define the following sets: • x = {y | (y, x) ∈ F } and x • = {y | (x, y) ∈ F }, which can be viewed as multisets. If x ∈ S then • x ∈ μT and x • ∈ μT ; analogously, if x ∈ T then • x ∈ μS and x • ∈ μS. A multiset of transitions A ∈ μT , called step, is enabled at a marking m ∈ μS, denoted by m [A , whenever A step A enabled at a marking m can fire and its firing produces the marking The firing of A at a marking m is denoted by m [A m . We assume that each transition t of a net N is such that • t = ∅, meaning that no transition may fire spontaneously. Given a generic marking m (not necessarily the initial one), a (step) firing sequence (shortened as fs) of N = S, T, F, m starting at m is defined as: (i) m is a firing sequence (of length 0), and (ii) if m [A 1 m 1 · · · m n−1 [A n m n is a firing sequence and m n [A m , then also m [A 1 m 1 · · · m n−1 [A n m n [A m is a firing sequence. Let us note that each step A such that |A| = n can be written as we denote with start(σ) the marking m, with lead (σ) the marking m n and with tail (σ) the fs σ [A n m n . tail (σ) is defined only when σ has length greater than 0. Given a net N = S, T, F, m , a marking m is reachable iff there exists an fs σ ∈ R N m such that lead (σ) is m. The set of reachable markings of N is A i for the multiset of transitions associated to fs. We call X σ a state of the net and write St(N ) = {X σ ∈ μT | σ ∈ R N m } for the set of states of N . In this paper we consider safe nets N = S, T, F, m where each transition can be fired, i.e. ∀t ∈ T ∃m ∈ M N . m [t , and every place is reachable (i.e., marked in at least one reachable marking). We now recall the notion of prime event structure [29] . Intuitively, e < e models that e can occur only after e, while e # e indicates that e and e are mutually exclusive. Given an event e ∈ E, e denotes the set Given a set X ⊆ E of events, we say that X is conflict free, written CF(X), iff for all e, e ∈ X it holds that e = e ⇒ ¬(e # e ). Given X ⊆ E such that CF(X) and Y ⊆ X, then also CF(Y ). When adding reversibility to peses, conflict heredity may not hold. Therefore, we rely on a weaker form of pes by following the approach in [24] . {e ∈ E | e < e} is finite and conflict free, and -∀e, e ∈ E. if e < e then not e # e . A ppes is a prime event structure in which conflict heredity does not hold, and since every pes is also a ppes the notions and results stated below for ppeses also apply to peses. When a ppes is a pes we shall write Conf pes (P ) instead of Conf ppes (P ), with Conf pes (P ) = Conf ppes (P ) holding. A pes can be obtained from a ppes. The following proposition relates ppes to pes [24] . -if P is a pes, then hc(P ) = P , and -Conf ppes (P ) = Conf pes (hc(P )). We now focus on the notion of reversible prime event structure. The definitions and the results in this subsection are drawn from [24] . In reversible event structures some events are categorised as reversible. In addition to the usual causality and conflict relations, reversible event structures incorporate two new ones that relate events and those representing the actual undoing of the reversible events. The undoing of events is represented by removing them (from a configuration), which is achieved by executing the appropriate reversing events. The ingredients of an rpes partly overlap with those of a pes: there is a causality relation (<) and a conflict one (#) and the two are related by the sustained causation relation . The new ingredients are the prevention relation and the reverse causality relation. The prevention relation states that certain events should be absent when trying to reverse an event, e.g., e u states that e should be absent when reversing u. The reverse causality relation e ≺ u says that u can be executed only when e is present. a and no conflict. Then a b because a < b and b a. P states that b causally depends on a and that c is concurrent w.r.t. both a and b. Note that every event is reversible in P because U = E. As expected, the reverse causality relation ≺ is defined such that every reverse event requires the presence of the corresponding reversible event, i.e., e ≺ e for all e ∈ E. Additionally, it also requires c ≺ a, i.e., a can be reversed only when c is present. The prevention relation states that a cannot be reversed when b is present, i.e., b a. if e e then e ∈ X ∪ A. Reachable configurations are sets of events that can be reached from the empty set by performing events or undoing previously performed events. Definition 10. Let P = (E, U, <, #, ≺, ) be an r pes and let X ⊆ E be a set of events such that CF(X). We say that X is a (reachable) configuration if there exist two sequences of sets A i and B i , for i = 1, . . . , n, such that The set of configurations of P is denoted by Conf rpes (P). As discussed in Sect. 1, rpeses accommodate different flavours of reversibility. Henceforth, we focus on causal-consistent reversibility [9, 16] , which is one of the most common models of reversibility in distributed systems, in which an event can be reversed only when all the events it has caused have already been reversed. In the setting of rpeses we consider these two forms of causal-consistent reversibility. Definition 11. Let P = (E, U, <, #, ≺, ) be an r pes. Then P is causerespecting if for any e, e ∈ E, if e < e then e e . P is causal if for any e ∈ E and u ∈ U the following holds: e ≺ u iff e = u, and e u iff u < e. Example 4. The rpes P in Example 1 is a cause-respecting rpes. However P is not causal because of c ≺ a, which means that c has to be present for a to be reversed even if c does not causally depend on a. If we remove c ≺ a then we obtain a causal rpes. Cause-respecting and causal rpeses enjoy the following useful properties [24] . A particular rôle will be played by the configurations that can be reached without executing any reversible event. Definition 12. Let P = (E, U, <, #, ≺, ) be an r pes and X ∈ Conf rpes (P) be a configuration. X is forwards reachable if there exists a sequence of sets A i ⊆ E, for i = 1, . . . , n, such that X i Ai −→ X i+1 for all i, with X 1 = ∅ and X n+1 = X. The set {b, c} in Example 6 is a reachable configuration which is not forwards reachable. The configurations of a cause-respecting rpes are forwards reachable (see [24] ). Let P = (E, U, <, #, ≺, ) be a cause-respecting r pes, and let X be a configuration of P. Then X is forwards reachable. We review the notion of occurrence nets [21, 29] . Given a net N = S, T, F, m , we write < N for the transitive closure of F , and ≤ N for the reflexive closure of < N . We say N is acyclic if ≤ N is a partial order. For occurrence nets, we adopt the usual convention and refer to places and transitions respectively as conditions and events, and correspondingly use B and E for the sets of conditions and events [29] . We will often confuse conditions with places and events with transitions. An occurrence net ( on) C = B, E, F, c is an acyclic, safe net satisfying the following restrictions: -∀b ∈ B. • b is either empty or a singleton, and ∀b ∈ c. iff ∃y, y ∈ E such that y # 0 y and y ≤ C x and y ≤ C x , is an irreflexive and symmetric relation. The intuition behind occurrence nets is the following: each condition b represents the occurrence of a token, which is produced by the unique event in • b, unless b belongs to the initial marking, and it is used by only one transition (hence if e, e ∈ b • , then e # e ). On an occurrence net C it is natural to define a notion of causality among elements of the net: we say that x is causally dependent on y iff y ≤ C x. Occurrence nets are often the result of the unfolding of a (safe) net. In this perspective an occurrence net is meant to describe precisely the non-sequential semantics of a net (a semantics where concurrency is faithfully represented), and each reachable marking of the occurrence net corresponds to a reachable marking in the net to be unfolded. Here we focus purely on occurrence nets and not on the nets they are unfoldings of. Then X is a configuration of C whenever CF(X) and ∀e ∈ X. e ⊆ X. The set of configurations of the occurrence net C is denoted by Conf on (C). Given an occurrence net C = B, E, F, c and a state X ∈ St(C), it is easy to see that it is conflict free, i.e. ∀e, e ∈ X. e = e ⇒ ¬(e # e ), and left closed, i.e. ∀e ∈ X. {e ∈ E | e ≤ C e} ⊆ X. The following propositions make clear the relations between prime event structures, occurrence nets, states of the occurrence nets and configurations of the prime event structures. Proofs are standard and can be found in papers investigating prime event structures and occurrence nets. Occurrence nets and prime event structures are connected as follows [29] . Example 7. Figure 1 illustrates some (finite) occurrence nets (nets are depicted as usual). We can associate peses to them as follows. The net C 1 has two concurrent events, which are neither causally ordered nor in conflict; hence < and # are empty. The events e 1 and e 2 in C 2 are in conflict, i.e., e 1 # e 2 , while they are causally ordered in C 3 , namely e 1 < e 2 , but not in conflict. Finally, in C 4 we have e 1 < e 3 and e 2 < e 4 and e 1 # e 2 . Additionally, conflict inheritance give us e 1 # e 4 , e 2 # e 3 and e 3 # e 4 . Conversely, every pes can be associated with an occurrence net. With #(A) we denote the set of events A such that ∀e, e ∈ A. e = e ⇒ e # e . is an occurrence net, and Conf pes (P ) = Conf on (E(P )). We now introduce the notion of reversible occurrence nets. A similar notion has been proposed in [19] for adding causal-consistent reversibility to Petri nets by making reversible every event in the unfolding of the net. In this work we deal with a generalised version of reversible occurrence nets in which transitions may be irreversible, i.e., we do not require every transition of a net to be undoable. The intuition behind reversible occurrence nets is the following: we add special transitions (events in the classical occurrence net terminology) to an occurrence net which, when executed, undo the execution of other (standard) transitions. When we remove these special transitions from a reversible causal net we obtain a standard occurrence net. The events in U are the reversing ones and we often say that a reversible occurrence net R is reversible with respect to U . We write E for the set of events E \ U and C E instead of C E\U . The first condition in Definition 15 implies that each reversing event u ∈ U is associated with a unique event e that causes the effects that u is intended to undo; hence e here is a reversible event. Moreover, the second condition ensures that there is an injective mapping h : U → E that associates each event u ∈ U with a different event e ∈ E such that • e = u • and e • = • u, in other words, each reversible event has exactly one reversing event. The third requirement guarantees that all conditions (places) of the net appear at least in the pre or the postset of some event (transition), i.e., there are no isolated conditions. The last condition ensures that the net obtained by deleting all reversing events is an occurrence net. Example 8. We present some reversible occurrence nets in Fig. 2 . The reversing events are drawn in red, and their names are underlined. The events e 1 and e 2 in R 1 are both reversible, while e 1 is the only reversible event in R 2 . In R 3 the events e 1 , e 3 and e 4 are the reversible ones. We prove that the set of reachable markings of a reversible occurrence net is not influenced by performing reversing events. A consequence of the above proposition is the following corollary, which establishes that each marking can be reached by using just forward events. Corollary 1. Let C = B, E, U, F, c be an ron and σ be an fs. Then, there exists an fs σ such that X σ ⊆ E and lead (σ) = lead (σ ). Let R = B, E, U, F, c be an ron, and X ⊆ E be a set of forward events. Then, X is a configuration of R whenever CF(X) and ∀e ∈ X. e ∩ E ⊆ X. The set of configurations of R is usually denoted with Conf ron (R). A configuration of a reversible occurrence net R with respect to U is a subset of E \U ; consequently, the reversing events (i.e., the ones in U ) that may have been executed to reach a particular marking are not considered as part of the configuration. Observe that, differently from occurrence nets, St(R) = Conf ron (R) because the former may contain also reversing events. However, as a consequence of Corollary 1, there is no loss of information. We show how to construct a reversible occurrence net from an occurrence net, once we have identified the events to be reversed. The construction above simply adds as many events (transitions) as those to be reversed. The preset of each added event is the postset of the corresponding event to be reversed, and its postset is defined as the preset of the event to be reversed. The events in U × {r} are the reversing events. Proof. We just have to prove that R(C) is a safe net; the other conditions are satisfied by construction. First we observe that if b ∈ c and • b is not a singleton in R(C) then • b contains at most one event of the form (e, f), and it contains at least one of the form (e , r), and these are originated by the events in b • in C. In the case b ∈ c and • b is not empty, then again • b contains only events of the form (e , r), and these are originated by the events in b • in C. Assume it is not, and assume that b ∈ B is the condition which receives a token when it is already marked. As C is an occurrence net, if the condition is marked then the event e ∈ E such that b ∈ e • has been executed and none of the events e ∈ E such that e ∈ b • (if any) have yet been executed. Thus in R(C) the event (e, f) has been executed and none of the events (e , f) ∈ b • has been executed yet. To be marked again an event of the form (e , r) ∈ • b should have occurred, but this is impossible as none of the events (e , f) ∈ b • have been executed, and among these also (e , f), contradicting the fact that the condition b is marked again. Example 9. Consider the occurrence net C 1 in Fig. 1 , and assume that both events are reversible. The net R 1 in Fig. 2 is R(C 1 ) (after renaming events with the convention that (e, f) is named as e and (e, r) as e). The ron R 3 in Fig. 2 is R(C 4 ), with C 4 in Fig. 1 and the set of reversible events U = {e 1 , e 2 , e 4 }. From ron to r pes: As is usually done for occurrence nets, we now associate each reversible occurrence net with a reversible prime event structure. Given an ron R = B, E, U, F, c , we denote the set of events {e | e < R e } by e . Observe that this set is not necessarily conflict-free. Proof. First of all it is quite clear that (E , <, #) is a ppes (if we close < reflexively we get indeed a pes), as it is obtained by C E . The relation ≺ ⊆ E × U satisfies the requirement that e ≺ e and that {e | e ≺ e} is finite for each e ∈ U as it contains just e. If e ≺ e then not e e as e ∈ e . The sustained causation relation coincides with the relation < and so the conflict relation is inherited along this relation. Furthermore, for e ∈ U , if e < e for some e , then we have that e e, as required. We can then conclude that C r (R) is an rpes. Example 10. Consider the reversible occurrence net R 3 in Fig. 2 . The associated rpes has the events {e 1 , e 2 , e 3 , e 4 } and the reversible events {e 1 , e 3 , e 4 }. The causality relation of the associated ppes is e 1 < e 3 , e 2 < e 4 , the conflict relation is generated by e 1 #e 2 , and it is inherited along , which coincides with <. The reverse causality stipulates that e 1 ≺ e 1 , e 3 ≺ e 3 and e 4 ≺ e 4 and finally e 3 e 1 , as to be allowed to undo e 1 it is necessary to undo e 3 first. The following result states that the rpes associated to a reversible occurrence net is causal, hence cause-respecting. We show that each configuration of an ron is a configuration of the corresponding rpes, and vice versa. Theorem 1. Let R = B, E, U, F, c be a reversible occurrence net with respect to U and C r (R) = (E , U , <, #, ≺, ) be the associated r pes. Then X ⊆ E is a configuration of R iff X is a configuration of C r (R). Proof. As C r (R) is a cause-respecting and causal rpes we have that each configuration is forward reachable, and the forward reachable configurations are precisely those conflict-free and left-closed of the ppes C r (R) = (E , <, #), which correspond to the configurations of the occurrence net R E . We stress that a reversing event in a reversible occurrence net is enabled at a marking when the conditions in the postset of the event to be reversed are marked. This may happen only when all the events that causally depend on the event to be reversed have either been executed and reversed or have not been executed at all. Thus every ron enjoys causally consistent reversibility [9, 15] , and consequently cannot implement the so called out-of-causal order reversibility [13] . In contrast, rpeses are able to model out-of-causal order reversibility (as illustrated in Example 5). Proposition 12 below formalises what are called mixed-reverse transitions in [11] , namely a correspondence between the steps in a reversible occurrence net and the sequences of reachable configurations of the associated rpes. We now introduce some auxiliary notation. Let R = B, E, U, F, c be an ron, and X ⊆ E be a configuration of R, we write mark(X) to denote the marking reached after executing the events in X; this marking can be expressed as (c ∪ X • ) \ • X. Proposition 12. Let R = B, E, U, F, c be a reversible occurrence net and C r (R) = (E , U , <, #, ≺, ) be its associated r pes. Let X ∈ Conf ron (R) and A ⊆ E be a set of events such that mark(X) Proof. By Theorem 1 we know that X ∈ Conf rpes (C r (R)). We have to check that A ∪ B is enabled at X. As mark(X) [A we know that • A ⊆ mark(X), hence A ∩ X should be equal to ∅. Furthermore for any e ∈ A ∩ U , as mark(X) [{e} , we have that h(e) ∈ X (otherwise the conditions enabling e would not have been produced), and then we have that B = {h(e) | e ∈ B} ⊆ X. Finally, as mark(X) [A , we have that CF(X ∪Â) holds. Consider now e ∈Â, and e < e. Clearly e ∈ X \ B. Assume the contrary, then e ∈ B and there exists an e ∈ A ∩ U such that h(e ) = e , but then we have that ¬mark(X) [A . Consider now e ∈ B (which means that e ∈ A ∩ U ) and e ≺ e. As C r (R) is a causal rpes, we know that e = e and e ∈ X \(B \{e}). Take now e ∈ B and e e. This means that e ∈ e which implies that e ∈ X, and also that e ∈Â. By Definition 9 we can conclude that ∪ B is enabled at X. Finally we observe that mark(Y ) = c From rpes to ron: Correspondingly to what is usually done when relating nets to event structures, we show that if we focus on causal rpeses then we can relate them to reversible occurrence nets. The construction is indeed quite standard (see [4, 29] among many others), but we do need a further observation on causal rpes. Proposition 13. Let P = (E, U, <, #, ≺, ) be a causal r pes. Then, # is inherited along <, i.e. e # e < e ⇒ e # e . Proof. In general we have that, given an rpes, (E, , #) is a pes [24] . But in a causal rpes we have that is indeed the transitive closure of <. A consequence of this proposition is that the conflict relation is fully characterized by the causality relation. The same intuition underlying the introduction of reversible occurrence net can be used in associating a net to a causal rpes like the one used to associate an occurrence net to a pes. Definition 18. Let P = (E, U, <, #, ≺, ) be a causal r pes, and ⊥ ∈ E be a new symbol. Define E r (P) as the Petri net B,Ê, F, c where In essence the construction above takes the pes associated to an rpes and constructs the associated occurrence net, which is then enriched with the reversing events (transitions). The result is a reversible occurrence net. Proof. By construction E r (P) E×{f} is a occurrence net. The other requirements can be easily checked. For each (e, r) there exists a unique event (e, f), and if two events share the same preset and postset they are clearly the same event. Each condition b ∈ B is clearly related to an event in E × {f} hence inÊ \ (E × {r}). Proof. Let P = (E, U, <, #, ≺, ). Consider X ∈ Conf rpes (P). As P is a causerespecting and causal rpes we have that X is forward reachable, hence X is a configuration of the ppes (E, <, #), which we denote with P , and then X = {(e, f) | e ∈ X} is a configuration also of the occurrence net associated to this event structure as, by Proposition 1, we have that Conf ppes (P ) = Conf pes (hc(P )). For the converse it is enough to observe that, up to renaming of events, C r (E r (P)) is indeed P. Clearly, if we start from a reversible occurrence net, we get an rpes from which a reversible occurrence net can be obtained having the same states (up to renaming of events). Let R be a ron. Then St(E r (C r (R))) = St(R). Example 11. Consider the rpes with four events {e 1 , e 2 , e 3 , e 4 } such that e 1 < e 3 and e 2 < e 4 , e 1 is in conflict with e 2 and this conflict is inherited along <. Furthermore, let e 1 and e 3 be reversible, and e 3 e 1 . The construction in Definition 18 gives the net below. The constructions we have proposed to associate a reversible occurrence net to a causal reversible prime event structure, and vice versa, are certainly driven by the classical ones (see [29] ) for relating occurrence nets and prime event structures. The consequence of this approach is that the causality relation, either the one given in an rpes or the one induced by the flow relation in the occurrence net obtained ignoring the reversing events, is the one driving the construction. One of the other two relations of an rpes is substantially ignored (and we obtain from a ron a causal rpes where the reverse causality relation just says that an event can be reversed only after it has occurred) whereas the second (prevention) is tightly related to the causality relation: b is caused by a precisely when b prevents undoing of a. The notion of reversible occurrence net we have proposed suggests this construction, so the problem of finding which kind of net would correspond to, for example, a cause-respecting or even an arbitrary rpes remains open and certainly deserves to be investigated. It is however interesting to observe that the construction in Definition 18 gives a reversible occurrence net even when the rpes one started with is not a causal rpes. Consider the rpes with two events {e 1 , e 2 } such that e 1 < e 2 and where the conflict and the prevention relations are empty. The only reversible event is e 1 and e 1 ≺ e 1 . The set {e 2 } is a reachable configuration: we can remove e 1 from a reachable configuration {e 1 , e 2 } by performing the event e 1 . This is an example of out-of-causal order computation. Given this rpes, our construction produces the following ron, which does not have {e 2 } among its configurations. The constructions we have proposed are somehow the more adherent to what is usually done, based on the interpretation that causality implies that the event causing some other event somehow produces something that is used by the latter. This is not the only interpretation of what causality could mean. In fact, causality is often confused with the observation that two causally related events appear ordered in the same way in each possible execution, and when we talk about ordered execution, it should be stressed that this can be achieved in several ways, for instance using inhibitor arcs. Consider the net C: Here the event e 2 can be executed only after the event e 1 has been executed. However, e 1 does not produce a token (resource) that must be used by e 2 . If we simply make the event e 1 reversible but do nothing to prevent reversing of e 1 before e 2 is reversed, then we would obtain the net C . We could do better in C where we model prevention using so-called read arcs [20] . Hence, using inhibitor or read arcs seem feasible ways forward to capture more precisely the new relations of rpeses, including prevention. A similar approach has been already pursued in [8] to model so-called modifiers that are able to change the causality pattern of an event. This suggests that, for arbitrary rpeses, we need to find relations different from the flow relation to capture faithfully (forward and reverse) causal and prevention dependencies. This will be the subject of future research. Dynamic Causality in Event Structures Domain and event structure semantics for Petri nets with read and inhibitor arcs Contextual petri nets, asymmetric event structures and processes Lending petri nets Reversible computation vs. reversibility in petri nets Flow event structures and flow nets Flow unfolding of multi-clock nets Petri nets and dynamic causality for service-oriented computations Reversible communicating systems Transactions in RCCS Reversing steps in petri nets Causal-consistent reversible debugging A calculus for local reversibility Concurrent flexible reversibility Reversibility in the higher-order πcalculus Causal-consistent reversibility Causal-consistent replay debugging for message passing programs Bundle event structures: a non-interleaving semantics for LOTOS Reversing P/T Nets Contextual nets Petri nets, event structures and domains, Part 1 Reversible computation in petri nets Reversing algebraic process calculi Reversibility and asymmetric conflict in event structures A reversible process calculus and the modelling of the ERK signalling pathway Reversing event structures Configuration structures, event structures and petri nets Checkpoint/Rollback vs causally-consistent reversibility Event structures Acknowledgments. The authors would like to thank the reviewers for useful comments and suggestions.