Paper deep dive
Cross-organisational Process Mining from Message Logs
Pieter Kwantes, Jetty Kleijn
Intelligence
Status: succeeded | Model: Gemma-4-26B-A4B | Prompt: intel-v1 | Confidence: 89%
Last extracted: 8/3/2026, 10:31:13 AM
Summary
This paper addresses the challenge of cross-organisational process mining by utilizing message logs instead of event logs, which are often inaccessible across organizational boundaries. It proposes a method to transform message logs (recordings of message exchanges between processes) into global event logs while preserving causal order. These event logs are then used to synthesize Industry nets, a Petri net framework for modeling collaborating business processes, using existing process discovery algorithms.
Entities (6)
Relation Signals (4)
Industry net → composedof → Enterprise net
confidence 90% · Industry nets consist of Enterprise nets that interact by exchanging messages
Message log → transformedinto → Event log
confidence 90% · message log can be transformed into a description of the communication behaviour in the form of an event log
Event log → usedforsynthesis → Industry net
confidence 90% · this event log can then be used to synthesis an Industry net
Message log → alternativeto → Event log
confidence 80% · it may be difficult to work with event logs from different organisations... Recordings of message exchanges... may be easier available
Cypher Suggestions (0)
No Cypher suggestions yet.
Abstract
Abstract:Enterprise nets and Industry nets are specific Petri net models that together form a framework for the modelling of collaborating business processes and the specification of interactions between them. In this set-up, individual business process are modelled as Enterprise nets, while Industry nets consist of Enterprise nets that interact by exchanging messages through unidirectional channels. In previous contributions (see [21,22]), it was established how to leverage algorithms for the discovery of single processes (modelled as Enterprise nets) from event logs (consisting of finite sequences of executed actions), to synthesise systems consisting of asynchronously communicating processes (modelled as Industry nets). However, in general, it may be difficult to work with event logs from different organisations or even get access to them. Recordings of message exchanges between processes may be easier this http URL, we focus in this paper on the communications between different processes and turn to the investigation of message logs, \ie collections of recordings of communications in the form of message exchanges (output and input events) between two processes. In particular, the question is addressed of how a message log can be transformed into a description of the communication behaviour in the form of an event log such that the causal order on message events is preserved. Following the approach from [21,22], this event log can then be used to synthesis an Industry net.
Tags
Links
- Source: https://arxiv.org/abs/2607.26917v1
- Canonical: https://arxiv.org/abs/2607.26917v1
Trouble viewing inline? Open PDF directly →
Full Text
158,052 characters extracted from source content.
Expand or collapse full text
11institutetext: LIACS, Leiden University, P.O.Box 9512 NL-2300 RA Leiden, The Netherlands 11email: p.m.kwantes,h.c.m.kleijn@liacs.leidenuniv.nl Cross-organisational Process Mining from Message Logs Pieter Kwantes Jetty Kleijn Pieter Kwantes Jetty Kleijn Abstract Enterprise nets and Industry nets are specific Petri net models that together form a framework for the modelling of collaborating business processes and the specification of interactions between them. In this set-up, individual business process are modelled as Enterprise nets, while Industry nets consist of Enterprise nets that interact by exchanging messages through unidirectional channels. In [14, 15], it was established how to leverage algorithms for the discovery of single processes (modelled as Enterprise nets) from event logs (consisting of finite sequences of executed actions), to synthesise systems consisting of asynchronously communicating processes (modelled as Industry nets). However, in general, it may be difficult to work with event logs from different organisations or even get access to them. Recordings of message exchanges between processes may be easier available. Therefore, we focus in this paper on the communications between different processes and turn to the investigation of message logs, i.e., collections of recordings of communications in the form of message exchanges (output and input events) between two processes. In particular, the question is addressed of how a message log can be transformed into a description of the communication behaviour in the form of an event log such that the causal order on message events is preserved. Following the approach from [14, 15], this event log can then be used to synthesis an Industry net.111This paper is the full version of an extended abstract with the same title, presented at the third International workshop on Collaboration Mining for Distributed Systems (COMINDS 2024) held in conjunction with ICPM 2024 in Copenhagen. Keywords: Enterprise net; Industry net; distributed process mining; event log; message log; causal partial order 1 Introduction Process mining is concerned with the algorithmic discovery of models of business processes from event data, to check their conformance, analyse bottlenecks, and suggest improvements, (see, e.g., [30, 24, 2, 16]). So far, the focus of process mining research has been on discovering local business processes, i.e., residing within the boundaries of a single organisation or enterprise. The interaction between business processes from different organisations has received less attention (see, e.g., [17, 20, 23]). Nevertheless, in many cases, organisations collaborate with other organisations, thereby forming cross-organisational processes, i.e., conglomerates of interacting local business processes. The behaviour of a cross-organisational process is a combination of the local behaviours of its individual business processes subject to their interactions. On the other hand, the behaviour of a local business process within a cross-organisational process will in general be affected by interactions with the other local business processes. The extension of established process mining methods and techniques from local processes of individual organisations to global (at the level of the collaborating organisations) processes appears in the research agenda in the Process Mining Manifesto [25] as an open challenge. Petri nets are a well-established formal framework for the modelling of a wide range of distributed systems (see, e.g., [11, 12, 18, 19]). Also the modelling of business processes is traditionally an important application domain of Petri nets, see [29, 26, 16]. A specific class of Petri nets that supports a formal algorithmic analysis of business processes and that is often used in practice are the workflow nets, originally introduced in [28]. In [13], a framework was proposed to specify the composition of a comprehensive global process model (an Industry net) from a set of local process models (Enterprise nets). Enterprise nets are Petri nets with typed input and output transitions, and internal transitions. They can be considered as a generalisation of workflow nets. Industry nets consist of separate Enterprise nets that interact by exchanging messages through unidirectional channels (in the form of additional places connecting a single output transition of one Enterprise net with a single input transition with the same type, of another Enterprise net). A comprehensive overview with a discussion of this and other models can be found in [3]. As argued in [13], the set-up proposed there ensures that global compliance of an Industry net with a reference model can be verified by local checks (of Enterprise nets) only. As stated in [25], it may be difficult to work with local information from different organisations as these are often reluctant to disclose their logs to the public domain. Furthermore, even if local information is available, there is the problem of so-called event correlation (see also [25]) to determine how local sequences of actions combine into global behaviour. Next, in the workshop paper [14] and its extended version [15], focus is on synthesising Industry nets from the observed global (combined) behaviour of collaborating Enterprise nets. More specifically, it is investigated to what extent existing algorithms for the discovery of local process models (Enterprise nets) from event logs, i.e., sets of finite sequences of events (occurrences of actions) representing the behaviour of a process, can be lifted to the synthesis of systems consisting of asynchronously communicating local processes (modelled as Industry nets), from global event logs. This requires a description of the distribution of actions over the components together with their role (internal, input, or output) in the form of a so-called distributed communicating alphabet. Whereas the information in local event logs is confined to single enterprises, communication involves multiple enterprises. Therefore, to address the problems mentioned earlier, we focus in this paper on the communications between local processes and turn to the investigation of message logs, collections of recordings of communications in the form of message exchanges between two processes, typically of typed messages over bilateral unidirectional channels. The type of a message represents its format (e.g., prescribed by the prevailing industry standard222Examples include the ISO15022 and ISO20022 industry standard for financial services, supported by SWIFT, RosettaNet for the electronics industry, and EDSN for the Dutch energy market, to name just a few. for groups of messages with similar processing characteristics). The subject of a message is referred to as the case of the message (e.g., an order number to identify a specific order). A single execution (or run) of a cross-organisational process comprises all events executed to complete a particular case. Recordings of such message exchanges appear as byproducts of day-to-day operations of message service providers (see, e.g., [7] for case studies exploring the use of recorded messages for process mining). Here, message exchanges will be defined in the form of two message events, an output event (representing the sending of the message by a local process) and an input event (representing the receipt of that message by a second local process). In this paper, we address the question of how message logs can be transformed into global event logs in such a way that essential properties of the behaviour of the global system as captured by the message log, are preserved. Following the approach from [14, 15], message logs thus transformed, can then be used for the discovery of an Industry net. The paper is organised as follows. Section 2 provides notation and notions used throughout this paper, including concepts relating to sequences (words), sets of sequences (languages), and partial orders. Special attention is given to the sequentialisation of partial orders. We argue how infinite partial orders can be represented by sets of finite sequences of actions. These observations are crucial in the following sections. In Section 3, message events and message logs are introduced. A message log is a (possibly infinite) set of message events together with their attributes, i.e., parameters giving the case to which an event belongs and its type, as well as the process executing the event and a local time. More precisely, each process has a time function which assigns time stamps to its message events in such a way that no two different events executed by the same process are assigned the same local time. Hence, the events of a local process are always totally ordered by their time stamps. This total order is assumed to be consistent with the causal dependencies between message events in the sense that whenever a message event e has an earlier time stamp than another message event e′e executed by the same local process, then e′e does not causally precede e (i.e., it is not necessary to execute e′e before e). Next, we discuss in Section 4, a natural precedence relation on message events belonging to the same case, and how and when this defines a partial order. As discussed in Section 2, this (possibly infinite) partial order can then be used to define a set of finite sequences of message events, that together describe one of the runs of the system captured by the message log. In Section 5, the aim is to associate an event log and a distributed communicating alphabet with a given message log. This entails an interpretation of output events and input events as occurrences of output actions and input actions, respectively, leading to a labelling of message events by action names. We investigate how to consistently identify message events in a message log that are to be labelled with the same action name. This leads to the concept of an action function that can be used to translate the set of finite sequences of message events defined by a message log into a global event log consisting of sequences of labelled message events. Moreover, action functions can be used to define a suitable distributed communicating alphabet which on the one hand describes the distribution of output and input actions over components, and on the other hand how they are paired up into unidirectional bilateral channels used to exchange the messages recorded in the message log. Clearly, as the global event logs thus derived are defined by identifying message events, they are more abstract than the original message logs. So, the main question addressed in Section 6 is whether the causalities in a message log as expressed by the partial order derived from the precedence relation, are faithfully preserved in the global event log defined by an action function. To settle this question we turn to the assignment functions introduced in [15], to relate occurrences of input and output actions in the labelled sequences constituting a global event log. It is demonstrated how the causal partial orders underlying the sequences of the message log coincide with the partial orders on the occurrences of actions defined by message preserving assignment functions. Moreover, all sequences defined by the partial orders of message preserving assignments are in the global event log. Thus, given a message log and an action function, a distributed alphabet and a global event log can be derived that faithfully represents the causalities in the message log. We also discuss assignment functions that are oblivous to the identities of the message exchanged and model a first-in-first-out channel policy based on output and input actions. In Section 7, we combine all technical results obtained and apply the procedure from [15] to synthesise on the basis of a given process discovery algorithm an Industry net that generates at least all sequences from the event log. Finally, Section 8 reflects on the research presented. In the Appendix, the proof of Lemma 2 is given. This auxiliary result is crucial for the representation of infinte partial orders by finite sequences. The Appendix also provides the definitions for Petri nets, Enterprise nets and Industry nets, as well as definitions of key concepts and results from [15]. Related work Using the messages exchanged between collaborating enterprises as input for process mining and process discovery, has been proposed before. In particular, the use of messages exchanged between web services (from different enterprises) has been described, e.g., in [27, 1, 9, 8, 7]. In [27], information from the so-called web services stack is used to obtain event logs. According to [1], global message logs comprising the messages from multiple parties involved in a collaboration of web services, can be reconstructed with middleware technology and translated into an event log including a case id, an activity name and a time stamp. It is then shown how this event log can be used to check conformance of the event log with a Petri net model of the business process, derived from a BPEL specification. Several case studies ([9, 8, 7]) describe how a message log, gathered at a particular enterprise, can be used to derive an event log and subsequently, using existing process discovering algorithms, a process model. For example, [7] proposes an approach for cross-organisational process mining, based on the use of EDI-messages, which is implemented in the EDI miner toolset [6]. Based on a review of 66 articles, the paper [20] provides an overview of current research. It concludes that research into the field has been dispersed and gives an agenda for future research with a focus on socio-technical aspects is proposed. In [3, 4] a survey of different approaches to modelling cross-organisational processes is provided. This leads to the conclusion that a standard modelling framework is lacking and to an investigation of a more standardised approach based on Petri nets. 2 Preliminaries General notions By ℕN we denote the set of natural numbers 0,1,2,…\0,1,2,…\. For n∈ℕn , [n]=1,2,…,n[n]=\1,2,…,n\. Hence, [0]=∅[0]= . Let A be a set. If A is a finite set, then (A) card(A) denotes its cardinality. Let =Ai∣Ai⊆A,i∈ℐA=\A_i A_i A,i∈I\ with ℐI an index set, be such that the AiA_i are pairwise disjoint, non-empty sets, and A=⋃Ai∣i∈ℐA= \A_i i∈I\. Then A is a partition of A. Functions are total unless explicitly stated otherwise. For a function f:A→Bf:A→ B and C⊆AC A, we define f(C)=f(c)∣c∈Cf(C)=\f(c) c∈ C\ and the restriction of f to C is the function f|C:C→Bf|_C:C→ B, defined by f|C(c)=f(c)f|_C(c)=f(c) for all c∈Cc∈ C. A function f:A→Af:A→ A is a complement function if A=B∪CA=B∪ C with B and C disjoint, f(B)⊆Cf(B) C, f(C)⊆Bf(C) B, and f(f(a))=af(f(a))=a for all a∈Aa∈ A. Note that such f is injective, because whenever f(a)=f(a′)f(a)=f(a ) for some a,a′∈Aa,a ∈ A, then a=f(f(a))=f(f(a′))=a′a=f(f(a))=f(f(a ))=a . Moreover, f(B)=Cf(B)=C, since c=f(f(c))c=f(f(c)) for all c∈Cc∈ C. Similarly, f(C)=Bf(C)=B. Thus, f is a bijection. Words and Languages Throughout the paper, we will be dealing with sequences of events, actions, labels, etc., represented as symbols. Sets of symbols may be empty, finite, or infinite. An alphabet is a set of symbols which is finite and non-empty, unless explicitly specified otherwise. Let Σ be a set of symbols. A word (over Σ ) is a possibly infinite sequence of symbols (from Σ ). As usual, Σ∗ ^* is the set of all finite words over Σ , Σω ^ω the set of all infinite words (or ω-words) over Σ , and Σ∞=Σ∗∪Σω ^∞= ^*∪ ^ω the set of all words over Σ . Any subset L of Σ∞ ^∞ is a language (over Σ ). If L⊆Σ∗L ^*, then L is finitary and if L⊆ΣωL ^ω, then it is an infinitary language. For a finite word w=a1⋯anw=a_1·s a_n with n≥0n≥ 0 and ai∈Σa_i∈ for all i∈[n]i∈[n], we refer to n as the length of w, denoted by |w||w|. If n=0n=0, then w=λw=λ, the empty word (over Σ ). It is often convenient to consider words as functions. Thus, a finite word w=a1⋯anw=a_1·s a_n with ai∈Σa_i∈ for all i∈[n]i∈[n], is defined by w:[n]→Σw:[n]→ with w(i)=aiw(i)=a_i for all i∈[n]i∈[n]; and an infinite word v=a1a2⋯v=a_1a_2·s is v:ℕ→Σv:N→ with v(i)=aiv(i)=a_i for all i∈ℕi . The domain of a word u∈Σ∞u∈ ^∞, denoted (u) dom(u), is the set of integers on which u is defined. Hence we have (u)=[n] dom(u)=[n] if |u|=n|u|=n and (u)=ℕ dom(u)=N if u is infinite. The alphabet of u, denoted by (u) alph(u), is the set of symbols that occur in u. Thus (u)=a∈Σ∣∃i∈(u):u(i)=a alph(u)=\a∈ ∃ i∈ dom(u):u(i)=a\ and, in particular, (λ)=∅ alph(λ)= . Moreover, the alphabet of u is infinite whenever u is an infinite word in which an infinite number of different symbols occur (hence in this case Σ must be an infinite set of symbols). For a language L, (L)=a∈Σ∣∃w∈L:a∈(w) Alph(L)=\a∈ ∃ w∈ L:a∈ alph(w)\ is the set of all symbols that occur in some word of L. Let w∈Σ∗w∈ ^* and a∈Σa∈ . Then #a(w)=(i∣w(i)=a)\#_a(w)= card(\i w(i)=a\) is the number of occurrences of a in w and (w)=(a,i)∣a∈(w)∧1≤i≤#a(w) occ(w)=\(a,i) a∈ alph(w) 1≤ i≤\#_a(w)\ is the set of all occurrences of symbols from Σ in w. The function w:(w)→[|w|] pos_w: occ(w)→[|w|] gives for each (a,i)∈(w)(a,i)∈ occ(w), its position in w: w((a,i))=k pos_w((a,i))=k if w(k)=aw(k)=a and #a(w(1)⋯w(k))=i\#_a(w(1)·s w(k))=i. Any function f:Σ→Δf: → where Δ is a set of symbols can be extended to a function f∞:Σ∞→Δ∞f^∞: ^∞→ ^∞ by setting f∞(λ)=λf^∞(λ)=λ and (f∞(w))(i)=f(w(i))(f^∞(w))(i)=f(w(i)) for all w∈Σ∞w∈ ^∞ and i∈(w)i∈ dom(w). Omitting the superscript ∞, we usually write f instead of f∞f^∞. Let now Δ⊆Σ . Then the projection of Σ on Δ is the function Σ,Δ:Σ∗→Δ∗ proj_ , : ^*→ ^*, defined by Σ,Δ(a)=a proj_ , (a)=a if a∈Δa∈ ; Σ,Δ(a)=λ proj_ , (a)=λ if a∈(Σ∖Δ)∪λa∈( )∪\λ\; and for all a∈Σa∈ and w∈Σ∗w∈ ^*, Σ,Δ(aw)=Σ,Δ(a)Σ,Δ(w) proj_ , (aw)= proj_ , (a) proj_ , (w). If Σ is clear from the context, we may omit the reference to Σ and write Δ proj_ . The (left-)concatenation of u∈Σ∗u∈ ^* and v∈Σ∞v∈ ^∞, denoted as uvuv, is the word w∈Σ∞w∈ ^∞ defined by w(i)=u(i)w(i)=u(i) for all i∈(u)i∈ dom(u) and w(|u|+i)=v(i)w(|u|+i)=v(i) for all i∈(v)i∈ dom(v). Let w∈Σ∞w∈ ^∞. If u∈Σ∗u∈ ^*, is such that w=uvw=uv for some v∈Σ∞v∈ ^∞, then u is a prefix of w. For n∈(w)n∈ dom(w), we denote by w[n]w[n] the prefix of w of length n. The set of all prefixes of w is denoted by (w) pref(w). Note that we only deal with finite prefixes and so (w)⊆Σ∗ pref(w) ^*. For a language L⊆Σ∞L ^∞, its set of prefixes is (L)=u∈Σ∗∣∃w∈L:u∈(w) Pref(L)=\u∈ ^* ∃ w∈ L:u∈ pref(w)\. We say that L is prefix-closed if (L)⊆L Pref(L) L. It should be noted here that, L⊆(L)L Pref(L) only holds for finitary languages. On the other hand, any infinite word can be viewed as the limit of its prefixes. More generally, let L⊆Σ∗L ^*. Then the limit of L (see, e.g., [10, 21]) is the language (L)=w∈Σω∣w[i]∈L for infinitely many i∈ℕ lim(L)=\w∈ ^ω w[i]∈ L for infinitely many i \. Clearly, ((w))=w lim( pref(w))=\w\ for every infinite word w. As a consequence, L⊆((L))L lim( Pref(L)) holds for every infinitary language L. Such inclusion may be strict, as there are infinitary languages L such that ((L))⊈L lim( Pref(L)) L. Example 1 Consider L=akbaω∣k∈ℕL=\a^kba^ω k∈N\. Then (L)=akbaℓ∣k,ℓ∈ℕ∪a∗ Pref(L)=\a^kba k, ∈N\∪\a\^*. And so, ((L))=L∪aω lim( Pref(L))=L∪\a^ω\. ∎ Finally, we recall a property of words (and languages) from [15], introduced there to formalise how in an action sequence, every occurrence of an input action is preceded by a corresponding occurrence of an output action. Let Σo,Σι⊆Σ _o, _ with Σo∩Σι=∅ _o∩ _ = and let f:Σo→Σιf: _o→ _ be a bijection. Let w∈Σ∞w∈ ^∞. Then w has the prefix property with respect to f if, for all v∈(w)v∈ pref(w) and for all a∈Σoa∈ _o, #a(v)≥#f(a)(v)\#_a(v)≥\#_f(a)(v). A language L⊆Σ∞L ^∞ is said to have the prefix property with respect to f if all w∈Lw∈ L have the prefix property with respect to f. Partial orders and total orders Let A be a set. Let R⊆A×AR A× A be a binary relation on A. The identity relation on A is A=(a,a)∣a∈A Id_A=\(a,a) a∈ A\. In what follows, we will mostly use the infix notation for binary relations. Thus we write aRba\,R\,b for (a,b)∈R(a,b)∈ R. Relation R is reflexive if A⊆R Id_A R, i.e., if aRa\,R\,a for all a∈Aa∈ A; it is irreflexive if there is no a∈Aa∈ A such that aRa\,R\,a; it is transitive if whenever aRba\,R\,b and bRcb\,R\,c, then also aRca\,R\,c; it is antisymmetric if whenever both aRba\,R\,b and bRab\,R\,a, then a=ba=b. The transitive closure R+R^+ of R is defined by R+=(a,b)∣∃n≥1, a0,a1,…,an∈A such that a0=a,an=b, and ∀i∈[n]: ai−1RaiR^+=\(a,b) ∃ n≥ 1, a_0,a_1,…,a_n∈ A such that a_0=a,a_n=b, and $∀ i∈[n]$: a_i-1\,R\,a_i\. The reflexive, transitive closure of R is R∗=R+∪AR^*=R^+∪ Id_A. R is said to be acyclic if R+∖AR^+ Id_A is irreflexive, i.e., there are no a,a1,…,an=a∈Aa,a_1,…,a_n=a∈ A, n≥1n≥ 1 with (a,a1),…,(an−1,a)∈R(a,a_1),…,(a_n-1,a)∈ R. If R is reflexive, transitive, and antisymmetric, it is a partial order on A. If R is a partial order such that xRyxRy or yRxyRx, for all x,y∈Ax,y∈ A, then R is a linear order (or total order). A partially ordered set, or poset, is a pair (A,≤A)(A, _A), where A is a set and ≤A _A is a partial order on A. If ≤A _A is a linear order, we refer to (A,≤A)(A, _A) as a linearly ordered set. Let =(A,≤A) po=(A, _A) be a poset. Poset (B,≤B)(B, _B) is said to be a sub-poset of po if B⊆AB A and ≤B⊆≤A _B\; \; _A. If B⊆AB A and ≤B=≤A∩(B×B) _B\;=\; _A\;∩\;(B× B), then we refer to (B,≤B)(B, _B) as the sub-poset induced by B. A linear extension of the poset =(A,≤A) po=(A, _A) is a poset =(A,≤′) lo=(A,≤ ) such that ≤′≤ is a linear order on A and ≤A⊆≤′ _A\; \;≤ . In such case, we also loosely call ≤′≤ a linear extension of ≤. Note that every poset is a sub-poset of each of its linear extensions. We use () linext( po) to denote the set of all linear extensions of po. The linear extensions of a poset are maximal in the sense that adding a new relation between two distinct elements leads to a cycle (and so the result is no longer a partial order). By Szpilrajn’s theorem [22] every poset has a linear extension. Moreover, as a consequence, every partial order is the intersection of its linear extensions. If every non-empty subset B of A has a minimal element with respect to ≤A _A (i.e., there exists an element b∈Bb∈ B such that for all a∈Ba∈ B whenever a≤Aba _Ab then a=ba=b), then both the partial order ≤A _A and the poset (A,≤A)(A, _A) are said to be well-founded333An equivalent definition is: ≤A _A is well-founded iff there is no infinite sequence a1,a2,…a_1,a_2,… of distinct ai∈Aa_i∈ A, such that ai+1≤Aaia_i+1 _Aa_i for all i∈ℕi . In other words, in a well-founded poset, every element has only finitely many elements that precede it.. Clearly, if A is finite, then every partial order on A is well-founded. In particular, the trivial poset (∅,∅)( , ) is well-founded. It is not difficult to see that if a partial order has a well-founded linear extension, then it is well-founded. Conversely, if =(A,≤A) po=(A, _A) is a well-founded poset, then po has a well-founded linear extension, see, e.g., [5]. In particular, if A is a countably infinite set444As it turns out, the partial orders that we consider in the body of the paper are all on finite or countably infinite sets. and =(A,≤A) po=(A, _A) is well-founded, then one can prove555See, e.g., https://math.stackexchange.com/questions/4194162/which-partial-orders-can-be-extended-to-a-copy-of-omega for a proof sketch, as outlined here: Given an enumeration a0,a1,a2,a3,…a_0,a_1,a_2,a_3,… of A, recursively define a sequence b0,b1,b2…b_0,b_1,b_2… in the following way. Assuming that b0,…,bk−1b_0,…,b_k-1 have been defined for some k≥0k≥ 0, let i be the least integer such that ai∉b0,…bk−1a_i ∈\b_0,… b_k-1\ and a∣a≤Aai⊆b0,…bk−1\a a _Aa_i\ \b_0,… b_k-1\. Then bk=aib_k=a_i. Now define ⪯A _A by a⪯a′a a with a≠a′a≠ a if a=bia=b_i, a′=bja =b_j for some i<ji<j. This ⪯A _A can be proved to be a linear extension of ≤A _A. that po has a well-founded linear extension on basis of an enumeration of A. Be aware though, that even a well-founded partial order on a countably infinite set, may have a linear extension that is not well-founded. Example 2 Consider =(A,A) po=(A, Id_A) with A=e0,e1,e2,…A=\e_0,e_1,e_2,…\ a countably infinite set. Then po is well-founded and (A,≤A)(A, _A) with ≤A=A∪(ei,ej)∣i,j∈ℕ and i<j _A= Id_A∪\(e_i,e_j) i,j∈N and i<j\ is a well-founded linear extension of A Id_A. However, (A,⪯A)(A, _A) with ⪯A=A∪((e2i,e2i−2)∣i≥1∪(e0,e1)∪(e2i+1,e2i+3∣i≥0)+ _A\;=\; Id_A∪(\(e_2i,e_2i-2) i≥ 1\∪\(e_0,e_1)\∪\(e_2i+1,e_2i+3 i≥ 0\)^+ is a linear extension of A Id_A that is not well-founded. ∎ Let =(A,≤A) lo=(A, _A) be a well-founded, linearly ordered set with A≠∅A≠ . Let ⋖A _A be the direct predecessor relation of lo: a⋖Aba _Ab holds if a≠ba≠ b, a≤Aba _Ab, and there is no c∈Ac∈ A such that a≠c≠ba≠ c≠ b and a≤Ac≤Aba _Ac _Ab. Then lo defines the unique sequence σ=a1a2⋯ _ lo=a_1a_2·s such that ai∣i∈(σ)⊆A\a_i i∈ dom( _ lo)\ A and A=ai∣i∈(σ)A=\a_i i∈ dom( _ lo)\ in case σ _ lo is finite, and, for all i,i+1∈(σ)i,i+1∈ dom( _ lo), ai⋖Aai+1a_i _Aa_i+1. Every a∈Aa∈ A occurs at most once in σ _ lo, because ≤A _A as a partial order is acyclic. Since lo is well-founded and a linear order, it has a least element a with a≤Aba _Ab for all b∈Ab∈ A. Clearly, this least element is a1a_1, the first element of σ _ lo. The language, i.e., the set of sequences defined by a well-founded, partial order po is ()=σ∣∈() and is well-founded seq( po)=\ _ lo lo∈ linext( po) and lo is well-founded\. We note that every well-founded poset defines at least one sequence. Example 3 Let =(A,≤A) po=(A, _A) be a poset with A=e0,e1,e2,…∪dA=\e_0,e_1,e_2,…\∪\d\ and ≤A=(d,d)∪(ei,ej)∣i,j∈ℕ and i≤j _A=\(d,d)\∪\(e_i,e_j) i,j∈N and i≤ j\. Then po is well-founded with minimal elements e0e_0 and d. We set ⪯A0=≤A∪(d,ei)∣i≥0 ^0_A\;=\; _A∪\;\(d,e_i) i≥ 0\, which is a well-founded linear extension of ≤A _A with minimal element d. Next, define, for all k∈ℕk , k≥1k≥ 1, the well-founded linear order ⪯Ak=≤A∪(ei,d)∣0≤i<k∪(d,ei)∣i≥k ^k_A\;=\; _A∪\;\(e_i,d) 0≤ i<k\\;∪\;\(d,e_i) i≥ k\. Each of these is a well-founded linear extension of ≤A _A with minimal element e0e_0. Finally, ⪯A=≤A∪(ei,d)∣i∈ℕ _A\;=\; _A∪\;\(e_i,d) i∈N\, which again is a well-founded linear extension of ≤A _A. With =(A,⪯A) lo=(A, _A), we have σ⪯A=e0e1e2⋯ _ _A=e_0e_1e_2·s, an infinite sequence with no occurrence of d. Since po has no other (well-founded) linear extensions than the ones discussed above, ()=de0e1e2⋯∪e0e1e2⋯ekdek+1ek+2⋯∣k≥0∪e0e1e2⋯ seq( po)=\de_0e_1e_2·s\∪\e_0e_1e_2·s e_kde_k+1e_k+2·s k≥ 0\∪\e_0e_1e_2·s\ is the set of sequences defined by po. ∎ Let =(A,≤A) po=(A, _A) be a poset. A subset B⊆AB A is said to be downward-closed in po if for all a∈Aa∈ A whenever a≤Aba _Ab for some b∈Bb∈ B, also a∈Ba∈ B. The downward closure of b∈Ab∈ A in po is the downward-closed set (b)=a∈A∣a≤Ab past_ po(b)=\a∈ A a _Ab\ consisting of all elements in A that precede b (including b itself). It is not difficult to see that the prefixes of sequences defined by the linear extensions of a well-founded, partial order are consistent with the downward closure of their elements. Formally: Lemma 1 Let =(A,≤A) po=(A, _A) be a partial order and lo a well-founded, linear extension of po. If a1⋯ai∈(σ)a_1·s a_i∈ pref( _ lo) where a1,…,ai∈Aa_1,…,a_i∈ A for some i≥1i≥ 1, then (ai)⊆a1,…,ai past_ po(a_i) \a_1,…,a_i\. ∎ Clearly, in case of an infinite partial order, each of its associated sequences is infinite and so each of these sequences is the limit of its finite prefixes. However, as the following result shows, also the converse holds: every word that can be obtained as the limit of finite prefixes of sequences of an infinite partial order po actually belongs to the sequences of po. Note the contrast with Example 1. As can be seen from its proof (in the Appendix), this result holds for all languages defined by partial orders, because for any word obtained as the limit of prefixes of words of a partial order po a linear extension lo of po can be constructed such that w=σw= _ lo. Lemma 2 Let =(A,≤A) po=(A, _A) be a well-founded, partial order with A an infinite set. Then ()=((())) seq( po)= lim( Pref( seq( po))). Proof See Appendix 0.A. ∎ 3 Message Logs A cross-organisational process is understood here as a global, distributed system consisting of a finite number of local business processes, executed in different organisations with the local processes communicating through asynchronous exchanges of typed messages over unidirectional, bilateral channels. Example 4 The so-called “over the counter” (OTC) trading of securities involves high volumes of standardised message exchanges between financial institutions. Figure 1 shows part of the message exchanges between an Investment Firm and a Custodian (an intermediary party) involved in a securities transaction. InvestmentFirmCustodianSISC Figure 1: OTC settlement The Investment Firm sends a Settlement Instruction, instructing the Custodian to transfer securities, previously traded (sold or bought) on the OTC market, from or into the account of the Investment Firm. On completion of the instruction, the Custodian returns a Settlement Confirmation to the Investment Firm. ∎ Every instantiation of a global process is represented by a case. In Example 4 above, the settlement of a transaction on the OTC market would be such instantiation and as a case typically be represented by a transaction identifier. A message is a uniquely identifiable unit of information. Messages are exchanged between local processes that run together for a given case until a certain objective has been achieved (e.g., the settlement of a specific transaction). If a message is exchanged between two processes, it is output from the sending process and input to the receiving process. Depending on its purpose, each message has a message format, or message type. Throughout the paper, the special symbols out and inp indicate the sending and receiving, respectively, of messages. It is convenient to combine these concepts in the following background sets, fixed for the rest of this paper. P is the universe of business processes; C is the universe of cases; Υ is the universe of messages; Υ×, ×\ out, inp\ is the universe of message events; ℳM is the universe of message types. Let e=(,)e=( m, x) be a message event with ∈Υ m∈ and ∈, x∈\ inp, out\. Then (e)= msg(e)= m is the message of e. If e=(,)e=( m, out), we refer to e as an output event (representing the sending of the message m) and if e=(,)e=( m, inp), it is an input event (representing the receipt of m). We use the following (complement) notation: ¯= inp= out and ¯= out= inp. Thus, ¯= inp= inp and ¯= out= out. Moreover, for ∈Υ m∈ and ∈, x∈\ inp, out\, we set (,)¯=(,¯) ( m, x)=( m, x). Messages involved in a cross-organisational process belong to a case and have a message type. Definition 1 Let ⊆ΥU be a set of messages. (1) A case function for U is a function f:→f:U . (2) A type function for U is a function f:→ℳf:U . ∎ Both case functions and type functions, and, in general, all functions defined for messages can be lifted to message events in the following way. Definition 2 Let Λ⊆Υ×, ×\ inp, out\ be a set of message events and let f:(Λ)→Df: msg( )→ D for some set D. Then the enhancement ⟨f⟩:(Λ)×,→D f : msg( )×\ inp, out\→ D of f is defined by ⟨f⟩(,)=f() f ( m, x)=f( m), for all ∈(Λ) m∈ msg( ) and ∈, x∈\ inp, out\. ∎ Thus, message events inherit type and case from their messages. As a consequence, given a message m and case function case and type function type both defined for m, we have that if e=(,)e=( m, x) with ∈Υ m∈ and ∈, x∈\ inp, out\, then e¯=(,¯) e=( m, x) and so ⟨⟩(e)=()=⟨⟩(e¯) type (e)= type( m)= type ( e) and ⟨⟩(e)=()=⟨⟩(e¯) case (e)= case( m)= case ( e). Other relevant attributes of a message event are the local process that executes that event and the local time stamp associated to its execution. Note that, since communications take place between different processes, message events e and e¯ e always belong to different processes. Moreover, no two different events executed by the same process (even if they belong to different cases) will have the same time stamp. Definition 3 Let Λ⊆Υ×, ×\ inp, out\. (1) A process function for Λ , is a function p:Λ→p: , such that p(e)≠p(e¯)p(e)≠ p( e), for all e∈Λe∈ , and p(Λ)p( ) is a finite set; (2) Let p be a process function for Λ . A local time function for p is a function t:Λ→ℕt: , such that, for all distinct e,e′∈Λe,e ∈ , t(e)≠t(e′)t(e)≠ t(e ) whenever p(e)=p(e′)p(e)=p(e ). ∎ We are now ready to define message logs as consisting of observations of communications, in the form of typed and time-stamped message events with an associated case, asynchronously exchanged over bilateral, unidirectional channels between a collection of local business processes. Definition 4 A message log is a pair =(Λ,)K=( , Att) such that (1) Λ⊆Υ×, ×\ inp, out\ is a set of message events such that e∈Λe∈ if and only if e¯∈Λ e∈ , and (2) =(⟨⟩,, Att=( case , proc, ,⟨⟩) time, type ) is tuple providing the attributes of K with case a case function for (Λ) msg( ), proc a process function for Λ , time a local time function for proc, and type a type function for (Λ) msg( ). ∎ Example 5 (Ex. 4 cont.) Figure 2 illustrates the exchange of messages to settle a transaction. There are two local processes, namely IF and CN. The downward pointing arrows represent the ordering of events along their local timelines. InvestmentFirmIF(1,)( m_1, out)(2,)( m_2, inp)CustodianCN(1,)( m_1, inp)(2,)( m_2, out)SISC Figure 2: OTC Settlement of transaction T1T1 Processes IF and CN exchange messages 1 m_1 (a Settlement Instruction) and 2 m_2 (a Settlement Confirmation). These exchanges are recorded in the message log =(Λ,)K=( , Att) with Λ=(1,),(1,),(2,),(2,) =\( m_1, out),( m_1, inp),( m_2, out),( m_2, inp)\ and =(⟨⟩, Att=( case , , proc, ,⟨⟩) time, type ). Let =,P=\ IF, CN\. The process function proc for Λ is defined by (1,)=(2,)= proc( m_1, out)= proc( m_2, inp)= IF and (1,) proc( m_1, inp) == (2,) proc( m_2, out) == CN. Let T1T1 be the identifier of this transaction. Then, (1)=(2)=T1 case( m_1)= case( m_2)=T1 and so we have ⟨⟩(e)=T1 case (e)=T1 for all message events e∈Λe∈ . The local time function time assigns time stamps such that (1,)<(2,) time( m_1, out)< time( m_2, inp) and (1,)<(2,) time( m_1, inp)< time( m_2, out). Finally, with (1)=SI type( m_1)=SI and (2)=SC type( m_2)=SC, we have ⟨⟩(1,)=SI type ( m_1, x)=SI and ⟨⟩(2,)=SC type ( m_2, x)=SC where ∈, x∈\ inp, out\. ∎ If =(Λ,(f1,f2,f3,f4))K=( ,(f_1,f_2,f_3,f_4)) is a message log, then (f2(e)∣e∈Λ) card(\f_2(e) e∈ \), the number of processes associated to K, is referred to as the dimension of K. Note that by Definition 3(1), f2(e)∣e∈Λ\f_2(e) e∈ \ is always a finite set. Moreover, by Definition 3(1) and Definition 4(1), if Λ≠∅ ≠ , then the dimension of K is always at least 22. In what follows, we identify the processes associated to the message events from a message log by an integer from [n][n], where n is the dimension of the message log. For the rest of this paper, =(Λ,)K=( , Att) is a fixed message log with Λ a non-empty set of message events and =(⟨⟩,,,⟨⟩) Att=( case , proc, time, type ) where case and type are a case function and a type function, respectively, for (Λ) msg( ). The dimension of K is n≥2n≥ 2 and (e)∣e∈Λ=[n]\ proc(e) e∈ \=[n]. 4 Structure of a message log In this section, we propose a relation to (partially) order the message events of message log K. This relation is then used to specify a finitary and prefix-closed language for K, that represents all sequences of message events defined by this partial order. Clearly, for each process of K, the time stamps defined by its local time function determine a total order on all message events of this process. Recall that we assume that whenever a message event e has an earlier (smaller) time stamp than another message event e′e belonging to the same process, then e′e does not causally precede e. In other words, the temporal order of two events from the same process as captured by its local time function, is either a necessary (causal) order determined by the (unknown) design of the process or a coincidental observation of their execution order. Note that for two events from the same process that belong to different cases, their allotted time stamps do not reflect a necessary ordering, as different cases are causally unrelated666This could have been formalised by having separate local time functions per case.. Thus, we only relate message events that belong to the same case and we do this by combining the temporal (process) orders with the send-receive relations between output events and their corresponding input events. Definition 5 The event relation of K is the relation R⊆Λ×ΛR_K\; × such that eRe′e\;R_K\;e if and only if (1) (e)=(e′) case(e)= case(e ), and (2) either (a) (e)=(e′) proc(e)= proc(e ) and (e)<(e′) time(e)< time(e ) or (b) e=(,)e=( m, out) and e′=(,)e =( m, inp) for some ∈(Λ) m∈ msg( ). ∎ Intuitively, the event relation of K captures for a given case an order of events that should be preserved in any global observation of its message events. However, as the following example shows, this relation is not necessarily acyclic. Example 6 Let =(Λ,)K=( , Att) be a message log with set of message events Λ= = (1,),(1,),(2,),(2,)\( m_1, out),( m_1, inp),( m_2, out),( m_2, inp)\ and its attributes defined by = Att= (⟨⟩,,,⟨⟩)( case , proc, time, type ). The process function proc is defined by (1,)=(2,)=P1 proc( m_1, inp)= proc( m_2, out)=P1 and (1,)=(2,)=P2 proc( m_1, out)= proc( m_2, inp)=P2. Note that P1≠P2P1≠ P2. Let time be such that (1,)=1 time( m_1, inp)=1, (2,)=2 time( m_2, out)=2, (2,)=1 time( m_2, inp)=1, and (1,)=2 time( m_1, out)=2. If (1)=(2) case( m_1)= case( m_2), then the event relation R_K of K defines a cycle, see Figure 6(a). P1P_1P2P_2(1,)( m_1, inp)(2,)( m_2, out)(2,)( m_2, inp)(1,)( m_1, out) (a) R_K P1P_1P2P_2(1,)( m_1, inp)(2,)( m_2, out)(2,)( m_2, inp)(1,)( m_1, out) (b) R′R_K Figure 3: (1,),(2,),(2,),(1,)( m_1, inp),( m_2, out),( m_2, inp),( m_1, out) form a cycle in R_K but not in R′R_K . However, if ′=(Λ,′)K =( , Att ) is a message log obtained from K by replacing case by a case function ′ case such that ′(1)≠′(2) case ( m_1)≠ case ( m_2), the event relation R′R_K is acyclic: ((1,),(2,))(( m_1, inp),( m_2, out)) and ((2,),(1,))(( m_2, inp),( m_1, out)) are not included in R′R_K , cf. Figure 6(b), even though (1,)<(2,) time( m_1, inp)< time( m_2, out) and (2,)<(1,) time( m_2, inp)< time( m_1, out). ∎ It is a straightforward observation that every non-empty cycle of R_K consisting of message events (which by definition all belong to the same case), contains an input event and an output event with the same underlying message. Consequently, cycles have an input event that precedes its corresponding output event, something which cannot happen in a message log that properly incorporates the execution order of its events. Hence Definition 6 K is sound if R_K is an acyclic relation. ∎ If R_K is acyclic, then its transitive closure R+R_K^+ is antisymmetric. By construction, R∗R_K^* is a transitive and reflexive relation. This leads to the following observation as a direct consequence of Definition 6. Lemma 3 R∗R_K^* is a partial order if and only if K is sound. ∎ For the rest of this paper, K is a sound message log. All message logs considered from here are assumed to be sound. Since K is fixed, the subscript K can be dropped from R∗R_K^*. To further simplify our notation, we write ⪯ instead of R∗R^*. So, from now on, we investigate the poset Λ=(Λ,⪯) po_ =( , ) defined by the sound message log =(Λ,)K=( , Att). In addition, given a subset C of Λ , we write C=(C,⪯C) po_C=(C, _C) for its induced sub-poset in (Λ,⪯)( , ). Next, we investigate the sequences of message events defined by Λ po_ that belong to the same case. Note that message events from different cases are not related in Λ po_ . As an initial, general, observation, we establish that every subset of Λ consisting of message events belonging to the same case, induces a partial order of which all linear extensions are well-founded. Lemma 4 Let C⊆ΛC be such that (e)=(e′) case(e)= case(e ), for all e,e′∈Ce,e ∈ C. Let =(C,⪯)∈(C) lo=(C, _ lo)∈ linext( po_C). Then lo is well-founded. Proof Let D⊆CD C be infinite (if C is finite, there is nothing to prove). Let, for all ℓ∈[n] ∈[n], Dℓ=e∈D∣(e)=ℓD_ =\e∈ D proc(e)= \ be the set of elements of D that belong to process ℓ . Recall that :→ℕ time:K→N is such that for all distinct message events e,e′e,e , (e)≠(e′) time(e)≠ time(e ) whenever (e)=(e′) proc(e)= proc(e ). Consequently, for all ℓ∈[n] ∈[n] and for every e∈Dℓe∈ D_ , there can be only finitely many e′∈Dℓe ∈ D_ such that (e′)<(e) time(e )< time(e) and hence e′⪯e _ loe (cf. Definition 5). Let ℓ∈[n] ∈[n]. Since ⪯ _ lo is a linear order on C, also its restriction to DℓD_ is a linear order. Hence, if DℓD_ is not empty, it has a unique minimal element w.r.t. ⪯ _ lo, which we denote by dℓd_ . Let us assume that none of the dℓd_ thus defined is minimal in D w.r.t. ⪯ _ lo. Hence, for all ℓ∈[n] ∈[n] and for all dℓd_ , there is an e∈De∈ D with e∉Dℓe ∈ D_ such that e⪯dℓe _ lod_ . It then follows from Definition 5 that all dℓd_ are input events. More precisely, for all ℓ∈[n] ∈[n], there exist an iℓ∈[n]i_ ∈[n] and an output event eℓ∈Diℓe_ ∈ D_i_ such that iℓ≠ℓi_ ≠ and eℓ=dℓ¯e_ = d_ . This implies that, for all ℓ∈[n] ∈[n], the minimal element diℓd_i_ of DiℓD_i_ precedes dℓd_ in lo since diℓ⪯eℓ⪯dℓd_i_ _ loe_ _ lod_ . Repeating the above argument leads to the conclusion, that - as we have only a finite number n of processes - there exists a cycle di⪯dj⪯did_i _ lod_j _ lod_i for some i,j∈[n]i,j∈[n]. This is in contradiction with lo being a partial order. Hence there must exist at least one ℓ∈[n] ∈[n] such that dℓd_ is minimal in D w.r.t. lo. We conclude that every nonempty subset of C has a minimal element w.r.t. ⪯ _ lo and so lo is well-founded. ∎ Since a partial order is well-founded if it has a linear extension that is well-founded (cf. Section 2), we have as an immediate corollary that C po_C is well-founded for every C⊆ΛC consisting of message events in C that all belong to the same case. Hence, by the definition of well-foundedness and because message events that belong to different cases are not ordered by ⪯ , every message event of K has a finite past. In what follows, we consider message events together with their past, i.e., all message events that precede them in Λ po_ . Thus, we are interested in sets of message events belonging to the same case together with their downward closure in Λ po_ . Definition 7 A conversation in K is a subset C⊆ΛC such that (1) (e)=(e′) case(e)= case(e ) for all e,e′∈Ce,e ∈ C, and (2) C is downward-closed in (Λ,⪯)( , ). ∎ Note that by Definition 5(1), all message events in the downward closure Λ(e) past_ po_ (e) of a message event e have the same case. Hence, requirements (1) and (2) in Definition 7 are independent. A conversation C captures (an initial part of) behaviour of the system for a certain case in the form of the partial order C po_C. By Lemma 4, all linear extensions of C po_C are well-founded. Since ⪯C=⋂⪯∣(C,⪯)∈(C _C\,= \ _ lo (C, _ lo)∈ linext( po_C\, cf. Section 2, we have (C) seq( po_C), comprising the sequences corresponding to the linear extensions of C po_C, as a full representation of the sequential behaviour captured by C. Since in the case of a finite conversation, all its elements appear in each of its sequences, the sets of sequences defined by different finite conversations are always disjoint. Lemma 5 Let C and C′C be finite conversations in K such that C≠C′C≠ C . Then (C)∩(C′)=∅ seq( po_C)∩ seq( po_C )= . ∎ However, as Λ may be infinite, conversations may be infinite as well. This implies that (C) seq( po_C) is not necessarily a finitary language. Therefore, we will now argue that we can restrict the representation of a system’s behaviour to finite conversations. First, we demonstrate that the sequences defined by the finite subconversations of a conversation C are exactly the (finite) prefixes of (C) seq( po_C). Lemma 6 Let C be a conversation in K. Let w∈Λ∗w∈ ^*. Then w∈((C))w∈ Pref( seq( po_C)) if and only if there exists a finite conversation C′⊆C C such that w∈(C′)w∈ seq( po_C ). Proof (only-if-direction) Assume that w∈((C))w∈ Pref( seq( po_C)). Let =(C,≤)∈(C) lo=(C, _ lo)∈ linext( po_C) be such that w∈(σ)w∈ pref( _ lo). Thus (w)⊆C alph(w) C. Let C′=(w)C = alph(w). We now set out to prove that C′C is a finite conversation in K and w=σ′w= _ lo for a linear extension ′ lo of C′=(C′,⪯C′) po_C =(C , _C ). Clearly, C′C is a finite set, as w is a finite prefix of σ _ lo. Since C is a conversation, (e)=(e′) case(e)= case(e ) for all e,e′∈C′⊆Ce,e ∈ C C. What remains to be shown is that C′C is downward-closed in (Λ,⪯)( , ). Since C is downward-closed, Λ(e)=C(e) past_ po_ (e)= past_ po_C(e) for all e∈Ce∈ C. Moreover, lo is well-founded by Lemma 4. Consequently, by Lemma 1, Λ(w(i))=C(w(i))=e∈Λ∣e⪯Cwi⊆w(1),…,w(i)⊆C′ past_ po_ (w(i))= past_ po_C(w(i))=\e∈ e _Cw_i\ \w(1),…,w(i)\ C for all i∈(w)i∈ dom(w). Hence, C′C is downward-closed in (Λ,⪯)( , ) thus a finite conversation in K. Consider now C′=(C′,⪯C′) po_C =(C , _C ) and define ⊑w=(w(i),w(j))∣i,j∈(w),i≤j _w=\(w(i),w(j)) i,j∈ dom(w),i≤ j\. Clearly, ⊑w _w is a linear order on C′C . Moreover, for all c,d∈C′c,d∈ C , we have c⊑wdc _wd if and only if c≤dc _ lod. Hence ⊑w=≤∩(C′×C′) _w= _ lo∩\;(C × C ). Thus, since lo is a linear extension of ⪯C _C, we have ⪯C′=⪯C∩(C′×C′)⊆≤∩(C′×C′)=⊑w _C \;=\; _C∩\;(C × C ) \; _ lo∩\;(C × C )=\; _w. Consequently, ′=(C′,⊑w)∈(C′) lo =(C , _w)∈ linext( po_C ). As it is easy to see that w=σ′w= _ lo , we are done. (if direction) Let C′⊆C C be a finite conversation in K such that w∈(C′)w∈ seq( po_C ). Let ′=(C′,≤′)∈(C′) lo =(C , _ lo )∈ linext( po_C ) be such that w=σlo′w= _lo . Consider ⊑C=≤′∪⪯C∪(c,d)∣c∈C′,d∈C∖C′ _C\;=\; _ lo ∪ _C∪\(c,d) c∈ C ,d∈ C C \, the relation over C capturing the linear order underlying w, combined with the partial order ⪯C _C induced by C, and extended in such a way that all message events in C′C precede all other message events in C. First, we establish that ⊑C _C is a partial order on C. Reflexivity of ⊑C _C follows immediately from the reflexivity of ⪯C _C. To establish transitivity of ⊑C _C, we first observe that there do not exist d∈C∖C′d∈ C C and e∈C′e∈ C such that d⊑Ced _Ce. Indeed, suppose to the contrary that d∈C∖C′d∈ C C and e∈C′e∈ C are such that d⊑Ced _Ce. Then by the definition of ⊑C _C it must be the case that d⪯Ced _Ce. However, C′C , as a conversation in Λ , is downward-closed in (,⪯)(K, ). Since (C,⪯C)(C, _C) is the sub-poset in (,⪯)(K, ) induced by C, C′C is also downward-closed in (C,⪯C)(C, _C). So, d∈C′d∈ C , a contradiction. Now, let a,b,c∈Ca,b,c∈ C be such that a⊑Cba _Cb and b⊑Ccb _Cc. Then, from the above it follows that if a∈C∖C′a∈ C C then also b∈C∖C′b∈ C C . Similarly, if b∈C∖C′b∈ C C then also c∈C∖C′c∈ C C . Furthermore, if a∈C′a∈ C and c∈C∖C′c∈ C C , then a⊑Cca _Cc by definition. Consequently, there are only two cases left to investigate, viz., a,b,c∈C′a,b,c∈ C and a,b,c∈C∖C′a,b,c∈ C C . In the former case, we first observe that ⪯C∩(C′×C′)⊆≤′ _C∩\;(C × C ) \; _ lo because ′ lo is a linear extension of C′ po_C and ⪯C′=⪯C∩(C′×C′) _C \;=\; _C∩\;(C × C ). Thus a⊑Cba _Cb and b⊑Ccb _Cc with a,b,c∈C′a,b,c∈ C together imply a≤′ba _ lo b and b≤′cb _ lo c. Then a≤′ca _ lo c by the transitivity of ≤′ _ lo , and so a⊑Cca _Cc. In the latter case, it follows from a⊑Cba _Cb and b⊑Ccb _Cc that a⪯Cba _Cb and b⪯Ccb _Cc. Hence by the transitivity of ⪯C _C, we have a⪯Cca _Cc and so a⊑Cca _Cc. To prove that ⊑C _C is antisymmetric, assume that we have a,b∈Ca,b∈ C such that a⊑Cba _Cb and b⊑Cab _Ca. If both a,b∈C′a,b∈ C , then a≤′ba _ lo b and b≤′ab _ lo a. Hence a=ba=b by the antisymmetry of ≤′ _ lo . Similarly, if both a,b∈C∖C′a,b∈ C C , then a⪯Cba _Cb and b⪯Cab _Ca, which implies that a=ba=b by the antisymmetry of ⪯C _C. If a∈C′a∈ C and b∈C∖C′b∈ C C , then it must be that b⪯Cab _Ca. Then, as above, since C′C is a conversation in K, it is downward-closed in (Λ,⪯)( , ) and thus also b∈C′b∈ C , a contradiction. Next, we consider a linear extension =(C,≤) lo=(C, _ lo) of (C,⊑C)(C, _C). Let v=σv= _ lo. We prove that w∈(v)w∈ pref(v). Suppose w∉(v)w ∈ pref(v). Let then i∈(w)i∈ dom(w) be such that w(j)=v(j)w(j)=v(j) for all j<ij<i, and w(i)≠v(i)w(i)≠ v(i). Let us assume first that v(i)∈C′v(i)∈ C . Then v(i)=w(k)v(i)=w(k) for some k>ik>i, and w(k)≤w(i)w(k) _ low(i). Since w(i)≤′w(k)w(i) _ lo w(k) also w(i)⊑Cw(k)w(i) _Cw(k) which implies that w(i)≤w(k)w(i) _ low(k) and thus w(i)=w(k)w(i)=w(k), a contradiction. Thus it must be the case that v(i)∈C∖C′v(i)∈ C C . Then w(i)⊑Cv(i)w(i) _Cv(i) by the definition of ⊑C _C. Furthermore, v(i)≤w(i)v(i) _ low(i) because v=σv= _ lo. Hence v(i)⊑Cw(i)v(i) _Cw(i). By the antisymmetry of ⊆C _C, v(i)=w(i)v(i)=w(i), again a contradiction. Therefore w∈(v)w∈ pref(v) and thus w∈(((C,⊑C)))w∈ Pref( seq((C, _C))). Since ⪯C⊆⊑C _C\; \; _C implies ((C,⊑C))⊆(C) linext((C, _C)) linext( po_C), it follows that w∈((C))w∈ Pref( seq( po_C)) which concludes the proof. ∎ It is interesting to observe here that every downward closed subset (‘prefix’) of a conversation is a subconversation of C. Conversely, any finite subconversation C′C of a conversation C is a prefix of C because it is downward closed. In other words, the finite subconversations of conversation C are its prefixes and by the above lemma, the prefixes of the sequences defined by C are the sequences defined by the prefixes of C. As an immediate consequence of Lemma 6 and Lemma 2, we have that for every infinite conversation, the infinitary language defined by its induced partial order, can be obtained as the limit of the union of the finitary languages defined by the partial orders induced by its finite subconversations. Theorem 4.1 Let C be an infinite conversation in K. Then (C)= seq( po_C)= (⋃(C′)∣C′ a finite subconversation of C) lim( \ seq( po_C ) C a finite subconversation of C\). ∎ Note that for every infinite conversation C, its language (C) seq( po_C) consists of infinite words only. On the other hand, for a finite conversation C′C , (C′) seq( po_C ) is a finite set comprising only finite words. By Theorem 4.1, all sequences defined by the linear extensions of an infinite conversation are approximated by the infinite set consisting of the finite sequences of the linear extensions of its finite subconversations. Thus, we can now define a finitary language for the message log K as the union of all languages of all its finite conversations (thus covering all cases). Definition 8 The event language of K is the set ()=⋃(C)∣C EL(K)= \ seq( po_C) C a finite conversation in a finite conversation in K\ comprising all sequences of message events defined by the linear extensions of the finite conversations in K. ∎ By Definition 8 and Lemma 6, () EL(K) is a finitary language consisting of all prefixes of all words from the languages defined by the partial orders of its conversations. This observation leads to Theorem 4.2 () EL(K) is a finitary, prefix-closed language. ∎ 5 Identifying actions in a message log To convert message log K into a global event log with an associated distributed communicating alphabet, message events have to be interpreted as executions of actions of local processes. In this section, we investigate how to consistently identify actions in a message log, leading to a labelling of events with action names that can be used to define a distributed communicating alphabet (Definition 22 in Appendix 0.D). Recall that =(Λ,)K=( , Att) with =(⟨⟩,,,⟨⟩) Att=( case , proc, time, type ). The number of processes (the dimension) of K is n≥2n≥ 2 and (e)∣e∈Λ=[n]\ proc(e) e∈ \=[n]. In what follows, we let Λi=e∈Λ∣(e)=i _i=\e∈ proc(e)=i\ where i∈[n]i∈[n], be the set of message events in Λ that belong to the i-th process. Note that, for all i∈[n]i∈[n], Λi≠∅ _i≠ because (e)∣e∈Λ=[n]\ proc(e) e∈ \=[n]. Let Λ=Λ∩(Υ×) _ out= \;∩\;( ×\ out\) and Λ=Λ∩(Υ×) _ inp= \;∩\;( ×\ inp\) be the set of output events and the set of input events of Λ , respectively. Since by Definition 4, e∈Λe∈ if and only if e¯∈Λ e∈ , we have Λ≠∅ _ out≠ and Λ≠∅ _ inp≠ . Thus, both Λ1,…,Λn\ _1,…, _n\ and Λ,Λ\ _ out, _ inp\ are partitions of Λ . Finally, we rephrase the complement notation introduced in Section 3, as a function: Definition 9 The message exchange function of Λ is the function :Λ→Λ mex: → defined by (e)=e¯ mex(e)= e, for all e∈Λe∈ . ∎ The function mex is clearly a complement function. It also preserves types. This follows from ⟨⟩((e))=⟨⟩(e¯)=((e¯))=((e))=⟨⟩(e) type ( mex(e))= type ( e)= type( msg( e))= type( msg(e))= type (e). Our aim is to associate a distributed communicating alphabet with K. So far, we have several entities defined by K which together closely resemble a DCA (cf. Definition 22), namely the sets Λ1,…,Λn _1,…, _n and Λ,Λ _ out, _ inp, with both [Λ1,…,Λn][ _1,…, _n] and [∅,Λ,Λ][ , _ out, _ inp] consisting of mutually disjoint sets such that ⋃i∈[n]Λi=Λ=Λ∪Λ _i∈[n] _i= = _ out∪ _ inp and for all i∈[n]i∈[n], Λi≠∅ _i≠ , as well as the functions ⟨⟩ type and mex. The function ⟨⟩ type assigns message types to message events and the complement function mex preserves message types. The tuple ([Λ1,…,Λn],[∅,Λinp,Λout],⟨⟩,)([ _1,…, _n],[ , _inp, _out], type , mex) is however not an n-DCA in case Λ is an infinite set. More fundamentally, message logs consist of unique message events rather than multiple occurrences of input or output actions. Thus we propose labelling functions to identify message events that represent different occurrences of the same action of a local process. These labelling functions should preserve the partitions defined by processes and input and output events. Furthermore, whenever events are identified by the labelling function, then so are their complements. Definition 10 An action function (for Λ ) is a function f:Λ→Df: → D with D a set of (action) labels, which satisfies the following two properties: Disjointness (DP): both f(Λi)∣i∈[n]\f( _i) i∈[n]\ and f(Λ),f(Λ)\f( _ inp),f( _ out)\ are partitions of f(Λ)f( ); Complement (CP): for all message events e,e′∈Λe,e ∈ , if f(e)=f(e′)f(e)=f(e ), then f((e))=f((e′))f( mex(e))=f( mex(e )). ∎ Example 7 Let =(Λ,)K=( , Att) be a message log, n≥2n≥ 2 its dimension, and f an action function for Λ . This function maps certain output events of process i to the action label s as depicted in Figure 4. We assume that (1,),( m_1, out), …,…, (ℓ,)( m_ , out) are all (here a finite number ℓ≥1 ≥ 1) output events of process i that are mapped to action label s. By the disjointness property (DP) of f, there are no message events belonging to another process that are also mapped to s. Now consider (1,),( m_1, inp), …,…, (ℓ,)( m_ , inp), the complements under mex of (1,),( m_1, out), …,…, (ℓ,)( m_ , out), respectively. By the complement property (CP) of f, each of (1,),( m_1, inp), … ,(ℓ,),( m_ , inp) is mapped to the same action label, here r. Moreover, again by DP, these input events all belong to the same process j with j≠ij≠ i. Thus, as depicted in Figure 4, actions s and r represent a communication channel between process i and process j with s representing the sending of an mim_i, i∈[ℓ]i∈[ ] and r representing the receiving of an mim_i, i∈[ℓ]i∈[ ]. Process i(m1,)(m_1, out)(mℓ,)(m_ , out)Process j(m1,)(m_1, inp)(mℓ,)(m_ , inp) mexsrffffffff Figure 4: Action function f. Note that one could also interpret the situation depicted in Figure 4 as resulting from a labelling of the messages 1, m_1, …,…, ℓ m_ by say a, which labelling is then lifted to the output events (1,),( m_1, out), …,…, (ℓ,)( m_ , out) as s (“send a” or (a,)( a, out)) and to the input events (1,),( m_1, inp), …,…, (ℓ,)( m_ , inp) as r (“receive a” or (a,)( a, inp)). ∎ As suggested in Example 7, another approach could be to start from a labelling of the messages and then lift this labelling to message events by a reference to their role as output or input event. This gives rise to the following definition. Definition 11 Let g:(Λ)→Dg: msg( )→ D where D is a set of (message) labels. Then the event extension g:Λ→D×,g_ e: → D×\ inp, out\ of g to message events, is defined by g((,))=(g(),)g_ e(( m, out))=(g( m), out) and g((,))=(g(),)g_ e(( m, inp))=(g( m), inp) for all ∈(Λ) m∈ msg( ). ∎ As our next result shows, a message labelling function defines through its event extension an action function, provided the message labels agree with the communication channels between the processes: two messages that get the same label should have the same sending and receiving processes. This is formalised in the next definition. Definition 12 (1) Let ∈(Λ) m∈ msg( ). Then the send/receive pair of m is ()=(((,)),((,))) sr( m)=( proc(( m, out)), proc(( m, inp))). (2) Let g:(Λ)→Dg: msg( )→ D for an alphabet D. Then g has the channel property if, for all ,′∈(Λ) m, m ∈ msg( ), g()=g(′)g( m)=g( m ) implies ()=(′) sr( m)= sr( m ). ∎ Theorem 5.1 Let g:(Λ)→Dg: msg( )→ D for some set D. Then g_ e is an action function if and only if g has the channel property. Proof (only if) Let ,′∈(Λ) m, m ∈ msg( ) be such that g()=g(′)g( m)=g( m ). It follows that g((,))=(g(),)=(g(′),)=g((′,))g_ e(( m, out))=(g( m), out)=(g( m ), out)=g_ e(( m , out)) and, similarly, that g(,)=g(′,)g_ e( m, inp)=g_ e( m , inp). Since g_ e is an action function, it satisfies DP, the disjointness property. Consequently, we have ((,))=((′,)) proc(( m, out))= proc(( m , out)) and ((,))=((′,)) proc(( m, inp))= proc(( m , inp)). Hence, ()=(′) sr( m)= sr( m ). We conclude that g has the channel property. (if) By assumption, g has the channel property. Firstly, we establish the disjointness property DP of g_ e. By definition, g(Λ)=g((Λ))×g_ e( _ inp)=g( msg( ))×\ inp\ and g(Λ)=g((Λ))×g_ e( _ out)=g( msg( ))×\ out\. Since Λ is not empty, neither Λ _ inp nor Λ _ out are. Hence, g(Λ),g(Λ)\g_ e( _ inp),g_ e( _ out)\ is a partition of g(Λ)g_ e( ). Moreover, since Λi∣i∈[n]\ _i i∈[n]\ is a partition of Λ , we have that ⋃i∈[n]g(Λi)=g(Λ) _i∈[n]g_ e( _i)=g_ e( ), and g(Λi)≠∅g_ e( _i)≠ , for all i∈[n]i∈[n]. What remains to be shown is that the g(Λi)g_ e( _i), i∈[n]i∈[n], are pairwise disjoint. So, assume that e,e′∈Λe,e ∈ are such that g(e)=g(e′)g_ e(e)=g_ e(e ). Thus either e and e′e are both output events or they are both input events. Moreover, g((e))=g((e′))g( msg(e))=g( msg(e )). Since g has the channel property, the latter implies that ((e))=((e′)) sr( msg(e))= sr( msg(e )). In other words, ((e),)=((e′),) proc( msg(e), out)= proc( msg(e ), out) and ((e),)=((e′),) proc( msg(e), inp)= proc( msg(e ), inp). Consequently, (e)=(e′) proc(e)= proc(e ). From this it follows that the g(Λi)g_ e( _i), i∈[n]i∈[n] are pairwise disjoint. We now turn to the complement property CP of g_ e. Assume g(e)=g(e′)g_ e(e)=g_ e(e ), for some e,e′∈Λe,e ∈ . By the definition of g_ e, either e and e′e are both output events or they are both input events. We set e=((e),)e=( msg(e), x) and e′=((e′),)e =( msg(e ), x) where ∈, x∈\ inp, out\. Moreover, g((e))=g((e′))g( msg(e))=g( msg(e )). It follows that g((e))=(g(((e))),¯)=(g((e)),¯)g_ e( mex(e))=(g( msg( mex(e))), x)=(g( msg(e)), x). Similarly, g((e′))=(g(((e′))),x¯)=(g((e′)),x¯)g_ e( mex(e ))=(g( msg( mex(e ))), x)=(g( msg(e )), x). Since g((e))=g((e′))g( msg(e))=g( msg(e )), we conclude that g((e))=g((e′))g_ e( mex(e))=g_ e( mex(e )), as required. ∎ Example 8 (Ex. 5 cont.) Consider a record of exchanges in the OTC settlement process in the form of message log ′=(Λ′,′)K =( , Att ) with Λ′=(i,),(i,)∣i∈[4] =\( m_i, out),( m_i, inp) i∈[4]\, ′=(⟨′⟩, Att =( case , ′, proc , ′,⟨′⟩) time , type ). We assume that there are two cases T1T1 and T2T2 such that ′(1)=′(2)=T1 case ( m_1)= case ( m_2)=T1 and ′(3)=′(4)=T2 case ( m_3)= case ( m_4)=T2. Messages m1m_1, m3m_3 are Settlement Instructions with ′(1)=′(3)=SI type ( m_1)= type ( m_3)=SI, while messages m2m_2, m4m_4 are Settlement Confirmations with ′(2)=′(4)=SC type ( m_2)= type ( m_4)=SC. Message events (1,),(2,)( m_1, out),( m_2, inp) and (3,),(4,)( m_3, out),( m_4, inp) belong to process IF and message events (1,),(2,)( m_1, inp),( m_2, out) and (3,),(4,)( m_3, inp),( m_4, out) to process CN, see Figure 5. Hence, we have the following send/receive pairs: (1)=(3)=(,) sr( m_1)= sr( m_3)=( IF, CN) and (2)=(4)=(,) sr( m_2)= sr( m_4)=( CN, IF). IFCN(m1,)(m_1, out)(m3,)(m_3, out)(m1,)(m_1, inp)(m3,)(m_3, inp)(si,out)(si,inp)α(m2,)(m_2, inp)(m4,)(m_4, inp)(m2,)(m_2, out)(m4,)(m_4, out)(sc,inp)(sc,out)α Figure 5: α=gα=g_ e is an action function. Let g:(Λ′)→si,scg: msg( )→\ si, sc\ be a message labelling function, where si and sc are message labels. It is defined by g(1)=g(3)=sig( m_1)=g( m_3)= si and g(2)=g(4)=scg( m_2)=g( m_4)= sc. Hence g has the channel property and g_ e, the event extension of g, is an action function, as can be seen in Figure 5. Indeed, g_ e satisfies (DP) because g(1,),(3,),(2,),(4,)g_ e\( m_1, out),( m_3, out),( m_2, inp),( m_4, inp)\ == (si,),(sc,)\( si, out),( sc, inp)\ is disjoint with g(1,),(3,),(2,),(4,)g_ e\( m_1, inp),( m_3, inp),( m_2, out),( m_4, out)\ == (si,),(sc,)\( si, inp),( sc, out)\. Furthermore, g(1,),(2,),(3,),(4,)g_ e\( m_1, out),( m_2, out),( m_3, inp),( m_4, out)\ == (si,),(sc,)\( si, out),( sc, out)\ and g(1,),(2,),(3,),(4,)g_ e\( m_1, inp),( m_2, inp),( m_3, inp),( m_4, inp)\ == (si,),(sc,)\( si, inp),( sc, inp)\ are disjoint sets. Hence, g_ e also satisfies (CP). ∎ Returning to the definition of action functions (Definition 10), we demonstrate how the complement property CP makes it possible to associate a complement function with each action function. Definition 13 Let f:Λ→Df: → D be a function that satisfies CP. Then the complement by f is the function f:f(Λ)→f(Λ) mex_f:f( )→ f( ), defined by f(f(e))=f((e)) mex_f(f(e))=f( mex(e)) for all e∈Λe∈ . ∎ That f mex_f is indeed a function whenever f satisfies CP, follows from the observation that whenever e,e′∈Λe,e ∈ are such that f(e)=f(e′)f(e)=f(e ), then f((e))=f((e′))f( mex(e))=f( mex(e )). Example 9 Consider the message log =(Λ,)K=( , Att) such that (1,)( m_1, out), (2,)( m_2, out), (1,)( m_1, inp), (2,)∈Λ( m_2, inp)∈ . Output events (1,)( m_1, out) and (2,)( m_2, out) belong to the same process, say P1P_1. Hence (1,)( m_1, inp) and (2,)( m_2, inp) also belong to a common process P2P_2 and P2≠P1P_2≠ P_1. Let α be an action function such that α((1,))=α((2,))=aα(( m_1, out))=α(( m_2, out))=a and α((1,))=α((2,))=bα(( m_1, inp))=α(( m_2, inp))=b. Then α(a)=α(((1,)))=α((1,))=b mex_α(a)=α( mex(( m_1, out)))=α(( m_1, inp))=b. Similarly, α(b)=a mex_α(b)=a. ∎ By the next lemma, f mex_f is a complement function if f is an action function. Lemma 7 Let f:Λ→Df: → D be a function that satisfies CP and such that f(Λ),f(Λ)\f( _ out),f( _ inp)\ is a partition of f(Λ)f( ). Then f mex_f is a complement function. Proof It follows from the definitions of mex and f mex_f that f(f(Λ))=f((Λ))=f(Λ) mex_f(f( _ out))=f( mex( _ out))=f( _ inp) and f(f(Λ))=f((Λ))=f(Λ) mex_f(f( _ inp))=f( mex( _ inp))=f( _ out). Moreover, f(f(f(e)))=f(f((e)))=f(((e))=f(e) mex_f( mex_f(f(e)))= mex_f(f( mex(e)))=f( mex( mex(e))=f(e) for all e∈Λe∈ . Thus f mex_f is a complement function. ∎ The following theorem shows how to associate a distributed communicating alphabet with K. Theorem 5.2 Let α:Λ→Dα: → D be an action function such that α(Λ)α( ) is a finite set. Let τ:α(Λ)→ℳτ:α( )→M be a function that assigns message types to labelled message events in such a way that τ(α((e)))=τ(α(e))τ(α( mex(e)))=τ(α(e)) for all e∈Λe∈ . Then (,α,τ)=([α(Λ1),…,α(Λn)],[∅,α(Λ),α(Λ)],τ,α)D\!A(K,α,τ)=([α( _1),…,α( _n)],[ ,α( _ out),α( _ inp)],τ, mex_α) is an n-DCA. Proof We verify the properties of an n-DCA as listed in Definition 22. (1) Since α, being an action function, satisfies the disjointness property (DP) and, moreover, α(Λ)α( ) is finite, we know that α(Λ1),…,α(Λn)α( _1),…,α( _n) are non-empty, pairwise disjoint and finite sets with α(Λ)=⋃i∈[n]α(Λi)α( )= _i∈[n]α( _i). (2) By the same arguments as above, α(Λ)α( _ inp) and α(Λ)α( _ out) are pairwise disjoint, finite sets such that ∅∪Σ∪Σ=α(Λ) ∪ _ inp∪ _ out=α( ). (3) ⋃i∈[n]α(Λi)=α(Λ)=∅∪Σ∪Σ _i∈[n]α( _i)=α( )= ∪ _ inp∪ _ out. (4) Function τ assigns a type to all elements of α(Λ)α( ). Note that whenever e,e′∈Λe,e ∈ are such that α(e)=α(e′)α(e)=α(e ), then α((e))=α((e′))α( mex(e))=α( mex(e )), because α satisfies CP. Hence, the condition that τ(α((e)))=τ(α(e))τ(α( mex(e)))=τ(α(e)) for all e∈Λe∈ , does not lead to inconsistencies. (5) We note that n≥2n≥ 2. (5.1) From Lemma 7 and its proof, we have that α mex_α is a complement function with α(α(Λ))=α(Λ) mex_α(α( _ out))=α( _ inp) and α(α(Λ))=α(Λ) mex_α(α( _ inp))=α( _ out). (5.2) That α(α(Λi))∩α(Λi)=∅ mex_α(α( _i))∩α( _i)= for all i∈[n]i∈[n] can be seen as follows. Assume, to the contrary, that α(α(d))=α(e) mex_α(α(d))=α(e) with d,e∈Λid,e∈ _i and i∈[n]i∈[n]. Hence, α((d))=α(e)α( mex(d))=α(e). By the definition of process function (cf. Definition 3(1)), d∈Λid∈ _i implies that (d)∉Λi mex(d) ∈ _i. Since α satisfies DP this implies that α((d))≠α(e)α( mex(d))≠α(e), a contradiction. (5.3) Finally, by the definition of α mex_α, τ(α(α(e)))=τ(α((e)))=τ(α(e))τ( mex_α(α(e)))=τ(α( mex(e)))=τ(α(e)) for all e∈Λe∈ . ∎ Note that in the statement of Theorem 5.2 we use the message types from ℳM also as types for actions. Moreover, the condition on τ is a minimal requirement in view of Definition 22(5.3). From Theorem 4.2, we know that () EL(K) is a finitary, prefix-closed language. Since α is an action function and thus maps every occurrence of a message event to a single action symbol, we have that for every word w∈Λ∗w∈ ^*, α(w)(i)=α(w(i))α(w)(i)=α(w(i)) for all i∈(w)i∈ dom(w). Consequently, when α is applied to () EL(K) the resulting language is also finitary and prefix-closed. Corollary 1 Let α:(Λ)→Dα: msg( )→ D be an action function. Then α(())α( EL(K)) is a finitary, prefix-closed language. ∎ So, we have a method to translate a message log into a finitary, prefix-closed language, i.e., a (global) event log, over a distributed communicating alphabet. In the next section, we investigate the structure of the labelled sequences comprising this event log. 6 The action language/event log of a message log It is convenient to fix here, for this section and the next, an action function, a type function, and an n-DCA, all as specified in the statement of Theorem 5.2. α:Λ→Dα: → D is an action function such that α(Λ)α( ) is a finite set; τ:α(Λ)→ℳτ:α( )→M is such that τ(α((e)))=τ(α(e))τ(α( mex(e)))=τ(α(e)) for all e∈Λe∈ ; and (,α,τ)D\!A(K,α,τ) is the n-DCA defined by K, α, and τ. As we will argue next, the causal structure of K as captured by Λ=(Λ,⪯) po_ =( , ) is preserved in α(())α( EL(K)). We start out by describing how in the words of α(())α( EL(K)), occurrences of input actions (elements from α(Λ)α( _ inp)) can be related to occurrences of their complementary output actions (elements from α(Λ)α( _ out)). Let us recall that the causality described by the event relation R_K of K (cf. Definition 5) requires that in every conversation, each input event is preceded by its corresponding output event. This leads, for their labelled occurrences in the words of α(())α( EL(K)), to the following observation. Lemma 8 Let w∈α(())w∈α( EL(K)), a∈α(Λ)a∈α( _ out). Then #a(w)≥#α(a)(w)\#_a(w)≥\#_ mex_α(a)(w). Proof Let u∈()u∈ EL(K) be such that w=α(u)w=α(u). If α(a) mex_α(a) does not occur in w, i.e., α(a)∉(w) mex_α(a) ∈ alph(w), then there is nothing to prove. So, let now i∈(w)i∈ dom(w) be such that w(i)=α(a)w(i)= mex_α(a). Hence u(i)=(,)u(i)=( m, inp) for some message m. Since K is a message log, (,)∈( m, inp) implies that also (,)∈( m, out) (cf. Definition 4). Moreover, (,)⪯(,)( m, out) ( m, inp) (cf. Definition 5). Let C be the unique finite conversation in Λ such that u∈(C)u∈ seq( po_C) (cf. Definition 8 and Lemma 5). Since ((,))=((,)) case(( m, inp))= case(( m, out)) and C is downward closed, it follows that (,)∈C( m, out)∈ C and hence (,)∈(u)( m, out)∈ alph(u). Let j∈[|u|]j∈[|u|] be such that u(j)=(,)u(j)=( m, out). Hence u(j)∈(u(i))u(j)∈ past(u(i)) and, by Lemma 1, j<ij<i. In other words (,)( m, out) precedes (,)( m, inp) in u. Moving back to w=α(u)w=α(u), we conclude that every occurrence of α(a) mex_α(a) as the image under α of a unique input event (,)( m, inp) has its own, unique, corresponding occurrence of α((,))=aα(( m, out))=a that precedes it in w, which proves the statement. ∎ By Corollary 1, the language α(())α( EL(K)) is prefix-closed. Hence it follows from Lemma 8 that every word in α(())α( EL(K)) has the prefix property with respect to α|α(Λ) mex_α|_α( _ out). We identify this function as follows. φ:α(Λ)→α(Λ) :α( _ out)→α( _ inp), the function defined by φ=α|α(Λ) = mex_α|_α( _ out), is the restriction of the complement function α mex_α to α(Λ)α( _ out). Note that φ:α(Λ)→α(Λ) :α( _ out)→α( _ inp) is a bijection. Theorem 6.1 α(())α( EL(K)) has the prefix property with respect to φ . ∎ In what follows, we may omit the reference to φ . Example 10 (Ex. 9 cont.) Assume that the message events (1,)( m_1, out), (2,)( m_2, out), (1,)( m_1, inp), and (2,)( m_2, inp) all belong to the same case. Furthermore, (1,)( m_1, out) precedes (2,)( m_2, out) in P1P_1 and (1,)( m_1, inp) precedes (2,)( m_2, inp) in P2P_2. Let C=(1,),(1,),(2,),(2,)C=\( m_1, out),( m_1, inp),( m_2, out),( m_2, inp)\. This C is a conversation in K with u=(1,)(2,)(1,)(2,)∈(C)u=( m_1, out)( m_2, out)( m_1, inp)( m_2, inp)∈ seq( po_C) and thus u∈()u∈ EL(K), see Figure 6(a). (a) Conversation C in K. (b) α(u)α(u) has the prefix property. Figure 6: Then α(u)=aabbα(u)=aabb as shown in Figure 6(b). Clearly, #b(v)≤#a(v)\#_b(v)≤\#_a(v) for all prefixes v of α(u)α(u). Hence, w=α(u)w=α(u) has the prefix property. ∎ As can be seen in Example 10, there is a clear relation between the occurrences of complementary message events in an event sequence, which is lacking in the labelled version. Assignment functions (introduced in [15]) explicitly relate the individual occurrences of input and output actions. Definition 14 Let w∈α(Λ)∗w∈α( )^* be a word with the prefix property. An assignment function (with respect to φ ) for w is an injective function θ:(w)∩(α(Λ)×ℕ)→(w)∩(α(Λ)×ℕ)θ: occ(w)∩(α( _ inp)×N)→ occ(w)∩(α( _ out)×N) with, for all (b,j)∈(w)(b,j)∈ occ(w) where b∈α(Λ)b∈α( _ inp): θ((b,j))=(α(b),i)∈(w)θ((b,j))=( mex_α(b),i)∈ occ(w) for some i such that w((α(b),i)) pos_w(( mex_α(b),i)) << w((b,j)) pos_w((b,j)). ∎ Assignment functions capture abstract channel policies as they define output/input relations through pairs of occurrences of complementary output and input actions. Example 11 (Ex. 10 cont.) Consider (w)=(a,1),(a,2), occ(w)=\(a,1),(a,2), (b,1),(b,2)(b,1),(b,2)\. Function θ1 _1 on (w) occ(w) is defined by θ1((b,1))=(a,2) _1((b,1))=(a,2) and θ1((b,2))=(a,1) _1((b,2))=(a,1). This function is an assignment function for w. As illustrated in Figure 7(a), it corresponds to a last-in-first-out (LIFO) channel policy. (a) θ1 _1 (b) θ2=θu,w,C _2= _u,w,C Figure 7: On the other hand, function θ2 _2 on (w) occ(w), defined by θ2((b,1))=(a,1) _2((b,1))=(a,1) and θ2((b,2))=(a,2) _2((b,2))=(a,2), specifies a first-in-first-out (FIFO) channel policy, see Figure 7(b). Another feature of θ2 _2 is that it preserves messages in the sense that (b,1)(b,1) and θ2((b,1)) _2((b,1)) have an underlying message event with the same message 1 m_1 and, similarly, (b,2)(b,2) and θ2((b,2)) _2((b,2)) have an underlying message event with the same message, in this case 2 m_2. Formally, u(w((b,1)))=(1,)u( pos_w((b,1)))=( m_1, inp) and u(w(θ2((b,1))))=(1,)u( pos_w( _2((b,1))))=( m_1, out) as well as u(w((b,2)))=(2,)u( pos_w((b,2)))=( m_2, inp) and u(w(θ2((b,2))))=(2,)u( pos_w( _2((b,2))))=( m_2, out). ∎ We now consider the labelled event sequences defined by a finite conversation in K. As we prove in the following lemma, all labelled event sequences of a single finite conversation have the same set of occurrences. Moreover, action functions are injective, when restricted to the event sequences of a single finite conversation.777Thus, if two distinct event sequences in () EL(K) yield the same action sequence, they must belong to different finite conversations in K; compare this with Lemma 5 by which no event sequence from ( EL(K) can belong to more than one conversation. Finally, the following lemma also shows that any finite conversation has essentially only one assignment function that preserves messages (as explained in Example 11). Lemma 9 Let u,u′∈(C)u,u ∈ seq( po_C) where C is a finite conversation in K. Let w=α(u)w=α(u) and w′=α(u′)w =α(u ). Then (1) (w)=(w′) occ(w)= occ(w ). (2) If w=w′w=w , then u=u′u=u . (3) If (b,j)∈(w)(b,j)∈ occ(w) is such that u(w((b,j)))=(,)u( pos_w((b,j)))=( m, inp) for some message m, then (,)∈(u)( m, out)∈ alph(u) and u((,))>u(,) pos_u(( m, inp))> pos_u( m, out). (4) If (b,j)∈(w)(b,j)∈ occ(w) is such that u(w((b,j)))=(,)u( pos_w((b,j)))=( m, inp) for some message m and i is such that u(w((α(b),i)))=(,)u( pos_w(( mex_α(b),i)))=( m, out), then also u(w′((b,j)))=(,)u( pos_w ((b,j)))=( m, inp) and u(w′((α(b),i)))=(,)u( pos_w (( mex_α(b),i)))=( m, out). Proof (1) Since both u and u′u are sequences defined by C po_C, (u)=C=(u′) alph(u)=C= alph(u ). Then (α(u))=(α(u′)) occ(α(u))= occ(α(u )) follows, as every element of C occurs exactly once in u and in u′u . (2) Assume α(u)=α(u′)α(u)=α(u ), but u≠u′u≠ u . Let i∈[|u|]i∈[|u|] be such that u(i)≠u′(i)u(i)≠ u (i) and u(j)=u′(j)u(j)=u (j) for all j∈[i−1]j∈[i-1]. Note that all message events that occur in u, occur only once. Similarly for those in u′u . Hence u(i),u′(i)∉u(1),…u(i−1)u(i),u (i) ∈\u(1),… u(i-1)\. Since α(u(i))=α(u′(i))α(u(i))=α(u (i)) and α is an action function, it follows from the disjointness property DP (Definition 10) that (u(i))=(u′(i)) proc(u(i))= proc(u (i)). Hence (u(i))≠(u′(i)) time(u(i))≠ time(u (i)). Thus, by the definition of ⪯C _C (cf. Definitions 5 and 7), either u(i)⪯Cu′(i)u(i) _Cu (i) or u′(i)⪯Cu(i)u (i) _Cu(i) in C po_C and so by Lemma 1, either u(i)u(i) is an element in the past of u′(i)u (i) or u′(i)u (i) is an element in the past of u(i)u(i). In other words, u(i)u(i) or u′(i)u (i) is an element of u(1),…,u(i−1)\u(1),…,u(i-1)\, a contradiction. (3) This follows from the observation that C is downward-closed in (Λ,⪯)( , ) and hence every input event in u is preceded by its corresponding output event. (4) Let (b,j)∈(w)(b,j)∈ occ(w) be such that u(w((b,j)))=(,)u( pos_w((b,j)))=( m, inp) for some message m. Hence by (2), (b,j)∈(w′)(b,j)∈ occ(w ). By the disjointness property DP of α (Definition 10), all message events x,x′∈Cx,x ∈ C such that α(x)=α(x′)α(x)=α(x ) belong to the same process and are thus linearly ordered by ⪯C _C. This implies that u(w′((b,j)))=(,)u( pos_w ((b,j)))=( m, inp). Since w,w′∈α(())w,w ∈α( EL(K)), we have from (3) that there are i,i′i,i such that u(w((α(b),i)))=(,)u( pos_w(( mex_α(b),i)))=( m, out) and u(w′((α(b),i′)))=(,)u( pos_w (( mex_α(b),i )))=( m, out). Again, by the disjointness property of α, i=i′i=i . ∎ We are now ready to show that any finite conversation C defines a single message preserving assignment function which moreover is shared by all message event sequences from (C) seq( po_C). Note that, by Lemma 9(1), (w)=(w′) occ(w)= occ(w ) for all w∈α((C))w∈α( seq( po_C)) for every finite conversation C in K. Therefore, we may write α(C) occ_α(C) to denote the set of all occurrences in any word from α((C))α( seq( po_C)). Definition 15 Let C be a finite conversation in K. Let u∈(C)u∈ seq( po_C) and w=α(u)w=α(u). Then θu,w,C:(w)∩(α(Λ)×ℕ)→(w)∩(α(Λ)×ℕ) _u,w,C: occ(w)∩(α( _ inp)×N)→ occ(w)∩(α( _ out)×N) is the (u,w)(u,w)-message preserving function for C if, for all (b,j)∈(w)(b,j)∈ occ(w) with b∈α(K)b∈α(K_ inp), θu,w,C((b,j))=(α(b),i) _u,w,C((b,j))=( mex_α(b),i) provided u(w((b,j)))=(,)u( pos_w((b,j)))=( m, inp) and i is such that u(w((α(b),i)))=(,)u( pos_w(( mex_α(b),i)))=( m, out). ∎ Let C be a finite conversation in K. Then, by Lemma 9(4), θu,w,C=θu′,w′,C _u,w,C= _u ,w ,C for all u,u′∈(C)u,u ∈ seq( po_C), w=α(u)w=α(u), and w′=α(u′)w =α(u ). We refer to this function as the message preserving function for C and denote it by θC _C. Example 12 (Ex. 11 cont.) Consider again w=α(u)=aabbw=α(u)=aabb with sequence u=(1,)(2,)(1,)(2,)∈(C)u=( m_1, out)( m_2, out)( m_1, inp)( m_2, inp)∈ seq( po_C), cf. Figure 7(b). Then function θu,w,C _u,w,C is defined by θu,w,C((b,1))=(a,1) _u,w,C((b,1))=(a,1) and θu,w,C((b,2))=(a,2) _u,w,C((b,2))=(a,2). Hence θu,w,C=θ2 _u,w,C= _2. Next, let u′=(1,)(1,)(2,)(2,)u =( m_1, out)( m_1, inp)( m_2, out)( m_2, inp). As can be seen in Figure 6(a), also u′∈(C)u ∈ seq( po_C) With w′=α(u′)=ababw =α(u )=abab, we then have θu′,w′,C(b,2)=(a,2) _u ,w ,C(b,2)=(a,2) and θu′,w′,C(b,1)=(a,1) _u ,w ,C(b,1)=(a,1), see Figure 8. Hence θu′,w′,C=θu,w,C=θC _u ,w ,C= _u,w,C= _C. ∎ u′u w′=α(u′)w =α(u )(m1,)(m_1, out)aα(m1,)(m_1, inp)bα(m2,)(m_2, out)aα(m2,)(m_2, inp)bα Figure 8: θu′,w′,C _u ,w ,C Lemma 10 Let C be a finite conversation in K and w∈α((C))w∈α( seq( po_C)). Then θC _C is an assignment function for w. Proof Firstly, we note that w has the prefix property (see Theorem 6.1). Let u∈(C)u∈ seq( po_C) be such that α(u)=wα(u)=w and consider (b,j)∈(w)(b,j)∈ occ(w) with u(w((b,i)))=(,)u( pos_w((b,i)))=( m, inp) for some message m. Recall that θC=θu,w,C _C= _u,w,C. Thus, by Definition 15, we have θC((b,j))=(α(b),i)∈(w) _C((b,j))=( mex_α(b),i)∈ occ(w) for some i such that u(w((α(b),i)))=(,)u( pos_w(( mex_α(b),i)))=( m, out). By Lemma 9(3), indeed (,)∈(u)( m, out)∈ alph(u) and u((,))<u((,)) pos_u(( m, out))< pos_u(( m, inp)). Since u((,))=w((b,j)) pos_u(( m, inp))= pos_w((b,j)) and u((,))=w((α(b),i)) pos_u(( m, out))= pos_w(( mex_α(b),i)), we have w((α(b),i))<w((b,j)) pos_w(( mex_α(b),i))< pos_w((b,j)). So, according to Definition 14, it follows that θC _C is an assignment function of w once we have established that θC _C injective. So, suppose that (b,j),(c,k)∈α(C)(b,j),(c,k)∈ occ_α(C) with b,c∈α(K)b,c∈α(K_ inp), are such that θC((b,j))=θC((c,k)) _C((b,j))= _C((c,k)). We observe that θC((b,j))=(α(b),i)=(α(c),ℓ)=θC((c,k)) _C((b,j))=( mex_α(b),i)=( mex_α(c), )= _C((c,k)), for certain i,ℓi, . Hence, i=ℓi= and α(b)=α(c) mex_α(b)= mex_α(c). The latter implies, by the complement property CP of α (cf. Definition 10), that b=cb=c. Let u(w(α(b),i))=(,)u( pos_w( mex_α(b),i))=( m, out). It follows from the definition of θC _C, that u(w((b,j)))=(,)=u(w((c,k)))u( pos_w((b,j)))=( m, inp)=u( pos_w((c,k))), Since u is an event sequence in which every message event occurs at most once, we have j=kj=k. Consequently, (b,j)=(c,k)(b,j)=(c,k) which shows that θC _C is an injective function. ∎ We are now ready to relate the common causality structure C=(C,⪯C) po_C=(C, _C) underlying all sequences of a finite conversation C in K, to structures associated with assignment functions for sequences in α((C))α( seq(C)). To do this, we use the following definition, originally from [15], which describes a relation on the occurrences in a word derived from an assignment function for that word. Definition 16 Let w∈α(())w∈α( EL(K)) and let θ be an assignment function for w. Let (a,j),(a′,j′)∈(w)(a,j),(a ,j )∈ occ(w) with a∈α(Λk)a∈α( _k) and a′∈α(Λℓ)a ∈α( _ ) for some k,ℓ∈[n]k, ∈[n]. Then (a,j)≤θ(a′,j′)(a,j) _θ(a ,j ) if either (1)(1) k=ℓk= and w((a,j))≤w((a′,j′)) pos_w((a,j))≤ pos_w((a ,j )) or (2)(2) k≠ℓk≠ , a′∈α(Λ)a ∈α( _ inp) and θ(a′,j′)=(a,j)θ(a ,j )=(a,j). ∎ Clearly, we have α(C)⊆≤θ Id_ occ_α(C) \; _θ for all assignment functions θ for w∈α((C))w∈α( seq( po_C)) with C a finite conversation. Moreover, by Lemma 5 in [15], the transitive closure ≤θ+≤^+_θ of ≤θ _θ is a partial order on α(C) occ_α(C). As the next lemma shows, the relation ≤θC _ _C defined by a message preserving function θC _C for a finite conversation C in K, can be seen as a transfer of R_K from C to α(C) occ_α(C). Lemma 11 Let C be a finite conversation in K. Let u∈(C)u∈ seq( po_C) and w=α(u)w=α(u). Let (a,j),(a′,j′)∈α(C)(a,j),(a ,j )∈ occ_α(C) be such that (a,j)≠(a′,j′)(a,j)≠(a ,j ). Then (a,j)≤θC(a′,j′)(a,j) _ _C(a ,j ) if and only if eRe′e\,R_K\,e where e=u(w((a,j)))e=u( pos_w((a,j))) and e′=u(w((a′,j′)))e =u( pos_w((a ,j ))). Proof By Lemma 10, θC _C is an assignment function for w. Note, furthermore, that a=α(e)a=α(e) and a′=α(e′)a =α(e ). Let k be such that e∈Λke∈ _k and let ℓ be such that e′∈Λℓe ∈ _ . We first consider the case that k=ℓk= . Then, (e)=(e′) proc(e)= proc(e ) which implies that (e)<(e′) time(e)< time(e ) or (e′)<(e) time(e )< time(e). From Definition 16, it follows that (a,j)≤θC(a′,j′)(a,j) _ _C(a ,j ) if and only if w((a,j))<w((a′,j′)) pos_w((a,j))< pos_w((a ,j )). Note that w((a,j))<w((a′,j′)) pos_w((a,j))< pos_w((a ,j )) if and only if e=u(w((a,j)))e=u( pos_w((a,j))) occurs in u before e′=u(w((a′,j′)))e =u( pos_w((a ,j ))) does. Finally, e occurs before e′e in u if and only if (e)<(e′) time(e)< time(e ) if and only if eRe′e\;R_K\;e . Next we assume that k≠ℓk≠ . Then we know from Definition 16, that (a,j)≤θC(a′,j′)(a,j) _ _C(a ,j ) if and only if a′∈α(Λ)a ∈α( _ inp) and θC((a′,j′))=(a,j) _C((a ,j ))=(a,j). By definition, θC((a′,j′))=(a,j) _C((a ,j ))=(a,j) if and only if e=u(w((a,j)))=(,)e=u( pos_w((a,j)))=( m, inp) and e′=u(w((a′,j′)))=(,)e =u( pos_w((a ,j )))=( m, out) for some message m, which by Definition 5 holds if and only if eRe′e\;R_K\;e . ∎ As an immediate consequence of Lemma 11, we have the result that the partial order ≤θC+≤^+_ _C is essentially the same as ⪯C _C. Theorem 6.2 Let C be a finite conversation in K and let w∈α((C))w∈α( seq( po_C)). Then (α(C),≤θC+)( occ_α(C),≤^+_ _C) and C=(C,⪯C) po_C=(C, _C) are isomorphic posets. ∎ Proof Let u∈(C)u∈ seq( po_C) be such that w=α(u)w=α(u). Define f:(w)→(u)f: occ(w)→ alph(u) by f(x)=u(w(x))f(x)=u( pos_w(x)) for all x∈(w)x∈ occ(w). This function is a bijection that relates every occurrence x∈(w)x∈ occ(w) to its underlying message event u(w(x))u( pos_w(x)). Thus, by Lemma 11, the partial orders ≤θC+≤^+_ _C and ⪯C _C are isomorphic. ∎ Theorem 6.2 specifically refers to the message preserving assignment functions associated with finite conversations. The following definition (adapted from [15]) introduces assignment functions based on the first-in-first-out policy as exemplified in Example 11. Definition 17 Let C be a finite conversation in K. The fifo-function for C, θC,:α(C)∩(α(Λ)×ℕ)→α(C)∩(α(Λ)×ℕ) _C, fifo: occ_α(C)∩(α( _ inp)×N)→ occ_α(C)∩(α( _ out)×N), is defined by θC,(b,j)=(α(b),j) _C, fifo(b,j)=( mex_α(b),j) for all (b,j)∈(w)(b,j)∈ occ(w) with b∈α(K)b∈α(K_ inp). ∎ Example 13 (Ex. 11 cont.) We recall that w=aabb=α(u)w=aabb=α(u) and that the assignment function θ2 _2 is defined by θ2((b,1))=(a,1) _2((b,1))=(a,1) and θ2((b,2))=(a,2) _2((b,2))=(a,2). As illustrated in Figure 7(b) and referred to in Example 11 this assignment function is the fifo-function for C. ∎ Because all sequences defined by finite conversations have the prefix property, it is immediately clear that every fifo-function is an assignment function. Lemma 12 Let C be a finite conversation in K and w∈α((C))w∈α( seq( po_C)). Then θC, _C, fifo is an assignment function for w. ∎ As argued in [15], fifo-functions are the least restrictive among the assignment functions. Here, we formulate this as follows. Lemma 13 Let C be a finite conversation in K and w∈α((C))w∈α( seq( po_C)). Let θ be an assignment function for w. Then ≤θC,+⊆≤θ+≤^+_ _C, fifo\; \;≤^+_θ. Proof We start from Definition 16. Let (a,j),(a′,j′)∈(w)(a,j),(a ,j )∈ occ(w) with a∈α(Λk)a∈α( _k) and a′∈α(Λℓ)a ∈α( _ ) for some k,ℓ∈[n]k, ∈[n], be such that (a,j)≤θw,(a′,j′)(a,j) _ _w, fifo(a ,j ). If k=ℓk= , then w((a,j))≤w((a′,j′)) pos_w((a,j))≤ pos_w((a ,j )) and hence also (a,j)≤θ(a′,j′)(a,j) _θ(a ,j ). Otherwise, k≠ℓk≠ and a′∈α(Λ)a ∈α( _ inp) with θC,(a′,j′)=(a,j) _C, fifo(a ,j )=(a,j). Thus j=j′j=j . Let θ(a′,j)=(a,i)θ(a ,j)=(a,i) for some i such that (a,i)∈(w)(a,i)∈ occ(w). There are two cases to consider. (1) i≥ji≥ j: In this case, (a,j)≤θ+(a,i)≤θ(a′,j)(a,j)≤^+_θ(a,i) _θ(a ,j) and so (a,j)≤θ+(a′,j)=(a′,j′)(a,j)≤^+_θ(a ,j)=(a ,j ). (2) i<ji<j: Since θ is an injective function on (w) occ(w), there are j′<j <j and i′≥ji ≥ j such that θ((a′,j′))=(a,i′)θ((a ,j ))=(a,i ). So, (a,j)≤θ+(a,i′)≤θ(a′,j′)≤θ+(a′,j)=(a′,j′)(a,j)≤^+_θ(a,i ) _θ(a ,j )≤^+_θ(a ,j)=(a ,j ). Thus, in all cases, (a,j)≤θC,(a′,j′)(a,j) _ _C, fifo(a ,j ) implies that (a,j)≤θ+(a′,j′)(a,j)≤^+_θ(a ,j ). Hence, ≤θC,+⊆≤θ+≤^+_ _C, fifo\; \;≤^+_θ. ∎ In other words, the partial order on the occurrences of a word w defined by a fifo-function, is the smallest of all partial orders defined by assignment functions for w. Consider, e.g., the assignment functions θ1 _1 and θ2 _2 from the Examples 11 and 13. Function θ2 _2 is a fifo-function. Moreover, (1,)( m_1, out) precedes (2,)( m_2, out) in P1P_1 and (1,)( m_1, inp) precedes (2,)( m_2, inp) in P2P_2. So, as can be seen in Figure 7, the partial order induced by θ2 _2 on the occurrences of w is less restrictive than the partial order induced by θ1 _1. In particular, θ2 _2 would allow to change in w, the order of the occurrences (a,2)(a,2) and (b,2)(b,2). This observation then leads to the last part of this section, where we consider the labelled sequences derived from the linear extensions of partial orders ≤θ+≤^+_θ defined by assignment functions θ. The following definition is from [15]. Definition 18 Let w∈α(())w∈α( EL(K)) and let θ be an assignment function for w. Then θ(w)=v∈α(Λ)∗∣(v)=(w) and ∀x,y∈(v):x≤θ+y⇒v(x)≤v(y) lin_θ(w)=\v∈α( )^* occ(v)= occ(w) and ∀ x,y∈ occ(v):x≤^+_θy pos_v(x)≤ pos_v(y)\ is the set of θ-linearisations of w. ∎ Note that Definition 18 describes θ-linearisations as sets of words, in contrast to linear extensions of partial orders which are linearly ordered sets. As a matter of fact, the θ-linearisations of w are labelled versions of the sequences in ((w),≤θC+) seq( occ(w),≤^+_ _C). Lemma 14 Let w∈α(())w∈α( EL(K)) and let θ be an assignment function for w. Then θ(w)=((((w),≤θ+))) lin_θ(w)= label( seq(( occ(w),≤^+_θ))), where :α(Λ)×(ℕ∖0)→α(Λ) label:α( )×(N \0\)→α( ) is defined by ((a,j))=a label((a,j))=a for all a∈α(Λ)a∈α( ) and j≥1j≥ 1. ∎ Combining Definition 18 with Lemma 13 leads immediately to the following observation. Lemma 15 Let C be a finite conversation in K and w∈α((C))w∈α( seq( po_C)). Let θ be an assignment function for w. Then θ(w)⊆θC,(w) lin_θ(w) lin_ _C, fifo(w) ∎ Example 14 Let ′=(Λ,′)K =( , Att ) be a message log with message events (1,)( m_1, out), (2,)( m_2, out), (1,)( m_1, inp), (2,)∈Λ( m_2, inp)∈ . Like in Example 9, the output events (1,)( m_1, out) and (2,)( m_2, out) belong to a process P1P_1 and the input events (1,)( m_1, inp) and (2,)( m_2, inp) to a second process P2P_2. Here, however, (1,)( m_1, out) precedes (2,)( m_2, out) in P1P_1 and (2,)( m_2, inp) precedes (1,)( m_1, inp) in P2P_2. So, C=(1,),(1,),(2,),(2,)C=\( m_1, out),( m_1, inp),( m_2, out),( m_2, inp)\ is a conversation in ′K , see Figure 9(a). Consider u=(1,)(2,)(2,)(1,)∈(C)u=( m_1, out)( m_2, out)( m_2, inp)( m_1, inp)∈ seq( po_C). (a) Conversation C in ′K . (b) (w)=(a,1),(a,2),(b,1),(b,2) occ(w)=\(a,1),(a,2),(b,1),(b,2)\. Figure 9: Now, action function α is defined such that α(1,)=α(2,)=aα( m_1, out)=α( m_2, out)=a and α(1,)=α(2,)=bα( m_1, inp)=α( m_2, inp)=b. As illustrated in Figure 9(b), we have α(u)=aabbα(u)=aabb and (w)=α(C)=(a,1),(a,2),(b,1),(b,2) occ(w)= occ_α(C)=\(a,1),(a,2),(b,1),(b,2)\. Hence, θC(b,1)=(a,2) _C(b,1)=(a,2) and θC(b,2)=(a,1) _C(b,2)=(a,1) where θC _C is the message preserving assignment function for C. This function differs from the fifo-function θC, _C, fifo which is defined by θC,(b,1)=(a,1) _C, fifo(b,1)=(a,1) and θC,(b,2)=(a,2) _C, fifo(b,2)=(a,2). The partial orders ≤θC2+≤^+_ _C_2 and ≤θC2,+≤^+_ _C_2, fifo are given in Figures 10(b,c). There we see that ≤θC+⊆≤θC,+≤^+_ _C\, \,≤^+_ _C, fifo. In fact, there are no other assignment functions for w than θC _C and θC, _C, fifo. (a,2)(a,2)(a,1)(a,1)(b,2)(b,2)(b,1)(b,1) (a) ≤θC2+≤^+_ _C_2 minus identity (a,2)(a,2)(a,1)(a,1)(b,2)(b,2)(b,1)(b,1) (b) ≤θC2,+≤^+_ _C_2, fifo minus identity Figure 10: ≤θC _ _C and ≤θC, _ _C, fifo are in bold. The set of θC _C-linearisations of w=aabbw=aabb comprises only w, since ≤θC+≤^+_ _C is a total order on (w) occ(w) which inhibits the swapping of occurrences in w. The set of θC, _C, fifo-linearisations of w consists of w and w′=ababw =abab. In this case, we can swap the second a and the first b, as (a,2)(a,2) and (b,1)(b,1) are not related by ≤θC,+≤^+_ _C, fifo. ∎ Wrapping up Lemmas 15, 14, and Theorem 6.2 yields: Theorem 6.3 Let C be a finite conversation in K and let w∈α((C))w∈α( seq( po_C)). Then, α((C))=θC(w)⊆θC,(w)α( seq( po_C))= lin_ _C(w) lin_ _C, fifo(w). ∎ Recall that the global event log α(())α( EL(K)) defined by the message log K is ⋃α((C))∣C a finite conversation in \α( seq( po_C)) C a finite conversation in K\;\. From the above we may thus conclude that, for every finite conversation C in K, the θC _C-linearisations of its sequences as defined by the message preserving assignment function θC _C are all in α(())α( EL(K)). Moreover, the causality between message events as described by C po_C is preserved by the translation from message log K to () EL(K) and event log α(())α( EL(K)). Corollary 2 α(())=α( EL(K))= ⋃linθC(w)∣C a finite conversation in and w∈α((C))⊆ \lin_ _C(w) C a finite conversation in K and w∈α( seq( po_C))\;\ ⋃linθC,(w)∣C a finite conversation in and w∈α((C)) \lin_ _C, fifo(w) C a finite conversation in K and w∈α( seq( po_C))\;\. ∎ 7 Conclusion In Sections 4 and 5, we have outlined a method to transform a message log of a distributed, cross-organisational process into a global event log over a distributed communicating alphabet. In particular, given message log K, action function α, and message type function τ, we thus obtain a message log α(())α( EL(K)) and an n-dimensional distributed communicating alphabet (,α,τ)D\!A(K,α,τ). Since α(())α( EL(K)) has the prefix property, the synthesis procedure proposed in [15] and outlined here in Appendix 0.D, can now be used. Given a process discovery algorithm A for a family L of languages, the following theorem is an immediate consequence of Theorem 5 from [15]. Theorem 7.1 If α(Λi)(α(()))∈ proj_α( _i)(α( EL(K))) , for all i∈[n]i∈[n], then α(())⊆ℒ(I(α(()),(,α,τ))α( EL(K)) (A_I(α( EL(K)),D\!A(K,α,τ)). ∎ However, the results in [15] also involve the fifo-linearisations of the words from global event log α(())α( EL(K)) because they are always included in the language of the I-net I(α(()),(,α,τ))A_I(α( EL(K)),D\!A(K,α,τ)). In general, the linearisations of a word, defined by an assignment function for that word, reflect the causality of its action occurrences induced by the channel policy captured by the given assignment function. As fifo-functions are oblivious to the identities of the messages exchanged, they are only concerned with occurrences of input/output actions. This is consistent with the causality and concurrency in the communicating behaviour of I-nets in terms of the occurrences of input and output transitions (actions in α(())α( EL(K))) meaning that independent occurrences of such transitions will not be ordered and can be swapped. Thus, by Corollary 4 in [15], we have the following corollary of Theorem 7.1 and Corollary 2. Corollary 3 If α(Λi)(α(()))∈ proj_α( _i)(α( EL(K))) , for all i∈[n]i∈[n], then α(())⊆α( EL(K)) ⋃linθC,(w)∣C a finite conversation in and w∈α((C))⊆ℒ(I(α(()),(,α,τ)) \lin_ _C, fifo(w) C a finite conversation in K and w∈α( seq( po_C))\;\ \\ L(A_I(α( EL(K)),D\!A(K,α,τ)). ∎ Finally, the inclusions in this corollary are equalities if two conditions are satisfied: (1) the fifo-function is message preserving and (2) α(())α( EL(K)) is complete with respect to the discovered I-net (see Appendix 0.D and Definition 9 in [15]). Theorem 7.2 If α(Λi)(α(()))∈ proj_α( _i)(α( EL(K))) , for all i∈[n]i∈[n], then α(())=ℒ(I(α(),(,α)))α( EL(K))=L(A_I(α( L_K),D\!A(K,α))), provided θC=θC, _C= _C, fifo for all finite conversations C in K and α(()))α( EL(K))) is complete with respect to I(α(()),(,α,τ))A_I(α( EL(K)),D\!A(K,α,τ)). ∎ 8 Discussion The main aim of this paper was to show how the communicating behaviour of a cross-organisational process in the form of a global event log over a distributed communicating alphabet, can be inferred from a message log, i.e., observations of message exchanges between component business processes. This should be done in such a way that the derived behaviour faithfully represents the relations between the communications as recorded in the message log. This made it possible to apply the results from [15]. So, existing algorithms for the discovery of Petri net models of local business processes that can be leveraged to the discovery of Petri net models of cross-organisational processes from global event logs, can now also be used to discover Industry nets from message logs. In [15] and in this paper as well, a global event log is understood as a prefix-closed, finitary language consisting of sequences of executed actions. However, being based on message logs, the sequences in the global event logs in this paper have no occurrences of internal actions. Since global event logs are in general infinite finitary languages, message logs are not a priori required to be finite. As a consequence, also conversations may be infinite sets. Such conversations define infinitary languages, which by Theorem 4.1 are fully described by the limits of their finite prefixes. In fact, by Lemma 6, the words defined by the finite subconversations of any infinite conversation are exactly the finite prefixes of its infinite sequences. Hence, our focus was on finite conversations and the prefix-closed, finitary languages defined by them. Next, message events had to be interpreted as executions of (output or input) actions of local processes, reflecting the idea that a single action may communicate many messages during a run (conversation) of the system. Moreover, our system models (Enterprise nets and Industry nets) are finitely specified and so are the distributed communicating alphabets associated with the global event logs. This led to the concept of an action function describing how to consistently label message events with finitely many different action names. The types of the message events had to be lifted to the level of action names in the distributed alphabet in such a way that the action labels of complementary message events have the same type. In other words, complementary actions should have the same type exactly what is required by the definition of a distributed communicating alphabet. Finally, note that – whereas the process function of the message log is explicitly represented in the distributed communicating alphabet – the case and time function are used to define its event language via the partial orders defined by the conversations. The results from [15] show how the global event log derived from a message log can be used to discover an Industry net the language of which includes the global event log (Theorem 7.1). Following [15], we then turned to assignment functions to further investigate this inclusion. Assignment functions relate occurrences of input and output actions in a sequence and thus induce a partial order on these occurrences. They can be seen as channel policies describing the order in which sent messages were received. In case of global event logs derived from message logs, message preserving assignment functions can be defined on basis of the underlying message events. Only these message preserving assignment functions (shared by all sequences that belong to the same conversation) preserve the order of sending at the receiving end. By Theorem 6.2, the partial order on the action occurrences defined by a message preserving assignment function associated with a conversation, coincides with the partial order of that conversation. However, in general, global event logs are more abstract and know only occurrences of actions. As a consequence, the causality between input and output actions cannot be based on the identities of the messages exchanged. In its least restrictive form, this causality is expressed through the prefix property as captured by fifo-functions. This explains why the linearisations defined by message preserving assignment functions are included in the linearisations defined by first-in-first-out functions (cf. Corollary 3). To conclude, as illustrated in this paper, the translation of communication (message exchanges) into global event logs makes it possible to extend established local process mining methods and techniques to the level of collaborating organisations. We consider this as a useful step towards overcoming this challenge from [25]. It would be interesting to investigate if this technique based on channel policies and (labelled) partial orders could also be useful in other settings. Acknowledgments We are grateful to Hendrik Jan Hoogeboom for his comments on a preliminary version of this paper and for his invaluable assistance with the figures. References [1] W. M. P. v. d. Aalst, M. Dumas, C. Ouyang, A. Rozinat, and E. Verbeek (2008) Conformance checking of service behavior. ACM Trans. Internet Technol. 8 (3), p. 1–30. External Links: Link, Document Cited by: §1. [2] A. Augusto, R. Conforti, M. Dumas, M. L. Rosa, F. M. Maggi, A. Marrella, M. Mecella, and A. Soo (2019) Automated discovery of process models from event logs: review and benchmark. IEEE Trans. Knowl. Data Eng. 31 (4), p. 686–705. External Links: Link, Document Cited by: §1. [3] J. Benzin and S. Rinderle-Ma (2023) Petri net classes for collaboration mining: assessment and design guidelines. In Process Mining Workshops - ICPM 2023 International Workshops, Rome, Italy, October 23-27, 2023, Revised Selected Papers, J. D. Smedt and P. Soffer (Eds.), Lecture Notes in Business Information Processing, p. 449–461. External Links: Link, Document Cited by: §1, §1. [4] J. Benzin and S. Rinderle-Ma (2024) Towards standardized modeling of collaboration processes in collaboration process discovery. In Process Mining Workshops - ICPM 2024 International Workshops, Lyngby, Denmark, October 14-18, 2024, Revised Selected Papers, A. Delgado and T. Slaats (Eds.), Lecture Notes in Business Information Processing, Vol. 533, p. 171–183. External Links: Link, Document Cited by: §1. [5] R. G. Downey, D. R. Hirschfeldt, S. Lempp, and R. Solomon (2003) Computability-theoretic and proof-theoretic aspects of partial and linear orderings. Israel Journal of Mathematics 138, p. 271–290. External Links: Link, Document Cited by: §2. [6] R. Engel, R. P. J. C. Bose, C. Pichler, M. Zapletal, and H. Werthner (2013) EDIminer: A toolset for process mining from EDI messages. In Proceedings of the CAiSE’13 Forum at the 25th International Conference on Advanced Information Systems Engineering (CAiSE), Valencia, Spain, June 20th, 2013, R. Deneckère and H. A. Proper (Eds.), CEUR Workshop Proceedings, Vol. 998, p. 146–153. External Links: Link Cited by: §1. [7] R. Engel, W. Krathu, M. Zapletal, C. Pichler, R. P. J. C. Bose, W. M. P. van der Aalst, H. Werthner, and C. Huemer (2016) Analyzing inter-organizational business processes - process mining and business performance analysis using electronic data interchange messages. Inf. Syst. E Bus. Manag. 14 (3), p. 577–612. External Links: Link, Document Cited by: §1, §1. [8] R. Engel, W. Krathu, M. Zapletal, C. Pichler, W. M. P. van der Aalst, and H. Werthner (2011) Process mining for electronic data interchange. In E-Commerce and Web Technologies - 12th International Conference, EC-Web 2011, Toulouse, France, August 30 - September 1, 2011. Proceedings, C. Huemer and T. Setzer (Eds.), Lecture Notes in Business Information Processing, Vol. 85, p. 77–88. External Links: Link, Document Cited by: §1. [9] R. Engel, W. M. P. van der Aalst, M. Zapletal, C. Pichler, and H. Werthner (2012) Mining inter-organizational business process models from EDI messages: A case study from the automotive sector. In Advanced Information Systems Engineering - 24th International Conference, CAiSE 2012, Gdansk, Poland, June 25-29, 2012. Proceedings, J. Ralyté, X. Franch, S. Brinkkemper, and S. Wrycza (Eds.), Lecture Notes in Computer Science, Vol. 7328, p. 222–237. External Links: Link, Document Cited by: §1. [10] J. Engelfriet and H. J. Hoogeboom (1993) X-automata on omega-words. Theor. Comput. Sci. 110 (1), p. 1–51. External Links: Link, Document Cited by: §2. [11] K. Jensen, W. M. P. van der Aalst, G. Balbo, M. Koutny, and K. Wolf (Eds.) (2013) Transactions on petri nets and other models of concurrency VII. Lecture Notes in Computer Science, Vol. 7480, Springer. External Links: Link, Document, ISBN 978-3-642-38142-3 Cited by: §1. [12] F. Kordon, L. Petrucci, J. Desel, J. Kleijn, M. Koutny, and Ł. Mikulski (Eds.) (2026 TO APPEAR.) 6th advanced course on petri nets. Lecture Notes in Computer Science, Vol. 16260, Springer. External Links: Link, Document, ISBN Cited by: §1. [13] P. M. Kwantes and J. Kleijn (2018) On the synthesis of industry level process models from enterprise level process models. In International Workshop on Algorithms & Theories for the Analysis of Event Data (ATAED), CEUR Workshop Proceedings, Vol. 2115, p. 6–22. Cited by: Appendix 0.C, §1. [14] P. M. Kwantes and J. Kleijn (2020) On discovering distributed process models - the case of asynchronous communication. In International Workshop on Algorithms & Theories for the Analysis of Event Data (ATAED), CEUR Workshop Proceedings, Vol. 2625, p. 49–65. Cited by: §1, §1. [15] P. M. Kwantes and J. Kleijn (2022) Distributed synthesis of asynchronously communicating distributed process models. Trans. Petri Nets Other Model. Concurr. 16, p. 49–72. External Links: Link, Document Cited by: Appendix 0.D, Appendix 0.D, Appendix 0.D, Appendix 0.D, §1, §1, §1, §2, §6, §6, §6, §6, §6, §6, §7, §7, §7, §7, §8, §8, §8. [16] J. Mendling, S. J. J. Leemans, B. F. van Dongen, and H. A. Reijers (Eds.) (2026) Mining a scientist’s process - essays dedicated to wil van der aalst on the occasion of his 60th birthday. Lecture Notes in Computer Science, Vol. 16480, Springer. External Links: Link, Document, ISBN 978-3-032-17617-2 Cited by: §1, §1. [17] J. Mendling, B. T. Pentland, and J. Recker (2020) Building a complementary agenda for business process management and digital innovation. Eur. J. Inf. Syst. 29 (3), p. 208–219. External Links: Link, Document Cited by: §1. [18] W. Reisig and G. Rozenberg (Eds.) (1998) Lectures on petri nets I: basic models, advances in petri nets 1996. Lecture Notes in Computer Science, Vol. 1491, Springer. External Links: Link, Document, ISBN 3-540-65306-6 Cited by: §1. [19] W. Reisig and G. Rozenberg (Eds.) (1998) Lectures on petri nets I: applications, advances in petri nets 1996. Lecture Notes in Computer Science, Vol. 1492, Springer. External Links: Link, Document, ISBN 3-540-65307-4 Cited by: §1. [20] J. Rott, M. Böhm, and H. Krcmar (2024) Laying the ground for future cross-organizational process mining research and application: a literature review. Business Process Management Journal 30 (8), p. 144–206. External Links: Link, Document Cited by: §1, §1. [21] L. Staiger (1997) ω-languages. In Handbook of Formal Languages, Volume 3: Beyond Words, G. Rozenberg and A. Salomaa (Eds.), p. 339–387. External Links: Link, Document Cited by: §2. [22] E. Szpilrajn (1930) Sur l’extension de l’ordre partiel. Fundamenta Mathematicae 16, p. 386 –389. External Links: Link, Document Cited by: §2. [23] M. Thiede, D. Fuerstenau, and A. P. Bezerra Barquet (2018) How is process mining technology used by organizations? A systematic literature review of empirical studies. Business Process Management Journal 24 (4), p. 900–922. External Links: Link, Document Cited by: §1. [24] W. M. P. van der Aalst and J. Carmona (Eds.) (2022) Process mining handbook. Lecture Notes in Business Information Processing, Vol. 448, Springer. External Links: Link, Document, ISBN 978-3-031-08847-6 Cited by: §1. [25] W. M. P. van der Aalst and et al (2011) Process mining manifesto. In Business Process Management Workshops - BPM 2011 International Workshops, Clermont-Ferrand, France, August 29, 2011, Revised Selected Papers, Part I, F. Daniel, K. Barkaoui, and S. Dustdar (Eds.), Lecture Notes in Business Information Processing, Vol. 85, p. 169–194. External Links: Link, Document Cited by: §1, §1, §8. [26] W. M. P. van der Aalst and C. Stahl (2011) Modeling business processes - A petri net-oriented approach. Cooperative Information Systems series, MIT Press. External Links: Link, ISBN 978-0-262-01538-7 Cited by: §1. [27] W. M. P. van der Aalst and H. M. W. Verbeek (2008) Process mining in web services: the websphere case. IEEE Data Eng. Bull. 31 (3), p. 45–48. External Links: Link Cited by: §1. [28] W. M. P. van der Aalst (1997) Verification of workflow nets. In Application and Theory of Petri Nets 1997, 18th International Conference, ICATPN ’97, Toulouse, France, June 23-27, 1997, Proceedings, P. Azéma and G. Balbo (Eds.), Lecture Notes in Computer Science, p. 407–426. External Links: Link, Document Cited by: §1. [29] W. M. P. van der Aalst (1998) The application of Petri nets to workflow management. J. Circuits Syst. Comput. 8 (1), p. 21–66. External Links: Link, Document Cited by: §1. [30] W. M. P. van der Aalst (2016) Process mining - data science in action, second edition. Springer. External Links: Link, Document, ISBN 978-3-662-49850-7 Cited by: §1. Appendix Appendix 0.A Proof of Lemma 2 Lemma 2 Let =(A,≤A) po=(A, _A) be a well-founded, partial order with A an infinite set. Then ()=((())) seq( po)= lim( Pref( seq( po))). Proof The inclusion of () seq( po) in ((())) lim( Pref( seq( po))) follows from our earlier observation that L⊆lim((L))L ( pref(L)) for all infinitary languages L. To prove the converse, consider a w∈((())w∈ lim( Pref( seq( po)). Since po is well-founded and A is infinite, such w∈Aωw∈ A^ω exists. Moreover, w[i]∈(())w[i]∈ Pref( seq( po)) for infinitely many i. This implies that w[i]∈(())w[i]∈ Pref( seq( po)) for all i∈ℕi∈N. Let D=d∈A∣d∉(w)D=\d∈ A d ∈ alph(w)\ comprise all elements of A that do not occur in w. Let D=(D,≤D) po_D=(D, _D) be the sub-poset of po induced by D and let (D,⪯D)∈(D,≤D)(D, _D)∈ linext(D, _D) be a linear extension of D po_D. We set ⪯=≤A∪⪯D∪(w(i),w(j))∣1≤i≤j∪(w(i),d)∣i≥1 and d∈D \;=\; _A\;∪\; _D∪\;\(w(i),w(j)) 1≤ i≤ j\∪\(w(i),d) i≥ 1 and d∈ D\. We first argue that there exist no a∈Da∈ D and b∈A∖Db∈ A D with a≤Aba _Ab. (*) This can be seen as follows. Assume to the contrary that a∈Da∈ D and b∈A∖Db∈ A D are such that a≤Aba _Ab. Thus b=w(j)b=w(j) for some j≥1j≥ 1. Since w[j]∈(())w[j]∈ Pref( seq( po)), it follows that (w(j))=c∈A∣c≤Aw(j)⊆w(1),…w(j) past_ po(w(j))=\c∈ A c _Aw(j)\ \w(1),… w(j)\ (see Lemma 1) which implies that a=w(i)a=w(i) for some i≤ji≤ j, in contradiction with a∈Da∈ D. Thus such a,ba,b do not exist. Next we prove that (A,⪯)∈()(A, )∈ linext( po). By definition, ≤A⊆⪯ _A\; \; . In addition, clearly, a⪯ba b or b⪯ab a for all a,b∈Aa,b∈ A. Hence, what remains to be shown is that ⪯ is a partial order on A. Since ≤A⊆⪯ _A\; \; , we immediately have that ⪯ is reflexive. To prove that ⪯ is antisymetric, let a,b∈Aa,b∈ A be such that a⪯ba b and b⪯ab a. Let a,b∈Da,b∈ D. Then, as ⪯D _D is total, we may assume without loss of generality that a⪯Dba _Db. There are two possible cases. If b⪯Dab _Da, then a=ba=b by the antisymmetry of ⪯D _D. And if b≤Aab _Aa, then also b⪯Dab _Da since ⪯D _D is a linear extension of the sub-poset of (A,≤A)(A, _A) induced by D. Thus, again a=ba=b by the antisymmetry of ⪯D _D. If both a,b∈A∖Da,b∈ A D, then a=w(i)a=w(i) and b=w(j)b=w(j) for some i,j≥1i,j≥ 1. Assume without loss of generality that i≤ji≤ j. Since w[j]∈(())w[j]∈ Pref( seq( po)), the pair (w(i),w(j))(w(i),w(j)) thus belongs to at least one linear extension of ≤A _A. On the other hand, if wj≤Awiw_j _Aw_i the pair (w(j),w(i))(w(j),w(i)) belongs to all linear extensions of ≤A _A. It follows that i=ji=j and thus a=ba=b. Finally, if a∈Da∈ D and b∈A∖Db∈ A D, then a⪯ba b implies a≤Aba _Ab in contradiction with (*) above. So we are done. To prove the transitivity of ⪯ , consider a,b,c∈Aa,b,c∈ A such that a⪯ba b and b⪯cb c. If a∈A∖Da∈ A D and c∈Dc∈ D, then a⪯ca c by definition. Moreover, by (*) above, the only remaining relevant cases are that a,b,c∈A∖Da,b,c∈ A D and either (1) (a,b)∈≤A(a,b)∈\; _A and (b,c)∉≤A(b,c) ∈\; _A or, conversely, (2) (a,b)∉≤A(a,b) ∈\; _A and (b,c)∈≤A(b,c)∈\; _A. In all other situations, transitivity follows from the transitivity of the four relations constituting ⪯ and their combinations. Now, let i,j,k≥1i,j,k≥ 1 be such that w(i)=aw(i)=a, w(j)=bw(j)=b, and w(k)=cw(k)=c. wj∈(w(k))⊆w(1),…,w(k)w_j∈ past(w(k)) \w(1),…,w(k)\. If (1) holds, then w(i)≤Aw(j)w(i) _Aw(j) with w[j]∈(())w[j]∈ Pref( seq( po)). Hence, by Lemma 1, w(i)∈(w(j))⊆w(1),…,w(j)w(i)∈ past(w(j)) \w(1),…,w(j)\ and so i≤ji≤ j. Moreover, w(j)=b⪯c=w(k)w(j)=b c=w(k) and so j≤kj≤ k. Hence i≤j≤ki≤ j≤ k and a=w(i)⪯w(k)=ca=w(i) w(k)=c follows. If (2) holds, a similar reasoning can be used to argue that a⪯ca c. We conclude by showing that w=σw= _ lo where =(A,⪯) lo=(A, ). From (*) and the definition of ⪯ , we have that w(1)w(1) is the unique minimal element of lo. Now, consider any pair w(i),w(i+1)w(i),w(i+1) where i≥1i≥ 1, and assume that w(i)⪯a⪯w(i+1)w(i) a w(i+1) for some a∈Aa∈ A. From (*) it follows that a∉Da ∈ D. So there exists j≥1j≥ 1 such that a=w(j)a=w(j). Since ⪯ is a linear order, it must be that j=ij=i or j=i+1j=i+1 and we are done. Hence, for all i∈(w)i∈ dom(w), w(i)w(i) is the direct predecessor of w(i+1)w(i+1) in lo. We conclude that w=σw= _ lo and thus w∈()w∈ seq( po). ∎ Appendix 0.B Petri nets A Petri net is a triple N=(P,T,F)N=(P,T,F), where P is a finite set of places, T is a finite, non-empty set888T is an alphabet. of transitions, P∩T=∅P∩ T= , and F⊆(P×T)∪(T×P)F (P× T)∪(T× P) is a set of arcs. Let N=(P,T,F)N=(P,T,F) be a Petri net. A marking of N is a function μ:P→ℕμ:P that assigns μ(p)μ(p) tokens to each place p of N. Let t∈Tt∈ T and let μ be a marking of N. Then t is enabled at μ if μ(p)>0μ(p)>0 for all p∈Pp∈ P such that (p,t)∈F(p,t)∈ F. If t is enabled at μ, it may occur, and thus lead to a new marking μ′μ of N. Here μ′μ is defined by μ′(p)=μ(p)−1μ (p)=μ(p)-1 if (p,t)∈F(p,t)∈ F and (t,p)∉F(t,p) ∈ F; μ′(p)=μ(p)+1μ (p)=μ(p)+1 if (p,t)∉F(p,t) ∈ F and (t,p)∈F(t,p)∈ F; and μ′(p)=μ(p)μ (p)=μ(p) otherwise. We write μ→Nμ′μ t_Nμ to denote that the occurrence of t at μ in N leads to μ′μ . Furthermore, μ→Nμ λ_Nμ for every marking μ of N; and in case v∈T∗v∈ T^* with v=wtv=wt for some w∈T∗w∈ T^* and some t∈Tt∈ T, then μ→Nμ′μ v_Nμ if there exists a marking μ′μ of N such that μ→Nμ′μ w_Nμ and μ′→Nμ′μ t_Nμ . A place p∈Pp∈ P is a source place of N if there is no t∈Tt∈ T such that (t,p)∈F(t,p)∈ F. The marking μ0 _0 of N such that, for all p∈Pp∈ P, μ0(p)=1 _0(p)=1 if p is a source place and μ0(p)=0 _0(p)=0 otherwise, is the default initial marking of N. The language of N is ℒ(N)L(N) = w∈T∗∣∃μ such that μ0→Nμ\w∈ T^* ∃μ such that _0 w_Nμ\. Note that ℒ(N)L(N) is a finitary, prefix-closed language. Appendix 0.C Enterprise nets and Industry nets Enterprise nets (introduced in [13]) are Petri nets with typed output and input transitions that can be used for asynchronous communication with other Enterprise nets. Definition 19 An Enterprise net (or E-net, for short) is a tuple ℰ=(P,E=(P, ⟨Tint,Tinp,Tout⟩, T_int,T_inp,T_out , F,F, M)M) such that Tint,TinpT_int,T_inp, and ToutT_out are pairwise disjoint sets; TintT_int is the set of internal transitions of ℰE, TinpT_inp its set of input transitions, and ToutT_out its set of output transitions; furthermore, the underlying Petri net of ℰE, und(ℰ)=(P,Tint∪Tinp∪Tout,F)und(E)=(P,T_int∪ T_inp∪ T_out,F), is a Petri net with exactly one source place; finally M is a function M:Tinp∪Tout→M:T_inp∪ T_out with T the set of message types of ℰE. ∎ ℒ(und(ℰ))L(und(E)), also denoted as ℒ(ℰ)L(E), is the language of the Enterprise net ℰE. Communications take place between pairs of Enterprise nets via (initially unmarked) intermediate places between an output transition of one Enterprise net and an input transition (of the same type) of another Enterprise net. When the output transition occurs, it puts a token in the intermediate place and every occurrence of the input transition takes a token from that intermediate place. Thus, to compose enterprise nets, the output and input transitions of the component nets have to be matched. Let V=ℰi∣i∈[n]V=\E_i i∈[n]\ with ℰi=(Pi,⟨Ti,int,Ti,inp,Ti,out⟩,Fi,Mi)E_i=(P_i, T_i,int,T_i,inp,T_i,out ,F_i,M_i) for each i∈[n]i∈[n], be a set of n≥1n≥ 1 E-nets that have no shared elements (places and transitions). A bijection φ:⋃i∈[n]Ti,out→⋃j∈[n]Tj,inp : _i∈[n]T_i,out→ _j∈[n]T_j,inp is a matching over V if, whenever t∈Ti,out∈ T_i,out and φ(t)∈Tj,inp (t)∈ T_j,inp, for some i,ji,j, then i≠ji≠ j and Mi(t)=Mj(φ(t))M_i(t)=M_j( (t)). Note that it may be that no matching over V exists. If a matching exist, V is said to be composable. In that case, an Industry net can be composed from the Enterprise nets from V by connecting matching output and input transitions via new places. Definition 20 Let n≥2n≥ 2. Let V=ℰi:i∈[n]V=\E_i:i∈[n]\ be a composable set of E-nets with ℰi=(Pi,⟨Ti,int,Ti,inp,Ti,out⟩,Fi,Mi)E_i=(P_i, T_i,int,T_i,inp,T_i,out ,F_i,M_i) and Ti=Ti,int∪Ti,inp∪Ti,outT_i=T_i,int∪ T_i,inp∪ T_i,out for all i∈[n]i∈[n]. Let φ be a matching over V. Then P(V,φ)=[t,φ(t)]∣t∈Ti,out,i∈[n]P(V, )=\[t, (t)] t∈ T_i,out,i∈[n]\ is the set of channel places of V and φ , and F(V,φ)=F(V, )= (t,[t,φ(t)])∣\(t,[t, (t)]) t∈Ti,out,i∈[n]∪([t,φ(t)],φ(t))∣t∈ T_i,out,i∈[n]\∪\([t, (t)], (t)) t∈Ti,out,i∈[n]t∈ T_i,out,i∈[n]\ is the set of channel arcs of V and φ . The sets P(V,φ)P(V, ), F(V,φ)F(V, ), and PiP_i, TiT_i, FiF_i, where i∈[n]i∈[n], are all pairwise disjoint. The Industry net (or I-net, for short) over (V,φ)(V, ) is the Petri net ℐ(V,φ)=(P,T,F)I(V, )=(P,T,F) with P=⋃i∈[n]Pi∪P(V,φ)P= _i∈[n]P_i∪ P(V, ), T=⋃i∈[n]TiT= _i∈[n]T_i, and F=⋃i∈[n]Fi∪F(V,φ)F= _i∈[n]F_i∪ F(V, ). ∎ Since channel places are not source places and consequently not marked by the default initial marking, it follows that in every word w from the language of an Industry net ℐ(V,φ)I(V, ), the number of occurrences of an input transition is at most the number of occurrences of its corresponding output transition. Moreover, this also hold for all prefixes of w: each occurrence of an input transition t must be preceded by a unique occurrence of the output transition φ−1(t) ^-1(t). In other words, ℒ(ℐ(V,φ))L(I(V, )) has the prefix property with respect to φ . Appendix 0.D Synthesising Industry nets from event logs In [15], process discovery algorithms are described in the following way. Definition 21 Let L be a family of languages. A process discovery algorithm A for L is an algorithm that computes for all L∈L , a Petri net (L)=(P,T,F)A(L)=(P,T,F) with a single source place such that T=(L)T= Alph(L) and L⊆ℒ((L))L (A(L)). ∎ Note that since Petri nets have a set of transitions that is an alphabet (a non-empty and finite set), the above implies that any family of languages for which a process discovery algorithm exists, comprises only languages that can be defined over a finite alphabet. Furthermore, to facilitate their conversion to Enterprise nets, the Petri nets discovered are required here to have a single source place, as do Enterprise nets. To leverage a process discovery algorithm for the discovery of Petri net models for individual component processes, to discovering a distributed process model for communicating processes, additional information is needed. In [15], next to the input of the global event log (in the form of a language), also the number of participating individual processes (leading to Enterprise nets) is given together with their communication channels described by pairs of matching input and output actions. All this is captured in the form of an alphabet together with a specification of the role of the actions (output, input, internal) and their distribution over the component processes. Definition 22 Let n≥1n≥ 1. An (n-dimensional) distributed communicating alphabet (n-DCA or DCA, for short) is a tuple =([Σ1,…,Σn],[Σint,Σinp,Σout],mt,cp)D\!A=([ _1,…, _n],[ _int, _inp, _out],mt,cp) such that (1) Σ1,…,Σn _1,…, _n are pairwise disjoint alphabets; (2) Σint _int, Σinp _inp, Σout _out are pairwise disjoint, finite sets of internal actions, input actions, and output actions, respectively; (3) ⋃i∈[n]Σi=Σint∪Σinp∪Σout _i∈[n] _i= _int∪ _inp∪ _out; (4) mt:Σinp∪Σout→mt: _inp∪ _out where T is a set of message types; and (5) cp:Σinp∪Σout→Σinp∪Σoutcp: _inp∪ _out→ _inp∪ _out; if n=1n=1, then cpcp is not defined 999If n=1n=1, then cp=∅cp= and usually omitted from the specification of D\!A.; otherwise cpcp is a complement function with space (5.1) cp(Σinp)=Σoutcp( _inp)= _out and cp(Σout)=Σinpcp( _out)= _inp; space (5.2) cp(Σi)∩Σi=∅cp( _i)∩ _i= for all i∈[n]i∈[n]; and space (5.3) mt(cp(a))=mt(a)mt(cp(a))=mt(a) for all a∈Σinp∪Σouta∈ _inp∪ _out. ∎ This definition reflects that local processes have disjoint sets of actions and that each action is either an internal, an input, or an output action of the process it belongs to. Moreover, with each input action corresponds a unique output action of another process and there is exactly one such corresponding input action for every output action. Finally, all input and output actions have a message type and complementary input/output actions have the same type. Actually, the distribution of transitions of an I-net ℐ(V,φ)=(P,T,F)I(V, )=(P,T,F) over its component E-nets in V with their role as internal, input or output actions and the message types from the E-nets, forms a DCA with underlying alphabet T and complement function φ∪φ−1 ∪ ^-1. In [15], it is demonstrated how from a process discovery algorithm A for language family L, an algorithm can be constructed to synthesise an Industry net from an event log and a distributed communicating alphabet. Definition 23 (1) The E-net discovery algorithm derived from A, is the algorithm EA_E that computes, for any pair (L,)(L,D\!A) such that L∈L , (L)=(P,T,F)A(L)=(P,T,F), and =(⟨T⟩,⟨Tint,Tinp,Tout⟩,mt)D\!A=( T , T_int,T_inp,T_out ,mt) is a 1-DCA, the E-net E(L,)=(P,⟨Tint,A_E(L,D\!A)=(P, T_int, Tinp,Tout⟩,F,mt)T_inp,T_out ,F,mt). (2) The I-net discovery algorithm derived from A, is the algorithm IA_I that computes, for any pair (L,)(L,D\!A) such that D\!A is an n-DCA where n≥2n≥ 2, =(⟨Σ1,…,Σn⟩,⟨Σint,Σinp,Σout⟩,mt,cp)D\!A=( _1,…, _n , _int, _inp, _out ,mt,cp), (L)=⋃i∈[n]Σi Alph(L)= _i∈[n] _i, and Σi(L)∈ proj_ _i(L) for all i∈[n]i∈[n], the I-net I(L,)=ℐ(V,φ)A_I(L,D\!A)=I(V, ) with V=E(Σi(L),i)∣i∈[n]V=\A_E( proj_ _i(L),D\!A_i) i∈[n]\ and φ(a)=cp(a) (a)=cp(a) for all a∈Σouta∈ _out. ∎ Assume a process discovery algorithm A for L as given. Let n≥2n≥ 2 and let (L,)(L,D\!A) be such that =(⟨Σ1,…,Σn⟩,⟨Σint,Σinp,Σout⟩,mt,cp)D\!A=( _1,…, _n , _int, _inp, _out ,mt,cp), (L)=⋃i∈[n]Σi Alph(L)= _i∈[n] _i, and Σi(L)∈ proj_ _i(L) for all i∈[n]i∈[n]. By Definition 21 and Definition 23, Σi(L)⊆ℒ(E(Σi(L),i))=ℒ(E(Σi(L)) proj_ _i(L) (A_E( proj_ _i(L),D\!A_i))=L(A_E( proj_ _i(L)). Furthermore, by Theorem 5 from [15], we have L⊆ℒ(I(L,))L (A_I(L,D\!A)) in case L has the prefix property with respect to φ . In [15], it is also shown how this result can be strengthened to an equality when L and I(L,))A_I(L,D\!A)) satisfy the additional property that every word from the language of I(L,))A_I(L,D\!A)) is represented in L by a word w′∈Lw ∈ L, i.e., Σi(w)=Σi(w′) proj_ _i(w)= proj_ _i(w ) for all i∈[n]i∈[n] - in which case L is said to be complete with respect to I(L,)A_I(L,D\!A).