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)