Event Structures for Resolvable Conflict^{⋆}

Rob van Glabbeek and Gordon Plotkin

Laboratory for Foundations of Computer Science School of Informatics, University of Edinburgh Edinburgh EH9 3JZ, UK

                  rvg@cs.stanford.edu   gdp@inf.ed.ac.uk

Abstract. We propose a generalisation of Winskel’s event structures, matching the expressive power of arbitrary Petri nets. In particular, our event structures capture resolvable conflict, besides disjunctive and conjunctive causality.

1 Introduction

Event structures were introduced in Nielsen, Plotkin & Winskel [8] as abstract representations of the behaviour of safe Petri nets. They describe a concurrent system by means of a set of events, representing action occurrences, and for every two events d and e it is specified whether one of them is a prerequisite for the other, whether they exclude each other, or—the remaining case—whether they may happen concurrently. A formal definition can be found in Fig. 2. The behaviour of an event structure is formalised by associating to it a family of configurations, these being sets of events that occur during (partial) runs of the represented system. A configuration x can also be understood as a state of the represented system, namely the state reached after performing all events in x.

Fig. 1. An event structure as in [8] and its family of configurations, together with a transition relation between the configurations indicating how one can move from one state to another by concurrently performing some events. The same system is also represented by means of a propositional theory [2] and a Petri net.

ab # c  • ab  •c • a ab  c ac b ⇒ a ¬(b ∧ c)

Winskel later proposed a variety of other notions of event structure. In [9, 10] he presented event structures where instead of indicating which events are prerequisites of other events, it is indicated which sets of events X are possible prerequisites of events e, written X ⊢ e. This enables one to model disjunctive causality (cf. Fig. 3), the phenomenon that an event is causally dependent on a disjunction of other events occurring in the same system run. The event struc-

⋆ To appear in: Vaclav Koubek & Jan Kratochvil, editors: Proceedings 29^{th} International Symposium on Mathematical Foundations of Computer Science (MFCS 2004), Prague, Czech Republic, LNCS, Springer, August 2004. \begin{matrix}c \\ ◯ \end{matrix} Springer-Verlag This work was supported by EPSRC under grant number GR/S22097.

The event structures of Nielsen, Plotkin & Winskel are triples E = ^{/} \E, ≤, #^{\} / where – E is a set of events,

– ≤ ⊆ E × E is a partial order, the causality relation,

– # ⊆ E ×E is an irreflexive, symmetric relation, the conflict relation, satisfying the principle of conflict heredity: ∀d, e, f ∈ E. d ≤ e ∧ d#f ⇒ e#f.

The set L(E) of configurations of such a structure consists of those X ⊆ E which are – conflict-free: #^{\}(X × X) = ∅,

– and left-closed: ∀d, e ∈ E. d ≤ e ∈ X ⇒ d ∈ X.

The prime event structures of Winskel [10] are defined likewise, but additionally requiring the principle of finite causes: {d ∈ E | d ≤ e} is finite for all e ∈ E.

The event structures of Winskel [9] are defined as triples E = ^{/} \E, Con, ⊢^{\} / where

– E is a set of events,

– Con ⊆ 𝒫_{fin}(E), satisfying ∅ ∈ Con and Y ⊆ X ∈ Con ⇒ Y ∈ Con, and

– ⊢ ⊆ Con×E is the enabling relation, which satisfies X ⊢ e∧X ⊆ Y ∈ Con ⇒ Y ⊢ e. Such a structure is stable if X ⊢ e ∧ Y ⊢ e ∧ Con(X ∪ Y ∪ {e}) ⇒ X ∩ Y ⊢ e.

The set S(E) of configurations of such a structure consists of those X ⊆ E which are – consistent: every finite subset of X is in Con,

– and secured: ∀e ∈ X. ∃e_{0}, …, e_{n} ∈ X. e_{n} = e ∧ ∀i ≤ n. {e_{0}, ..., e_{i−1}} ⊢ e_{i}.

The event structures of Winskel [10] are defined likewise, except that the consistency predicate Con is generated by a given symmetric, irreflexive conflict relation # ⊆ E×E, through Con(X) ⇔ (X finite) ∧ ∀d, e ∈ X. ¬(d#e).

The prime event structures of Winskel [9] are defined as triples E = ^{/} \E, Con, ≤^{\} / combining the requirements for Con from [9] with those for ≤ from [10], and additionally satisfying {e} ∈ Con for all e ∈ E and d ≤ e ∈ X ∈ Con ⇒ X ∪ {d} ∈ Con.

Fig. 2. Formal definitions of 5 types of event structures

tures in [9] moreover allow one to express for any finite set of events whether it is in conflict, i.e. can not happen in full in the same run; in [8, 10] this can only be specified for sets with two events.

However, not every Petri net can be faithfully represented as an event structure from [8–10], due to the phenomenon of resolvable conflict illustrated in Fig. 4. In order to capture this type of behaviour, we simply extend the notion of event structure from [9, 10] by allowing enablings of the form X ⊢ Y, with X and Y sets of events. The enablings X ⊢ Y do not place any restrictions on the occurrence of individual events in Y, but say that for all events in Y to occur, for some set X with X ⊢ Y the events in X have to happen first.

Definition 1. An event structure is a pair E = ^{/}_{\}E, ⊢^{\}_{/} with

– E a set of events,

– ⊢ ⊆ 𝒫(E) × 𝒫(E), the enabling relation.

With this type of event structure we do not need a separate conflict or consistency relation; that a set X of events is in irresolvable conflict can be expressed by not

c • a  •b • • a ac abc ab  b bc \begin{aligned}E & = & \{a, b, c\} \\ # & = & ∅ \\ ∅ & ⊢ & a \\ ∅ & ⊢ & b \\ a & ⊢ & c \\ b & ⊢ & c \end{aligned} c ⇒ (a ∨ b)  a c_{1} # b c_{2}

Fig. 3. A system with disjunctive causality represented as an event structure of [10], a family of configurations with transition relation, a propositional theory and a Petri net. The last picture is the best representation of the same system as an event structure from [8]. It requires the decomposition of the event c, which is causally dependent on the disjunction of a and b, into two events c_{1} and c_{2}, only one of which may happen: c_{1} being causally dependent only on a, and c_{2} on b. Antoni Mazurkiewicz argued against the accuracy of this representation by letting a and b be £1 contributions of two school children to buy a present for their teacher. The act of buying the present, which only costs £1, is represented by c. Now the event structure from [8] has two maximal runs, representing that the present is bought from the contribution from either one child or the other. The event structure from [10] on the other hand has only one possible run, in which the buying of the present is caused by the disjunction of the two contributions. The latter would be a fairer description of the intended state of affairs.

having any enabling of the form Y ⊢ X. When describing an event structure of [9, 10] as one of ours, we have to omit enablings X ⊢ e with {e} ∉ Con and add enablings ∅ ⊢ X for sets X with |X| ≠ 1 and Con(X), and also for infinite X.

In Sect. 2 we discuss various forms of behavioural equivalence on these new event structures. In Sect. 3 we show how they include the classical event structures, thereby establishing their generality. In Sect. 4 we consider the relation

•c• • a  •b  • a ac abc c  b bc \begin{aligned}E & = & \{a, b, c\} \\ c & ⊢ & \{a, b\} \\ ∅ & ⊢ & X & for X ≠ \{a, b\} \end{aligned} (a ∧ b) ⇒ c  a_{1} # # a_{2} # c b_{1} # b_{2}

Fig. 4. A system with resolvable conflict represented as a Petri net, an event structure as introduced here, a family of configurations with transition relation, and a propositional theory. The events a and b are initially in conflict (only one of them may happen), but as soon as c occurs this conflict is resolved. The last picture is the best representation of the same system as an event structure from [8], again with arguable accuracy. It yields a system with two maximal runs, in one of which c causes just a, and in the other just b.

P: • a  •b  M: • a  •  •b \begin{aligned}E & = & \{a, b\} \\ ∅ & ⊢ & ∅ \\ ∅ & ⊢ & \{a\} \\ ∅ & ⊢ & \{b\} \\ ∅ & ⊢ & \{a, b\} \end{aligned}  \begin{aligned}E & = & \{a, b\} \\ ∅ & ⊢ & ∅ \\ ∅ & ⊢ & \{a\} \\ ∅ & ⊢ & \{b\} \\ \{a\} & ⊢ & \{a, b\} \\ \{b\} & ⊢ & \{a, b\} \end{aligned} • a  ab  b

Fig. 5. Two systems P (parallelism) and M (mutual exclusion) represented as a Petri net and an event structure. The figure in the middle describes the configurations of P and M, as well as the transition relation of P. The dashed transition is lacking in Q. Even though P and M have the same configurations and single action transition relations, their behaviour is different, as witnessed by the transition ∅ ⟶_{P} {a, b}.

between event structures and Petri nets, making use of infinitary propositional theories to translate between them. We show that our new event structures enable us to represent any Petri net, thereby establishing their universality.

2 Configurations and Transitions

We formalise the dynamic behaviour of an event structure by defining a transition relation between sets of events. The idea here is that when X is the set of events that have happened so far, an additional set U of events can happen (concurrently) iff every subset of X ∪ U is enabled by a set of events that have happened before, i.e. a subset of X.

Definition 2. The step transition relation ⟶_{E} between sets of events X, Y ⊆E of an event structure E = ^{/}_{\}E, ⊢^{\}_{/} is given by

X ⟶_{E} Y ⇔ (X ⊆ Y ∧ ∀Z ⊆ Y. ∃W ⊆ X. W ⊢ Z).

For the single action transition relation we also require that |Y − X| ≤ 1. The set L(E) of (left-closed) configurations of E is L(E) = {X ⊆ E | X ⟶_{E} X}. Two event structures E and F are transition equivalent if they have the same events and ⟶_{E}=⟶_{F}.

Thus, X ∈ L(E) ⇔ ∀Y ⊆ X. ∃Z ⊆ X. Z ⊢ Y and if X ⟶_{E} Y then X, Y ∈L(E). In Figs. 1, 3 and 4 we have indicated the single action transition relation with solid arrows, and the rest of the step transition relation with dashed ones. Figure 5 shows that the step transition relation can provide important information about an event structure which is included neither in its family of configurations nor in its single action transition relation.

2.1 Purity

We now introduce an important class of event structures whose step transition relation is completely determined by their family of configurations.

Definition 3. An event structure is pure if X ⊢ Y only if X ∩ Y = ∅.

Proposition 1. Let E = ^{/}_{\}E, ⊢^{\}_{/} be a pure event structure, and x, y ∈ L(E). Then

x ⟶_{E} y iff x ⊆ y ∧ ∀Z(x ⊆ Z ⊆ y ⇒ Z ∈ L(E)).

Proof. “Only if” follows immediately from the definitions.

For “if” let x ⊆ y and ∀Z(x ⊆ Z ⊆ y ⇒ Z ∈ L(E)). Let Z ⊆ y. Then x ⊆ x ∪ Z ⊆ y, so x ∪ Z ∈ L(E). Hence, by Definition 2, ∃W ⊆ x ∪ Z. W ⊢ Z. As E is pure, W ∩ Z = ∅, hence W ⊆ x, which had to be proved. ⊓ ⊔

Corollary 1. Two pure event structures E and F are transition equivalent iff they have the same events and L(E) = L(F).

2.2 Reachability

It can be argued that only the reachable configurations and the reachable part of the step transition relation are semantically relevant.

Definition 4. A configuration x of an event structure E is reachable if there is a sequence ∅ = x_{0} ⟶_{E} x_{1} ⟶_{E} … ⟶_{E} x_{n} = x. Let R(E) denote the set of reachable configurations of E. Two event structures E and F are reachable transition equivalent if they have the same events and ⟶_{E} ^{\}R(E) =⟶_{F} ^{\}R(F).

Clearly, transition equivalence is finer than reachable transition equivalence. The following example shows that this is strictly so.

Example 1. Take as events of E the set Q of rational numbers and define ⊢ by ∅ ⊢ X for any X with |X| ≠ 1, and X ⊢ {e} iff X = {d ∈ Q | d < e}. We have R(E) = {∅}, whereas L(E) additionally contains representatives of all reals as well as extra copies of the rationals and Q itself (infinity). If F is /_{\}Q, {∅ ⊢∅}^{\}_{/} then E and F are reachable transition equivalent, yet L(E) ≠ L(F) (hence ⟶_{E}≠⟶_{F}).

The following shows that, unlike in the pure case, the reachable configurations of impure event structures, and thus also their step transition relations, are in general not determined by their left-closed configurations.

Example 2. Let E = ^{/}_{\}{e}, {∅ ⊢∅, {e} ⊢{e}}^{\}_{/}. Then L(E) = {∅, {e}}, whereas R(E)={∅}. Let F = ^{/}_{\}{e}, {∅ ⊢∅, ∅ ⊢{e}}^{\}_{/}. Then L(E)=L(F) but R(E)≠R(F).

Using Prop. 1 we obtain a reachable analogue of Cor. 1. This result can be slightly strengthened as follows.

Definition 5. Call an event structure reachably pure if X ⊢ Y only if either X ∩ Y = ∅ or Y ⊆ X.

The event structure E of Example 2 for instance is reachably pure, but not pure.

Proposition 2. Two reachably pure event structures E and F are reachable transition equivalent iff they have the same events and R(E) = R(F).

Proof. Enablings X ⊢ Y with ∅ ≠ Y ⊆ X can be omitted while preserving the reachable configurations and the step transition relation between them.

3 Connecting with Classical Event Structures

In this section we define various properties of our event structures which, in suitable combinations, determine subclasses corresponding to the various event structures in [8–10]. We also show how our left-closed configurations generalise the configurations used for the event structures of [8] as well as for the prime event structures of [9, 10], and we develop a notion of secured configuration that generalises the notion of configuration used for all event structures of [9, 10].

Definition 6. Let E = ^{/}_{\}E, ⊢^{\}_{/} be an event structure. A set of events X ⊆ E is consistent, written Con(X), if ∀Y ⊆ X. ∃Z ⊆ E. Z ⊢ Y. The direct causality relation ≺ ⊆ E × E is given by d ≺ e ⇔ ∀X. (X ⊢ {e} ⇒ d ∈ X). We take the causality relation, ≤, to be the reflexive and transitive closure of ≺. E is

– rooted if ∅ ⊢ ∅,

– singular if X ⊢ Y ⇒ X = ∅ ∨ |Y | = 1,

– conjunctive if X_{i} ⊢ Y (i ∈ I ≠ ∅) ⇒ ⋂_{i∈I} X_{i} ⊢ Y,

– locally conjunctive if X_{i} ⊢Y (for i∈I ≠∅)∧Con(⋃_{i∈I} X_{i}∪Y) ⇒ ⋂_{i∈I} X_{i} ⊢Y,

– L-irredundant if each event occurs in a configuration, i.e. E =⋃ L(E),

– R-irredundant if E =⋃ R(E),

– and cycle-free if there is no chain e_{0} ≺ e_{1} ≺ ⋯ ≺ e_{n} ≺ e_{0} and has

– finite causes if X ⊢ Y ⇒ X finite,

– finite conflict if X infinite ⇒ ∅ ⊢ X

– and binary conflict if |X| > 2 ⇒ ∅ ⊢ X.

Clearly, conjunctivity implies local conjunctivity, R-irredundancy implies Lirredundancy and cycle-freeness, and binary conflict implies finite conflict.

3.1 Correspondence through Left-closed Configurations

For singular event structures, our notion of a left-closed configuration can be simplified as follows:

Observation 1. Let E be a singular event structure. Then

X ∈ L(E) ⇔ Con(X) ∧ ∀e ∈ X. ∃Z ⊆ X. Z ⊢ {e}.

When d ≤ e, any configuration containing e also contains d. When E = ^{/}_{\}E, ⊢^{\}_{/} is conjunctive, for any consistent event e ∈ E there is a smallest set X ⊆ E with X ⊢ {e}. Therefore, the part of the enabling relation consisting of enablings X ⊢ {e} is in essence completely determined by the causality relation ≤.

Observation 2. Let E be a singular, conjunctive event structure. Then

X ∈ L(E) ⇔ Con(X) ∧ ∀d, e ∈ E. d ≤ e ∈ X ⇒ d ∈ X.

An event structure as in [8], or a prime event structure as in [9, 10], can be translated into our framework by defining enablings {d | d < e} ⊢ {e}, as well as some enablings of the form ∅ ⊢ X. For prime event structures with a binary conflict relation # we take ∅ ⊢ X whenever |X| ≠ 1, 2, and when X = {d, e} with ¬(d#e); for prime event structures as in [9] we take ∅ ⊢ X when X is infinite or |X| ≠ 1 and Con(X). Clearly, the resulting event structure is pure. Hence the dynamic behaviour of such an event structure, as given by its step transition relation, is fully determined by its left-closed configurations.

Using the translation given above, an event structure as in [8], or a prime event structure as in [9, 10], maps to an event structure in our sense that is singular and conjunctive (as well as rooted and with finite conflict). By Obs. 2, it now follows that our notion of left-closed configuration generalises the notion of configuration employed in [8] and for prime event structures in [9, 10].

3.2 Correspondence through Secured Configurations

Definition 7. A set of events X is a secured configuration of an event structure E if there is an infinite sequence ∅ = x_{0} ⟶_{E} x_{1} ⟶_{E} … with X = ⋃_{i=0}^{∞} x_{i}.

Computationally, a secured configuration can be understood by partitioning time in countably many successive stages S_{n} (n ≥ 1). The set x_{n} − x_{n−1} contains the events that occur during stage S_{n}. These events must be enabled by events occurring in earlier stages. The set X contains all events that happen during such a run. The secured configurations include the reachable ones (just take x_{i} = x_{n} for i > n).

Observation 3. Any event structure E with finite conflict satisfies S(E)⊆L(E).

For the event structures that result from mapping prime event structures as in [9, 10] into our framework we find, using the principle of finite causes, that all left-closed configurations are secured. It follows that both the secured and the left-closed configurations can be understood as generalisations of the notion of configuration for prime event structures from [9, 10].

Proposition 3. Two singular event structures with finite conflict E and F are reachable transition equivalent iff they have the same events and S(E) = S(F).

Proof. “only if” follows immediately from Definition 7.

“if”: Singular event structures are always reachably pure. Using the proof of Prop. 2, we can restrict attention to the case that E and F are pure. For F one of L, R or S we define ⟶_{F(E)} by

x ⟶_{F(E)} y iff x ⊆ y ∧ ∀Z(x ⊆ Z ⊆ y ⇒ Z ∈ F(E)).

By Definition 7 and Obs. 3 we have R(E) ⊆ S(E) ⊆ L(E), hence

⟶_{E} ^{\}R(E) = ⟶_{R(E)} ⊆ ⟶_{S(E)} ⊆ ⟶_{L(E)} = ⟶_{E} .

As the reachable part of both ⟶_{R(E)} and ⟶_{L(E)} (defined the obvious way) is ⟶_{E} ^{\}R(E), the reachable part of ⟶_{S(E)} must also be ⟶_{E} ^{\}R(E), and so the latter is fully determined by S(E).

Using the translation given at the end of Sect. 1, an event structure as in [9, 10] maps to an event structure in our sense that is singular and with finite causes and finite conflict. Hence the dynamic behaviour of such an event structure, as given by the reachable part of its step transition relation, is fully determined by its secured configurations.

Table 1. This table indicates in which way the event structures from [8–10] correspond with subclasses of our event structures. In all 7 cases we have that any event structure from [8–10] translates into one of ours with the listed properties, that has the same events and configurations; and vice versa, that for each of our event structures with the required properties an event structure from [8–10] can be found that has the same events and configurations. As indicated, we use the left-closed configurations for the event structures from [8], and the secured configurations for the ones from [9, 10]. For the prime event structures from [9, 10] the two notions of configuration coincide.

ev. str. [9] rooted, singular, finite causes & finite conflict  S
stable [9] same & locally conjunctive  S
prime [9] same & conjunctive & R-irredundant  S, L
ev. str. [10] rooted, singular, finite causes & binary conflict  S
stable [10] same & locally conjunctive  S
prime [10] same & conjunctive & R-irredundant  S, L
ev. str. [8] rooted, singular, binary conflict, conjunctive, L-irr. & cycle-free L

The next proposition says that for such event structures the secured configurations in turn are completely determined by the finite secured ones. In addition, it provides a simplification of the notion of a secured configuration.

Proposition 4. Let E be a singular event structure with finite conflict and finite causes. Then

X ∈ S(E) ⇔ ∀Y ⊆_{fin} X. ∃Z ∈ S(E). Z is finite ∧ Y ⊆ Z ⊆ X,

i.e. the secured configurations are the directed unions over the set of finite secured configurations. Moreover,

X ∈ S(E) ⇔ \begin{cases}Con(X) ∧ \\ ∀e ∈ X. ∃e_{0}, …, e_{n} ∈ X. e = e_{n} ∧ \\ ∀k ≤ n. ∃Y ⊆ \{e_{0}, ..., e_{k−1}\}. Y ⊢ \{e_{k}\}. \end{cases}

The proof of this proposition will appear in [3]. It follows that our secured configurations generalise the configurations of [9, 10]. Table 1 tells exactly how the various event structures of [8–10] can be regarded as subclasses of our event structures. Again, the proofs of the claims therein will be provided in [3].

4 Petri Nets and Propositional Theories

In this section we describe how any Petri net can be represented, in a behaviour preserving way, by a rooted event structure with finite conflict, and vice versa. We also show how to represent an event structure as a propositional theory.

4.1 From Nets to Event Structures

Definition 8. A Petri net is a tuple N = ^{/}_{\}S, T, F, I^{\}_{/} with

– S and T two disjoint sets of places (Stellen in German) and transitions,

– F ⊆ S × T ∪ T × S, the flow relation,

– and I : S → IN, the initial marking.

In [2] we described how any Petri net can be transformed, in a behaviour preserving way, into a 1-occurrence net, this being a Petri net with the property that in any run each transition can fire at most once. The transformation replaces any transition by countably many copies, each of which is connected to the places of the net (through the flow relation) in the same way as the original transition. Each of the obtained transitions gets a private preplace, initially marked with 1 token. This ensures that whenever a transition could fire in the original net, one of its copies can fire in the transformed net—but each of the new transitions can fire only once. A formal account of the way in which this transformation is behaviour preserving would require the use of labelled Petri nets.

We now show how any 1-occurrence net can be represented as an event structure. Let N = ^{/}_{\}S, E, F, I^{\}_{/} be a 1-occurrence net. For any place s ∈ S let s^{•} = {t∈E | (s, t)∈F } be its set of posttransitions and^{•}s = {t∈E | (t, e)∈F } its set of pretransitions. For any finite set Y ⊆ s^{•} of posttransitions of s, |Y | is the number of tokens needed in place s for all transitions in Y to fire, so |Y | · − I(s) is the number of tokens that have to arrive in place s before all transitions in Y can fire. Furthermore, let ^{n}s = {X ⊆ ^{•}s | |X| = n} be the collection of sets X of pretransitions of s, such that if all transitions in X fire, n∈IN tokens will arrive in s. Write ^{Y}s for ^{|Y |· −I(s)}s. One of the sets of transitions in ^{Y}s has to fire entirely before all transitions in Y can fire.

For any finite set of transitions Y ⊆ E, let S_{Y} be the set of places s with Y ⊆ s^{•} and |Y | − I(s) > 0. Now write X ⊢_{N} Y whenever X = ⋃_{s∈S_{Y}} X_{s} with X_{s} ∈ ^{Y}s. We also write ∅ ⊢_{N} Y whenever Y is infinite. The event structure associated to N is defined as E(N) = ^{/}_{\}E, ⊢_{N}^{\}_{/}. Note that E(N) is rooted and with finite conflict. It can be shown that this event structure has the same step transition relation as N, at least when restricting to steps of finitely many events, although we didn’t have space to formalise the latter notion for Petri nets here.

It is not hard to extend the above construction to nets with arcweights [3].

4.2 From Event Structures to Propositional Theories

With any event structure E = ^{/}_{\}E, ⊢^{\}_{/} we associate the (infinitary) propositional theory

T (E) = {⋀ X ⇒ ⋁{⋀ Y | Y ⊢ X} | X ⊆ E}.

In this context, an event is regarded as the proposition that it has happened. The propositional formulae generated above give necessary and sufficient conditions for a set of events to be a left-closed configuration; it is not hard to see that L(E) is exactly the set of models of T (E) in the sense of propositional logic.

A propositional theory provides a pleasant alternative representation of an event structure; examples of this can be found in the figures of Sect. 1.

For any two subsets X,Y of E, let the clause X ⇒ Y abbreviate the implication ⋀ X ⇒ ⋁ Y. A theory consisting of a set of clauses is said to be in conjunctive normal form. Using the distributivity of ⋁ over ⋀, and that φ ⇒ ⋀_{i∈I} ψ_{i} is equivalent to ⋀_{i∈I}(φ ⇒ ψ_{i}), the theory T (E) can be turned into the conjunctive normal form T_{CNF}(E). We say that a propositional theory in conjunctive normal form is rooted if it has no clauses of the form ∅ ⇒ X, and that it has finite conflict if there are no clauses X ⇒ Y with X infinite. Clearly, if E is a rooted and with finite conflict, then so is T_{CNF}(E).

4.3 From Propositional Theories to Petri nets

Let T = ^{/}_{\}E, T^{\}_{/} be a propositional theory in conjunctive normal form that is rooted and with finite conflict. As in [2], we define the associated Petri net N (T) as follows. As transitions of the net we take the events from E. For every transition we add one place, containing one initial token, that has no incoming arcs, and with its only outgoing arc going to that transition. These 1-occurrence places make sure that every transition fires at most once. For every clause X ⇒ Y in T, we introduce a place in the net. This place has outgoing arcs to each of the transitions in X, and incoming arcs from each of the places in Y. Let n be the cardinality of X. As T is rooted and with finite conflict, n ≠ 0 and n is finite. We finish the construction by putting n − 1 initial tokens in the created place:

X {  _{•• • X ⇒ Y}  } Y

The place belonging to the clause X ⇒ Y does not place any restrictions on the firing of the first n − 1 transitions in X. However, the last one can only fire after an extra token arrives in the place. This can happen only if one of the transitions in Y fires first. The firing of more transitions in Y has no adverse effects, as each of the transitions in X can fire only once. Thus this place imposes the same restriction on the occurrence of events as the corresponding clause.

It should be intuitively clear that the dynamic behaviour of N (T_{CNF}(E)) strongly resembles that of E, although it should be admitted that in the standard semantics of Petri nets only finitely many transitions may fire in one step, whereas Definition 2 allows infinite steps. Nevertheless, we have

Theorem 1. Let E be a rooted event structure with finite conflict. Then E(N (T_{CNF}(E))) is transition equivalent to E.

Proof sketch. It is straightforward to find mappings T from nets to propositional theories [3] and E′ from propositional theories of the form T (N) with N a net to event structures, such that E(N) = E′(T (N)) for all Petri nets, T (N (T)) = T for all propositional theories T in conjunctive normal form, and E′(T_{CNF}(E)) ≡ E for all event structures E, where ≡ denotes transition equivalence.

In general this theorem depends intrinsically on the specific form of T_{CNF}(E); however, for pure event structures any conjunctive normal form of T (E) (up to logical equivalence, i.e. having the same models) will do, as shown in [3].

Also note that the construction N ∘ T_{CNF} ∘ E converts any 1-occurrence net into an equivalent net without arcweights.

Table 2. Corresponding properties

Event structures  Propositional theories and nets Petri nets
rooted  (>0, any)  (any, any)
singular  (1, any), (any, 0)  (≤1, any), (any, 0)
manifestly conjunctive (any, ≤1)  (any, ≤1)
finite conflict  (finite, any)  (any, any)
binary conflict  (≤2, any)  (≤2, any)

4.4 Comparing Models

It is interesting to see how three important properties of event structures correspond with structural properties of Petri nets. Call an event structure manifestly conjunctive if for every set of events Y there is at most one set X with X ⊢ Y. Every conjunctive event structure can be made manifestly conjunctive by deleting, for every set Y, all but the smallest X for which X ⊢ Y. The property of conjunctivity implies that such a smallest X exists. This normalisation preserves transition equivalence, and all properties of Definition 6.

When E is an event structure satisfying any of the properties from the left column of Table 2, then T_{CNF}(E) satisfies the corresponding properties from the middle column. These are to be read as cardinality restrictions on the sets X and Y, respectively, in each of its clauses X ⇒ Y. For instance, if E is singular, T_{CNF}(E) has only clauses X ⇒ Y with |X| = 1 or |Y | = 0. Furthermore, if T is a rooted propositional theory with finite conflict satisfying any of the properties of the middle column, then N (T) satisfies these same properties, but now they are cardinality restrictions on the number of outgoing and incoming arcs, respectively, for every place in N (T). Finally, any net satisfying some of the restrictions from the middle column, or even the weaker variants from the right column, translates to an event structure satisfying the corresponding restrictions on the left. This remains true if any place with n incoming arcs and k initial tokens is deemed to satisfy the restriction “(≤k+n, ≤n) or (k+n+1, 0)”.

5 Related Work

A bundle event structure, as studied in Langerak [7], can in our framework best be understood as a propositional theory. Using the translation of Sect. 4 it maps to a special kind of stable event structure [10]. Langerak’s notion of an extended bundle event structure on the other hand does not correspond to an event structure as in [9, 10]. Here the symmetric binary conflict relation # is replaced by an asymmetric counterpart ⇝. When a ⇝ b, the event b can happen regardless of a, and a is initially enabled as well; however, as soon as b happens, a is blocked. Asymmetric conflict a ⇝ b can be translated into our framework as {b} ⊢ {a, b}. (As this translation introduces impurity, for its correctness it is necessary to consider the transition relation of Definition 2.) Thus, extended bundle event structures are subsumed by our event structures too.

The same can be said for the extended dual event structures of Katoen [6]. Here the crucial feature is the symmetric and irreflexive interleaving relation, modelling mutual exclusion of events, i.e. disallowing them to overlap in time. As in Fig. 5, this can be modelled in our framework as {a} ⊢ {a, b} {b} ⊢ {a, b}. Using similar techniques, we believe it is also possible to embed the causal automata of Gunawardena [4] in our framework.

Boudol [1] provides translations between a class of 1-occurrence nets, the flow nets, and a class of flow event structures that fall in expressive power between the prime and the stable event structures of [10]. His correspondence extends the correspondence between safe occurrence nets and prime event structures due to [8]. As Boudol’s translations preserve the notions of event (=transition) and configuration, they are consistent with our approach. Our translations can be regarded as an extension of the work of [1] to general Petri nets.

Another translation between Petri nets and a new model of event structures has been provided in Hoogers, Kleijn & Thiagarajan [5], albeit for systems without autoconcurrency only. Their event structures are essentially families of configurations with a step transition relation between them. The translations of [5] are quite different from ours: even on 1-occurrence nets an individual transition may correspond to multiple events. We conjecture the two approaches are equivalent under a suitable notion of history preserving bisimulation.

References

1. G. Boudol (1990): Flow event structures and flow nets. In I. Guessarian, editor: Semantics of Systems of Concurrent Processes, Proceedings LITP Spring School on Theoretical Computer Science, La Roche Posay, France, LNCS 469, pp. 62–95.

2. R.J. van Glabbeek & G.D. Plotkin (1995): Configuration structures (extended abstract). In D. Kozen, editor: Proc. LICS’95, San Diego, USA, pp. 199–209.

3. R.J. van Glabbeek & G.D. Plotkin (2004): Configuration structures, event

structures and Petri nets. Draft at http://theory.stanford.edu/~rvg/event/.

4. J. Gunawardena (1992): Causal automata. TCS 101, pp. 265–288.

5. P.W. Hoogers, H.C.M. Kleijn & P.S. Thiagarajan (1996): An event structures semantics for general Petri nets. TCS 153, pp. 129–170.

6. J.-P. Katoen (1996): Quantitative and Qualitative Extensions of Event Structures, PhD thesis, Department of Computer Science, University of Twente.

7. R. Langerak (1992): Transformations and Semantics for LOTOS. PhD thesis, Department of Computer Science, University of Twente.

8. M. Nielsen, G.D. Plotkin & G. Winskel (1981): Petri nets, event structures and domains, part I. TCS 13(1), pp. 85–108.

9. G. Winskel (1987): Event structures. In W. Brauer, W. Reisig & G. Rozenberg, editors: Petri Nets: Applications and Relationships to Other Models of Concurrency, Advances in Petri Nets 1986, Part II; Proceedings of an Advanced Course, Bad Honnef, September 1986, LNCS 255, Springer, pp. 325–392.

10. G. Winskel (1989): An introduction to event structures. In J.W. de Bakker, W.P. de Roever & G. Rozenberg, editors: REX School/Workshop on Linear Time, Branching Time and Partial Order in Logics and Models for Concurrency, Noordwijkerhout, The Netherlands, May/June 1988, LNCS 354, Springer, pp. 364–397.