=Paper=
{{Paper
|id=None
|storemode=property
|title=Causal Structures for General Concurrent Behaviours
|pdfUrl=https://ceur-ws.org/Vol-1032/paper-17.pdf
|volume=Vol-1032
|dblpUrl=https://dblp.org/rec/conf/csp/JanickiKKM13
}}
==Causal Structures for General Concurrent Behaviours==
https://ceur-ws.org/Vol-1032/paper-17.pdf
Causal Structures for General Concurrent
Behaviours
Ryszard Janicki1 , Jetty Kleijn2 , Maciej Koutny3 , and Łukasz Mikulski3,4
1
McMaster University, Canada
2
LIACS, Leiden University, The Netherlands
3
Newcastle University, U.K.
4
Nicolaus Copernicus University, Poland
Abstract. Non-interleaving semantics of concurrent systems is often
expressed using posets, where causally related events are ordered and
concurrent events are unordered. Each causal poset describes a unique
concurrent history, i.e., a set of executions, expressed as sequences or
step sequences, that are consistent with it. Moreover, a poset captures
all precedence-based invariant relationships between the events in the
executions belonging to its concurrent history. However, concurrent his-
tories in general may be too intricate to be described solely in terms
of causal posets. In this paper, we introduce and investigate generalised
mutex order structures which can capture the invariant causal relation-
ships in any concurrent history consisting of step sequence executions.
Each such structure comprises two relations, viz. interleaving/mutex and
weak causality. As our main result we prove that each generalised mutex
order structure is the intersection of the step sequence executions which
are consistent with it.
Keywords: concurrent history, causal poset, weak causal order, mutex
relation, interleaving, step sequence, causality semantics.
1 Introduction
In order to design and validate complex concurrent systems, it is essential to
understand the fundamental relationships between events occurring in their ex-
ecutions. However, looking at sequential descriptions of executions in the form
of sequences or step sequences is insufficient when it comes to providing faith-
ful information about causality and independence between events. To address
this drawback, one may resort to using partially ordered sets of events provid-
ing explicit representation of causality in the executions of a concurrent system.
In particular, the order in which independent events are observed may be ac-
cidental and those executions which only differ in the order of occurrences of
independent events may be regarded as belonging to the same concurrent his-
tory, underpinned by a causal poset [1, 13, 16, 17, 21].
In general, concurrent behaviours can be investigated at the level of individual
executions as well as at the level of order structures, like causal posets, capturing
the essential invariant dependencies between events. The key link between these
194 R. Janicki, J. Kleijn, M. Koutny, Ł. Mikulski
(a) (b) (c)
a b a b a b
c d c d c d
Fig. 1. A safe Petri net (a), extended with an inhibitor arc implying that when c is
executed the output place of d must be empty (b), and extended with a mutex arc
implying that c and d cannot be executed simultaneously (c).
two levels is the notion of a concurrent history [6], an invariant closed set ∆ of
executions. The latter means that ∆ is fully determined by invariant relationships
over X, its set of events: causality (e ≺∆ f if, in all executions of ∆, e precedes
f ); weak causality (e @∆ f if, in all executions of ∆, e either precedes or is
simultaneous with f ); and interleaving/mutex (e ∆ f if, in all executions of
∆, e is not simultaneous with f ). In the case of safe Petri nets with sequential
executions, ≺∆ is the only invariant we need (as then, e.g., ≺∆ = @∆ and
−1
∆ = ≺∆ ∪ ≺∆ ). In particular, ∆ is the set of all sequential executions
corresponding to the linearisations of ≺∆ . The soundness of this approach is
validated by Szpilrajn’s Theorem [20] which states that each poset is equal to
the intersection of its linearisations.
In this paper, executions are observed as step sequences, i.e., sequences of
finite sets (steps) of simultaneously executed events. As an example, consider
the safe Petri net depicted in Figure 1(a) which generates three step sequences
involving a, c and d, viz. σ = {a}{c, d}, σ 0 = {a}{c}{d} and σ 00 = {a}{d}{c}.
They can be seen as forming a single concurrent history ∆ = {σ, σ 0 , σ 00 } under-
pinned by a causal poset ≺∆ satisfying a ≺∆ c and a ≺∆ d . Moreover, such a
∆ adheres to the following true concurrency paradigm:
Given two events (c and d in ∆), they can be observed as simultaneous
(in σ) ⇐⇒ they can be observed in both orders (c before d in σ 0 , and d
before c in σ 00 ). (TrueCon)
Concurrent histories adhering to TrueCon are underpinned by causal partial
orders, in the sense that each such history comprises all step sequence executions
consistent with a unique causal poset on events involved in the history.
In [6] fundamental concurrency paradigms are identified, including (TrueCon).
Another paradigm is characterised by (TrueCon) with ⇐⇒ replaced by ⇐=.
This paradigm has a natural system model interpretation provided by safe Petri
nets with inhibitor arcs. Figure 1(b) depicts such a net generating two step se-
quences involving a, c and d, viz. σ = {a}{c, d} and σ 0 = {a}{c}{d}. They form
Causal Structures for General Concurrent Behaviours 195
a concurrent history ∆0 = {σ, σ 0 } adhering to the paradigm that unorderedness
implies simultaneity, but not to the true concurrency paradigm as ∆0 has no
step sequence in which d precedes c although in σ, c and d occur in a single step.
As a result, histories adhering to the weaker paradigm are not underpinned
by causal partial orders, but rather by causality structures (X, ≺, @) introduced
in [7] — called stratified order structures (so-structures) — based on causal-
ity and an additional weak causality (‘not later than’) relation. A version of
Szpilrajn’s Theorem can be shown to hold also for so-structures and the con-
current histories they generate. Stratified order structures were independently
introduced in [3] (as ‘prossets’). Their comprehensive theory was developed in
e.g. [8, 9, 12, 15]. As shown in this paper, so-structures can be represented in
a one-to-one manner by mutex order structures, or mo-structures, (X, , @)
based on interleaving/mutex and weak causality. The first, symmetric, relation
defines the events that never occur simultaneously. Hence strict event precedence
(causality) can be captured as a combination of mutex and weak causality.
This paper focuses on the least restrictive paradigm. i.e., there are no con-
straints imposed on concurrent histories. It admits all (invariant closed) con-
current histories comprising step sequence executions. As shown in [6], it is now
sufficient to consider only two invariant relations, viz. mutex and weak causality.
Figure 1(c) depicts a safe Petri net with mutex arcs (see [11]) generating two
step sequences involving a, c and d, viz. σ 0 = {a}{c}{d} and σ 00 = {a}{d}{c}.
We first observe that they form a concurrent history ∆00 = {σ 0 , σ 00 } in which the
executions of c and d interleave, and are both preceded by a; in other words,
c ∆00 d, a @∆00 c, a @∆00 d and c ∆00 a ∆00 d. That ∆00 is a concurrent
history then follows from the observation that ∆00 contains all step sequences
involving a, c and d which obey these invariant relationships. However, ∆00 does
not conform to the two earlier considered paradigms as there is no step sequence
in ∆00 in which c and d occur simultaneously. To summarise, a nonempty set
∆ of step sequence executions over a common set of events X, is a concurrent
history iff ∆ consists of all step sequences σ over X such that for all e, f ∈ X:
e ∆ f implies that e and f are not simultaneous in σ, and e @∆ f implies that
e precedes or is simultaneous with f in σ.
The aim of this paper is to provide a structural characterisation of general
concurrent histories (consisting of step sequence executions). An early attempt to
describe structures of this kind was made in [4]. The there proposed generalised
stratified order structures (or gso-structures) do however not always capture all
implied invariant relationships involving the mutex relation. Here, we will show
that generalised mutex order structures (or gmo-structures) describe exactly all
general concurrent histories. The main result is a version of Szpilrajn’s Theorem,
formulated and proven to hold for gmo-structures and concurrent histories. For
this we develop a notion of gmo-closure which is the gmo-structure counterpart
of transitive closure of an acyclic relation.
First, we recall key notions and notations used throughout the paper. In Sec-
tion 3, we introduce mo-structures and establish their relationship with strat-
ified order structures. Then, Section 4 introduces gmo-structures and proves
196 R. Janicki, J. Kleijn, M. Koutny, Ł. Mikulski
their main properties, including gmo-closure and the gmo-structure version of
Szpilrajn’s Theorem. Section 5 presents concluding remarks.
Proofs of all the results can be found in the Technical Report available at
http://www.cs.ncl.ac.uk/publications/trs/papers/1378.pdf.
2 Preliminary Definitions
Throughout the paper we useUthe standard notions of set theory and formal
language theory. In particular, denotes disjoint set union. The identity relation
on a set X is defined as Id X = {ha, ai | x ∈ X}, the index X may be omitted if
it is clear from the context.
Composing relations. The composition of two binary relations, R and Q, over
X is given by R ◦ Q = {ha, bi | ∃x ∈ X : aRx ∧ xQb}. Moreover, if P ⊆ X × X,
then we define R ◦P Q = {ha, bi | ∃hx, yi ∈ P : aRxQb ∧ aRyQb} (see Figure 2).
ha, bi ∈ R ◦P Q: x
R:
a b Q:
y P :
Fig. 2. A visualisation of ◦P composition.
Note that ◦ = ◦Id , and the associativity of relation composition holds for the
extended notion. We will also denote a1 . . . ak Rb1 . . . bm whenever ai Rbj , for all
i, j. For example, aRbcQd means that aRbQd and aRcQd.
Given a relation R ⊆ X × X, R0 = Id and Rn = Rn−1 ◦ R, for all n ≥ 1.
S reflexive closure of R is defined by R ∪Id ; (ii) the transitive closure
Then: (i) the
by R+ = i≥1 Ri ; (iii) the reflexive transitive closure by R∗ = Id ∪ R+ ; and
(iv) the irreflexive transitive closure by R = R+ \ Id = R∗ \ Id . Moreover, the
inverse of R is given by R−1 = {ha, bi | hb, ai ∈ R}, and the symmetric closure
by Rsym = R ∪ R−1 .
Order relations. A relation R ⊆ X × X is: (i) symmetric if R = R−1 ; (ii)
antisymmetric if R ∩ R−1 ⊆ Id ; (iii) reflexive if Id ⊆ R; (iv) irreflexive if
Id ∩ R = ∅; (v) transitive if R ◦ R ⊆ R ∪ Id ; and (vi) total if R ∪ R−1 = X × X.
A relation R ⊆ X × X is: (i) an equivalence relation if it is symmetric,
transitive and reflexive; (ii) a pre-order if it is transitive and irreflexive; (iii) a
partial order if it is an antisymmetric pre-order; and (iv) a total order if it is a
partial order and R ∪ Id is total; (v) a stratified order if it is a partial order such
that X × X \ Rsym is an equivalence relation.
Every irreflexive relation R ⊆ X × X induces a least pre-order containing
R defined by R . Following E. Schröder [19], we define the largest equivalence
relation contained in R∗ as R~ = R∗ ∩ (R∗ )−1 = (R ∩ (R )−1 ) ] Id .
Causal Structures for General Concurrent Behaviours 197
For a stratified order R ⊆ X × X we define two relations, @R and R , such
that, for all distinct a, b ∈ X:
a @R b ⇐⇒ ¬(bRa) and a R b ⇐⇒ ¬(a @~
R b) ⇐⇒ aRb ∨ bRa .
Intuitively, if R represents a stratified order execution, aRb means ‘a occurred
earlier than b’. In such a case a @R b means ‘a occurred not later than b’, a R b
means ‘a did not occur simultaneously with b’, and a @~ R b means ‘a occurred
simultaneously with b’.
Relational structures. A tuple S = (X, R1 , R2 , . . . , Rn ), where n ≥ 1 and each
Ri ⊆ X × X is a binary relation on X, is an (n-ary) relational structure. By
the domain of a relational structure S we mean the set X. An extension of S
is any relational structure S 0 = (X, R10 , R20 . . . , Rn0 ) satisfying Ri ⊆ Ri0 , for every
1 ≤ i ≤ n. We denote this by S ⊆ S 0 . The intersection of a nonempty family
R = {(X, R1i , . . . T
, Rni ) | i ∈ I}
T of relationalTstructures with the same domain and
arity is given by R = (X, i∈I R1i , . . . , i∈I Rni ). In what follows, we consider
only relational structures that contain two relations, while the set X is finite.
A relational structure S = (X, Q, R) is: (i) separable if Q ∩ R~ = ∅, Q is
symmetric and R is irreflexive; and (ii) saturated in a family of relational struc-
tures X if it belongs to X and for every extension S 0 ∈ X of S, we have
S = S 0 . It is easily seen that an intersection of separable relational structures is
also separable. Intuitively, if Q represents ‘mutex’ and R ‘weak precedence’, then
separability means that simultaneous events cannot be in the mutex relation.
A stratified order structure (or so-structure) is defined as a relational struc-
ture sos = (X, ≺, @), where ≺ and @ are binary relations on X such that, for
all a, b, c ∈ X:
S1 : a 6@ a S3 : a @ b @ c ∧ a 6= c =⇒ a @ c
S2 : a ≺ b =⇒ a @ b S4 : a @ b ≺ c ∨ a ≺ b @ c =⇒ a ≺ c .
A generalized stratified order structure [4] (or gso-structure) is a relational
structure gsos = (X, , @) such that @ is irreflexive, is irreflexive and sym-
metric, and (X, ∩ @, @) is an so-structure. A comprehensive treatment of
gso-structures can be found in [5].
Properties. For every binary relation R ⊆ X × X and all a, b ∈ X, we have:
(R ∪ ha, bi)∗ = R∗ ∪ {hc, di | cR∗ a ∧ bR∗ d} . (1)
∗ ~ ~
¬(bR a) =⇒ (R ∪ ha, bi) = R (2)
~ ~ −1 ∗
R = (R ) ⊆R (3)
∗ ∗ ∗ ∗ ∗ ~ ~
(R ) = R
(R ) = R (R ) = R (R ) = R (4)
~ ~ ~ ∗ ~ ~ ∗ ∗ ∗ ∗
R ◦R =R R ◦R =R ◦R =R ◦R =R (5)
If R ⊆ X × X is a stratified order, then R is irreflexive and symmetric, while
@R is a pre-order such that:
−1
@R = @+
R \Id = @R
and @~
R \Id = @R ∩ @R . (6)
198 R. Janicki, J. Kleijn, M. Koutny, Ł. Mikulski
Moreover, for all distinct a, b ∈ X, we have:
¬(a R b) ⇐⇒ a @R b ∧ b @R a (7)
¬(a @R b) =⇒ b @R a (8)
aRb ⇐⇒ a R b ∧ a @R b . (9)
and exactly one of the following holds:
a b a @ b 6@ a
a b a 6@ b @ a (10)
a 6 b 6 a @ b @ a.
Intuitively, (9) means that ‘a occurred earlier than b’ iff ‘a and b were not
simultaneous’ and ‘a occurred not later than b’.
3 Separable Order Structures
In this section we take another look at the stratified order structures, substan-
tially different from that of, e.g., [8, 12, 15]. We provide for them a new represen-
tation more suitable for further generalisation. The new representation replaces
causal orders by mutex relations between events. While so-structures allow for
more compact representation (strict precedence involves fewer pairs of events
than mutex), the new order structures are easier to generalise to cater for gen-
eral interleaving/mutex requirements and their properties.
In the rest of this paper, we will be concerned with order structures of the
form S = (X, , @). Intuitively, X is a set of events involved in some history of
a concurrent system, is a ‘mutex’ (or ‘interleaving’) relation which identifies
pairs of events which cannot occur simultaneously, and @ is a ‘weak precedence’
relation between events. The latter means, in particular, that if a @ b @ a then
a and b must occur simultaneously in any execution belonging to the history
represented by S; in other words, S must be separable (i.e., ∩ @~ = ∅).
Mutex order structures The definition of the first class of order structures based
on mutex and weak precedence relations is motivated by the observation that the
‘precedence’ (or ‘causality’) relation is nothing but ‘mutex’+‘weak precedence’,
c.f. (9). Therefore, the axioms defining stratified order structures can easily be
rendered in terms of the latter relations.
Definition 1 (mutex order structure). A mutex order structure ( mo-struc-
ture) is a relational structure mos = (X, , @), where and @ are binary
relations on X such that, for all a, b, c ∈ X:
M1 : a b =⇒ b a
M2 : a 6@ a
M3 : a b =⇒ a @ b ∨ b @ a
M4 : a @ b @ c ∧ a 6= c =⇒ a @ c
M5 : a @ b @ c ∧ (a b ∨ b c) =⇒ a c.
Causal Structures for General Concurrent Behaviours 199
a b
a b M3
a b
a b c
M4 a b c
a 6= c
a b c a b c
M5
a c @:
a b c b
:
Fig. 3. A visualisation of axioms M3 − M5 .
Axioms M3 − M5 are illustrated in Figure 3, and some relevant properties
of mo-structures are given below.
Proposition 1. Let mos = (X, , @) be an mo-structure. Then mos is sepa-
rable and, for all a, b, c, d ∈ X, we have:
a6 a (11)
a@b@a ∧ a c =⇒ b c (12)
a@c@b ∧ a@d@b ∧ c d =⇒ a b. (13)
The next results demonstrate that mo-structures are in a one-to-one rela-
tionship with so-structures. Below, we use two mappings between these two
classes of order structures. For every so-structure sos = (X, ≺, @), we define
so2mo(sos) = (X, ≺sym , @), and for every mo-structure mos = (X, , @), we
define mo2so(mos) = (X, ∩ @, @).
Theorem 1. The mappings mo2so and so2mo are inverse bijections.
Layered order structures In general, order structures like mo-structures are not
saturated, and may capture histories comprising several executions (like a single
causal partial order may have numerous total order linearisations). However,
there is also a class of order structures which correspond in a one-to-one way to
step sequences.
Definition 2. Let R ⊆ X × X be a stratified order. Then los = (X, R , @R ) is
the layered order structure (or lo-structure) induced by R.
For a separable relational structure sr = (X, , @), we will denote by sr2los(sr )
the set of all lo-structures los extending sr , i.e., sr ⊆ los. With this nota-
tion, a Tnonempty
set LOS of lo-structures is a concurrent history if LOS =
sr2los LOS .
200 R. Janicki, J. Kleijn, M. Koutny, Ł. Mikulski
Proposition 2. Every layered order structure is separable and saturated in the
set of all separable order structures.
Proposition 3. Every lo-structure is an mo-structure.
An mo-structure is linked with lo-structures (step sequences) through the set
sr2los(mos) of all lo-structures extending mos. Similarly, for every so-structure
sos we can define so2los(sos) = sr2los(so2mo(sos)). It can then be seen ([8]) that
so2los(sos) is a nonempty set and (in the notation used in this paper):
\
sos = mo2so(so2los(sos)) . (14)
That result corresponds to Szpilrajn’s Theorem that any partial order is the
intersection of its linearisations (c.f. [5, 8]). Such a result extends to mo-struc-
tures and we obtain
T
Theorem 2. For every mo-structure mo, sr2los(mo) 6= ∅ and mo = sr2los(mo).
We can therefore conclude that the saturated extensions of an mo-structure
mos form a concurrent history represented by mos. It is then important to ask
which concurrent histories can be derived in this way; in other words, which
concurrent histories can be represented by mo-structures.
Consider now a nonempty set LOS = {(X, i , @i ) | i ∈TI} of lo-structures
forming a concurrent history, and their intersection S = LOS = (X, , @).
Since every lo-structure is also an mo-structure, we immediately obtain that S
is an order structure satisfying axioms M1 , M2 , M4 and M5 . However, M3 in
general does not hold although it holds for histories in which the possibility of
executing two events in either order always implies also simultaneous execution,
meaning that, for all distinct a, b ∈ X,
∃i ∈ I : ha, bi ∈ i ∩ @i
=⇒ ∃k ∈ I : ha, bi ∈ @sym
j .
∃j ∈ I : hb, ai ∈ j ∩ @j
One might now wonder what happens if we do not assume any special proper-
ties of a concurrent history. As we will show in the rest of the paper,TProposition 1
in combination with the observation that it always holds for S = LOS , yields
axioms for order structures underpinning general concurrent histories.
4 Generalised Order Structures
In this section, we provide a complete characterisation of general concurrent
histories where executions are represented by layered order structures; in other
words, histories comprising step sequence executions. We achieve this by retain-
ing all those mo-structure axioms which hold in general, and then replacing the
only dropped axiom M3 by Proposition 1.
Causal Structures for General Concurrent Behaviours 201
a a
c G5 c
b b
c c
a b G6 a b
@:
d d
:
Fig. 4. A visualisation of axioms G5 and G6 .
Definition 3 (generalised mutex order structure). A generalised mutex
order structure (or gmo-structure) is a relational structure gmos = (X, , @),
where and @ are binary relations on X such that, for all a, b, c, d ∈ X:
G1 : a b =⇒ b a M1
G2 : a 6@ a ∧ a 6 a M2 & (11)
G3 : a @ b @ c ∧ a 6= c =⇒ a @ c M4
G4 : a @ b @ c ∧ (a b ∨ b c) =⇒ a c M5
G5 : a@b@a ∧ a c =⇒ b c (12)
G6 : a@c@b ∧ a@d@b ∧ c d =⇒ a b (13)
The set of axioms in Definition 3 is minimal (see Figure 5). Moreover, gmo-
structures enjoy a number of useful properties.
Proposition 4. Let gmos = (X, , @) be a gmo-structure. Then gmos is sep-
arable and, for all a, b ∈ X, we have:
a @ b =⇒ a @ b a @ b @ a =⇒ a 6 b.
Proposition 5. Each mo-structure is a gmo-structure.
The converse of Proposition 5 does not hold; for example, as M3 does not
hold, ({a, b}, {ha, bi, hb, ai}, ∅) is a gmo-structure but not an mo-structure.
Proposition 6. If gmos = (X, , @) is a gmo-structure, then (X, ∩ @, @)
is an so-structure.
Proposition 6 states that every gmo-structure is a gso-structure. We observe
that the converse is not true, with suitable counterexamples provided by the
gso-structures SG5 and SG6 in Figure 5.
Closure operator for generalised mutex order structures We will now provide a
method for deriving valid gmo-structures from other relational structures.
202 R. Janicki, J. Kleijn, M. Koutny, Ł. Mikulski
SG1 : a b SG2 : SG3 : a c
a b
SG5 : a SG6 : c
SG4 : a c
b c a b
@:
b d :
Fig. 5. Examples showing that the set of axioms in Definition 3 is minimal. Each
relational structure SGi satisfies all axioms except for Gi.
Definition 4 (gmo-closure). Let S = (X, Q, R) be a relational structure and
Q[R] = R~ ◦ Q ∪ (R∗ ◦Q R∗ )sym ◦ R~ . Then the gmo-closure of S is given by:
S = X , Q[R] , R .
The gmo-closure operator introduced here can be seen as related to two
different closure operators: (i) the transitive closure operator for acyclic reflexive
binary relations; and (ii) the ♦-operator for ♦-acyclic order structures introduced
in [7] in order to obtain so-structures. It is also be seen as a generalisation of
the gso-closure introduced in [10] for gso-acyclic structures in order to obtain
gso-structures.
The main property we want from the notion of gmo-closure is that whenever
S = (X, Q, R) is a separable relational structure, S is a gmo-structure. Fur-
thermore, if S is already a gmo-structure, then we want S = S. The form of
Q[R] follows from the requirement that S should be a gmo-structure and the
axioms for gmo-structures. In particular the factor (R∗ ◦Q R∗ )sym follows from
axioms G4 and G6 , while the factor R~ ◦Q R~ corresponds to G5 .
a • • b
•
a • • b
•
•
a • • b R∗ :
• Q:
Fig. 6. A visualisation of the three cases of ha, bi ∈ Q[R] .
Causal Structures for General Concurrent Behaviours 203
The next four results respectively correspond to saying that: (i) the transitive
closure of an acyclic relation is also acyclic; (ii) gmo-closure is a closure operation
in the usual sense; (iii) the transitive closure of an acyclic relation yields a poset;
and (iv) posets are transitively closed.
Proposition 7. If S is a separable relational structure, then S is also separa-
ble, S ⊆ S and (S ) = S . Moreover, S is a gmo-structure.
Proposition 8. If gmos is a gmo-structure, then gmos = gmos.
As layered order structures and mutex order structures are special cases of
generalised mutex order structures, we obtain an immediate
Corollary 1. Let los be an lo-structure and mos be an mo-structure. Then
los = los and mos = mos.
The following technical lemma describes a single stage of the saturation pro-
cess for a gmo-structure leading to a los-structure. In such a process, we may
add an arbitrary link between two elements that do not yet satisfy (10). We only
need to remember that in the case of extending the relation Q, together with
ha, bi we have to add hb, ai. After such an addition, we get a separable order
structure that may be closed. As a result, we obtain one of possible extensions
of an initial gmos. The above process terminates after obtaining an lo-structure
and it is central to the proof of the main Theorem 3.
In what follows, we denote Rxy = R∪{hx, yi} and Qxyx = Q∪{hx, yi, hy, xi}.
Lemma 1. Let gmos = (X, Q, R) be a gmo-structure, a, b ∈ X and a 6= b.
ha, bi ∈ / R =⇒ (X, Q, Rab ) is a gmo-structure
/ R ∧ hb, ai ∈
ha, bi ∈ / Q =⇒ (X, Q, Rab ) is a gmo-structure
/ R ∧ ha, bi ∈
ha, bi ∈ / Q =⇒ (X, Qaba , R) is a gmo-structure .
/ R ∧ ha, bi ∈
To complete the properties of the saturation process described in Lemma 1
and used in the proof of Theorem 3, we formulate the following
Lemma 2. Let gmos = (X, Q, R) be a gmo-structure such that a, b ∈ X, a 6= b,
ha, bi ∈ / Q and S 0 = (X, Q, Rab ) = (X, Q0 , Rab
/ R and ha, bi ∈
/ Q0 .
). Then ha, bi ∈
In Lemmas 1 and 2 we have captured a method of saturating gmo-structures
that are not lo-structures. It moreover allows us to formulate an immediate
Corollary 2. Every relational structure saturated among all separable relational
structures is a layered order structure.
General concurrent histories We now return to our original goal which was to
provide a structural characterisation of all histories comprising step sequence
executions. Recall that sr2los(gmos) is the set of all lo-structures associated
with a gmo-structure gmos. Then we obtain a result corresponding to Szpilrajn’s
Theorem:
204 R. Janicki, J. Kleijn, M. Koutny, Ł. Mikulski
Theorem 3. For every gmo-structure gmos,
\
sr2los(gmos) 6= ∅ and gmos = sr2los(gmos) .
T that, for every nonempty set LOS of lo-structures
Together with the fact
with the same domain, LOS is a gmos-structure, this leads to the conclusion
that all concurrent histories are represented by gmo-structures.
5 Concluding Remarks
We can finally clarify the relationship between gso-structures and gmo-struc-
tures. In general, in order to accept an order structure os = (X, , @) as an
invariant representation of a concurrent history, we require that
\
sr2los(os) 6= ∅ and os = sr2los(os) .
We demonstrated that this property holds whenever os is a gmo-structure,
and that it may fail to hold for a gso-structure. We have further shown that gmo-
structures are gso-structures, but that the converse does not hold. However,
what is the case is that each gso-structure gsos is separable, and so its gmo-
closure gsos is a gmo-structure satisfying sr2los(gsos ) = sr2los(gsos). In other
words, concurrent histories described by separable order structures and their
gmo-closures are the same. The importance of gso-structures comes from the
fact that they paved the way for gmo-structures, by exposing the fundamental
property that causal ordering is a combination of mutex and weak ordering.
A key motivation for the research presented in this paper comes from concur-
rent behaviours as exhibited by safe Petri nets with mutex arcs. The resulting se-
mantical approach — which has been meticulously worked out above — is based
on gmo-structures which characterise all concurrent histories comprising step
sequence executions. A natural direction for further work is to provide a com-
patible language-theoretic representation of concurrent histories, by generalising
Mazurkiewicz traces [13] which correspond to causal posets, and comtraces [7]
which correspond to so-structures (or mo-structures). This development would
also allow to link the dynamic notions of mutex and weak causality with the
static properties of Petri nets with mutex arcs. The resulting semantics can also
support efficient verification techniques [2, 14, 18].
Acknowledgements
We would like to thank the anonymous reviewers for useful comments and sug-
gestions. This research was supported by a fellowship funded by the “Enhancing
Educational Potential of Nicolaus Copernicus University in the Disciplines of
Mathematical and Natural Sciences” Project Pokl.04.01.01-00-081/10, the Ep-
src Gaels and Uncover projects, and by an Nserc of Canada grant.
Causal Structures for General Concurrent Behaviours 205
References
1. Best, E., Devillers, R.: Sequential and concurrent behaviour in Petri net theory.
TCS 55(1), 87–136 (1987)
2. Esparza, J., Heljanko, K.: Unfoldings: A Partial-Order Approach to Model Check-
ing. Monographs in Theoretical Computer Science, Springer (2008)
3. Gaifman, H., Pratt, V.R.: Partial order models of concurrency and the computation
of functions. In: LICS. pp. 72–85 (1987)
4. Guo, G., Janicki, R.: Modelling concurrent behaviours by commutativity and weak
causality relations. In: AMAST. pp. 178–191 (2002)
5. Janicki, R.: Relational structures model of concurrency. Act. Inf. 45, 279–320 (2008)
6. Janicki, R., Koutny, M.: Structure of concurrency. TCS 112(1), 5–52 (1993)
7. Janicki, R., Koutny, M.: Semantics of inhibitor nets. Inf.&Comp. 123(1), 1 – 16
(1995)
8. Janicki, R., Koutny, M.: Fundamentals of modelling concurrency using discrete
relational structures. Acta Inf. 34, 367–388 (1997)
9. Juhás, G., Lorenz, R., Mauser, S.: Causal semantics of algebraic Petri nets distin-
guishing concurrency and synchronicity. Fundam. Inf. 86(3), 255–298 (2008)
10. Kleijn, J., Koutny, M.: The mutex paradigm of concurrency. In: Petri Nets. pp.
228–247 (2011)
11. Kleijn, J., Koutny, M.: Mutex causality in processes and traces. Fundam. Inf. 122,
119–146 (2013)
12. Le, D.T.M.: On three alternative characterizations of combined traces. Fundam.
Inf. 113(3), 265–293 (2011)
13. Mazurkiewicz, A.: Concurrent program schemes and their interpretations. DAIMI
Rep. PB 78, Aarhus University (1977)
14. McMillan, K.L.: Using unfoldings to avoid the state explosion problem in the ver-
ification of asynchronous circuits. In: CAVC. pp. 164–177 (1992)
15. Mikulski, Ł., Koutny, M.: Hasse diagrams of combined traces. In: Brandt, J., Hel-
janko, K. (eds.) ACSD. pp. 92–101 (2012)
16. Nielsen, M., Plotkin, G.D., Winskel, G.: Petri nets, event structures and domains,
Part I. TCS 13, 85–108 (1981)
17. Pratt, V.R.: Some constructions for order-theoretic models of concurrency. In:
Logic of Programs. pp. 269–283 (1985)
18. Rodriguez, C., Schwoon, S., Khomenko, V.: Contextual merged processes. In: Petri
Nets. LNCS, vol. 7927, pp. 29–48 (2013)
19. Schröder, E.: Vorlesungen über die Algebra der Logik (Exakte Logik). Dritter
Band: Algebra und Logik der Relative. B. G. Teubner (1895)
20. Szpilrajn, E.: Sur l’extension de l’ordre partiel. Fundam. Math. 16, 386–389 (1930)
21. Winkowski, J., Maggiolo-Schettini, A.: An algebra of processes. Journal of Com-
puter and System Sciences 35(2), 206–228 (1987)