Configuration Structures, Event Structures and Petri Nets^{∗}

R.J. van Glabbeek

NICTA, Sydney, Australia

University of New South Wales, Sydney, Australia Stanford University, USA

rvg@cs.stanford.edu

G.D. Plotkin

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

Stanford University, USA

             gdp@inf.ed.ac.uk

In this paper the correspondence between safe Petri nets and event structures, due to Nielsen, Plotkin and Winskel, is extended to arbitrary nets without self-loops, under the collective token interpretation. To this end we propose a more general form of event structure, matching the expressive power of such nets. These new event structures and nets are connected by relating both notions with configuration structures, which can be regarded as representations of either event structures or nets that capture their behaviour in terms of action occurrences and the causal relationships between them, but abstract from any auxiliary structure.

A configuration structure can also be considered logically, as a class of propositional models, or—equivalently— as a propositional theory in disjunctive normal from. Converting this theory to conjunctive normal form is the key idea in the translation of such a structure into a net.

For a variety of classes of event structures we characterise the associated classes of configuration structures in terms of their closure properties, as well as in terms of the axiomatisability of the associated propositional theories by formulae of simple prescribed forms, and in terms of structural properties of the associated Petri nets.

Introduction

The aim of this paper is to connect several models of concurrency, by providing behaviour preserving translations between them.

Figure 1: Behaviour preserving translations in [25]

Occurrence nets  Prime event structures_{w. bin. conflict}  Prime algebraic coherent domains Families of configurations_{unfol ding} Safe Petri Nets

In Nielsen, Plotkin & Winskel [25] event structures were introduced as a stepping stone between Petri nets and Scott domains. It was established that every safe Petri net can be unfolded into an occurrence net; the occurrence nets are then in correspondence with event structures; and they in turn are in correspondence with prime algebraic coherent Scott domains. In Winskel [34] a more general notion of event structure was proposed, corresponding to a more general kind of Scott domain. The event structures from [25] are now called prime event structures with binary conflict.

The translation from event structures to domains passes through a stage of families of configurations of event structures. Winskel [33] and Van Glabbeek & Goltz [11] found it convenient to use such families as a model of concurrency in its own right. In this context the families were called configuration structures [11].

Figure 2: Our main contribution: behaviour preserving translations between four models of concurrency

1-occurrence nets  Configuration structures  Pure event structures Propositional theories  Transition systems_{occ. nets}  _{families}  _{domains}_{prime}_{[29]}_{[25]}_{1-}_{unf}Pure Petri Nets  _{[8]}

The present paper generalises the correspondence between safe Petri nets and configuration structures to (possibly unsafe) nets without self-loops (the pure nets). For this purpose we use a more general kind of configuration structure than in [11], the set systems. These have an attractive alternative presentation as propositional theories [29], which is exploited in their translation to nets. We also generalise the event structures of [34], so that, again, our configuration structures arise as their families of configurations. The connection between configuration structures and Scott domains is generalised in Van Glabbeek [8], who proposes transition systems as alternative presentations of domains; we do not consider these matters further in the present paper.

∗This work was supported by ONR grant N00014-92-J-1974 (when both authors were at Stanford), by EPSRC grant GR/S22097 (when both authors were at the University of Edinburgh) and by a Royal Society-Wolfson Award.

The relationship between configuration structures, infinitary propositional theories, event structures and Petri nets is described in Section 1. We 1-unfold pure nets into pure 1-occurrence nets, which generalise the occurrence nets of [25], and argue that this 1-unfolding preserves the causal and branching time behaviour of the represented system. This allows us to restrict attention to pure 1-occurrence nets in the rest of the paper. Moreover, we give translations showing that configuration structures, propositional theories and event structures are equivalent up to so-called configuration equivalence (which is defined as being mapped to the same configuration structures) and that, with a slight restriction, all four models are equivalent up to finitary equivalence.

Section 2 introduces a computational interpretation of configuration structures, Petri nets and event structures in terms of associated transition relations; restricted to pure Petri nets and pure event structures, these transition relations can be derived from the relevant sets of configurations, but not in general. With that, Section 3 provides definitions of notions of reachable and secured (reachable in the limit) configurations and considers corresponding notions of equivalence by restricting to reachable or secured, and possibly finite, configurations.

With the general framework thus provided, Section 4 considers the various brands of event structures introduced by Winskel and his co-workers. They are shown to correspond to natural restrictions on the general notion of event structure, adapting the comparisons, on the one hand, to the original notion of configuration and, on the other hand, to the relevant one from the general theory. These comparisons are summarised in Table 1.

It is then natural to enquire how the event structure restrictions are reflected in corresponding restrictions on configurations structures and so on; this is the subject of Section 5. Sections 5.1 and 5.2 provide such comparisons, summarised in Table 2, for configuration structures and propositional theories up to configuration equivalence. The restrictions on configuration structures are natural closure properties, and those on propositional theories concern the form of the formulae occurring in an axiomatisation. Section 5.3 does the same, see Table 3, but now with the comparison based on the secured configurations.

Section 5.4 concerns the finitary case, with general comparisons being summarised in Table 4 and the restriction to the finite reachable configurations summarised in Table 5. Section 5.5 ties in Petri nets, providing corresponding structurally defined subclasses; however we were not successful in doing this in all cases. The main mathematical work is done in Sections 5.1 and 5.2, with the rest of the section adapting this work to the various cases at hand.

Section 6 contains a discussion of related work and presents some possibilities for future research. Finally, there is an index for the many technical terms introduced in the course of the paper.

The papers [12] and [13] contain extended abstracts of parts of this work, together with additional material.

1 Four models of concurrency

In this section we present the four models of concurrency mentioned in the introduction, and provide translations between them.

1.1 Configuration structures

Definition 1.1 A set system is a pair C = ^{/}_{\}E, C^{\}_{/} with E a set and C ⊆ 𝒫(E) a collection of subsets.

When a set system is used to represent a concurrent system, we call it a pure configuration structure, but generally drop the word “pure”. (We envision introducing a broader class of configuration structures in the future, matching the expressive power of impure nets.) The elements of E are then called events and the elements of C configurations. An event represents an occurrence of an action the system may perform; a configuration x represents a state of the system, namely the state in which the events in x have occurred.

1.2 Propositional theories

A set system can also be considered from a logical point of view: E is thought of as a collection of propositions and C as the collection of models. Connecting with the computational point of view, we associate with an event the proposition that it has happened. This point of view is due to Pratt [18, 29]. We can now represent a set system by the valid sentences, those holding in all models; these are the laws of C.

To make this precise, we choose a language: infinitary propositional logic. Given a set E of (propositional) variables, the formulae over E form the least class including E and closed under ¬ (negation) and ⋀ (conjunction of sets of formulae). We make free use of other standard connectives such as ⇒, ⋁, ⊥, ⊤: they are all definable from ¬ and ⋀. As usual, an interpretation of E is just a subset of E and one defines in the standard way when an interpretation makes a formula true.

Definition 1.2 An (infinitary) propositional theory is a pair T = ^{/}_{\}E, T^{\}_{/} with E a set of propositional variables and T a class of infinitary propositional formulae over E.

A formula φ over E is valid in a set system C = ^{/}_{\}E, C^{\}_{/} iff it is true in all elements of C; the theory associated to C is T (C) := ^{/}_{\}E, T (C)^{\}_{/}, where T (C) denotes the class of formulae valid in C. Equally, given a propositional theory T = ^{/}_{\}E, T^{\}_{/}, its associated set system is M(T) := ^{/}_{\}E, M(T)^{\}_{/}, where M(T) is the set of models of T, those interpretations of E making every formula in T true. We say that T axiomatises M(T). A formula φ over E is a logical consequence of a theory T if φ is true in any model of T; a formula ψ over E implies φ iff the latter is a logical consequence of the theory ^{/}_{\}E, {ψ}^{\}_{/}. Two propositional theories T and T′ are logically equivalent if M(T) = M(T′), which is easily seen to be the case iff they have the same logical consequences.

Theorem 1 Let C = ^{/}_{\}E, C^{\}_{/} be a set system. Then T (C) axiomatises C, i.e., M(T (C)) = C.

Proof: The single formula ⋁_{X∈C}(⋀ X ∧⋀ ¬(E −X)) already constitutes an axiomatisation of C. It is called the disjunctive normal form of T (C). □

Thus T and M provide a bijective correspondence between set systems and infinitary propositional theories up to logical equivalence. For any two subsets X,Y of E, let the clause X ⇒ Y abbreviate the implication ⋀ X ⇒ ⋁ Y; we say that the elements of X are the antecedents of the clause, and those of Y its consequents. Then for any set system C = ^{/}_{\}E, C^{\}_{/}, the set of clauses {X ⇒ (E − X) | X ∉ C} constitutes another axiomatisation of C. A theory consisting of a set of clauses is said to be in conjunctive normal form.

1.3 Event structures

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

• E a set of events, • ⊢ ⊆ 𝒫(E) × 𝒫(E), the enabling relation.

Like a configuration structure, an event structure describes a concurrent system in which the events represent action occurrences. In previous notions of event structure [34, 35], one only had singleton enablings: ⊢ ⊆ 𝒫(E) × E. Here we generalise ⊢ to a relation between sets of events. As before, the enabling relation places some restrictions on which events can happen when. The idea here is that when X is the set of events that 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 happened before, i.e., a subset of X.

Example 1 Let E = {d, e, f} and the enabling relation be given by ∅ ⊢ X for any X ⊆ E with X ≠ E. In the initial state of the event structure E = ^{/}_{\}E, ⊢^{\}_{/}, each of the events d, e and f can happen, and any two of them can happen concurrently. However, there is no way all three events can ever happen, because there is no set of events X with X ⊢ {d, e, f}. This is a case of ternary conflict.

Example 2 Let E = {a, b, c} and the enabling relation be given by {c} ⊢ {a, b} and ∅ ⊢ X for any X ⊆ E with X ≠ {a, b}. Initially, each of the events a, b and c can occur, and the events a and c can even happen concurrently. The events a and b, on the other hand, can initially not happen concurrently, for we do not have ∅ ⊢ {a, b}. However, as soon as c occurs, the events a and b can occur in parallel. We say that the conflict between a and b is resolved by the occurrence of c.

Example 3 Let E = {d, e} and the enabling relation be given by {d} ⊢ {d, e} and ∅ ⊢ X for any X ⊆ E with X ≠ {d, e}. Initially, d and e can both occur, but not in parallel. After d has happened, e may follow, but when e happens first, d cannot follow. The reason is that we do not have X ⊢ {d, e, } for some X ⊆ {e}. This is a case of asymmetric conflict [22, 26].

In Section 4 we will explain how these event structures generalise the ones of [25, 34, 35]. In those papers the behaviour of an event structure is formalised by associating to it a family of configurations. However, there are several ways to do so (cf. Section 3); here we only consider the simplest variant.

Definition 1.4 Let E = ^{/}_{\}E, ⊢^{\}_{/} be an event structure. The set L(E) of left-closed configurations of E is given by

X ∈ L(E) ⇔ ∀Y ⊆ X. ∃Z ⊆ X. Z ⊢ Y.

The left-closed configuration structure associated to E is L(E) := ^{/}_{\}E, L(E)^{\}_{/}. Two event structures E and F are L-equivalent if L(E) = L(F).

In Section 2 we provide a computational interpretation of event structures with the property that the leftclosed configurations of an event structure adequately represent the behaviour of the represented system for the following class of “pure” event structures:

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

The event structures of Examples 1 and 2 are pure, but the one of Example 3 is not.

We now show that any configuration structure can be obtained as the left-closed configuration structure associated to a pure event structure.

Definition 1.6 Let C = ^{/}_{\}E, C^{\}_{/} be a configuration structure. The event structure associated to C is E(C) := ^{/}_{\}E, ⊢^{\}_{/}, with X ⊢ Y iff X ∩Y =∅ ∧ X ∪Y ∈C.

Theorem 2 Let C be a configuration structure. Then E(C) is pure and L(E(C)) = C.

Proof: Let C = ^{/}_{\}E, C^{\}_{/} and E(C) = ^{/}_{\}E, ⊢^{\}_{/}. Suppose x ∈ C. For any Y ⊆ x take Z := x − Y. Then Z ⊆ x and Z ⊢ Y. So x ∈ L(E(C)). Conversely, suppose x ∈ L(E(C)). Then there is a Z ⊆ x such that Z ⊢ x. (In fact, Z = ∅.) By construction, x = Z ∪ x ∈ C. □

Hence, E and L provide a bijective correspondence between configuration structures and (pure) event structures up to L-equivalence.

Event structures vs. propositional theories

By combining Theorems 1 and 2 we find that T ∘ L and E ∘ M constitute a bijective correspondence between (pure) event structures up to L-equivalence and propositional theories up to logical equivalence. Below we provide direct translations between them.

To any event structure E = ^{/}_{\}E, ⊢^{\}_{/} we associate the propositional theory T (E) := ^{/}_{\}E, T (E)^{\}_{/}, where

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

This logical view of event structures corresponds exactly with their left-closed interpretation:

Proposition 1.1 M(T (E)) = L(E) for any event structure E.

Proof: Immediate from the definitions. □

Similarly, to any propositional theory T = ^{/}_{\}E, T^{\}_{/} in conjunctive normal form we associate the (not necessarily pure) event structure E(T) := ^{/}_{\}E, ⊢_{T}^{\}_{/}, where

X ⊢_{T} Y ⇔ ∀Z. ((Y ⇒ Z) ∈ T ⇒ X ∩ Z ≠ ∅).

Proposition 1.2 L(E(T)) = M(T) for any theory T in conjunctive normal form.

Proof: Let x ∈ M(T). To establish x ∈ L(E(T)) we take Y ⊆ x and show x ⊢_{T} Y. Let Z ⊆ E be such that (Y ⇒ Z) ∈ T. As Y ⇒ Z is true in x we have Z ∩ x ≠ ∅. It follows that x ∈ L(E(T)).

Now let x ∈ L(E(T)). To establish x ∈ M(T) we take (Y ⇒ Z) ∈ T. We have to show that Y ⇒ Z is true in x. So suppose Y ⊆ x. Then there must be a W ⊆ x with W ⊢_{T} Y, hence W ∩ Z ≠ ∅. It follows that x ∩ Z ≠ ∅, which had to be shown. □

Thus T and E provide a bijective correspondence between event structures up to L-equivalence and propositional theories up to logical equivalence.

Definition 1.7 A propositional theory in conjunctive normal form is pure if it only contains clauses X ⇒ Y with X ∩ Y = ∅.

Clearly every propositional theory is logically equivalent to a pure one, as impure clauses are tautologies, i.e., they hold in all interpretations. In case T = ^{/}_{\}E, T^{\}_{/} is a pure theory, we can define the associated pure event structure E_{p}(T) := ^{/}_{\}E, ⊢_{p}^{\}_{/} by X ⊢_{p} Y ⇔ X ∩ Y = ∅ ∧ X ⊢_{T} Y. Note that E_{p}(T) is pure and L(E_{p}(T)) = M(T).

1.4 Petri nets

Definition 1.8

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

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

• F : (S×T ∪ T ×S) → IN, the flow relation,

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

Petri nets are pictured by drawing the places as circles and the transitions as boxes. For x, y ∈ S ∪T there are F (x, y) arcs from x to y. A net is said to be without arcweightsarcweights if the range of F is {0, 1}.

When a Petri net represents a concurrent system, a global state of such a system is given as a marking, which is a multiset over S, i.e., a function M ∈ IN^{S}. Such a state is depicted by placing M(s) dots (tokens) in each place s. The initial state is given by the marking I. In order to describe the behaviour of a net, we describe the step transition relation between markings.

Definition 1.9 For two multisets M and N over S, or more generally for functions M, N ∈ ℤ^{S}, write M ≤ N if M(s) ≤ N(s) for all s∈S; M+N ∈ ℤ^{S} is the function given by (M + N)(s) := M(s) + N(s), and 0 ∈ IN^{S} the one with 0(s) := 0 for all s ∈ S; M − N ∈ ℤ^{S} is given by (M − N)(s) := M(s) − N(s).

A multiset M over S is finite if {s ∈ S | M(s) > 0} is finite. A multiset M ∈ IN^{S} with M(s) ≤ 1 for all s ∈ S is identified with the set {s ∈ S | M(s) = 1}.

Note that for multisets M and N, the function M −N need not be a multiset.

Definition 1.10 For a finite multiset U : T → IN of transitions in a Petri net, let ^{•}U, U^{•} : S → IN be the multisets of pre- and postplaces of U, given by

•U(s) := ∑_{t∈T} F (s, t)U(t) and U^{•}(s) := ∑_{t∈T} U(t)F (t, s)

for s ∈ S. We say that U is enabled under a marking M if ^{•}U ≤ M. In that case U can fire under M, yielding the marking M′ := M −^{•}U + U^{•}, written M ⟶^{U} M′.

A chain I ⟶^{U_{1}} M_{1} ⟶^{U_{2}} ⋯ ⟶^{U_{n}} M_{n} is called a firing sequence. A marking M is reachable if there is such a sequence ending in M = M_{n}.

If a multiset U of transitions fires, for every transition t in U and every arc from a place s to t, a token moves along that arc from s to t. These tokens are consumed by the firing, but also new tokens are created, namely one for every outgoing arc of t. These end up in the places at the end of those arcs. If t occurs several times in U, all this happens several times (in parallel) as well. The firing of U is only possible if there are sufficiently many tokens in the preplaces of U (the places where the incoming arcs come from). In Section 2.6 we explain why we consider the firing of finite multisets only.

From Petri nets to configuration structures

As for event structures, the behaviour of a net can be captured by associating to it a family of configurations.

Definition 1.11 A (finite) configuration of a Petri net N = ^{/}_{\}S, T, F, I^{\}_{/} is any finite multiset X of transitions with the property that the function M_{X} : S → ℤ given by M_{X} := I−^{•}X+X^{•} is a marking, i.e., M_{X} ≥ 0. Let C(N) denote the set of configurations of N.

Note that 0 is a configuration and M_{0} = I; note further that if x is a configuration and M_{x} ⟶^{U} M′ then x + U is a configuration and M′ = M_{x+U}. So if I ⟶^{U_{1}} M_{1} ⟶^{U_{2}} ⋯ ⟶^{U_{n}} M_{n} is a firing sequence, then x := U_{1} +⋯+U_{n} is a configuration and M_{n} = M_{x}. In general, when x ∈ C(N) then M_{x} is the marking that would result from firing all transitions in x, if possible, regardless of the order in which they fire.

Next we will determine which nets can be faithfully described in this way by means of set systems.

Definition 1.12 A 1-occurrence net is a net in which every configuration is a set.

This implies that any transition can fire at most once, i.e., in every firing sequence M_{0} ⟶^{U_{1}} ⋯ ⟶^{U_{n}} M_{n} the multisets U_{1}, ..., U_{n} are sets and disjoint. When dealing with a 1-occurrence net, typically presented as a tuple ^{/}_{\}S, E, F, I^{\}_{/}, we call its transitions events.

Definition 1.13 A net N = ^{/}_{\}S, T, F, I^{\}_{/} is pure if there is no s in S and t in T with F (s, t) > 0 and F (t, s) > 0, i.e., if it is without self-loops.

In Section 2 we will argue that the configurations of a 1-occurrence net adequately represent the behaviour of the represented system only in the case of pure nets. Therefore we will restrict attention to pure 1occurrence nets.

Definition 1.14 Let N = ^{/}_{\}S, E, F, I^{\}_{/} be a pure 1occurrence net. Its associated configuration structure C(N) is ^{/}_{\}E, C(N)^{\}_{/}. Two such nets N and N′ are configuration equivalent—written N =_{C} N′—if C(N) = C(N′).

Individual vs. collective tokens

There are two different schools of thought in interpreting the causal behaviour of Petri nets, which can be described as the individual and collective token philosophy [12, 9].^{1} The following example illustrates their difference.

A: •  a  •  b  •

In this net, the transitions a and b can fire once each. After a has fired, there are two tokens in the middle place. According to the individual token philosophy, it makes a difference which of these tokens is used in firing b. If the token that was there already is used (which must certainly be the case if b fires before the token from a arrives), the transitions a and b are causally independent. If the token that was produced by a is used, b is causally dependent on a. Thus, the net A above has two maximal computations, that can be characterised by partial orders: a \overline{}b and the trivial one \begin{matrix}a \\ b \end{matrix}. According to the collective token philosophy on the other hand, all that is present in the middle place after the occurrence of a is the number 2. The preconditions for b to fire do not change, and consequently b is always causally independent of a.

1The individual token interpretation of ordinary nets should not be confused with the concept of Petri nets with individual tokens [30] such as predicate/transition nets or coloured Petri nets; there the individuality is hardwired into the syntax of nets.

A net is called safe if no reachable marking has multiple tokens in the same place. For safe nets there is no difference between the individual and collective token interpretations.

The individual token approach has been formalised by the notion of a process, described in Goltz & Reisig [14]. A causality-respecting bisimulation relation based on this approach was proposed by Best, Devillers, Kiehn & Pomello [3] under the name fully concurrent bisimulation. Also the unfolding of non-safe nets into (safe) occurrence nets proposed by Engelfriet [6] and Meseguer, Montanari & Sassone [24] embraces the individual token philosophy.

Best & Devillers [2] adapted the process concept of [14] to fit the collective token philosophy. Equivalence relations on Petri nets based on the collective token interpretation were proposed by us in [12], and include configuration equivalence, defined above. There is no unfolding construction that converts arbitrary non-safe nets into safe nets while preserving their collective token interpretation, for under the collective token interpretation non-safe nets are strictly more expressive than safe ones [9]: only the former can express resolvable conflict [13].

The following example shows that the collective token philosophy allows the identification of nets that are distinguished under the individual token philosophy.

B: •  a  •  b  •

Under the collective token interpretation the precondition of b expressed by the place in the middle of net A is redundant, and hence A must be equivalent to B. In fact, A =_{C} B. However, A and B are not fully concurrent bisimulation equivalent, as B lacks the computation a \overline{}b.

Conversely, the individual token philosophy allows identifications that are invalid under the collective token philosophy, but these necessarily involve labelled nets. A labelled net is a tuple ^{/}_{\}S, T, F, I, l^{\}_{/} with /_{\}S, T, F, I^{\}_{/} a net and l : T → Act a labelling function over some set of action names Act. The labelling enables the presence of multiple transitions with the same name. The net A is fully concurrent bisimulation equivalent with the labelled net C below.

C: •  a  b  • b •

In fact, C is the occurrence net obtained from A by the unfolding of [6, 24]. In the individual token philosophy, both A and C have the computations a \overline{}b and \begin{matrix}a \\ b \end{matrix}. However, in the collective token philosophy A does not have a run a \overline{}b and can therefore not be equivalent to C in any causality preserving way.

Thus, capturing the behaviour of nets by means of our mapping C to configuration structures is compatible with the collective token interpretation only. In the remainder of this paper, we therefore take the collective token approach.

Rooted structures and finitary equivalence

The configuration structure associated to a pure 1occurrence net is always finitary, meaning that all configurations are finite, and rooted, meaning that the empty set of events is a configuration. In order to translate between the models of concurrency seen before and Petri nets, we therefore restrict attention to rooted structures, and ignore infinite configurations.

Definition 1.15 A configuration structure C=^{/}_{\}E, C^{\}_{/} is rooted if ∅ ∈ C. A propositional theory is rooted if it has no clause of the form ∅ ⇒ X as a logical consequence. An event structure E = ^{/}_{\}E, ⊢^{\}_{/} is rooted if ∅ ⊢ ∅.

Proposition 1.3 If C is rooted, then so are T (C) and E(C). If T is rooted, then so are M(T) and E(T). If E is rooted, then so are L(E) and T (E).

Proof: Straightforward. □

Definition 1.16 Given a configuration structure C, let F(C) be the configuration structure with the same events but with only the finite configurations of C. Two configuration structures C and D are finitarily equivalent—written C ≃_{f} D—if F(C) = F(D).

Instead of considering configuration structures up to finitary equivalence, we could just as well restrict attention to finitary configuration structures, thereby taking a normal form in each equivalence class. However, on the level of propositional theories this involves adding clauses X ⇒ ∅ for every infinite set of events X, which would needlessly complicate the forthcoming Proposition 1.4. Moreover, the fact that C(N) is finitary for every pure 1-occurrence net N is more a consequence of not considering infinite configurations of Petri nets than of there not being any (cf. Section 2.6).

From configuration structures to Petri nets

We now proceed to show that, up to finitary equivalence, every rooted configuration structure can be obtained as the image of a pure 1-occurrence net.

Definition 1.17 Let T = ^{/}_{\}E, T^{\}_{/} be a rooted propositional theory in conjunctive normal form. 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 with X finite, 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 transitions in Y. Let n be the cardinality of X. As T is rooted, n ≠ 0. 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 does the corresponding clause.

Theorem 3 Let T be a rooted propositional theory in conjunctive normal form. Then

C(N (T)) ≃_{f} M(T).

Proof: z ∈ C(N (T)) iff z is finite and M_{z}(s) ≥ 0 for any place s. We have M_{z}(s) ≥ 0 for all 1-occurrence places s exactly when no transition fires twice in z, i.e., when z is a set. For a place s belonging to the clause X ⇒ Y we have M_{z}(s) ≥ 0 iff either one of the transitions in Y has fired, or not all of the transitions in X have fired, i.e., when X ⇒ Y holds in z, seen as a model of propositional logic. The clauses X ⇒ Y of T with X infinite surely hold in any finite configuration z. Thus, z ∈ C(N (T)) iff z is a finite model of T. □

The net N (T) is always without arcweights. Moreover, in case T is pure (cf. Definition 1.7), so is the net N (T). As any rooted configuration structure can be axiomatised by a pure rooted propositional theory in conjunctive normal form, it follows that

Corollary 1 For every rooted configuration structure there exists a pure 1-occurrence net without arcweights with the same finite configurations. □

Thus we have established a bijective correspondence between rooted configuration structures up to finitary equivalence and pure 1-occurrence nets up to configuration equivalence. Moreover, every pure 1-occurrence net is configuration equivalent to a pure 1-occurrence net without arcweights.

Example 4 The event structure with ternary conflict of Example 1 can be represented by the propositional theory

(d ∧ e ∧ f) ⇒ ⊥ .

The Petri net associated to

this theory by Definition 1.17 is:  •• d  e  f• • •

Example 5 Below are the event structure with resolvable conflict from Example 2, its representation as a propositional theory, and the associated Petri net, as well as its configurations, ordered by inclusion.

•c• • a  •b \begin{aligned}E & = & \{a, b, c\} \\ \{c\} & ⊢ & \{a, b\} \\ ∅ & ⊢ & X & for X ≠ \{a, b\} \end{aligned} (a ∧ b) ⇒ c [figure: ∅; \{a\}; \{b\}; \{c\}; \{a, c\}; \{b, c\}; \{a, b, c\}]

Example 6 Below is a propositional theory describing a system in which either a or b is sufficient to enable the event c; this is sometimes called disjunctive causality. We also display the associated Petri net, and its representation as an event structure and a configuration structure.

c • a  •b • \begin{aligned}E & = & \{a, b, c\} \\ \{a\} & ⊢ & \{c\} \\ \{b\} & ⊢ & \{c\} \\ ∅ & ⊢ & X & for X ≠ \{c\} \end{aligned} c ⇒ (a ∨ b) [figure: ∅; \{a\}; \{b\}; \{a, b\}; \{a, c\}; \{b, c\}; \{a, b, c\}]

In case we modify the event structure by omitting the enabling ∅ ⊢ {a, b}, the propositional theory gains a clause (a ∧ b) ⇒ ⊥, the Petri net gains a marked place with arrows to a and b, and the configuration structure loses the configurations {a, b} and {a, b, c}.

From nets to theories and event structures

We know already how to translate pure 1-occurrence nets into propositional theories and event structures, namely through the intermediate stage of configuration structures. Below we provide direct translations that might shed more light on the relationships between these models of concurrency.

Let N = ^{/}_{\}S, E, F, I^{\}_{/} be a 1-occurrence net. For any place s ∈ S let s^{•} := {t ∈ E | F (s, t) > 0} be its set of posttransitions and^{•}s := {t ∈ E | F (t, e) > 0} its set of pretransitions. For any finite set Y ⊆ s^{•} of posttransitions of s, ^{•}Y (s) is the number of tokens needed in place s for all transitions in Y to fire,^{2} so ^{•}Y (s)−I(s), if positive, is the number of tokens that have to arrive in s before all transitions in Y can fire. Furthermore, for n∈ℤ, let ^{n}s := {X ⊆ ^{•}s | X^{•}(s) ≥ n} be the collection of sets X of pretransitions of s, such that if all transitions in X fire, at least n tokens will arrive in s. Write ^{Y}s for ^{^{•}Y (s)−I(s)}s. One of the sets of transitions in ^{Y}s has to fire entirely before all transitions in Y can fire.

The formula φ_{s}^{n} := ⋁_{X∈^{n}s} ⋀ X expresses which transitions need to fire for n tokens to arrive in s. The formula ⋀ Y ⇒ φ_{s}^{^{•}Y (s)−I(s)} expresses that one of the sets of transitions in ^{Y}s has to fire entirely before all transitions in Y can fire. The propositional theory associated to N is defined as T (N) := ^{/}_{\}E, T (N)^{\}_{/}, where T (N) consists of all formulae ⋀ Y ⇒ φ_{s}^{^{•}Y (s)−I(s)} with s ∈ S and Y ⊆_{fin} s^{•}. It follows that

Proposition 1.4 M(T (N)) ≃_{f} C(N) for any pure 1occurrence net N. □

Proof: Let N = ^{/}_{\}S, E, F, I^{\}_{/} be a pure 1-occurrence net and X ⊆_{fin} E be a finite set of transitions of N. Then X ∈ M(T (N)) iff for all s ∈ S and Y ⊆_{fin} s^{•} the formula ⋀ Y ⇒ φ_{s}^{^{•}Y (s)−I(s)} is true in X, which is the case iff (Y ⊆ X) ⇒ ∃Z ⊆ X. Z ∈^{^{•}Y (s)−I(s)}s, or

(Y ⊆ X) ⇒ ∃Z ⊆ X. Z ⊆ ^{•}s ∧ Z^{•}(s) ≥ ^{•}Y (s) − I(s).

In the latter formula the clause Z ⊆ ^{•}s can just as well be deleted, as transitions in Z that are not in ^{•}s do not make a contribution to Z^{•}(s) anyway. Thus this formula is equivalent to

(Y ⊆ X) ⇒ X^{•}(s) ≥ ^{•}Y (s) − I(s).

Likewise, requiring this implication to merely hold for sets of transitions Y with Y ⊆_{fin} s^{•} is moot. Hence

X ∈ M(T (N)) \begin{matrix}⇔ ∀s ∈ S. X^{•}(s) ≥ ^{•}X(s) − I(s) \\ ⇔ ∀s ∈ S. I(s) −^{•}X(s) + X^{•}(s) ≥ 0 \\ ⇔ M_{X} ≥ 0 \\ ⇔ X ∈ C(N). \end{matrix}

□

For any finite set of transitions Y ⊆ E, let S_{Y} be the set of places s with Y ⊆ s^{•} and ^{•}Y (s)−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 if N is pure, then so is E(N).

Proposition 1.5 Let N be a pure 1-occurrence net. Then L(E(N)) ≃_{f} C(N). □

Proof: Let N = ^{/}_{\}S, E, F, I^{\}_{/} be a pure 1-occurrence net and X ⊆_{fin} E be a finite set of transitions of N. Then

X ∈ L(E(N)) ⇔ ∀Y ⊆ X. ∃Z ⊆ X. Z ⊢_{N} Y
⇔ ∀Y ⊆ X. ∀s ∈ S_{Y} . ∃Z_{s} ⊆ X. Z_{s} ∈ ^{Y}s ⇔

∀Y ⊆X. ∀s∈S_{Y} . ∃Z_{s} ⊆X. Z_{s} ⊆^{•}s∧Z_{s}^{•}(s)≥^{•}Y(s)−I(s)

⇔ ∀Y ⊆X. ∀s∈S_{Y} . X^{•}(s) ≥ ^{•}Y (s) − I(s)

⇔ ∀Y ⊆X. ∀s∈S. (Y ⊆s^{•} ⇒ X^{•}(s) ≥ ^{•}Y (s) − I(s))

⇔ ∀s∈S. ∀Y ⊆X. X^{•}(s) ≥ ^{•}Y (s) − I(s)

⇔ ∀s∈S. X^{•}(s) ≥ ^{•}X(s) − I(s)

⇔ M_{X} ≥ 0 ⇔ X ∈ C(N). □

The size of T (N) and E(N) can be reduced by redefining ^{n}s to consist of the minimal subsets X of ^{•}s with X^{•}(s) ≥ n. This does not affect the truth of Propositions 1.4 and 1.5, although it slightly complicates their proofs. Likewise, in the definition of T (N) only those formulae ⋀ Y ⇒ φ_{s}^{^{•}Y (s)−I(s)} are needed for which ^{•}Y (s) − I(s) > 0 (the remaining formulae being tautologies). This yields the maps of [13].

1-Unfolding

Below we show that the restriction to 1-occurrence nets is not very crucial; every net can be “unfolded” into a 1-occurrence net without changing its behaviour in any essential way. However, the unfolding cannot be configuration equivalent to the original, as the identity of transitions cannot be preserved.

Definition 1.18 Let N = ^{/}_{\}S, T, F, I^{\}_{/} be a Petri net. Its 1-unfolding N′ := ^{/}_{\}S′, T′, F′, I′^{\}_{/} into a 1-occurrence net is given by (for s ∈ S, t ∈ T, u, u′ ∈ T′)

2In case N is without arcweights, ^{•}Y(s) is simply |Y | (cf.[13]).

• T′ := T × IN,

• S′ := S ∪ (T′ × {∗}),

• F′(s, (t, n)) := F (s, t) and F′((t, n), s) := F (t, s),

• F′(u, (u, ∗)) = F′((u, ∗), u′) = F (u′, (u, ∗)) := 0 and F′((u, ∗), u) := 1 for u, u′ ∈ T′ with u ≠ u′,

• I′(s) := I(s) and I′((u, ∗)) := 1.

Thus, every transition is replaced by countably many copies, each of which is connected with its environment (though the flow relation) in exactly the same way as the original. Furthermore, for every such copy u an extra place (u, ∗) is created, containing one initial token, and having no incoming arcs and only one outgoing arc, going to u. This place guarantees that u can fire only once.

•

•

•

. . .

A net fragment and its 1-unfolding

We argue that the causal and branching time behaviour of the represented system is preserved under 1-unfolding. When dealing with labelled Petri nets, all copies (t, n) of a transition t carry the same label as t. In this setting, common semantic equivalences like the fully concurrent bisimulation equivalence [3] or the (hereditary) history preserving bisimulation equivalence [10] under either the individual or collective token interpretation identify a net and its 1-unfolding.

Note that the construction above does not introduce self-loops. Thus unfoldings of pure nets remain pure. We therefore have translations between arbitrary pure nets, event structures, configuration structures and propositional theories, as indicated in the introduction.

It is possible to give a slightly different interpretation of nets, namely by excluding transitions from firing concurrently with themselves (cf. [14]).^{3} This amounts to simplifying Definition 1.10 by requiring U to be a set rather than a multiset. Under this interpretation our unfolding could introduce concurrency that was not present before. However, for this purpose Definition 1.18 can be adapted by removing the initial tokens from the places ((t, n), ∗) for t ∈ T and n > 0 (but leaving the token in ((t, 0), ∗)), and adding an arc from transition (t, n) to place ((t, n + 1), ∗) for every t ∈ T and n ∈ IN.

2 Computational interpretation

In this section we formalise the dynamic behaviour of configuration structures, Petri nets and event structures, by defining a transition relation between their configurations. This transition relation tells how a represented system can evolve from one state to another. We prove that on the classes of pure 1-occurrence nets and pure event structures the translations of Section 1 preserve these transition relations, and show that this result does not extend to impure 1-occurrence nets or impure event structures.

We indicate that impure nets and event structures may be captured by considering configuration structures upgraded with an explicit transition relation between their configurations. However, the methodology of the present paper is incapable of providing transition preserving translations between general event structures, 1-occurrence nets and the upgraded configuration structures. It is for this reason that we focus on pure nets and pure event structures.

Our transition relation for Petri nets is derived directly from the firing rule, which constitutes the standard computational interpretation of nets. The idea of explicitly defining a transition relation between the configurations of an event structure may be new, but we believe that our transition relation is the only natural candidate that is consistent with the notion of configuration employed in Winskel [34, 35] (cf. Sections 3 and 4). Our transition relation on configuration structures is chosen so as to match the ones on nets and on event structures, and formalises a computational interpretation of configuration structures which we call the asynchronous interpretation.

We briefly discuss two alternative interpretations of configuration structures, formalised by alternative transition relations. The first is the computational interpretation of Chu spaces from Gupta & Pratt [18, 17, 29]. The second is a variant of our asynchronous interpretation, based on the assumption that only finitely many events can happen in a finite time. This finitary asynchronous interpretation matches the standard computational interpretation of Petri nets better than does the asynchronous interpretation, although it falls short in explaining uncountable configurations of event structures [34, 35]. We point out some problems that stand in the way of lifting the computational interpretation of nets to the infinitary level.

3This distinction is independent of the individual–collective token dichotomy, thus yielding four computational interpretations of nets [9].

2.1 The asynchronous interpretation

Definition 2.1 Let C = ^{/}_{\}E, C^{\}_{/} be a configuration structure. For x, y in C write x ⟶_{C} y if x ⊆ y and

∀Z(x ⊆ Z ⊆ y ⇒ Z ∈ C).

The relation ⟶_{C} is called the step transition relation.

Here x ⟶_{C} y indicates that the represented system can go from state x to state y by concurrently performing a number of events (namely those in y − x). The first requirement is unavoidable. The second one says that a number of events can be performed concurrently, or simultaneously, only if they can be performed in any order. This requirement represents our postulate that different events do not synchronise in any way; they can happen in one step only if they are causally independent. Hence our transition relation ⟶_{C} and the corresponding computational interpretation of configuration structures is termed asynchronous.

The single-action transition relation ⟶_{C}^{1} on C ×C is given by x ⟶_{C}^{1} y iff x ⊆ y and y − x is a singleton. In pictures we omit transitions of the form x ⟶_{C} x, that exists for every configuration x, we indicate the single-action transition relation by solid arrows, and the rest of the step transition relation by dashed ones.

Example 7 These are the transition relations for D = ({d, e}, {∅, {d}, {e}, {d, e}}) and two structures E and F.

[figure: ∅; {d}; {e}; {d, e}; D; ∅; {d}; {e}; {d, f}; {e, f}; {d, e, f}; E; ∅; {d}; {e}; {d, f}; {e, f′}; {d, e, f}; {d, e, f′}; F]

Such pictures of configuration structures are somewhat misleading representations, as they suggest a notion of global time, under which at any time the represented system is in one of its states, moving from one state to another by following the transitions. Although this certainly constitutes a valid interpretation, we favour a more truly concurrent view, in which all events can be performed independently, unless the absence of certain configurations indicates otherwise. Under this interpretation, the configurations can be thought of as possible states the system can be in, from the point of view of a possible observer. They are introduced only to indicate (by their absence) the dependencies between events in the represented system.

In particular, in the structure D above, the events d and e are completely independent, and there is no need to assume that they are performed either simultaneously or in a particular order. The “diagonal” in the picture serves merely to remind us of the independence of these events. In terms of higher dimensional automata [28] it indicates that “the square is filled in”.

On the other hand, the absence of any “diagonals” in E indicates two distinct linearly ordered computations. In one the event f can only happen after event d, and e in turn has to wait for f; the other has a causal ordering e < f < d. There is no way to view d and e as independent; if there were, there should be a transition ∅ ⟶_{C} {d, e}. In labelled versions of configuration structures, a computationally motivated semantic equivalence would identify the structures E and F, provided the events f and f′ carry the same label. We do not address such semantic equivalences in this paper, however.

The configuration structure E is completely axiomatised by the two clauses

f ⇒ d ∨ e
d ∧ e ⇒ f

indicating the absence of configurations {f} and {d, e}, respectively. On the other hand, D has the empty axiomatisation. An event structure representing D is given by the enabling relation ∅ ⊢ ∅, ∅ ⊢ {d}, ∅ ⊢ {e} and ∅ ⊢ {d, e}, whereas an enabling relation for E is ∅ ⊢ ∅, ∅ ⊢ {d}, ∅ ⊢ {e}, {d} ⊢ {f}, {e} ⊢ {f}, ∅ ⊢ {d, f}, ∅ ⊢ {e, f}, {f} ⊢ {d, e} and ∅ ⊢ {d, e, f}. Petri net representations of D and E are given below.

• d  •e D  • d •  f  e  • E

Example 8 Take the system G, represented below as a configuration structure with a transition relation, a propositional theory, an event structure and a Petri net. There is no need to assume, as following the transitions might suggest, that in any execution of G the event d happens either after e or before f; when actions may have a duration, d may overlap with both e and f. The configuration structure, with its step transition relation, is not meant to order d with respect to e and f. All it does is specify that f comes after e, and it does so by not including configurations {f} and {d, f}. This is concisely conveyed by the representation of G as a propositional theory in conjunctive normal form.

[figure: ∅; {d}; {e}; {d, e}; {e, f}; {d, e, f}; G; f ⇒ e; E = {d, e, f}; {e} ⊢ {f}; ∅ ⊢ X for X ≠ {f}] • d  •e f

2.2 Petri nets

The firing relation between markings induces a transition relation between the configurations of a net:

Definition 2.2 The step transition relation ⟶_{N} between the configurations x, y of a net N is given by

x ⟶_{N} y ⇔ (x ≤ y ∧ M_{x} ⟶^{y−x} M_{y}).

We now show that on pure 1-occurrence nets this step transition relation matches the one on configuration structures defined above.

Proposition 2.1 In a pure net N we have

x ⟶_{N} y iff x ≤ y ∧ ∀Z(x ≤ Z ≤ y ⇒ Z ∈ C(N))

for all x, y in C(N). (In case N is a pure 1-occurrence net, the right-hand side can be written as x ⟶_{C(N)} y.)

Proof: “Only if”: Let x ⟶_{N} y for x, y ∈ C(N). Then M_{x} = I −^{•}x + x^{•} ≥ 0 and y − x is enabled under M_{x}, i.e., ^{•}(y − x) ≤ M_{x}. Now let x ≤ Z ≤ y. Then •(Z − x) ≤ ^{•}(y − x) ≤ M_{x}, so

M_{Z} \begin{matrix}= I −^{•}Z + Z^{•} = I −^{•}x + x^{•} −^{•}(Z−x) + (Z−x)^{•} \\ = M_{x} −^{•}(Z−x) + (Z−x)^{•} ≥ 0 + (Z−x)^{•} ≥ 0, \end{matrix}

i.e., Z is a configuration of N. Note that for this direction pureness is not needed.

“If”: Suppose x, y ∈C(N) and x≤y, but x −̸→_{N} y. Then y − x is not enabled under M_{x}, i.e., there is a place s ∈ S, such that ^{•}(y − x)(s) > M_{x}(s). Let U be the multiset of those transitions t in y − x for which F (s, t) > 0. Then ^{•}U(s) = ^{•}(y − x)(s) > M_{x}(s). As N is pure, for all transitions t∈U we have F (t, s) = 0, i.e., U^{•}(s) = 0. Hence

M_{(x+U)}(s) = M_{x}(s) −^{•}U(s) + U^{•}(s) < 0,

i.e., x + U ∉ C(N). Yet x ≤ (x + U) ≤ y. □

It follows that the step transition relation on a pure net N is completely determined by the set of configurations of N, and that for pure 1-occurrence nets this transition relation exactly matches the one of Definition 2.1. This makes C(N) an acceptable abstract representation of a pure 1-occurrence net N.

On an impure net N the step transition relation is in general not determined by the set of configurations of N. The 1-occurrence nets P and M below have very different behaviour: in P the transitions d and e can be done in parallel (there is a transition ∅ ⟶_{P} {d, e}), whereas in M there is mutual exclusion. Yet their configurations are the same: C(P) =

P: • d  •e  M: •  • d  •e

C(M) = {∅, {d}, {e}, {d, e}}. Therefore it is not a good idea to represent each 1-occurrence net N = ^{/}_{\}S, E, F, I^{\}_{/} by the configuration structure ^{/}_{\}E, C(N)^{\}_{/}.

2.3 Event structures

Definition 2.3 The step transition relation ⟶_{E} between configurations x, y ∈ L(E) of an event structure E = ^{/}_{\}E, ⊢^{\}_{/} is given by

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

This formalises the intuition provided in Section 1.3. The following proposition says that for pure event structures this transition relation also exactly matches the one of Definition 2.1.

Proposition 2.2 Let E be a pure event structure, and x, y ∈ L(E). Then x ⟶_{E} y iff x ⟶_{L(E)} y.

Proof: We have to establish that

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

“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 1.4, ∃W ⊆ x ∪ Z. W ⊢ Z. As E is pure, W ∩ Z = ∅, hence W ⊆ x, as required. □

This makes L(E) an acceptable abstract representation of a pure event structure E.

As for Petri nets, Proposition 2.2 does not generalise to impure event structures, with again the systems P and M serving as a counterexample. An event structure representation for M is ^{/}_{\}E, ⊢^{\}_{/}, with E = {d, e} and ⊢ given by ∅ ⊢ ∅, ∅ ⊢ {d}, ∅ ⊢ {e}, {d} ⊢ {d, e} and {e} ⊢ {d, e}. Another counterexample is the event structure, say H, of Example 3. The transition relations of P, M and H are

[figure: ∅; {d}; {e}; {d, e}; P:; ∅; {d}; {e}; {d, e}; M:; ∅; {d}; {e}; {d, e}; H:]

2.4 The impure case

In order to provide an adequate abstract representation of impure 1-occurrences nets or impure event structures one could use triples ^{/}_{\}E, C, →^{\}_{/} with ^{/}_{\}E, C^{\}_{/} a configuration structure and → ⊆ C ×C an explicitly defined transition relation between its configurations. To capture arbitrary Petri nets one could further allow the configurations to be multisets of events, rather than sets.

Definition 2.4 A multiset transition system is a triple ^{/}_{\}E, C, →^{\}_{/} with E a set, C ⊆ IN^{E} a collection of multisets over E and → ⊆ C × C.

For a configuration structure C = ^{/}_{\}E, C^{\}_{/}, an event structure E = ^{/}_{\}E, ⊢^{\}_{/} and a Petri net N = ^{/}_{\}S, T, F, I^{\}_{/}, the associated multiset transition system is given by C^{+}(C) := ^{/}_{\}E, C, ⟶_{C}^{\}_{/}, C^{+}(E) := ^{/}_{\}E, L(E), ⟶_{E}^{\}_{/} and C^{+}(N) := ^{/}_{\}T, C(N), ⟶_{N}^{\}_{/}, respectively.

Two structures K and L that may be configuration structures, event structures and/or Petri nets are transition equivalent if C^{+}(K) = C^{+}(L).

By Propositions 2.1 and 2.2, for pure 1-occurrence nets transition equivalence coincides with configuration equivalence, and for pure event structures it coincides with L-equivalence.

We conjecture that there exist maps between 1occurrence nets and event structures that preserve transition equivalence. However, the set-up of the present paper, that uses propositional theories up to logical equivalence as a stepping stone in the translation from event structures to Petri nets, is insufficient to establish this beyond the pure case. It is for this reason that we focus on pure nets and pure event structures.

2.5 The Gupta-Pratt interpretation

Our configuration structures are, up to isomorphism, the extensional Chu spaces of Gupta & Pratt [18, 17, 29]. It was in their work that the idea arose of using the full generality of such structures in modelling concurrency. It should be noted however that the computational interpretation they give in [18, 17, 29] differs somewhat from the asynchronous interpretation above; it can be formalised by means of the step transition relation given by x ⟶_{C} y ⇔ x ⊆ y [18, 29], thereby dropping the asynchronicity requirement of Definition 2.1. This allows a set of events to occur in one step even if they cannot happen in any order. When using the translations between configuration structures and Petri nets described in Section 1.4, the Gupta-Pratt interpretation of configuration structures matches a firing rule on Petri nets characterised by the possibility of borrowing tokens during the execution of a multiset of transitions: a multiset U of transitions would be enabled under a marking M when M′ := M −^{•}U + U^{•} ≥ 0. In that case U can fire under M, yielding M′. Thus the requirement that ^{•}U ≤ M is dropped; tokens that are consumed by the transitions in U may be borrowed when not available in M, as long as they are returned “to the bank” when reproduced by the firing of U.

Example 9 The configuration structure C = ^{/}_{\}E, C^{\}_{/} with E = {a, b, c} and C = {∅, {a}, {b}, {a, b, c}} models a system in which the events a and b jointly cause c as their immediate effect, as it is impossible to have done both a and b without doing c also. Below are the representations of the same system as a propositional theory, an event structure and a Petri net.

c ⇔ a ∧ b
{a, b} ⊢ {c}
{c} ⊢ {a, b}

∅ ⊢ X for any X with {c} ≠ X ≠ {a, b}

• a •b •c•

It takes the Gupta-Pratt interpretation to obtain the transitions {a} ⟶_{C} {a, b, c} and {b} ⟶_{C} {a, b, c}, because under the asynchronous interpretation the configuration {a, b, c} is unreachable.

2.6 Finite vs. infinite steps

In [12] we employed a variant of the transition relation of Definition 2.1, obtained by additionally requiring, for x ⟶_{C} y, that y − x be finite. This transition relation can be motivated computationally by the assumption that only finitely many events can happen in a finite amount of time.

In the present paper the asynchronous computational interpretation of configuration structures given in Section 2.1 will be our default; we refer to the interpretation of [12] as the finitary asynchronous interpretation, and denote the associated transition relation by ⟶^{f}.

The step transition relations ⟶^{f} and ⟶ on the configurations of Petri nets coincide; however, this is merely a spin-off of considering only finite configurations of nets. It would be more accurate to recognise the step transition relation of Section 1.4, defined between markings, and the inherited step transition relation between configurations, as finitary ones.

It is tempting to generalise the firing rule of Definition 1.10 to infinite multisets. The simplest implementation of this idea, however, yields infinitary

markings, as illustrated in Figure 3. After all transi- I: _{•}_{t_{0}}  _{•}_{t_{1}}  _{•}_{t_{2}}  _{•}_{t_{3}} ⋯_{s}  _{L:} _{∞}_{t}_{•}_{t_{0}}  _{•}_{t_{1}}  _{•}_{t_{2}}  _{•}_{t_{3}} ⋯_{J:} _{•}_{t_{0}}  _{•}_{t_{1}}  _{•}_{t_{2}}  _{•}_{t_{3}} ⋯_{t}_{K:}

Figure 3: Unbounded parallelism

tions t_{i} (i ∈ IN) of net I have fired (in one step) there are infinitely many tokens in place s, contrary to the definition of a marking. One way to fix this problem is to allow infinite markings. This, however, causes the problem illustrated by the net L: after transition t has fired countably often, are there tokens left to fire once more? Such problems appear best avoided by sticking to finitary markings. Another solution is to allow a multiset of transitions to fire only if by doing so none of its postplaces receives an infinite amount of tokens. This would enable any finite multiset over {t_{i} | i ∈ IN} to fire initially, but no infinite one. A disadvantage of this solution is that the nets I and J, which normally would be regarded equivalent, have now a different behaviour, as in J all transitions t_{i} can still fire in one step. As a consequence, the theorem of [12] that any net is step bisimulation equivalent to a safe net, or a prime event structure, would no longer hold; I constitutes a counterexample.

Therefore we stick in this paper to the convention, formalised by Definition 1.10, that only finitely many transitions can fire in a finite time. As a consequence, the transition t in net K can never fire and this net is semantically equivalent to I and J.

3 Four notions of equivalence

In this paper we compare configuration structures, pure event structures and pure 1-occurrence nets up to four notions of equivalence, the finest one of which is configuration equivalence. Two such structures are configuration equivalent iff they have the same events and the same configurations (taking the left-closed configurations of pure event structures). By Propositions 2.1 and 2.2 this implies that they also have the same step transition relation between their configurations. On pure 1-occurrence nets configuration equivalence is defined in Definition 1.14, on pure event structures it is defined in Definition 1.4 under the name L-equivalence and for configuration structures it is the identity relation. However, we can also compare nets with event structures, or any other combinations of models, up to configuration equivalence. The other three equivalence relations are obtained by restricting attention to the configurations that are finite, reachable, or both, as we now see.

Definition 3.1 Let C = ^{/}_{\}E, C^{\}_{/} be a configuration structure. A configuration x ∈ C is reachable if there is a sequence of configurations

∅ = x_{0} ⟶_{C} x_{1} ⟶_{C} … ⟶_{C} x_{n} = x.

Let R(C) denote the set of reachable configurations and F (C) the set of finite configurations of C. The reachable part of C is given by R(C) := ^{/}_{\}E, R(C)^{\}_{/} and the finite part by F(C) := ^{/}_{\}E, F (C)^{\}_{/}.

A configuration structure C is connected if all its configurations are reachable, i.e., if R(C) = C. It is finitary if its configurations are finite, i.e., if F(C) = C.

Two configuration structures C and D are

• configuration equivalent if C = D;

• finitarily equivalent if F(C) = F(D)—cf. Def. 1.16;

• reachably equivalent if R(C) = R(D); and

• finitarily reachably equivalent if R(F(C))=R(F(D)). For E a pure event structure let C(E) be L(E), and for C a configuration structure let C(C) be C. Two structures K and L that may be configuration structures, pure event structures or pure 1-occurrence nets are called configuration equivalent if the configuration structures C(K) and C(L) are configuration equivalent. The other three equivalences lift to general pure structures in the same way.

Proposition 3.1 Let C = ^{/}_{\}E, C^{\}_{/} be a configuration structure, x ∈ R(C) and Y ⊆ E. Then x ⟶_{R(C)} Y iff x ⟶_{C} Y.

Proof: Let x ∈ R(C) and Y ⊆ E. Then, x ⟶_{C} Y iff (by Definition 2.1) x ⊆ Y ∧ ∀Z(x ⊆ Z ⊆ Y ⇒ Z ∈ C) iff x ⊆ Y ∧ ∀Z. ∀W (x ⊆ W ⊆ Z ⊆ Y ⇒ W, Z ∈ C) iff x ⊆ Y ∧ ∀Z(x ⊆ Z ⊆ Y ⇒ (Z ∈ C ∧ x ⟶_{C} Z)) iff x ⊆ Y ∧ ∀Z(x ⊆ Z ⊆ Y ⇒ Z ∈ R(C)). □

In particular (taking Y ∈ R(C) above), the step transition relation on R(C) is exactly the step transition relation on C restricted to the reachable configurations of C. Likewise, the step transition relation on F(C) is exactly the step transition relation on C restricted to the finite configurations of C.

Proposition 3.2 For any configuration structure C one has R(R(C)) = R(C), F(F(C)) = F(C) and F(R(C)) = R(F(C)).

Proof: Straightforward, for the first statement using Proposition 3.1. □

Thus, any reachable equivalence class of configuration structures contains exactly one connected configuration structure, which can be obtained as the reachable part of any member of the class. Likewise, any finitary equivalence class of configuration structures contains exactly one finitary configuration structure, which can be obtained as the finite part of any member of the class. Finally, any finitary reachable equivalence class of configuration structures contains exactly one configuration structure that is both finitary and connected; it can be obtained as the reachable part of the finite part of any member of the class.

By definition, C(N) is finitary for any pure 1occurrence net N. Hence on pure 1-occurrence nets, finitary equivalence coincides with configuration equivalence, and finitary reachable equivalence with reachable equivalence.

If in Definition 3.1 we would have defined reachability in terms of the step transition relation formalising the Gupta-Pratt interpretation of configuration structures (cf. Section 2.5), either all or no configurations of a configuration structure C would be reachable, depending on whether or not C is rooted. If we would use the step transition relation ⟶^{f} formalising the finitary asynchronous interpretation (cf. Section 2.6), what we would get as R(C) is actually R(F(C)).

When dealing with systems that merely take a finite number of transitions in a finite amount of time, only their reachable parts are semantically relevant. In this setting it makes sense to study configuration structures, pure event structures and pure 1-occurrence nets up to reachable equivalence. When moreover assuming that only finitely many actions can happen in a finite amount of time, it even suffices to work up to finitary reachable equivalence.

Clearly, reachable equivalence is coarser than configuration equivalence. The following example illustrates for event structures that this is strictly so.

Example 10 Let E = ^{/}_{\}E, ⊢^{\}_{/} be the event structure with as events the set ^{|}Q of rational numbers, ∅ ⊢ X for any X with |X| ≠ 1, and X ⊢ {e} iff X = {d ∈ ^{|}Q | d < e}. Then L(E) consists of all downwards closed subsets of rational numbers and thus contains representatives of all reals as well as extra copies of the rationals and ^{|}Q itself (infinity); however R(L(E)) = {∅}. So if F is ^{/}_{\} ^{|}Q, {∅ ⊢∅}^{\}_{/} then E and F are reachably equivalent, yet L(E) ≠ L(F).

This example also illustrates that the justification of working up to reachable equivalence depends on the precise computational interpretation of event structures.

We have established the bijective correspondences between configuration structures, propositional theories, pure event structures and pure 1-occurrence nets up to the finest semantic equivalence possible. This way our correspondences are compatible, for instance, with the Gupta-Pratt interpretation of configuration structures. Under this interpretation, unreachable configurations may be semantically relevant, as witnessed by the notions of causality and internal choice in [18, 29] (see Example 9) and that of history preserving bisimulation in [17].

3.1 Hyperreachability

Below we consider a class of SR-secure configuration structures, on which we define the hyperconnected configuration structures as alternative canonical representatives of reachable equivalence classes, and we propose a function S that transforms each SR-secure configuration structure into an alternative normal form: the unique hyperconnected configuration structure inhabiting a reachable equivalence class of SR-secure configuration structures. We also show that the function S ∘ F transforms each configuration function into an alternative canonical representation of its finitary reachable equivalence class. As we will show in Section 4, it is the function S that generalises the notion of configuration employed in Winskel [34, 35].

Definition 3.2 Let C = ^{/}_{\}E, C^{\}_{/} be a configuration structure. A set of events X ⊆ E is hyperreachable, or a secured configuration of C, if X = ⋃_{i=0}^{∞} x_{i} for an infinite sequence of configurations

∅ = x_{0} ⟶_{C} x_{1} ⟶_{C} x_{2} ⟶_{C} ….

Let S(C) be the set of secured configurations of C, and write S(C) := ^{/}_{\}E, S(C)^{\}_{/}. The structure C is hyperconnected if S(C) = C.

The secured configurations include the reachable ones (just take x_{i} = x_{n} for i > n). Whereas reachable configurations could be regarded as modelling possible partial runs of the represented system,^{4} happening in a finite amount of time, secured configurations additionally model possible total runs, happening in an unbounded amount of time.

Proposition 3.3 Let C be a configuration structure. Then S(C) = S(R(C)) and R(C) ⊆ R(S(C)).

Proof: The first statement follows immediately from Proposition 3.1; the second holds because ⟶_{R(C)} ⊆ ⟶_{S(C)}. □

However, it is not always true that R(S(C)) = R(C).

Example 11 Take E:=IN and C:=𝒫_{fin}(IN) consisting of all finite subsets of IN. Then S(C) = 𝒫(IN) and in the configuration structure S(C) one has ∅ ⟶_{S(C)} X for every X ⊆ IN. Thus R(S(C)) = 𝒫(IN), whereas R(C) = 𝒫_{fin}(IN).

It is also not always the case that S(S(C)) = S(C); finding a counterexample is left as a puzzle for the reader. The problem underlying Example 11 is that the induced step transition relation on S(C) may differ from the one on C, even when restricting attention to transitions originating from reachable configurations of C (and hence of S(C)). Thus the map S may alter the computational interpretation of configuration structures as proposed in Section 2. We now characterise the class of configuration structures for which this does not happen.

Definition 3.3 A configuration structure C is SRsecure iff R(S(C)) = R(C).

Observation 3.1 A configuration structure C=^{/}_{\}E,C^{\}_{/} is SR-secure iff for all x∈R(C) and all Y ⊆ E one has x ⟶_{S(C)} Y iff x ⟶_{C} Y.

A configuration structure C = ^{/}_{\}E, C^{\}_{/} with S(C) ⊆ C, i.e., for which all its secured configurations are in fact configurations, is certainly SR-secure. Proposition 3.3 yields:

Proposition 3.4 Let C be an SR-secure configuration structure. Then S(S(C)) = S(C), i.e., S(C) is hyperconnected. □

If a configuration structure C is SR-secure, then so are R(C) and S(C). However, it is not the case that F(C) is always SR-secure when C is; a counterexample is the SR-secure configuration structure C := ^{/}_{\}IN, 𝒫(IN)^{\}_{/}: here F(C) is the SR-insecure configuration structure of Example 11.

Proposition 3.5 Let C and D be SR-secure configuration structures. Then R(C) = R(D) iff S(C) = S(D).

Proof: It follows from Proposition 3.3 that S(C) is completely determined by R(C), whereas by Definition 3.3 R(C) is completely determined by S(C). □

Proposition 3.5 says that two SR-secure configuration structures are reachable equivalent iff they have the same secured configurations. Thus, in any reachable equivalence class of SR-secure configuration structures there are two normal forms: a connected configuration structure that can be obtained as R(C) for C an arbitrary member of the class, and a hyperconnected configuration structure that can be obtained as S(C) for C an arbitrary member of the class. In the sequel we will often use the normal form S when dealing with event structures, as our notion of a secured configuration of an event structure is the one that generalises the notion of configuration of [34, 35].

Example 11 shows that for C an SR-insecure configuration structure, S(C) need not be reachable equivalent with C. Therefore, when working up to reachable equivalence, we will not study the configuration structures S(C) for SR-insecure C. However, this restriction is not needed when working up to finitary reachable equivalence, as we will show below.

Proposition 3.6 Let C be a configuration structure. Then F(S(C)) = F(R(C)).

Proof: That any finite secured configuration is reachable follows directly from Definition 3.2, whereas “⊇” follows from the earlier observation that S(C) ⊇ R(C). □

Proposition 3.7 Let C be a configuration structure. Then R(F(S(C))) = R(F(C)), i.e., S(C) is finitarily reachably equivalent with C.

Proof: R(F(S(C))) =^{3.6} R(F(R(C))) =^{3.2} R(F(C)). □

Proposition 3.8 For configuration structures C, D:

R(F(C)) = R(F(D)) iff S(F(C)) = S(F(D)).

4The idea of a configuration modelling a possible partial run is consistent with the idea that it also models a possible state of the represented system, namely the state obtained after executing all the events that make up the run.

Proof: It follows from Proposition 3.3 that S(F(C)) is completely determined by R(F(C)), whereas Propositions 3.2 and 3.6 (or 3.7) imply that R(F(C)) is completely determined by S(F(C)). □

Thus, in any finitary reachable equivalence class of configuration structures there are two normal forms: a finitary and connected configuration structure that can be obtained as R(F(C)) for C an arbitrary member of the class, and a configuration structure that can be obtained as S(F(C)) for C an arbitrary member of the class.

3.2 Petri nets

In this section we directly define the reachable configurations of a Petri net, and observe that for pure 1-occurrence nets this definition agrees with Definition 3.1. Moreover, we infer that finitary, connected rooted configurations structures are canonical representatives of equivalence classes of nets that have the same reachable configurations.

Definition 3.4 The set R(N) of reachable configurations of a Petri net N = ^{/}_{\}S, T, F, I^{\}_{/} consists of the multisets Σ_{i=1}^{n}U_{n} such that there is a firing sequence

I ⟶^{U_{1}} M_{1} ⟶^{U_{2}} ⋯ ⟶^{U_{n}} M_{n}.

In case N = ^{/}_{\}S, E, F, I^{\}_{/} is a pure 1-occurrence net, we write R(N) := ^{/}_{\}E, R(N)^{\}_{/}.

Proposition 3.9 If N is a pure 1-occurrence net, then R(N) = R(C(N)).

Proof: Immediate from Definitions 3.1 and 2.2, using Proposition 2.1. □

The configuration structure R(N) is always rooted, finitary and connected. Moreover, combining Proposition 3.9 with Corollary 1 yields:

Proposition 3.10 For every rooted, finitary and connected configuration structure C there exists a pure 1-occurrence net N without arcweights, such that R(N) = C. □

Thus, we have established a bijective correspondence between pure 1-occurrence nets (with or without arcweights) up to reachable equivalence and finitary, connected, rooted configuration structures.

3.3 Event structures

In this section we define the four notions of configuration S, R, R ∘ F and S ∘ F directly on event structures, and observe that for pure event structures these definitions agree with Definitions 3.1 and 3.2. In Section 4 we will show that our secured configurations generalise the configurations of the event structures that appear in Winskel [34, 35]. As the family of all configurations of an event structure from [34, 35] is completely determined by the subfamily of its finite configurations, in [11] attention has been restricted to finite configurations only. A generalisation of these finite configurations to the event structures of this paper are our finite reachable configurations below.

Definition 3.5 The set S(E) of secured configurations of an event structure E = ^{/}_{\}E, C^{\}_{/} consists of the sets of events ⋃_{i=0}^{∞} X_{i} with X_{0} = ∅ such that

∀i ∈ IN. X_{i} ⊆ X_{i+1} ∧ ∀Y ⊆ X_{i+1}. ∃Z ⊆ X_{i}. Z ⊢ Y.

The set R(E) of reachable configurations of E consists of the sets of events ⋃_{i=0}^{n} X_{i} with X_{0} = ∅ such that

∀i < n. X_{i} ⊆ X_{i+1} ∧ ∀Y ⊆ X_{i+1}. ∃Z ⊆ X_{i}. Z ⊢ Y.

The set R_{f}(E) of finite reachable configurations of E consists of the sets of events {e_{1}, …, e_{n}} such that

∀i ≤ n. ∀Y ⊆ {e_{1}, ..., e_{i}}. ∃Z ⊆ {e_{1}, ..., e_{i−1}}. Z ⊢ Y.

Finally, the set S_{f}(E) extends R_{f}(E) with the infinite sets of events {e_{1}, e_{2}, …} such that

∀i ∈ IN. ∀Y ⊆ {e_{1}, ..., e_{i}}. ∃Z ⊆ {e_{1}, ..., e_{i−1}}. Z ⊢ Y.

The secured configuration structure associated to E is S(E) := ^{/}_{\}E, S(E)^{\}_{/}. Likewise, let R(E) := ^{/}_{\}E, R(E)^{\}_{/}, R_{f}(E) := ^{/}_{\}E, R_{f}(E)^{\}_{/} and S_{f}(E) := ^{/}_{\}E, S_{f}(E)^{\}_{/}. An event structure E is SR-secure iff R(S(E))=R(E).

Thus X ∈ S(E) iff X = ⋃_{i=0}^{∞} X_{i} for a sequence

∅ = X_{0} ⟶_{E} X_{1} ⟶_{E} X_{2} ⟶_{E} …

and likewise for R(E). Again, the secured configurations include the reachable ones (just take X_{i} := X_{n} for i > n). We call a sequence X_{0}, X_{1}, … as occurs in the definitions of S(E) and R(E) a stepwise securing of X; a sequence e_{1}, e_{2}, … as occurs in the definitions of R_{f}(E) and S_{f}(E) is an eventwise securing of X. Computationally, a stepwise securing can be understood to model a particular run of the represented system by partitioning time in countably many successive intervals I_{k} (k ≥ 1). The set X_{k} −X_{k−1} contains the events that occur in the interval I_{k}. These events must be enabled by events occurring in earlier intervals. The set X contains all events that happen during such a run. An eventwise securing can be understood by imposing the restriction that |X_{k} −X_{k−1}| = 1, i.e., in each interval exactly one event takes place. We now show that R_{f}(E) consists of the finite configurations in R(E).

Proposition 3.11 Let E be an event structure. Then R_{f}(E) = F(R(E)) = F(S(E)).

Proof: Given X ∈ R_{f}(E), let e_{1}, …, e_{n} be an eventwise securing of X. Take X_{i} := {e_{1}, …, e_{i}} for i = 0, 1, …, n. Then X_{0}, …, X_{n} is a stepwise securing of X. As X is finite we have X ∈ F (R(E)).

Given X ∈ F (R(E)), let X_{0}, …, X_{n} be a stepwise securing of X. Removing duplicate entries (where X_{i−1} = X_{i} with 1 ≤ i ≤ n) from this sequence preserves the property of the sequence being a stepwise securing. Furthermore, if X_{i−1} ⊂ Y ⊂ X_{i} for some 1 ≤ i ≤ n, then adding Y between X_{i−1} and X_{i} also preserves the property of the sequence being a stepwise securing. In this way (using that all X_{i} are finite) the stepwise securing X_{0}, ..., X_{n} can be modified into a stepwise securing Y_{0}, ..., Y_{m} with |Y_{i} − Y_{i−1}| = 1 for i = 1, ..., m. The latter can be written as an eventwise securing.

That F(R(E)) = F(S(E)) is trivial (cf. Pr. 3.6). □

The proof above shows that events cannot be “synchronised” in event structures. If a finite number of events takes place simultaneously, they could just as well have occurred one after the other, in any order.

Proposition 3.12 Let E be a pure event structure. Then R(E) = R(L(E)) and S(E) = S(L(E)). Moreover, R_{f}(E) = R(F(L(E))) and S_{f}(E) = S(F(L(E))).

Proof: The first two statements follow directly from Definitions 3.1, respectively 3.2, and 2.3, using Proposition 2.2. The third statement now follows from Proposition 3.11, the first statement, and Proposition 3.2.

For the last statement, let X ∈ S_{f}(E). In case X is finite, X ∈ R_{f}(E) = R(F(L(E))) ⊆ S(F(L((E))). Otherwise, let e_{1}, e_{2}, … be an eventwise securing of X. Let X_{i}:={e_{1}, …, e_{i}} for i≥0. Then X_{i} ∈ F (L(E)) for i ∈ IN and ∅ = X_{0} ⟶_{L(E)} X_{1} ⟶_{L(E)} X_{2} ⟶_{L(E)} ⋯, so X = ⋃_{i=0}^{∞} X_{i} ∈ S(F(L(E))) by Definition 3.2.

Conversely, let X ∈ S(F(L(E))). Then, by Definition 3.2, X = ⋃_{i=0}^{∞} x_{i} for x_{i} ∈ F (L(E)) (i ∈ IN) such that ∅ = x_{0} ⟶_{L(E)} x_{1} ⟶_{L(E)} x_{2} ⟶_{L(E)} . . .. As in the proof of Proposition 3.11, this sequence can be modified into a finite or infinite sequence y_{i} ∈ F (L(E)) with ∅ = y_{0} ⟶_{L(E)} y_{1} ⟶_{L(E)} y_{2} ⟶_{L(E)} … and |y_{i}−y_{i−1}| = 1 for relevant all i > 0. By Proposition 2.2 we have ∅ = y_{0} ⟶_{E} y_{1} ⟶_{E} y_{2} ⟶_{E} . . .. Writing e_{i} for the unique element of y_{i} − y_{i−1}, for i > 0, Definition 2.3 yields that e_{1}, e_{2}, … is an eventwise securing of X. Hence X = {e_{1}, e_{2}, …} ∈ S_{f}(E). □

Corollary 2 A pure event structure E is SR-secure iff L(E) is an SR-secure configuration structure.

Proof: Let E be pure. If E is SR-secure then

R(S(L(E))) = R(S(E)) = S(E) = S(L((E)). Conversely, if L(E) is SR-secure then

R(S(E)) = R(S(L(E))) = S(L((E)) = S(E). □

Corollary 3 Let E be a pure and SR-secure event structure. Then S(E) is hyperconnected. Conversely, if C is a hyperconnected configuration structure, then E(C) is a pure and SR-secure event structure. □

Using Theorem 2, Proposition 3.12 yields

Proposition 3.13 Let C be a connected configuration structure. Then R(E(C)) = C.

Proof: R(E(C)) = R(L(E(C))) = R(C) = C. □

Likewise, if C is a hyperconnected configuration structure then S(E(C)) = C; if C is a finitary connected configuration structure then R_{f}(E(C)) = C; and if C is a configuration structure of the form S(D) with D a finitary configuration structure then S_{f}(E(C)) = C. Thus R and E provide a bijective correspondence between pure event structures up to reachable equivalence and connected configuration structures (using Proposition 3.12, Definition 3.1, Theorem 2 and the above). Likewise, S and E provide a bijective correspondence between pure and SR-secure event structures up to reachable equivalence and hyperconnected configuration structures (additionally using Corollaries 3 and 2 and Proposition 3.5); R_{f} and E provide a bijective correspondence between pure event structures up to finitary reachable equivalence and finitary connected configuration structures; and S_{f} and E provide a bijective correspondence between pure event structures up to finitary reachable equivalence and configuration structures of the form S(D) with D finitary (additionally using Proposition 3.8).

Impure event structures

Proposition 3.12 does not extend to impure event structures. For those, their reachable configurations are not determined by their left-closed ones.

Example 12 Let E := ^{/}_{\}{e}, {∅ ⊢∅, {e} ⊢{e}}^{\}_{/}. Then L(E) = ^{/}_{\}{e}, {∅, {e}}^{\}_{/}, whereas R(E) = ^{/}_{\}{e}, {∅}^{\}_{/}. Both configuration structures are connected.

Let F := ^{/}_{\}{e}, {∅ ⊢∅, ∅ ⊢{e}}^{\}_{/}. Then we have L(E) = L(F) but R(E) ≠ R(F).

When the step transition relation of Definition 2.3 is taken to be part of the meaning of an event structure, neither the left-closed nor the reachable configurations capture the meaning of impure event structures faithfully, as illustrated by the systems P and M mentioned in Section 2.3. When, on the other hand, the behaviour of an event structure is deemed to be determined by its configurations, then on impure event structures L and R represent mutually inconsistent interpretations. However, under either interpretation the impure event structures are redundant: for every event structure there exists a pure one with the same configurations. Obviously, which one depends on whether the left-closed or the reachable configurations are to be preserved.

Proposition 3.14 For any event structure E there is a pure event structure E_{L} with L(E_{L}) = L(E), and a pure event structure E_{R} with R(E_{R}) = R(E).

Proof: One can take E_{L} to be E(L(E)) and E_{R} to be E(R(E)). □

A structure E_{L} = ^{/}_{\}E, ⊢_{L}^{\}_{/} can also be directly obtained by putting ⊢_{L} := {(X − Y, Y) | X ⊢ Y }.

Proposition 3.14 shows that any event structure could be transformed into a pure one, while preserving its reachable configurations. However, there is no way to purify any event structure while preserving its secured configurations:

Example 13 Let E = ^{/}_{\}E, ⊢^{\}_{/} be given by E := IN∪{e}, {n} ⊢ {n + 1} and {n} ⊢ {e, n} for n ∈ IN and ∅ ⊢ X for X not of the form {n + 1} or {e, n}. Then R(E) = {{i | i < n}, {i | i < n} ∪ {e} | n ∈ IN}, S(E) = R(E)∪{IN} and L(E) = S(E)∪{IN∪{e}}. The configuration IN ∪ {e} is not secured, because countably many stages are needed to perform the events in IN, and whenever both e and n happen, n needs to happen first. Using Proposition 3.12, S(E) cannot be the set of secured configurations of a pure event structure, because S(E) is not of the form S(C): as R(C) would contain all sets {i | i < n}∪{e} for n ∈ IN, S(C) would also contain their limit IN ∪ {e}.

As E above is SR-secure, Example 13 also shows that Corollary 3 does not extend to impure structures.

Reachably pure event structures

For impure event structures, the functions L, R, S, R_{f} and S_{f} do not reflect the step transition relation between configurations and hence may translate an event structure into a configuration structure with a different computational interpretation. This is illustrated by the event structure M of Section 2.3, for which we have ∅ −̸→_{M} {d, e} but ∅ ⟶_{S(M)} {d, e}. We now extend the class of pure event structures to a slightly larger class of reachably pure event structures, on which the functions R, S, R_{f} and S_{f}, but not L, still preserve the computational interpretation of event structures. This extension is necessary in order to cast the event structures of Winskel [34, 35] as special cases of ours, for they translate into our framework as event structures that are reachably pure but not pure.

Definition 3.6 An event structure is reachably pure if X ⊢ Y only if either X ∩ Y = ∅ or Y ⊆ X.

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

Proposition 3.15 For every reachably pure event structure E there exists a pure event structure Ê such that X ⟶Ê Y iff X ⟶_{E} Y for all X ∈ L(Ê) ⊆ L(E) and Y ⊆ E with X ≠ Y. Also, if E is rooted, so is Ê.

Proof: Obtain Ê by omitting all enablings X ⊢ Y with ∅ ≠ Y ⊆ X. Apply Definition 2.3. □

Corollary 4 For any reachably pure event structure E one has R(Ê) = R(E), S(Ê) = S(E), R_{f}(Ê) = R_{f}(E) and S_{f}(Ê) = S_{f}(E). Moreover, Ê is SR-secure iff E is.

However, in Example 12 we have L(Ê) ≠ L(E).

With the above results and Proposition 3.12, all results for configuration structures in this section, namely Propositions 3.1–3.8 and Observation 3.1, lift to reachably pure event structures:

Corollary 5 Let E = ^{/}_{\}E, ⊢^{\}_{/} be a reachably pure event structure, x ∈ R(E) and Y ⊆ E. Then x ⟶_{R(E)} Y iff x ⟶_{E} Y. □

Corollary 6 A reachably pure event structure E = /_{\}E, ⊢^{\}_{/} is SR-secure iff for all x ∈ R(E) and all Y ⊆ E one has x ⟶_{S(E)} Y iff x ⟶_{E} Y. □

Corollary 7 For any reachably pure event structure E it holds that R(R(E)) = R(E), S(R(E)) = S(E), R(E) ⊆ R(S(E)) and F(R(E)) = F(R(S(E))). □

Corollary 8 For any reachably pure and SR-secure event structure E it holds that S(S(E)) = S(E), i.e., S(E) is hyperconnected. □

Corollary 9 Let E and F be reachably pure and SRsecure event structures. Then R(E) = R(F) iff S(E) = S(F). □

Corollary 10 Let E, F be reachably pure event structures. Then R_{f}(E) = R_{f}(F) iff S_{f}(E) = S_{f}(F). □

We call two reachably pure event structures E and F reachably equivalent iff R(E) = R(F) and finitarily reachably equivalent iff R_{f}(E) = R_{f}(F). Restricted to pure event structures these definitions agree with Definition 3.1.

Secure event structures

When dealing with secured configurations, we will mainly be interested in event structures E that are reachable pure and SR-secure, and satisfy S(E) ⊆ L(E). The third property says that all secured configurations of E are in fact left-closed configurations. Together, these three properties ensure that the computational behaviour of E is adequately represented by S(E). An event structure with these properties is called secure.

Proposition 3.16 If C is a hyperconnected configuration structure, then E(C) is secure.

Proof: Hyperconnected configuration structures are SR-secure, so that E(C) is pure and SR-secure follows from Corollary 2. Moreover, using Proposition 3.12, S(E(C)) = S(L(E(C))) = S(C) = C = L(E(C)). □

Thus S and E provide a bijective correspondence between secure event structures up to reachable equivalence and hyperconnected configuration structures.

Remark For reachably pure event structures E, unlike for configuration structures, the requirement S(E) ⊆ L(E) does not imply SR-security. Moreover, this requirement would be insufficient in Corollary 9.

Example 14 Take E := ^{/}_{\}IN, ⊢^{\}_{/} with ∅ ⊢ X for X finite, and X ⊢ X otherwise. This event structure is reachably pure and satisfies S(E) ⊆ L(E). However, R(E) = 𝒫_{fin}(IN), yet R(S(E)) = 𝒫(IN).

Take F := ^{/}_{\}IN, ⊢′^{\}_{/} and ∅ ⊢′ X for all X. The event structures E and F have the same secured configurations, yet are not reachably equivalent.

4 Other brands of event structures

Event structures have been introduced in Nielsen, Plotkin & Winskel [25] as triples ^{/}_{\}E, ≤, #^{\}_{/}, in Winskel [34] as triples ^{/}_{\}E, Con, ⊢^{\}_{/} and ^{/}_{\}E, Con, ≤^{\}_{/}, and in Winskel [35] as triples ^{/}_{\}E, #, ⊢^{\}_{/} and ^{/}_{\}E, #, ≤^{\}_{/} —a special case of those in [25]. Here we will explain how our event structures generalise these previous proposals. The components #, Con, ⊢ and ≤ that occur in the triples mentioned above can be defined in terms of our event structures as follows.

Definition 4.1 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 binary conflict relation # ∈ E × E is given by d#e iff d ≠ e ∧ ¬Con({d, e}). Write fCon(X) for “X is finite and consistent”—this is our rendering of the component Con in [34]. For X ⊆_{fin} E and e ∈ E, write X ⊢_{s} e for

fCon(X) ∧ ∃Y ⊆ X. Y ⊢ {e}.

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 ≺.

The next definition gives various properties of our event structures which, in suitable combinations, determine subclasses corresponding to the various event structures in [25, 34, 35].

Definition 4.2 An event structure E = ^{/}_{\}E, ⊢^{\}_{/} is

• 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,

• S-irredundant if every event occurs in a secured configuration, i.e., E = ⋃_{x∈S(E)} x,

• L-irredundant if every event occurs in a left-closed configuration, i.e., E = ⋃_{x∈L(E)} x,

• 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.

As we will explain below, the event structures of [25, 34, 35] all correspond to event structures in our sense that are rooted, singular and with finite conflict. The event structures given as triples involving # even have binary conflict, the ones from [34, 35] have finite causes, and the ones involving ≤ are conjunctive, L-irredundant and cycle-free. The event structures of [34, 35] that involve ≤ are moreover S-irredundant, a property that implies L-irredundancy and cyclefreeness. The requirement of stability in [34, 35] corresponds to our notion of local conjunctivity.

Each of the correspondences above will be established by means of evident translations from the class of event structures from [25, 34, 35] under consideration to the class of our event structures with the mentioned properties, and vice versa. These translations will preserve the sets of events of related structures as

ev. str. [34] Con, ⊢ rtd, sing, f.causes & f.conflict  S
stable [34] Con, ⊢ same & locally conjunctive  S
prime [34] Con, ≤ same & conjunctive & S-irr.  S, L
ev. str. [35] #, ⊢ rtd, sing, f.causes & bin.conflict S
stable [35] #, ⊢ same & locally conjunctive  S
prime [35] #, ≤ same & conjunctive & S-irr.  S, L
ev. str. [25] #, ≤ rtd, sing, b.c., conj, L-irr & c.-f. L

Table 1: 7 corresponding classes of event structures

well as their configurations. However, which configurations will be preserved varies, as indicated in Table 1. The configurations employed in [34, 35] correspond to our secured configurations, whereas the configurations employed for event structures involving ≤ correspond to our left-closed configurations. In the intersection of those two situations, the secured and left-closed configurations of event structures coincide.

Definition 4.3 An event structure is 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 from ⊢, 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 L-equivalence and even transition equivalence (cf. Definition 2.4) and all properties of Definition 4.2. The event structures in our sense that arise as translations of event structures from [25, 34, 35] that involve ≤ are all manifestly conjunctive.

Observation 4.1 Any singular, cycle-free, manifestly conjunctive event structure is pure.

Hence the translations between the event structures from [25, 34, 35] involving ≤ and subclasses of our event structures will preserve not only L-equivalence, but even transition equivalence.

Lemma 1 If E has finite conflict, then S(E) ⊆ L(E).

Proof: Let X ∈ S(E) and let X_{0}, X_{1}, … be a stepwise securing of X. Let Y ⊆ X. Then either Y is infinite and ∅ ⊢ Y or Y is finite and hence contained in X_{i+1} for some i ∈ IN. In the latter case ∃Z ⊆ X_{i} ⊆ X with Z ⊢ Y. □

Observation 4.2 Any singular event structure is reachably pure.

Proposition 4.1 Any singular event structure with finite conflict is secure.

Proof: Let E be a singular event structure with finite conflict. Then the event structure Ê, as defined in the proof of Proposition 3.15, is pure and with finite conflict. Lemma 1 yields S(Ê) ⊆ L(Ê). Hence, R(S(E)) = R(S(Ê)) ⊆ R(L(Ê)) = R(Ê) = R(E). The other direction follows from Corollary 7. □

As all event structures of [25, 34, 35] correspond to event structures in our sense that are singular and with finite conflict, they all fall in the scope of Corollaries 5 and 9, so reachable equivalence preserves the computational interpretation of event structures and is characterised by having the same secured configurations. Hence the translations between the event structures from [34, 35] and subclasses of our event structures will preserve reachable equivalence. We will show that they also preserve L-equivalence, and even transition equivalence (cf. Definition 2.4); however, this involves defining the left-closed configurations and a transition relation on the structures of [34, 35].

4.1 Left-closed configurations and transitions

For singular event structures E, the enabling relation consists of two parts: enablings of the form ∅ ⊢ Y with |Y | ≠ 1, and enablings of the form X ⊢ {e}. When E has finite conflict, the first part can be fully expressed in terms of fCon, at least to the extent to which it determines which sets of events are configurations. When E has finite causes, the second part can similarly be expressed in terms of ⊢_{s}. One obtains the following.

Observation 4.3 Let E be a singular event structure with finite causes and finite conflict. Then

X ⟶_{E} Y ⇔ \begin{cases}X ⊆ Y ∧ ∀Z ⊆_{fin} Y. fCon(Z) ∧ ^{5} \\ ∀e ∈ Y. ∃W ⊆ X. W ⊢_{s} e. \end{cases}

It follows that such structures can alternatively be represented as triples ^{/}_{\}E, fCon, ⊢_{s}^{\}_{/} with fCon ⊆ 𝒫_{fin}(E) and ⊢_{s} ⊆ fCon × E, as are the structures of [34].

When E moreover is rooted and with binary conflict, fCon, when applied to non-singleton sets, can be fully expressed in terms of #.

Observation 4.4 Let E be a rooted, singular event structure with finite causes and binary conflict. Then

X ⟶_{E} Y ⇔ \begin{cases}X ⊆ Y ∧ ∀d, e ∈ Y. ¬(d#e) ∧ \\ ∀e ∈ Y. ∃W ⊆ X. W ⊢_{s} e. \end{cases}

It follows that such event structures can alternatively be represented as triples ^{/}_{\}E, #, ⊢_{s}^{\}_{/} with # ⊆ E × E symmetric and irreflexive and ⊢_{s} ⊆ fCon × E, as are the structures of [35].

5Note that X ∈ L(E) iff X ⟶_{E} X. Hence, characterisations of ⟶_{E} such as this one entail also characterisations of L(E).

When d ≤ e, any configuration containing e also contains d. When E = ^{/}_{\}E, ⊢^{\}_{/} is conjunctive and satisfies Con({e}) for all e ∈ E, then for any event e ∈ E there is a smallest set X ⊆ E with X ⊢ e. In that case, the part of the enabling relation consisting of enablings X ⊢ e is in essence completely determined by the causality relation ≤.

Observation 4.5 Let E = ^{/}_{\}E, ⊢^{\}_{/} be a singular, conjunctive event structure with finite conflict, such that Con({e}) for all e ∈ E. Then

X ∈ L(E) ⇔ \begin{cases}∀Y ⊆_{fin} X. fCon(Y) ∧ \\ ∀d, e ∈ E. d ≤ e ∈ X ⇒ d ∈ X. \end{cases}

If E moreover is rooted and with binary conflict, then

X ∈ L(E) ⇔ \begin{cases}∀d, e ∈ X. ¬(d#e) ∧ \\ ∀d, e ∈ E. d ≤ e ∈ X ⇒ d ∈ X. \end{cases}

It follows that, up to L-equivalence, such structures can alternatively be represented as triples ^{/}_{\}E, fCon, ≤^{\}_{/} with fCon ⊆ 𝒫_{fin}(E) and ≤ ⊆ E × E, as are the prime event structures of [34], respectively as triples /_{\}E, #, ≤^{\}_{/}, as are the prime event structures of [25, 35].

4.2 Secured configurations

In this section we augment Observations 4.3 to 4.5 with characterisations of the secured configurations. To this end we first provide a characterisation of the finite reachable configurations of singular event structures.

Observation 4.6 Let E be a singular event structure. Then

X ∈ R_{f}(E) ⇔ \begin{cases}fCon(X) ∧ \\ ∃e_{1}, …, e_{n} ∈ X. X = \{e_{1}, ..., e_{n}\} ∧ \\ ∀i ≤ n. \{e_{1}, ..., e_{i−1}\} ⊢_{s} e_{i}. \end{cases}

If E is furthermore rooted and with binary conflict, then

X ∈ R_{f}(E) ⇔ \begin{cases}∀d, e ∈ X. ¬(d#e) ∧ \\ ∃e_{1}, …, e_{n} ∈ X. X = \{e_{1}, ..., e_{n}\} ∧ \\ ∀i ≤ n. \{e_{1}, ..., e_{i−1}\} ⊢_{s} e_{i}. \end{cases}

The next proposition says that for certain event structures, including the ones from [34, 35], the secured configurations are completely determined by the finite reachable ones. In addition, it provides the counterpart of Observation 4.3 for the secured configurations.

Proposition 4.2 Let E = ^{/}_{\}E, ⊢^{\}_{/} be a singular event structure with finite causes and finite conflict. Then

X ∈ S(E) ⇔ ∀Y ⊆_{fin} X. ∃Z ∈ R_{f}(E). Y ⊆ Z ⊆ X,

i.e., S(E) is the set of directed unions over R_{f}(E), and

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

Proof: “⇒, above”: Let X ∈ S(E) and Y ⊆_{fin} X. Let X_{0}, X_{1}, ... be a stepwise securing of X (cf. Definition 3.5) and choose n in IN such that Y ⊆ X_{n}. For k = n, n − 1, n − 2, ..., 0 choose the finite subset Y_{k} of X_{k} recursively as follows. Y_{n} = Y. Given Y_{k} with 1 ≤ k ≤ n, choose for any event e ∈ Y_{k} a set Z_{e} ⊆ X_{k−1} with Z_{e} ⊢ e, and let Y_{k−1} = ⋃_{e∈Y_{k}} Z_{e}. Because E has finite causes, the sets Z_{e} are finite, and so is Y_{k−1}. As E is singular we have ∅ ⊢ Z for any Z ⊆ X with |Z| ≠ 1. Therefore the sets ⋃_{i=0}^{k} Y_{i} for k ≤ n form a stepwise securing of the finite set Z = ⋃_{i=0}^{n} Y_{i}. Hence Z ∈ R_{f}(E). Furthermore we have Y ⊆ Z ⊆ X. “⇓” follows immediately from Observation 4.6. “⇐, below”: Let X ⊆ E be such that the right-hand side holds. Take X_{n+1} := {e_{n} | ∃e_{0}, …, e_{n−1} ∈ X. ∀i≤n. {e_{0}, ..., e_{i−1}} ⊢_{s} e_{i}} for n∈IN, and take X_{0} := ∅. Now X = ⋃_{n=0}^{∞} X_{n}. As a sequence e_{0}, ..., e_{n} as occurs above can be prolonged by repeating events, we have X_{n} ⊆ X_{n+1} for all n ∈ IN. Let Y ⊆ X_{n+1}. It remains to be shown that ∃Z ⊆ X_{n}. Z ⊢ Y. In case Y is infinite, this follows because E has finite conflict. Otherwise, if |Y | ≠ 1 it follows because E is singular and fCon(Y). Now suppose |Y | = 1. Then ∃e_{0}, ..., e_{n} ∈ X. Y ={e_{n}} ∧ ∀i ≤ n. {e_{0}, ..., e_{i−1}} ⊢_{s} e_{i}. So in particular ∃Z ⊆ {e_{0}, ..., e_{n−1}}. Z ⊢ Y. We have Z ⊆ ⋃_{i=1}^{n} X_{i} = X_{n}. □

Thus, recalling Observation 4.2, Proposition 4.1 and Corollary 9, for singular event structures with finite causes and finite conflict we have

R(E) = R(F) iff S(E) = S(F) iff R_{f}(E) = R_{f}(F).

In both statements of Proposition 4.2, “⇒” requires singularity and finite causes, and “⇐” singularity and finite conflict. That these conditions cannot be dropped follows from the following counterexamples.

• Let E be uncountable let ∅ ⊢ X for every finite set X (with no other enablings). This event structure is singular and has finite causes, but does not have finite conflict, and “⇐” fails for uncountable X.

• Let E be uncountable, with X ⊢ Y iff X = ∅ and Y is empty or infinite, or Y is finite and X contains one event less. This event structure has finite causes and finite conflict, but is not singular, and “⇐” fails for uncountable X (even though such X are left-closed configurations).

• Let E := IN ∪ {a}, ∅ ⊢ X for any X ≠ {a}, and IN ⊢ a. This event structure is singular and has finite conflict, but does not have finite causes, and “⇒” fails for X = E.

• Let E := IN∪{a}, {0} ⊢ a, {n+1} ⊢ {a, n} and ∅ ⊢ X for any other set X. This event structure has finite causes and finite conflict, but is not singular, and “⇒” fails for X = E.

The following counterpart of Observation 4.4 is an easy consequence.

Observation 4.7 Let E be a rooted, singular event structure with finite causes and binary conflict. Then

X ∈ S(E) ⇔ \begin{cases}∀d, e ∈ X. ¬(d#e) ∧ \\ ∀e ∈ X. ∃e_{0}, …, e_{n} ∈ X. e = e_{n} ∧ \\ ∀i ≤ n. \{e_{0}, ..., e_{i−1}\} ⊢_{s} e_{i}. \end{cases}

For X a left-closed configuration of a singular, conjunctive event structure and e_{0} ∈ X we say that e_{0} can happen at stage n, if there is no chain e_{n} ≺ ⋯ ≺ e_{1} ≺ e_{0}. Now we have X ∈ S(E) iff each event in X can happen at some finite stage. It follows that:

Observation 4.8 Let E = ^{/}_{\}E, ⊢^{\}_{/} be a singular, conjunctive event structure. Then

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

2. E is L-irredundant iff ∀e ∈ E. Con({d | d ≤ e}).

3. E is S-irredundant iff E is L-irredundant and for every e ∈ E there is an n ∈ IN such that there is no chain e_{n} ≺ ⋯ ≺ e_{1} ≺ e_{0} = e.

4. In case E is cycle-free we have

X ∈ R_{f}(E) ⇔ X ∈ L(E) ∧ X is finite.

5. If E is S-irredundant then L(E) ⊆ S(E).

Together with Lemma 1 this yields

Corollary 11 Let E = ^{/}_{\}E, ⊢^{\}_{/} be a singular, conjunctive, S-irredundant event structure with finite conflict. Then S(E) = L(E). □

4.3 The event structures of Winskel [34]

These are defined as triples E = ^{/}_{\}E, Con, ⊢^{\}_{/} where

• E is a set of events,

• Con ⊆ 𝒫_{fin}(E) is a nonempty consistency predicate such that: Y ⊆ X ∈ Con ⇒ Y ∈ Con,

• and ⊢ ⊆ Con × E is the enabling relation, which satisfies X ⊢ e ∧ X ⊆ Y ∈ Con ⇒ Y ⊢ e.

Such an event structure is stable if it satisfies

X ⊢ e ∧ Y ⊢ e ∧ Con(X ∪ Y ∪ {e}) ⇒ X ∩ Y ⊢ e.

The family S(E) of configurations of such an event structure (written F(E) in [34]) 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},

just as in Proposition 4.2. In addition, we define L(E) and ⟶_{E} exactly as in Observation 4.3, but reading Con for fCon and ⊢ for ⊢_{s}. Again, we write S(E) for /_{\}E, S(E)^{\}_{/}, and C^{+}(E) for ^{/}_{\}E, L(E), ⟶_{E}^{\}_{/}.

Here we will show that up to reachable equivalence and even transition equivalence (cf. Definition 2.4) these event structures are exactly the ones in our sense which are rooted, singular, with finite causes and with finite conflict; and the stable event structures of [34] are the ones which are moreover locally conjunctive.

For E = ^{/}_{\}E_{W} , Con_{W} , ⊢_{W} ^{\}_{/} an event structure as in [34], let the event structure E(E) := ^{/}_{\}E_{W} , ⊢^{\}_{/} be given by

X ⊢ Y iff \begin{cases}either Y = \{e\}, Con_{W} (\{e\}) and X ⊢_{W} e \\ or |Y | ≠ 1, X = ∅ and Con_{W} (Y) \\ or Y is infinite and X = ∅. \end{cases}

Now, for X ⊆_{fin} E_{W},

fCon(X) ⇔ Con_{W} (X)∧∀e∈X. ∃Y ⊆E_{W} . Y ⊢_{W} e (1)

and whenever fCon(X) we have

X ⊢_{s} e ⇔ Con_{W} ({e}) ∧ X ⊢_{W} e.  (2)

Proposition 4.3 Let E be an event structure as in [34]. Then E(E) is rooted, singular and with finite causes and finite conflict. If E is stable then E(E) is locally conjunctive. Moreover, S(E(E)) = S(E) and C^{+}(E(E)) = C^{+}(E).

Proof: Let E = ^{/}_{\}E_{W} , Con_{W} , ⊢_{W} ^{\}_{/} be an event structure as in [34]. As Con_{W} is nonempty and subsetclosed we have ∅ ∈ Con_{W}. Thus ∅ ⊢ ∅, i.e., E(E) is rooted. By construction, E(E) is singular and with finite causes and finite conflict. That the stability of E implies the local conjunctivity of E(E) follows because fCon(X) ⇒ Con_{W} (X) and every collection of finite sets has a finite subcollection with the same intersection. With Proposition 4.2 and Observation 4.3, respectively, using (1) and (2), one easily checks that S(E(E)) = S(E) and C^{+}(E(E)) = C^{+}(E). □

For E = ^{/}_{\}E, ⊢^{\}_{/} a rooted event structure, the structure W(E) := ^{/}_{\}E, fCon, ⊢_{s}^{\}_{/}, where fCon and ⊢_{s} are given by Definition 4.1, is clearly an event structure in the sense of [34].

Proposition 4.4 Let E be a rooted, singular event structure with finite causes and finite conflict. Then S(W(E)) = S(E) and C^{+}(W(E)) = C^{+}(E). Moreover, W(E) is stable if E is locally conjunctive.

Proof: Trivial, with Proposition 4.2 and Observation 4.3. □

4.4 The event structures of Winskel [35]

These are defined as triples E = ^{/}_{\}E, #, ⊢^{\}_{/} where

• E is a set of events,

• # ⊆ E × E is a symmetric, irreflexive conflict relation. Write Con for the set of finite, conflictfree subsets of E, i.e., those finite subsets X ⊆ E for which

∀e, e′ ∈ X. ¬(e#e′),

• and ⊢ ⊆ Con × E is the enabling relation, which satisfies X ⊢ e ∧ X ⊆ Y ∈ Con ⇒ Y ⊢ e.

Such an event structure is stable if it satisfies

X ⊢ e ∧ Y ⊢ e ∧ Con(X ∪ Y ∪ {e}) ⇒ X ∩ Y ⊢ e.

The family S(E) of configurations of such an event structure (written F(E) in [35]) consists of those X ⊆ E which are

• conflict-free: ∀e, e′ ∈ X. ¬(e#e′),

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

just as in Observation 4.7. Note that a set of events X is conflict-free iff every finite subset of X is in Con. In addition, we define L(E) and ⟶_{E} exactly as in Observation 4.4, reading Con for fCon and ⊢ for ⊢_{s}.

Say that an event structure ^{/}_{\}E, Con, ⊢^{\}_{/} in the sense of [34] has binary conflict if for any X ⊆_{fin} E:

Con(X) ⇔ ∀Y ⊆ X. (|Y | = 2 ⇒ Con(Y)).

Clearly, the event structures of [35] are just a reformulation of the event structures of [34] that have binary conflict. A small variation of the arguments from the previous section shows that, up to reachable equivalence and even transition equivalence, the event structures of [35] are exactly the ones in our sense which are rooted, singular, with finite causes and with binary conflict; and the stable event structures of [35] are the ones which are moreover locally conjunctive:

For E=^{/}_{\}E_{W} , #_{W} , ⊢_{W} ^{\}_{/} an event structure as in [35], let the event structure E(E) := ^{/}_{\}E_{W} , ⊢^{\}_{/} be given by

X ⊢ Y iff \begin{cases}either Y = \{e\} and X ⊢_{W} e \\ or |Y | = \{d, e\}, d≠e, X =∅ and ¬(d#_{W} e) \\ or Y = X = ∅ \\ or |Y | > 2 and X = ∅. \end{cases}

Write Con_{W} (X) for |X| < ∞ ∧ ∀e, e′ ∈ X. ¬(e#_{W} e′). Then equations (1) and (2) of Section 4.3 hold again.

Proposition 4.5 Let E be an event structure as in [35]. Then E(E) is rooted, singular and with finite causes and binary conflict. If E is stable then E(E) is locally conjunctive. Moreover, S(E(E)) = S(E) and C^{+}(E(E)) = C^{+}(E).

Proof: Let E = ^{/}_{\}E_{W} , #_{W} , ⊢_{W} ^{\}_{/} be an event structure as in [35]. By construction, E(E) is rooted, singular and with finite causes and binary conflict. That the stability of E implies the local conjunctivity of E(E) follows exactly as in the proof of Proposition 4.3. With Observations 4.7 and 4.4, respectively, one obtains S(E(E)) = S(E) and C^{+}(E(E)) = C^{+}(E). □

For E = ^{/}_{\}E, ⊢^{\}_{/} a rooted event structure with binary conflict, the structure W^{#}(E) := ^{/}_{\}E, #, ⊢_{s}^{#}^{\}_{/}, where # is given by Definition 4.1 and X ⊢_{s}^{#} e iff

(fCon(X) ∨ |X| = 1) ∧ ∃Y ⊆ X. Y ⊢ {e},

is clearly an event structure in the sense of [35].

Proposition 4.6 Let E be a rooted, singular event structure with finite causes and binary conflict. Then S(W^{#}(E)) = S(E) and C^{+}(W^{#}(E)) = C^{+}(E). Moreover, W^{#}(E) is stable if E is locally conjunctive.

Proof: The first two statements are trivial, with Observations 4.7 and 4.4. Now assume E is locally conjunctive; we show that W(E) is stable. So assume X ⊢_{s}^{#} e, Y ⊢_{s}^{#} e and for d, f ∈ X ∪ Y ∪ {e} it holds that ¬(d#f). The latter means that either d = f or Con({d, f}). We have to show that X ∩ Y ⊢_{s}^{#} e.

Claim: Con(X ∪ Y ∪ {e}).

proof: Let W ⊆ X ∪ Y ∪ {e}. We have to find a Z with Z ⊢ W. In case W = ∅ or |W | > 2 we can take Z = ∅, because E is rooted and with binary conflict.

In case W = {d, f} with d≠f, we have Con({d, f}). In case W = {e}, we use X ⊢_{s}^{#} e to infer that there

is an X′ ⊆ X with X′ ⊢ {e}.

In case W = {d} with d ≠ e, then Con({d, e}) and hence Con({d}).

Application of the Claim: Since X ⊢_{s}^{#} e, there is an X′ ⊆ X with X′ ⊢ e. Likewise, there is an Y′ ⊆ Y with Y′ ⊢ e. Now Con(X′ ∪ Y′ ∪ {e}), so the local conjunctivity of E yields X′ ∩ Y′ ⊢ {e}. Furthermore, X and Y must be finite, by definition of ⊢_{s}^{#}, so the claim also yields fCon(X ∩ Y). As X′ ∩ Y′ ⊆ X ∩ Y we obtain X ∩ Y ⊢_{s}^{#} e. □

4.5 The prime event structures of [34]

These are defined as triples E = ^{/}_{\}E, Con, ≤^{\}_{/} where

• E is a set of events,

• Con ⊆ 𝒫_{fin}(E) is a nonempty consistency predicate such that: Y ⊆ X ∈ Con ⇒ Y ∈ Con, and {e} ∈ Con for all e ∈ E,

• and ≤ ⊆ E × E is a partial order, the causality relation, satisfying

– d ≤ e ∈ X ∈ Con ⇒ X ∪ {d} ∈ Con

– and ↓e = {d ∈ E | d ≤ e} is finite for all e ∈ E.

The set L(E) of configurations of such an event structure consists of those X ⊆ E which are

• consistent: every finite subset of X is in Con,

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

just as in Observation 4.5. Write L(E) for ^{/}_{\}E, L(E)^{\}_{/}.

Here we will show that up to L-equivalence these event structures are exactly the ones in our sense which are rooted, singular, (manifestly) conjunctive, (pure,) S-irredundant and with finite causes and finite conflict. On this class of event structures, Corollary 11 says that S coincides with L. Thus each of S and L can be understood as generalisation of the notion of configuration for prime event structures from [34].

For E = ^{/}_{\}E_{W} , Con_{W} , ≤_{W} ^{\}_{/} a prime event structure as in [34], let the event structure E(E) := ^{/}_{\}E_{W} , ⊢^{\}_{/} be given by

X ⊢ Y iff \begin{cases}Y = \{e\} and X = \{d | d <_{W} e\} \\ or |Y | ≠ 1, X = ∅ and Con_{W} (Y) \\ or Y is infinite and X = ∅. \end{cases}

Now fCon = Con_{W} and ≤ = ≤_{W}.

Proposition 4.7 Let E be a prime event structure as in [34]. Then E(E) is rooted, singular, manifestly conjunctive, pure, S-irredundant and with finite causes and finite conflict. Moreover, L(E(E)) = L(E) = S(E).

Proof: Let E = ^{/}_{\}E_{W} , Con_{W} , ≤_{W} ^{\}_{/} be a prime event structure as in [34]. As Con_{W} is nonempty and subset-closed we have ∅ ∈ Con_{W}. Thus ∅ ⊢ ∅, i.e., E(E) is rooted. By construction, E(E) is singular, manifestly conjunctive, pure, and with finite causes and finite conflict. By Observation 4.8 E(E) is Sirredundant, and Observation 4.5 and Corollary 11 yield L(E(E)) = L(E) = S(E). □

For E = ^{/}_{\}E, ⊢^{\}_{/} a rooted, S-irredundant event structure with finite causes, the structure W′(E):=^{/}_{\}E, Con′, ≤^{\}_{/}, where Con′(X) iff fCon({d ∈ E | ∃e ∈ X. d ≤ e}), and fCon and ≤ are given by Definition 4.1, is a prime event structure in the sense of [34]. In particular, by S-irredundancy, for any e ∈ E there is an n ∈ IN such that there is no chain e_{n} ≺ ⋯ ≺ e_{1} ≺ e. As E has finite causes, for any e ∈ E there are only finitely many d ∈ E with d ≺ e; thus the set ↓e is finite. As ↓e must be part of any configuration containing e, fCon(↓e), and hence {e}∈Con′ for any e∈E. As S-irredundancy implies cycle-freeness, ≤ must be a partial order.

Proposition 4.8 Let E be a rooted, singular, conjunctive, S-irredundant event structure with finite causes and finite conflict. Then L(W′(E)) = L(E) = S(E).

Proof: Trivial, with Obs. 4.5 and Corollary 11. □

4.6 The event structures of [25]

These 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

∀d, e, f ∈ E. d ≤ e ∧ d#f ⇒ e#f,

the principle of conflict heredity.

The set L(E) of configurations of such an event structure consists of those X ⊆ E which are

• conflict-free: # ∩ (X × X) = ∅,

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

just as in Observation 4.5. In addition, we define R_{f}(E) as the set of finite configurations in L(E).

The prime event structures of [35] are defined likewise, but additionally requiring

{d ∈ E | d ≤ e} is finite for all e ∈ E,

the principle of finite causes.

Here we will show that up to L-equivalence these event structures are exactly the ones in our sense which are (pure,) rooted, singular, (manifestly) conjunctive, L-irredundant, cycle-free and with binary conflict, and for the ones from [35] also S-irredundant and with finite causes.

For E = ^{/}_{\}E_{N}, ≤_{N}, #_{N}^{\}_{/} a prime event structure as in [25], let the event structure E(E) := ^{/}_{\}E_{N}, ⊢^{\}_{/} be given by

X ⊢ Y iff \begin{cases}Y = \{e\} and X = \{d | d <_{N} e\} \\ or Y =\{d, e\}, d≠e, X =∅ and ¬(d#_{N}e) \\ or |Y | ≠ 1, 2 and X = ∅. \end{cases}

Now ≤ = ≤_{N} and # = #_{N}.

Proposition 4.9 Let E be an event structure as in [25]. Then E(E) is pure, rooted, singular, manifestly conjunctive, L-irredundant, cycle-free and with binary conflict. If E satisfies the principle of finite causes then E(E) is moreover S-irredundant and with finite causes. Furthermore, L(E(E)) = L(E).

Proof: Let E = ^{/}_{\}E_{N}, ≤_{N}, #_{N}^{\}_{/} be an event structure as in [25]. By construction, E(E) is pure, rooted, singular, manifestly conjunctive and with binary conflict. The relation ≺ coincides with <, so E(E) is cycle-free. With Observation 4.5, L(E(E)) = L(E), and by Observation 4.8.4, R_{f}(E(E)) = R_{f}(E).

For every e ∈ E_{N}, the set ↓ e := {d ∈ E_{N} | d ≤ e} must be conflict-free, using the principle of conflict heredity and the irreflexivity of #. Hence, e ∈ ↓e ∈ L(E) = L(E(E)). Therefore E(E) is L-irredundant. In case E satisfies the principle of finite causes, E(E) has finite causes, and e ∈ ↓ e ∈ R_{f}(E) = R_{f}(E(E)) ⊆ S(E(E)). In this case E(E) is even S-irredundant. □

For E = ^{/}_{\}E, ⊢^{\}_{/} an L-irredundant, cycle-free event structure, the structure W_{NP}(E) := ^{/}_{\}E, ≤, #_{h} ^{\}_{/}, where d#_{h}e iff ∃d′ ≤ d. ∃e′ ≤ e. d′#e′, and ≤ and # are given by Definition 4.1, is clearly an event structure in the sense of [25]. In particular, ≤ is a partial order since E is cycle-free, and #_{h} is irreflexive since if e#_{h}e then e could not occur in any configuration, contradicting L-irredundancy. In case E is moreover S-irredundant and with finite causes, then, by the argument in the previous section, the sets ↓e have to be finite. In this case W_{NP}(E) is a prime event structure as in [35].

Proposition 4.10 Let E be a rooted, singular, conjunctive, L-irredundant and cycle-free event structure with binary conflict. Then L(W_{NP}(E)) = L(E).

Proof: Trivial, with Observation 4.5. □

If E is moreover S-irredundant, then S(E) = L(E), by Corollary 11. This does not extend to the structures corresponding to the event structures of [25] however:

Example 15 Let E be given by E = {e_{0}, e_{1}, ...} ∪ {e_{∞}}, # = ∅ and e_{i} < e_{j} iff i < j. Then E ∈ L(E) but E ∉ S(E).

4.7 Summary and remarks

The left-closed configurations of an event structure generalise the left-closed and conflict-free subsets of events considered in Nielsen, Plotkin & Winskel [25], as well as the families of configurations of prime event structures as considered in Winskel [34, 35]. The secured configurations generalise the families of configurations of event structures (prime and otherwise) considered in [34, 35]. The families of configurations of such event structures are completely determined by their finite reachable configurations.

As indicated in Table 1, for each of the seven classes of event structures proposed in [25, 34, 35] a corresponding subclass of our event structures has been defined, together with event and configuration preserving translations in both directions. Upon defining leftclosed configurations and a transition relation on the event structures of [25, 34, 35], these translations even preserve transition equivalence.

For the event structures in our sense corresponding to the prime event structures of [34, 35], the requirements of S-irredundancy and having finite causes can be replaced by the requirement of R_{f}-irredundancy: any event should occur in a finite reachable configuration.

Preserving finitary equivalence—that is, preserving events and finite configurations—any event structure can be converted into one with finite causes and finite conflict, namely by adding all enablings ∅ ⊢ Y with Y infinite, and omitting the enablings X ⊢ Y with X infinite. This procedure preserves the other properties of Definition 4.2, except S- and L-irredundancy. It also preserves R_{f}-irredundancy. Hence, up to finitary equivalence the first 6 correspondences of Table 1 hold without finite causes and finite conflict, and using R_{f}- irredundancy instead of S-irredundancy.

Any event structure E = ^{/}_{\}E, ⊢^{\}_{/} can be converted into an S-irredundant structure, namely by omitting from E all events that do not occur in any secured configuration, and omitting from ⊢ any enablings X ⊢ Y in which such events occur in X or Y. This clearly preserves S(E), as well as the properties rootedness, singularity, (local) conjunctivity, cycle-freeness and having finite causes and finite or binary conflict. Thus, up to having the same secured configurations, the prime event structures of [34] (resp. [35]) even correspond to the class of our event structures that are rooted, singular, conjunctive and with finite causes and finite (resp. binary) conflict, i.e., not requiring S-irredundancy. However, it should be noted that this correspondence does not hold up to S-equivalence, as the set of events is not preserved. The same can be said for L and R_{f}- irredundancy.

5 Comparing Models

Having seen the general correspondences between our various models of computation—event structures, configuration structures, propositional theories and Petri nets—we now trace the relationships for various natural subclasses; we are guided in our choice of these subclasses by the concepts isolated in our exploration of previous notions of event structure in the last section.

In Sections 5.1, 5.3 and 5.4 we first of all give properties of configuration structures corresponding to those of event structures. We then tackle the converse completeness problem for collections of properties: given a configuration structure with a collection of these properties, is there an event structure satisfying the corresponding properties which yields the given configuration structure? Following our general point of view, we understand the configuration structures to

Event  Configuration Propositional
structures  structures  theories
rooted  rooted  (>0, any)
singular  closed under \overline{⋃} (1, any), (any, 0)
conjunctive  closed under ⋂_{•} (any, ≤1)
locally conj.  closed under \overline{⋂}_{•} (any, ddc)
finite conflict finite conflict (finite, any)
binary conflict binary conflict (≤2, any)
sing. & fin. con. closed under \overline{⋃}^{f} (1, any), (fin., 0)
sing. & bin. con. closed under \overline{⋃}^{2} (1, any), (≤2, 0)
loc. conj. & f.c. closed under \overline{⋂}_{•}^{f} (finite, fddc)
loc. conj. & b.c. closed under \overline{⋂}_{•}^{2} (≤2, bddc)

Table 2: Corresponding properties

provide our (semantic) model of behaviour. So we are content to consider the map from event structures to configuration structures for each of the various classes, and show that it is onto; we do not seek such properties of a map or maps in the converse direction. As map from event structures to configuration structures we take L in Section 5.1, S in Section 5.3 (but only covering secure event structures) and F ∘ L and R_{f} in Section 5.4.

In Section 5.2 we provide corresponding classes of propositional theories, described according to the syntactic form of the allowed formulae. Finally, in Section 5.5 we tie in corresponding classes of Petri nets.

5.1 Event vs. configuration structures

Table 2 gives the various corresponding properties. We have already defined all those we need for event structures. For configuration structures we first need some notions of consistency.

Definition 5.1 Let C = ^{/}_{\}E, C^{\}_{/} be a configuration structure. A set of events X ⊆ E is consistent, written Cn(X), if ∃z ∈C. X ⊆ z. Further, X is finitely consistent, written Cn_{fin}(X), if

∀Y ⊆_{fin} X. Cn(Y)

and pairwise consistent, written Cn_{2}(X), if

∀Y ⊆X. (|Y |≤2 ⇒ Cn(Y)).

Now we can define the corresponding properties used in the table.

Definition 5.2 Let C = ^{/}_{\}E, C^{\}_{/} be a configuration structure. Then:

1. C is said to be consistently complete [27] or closed under bounded unions (\overline{⋃}) if

A ⊆ C ∧ Cn(⋃ A) ⇒ ⋃ A ∈ C

2. C is said to be closed under nonempty intersections (⋂_{•}) if

∅ ≠ A ⊆ C ⇒ ⋂ A ∈ C

3. C is said to be closed under bounded nonempty intersections (\overline{⋂}_{•}) if

∅ ≠ A ⊆ C ∧ Cn(⋃ A) ⇒ ⋂ A ∈ C

4. C has finite conflict if

[∀Y ⊆X. (Y finite ⇒ ∃z ∈C. Y ⊆z ⊆X)] ⇒ X∈C

5. C has binary conflict if

[∀Y ⊆X. (|Y | ≤ 2 ⇒ ∃z ∈C. Y ⊆z ⊆X)] ⇒ X∈C

6. C is said to be closed under finitely consistent unions (\overline{⋃}^{f}) if

A ⊆ C ∧ Cn_{fin}(⋃ A) ⇒ ⋃ A ∈ C

7. C is said to be closed under pairwise consistent unions (\overline{⋃}^{2}) if

A ⊆ C ∧ Cn_{2}(⋃ A) ⇒ ⋃ A ∈ C

8. C is said to be closed under finitely consistent nonempty intersections (\overline{⋂}_{•}^{f}) if

∅ ≠ A ⊆ C ∧ Cn_{fin}(⋃ A) ⇒ ⋂ A ∈ C

9. C is said to be closed under pairwise consistent nonempty intersections (\overline{⋂}_{•}^{2}) if

∅ ≠ A ⊆ C ∧ Cn_{2}(⋃ A) ⇒ ⋂ A ∈ C.

By their definition, these notions are related as follows:

\overline{⋃}^{2}-closed  ⇒ \overline{⋃}^{f}-closed ⇒ \overline{⋃}-closed
⇓  ⇓
binary conflict ⇒ finite conflict
\overline{⋃}^{2}- and \overline{⋂}_{•}-closed \overline{⋃}^{f}- and \overline{⋂}_{•}-closed
⇓  ⇓

⋂_{•} -closed ⇒ \overline{⋂}_{•}^{2}-closed ⇒ \overline{⋂}_{•}^{f}-closed ⇒ \overline{⋂}_{•}-closed.

We can illustrate these properties with the aid of previously given examples. The configuration structure G from Example 8 has all properties of Definition 5.2, and indeed its event structure representation has all the corresponding properties of Table 2.

The configuration structure of Example 5 fails to be closed under bounded unions, for there is no configuration {a} ∪ {b}, even though its superset {a, b, c} is a configuration. Indeed, the corresponding event structure is not singular.

The configuration structure of Example 6 fails to be closed under bounded nonempty intersections, for there is no configuration {c}. Indeed its associated event structure is not locally conjunctive. The modified event structure of Example 6 is locally conjunctive, although not conjunctive. Its associated configuration structure is closed under bounded nonempty intersections, but not under (general) nonempty intersections.

The configuration structure of Example 11 fails to have finite conflict, whereas the event structure from Example 1 has finite conflict but fails to have binary conflict.

By combining these examples it is not hard to show that for each selection from the first five properties, respecting the implications above, there exists a configuration structure with the selected properties and none of the others.

The first three conditions above are particularly natural as they are (essentially) couched in terms of the lattice-theoretic structure the configuration structure inherits from that of the powerset lattice of all events. The following are natural replacements of this kind for the remaining six conditions.

Definition 5.3 Let C = ^{/}_{\}E, C^{\}_{/} be a configuration structure.

4′. C is said to be closed under directed unions (⋃_{↑}) if for every nonempty family A of configurations:

[∀x, y ∈A. ∃z ∈A. x ∪ y ⊆ z] ⇒ ⋃ A ∈ C

5′. C is said to be weakly coherent iff for every family A ⊆ C of configurations:

[∀x, y ∈A. ∃z ∈C. x ∪ y ⊆ z ⊆ ⋃ A] ⇒ ⋃ A ∈ C

6′. C is said to be finitely complete [34] or closed under finitely compatible unions (\overline{⋃}^{fc}) if

A ⊆ C ∧ ∀F ⊆_{fin} A. Cn(⋃ F) ⇒ ⋃ A ∈ C

7′. C is said to be coherent [27, 35] or closed under pairwise compatible unions (\overline{⋃}^{2c}) if

A ⊆ C ∧ ∀x, y ∈A. Cn(x ∪ y) ⇒ ⋃ A ∈ C

8′. C is said to be closed under finitely compatible nonempty intersections (\overline{⋂}_{•}^{fc}) if

∅ ≠ A ⊆ C ∧ ∀F ⊆_{fin} A. Cn(⋃ F) ⇒ ⋂ A ∈ C

9′. C is said to be closed under pairwise compatible nonempty intersections (\overline{⋂}_{•}^{2c}) if

∅ ≠ A ⊆ C ∧ ∀x, y ∈A. Cn(x ∪ y) ⇒ ⋂ A ∈ C.

In all six cases the property of Definition 5.3 is strictly weaker than the corresponding one of Definition 5.2, except that (weak) coherence also implies rootedness. Strictness is illustrated by the configuration structure consisting of ∅ and the co-singleton sets of natural numbers. However, in all six cases (trivially in the last two) the two properties coincide for those configuration structures closed under non-empty intersections.

Proposition 5.1 Let C = ^{/}_{\}E, C^{\}_{/} be a configuration structure that is closed under ⋂_{•}. Then

• C is closed under ⋃_{↑} iff it has finite conflict,

• C is weakly coherent iff it is rooted and has binary conflict,

• C is closed under \overline{⋃}^{fc} iff it is closed under \overline{⋃}^{f}, and

• C is coherent iff it is rooted and closed under \overline{⋃}^{2}.

Proof: We only prove the first and last statement; the other proofs are similar.

Suppose C has finite conflict. Let ∅ ≠ A ⊆ C satisfy

∀x, y ∈A. ∃z ∈A. x ∪ y ⊆ z.

Then every finite subset Y of ⋃ A is contained in the union of a finite subset of A and hence in an element of A. As C has finite conflict it follows that ⋃ A ∈ C. Now suppose C is closed under ⋃_{↑} and ⋂_{•}. Let X

be a set of events satisfying

∀Y ⊆X. (Y finite ⇒ ∃z ∈C. Y ⊆z ⊆X).

As C is closed under ⋂_{•}, for every finite subset Y of X there is a least configuration z_{Y} ∈ C satisfying Y ⊆ z_{Y} ⊆ X. Clearly z_{Y} ∪ z_{Y′} ⊆ z_{Y ∪Y′}. Hence X = ⋃_{Y ⊆_{fin} X} z_{Y} ∈ C.

Suppose C is rooted and closed under \overline{⋃}^{2}. Let A satisfy

A ⊆ C ∧ ∀x, y ∈A. Cn(x ∪ y).

Then Cn(Y) for each Y ⊆⋃ A with |Y |≤2, so ⋃ A∈C.

Now suppose C is closed under \overline{⋃}^{2c} and ⋂_{•}. Taking A = ∅ in Definition 5.3.7 we find that C is rooted. Let

A ⊆ C ∧ Cn_{2}(⋃ A).

As C is closed under ⋂_{•}, for every e ∈ x ∈ A there is a least configuration z_{e} ∈ C satisfying e ∈ z_{e} ⊆ x. Moreover, for every d, e ∈ ⋃ A there is a least z_{d,e} ∈ C satisfying d, e ∈ z_{d,e}. Clearly z_{d} ∪ z_{e} ⊆ z_{d,e}. Hence ⋃ A = ⋃_{e∈x∈A} z_{e} ∈ C. □

Proposition 5.2 A configuration structure is closed under \overline{⋃}^{fc} iff it is closed under \overline{⋃} and ⋃_{↑}. Likewise, it is coherent iff it is closed under \overline{⋃} and weakly coherent.

Proof: For both claims “only if” is straightforward. So suppose C = ^{/}_{\}E, C^{\}_{/} is closed under \overline{⋃} and ⋃_{↑}. Let

A ⊆ C ∧ ∀F ⊆_{fin} A. Cn(⋃ F).

As C is closed under \overline{⋃} we have ∀F ⊆_{fin} A. ⋃ F ∈ C. Thus the family consisting of ⋃ F ∈ C for F ⊆_{fin} A is a directed union, and ⋃ A = ⋃_{F ⊆_{fin} A} ⋃ F ∈ C.

The last claim follows because in the presence of closure under \overline{⋃}, both coherence and weak coherence simplify to:

A ⊆ C ∧ ∀x, y ∈A. x ∪ y ∈ C ⇒ ⋃ A ∈ C. □

We will now proceed to establish the correspondence between the properties of event structures in the first column of Table 2 and the properties of configuration structures in the second column.

Theorem 4 Let E be an event structure.

1. If E is singular, then L(E) is closed under \overline{⋃}.

2. If E is conjunctive, then L(E) is closed under ⋂_{•}.

3. If E is locally conjunctive, then L(E) is closed under \overline{⋂}_{•}.

4. If E has finite conflict, then so does L(E).

5. If E has binary conflict, then so does L(E).

6. If E is singular and with finite conflict, then L(E) is closed under \overline{⋃}^{f}.

7. If E is singular and with binary conflict, then L(E) is closed under \overline{⋃}^{2}.

8. If E is locally conjunctive and with finite conflict, then L(E) is closed under \overline{⋂}_{•}^{f}.

9. If E is locally conjunctive and with binary conflict, then L(E) is closed under \overline{⋂}_{•}^{2}.

Proof: The details are routine and are omitted. □

In the next theorem we will show that none of the nine properties of configuration structures that figure in Theorem 4 can be strengthened.

Something unexpected arises in the last four statements of Theorem 4: the conjunction of two properties of an event structure gives rise to a property of configuration structures which does not follow from the properties associated to the two event structure properties separately. The following example illustrates this.

Example 16 Consider the configuration structure C = ^{/}_{\}E, C^{\}_{/} where

E := {a_{i} | i ≥ 1} ∪ {b, c} ∪ {d_{i} | i ≥ 1}

and where C contains the sets:

∅, {a_{i} | i ≥ 1} ∪ {b}, {a_{i} | i ≥ 1} ∪ {c}

and, for all n ≥ 1,

{a_{1}, …, a_{n}, d_{n}, b, c}.

Then C is rooted and closed under \overline{⋃} and \overline{⋂}_{•}, and has finite and binary conflict. But it is not closed under either \overline{⋃}^{f} or \overline{⋃}^{2} or \overline{⋂}_{•}^{f}or \overline{⋂}_{•}^{2}.

We would therefore not, for example, expect to recognise a configuration structure closed under \overline{⋃} and with finite conflict as the configuration structure of a singular event structure with finite conflict. For that we should also require the configuration structure to be closed under ^{\overline{⋃}^{f}}.

So it is natural to define a notion of package of properties of configuration structures with the intention that packages are the collections of properties for which corresponding event structures are expected to exist. We call a set of properties from the second column of Table 2 a package if

– it contains the property “closed under \overline{⋃}^{f}” iff it contains the properties “closed under \overline{⋃}” and “having finite conflict”,

– it contains the property “closed under \overline{⋃}^{2}” iff it contains the properties “closed under \overline{⋃}” and “having binary conflict”,

– it contains the property “closed under \overline{⋂}_{•}^{f}” iff it contains the properties “closed under \overline{⋂}_{•}” and “having finite conflict”, and

– it contains the property “closed under \overline{⋂}_{•}^{2}” iff it contains the properties “closed under \overline{⋂}_{•}” and “having binary conflict.”

By Propositions 5.1 and 5.2, the phenomenon of Example 16 does not apply to event structures closed under ⋂_{•}. When restricting attention to those, packaging would not be needed.

Theorem 5 A configuration structure C has any package of properties from the second column of Table 2 iff there is a (pure) event structure E with the corresponding properties such that L(E) = C.

Proof: Let C = ^{/}_{\}E, C^{\}_{/} be a configuration structure. Define E := ^{/}_{\}E, ⊢^{\}_{/} by X ⊢ Y iff X ∩Y = ∅∧X ∪Y ∈C. Thus E = E(C). It is straightforward to check that – E is always pure,

– if C is rooted, then so is E,

– if C is closed under ⋂_{•} then E is conjunctive,

– and if C is \overline{⋂}_{•}-closed then E is locally conjunctive. We show that L(E) = C. Suppose x ∈ C. For any Y ⊆ x take Z := x − Y. Then Z ⊆ x and Z ⊢ Y. So x ∈ L(E). Conversely, suppose x ∈ L(E). Then there is a Z ⊆ x such that Z ⊢ x. (In fact, Z must be ∅.) By construction, x = Z ∪ x ∈ C.

Next let C have finite conflict. Let E := ^{/}_{\}E, ⊢∪ ⊢^{ω}^{\}_{/} with ⊢ defined as before, and X ⊢^{ω} Y iff X = ∅ and Y infinite. It is straightforward to check that

– E is always pure and with finite conflict,

– if C is rooted, then so is E,

– if C is closed under ⋂_{•} then E is conjunctive,

– and if C is \overline{⋂}_{•}^{f}-closed then E is locally conjunctive. We show that L(E) = C. That C ⊆ L(E) goes exactly as in the previous case, so suppose x ∈ L(E). For any finite Y ⊆ x there must be a Z ⊆ x with Z ⊢ Y. By construction, Z ∪ Y ∈ C. As Y ⊆ Z ∪ Y ⊆ x, and C has finite conflict, we have x ∈ C.

The case that C has binary conflict goes similarly. Now assume C is closed under bounded unions (\overline{⋃}).

Let E := ^{/}_{\}E, ⊢_{1} ∪ ⊢_{2}^{\}_{/} with

X ⊢_{1} Y iff |Y | = 1, X ∩ Y = ∅ and X ∪ Y ∈ C, X ⊢_{2} Y iff X = ∅, |Y | ≠ 1 and Cn(Y).

It is straightforward to check that

– E is always pure and singular,

– if C is rooted, then so is E,

– if C is closed under ⋂_{•} then E is conjunctive,

– and if C is \overline{⋂}_{•}-closed then E is locally conjunctive. We show that L(E) = C. Suppose x ∈ C. For any Y ⊆ x take Z := x−Y if |Y | = 1 and Z := ∅ otherwise. Then Z ⊆ x and Z ⊢ Y. So x ∈ L(E). Conversely, suppose x ∈ L(E). Then there is a Z ⊆ x such that Z ⊢ x. In case |x| = 1 we have x = Z ∪ x ∈ C. In case |x| ≠ 1 it must be that Z = ∅ and Cn(x). Moreover, for any e ∈ x there is a Z_{e} ⊆ x such that Z_{e} ⊢ {e}. By construction, Z_{e}∪{e} ∈ C. As ⋃_{e∈x}(Z_{e}∪{e}) = x and Cn(x), and C is closed under bounded unions, x ∈ C.

Next assume C is closed under \overline{⋃}^{2}. Let E := ^{/}_{\}E, ⊢_{1} ∪ ⊢_{2} ∪ ⊢_{3}^{\}_{/} with

X ⊢_{1} Y iff |Y | = 1, X ∩ Y = ∅ and X ∪ Y ∈ C, X ⊢_{2} Y iff X = ∅, (|Y | = 0 or |Y | = 2) and Cn(Y), X ⊢_{3} Y iff X = ∅ and |Y | > 2.

It is straightforward to check that

– E is always pure, singular and with binary conflict,

– if C is rooted, then so is E,

– if C is closed under ⋂_{•} then E is conjunctive,

– and if C is \overline{⋂}_{•}^{2}-closed then E is locally conjunctive. We show that L(E) = C. That C ⊆ L(E) goes exactly as in the previous case, so suppose x ∈ L(E). In case |x| = 1 there again is a Z ⊆ x such that Z ⊢ x, and we have x = Z ∪ x ∈ C. So suppose |x| ≠ 1. For every Y ⊆ x with |Y | = 0 or |Y | = 2 there is a Z with Z ⊢ Y. It must be that Z = ∅ and Cn(Y). Hence Cn_{2}(x). Moreover, for any e ∈ x there is a Z_{e} ⊆ x such that Z_{e} ⊢ {e}. By construction, Z_{e} ∪ {e} ∈ C. As ⋃_{e∈x}(Z_{e} ∪ {e}) = x and Cn_{2}(x), and C is closed under pairwise consistent unions, x ∈ C.

The case that C is closed under \overline{⋃}^{f} goes likewise. □

A noteworthy consequence of this theorem is that every event structure with a given collection of properties from the first column of Table 2 is L-equivalent to a pure one with the same set of properties.

The property L-irredundancy of event structures is defined in terms of associated configuration structures: call a configuration structure irredundant if every event occurs in a configuration, then an event structure E is L-irredundant iff L(E) is irredundant. Thus Theorems 4 and 5 can be trivially upgraded by adding L-irredundancy and irredundancy to the table.

Likewise, call a configuration structure S-irredun-dant if every event occurs in a secured configuration. Using that S(E) ⊆ S(L(E)), even for impure event structures E, whenever E is an S-irredundant event structure then L(E) is an S-irredundant configuration structure. Conversely, if C is an S-irredundant configuration structure, then any pure event structure E with L(E) = C is S-irredundant. Thus Theorems 4 and 5 can be upgraded by adding S-irredundancy to the first two columns of the table.

Cycle-freeness, as defined in Section 4, is a meaningful concept only for singular conjunctive L-irredundant event structures; there it matches the concept of coincidence-freeness on configuration structures.

Definition 5.4 A configuration structure is coincidence-free if for every two distinct events occurring in a configuration there is a subconfiguration containing one but not the other.

Proposition 5.3 A singular, conjunctive, L-irredun-dant event structure E=^{/}_{\}E, C^{\}_{/} is cycle-free iff L(E) is coincidence-free.

Proof: For all e in E, the set ↓ (e) := {d ∈ E | d ≤ e} is the least left-closed configuration of E containing e. This implies that a failure of coincidence-freeness in L(E) occurs if and only if there are two distinct events d and e with d ≤ e ≤ d, i.e., in case of a cycle in E. □

We can now characterise the configuration structures associated to the event structures of [25].

Corollary 12 A configuration structure arises as the family of configurations of an event structure of [25] iff it is rooted, irredundant, coincidence-free and closed under \overline{⋃}^{2} and ⋂_{•}, or, equivalently, irredundant, coincidence-free, coherent and closed under ⋂_{•}. □

Although [25] contains a characterisation of the domains induced by families of configurations of event structures of [25], ordered by inclusion, a characterisation as above seems not to have appeared before.

The (secured) configuration structures that arise as the families of configurations of the various event structure of Winskel [34, 35] will be characterised in Section 5.3. We do not have a characterisation of the left-closed configuration structures associated to event structures with finite causes, and consequently no characterisation of the left-closed configuration structures associated to the general and stable event event structures of [34, 35].

5.2 Propositional theories

We now consider a variety of forms of formulae, written as (L, R) where L is taken from the lattice on the left of Figure 4 and R is taken from the lattice on the right. Other than the case where R is “bddc” these formulae are always implications, and then they are always clauses except when R is “ddc” or “fddc”. If they are clauses then L and R indicate in an evident way how many variables there are on each side of the implication; for example the form (any, ≤ 1) indicates a clause X ⇒ Y such that Y has at most one element and with no restriction on X. In the left-hand lattice, “nef” stands for “finite and non-empty”.

Formulae of the form (L, ddc) are implications where the hypothesis is a conjunction of variables whose size is specified by L and whose conclusion

any finite ≤ 2  > 0 nef 1 or 2 1  any ddc fddc bddc ≤ 1 0

Figure 4: Form Lattices

is a formula in “ddc” form, a disjoint disjunction of clauses, viz. a formula· ⋁_{j∈J} ⋀ Y_{j} where the Y_{j} are sets of variables, and we write· ⋁Φ for (⋁ Φ)∧⋀{¬(φ∧φ′) | φ, φ′ ∈ Φ, φ ≠ φ′}, the disjoint disjunction of Φ.

Sometimes such inconsistencies are signalled by finitary or even binary means. Formulae of the form (L, fddc) are again implications where the hypothesis is a conjunction of variables whose size is specified by L but now the conclusion is a formula in “fddc” form, a finitely disjoint disjunction of clauses, viz.

( ⋁_{j∈J} ⋀ Y_{j}) ∧ ⋀_{j,k∈J, j≠k} ¬(⋀ Z_{j,k} ∧ ⋀ Z_{k,j})

where the Y_{j} are sets of variables and the Z_{j,k} are finite subsets of Y_{j}. Finally we say that a formula has the (L, bddc) form if it has the form

(⋀ X ⇒ ⋁_{j∈J} ⋀ Y_{j}) ∧ ⋀_{j,k∈J, j≠k} ¬(e_{j,k} ∧ e_{k,j})

where X is a set of variables with size specified by L, the Y_{j} are sets of variables and the e_{j,k} are in Y_{j}.

Formulae of any of the above forms are called pure if no variable occurs at both sides of the implication.

Theorem 6 Let T be a propositional theory all of whose formulae have one of the forms given in a row of Table 2. Then M(T) has the corresponding property, as given in the table.

Proof: We consider only the cases (any, ddc) and (finite, fddc), leaving the others to the reader. To this end we first of all show that the collection of models of a family Φ of implications of the form ⋀ X ⇒· ⋁_{j∈J} ⋀ Y_{j} is closed under bounded non-empty intersections. Suppose that {m_{i} | i ∈ I} is a set of models of Φ, with upper bound m′. Let m be the intersection of the m_{i}; we must show it is a model. To this end, choose one implication ⋀ X ⇒· ⋁_{j∈J} ⋀ Y_{j} in Φ and suppose that m includes its premise X. Then, for i ∈ I, so does m_{i} and hence there is a unique j(i) in J such that Y_{j(i)} ⊆ m_{i}. We claim that, for i ∈ I, all j(i) are the same. For otherwise m′ would contain X ∪ Y_{j} ∪ Y_{k} for j, k ∈ J, j ≠ k, contradicting the fact that m′ satisfies ⋀ X ⇒· ⋁_{j∈J} ⋀ Y_{j}. Hence there is a unique j in J such that Y_{j} ⊆ m_{i} for all i ∈ I. So Y_{j} ⊆ m, and this must be the unique j with this property as m ⊆ m′, since I is non-empty.

We deal with the case (finite, fddc) by showing that the set of models of a family Φ of formulae of the form ⋀ X ⇒ (⋁_{j∈J} ⋀ Y_{j}) ∧ ⋀_{j,k∈J, j≠k} ¬(⋀ Z_{j,k} ∧ ⋀ Z_{k,j}), with X finite and the Z_{j,k} finite subsets of Y_{j}, is closed under finitely consistent non-empty intersections. Suppose that {m_{i} | i ∈ I} is a set of models of Φ, with union m′ and intersection m, such that Cn_{fin}(m′). We must show that m is a model. To this end, choose one implication X ⇒ (⋁_{j∈J} ⋀ Y_{j}) ∧ ⋀_{j,k∈J, j≠k} ¬(⋀ Z_{j,k} ∧ ⋀ Z_{k,j}) in Φ and suppose that m includes its premise X. Then, for i ∈ I, so does m_{i} and hence there is a unique j(i) in J such that Y_{j(i)} ⊆ m_{i}. We claim that, for i ∈ I, all j(i) are the same. For otherwise m′ would contain the finite set X ∪ Z_{j,k} ∪ Z_{k,j} for j, k ∈ J, j ≠ k. As Cn_{fin}(m′) this set would be included in a model of Φ, which is a contradiction. Hence there is a unique j in J such that Y_{j} ⊆ m_{i} for all i ∈ I. So Y_{j} ⊆ m, and this must be the unique j with this property as m ⊆ m′, since I is non-empty. □

For the converse direction we go from event structures to propositional theories. Given any event structure E satisfying a collection of properties of Table 2 we seek to axiomatise its associated configuration structure L(E) by formulae whose form is one of the combinations of the forms found on the corresponding lines of the table. In combining forms (L_{i}, R_{i}) (i ∈ I) into a form (L, R) we obtain L and R as the meets in the form lattices given in Figure 4. For example, for singular conjunctive event structures the axiomatisation will be by formulae of one of the two forms (1, ≤1) and (any, 0).

Theorem 7 Let E be a (pure) event structure satisfying any collection of properties of Table 2. Then L(E) can be axiomatised by (pure) formulae whose forms are one of the combinations of the forms found on the corresponding lines of the table.

Proof: We first consider collections of properties not involving (local) conjunctivity. By Proposition 1.1, for any event structure E, L(E) can be axiomatised by the set of formulae

φ_{X} := (⋀ X ⇒ ⋁_{Y ⊢X} ⋀ Y)

for X ⊆ E; expanding out φ_{X} to conjunctive normal form yields a set of clauses Φ_{X}, and ⋃_{X⊆E} Φ_{X} axiomatises L(E).

If E is rooted, i.e., ∅ ⊢ ∅, then φ_{∅} is a tautology and Φ_{∅} is empty. Hence all clauses in ⋃_{X⊆E} Φ_{X} have the form (>0, any).

If E is singular, whenever Y ⊢ X then either Y is empty or X is a singleton. If |X| = 1 then Φ_{X} is a set of formulae of the form (1, any). If |X| ≠ 1, there either is a relation Y ⊢ X or not: if there is then φ_{X} is a tautology and Φ_{X} is empty, and if not we obtain the single clause (X, ∅).

If E has finite conflict then for any infinite X, φ_{X} is a tautology and Φ_{X} empty. For finite X, Φ_{X} consists of clauses of the form (finite, any). The case of binary conflict is similar.

We now turn to collections of properties including (local) conjunctivity. Note that conjunctivity implies local conjunctivity. Let E be a locally conjunctive event structure. One easily sees that if Y ⊢ X and Con(Y ∪ X) then there is a least Z ⊆ Y such that Z ⊢ X and, further, if Z and W are two minimal sets with Z ⊢ X and W ⊢ X, then either Z = W or else it is not true that Con(Z ∪ W ∪ X). If we now keep only those pairs Y ⊢ X such that Con(Y ∪ X), and such that Y is a minimal set with Y ⊢ X, then we obtain an event structure E′ = ^{/}_{\}E, ⊢′^{\}_{/} with the same collection of configurations as E and such that if Z ⊢′ X and W ⊢′ X then either Z = W or else it is not true that Con′(Z ∪ W ∪ X). Further if E was pure, rooted, singular, conjunctive, or with finite or binary conflict then so is E′.

First consider the case that conjunctivity is among the considered properties of E. Exactly as above we find that L(E′) is axiomatised by the set of formulae φ′_{X} := (⋀ X ⇒ ⋁_{Y ⊢′X} ⋀ Y) for X ⊆ E; and by its conjunctive normal form ⋃_{X⊆E} Φ′_{X}. As E′ is conjunctive, for each set of events X there is at most one set Y with Y ⊢′ X. If such a Y exists, Φ′_{X} consists of the formulae (X, {e}) for e ∈ Y; otherwise it consists of the single clause (X, ∅). Thus all formulae have the form (any, ≤ 1). The arguments for the other properties of E are exactly as before.

We proceed with collections of properties including local connectivity, but excluding connectivity. We see again that L(E′) is axiomatised by the set of formulae φ′_{X} := (⋀ X ⇒ ⋁_{Y ⊢′X} ⋀ Y) for X ⊆ E. But since it is false that Con′(Z ∪ W ∪ X) when Z ⊢′ X, W ⊢′ X and Z ≠ W, no configuration can include Z ∪ W ∪ X.

Hence the set of formulae

φ̇_{X} := (⋀ X ⇒ · ; ⋁ ; Y ⊢′X ⋀ Y)

for X ⊆ E axiomatises L(E′), and thus L(E), as φ̇_{X} implies φ_{X} and holds in all interpretations in L(E′). These formulae have the form (any, ddc).

If E, and hence E′, is rooted then φ̇_{∅} is a tautology and can be omitted. All remaining formulae have the form (>0, ddc).

Suppose next that E, and hence E′, is both locally conjunctive and singular. Then, much as above, for nonsingular X, φ̇_{X} is either a tautology or equivalent to a formula of the form (any, 0), and for singular X it has the form (1, ddc).

Suppose now that E′ is both locally conjunctive and with finite conflict. Then for infinite X, φ̇_{X} is a tautology. For finite X we know that if Z ⊢′ X, W ⊢′ X and Z ≠ W then it is not true that Con′(Z ∪ W ∪ X). So as E′ has finite conflict, it follows that there are finite subsets Z_{1} and W_{1} of, respectively, Z and W such that for no Y is it the case that Y ⊢′ Z_{1} ∪ W_{1} ∪ X. It follows that Z_{1} ∪ W_{1} ∪ X is a subset of no configuration. Since this works for any such Z and W there is a (finite, fddc) formula that implies φ̇_{X} and that holds in all interpretations in L(E′), and so we have the required axiomatisation.

The case where E′ is locally conjunctive, singular and with finite conflict is an easy combination of the previous two cases. When E′ is rooted, ∅ ⊢′ ∅ and so we need only then consider φ̇_{X} for nonempty X.

Suppose now that E′ is both locally conjunctive and with binary conflict. Then for X with |X| > 2, φ̇_{X} is a tautology. For X with |X| ≤ 2 we know that if Z ⊢′ X, W ⊢′ X and Z ≠ W then it is not true that Con′(Z ∪ W ∪ X). So as E′ has binary conflict, and Con′(Z∪X) and Con′(W ∪X), it follows that there are elements e and e′ of, respectively, Z and W such that for no Y is it the case that Y ⊢′ {e, e′}. It follows that {e, e′} is a subset of no configuration. Since this works for any such Z and W there is a (≤ 2, bddc) formula that implies φ̇_{X} and that holds in all interpretations in L(E′), and so we have the required axiomatisation.

The cases where E′ is locally conjunctive and has binary conflict, and is one or both of singular or rooted are dealt with as before.

Finally we remark that, in the above, in all cases the axiomatisation obtained is pure if E′ is. □

An immediate consequence of the above work (Theorems 6, 5 and 7 and Proposition 5.1) is that a configuration structure is axiomatisable by formulae of the form (finite, ≤ 1) iff it is closed under nonempty intersections and directed unions; this result is essentially due to Larsen and Winskel [23] as axiomatisations of the form (finite, ≤1) correspond to Scott information systems. There are two related cases of logical interest: Horn clauses where there are finitely many antecedents and one consequent, and Scott clauses where, more generally, there may be finitely many consequents [7, 32].

Proposition 5.4 A configuration structure ^{/}_{\}E, C^{\}_{/} is Horn clause axiomatisable iff it is closed under arbitrary intersections and directed unions. It is Scott clause axiomatisable iff C is closed in the product topology on 2^{E}.

Proof: For the implication from left to right in the first statement, we have just established closure under directed unions and non-empty intersections. Closure under the empty intersection is immediate, as E is a model of any set of Horn clauses. For the converse, we have an axiomatisation by clauses of the form X ⇒ Y where X is finite and Y is empty or a singleton. But the first case cannot obtain, as here E is a model.

For the second statement, the product topology on 2^{E} is the E-fold power of the discrete topology on the two-point set. Identifying 2^{E} with P(E), we see that the space has as basis all sets of the form

U_{x,y} = {m ⊆ E | x ⊆ m, (m ∩ y) = ∅}

where x,y are finite subsets of E. The statement now follows, noting that the complement of U_{x,y} is the set of models of x ⇒ y. □

5.3 Secured configuration structures

In Section 5.1 we characterised the left-closed configuration structures associated to various classes of event structures. Here we do the same for the secured configuration structures of secure event structures. Our results are indicated in Table 3.

Unlike in Theorem 4 it is not always the case that the secured configuration structure associated to a secure event structure with finite (resp. binary) conflict has finite (resp. binary) conflict.

Example 17 Let E = ^{/}_{\}E, ⊢^{\}_{/} be given by

E := {a_{i}, b_{i} | i ∈ IN} ∪ {c},

{a_{i}} ⊢ {b_{i}}, {b_{i}} ⊢ {a_{i+1}}, {b_{i}} ⊢ {c, a_{i}} (i ∈ IN) and ∅ ⊢ X for any X ⊆ E unequal to {a_{i+1}}, {b_{i}} or {c, a_{i}} (i ∈ IN). Then

R_{f}(E) = \begin{cases}\{a_{i}, b_{i} | i < n\} \\ \{a_{i}, b_{i} | i < n\} ∪ \{a_{n}\} \\ \{a_{i}, b_{i} | i < n\} ∪ \{c\} \end{cases} | n ∈ IN\} ,

Event  Configuration
structures  structures
rooted  rooted
singular  closed under \overline{⋃}
conjunctive  closed under ⋂_{•}
locally conjunctive closed under \overline{⋂}_{•}
finite conflict  hyperreachable finite conflict
binary conflict  hyperreachable binary conflict
singular & fin. con. closed under \overline{⋃}^{f}
singular & bin. con. closed under \overline{⋃}^{2}
loc. conj. & fin. con. closed under \overline{⋂}_{•}^{f}
loc. conj. & bin. con. closed under \overline{⋂}_{•}^{2}

Table 3: Corresponding properties, secured case

S(E) = R_{f}(E) ∪ {{a_{i}, b_{i} | i ∈ IN}}

and L(E) = S(E) ∪ {E}.

The configuration E is not secured because once c happens only finitely many of the a_{i} and b_{i}’s can have happened, and no further a_{i} and b_{i}’s can happen, because such an a_{i} needs to be preceded by b_{i} and vice versa. Nevertheless, each finite subset of E is contained in a secured configuration. It follows that S(E) does not have finite (or binary) conflict, even though E does have finite (even binary) conflict.

The event structure of Example 17 is pure, secure, rooted and conjunctive. By Theorem 8.6 below there can be no such example with a singular event structure. Example 17 shows in fact that the requirement of being hyperconnected, which by Corollary 8 holds for configuration structures of the form S(E) with E secure, can prevent the presence of configurations required by Definition 5.2.4. Hence it is appropriate to weaken the requirement of Definition 5.2.4.

Definition 5.5 Let C = ^{/}_{\}E, C^{\}_{/} be a configuration structure. Its closure under finite conflict, C^{f} := /_{\}E, C^{f}^{\}_{/}, is the configuration structure with the same set of events, and as configurations those sets X satisfying

∀Y ⊆ X. (Y finite ⇒ ∃z ∈C. Y ⊆ z ⊆ X).

Likewise, its closure under binary conflict, C^{b} := /_{\}E, C^{b}^{\}_{/}, has as configurations those sets X satisfying

∀Y ⊆ X. (|Y | ≤ 2 ⇒ ∃z ∈C. Y ⊆ z ⊆ X).

One always has C ⊆ C^{f} ⊆ C^{b} (in the first inclusion take z to be X). Note that C has finite conflict iff C = C^{f} and C has binary conflict iff C = C^{b}. Hence the following appear to be suitable replacements of these notions for hyperconnected configuration structures.

Definition 5.6 A configuration structure C = ^{/}_{\}E, C^{\}_{/} has hyperreachable finite conflict if C = S(C^{f}). It has hyperreachable binary conflict if C = S(C^{b}).

In other words, a configuration structure C = ^{/}_{\}E, C^{\}_{/} has hyperreachable finite (resp. binary) conflict iff X ∈ C exactly when X can be written as ⋃_{i=0}^{∞} X_{i} such that X_{0} = ∅ and, for all i ∈ IN, X_{i} ⊆ X_{i+1} and for all X with X_{i} ⊆ X ⊆ X_{i+1} one has

∀Y ⊆X. Y finite (resp. |Y |≤2) ⇒ ∃z ∈C. Y ⊆ z ⊆ X.

We proceed to show that a configuration structure has hyperreachable finite (resp. binary) conflict iff it has the form S(C) for C a configuration structure with finite (resp. binary) conflict.

Lemma 2 Let C be a configuration structure. Then (C^{f})^{f} = C^{f} and (C^{b})^{b} = C^{b}.

Proof: Suppose X is a set of events satisfying

∀Y ⊆ X. Y finite ⇒ ∃z ∈C^{f}. Y ⊆ z ⊆ X

and let Y ⊆ X be finite. Then there is a z ∈ C^{f} with Y ⊆ z ⊆ X. Hence there is a w ∈ C with Y ⊆ w ⊆ z ⊆ X. Thus X ∈ C^{f}.

That (C^{b})^{b} = C^{b} follows likewise. □

Corollary 13 Let C be a configuration structure. Then C^{f} has finite conflict and C^{b} binary conflict. □

Proposition 5.5 A configuration structure has hyperreachable finite conflict iff it has the form S(C) for C a configuration structure with finite conflict.

Likewise, a configuration structure has hyperreachable binary conflict iff it has the form S(C) for C a configuration structure with binary conflict.

Proof: “Only if” follows immediately from Definition 5.6 and Corollary 13. For “if” suppose that C = /_{\}E, C^{\}_{/} has finite conflict, i.e., C = C^{f}. By Theorem 5 there is a pure event structure with finite conflict such that C = L(E). So S(C) = S(L(E)) = S(E) ⊆ L(E) = C by Proposition 3.12 and Lemma 1. Hence C is SRsecure, and Proposition 3.4 yields S(S(C)) = S(C). Using the monotonicity w.r.t. the inclusion ordering of the operators (·)^{f} and S we find

S((S(C))^{f}) ⊆ S(C^{f}) = S(C) = S(S(C)) ⊆ S((S(C))^{f}).

Thus S(C) = S((S(C))^{f}), i.e., S(C) has hyperreachable finite conflict, which had to be shown.

The second statement is obtained likewise, reading “binary” for “finite” and b for f. □

We are now ready to prove the implications from the left to the right column of Table 3.

Theorem 8 Let E be a secure^{6} event structure.

0. If E is rooted, then so is S(E).

1. If E is singular, then S(E) is closed under \overline{⋃}.

2. If E is conjunctive, then S(E) is closed under ⋂_{•}.

3. If E is locally conjunctive, then S(E) is closed under \overline{⋂}_{•}.

4. If E has finite conflict, then S(E) has hyperreachable finite conflict.

5. If E has binary conflict, then S(E) has hyperreachable binary conflict.

6. If E is singular and with finite conflict, then S(E) is closed under \overline{⋃}^{f}.

7. If E is singular and with binary conflict, then S(E) is closed under \overline{⋃}^{2}.

8. If E is locally conjunctive and with finite conflict, then S(E) is closed under \overline{⋂}_{•}^{f}.

9. If E is locally conjunctive and with binary conflict, then S(E) is closed under \overline{⋂}_{•}^{2}.

Proof: Claim 0 is immediate from Definition 3.2. For claims 4 and 5, note that if E is reachably pure and with finite (or binary) conflict, then Ê, as constructed in the proof of Proposition 3.15, is pure and with finite (or binary) conflict, and S(E) = S(Ê). Now the results are immediately from Theorem 4 and Propositions 3.12 and 5.5. For the remaining claims, let A ⊆ S(E). By “consistency” we will mean that Con(⋃ A). This follows for Claims 1, 3, 6, 7, 8 and 9 (but not 2) because S(E) ⊆ L(E) and either Cn(⋃ A), or Cn_{fin}(⋃ A) and E has finite conflict, or Cn_{2}(⋃ A) and E has binary conflict. Applying Definition 3.5, for each x ∈ A let x = ⋃_{n=0}^{∞} x_{n} with x_{0} = ∅ and

∀n ∈ IN. x_{n} ⊆ x_{n+1} ∧ ∀Y ⊆ x_{n+1}. ∃Z ⊆ x_{n}. Z ⊢ Y.

Ad 1, 6 and 7. Let X_{n} := ⋃_{x∈A} x_{n} for n ∈ IN. Then X := ⋃ A = ⋃_{n=0}^{∞} X_{n}. Moreover, X_{0} = ∅ and X_{n} ⊆ X_{n+1} for n ∈ IN. Let e ∈ X_{n+1} for some n ∈ IN. Then e ∈ x_{n+1} for certain x ∈ A. Thus ∃Z ⊆ x_{n} ⊆ X_{n}. Z ⊢ {e}. By consistency and singularity, ∅ ⊢ Y for any Y ⊆ X with |Y | ≠ 1. Hence X ∈ S(E).

Ad 2, 3, 8 and 9. Let A ≠ ∅ and pick a y from A. Let X_{n} = y_{n} ∩ ⋂ A for n∈IN. Then ⋂ A = ⋃_{n=0}^{∞} X_{n}. Moreover, X_{0} = ∅ and X_{n} ⊆ X_{n+1} for n ∈ IN. Now let Y ⊆ X_{n+1} for some n ∈ IN. Then Y ⊆ y_{n+1} and Y ⊆ x for x∈A. Hence there is a Z ⊆ y_{n} with Z ⊢ Y. Moreover, as E is secure, for x ∈ A we have x ∈ L(E), so there must be a Z_{x} ⊆ x with Z_{x} ⊢ Y. Now by the conjunctivity of E, or by consistency and the local conjunctivity of E, we obtain that Z∩⋂_{x∈A} Z_{x} ⊢ Y, with Z∩⋂_{x∈A} Z_{x} ⊆ X_{n}. Hence X ∈ S(E). □

By Lemma 1, the security requirement S(E) ⊆ L(E) holds trivially in case E has finite conflict, i.e., in Claims 4–9 of Theorem 8; it is not needed for Claims 0 and 1 and used in the proof of claims 2 and 3. The question whether this requirement is needed there is open. The following example shows that Claims 4 and 5 fail for general event structures that are not reachably pure:

Example 18 Let E := ^{/}_{\}IN, ⊢^{\}_{/} be given {j} ⊢ {i, j} for i < j and ∅ ⊢ X when |X| ≠ 2. Then S(E) = R_{f}(E) = 𝒫_{fin}(IN) but S((S(E))^{f}) = L(E) = 𝒫(IN). The infinite configurations are not secured, because events can happen only in decreasing order. Nevertheless, each finite set of events is (contained in) a secured configuration. It follows that S(E) does not have hyperreachable finite (or binary) conflict, even though E does have finite (even binary) conflict.

There does not appear to be an obvious way around this example, as the above event structure has the same secured configurations as one with X ⊢ Y iff X = ∅ and Y finite, which is a prototypical example of an otherwise trivial event structure with infinite conflict. Happily, our goal is to deal with secure event structures anyway, as those fit the computational interpretation of configuration structures.

In order to establish the completeness of the characterisations of Table 3 we first show that some crucial properties of Definition 5.2 are preserved under closure under finite or binary conflict.

Lemma 3 Let C be a configuration structure.

• If C is closed under ^{\overline{⋃}^{f}} then so is C^{f}.

• If C is closed under \overline{⋂}_{•}^{f} then so is C^{f}.

• If C is closed under ^{\overline{⋃}^{2}} then so is C^{b}.

• If C is closed under \overline{⋂}_{•}^{2} then so is C^{b}.

• If C is closed under ⋂_{•} then so are C^{f} and C^{b}.

• If C is rooted then so are C^{f} and C^{b}.

6In fact, for Claims 4 and 5 it suffices to assume that E is reachably pure, and for the other claims that S(E) ⊆ L(E).

Proof: Let C = ^{/}_{\}E, C^{\}_{/}. Note that, for each X ⊆ E,

∀Y ⊆_{fin} X. ∃z ∈C^{f}. Y ⊆z ⇔ ∀Y ⊆_{fin} X. ∃z ∈C. Y ⊆z,

i.e., X is finitely consistent w.r.t. C^{f} iff it is finitely consistent w.r.t. C—hence we can write Cn_{fin}(X) without indicating whether it is w.r.t. C^{f} or C.

Suppose first that C is closed under \overline{⋃}^{f}. Let A ⊆ C^{f} be a family of configurations of C^{f} such that Cn_{fin}(⋃ A). We wish to show that ⋃ A ∈ C^{f}. Suppose that Y ⊆_{fin} ⋃ A. Then Y has the form ⋃_{i=1}^{n} Y_{i} for some n ≥ 0 where Y_{i} ⊆_{fin} x_{i} for some x_{i} ∈ A for i = 1, ..., n. So there are z_{i} ∈ C such that Y_{i} ⊆ z_{i} ⊆ x_{i}. We then have that Z := ⋃_{i=1}^{n} z_{i} ⊆ ⋃ A. Since Cn_{fin}(⋃ A) we have Cn_{fin}(Z). As C is closed under ^{\overline{⋃}^{f}} it follows that Z ∈ C. As we also have that Y ⊆ Z ⊆ ⋃ A, it follows that ⋃ A is a configuration of C^{f}, as required.

Suppose instead that C is closed under \overline{⋂}_{•}^{f}. Let ∅ ≠ A ⊆ C^{f}, such that Cn_{fin}(⋃ A). We wish to show that ⋂ A ∈ C^{f}. Suppose that Y ⊆_{fin} ⋂ A. Then Y ⊆_{fin} x for each x∈A and so there are z_{x} ∈ C with Y ⊆ z_{x} ⊆ x. Since Cn_{fin}(⋃_{x∈A} x) we have Cn_{fin}(⋃_{x∈A} z_{x}). As C

is closed under \overline{⋂}_{•}^{f} it follows that z := ⋂_{x∈A} z_{x} ∈ C. As moreover Y ⊆ z ⊆ X, it follows that ⋂ A is a configuration of C^{f}, as required.

The claims about binary conflict are proved just like the ones about finite conflict, and the claims about closure under ⋂_{•} are obtained as simplifications of the arguments about \overline{⋂}_{•}^{f} above. The claims about rootedness are trivial. □

Theorem 9 A hyperconnected configuration structure C has any package of properties from the second column of Table 3 iff there is a (pure and) secure event structure E with the corresponding properties such that S(E) = C.

Proof: “If” follows from Theorem 8 and Corollary 8. For “only if”, let C^{∗} := C^{b} in case the package contains hyperreachable binary conflict; if that does not apply, C^{∗} := C^{f} in case the package contains hyperreachable finite conflict, and C^{∗} := C otherwise. Now S(C^{∗}) = C and, by Lemma 3 and Corollary 13, C^{∗} has the same package of properties as C but dropping the adjective “hyperreachable”. Thus, using Theorem 5, there exists a pure event structure E with the corresponding properties such that L(E) = C^{∗}. Using Proposition 3.12, S(E) = S(L(E)) = S(C^{∗}) = C. By Proposition 3.16, the event structure E is secure. □

Trivially, an event structure E is S-irredundant iff the configuration structure S(E) is irredundant; thus Theorems 8 and 9 can be upgraded by adding S-irredun-dancy and irredundancy to Table 3. L-irredundan-cy and cycle-freeness are not particularly interesting properties when studying secured configurations. For the property finite causes we have correspondence results only for singular event structures:

Definition 5.7 A configuration structure is said to satisfy the axiom of finiteness [34, 35] if any configuration is the union of its finite subconfigurations.

Proposition 5.6 If E is a singular event structure with finite causes, then S(E) satisfies the axiom of finiteness (and is closed under \overline{⋃}). Conversely, if C is a hyperconnected configuration structure satisfying the axiom of finiteness and any package of properties from the second column of Table 3 including closure under \overline{⋃}, then there is a pure and secure event structure E with finite causes and the corresponding properties of Table 3, such that S(E) = C.

Proof: The first claim has been established in the first statement of Proposition 4.2, of which direction “⇒” only requires singularity and finite causes.

For “conversely”, first of all note that if C satisfies the axiom of finiteness, then so do C^{f} and C^{b}. Now note that in the proof of Theorem 5, which is called in the proof of Theorem 9, one may replace the definition of ⊢_{1} by

X ⊢_{1} Y iff |Y | = 1, X ∩ Y = ∅ and X ∪ Y ∈ F (C)

because any Y -event occurring in a configuration occurs in a finite subconfiguration and whenever X ⊢ Y all enablings X′ ⊢ Y with X′ ⊇ X may be dropped. By construction, the resulting event structure has finite causes. □

For configuration structures satisfying the axiom of finiteness we can reformulate the condition of being closed under ^{\overline{⋃}^{f}}.

Proposition 5.7 Let C be a configuration structure satisfying the axiom of finiteness. Then C is closed under ^{\overline{⋃}^{f}} iff it is closed under ^{\overline{⋃}^{fc}}.

Proof: “Only if” is trivial, so suppose C = ^{/}_{\}E, C^{\}_{/} is closed under \overline{⋃}^{fc}. Let A ⊆ C with Cn_{fin}(⋃ A). We have to show that ⋃ A ∈ C. Let B be the set of all finite configurations included in members of A. Then for all F ⊆_{fin} B we have that ⋃ F ⊆_{fin} ⋃ A and hence Cn(⋃ F). By the axiom of finiteness, ⋃ A = ⋃ B ∈ C.

Moreover, for configuration structures satisfying the axiom of finiteness and closed under^{\overline{⋃}^{f}} we reformulate the condition of being hyperconnected.

Proposition 5.8 Let C be a configuration structure closed under ^{\overline{⋃}^{f}} and satisfying the axiom of finiteness. Then C is hyperconnected iff it is coincidence-free.

Proof: “Only if” is trivial, so suppose C = ^{/}_{\}E, C^{\}_{/} is coincidence-free. Closure under ^{\overline{⋃}^{f}} immediately implies that S(C) ⊆ C, so it remains to be shows that C ⊆ S(C). Let x ∈ C. For any e ∈ x say that e can happen at stage n if n is the smallest cardinality of a subconfiguration of x containing e. By the axiom of finiteness, this cardinality is always finite. Let X_{n} be the set of all events in x that can happen at stage ≤n. Then X_{0} = ∅, X_{n} ⊆ X_{n+1} for n∈IN and ⋃_{n=0}^{∞} X_{n} = x. As X_{n} is the union of all subconfigurations of x of size ≤n and C is closed under \overline{⋃}, we have X_{n} ∈C for n∈IN. Let X_{n} ⊆ Y ⊆ X_{n+1} for some n ∈ IN. It suffices to show that Y ∈ C. For any e ∈ Y − X_{n} pick a subconfiguration y_{e} of x of n + 1 elements, containing e. Given that y_{e} does not have a proper subconfiguration containing e, for any d ≠ e in y_{e}, by coincidencefreeness, there must be subconfiguration z_{d} of y_{e} with d ∈ z_{d} ⊆ y_{e} − {e}, showing that d ∈ X_{n} ⊆ Y. It follows that y_{e} ⊆ Y. Hence Y = X_{n} ∪ ⋃_{e∈Y −X_{n}} y_{e} and as C is closed under \overline{⋃} we have Y ∈ C. □

We now apply the results of this section to characterise the secured configuration structures associated to the various event structures of Winskel [34, 35].

Corollary 14 A configuration structure arises as the family of (secured) configurations of an event structure of [34] iff it satisfies the axioms of rootedness, finiteness, coincidence-freeness and finite-completeness.

A configuration structure arises as the family of (secured) configurations of a stable event structure of [34] iff it moreover is closed under \overline{⋂}_{•}. □

These characterisations were obtained earlier in [34]. However, the following one seems to be new.

Corollary 15 A configuration structure arises as the family of configurations of a prime event structure of [34] iff it satisfies the axioms of rootedness, finiteness, coincidence-freeness, finite-completeness, irredundancy and closure under ⋂_{•}. □

Recall that for these structures the left-closed and secured configurations are the same.

Corollary 16 A configuration structure arises as the family of (secured) configurations of an event structure of [35] iff it satisfies the axioms of rootedness, finiteness, coincidence-freeness and closure under ^{\overline{⋃}^{2}}.

A configuration structure arises as the family of (secured) configurations of a stable event structure of [35] iff it moreover is closed under \overline{⋂}_{•}. □

In [34] the characterisations above were claimed, but using coherence (cf. Definition 5.3.7) instead of closure under ^{\overline{⋃}^{2}}. Arend Rensink [personal communication, around 1996] provided the following counterexample against that characterisation.

Example 19 Let C = ^{/}_{\}E, C^{\}_{/} be given by E:= {a, b, c} and

C := {∅, {a}, {b}, {a, b}, {a, c}, {b, c}}.

Then C satisfies the axioms of rootedness, finiteness, coincidence-freeness, closure under \overline{⋂}_{•} and coherence, but it is not closed under ^{\overline{⋃}^{2}} (cf. Definition 5.2.7). By Corollary 16 it therefore cannot arise as the family of configurations of an event structure of [35].

We now propose the property of closure under ^{\overline{⋃}^{2}} as the replacement for coherence in this theorem. Using Proposition 5.1 we can replace closure under ^{\overline{⋃}^{2}} (and rootedness) by coherence if we have closure under ⋂_{•}. This gives the following, apparently novel, characterisation.

Corollary 17 A configuration structure arises as the family of configurations of a prime event structure of [35] iff it satisfies the axioms of finiteness, coincidencefreeness, coherence, irredundancy and closure under ⋂_{•}. □

Propositional theories

We do not have axiomatic characterisations of properties like connectedness or hyperconnectedness, and therefore we cannot offer a third column for Table 3 such that for C a hyperconnected configuration structure satisfying a package of properties, a suitably axiomatised T theory can be found for which M(T) = C. As best we could work up to reachable equivalence, and be content with a theory T such that S(M(T)) = C. In this context we directly inherit the third column of Table 2—however, only for theories that are secure, a property for which we have no axiomatic characterisation.

Definition 5.8 A configuration structure C = ^{/}_{\}E, C^{\}_{/} is secure if S(C) ⊆ C, and a propositional theory T is secure if M(T ) is.

Note that if C is secure, then so is any pure event structure E with L(E) = C.

Corollary 18 A hyperconnected configuration structure C has any package of properties from the second column of Table 3 iff there is a secure propositional theory T whose formulae are of one of the combinations of the forms found on the corresponding lines of Table 2, such that S(M(T)) = C.

Proof: Given a hyperconnected configuration structure C satisfying a package of properties from the second column of Table 3, Theorem 9 yields a pure and secure event structure with the corresponding properties such that S(E) = C. By Theorem 7, there is a theory T whose formulae are of one of the combinations of the forms found on the corresponding lines of Table 2, such that M(T) = L(E). As E is secure, so is L(E) and hence T. Using Proposition 3.12 we find S(M(T)) = S(L(E)) = S(E) = C.

Conversely, given a package of properties from the second column of Table 3, let T be a secure theory whose formulae are of one of the combinations of the forms found on the corresponding lines of Table 2. Then Theorem 6 yields that M(T) has the corresponding package of properties from the second column of Table 2 (i.e., skipping “hyperreachable”), so by Theorem 5 there is a pure event structure E with the corresponding properties such that L(E) = M(T). As noted above, E is secure, and by Theorem 8 S(E) has the given package of properties. Furthermore, S(E) = S(L(E)) = S(M(T)). □

In case of a package of properties including finite conflict, or excluding (local) conjunctivity, the requirement that T be secure may be dropped. This follows from the remarks following Theorem 8.

We do not have an axiomatic characterisation of irredundancy, nor of the axiom of finiteness, and hence neither of the event structures from [34, 35].

Reachable configuration structures

We were unable to find correspondences of the form of Table 3 using reachable configurations instead of secured ones. The problem we encountered is that the set of reachable configurations of a singular event structure need not be closed under bounded unions.

Example 20 Let E=^{/}_{\}E, ⊢^{\}_{/} be given by E:=IN · ∪ {e}, {n} ⊢ {n + 1} and {e} ⊢ {n + 1} for n ∈ IN and ∅ ⊢ X for X not of the form {n + 1}. This event structure is rooted and singular and has finite conflict. Its reachable configurations include {0 …, n} for all numbers n, together with all sets containing e. In particular the set of all events is a reachable configuration, because after e all other events can happen in one step. However, IN is not a reachable configuration. Therefore, R(E) fails to be closed under bounded intersections.

5.4 Two finitary comparisons

In this section we characterise the configuration structures that arise by taking the finite left-closed configurations of the various classes of event structures. We also characterise the corresponding propositional theories, but working up to finitary equivalence only. Thus, given a finitary configuration structure C satisfying some relevant closure properties, we seek a proposition theory T of a particular form such that F(M(T)) = C; we do not seek a theory T with M(T) = C. Subsequently, we do the same for the finite reachable configurations of the various classes of event structures. We can put any event structure E into a “finitary” form E_{f} by removing all causal relations Y ⊢ X with X or Y infinite and then adding all ∅ ⊢ X for X infinite. Clearly E_{f} has finite causes and finite conflict, and F(L(E_{f})) = F(L(E)). Thus, by Theorem 5, any finitary configuration structures arises as F(L(E)) for an event structure E with finite causes and finite conflict. Next, since every clause of the form Y ⇒ X with Y infinite is satisfied by any finite configuration, up to finitary equivalence any configuration structure has an axiomatisation by formulae of the form (fin, any). Thus, at the level of finitary equivalence, we have a general correspondence between (pure) event structures (with finite causes and finite conflict), finitary configuration structures and this class of propositional theories.

For particular correspondences we again consider the relevant properties of event structures and their correspondences in configuration structures and propositional theories. We consider pureness, rootedness, singularity, conjunctivity, local conjunctivity and binary conflict, as finite conflict is already built in. For finitary configuration structures, the distinctions between \overline{⋃} and \overline{⋃}^{f}, and between \overline{⋂}_{•} and \overline{⋂}_{•}^{f}, disappear, and indeed we are left with closure conditions, \overline{∪}_{f}, ∩, \overline{∩}, \overline{∪}_{f}^{2} and \overline{∩}^{2}, meaning, respectively: closure under finite bounded unions, binary intersections, bounded binary intersections, finite pairwise consistent unions and pairwise consistent binary intersections.

Observation 5.1 A finitary configuration structure – is closed under \overline{⋃} iff it is closed under \overline{∪}_{f};

– is closed under ⋂_{•} iff it is closed under ∩;

– is closed under \overline{⋂}_{•} iff it is closed under \overline{∩};

– is closed under \overline{⋃}^{2} iff it is closed under \overline{∪}_{f}^{2};

– is closed under \overline{⋂}_{•}^{2} iff it is closed under \overline{∩}^{2}.

Note that a configuration structure is closed under \overline{∪}_{f} iff it is closed under \overline{∪} and is either rooted or empty. We say that a configuration structure C has finite binary conflict iff for every finite set of events X

[∀Y ⊆X. (|Y | ≤2 ⇒ ∃z ∈C. Y ⊆z ⊆X)] ⇒ X∈C.

Note that a finitary configuration structure C has finite binary conflict iff C = F(C^{b}) with C^{b} its closure under binary conflict, as introduced in Definition 5.5.

Observation 5.2 If a configuration structure C is closed under \overline{⋃}, ⋂_{•}, \overline{⋂}_{•}, \overline{⋃}^{2} or \overline{⋂}_{•}^{2}, then so is F(C). Furthermore, if C has binary conflict then F(C) has finite binary conflict.

For propositional theories used for comparison up to finitary equivalence we replace “ddc” and “bddc” by new forms “ddfc” and “bddfc”, meaning finite conjunctions. The interpretation of the resulting forms (L, R) should be clear; as before, they are combined by taking meets in the left and right lattices. We get the correspondences summarised by Table 4.

Event  Configuration Propositional
structures  structures  theories
rooted  rooted  (nef, any)
singular  closed under \overline{∪}_{f} (1, any), (fin., 0)
conjunctive  closed under ∩ (fin., ≤1)
locally conj.  closed under \overline{∩} (fin., ddfc)
binary conflict fin. bin. conflict (≤2, any)
sing. & bin. con. closed under \overline{∪}_{f}^{2} (1, any), (≤2, 0)
loc. conj. & b.c. closed under \overline{∩}^{2} (≤2, bddfc)

Table 4: Corresponding properties for finite parts

We define a package of properties of configuration structures from the table analogously to before. We call a set of properties from the second column of Table 4 a package if

– it contains the property “closed under \overline{∪}_{f}^{2}” iff it contains the properties “closed under \overline{∪}_{f}” and “having finite binary conflict”, and

– it contains the property “closed under \overline{∩}^{2}” iff it contains the properties “closed under \overline{∩}” and “having finite binary conflict.”

We can now formulate the correspondences explicitly as:

Theorem 10

1. Let E be a (pure) event structure satisfying any collection of properties from Table 4. Then there is a (pure) propositional theory T whose axioms have forms which are combinations of the forms corresponding to the event structure properties, such that F(M(T)) = F(L(E)).

2. Let T be a propositional theory whose axioms have forms which are combinations of forms from a given collection of rows of Table 4. Then F(M(T)) has the corresponding collection of properties of configuration structures.

3. Let C be a finitary configuration structure satisfying a given package of properties from Table 4. Then there is a pure event structure E with finite causes and finite conflict such that F(L(E)) = C and with the corresponding collection of properties of event structures.

Proof:

1. Given a (pure) event structure E satisfying a given collection of properties of the table, Theorem 7 yields an axiomatisation of L(E) by a (pure) propositional theory T whose axioms have the form of a combination of the forms corresponding to the properties given by Table 2. Now we can remove any formulae of the form (X, −) with X infinite from the axiomatisation as they are automatically true in finite interpretations (i.e., the finite subsets of E). (Alternatively, we could have obtained these forms by requiring E, without limitation of generality, to be with finite conflict.) Next, to any formula of the form (−, ddc) one can associate a formula of the form (−, ddfc) by removing all infinite disjuncts, and the associated formula is true in a finite interpretation iff the original one is; the same holds for (−, bddc) and (−, bddfc) formulae. Making these replacements as necessary, one arrives at the required (pure) propositional theory

2. Given any propositional theory T whose axioms have the form of combinations of forms given in rows of the table, then, by Theorem 6, M(T) satisfies the corresponding properties of Table 2 and so, by Observations 5.2 and 5.1, F(M(T)) satisfies the corresponding properties of Table 4.

3. Let C be a finitary configuration structure with a given package of properties of the table, not including finite binary conflict. Then, by Observation 5.1, C satisfies the corresponding package of properties of Table 2, and so, by Theorem 5, there is a pure event structure E satisfying the corresponding properties for event structures such that L(E) = C. Now E_{f} also satisfies these properties, and F(L(E_{f})) = F(L(E)) = F(C) = C. In the case of a package of properties which does include finite binary conflict, by Lemma 3 and Corollary 13, C^{b} has the same package of properties but with binary conflict instead of finite binary conflict. Thus, by Theorem 5, there is a pure event structure E with the corresponding properties such that L(E) = C^{b}. Now E_{f} is pure and also satisfies these properties, and F(L(E_{f})) = F(L(E)) = F(C^{b}) = C. □

Comparisons via finite reachable parts

We now turn to comparisons via finite reachable parts. A similar obstacle as in Section 5.3 presents itself: an event structure E may have binary conflict even though R_{f}(E) does not have finite binary conflict.

Example 21 Let C be the configuration structure with events {a_{0}, …, a_{4}} and with configurations:

∅, {a_{i}}, {a_{i}, a_{i+1}}, {a_{i}, a_{i+1}, a_{i+2}}

and {a_{0}, …, a_{4}}

where the counting is done mod 5. Then C is finitary and has (finite) binary conflict, but its reachable part has not, as {a_{0}, …, a_{4}} is not reachable. Furthermore, C can be given by a pure rooted event structure with finite causes and binary conflict, namely the one with the enablings

∅ ⊢ a_{i}, ∅ ⊢ a_{i}, a_{i+1} and a_{i+1} ⊢ a_{i}, a_{i+2}

again counting mod 5 (and omitting explicit set parentheses), plus those needed for rootedness and binary conflict.

Since our primary interest is in characterising natural properties of event structures we find a suitable weakening of this property of configuration structures, and proceed analogously to Section 5.3.

Definition 5.9 A configuration structure C has finite reachable binary conflict iff C = R(F(C^{b})).

In other words, a configuration structure C = ^{/}_{\}E, C^{\}_{/} has finite reachable binary conflict iff X ∈ C exactly when X can be written as {e_{1}, …, e_{n}} so that for every j ≤ n and Y ⊆ {e_{1}, …, e_{j}} with |Y | ≤ 2 there is a configuration z ∈ C such that Y ⊆ z ⊆ {e_{1}, …, e_{j}}.

We then obtain the correspondences summarised by Table 5.

Event  Configuration Propositional
structures  structures  theories
rooted  rooted  (nef, any)
singular  closed under \overline{∪}_{f} (1, any), (fin., 0)
conjunctive  closed under ∩ (fin., ≤1)
locally conj.  closed under \overline{∩} (fin., ddfc)
binary conflict fin. reach. b.c. (≤2, any)
sing. & bin. con. closed under \overline{∪}_{f}^{2} (1, any), (≤2, 0)
loc. conj. & b.c. closed under \overline{∩}^{2} (≤2, bddfc)

Table 5: Corresponding properties for finite reachable parts Lemma 4 Let E be a pure event structure with the properties given in one of the rows of Table 5. Then R_{f}(E) has the corresponding property, as given in the table.

Proof: The event structure E_{f} has the same properties as E and in addition has finite conflict. Clearly R_{f}(E) = R_{f}(E_{f}), and by Proposition 3.11 we have R_{f}(E_{f}) = F(S(E_{f})). By Lemma 1 S(E_{f}) ⊆ L(E_{f}). Hence, by Theorem 8, S(E_{f}) has the corresponding property given in Table 3. In case the row we started with was not that of binary conflict, by Observations 5.2 and 5.1 F(S(E_{f})) has the corresponding property of Table 5. In case the row we started with was that of binary conflict, by expanding Definition 5.6 we find that S(E_{f}) = S(S(E_{f})^{b}). Now observe that F(C^{b}) = F(F(C)^{b}) for any configuration structure C. Applying Propositions 3.11 and 3.2 this yields

\begin{matrix}F(S(E_{f})) = & F(S(S(E_{f})^{b})) \\ = & F(R(S(E_{f})^{b})) \\ = & R(F(S(E_{f})^{b})) \\ = & R(F(F(S(E_{f}))^{b})) . \end{matrix}

Hence R_{f}(E) = F(S(E_{f})) has finite reachable binary conflict. □

Note that the purity requirement in Lemma 4 can be weakened to reachable purity, and is only needed for the binary conflict row, namely in the application of Theorem 8. The following example shows that this requirement cannot be omitted.

Example 22 Let E = ^{/}_{\}E, ⊢^{\}_{/} be the event structure with E := {a_{1}, a_{2}, a_{3}} and the enablings ∅ ⊢ X when |X| ≠ 2, as well as

a_{i} ⊢ a_{i}, a_{i+1}

where the counting is done mod 3. Then E has binary conflict, L(E) = 𝒫(E) and R_{f}(E) = 𝒫(E) − {E}. Hence R_{f}(E) does not have finite reachable binary conflict.

We can now establish the correspondences of Table 5. We define packages of properties of configuration structures from the table just as we did for finitary equivalence, substituting finite reachable binary conflict for finite binary conflict; and we keep the same form lattices and their interpretation as just used for finitary equivalence.

Theorem 11

1. Let E be a (pure) event structure satisfying any collection of properties from Table 5. Then there is a (pure) propositional theory T whose axioms have forms which are combinations of the forms corresponding to the event structure properties such that R(F(M(T))) = R(F(L(E))).

2. Let T be a propositional theory whose axioms have forms which are combinations of forms from a given collection of rows of Table 5. Then R(F(M(T))) has the corresponding collection of properties of configuration structures.

3. Let C be a finitary connected configuration structure satisfying a given package of properties from Table 5. Then there is a pure event structure E with finite causes and finite conflict such that R_{f}(E) = C and with the corresponding collection of properties of event structures.

Proof:

1. This is immediate from part 1 of Theorem 10.

2. Let T be such a theory. It follows from Theorem 10 that there is a pure event structure E satisfying the corresponding properties from the table such that F(L(E)) = F(M(T)). The conclusion then follows from Lemma 4 and Proposition 3.12.

3. This follows just as in the proof of Theorem 10: Let C be a finitary connected configuration structure with a given package of properties of the table, not including finite reachable binary conflict. Then, by Observation 5.1, C satisfies the corresponding package of properties of Table 2, and so, by Theorem 5, there is a pure event structure E satisfying the corresponding properties for event structures such that L(E) = C. Now E_{f} is pure and also satisfies these properties, so Proposition 3.12 yields R_{f}(E_{f}) = R(F(L(E_{f}))) = R(F(L(E))) = R(F(C)) = C.

In the case of a package of properties which does include finite reachable binary conflict, by Lemma 3 and Corollary 13, C^{b} has the same package of properties but with binary conflict instead of finite reachable binary conflict. Thus, by Theorem 5, there is a pure event structure E with the corresponding properties such that L(E) = C^{b}. Now E_{f} also satisfies these properties, and R_{f}(E_{f}) = R(F(L(E_{f}))) = R(F(L(E))) = R(F(C^{b})) = C. □

We now apply the results of this section to characterise the finitary configuration structures associated to the various event structures of Winskel [34, 35].

Corollary 19 A configuration structure arises as the family of finite left-closed configurations of an event structure of [34] iff it is finitary, rooted and closed under \overline{∪}. It arises as the family of finite left-closed configurations of a stable event structure of [34] iff it moreover is closed under \overline{∩}.

A configuration structure arises as the family of finite left-closed configurations of an event structure of [35] iff it is finitary, rooted and closed under \overline{∪}^{2}. It arises as the family of finite left-closed configurations of a stable event structure of [35] iff it moreover is closed under \overline{∩}. □

The four classes of configuration structures mentioned in the above corollary arise as the finite models of propositional theories whose axioms have the forms

(1, any), (nef, 0) (1, ddfc), (nef, 0) (1, any), (2, 0) (1, bddfc), (2, 0),

respectively.

When dealing with finite reachable configurations, the same characterisations as in Corollary 19 are obtained, but now the resulting configuration structures are additionally connected.

Proposition 5.9 Let C be a finitary configuration structure closed under \overline{⋃}. Then C is connected iff it is coincidence-free.

Proof: Similar to the proof of Proposition 5.8. □

Corollary 20 A configuration structure arises as the family of finite reachable configurations of an event structure of [34] iff it is finitary, rooted, coincidencefree and closed under \overline{∪}. It arises as the family of finite reachable configurations of a stable event structure of [34] iff it moreover is closed under \overline{∩}.

A configuration structure arises as the family of finite reachable configurations of an event structure of [35] iff it is finitary, rooted, coincidence-free and closed under \overline{∪}^{2}. It arises as the family of finite reachable configurations of a stable event structure of [35] iff it moreover is closed under \overline{∩}. □

The first class of configuration structures in this corollary was the class of configuration structures originally considered in [11].

We have no characterisation of the finitary configuration structures associated to the event structures from [25]; in particular, the property of Lirredundancy appears hard to express in terms of finite configurations. As for the prime event structures from [34, 35], recall that their finite left-closed configurations are the same as their finite reachable or finite secured configurations.

Corollary 21 A configuration structure arises as the family of finite configurations of a prime event structure of [34] iff it is finitary, rooted, coincidence-free, irredundant and closed under \overline{∪} and ∩.

A configuration structure arises as the family of finite configurations of a prime event structure of [35] iff it is finitary, coherent, coincidence-free, irredundant and closed under ∩. □

The two classes of configuration structures mentioned above arise as the finite reachable models of propositional theories whose axioms have the forms

{(1, 1), (nef, 0) \atop (1, 1), (2, 0)}

respectively. We do not have axiomatic characterisations of connectedness or coincidence-freedom; that lack is circumvented in the above characterisations by talking about reachable models.

5.5 Tying-in Petri nets

The third columns of Tables 2, 4, 5 also provide characterisations of classes of Petri nets corresponding to various combinations of properties of event structures or configuration structures. The pure 1-occurrence nets correspond up to finite configuration equivalence to event and configuration structures that are rooted and with finite conflict. We do not have a structural characterisation of the subclass of those pure 1-occurrence nets corresponding to locally conjunctive event structures. However, for each combination of the properties singular, conjunctive, and binary conflict, the forms (L, R) that characterise the associated propositional theory also provide a structural characterisation of the associated subclass of pure 1-occurrence nets. Here L restricts the cardinality of the set of posttransitions of any given place, and R restricts the cardinality of its set of pretransitions; we say that the place has the form (L, R). For example, rooted singular pure event structures correspond to the pure 1-occurrence nets each of whose places have either no pretransitions or exactly one posttransition. The proof of the correspondences goes via the characterisations of the associated propositional theories.

Theorem 12 Let T be a (pure) rooted propositional theory in conjunctive normal form, whose clauses are combinations of the forms found in lines 2, 3 and 5 of Table 2. Then N (T) is a (pure) 1-occurrence net whose places have the corresponding combinations of forms, as well as (nef, any).

Similarly, if N is a (pure) 1-occurrence net whose places have combinations of the forms found in lines 2, 3 and 5 of Table 2, then T (N), as defined at the end of Section 1.4, is a (pure) rooted propositional theory axiomatised by clauses obeying these forms, as well as (nef, any).

Proof: The first statement follows immediately from the construction in Definition 1.17. For the second statement, recall that T (N) consists of the formulae ⋀ Y ⇒ ⋁_{X∈^{^{•}Y (s)-I(s)}s} ⋀ X for s ∈ S and Y ⊆_{fin} s^{•}. When converting such formulae to conjunctive normal form, one obtains clauses Y ⇒ Z with Y ⊆_{fin} s^{•} for some place s. As remarked at the end of Section 1.4, one can omit any clauses for Y = ∅, or more generally for which ^{•}Y (s)−I(s) ≤ 0, as then ∅ ∈^{^{•}Y (s)−I(s)}s. Hence all clauses obey the restriction (nef, any) and T (N) is rooted. By construction, T (N) is pure when N is. If s has the form (1, any) or (≤2, any), then so do the associated clauses. Furthermore, if s has no pretransitions, then the associated clauses have the form Y ⇒ ∅, and if s has one pretransition t, then the associated clauses have the form Y ⇒ ∅ for Y ⊆_{fin} s^{•} with ^{•}Y (s) − I(s) > t^{•}(s), and Y ⇒ t for Y ⊆_{fin} s^{•} with 1 ≤ ^{•}Y (s) − I(s) ≤ t^{•}(s). Thus, if s has the form (any, 0) or (any, ≤1), then so do the associated clauses. □

This theorem also holds when using the third columns of Tables 4 or 5 (which are the same) instead of the one of Table 2. For these columns are obtained by additionally imposing the condition (finite, any), a condition that is implied by (nef, any). Furthermore, the theorem remains true if any place s with n incoming arcs and k initial tokens is deemed to additionally have the form “(≤ k+n, ≤ n) or (k+n+1, 0)”. Namely if Y ⊆_{fin} s^{•} and |Y | > k + n then the transitions in Y cannot all happen, so we obtain the clause ⋀ Y ⇒ ∅. Among such clauses one only needs to retain the ones with |Y | minimal, that is, with |Y | = k + n + 1. Finally, places without posttransitions may be ignored. Thus, for example, pure 1-occurrence nets whose places either have ≤1 posttransition, or one incoming arc and no initial tokens, or no incoming arcs and ≤1 initial token correspond to pure singular event structures with binary conflict.

This theorem, together with Theorem 3 and Proposition 1.4, yields a bijection up to finitary equivalence between the stated subclasses of pure rooted propositional theories and the corresponding subclasses of pure 1-occurrence nets. As the nets are pure, these bijections also hold up to finitary reachable equivalence.

6 Related Work

The notion of a configuration structure as a model of concurrency in its own right stems from Winskel [33]; our configuration structures are obtained by dropping the requirements imposed in [33]: coherence, stability, coincidence-freeness and the axiom of finiteness. The term configuration structures stems from [11]; their configuration structures obeyed the requirements of finitariness, rootedness, coincidence-freeness and closure under \overline{∪}, that together ensured that these structures were exactly the families of finite configurations of Winskel’s event structures [34]. Two further partial generalisations of this model were previously proposed by Pinna & Poigné [26] and Hoogers, Kleijn & Thiagarajan [20]. The event automata of [26] are rooted finitary configuration structures together with a transition relation between the configurations; each transition extends a configuration with exactly one event. The local event structures of [20] are rooted, finitary, connected configuration structures together with a step transition relation → between the configurations that satisfies

• X → X,

• X → Y implies X ⊆ Y, and

• X → Z and X ⊆ Y ⊆ Z implies X → Y → Z.

In [20] X → Y is denoted X ⊢ (Y − X), so that their notation X ⊢ Y implies X ∩ Y = ∅ and translates to X → X ∪ Y.

Our configuration structures are, up to isomorphism, the extensional Chu spaces of Gupta & Pratt [18, 17, 29]. It was in their work that the idea arose of using the full generality of such structures in modelling concurrency. Also the propositional representation of configuration structures stems from [18, 29]. It should be noted however that the computational interpretation in [18, 17, 29] differs somewhat from that in [34, 11, 26, 20] and the current work. In particular, in [18, 17, 29] unreachable configurations may be semantically relevant, as witnessed by the notions of causality and internal choice in [18, 29] and that of history preserving bisimulation in [17].

Gunawardena proposes causal automata in [16] and geometric automata in [15]. The first are given by a set of events with, for each event e, a boolean expression ρ(e) over the set of events. Each event occurrence in ρ(e) is interpreted as the proposition that it happened, and e is enabled when ρ(e) evaluates to true. In geometric automata, a more complicated infinitary logic is used, and the boolean expression is replaced by two positive logical expressions, one of which must evaluate to true, and the other to false, in order for the associated event to be enabled. Both models can be interpreted in a natural way in terms of event automata; plain configuration structures are not sufficient here.

Our event structures are directly inspired by, and generalise, the ones of Winskel [25, 34, 35]. Many other variants of these event structures have been proposed in the literature.

A bundle event structure, as studied in Langerak [22], is given as a tuple (E, #, ↦, l) with E a set of events, # an irreflexive, symmetric conflict relation, ↦ ⊆ 𝒫(E) × E, the bundle relation, and l : E → Act a labelling function, labelling events with actions from a given alphabet Act. When X ↦ e, the events in X should be pairwise in conflict; in this case e can happen only if one of the events in X occurred earlier. Ignoring the labelling function, a bundle event structure can in our framework best be understood as a propositional theory, namely one whose formulae have the forms (2, 0) and (1, dds). Here “dds” stands for disjoint disjunction of singletons; in the right form lattice of Figure 4 it can be positioned right below “bddc”, or right below “bddfc” of Section 5.4. The configurations used in [22] are in our terminology finite reachable configurations. Using the translations of Section 5, preserving finitary reachable equivalence, the bundle event structures map to a subclass of rooted, singular, locally conjunctive event structures with binary conflict, and hence to a subclass of stable event structures as defined in [35] that contains the class of prime event structures of [35].

Langerak’s notion of an extended bundle event structure on the other hand does not correspond to an event structure as in [34, 35]. Here the symmetric binary conflict relation # is replaced by an asymmetric counterpart ⇝, a relation that was considered independently in [26], writing e ⇝̸ d for d ⇝ e. When d ⇝ e, the event e can happen either initially or after d; however, as soon as e happens, d is blocked. When both d and e happen, d causally precedes e. Asymmetric conflict d ⇝ e can be translated into our framework as {d} ⊢ {d, e}, where it is important that {d} is the only set of events enabling {d, e}. The absence of both d ⇝ e and e ⇝ d translates to ∅ ⊢ {d, e}, and the conjunction of d ⇝ e and e ⇝ d is simply d#e and translates to the absence of any X with X ⊢ {d, e}. Under this translation, the configurations of extended bundle event structures defined in [22] are exactly our finite reachable configurations of Definition 3.5. Thus, the class of extended bundle event structures can be regarded as a subclass of our rooted, locally conjunctive event structures with binary conflict. However, they are not pure, and cannot be faithfully represented by configuration structures as studied in this paper. The relationship between event structures with asymmetric conflict, Petri nets, and domains, is studied in [1].

A dual event structure, as studied in Katoen [21], is like an extended bundle event structure, but without the requirement that when X ↦ e the events in X should be pairwise in conflict. This amounts to generalising the formulae of the form (1, dds) to (1, any). They correspond to a subclass of our rooted event structures with binary conflict. The same can be said for the extended dual event structures of [21]. Here the new feature is the irreflexive and symmetric interleaving relation ⇀ ↽, modelling mutual exclusion of events, i.e., disallowing them to overlap in time. As for the event structure M in Section 2.3, d ⇀ ↽ e can in our framework be modelled as {d} ⊢ {d, e} {e} ⊢ {d, e}.

As remarked in the introduction, behaviour preserving translations from safe Petri nets to a class of event structures, and from there to configuration structures, are defined in [25]. In Section 4.6 we saw that the event structures of [25] can be seen as a subclass of our event structures, in the sense that there are translations back and forth that respect the identify of events and the sets of associated configurations. The translation in [25] from safe nets to event structures proceeds in two steps: an unfolding turns every safe net into an occurrence net—a particular kind of pure safe 1-occurrence net—and a mapping ξ takes occurrence nets to event structures. The transitions of an occurrence net N become the events of the event structure ξ(N), and the finite configurations of N, as defined in this paper, equal the finite configurations of ξ(N) as defined in [25]. This follows directly from the definitions. Hence the translation ξ preserves finitary configuration equivalence. It is not hard to check that the unfolding of a safe 1-occurrence net preserves finitary configuration equivalence as well. Thus, restricted to safe 1occurrence nets, the translations of [25] are entirely in agreement with ours.

This agreement extends to pure safe nets that are not 1-occurrence nets. However, this cannot be stated in the terminology of this paper, for the unfolding may make multiple copies of a single transition, namely one for every possible way in which it can be fired. Since the identify of events is thereby not preserved, this unfolding does not respect the equivalences of this paper.

Define a 1-reachable-occurrence net to be a net in which every reachable configuration is a set. This notion is a slight generalisation of a 1-occurrence net. When working up to reachable equivalence, all our work generalises without change from 1-occurrence nets to 1-reachable-occurrence nets. Similarly, define a 1-reachable-occurrence net N to be semantically pure if there exists a pure net N̂ with the same places and transitions, and possibly less arcs and less initial tokens, that has the same reachable configurations and the same step transition relation between those configurations. When working up to reachable equivalence, also preserving the transitions between reachable configurations, our connections between pure 1-reachable-occurrence nets and pure event structures evidently generalise to semantically pure 1-reachable-occurrence nets—just as they did to reachably pure event structures.

Boudol [4] provides translations between a class of 1-reachable-occurrence nets, the flow nets, and a class of flow event structures that have expressive power strictly between the bundle event structures of [22] and the stable event structures of [35]. His correspondence extends the correspondence due to [25] between occurrence nets and prime event structures with binary conflict. Flow nets are defined to have the property that transitions that can occur in the same firing sequence do not share a preplace. This implies that the reachable configurations of a flow net N, as well as the transition relation ⟶_{N} between them, are unaffected by omitting the arcs from a transition e to a place s for which there also is an arc from s to e. Any flow net can thereby be transformed, in a behaviour preserving way, into a pure 1-reachable-occurrence net. Hence flow nets are semantically pure.

As Boudol’s translations preserve the notions of event (= transition) and finite reachable configuration, they are consistent with our approach. Our translations can thus be regarded as an extension of the work of [4] to a more general class of Petri nets and event structures.

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

Future research

As we have seen, both event structures and Petri nets have naturally associated transition relations. In the pure case these transition relations can be derived from their associated sets of configurations, but this fails more generally. A natural line of future work is therefore to go beyond the pure case, looking for a suitable notion of configuration structure equipped with a transition relation and, perhaps, a suitable notion of propositional theory.

We would also like to connect our models with appropriate versions of higher dimensional automata [28]. An embedding up to finitary reachable equivalence of rooted configuration structures as well as Petri nets into a form of higher dimensional automata called cubical sets is proposed in [10]. Another form of higher dimensional automata called labelled step transition systems is considered in [9].

After the initial work of [25] it was natural to ask whether their unfolding could be seen as a universal construction. This led to a development of categories of event structures, nets and related models, and, in turn, to a general process algebra whose constructions were natural categorically: see [34, 37, 31]. In our case it would be natural to look for categories of configuration structures and the other models of this paper, so that, for example, the connections developed in Section 1 became functorial. The recent work of [36, 19] on adding symmetry to structures may prove helpful here. Proposals for a category of configuration structures can be found in [29] and [5].

In a different direction, the equivalences considered in this paper are quite fine and it would be interesting to look at coarser ones, say along the lines of history preserving bisimulation. In that connection, and also the categorical one, it may be useful to consider configuration structures, and other models, equipped with event labellings.

Acknowledgement We thank the referees for their helpful comments.

References

[1] P. Baldan, A. Corradini & U. Montanari (2001): Contextual Petri nets, asymmetric event structures and processes. Information and Computation 171(1), pp. 1–49.

[2] E. Best & R. Devillers (1987): Sequential and Concurrent Behaviour in Petri Net Theory. Theoretical Computer Science 55, pp. 87–136.

[3] E. Best, R. Devillers, A. Kiehn & L. Pomello (1991): Concurrent bisimulations in Petri nets. Acta Informatica 28, pp. 231–264.

[4] 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, Springer, pp. 62–95.

[5] R. Bruni, J. Meseguer, U. Montanari & V. Sassone (1998): A comparison of Petri net semantics under the collective token philosophy. In J. Hsiang & A. Ohori, editors: Proceedings 4^{th} Asian Computing Science Conference Advances in Computing Science, ASIAN’98, Manila, The Philippines, LNCS 1538, Springer, pp. 225–244.

[6] J. Engelfriet (1991): Branching processes of petri nets. Acta Informatica 28(6), pp. 575–591.

[7] D.M. Gabbay (1981): Semantic Investigations in Heyting’s Intuitionistic Logic, Synthese Library 148. D. Reidel.

[8] R.J. van Glabbeek (1995): History preserving process graphs. Draft available at http://theory.

stanford.edu/^{∼}rvg/abstracts.html#hppg.

[9] R.J. van Glabbeek (2005): The Individual and Collective Token Interpretations of Petri Nets. In M. Abadi & L. de Alfaro, editors: Proceedings 16^{th} International Conference on Concurrency Theory, CON-CUR’05, San Francisco, USA, LNCS 3653, Springer, pp. 323-337.

[10] R.J. van Glabbeek (2006): On the Expressiveness of Higher Dimensional Automata. Theoretical Computer Science 368(1-2), pp. 169-194.

[11] R.J. van Glabbeek & U. Goltz (1990): Refinement of actions in causality based models. In J.W. de Bakker, W.P. de Roever & G. Rozenberg, editors: Proceedings REX Workshop on Stepwise Refinement of Distributed Systems: Models, Formalism, Correctness, Mook, The Netherlands 1989, LNCS 430, Springer, pp. 267–300.

[12] R.J. van Glabbeek & G.D. Plotkin (1995): Configuration structures (extended abstract). In D. Kozen, editor: Proceedings 10^{th} Annual IEEE Symposium on Logic in Computer Science, LICS’95, San Diego, USA, IEEE Computer Society Press, pp. 199–209.

[13] R.J. van Glabbeek & G.D. Plotkin (2004): Event structures for resolvable conflict. In: V. Koubek & J. Kratochvil, editors, Proceedings 29^{th} International Symposium on Mathematical Foundations of Computer Science, MFCS’04, Prague, Czech Republic, LNCS 3153, Springer, pp. 550-561.

[14] U. Goltz & W. Reisig (1983): The non-sequential behaviour of Petri nets. Information and Computation 57, pp. 125–147.

[15] J. Gunawardena (1991): Geometric Logic, Causality and Event Structures. In J.C.M. Baeten & J.F. Groote, editors: Proceedings 2^{nd} International Conference on Concurrency Theory, CONCUR’91, Amsterdam, The Netherlands, LNCS 527, Springer, pp. 266-280.

[16] J. Gunawardena (1992): Causal automata. Theoretical Computer Science 101(2), pp. 265–288.

[17] V. Gupta (1994): Chu Spaces: A Model of Concurrency. PhD thesis, Stanford University. Available at

http://boole.stanford.edu/pub/gupthes.ps.gz.

[18] V. Gupta & V.R. Pratt (1993): Gates accept concurrent behavior. In Proceedings 34^{th} Annual Symposium on Foundations of Computer Science, FOCS’93, Palo Alto, USA, IEEE Computer Society Press, pp. 62–71.

[19] J. Hayman & G. Winskel (2008): The unfolding of general Petri nets. In: R. Hariharan, M. Mukund & V. Vinay, editors: Proceedings IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science, Bangalore, In-

dia 2008. Available at http://drops.dagstuhl.de/
opus/volltexte/2008/1755/.

[20] P.W. Hoogers, H.C.M. Kleijn & P.S. Thiagarajan (1996): An event structure semantics for general Petri nets. Theoretical Computer Science 153, pp. 129–170.

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

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

[23] K.G. Larsen & G. Winskel (1991): Using information systems to solve recursive domain equations. Information and Computation 91(2), pp. 232–258.

[24] J. Meseguer, U. Montanari & V. Sassone (1992): On the semantics of Petri nets. In W.R. Cleaveland, editor: Proceedings Third International Conference on Concurrency Theory, CONCUR’92, Stony Brook, NY, USA, LNCS 630, Springer, pp. 286–301.

[25] M. Nielsen, G.D. Plotkin & G. Winskel (1981): Petri nets, event structures and domains, part I. Theoretical Computer Science 13(1), pp. 85–108.

[26] G.M. Pinna & A. Poigné (1995): On the nature of events: another perspective in concurrency. Theoretical Computer Science 138(2), pp. 425–454.

[27] G.D. Plotkin (1978): 𝕋^{ω} as a universal domain. J. Comput. Syst. Sci. 17(2), pp. 209–236.

[28] V.R. Pratt (1991): Modeling concurrency with geometry. In Conference Record of the 18^{th} Annual ACM Symposium on Principles of Programming Languages, POPL’91, Orlando, USA, pp. 311–322.

[29] V.R. Pratt (1994): Chu spaces: complementarity and uncertainty in rational mechanics. Course Notes, TEMPUS Summer School, Budapest. Available at

                                                       http://boole.stanford.edu/pub/bud.pdf.

[30] W. Reisig (1985): Petri Nets: An Introduction. Springer.

[31] V. Sassone, M. Nielsen & G. Winskel (1996): Models for concurrency: Towards a classification. Theoretical Computer Science 170, pp. 297-348.

[32] D.S. Scott (1974): Completeness and axiomatizability in many-valued logic. In L. Henkin et al., editors: Proceedings Tarski Symposium, AMS, pp. 411–435.

[33] G. Winskel (1982): Event structure semantics for CCS and related languages. In M. Nielsen and E.M. Schmidt, editors: Proceedings 9^{th} Colloquium on Automata, Languages and Programming, ICALP’82, Aarhus, Denmark, 1982, LNCS 140, Springer, pp. 561-576.

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

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

[36] G. Winskel (2008): Events, Causality and Symmetry. In: E. Gelenbe, S. Abramsky and V. Sassone, editors: Proceedings BCS International Academic Conference Visions in Computer Science, London, UK 2008. Electronic Workshops in Comput-

                                                       ing. Available at http://www.bcs.org/server.php?
                                                       show=ConWebDoc.22872.

[37] G. Winskel & M. Nielsen (1995): Models for Concurrency. In: Handbook of Logic in Computer Science, volume 4, Oxford University Press, pp. 1-148.

Index

L-equivalent, 4 L-irredundant, 19 R_{f}-irredundancy, 25 S-irredundant, 19, 29 SR-secure, 14–16 1-occurrence net, 5 1-occurrence places, 7 1-reachable-occurrence net, 43 1-unfolding, 8

antecedents, 3 arcs, 4 arcweights, 4 associated configuration structure, 5 associated multiset transition system, 12 associated set system, 3 asymmetric conflict, 3, 42 asynchronous, 10 asynchronous interpretation, 9 axiom of finiteness, 35 axiomatises, 3

binary conflict, 19, 23, 26 bounded nonempty intersections, 26 bounded unions, 26 bundle event structure, 42 bundle relation, 42

causal automata, 42 causality, 12, 14, 42 causality relation, 19, 23, 24 Chu spaces, 12, 42 clause, 3 closure under binary conflict, 33 closure under finite conflict, 33 coincidence-free, 30 coherent, 27 collective token interpretation, 5 coloured Petri nets, 5 completeness, 25 configuration equivalence, 2, 5, 13 configuration structures, 1, 2 configurations, 2

of a Petri net, 5 conflict relation, 19, 23, 24 conflict-free, 23, 24 conjunctive, 19 conjunctive normal form, 3 connected, 13 consequents, 3 consistency predicate, 22, 23 consistent, 19, 22, 24, 26 consistently complete, 26 cubical sets, 44 cycle-free, 19

direct causality relation, 19 directed unions, 21, 27 disjoint disjunction, 30 disjoint disjunction of clauses, 30 disjoint disjunction of singletons, 42 disjunctive causality, 7 disjunctive normal form, 3 dual event structure, 43

enabled, 5

enabling relation, 3, 22, 23

event automata, 42

event structure associated to, 4, 8

event structures, 1, 3 events, 2, 3, 5, 22–24 eventwise securing, 16 extended bundle event structure, 42 extended dual event structures, 43

families of configurations of event structures, 1, 22 finitary, 6, 13 finitary asynchronous interpretation, 9, 12 finitary equivalence, 6, 13 finitary reachable equivalence, 13, 18 finite, 5 finite binary conflict, 37 finite causes, 19 finite conflict, 19, 26 finite part, 13 finite reachable binary conflict, 39 finitely compatible nonempty intersections, 27 finitely compatible unions, 27 finitely complete, 27 finitely consistent, 26 finitely consistent nonempty intersections, 26 finitely consistent unions, 26 finitely disjoint disjunction of clauses, 30 fire, 5 firing sequence, 5 flow nets, 43 flow relation, 4 forms, 30 formulae over E, 3 fully concurrent bisimulation, 6, 9

geometric automata, 42

Gupta-Pratt interpretation, 12

history preserving bisimulation, 9, 14, 42 Horn clauses, 32 hyperconnected, 14, 15 hyperreachable, 14 hyperreachable binary conflict, 33 hyperreachable finite conflict, 33

implies, 3 individual token interpretation, 5 initial marking, 4 interleaving relation, 43 internal choice, 14, 42 interpretation, 3 irredundant, 29

labelled nets, 6 labelled step transition systems, 44 labelling function, 6 laws of C, 2 left-closed, 24 left-closed configuration structure associated to, 4 left-closed configurations, 3 local event structures, 42 locally conjunctive, 19 logical consequence, 3 logically equivalent, 3

manifestly conjunctive, 20 marking, 4 models, 2, 3 multiset transition system, 12

nonempty intersections, 26

occurrence net, 1, 43

package, 28 pairwise compatible nonempty intersections, 27 pairwise compatible unions, 27 pairwise consistent, 26 pairwise consistent nonempty intersections, 26 pairwise consistent unions, 26 Petri nets, 1, 4 Petri nets with individual tokens, 5 places, 4 postplaces, 5 posttransitions, 8 predicate/transition nets, 5 preplaces, 5 pretransitions, 8 prime algebraic coherent Scott domains, 1 prime event structures with binary conflict, 1 principle of conflict heredity, 24 principle of finite causes, 24 process, 6 propositional theories, 2, 3 propositional theory associated to, 3, 8 propositions, 2 pure, 1, 4, 5, 30 pure configuration structure, 2

reachable configurations, 13, 16 reachable equivalence, 13, 18 reachable marking, 5 reachable part, 13 reachably pure, 18 resolvable conflict, 3, 6 rooted, 6

safe, 1, 6

Scott clauses, 32 Scott domains, 1 secure, 19, 36 secured, 22, 23 secured configuration structure associated to, 16 secured configurations, 2, 14, 16 self-loops, 5 self-sequential interpretation of Petri nets, 9 semantically pure, 43 set systems, 2 single-action transition relation, 10 singular, 19 stable, 22, 23 step transition relation, 4, 10, 11 stepwise securing, 16

ternary conflict, 3

tokens, 4

transition equivalent, 12 transition systems, 2 transitions, 4

unfolding, 6, 43

valid, 3

weakly coherent, 27