
## 2.1 Events, Event Occurrences And Observations

Everything is either an event, event occurrence or *observation*:
(∀x) (event(x)∨event occurrence(x)∨observation(x)) (2.1)
The sets of events, event occurrences and observations are pair-wise disjoint.

(∀x)
¬(event(x)∧event occurrence(x))∧ ¬(event(x)∧observation(x))
∧¬(event occurrence(x)∧observation(x)) (2.2)
The *occurrence* relation only holds between events and event occurrences.

(∀e,o) (occurrence(o,e) ⊃ event(e)∧event occurrence(o)) (2.3)
Every event occurrence is an occurrence of some event.

(∀o) (event occurrence(o) ⊃ (∃e) (event(e)∧occurrence(o,e))) (2.4)
Every event occurrence is an occurrence of a unique event.

(∀o1,e1,e2) (occurrence(o1,e1)∧occurrence(o1,e2) ⊃ e1 = e2) (2.5)

## 2.2 Gso-Structure And Its Relations

We now axiomatize the gso-structure, which describes the *specification level* of a concurrent system. The relations of gso-structure are earlier than, not later than and nonsimultaneous. The relation earlier than can be defined as the intersection of the latter two, yet is added because it helps to make our axioms shorter and more intuitive.

We have to make sure that the field of the relations earlier than, not later than and nonsimultaneous consists of only event occurrences.

(∀o1,o2)
earlier than(o1,o2) ⊃ (occurrence(o1)∧occurrence(o2)) (2.6)
(∀o1,o2)
not later than(o1,o2) ⊃ (occurrence(o1)∧occurrence(o2)) (2.7)
(∀o1,o2)
nonsimultaneous(o1,o2) ⊃ (occurrence(o1)∧occurrence(o2)) (2.8)
The relation nonsimultaneous is irreflexive and symmetric.

(∀o1)(¬nonsimultaneous(o1,o1)) (2.9)
(∀o1,o2)(nonsimultaneous(o1,o2) ⊃ nonsimultaneous(o2,o1)) (2.10)
The earlier than relation is the intersection of the not later than and the nonsimultaneous relations.

$$\tau o_{1},o_{2})\left[\begin{array}{c}{{0}}\\ {{0}}\end{array}\right]$$
(∀o1,o2)
$$(2.11)$$
Later_than($o_{1},o_{2}$) $\Lambda$ nonsimultaneous($o_{1},o_{2}$))  $\equiv$ earlier_than($o_{1},o_{2}$)