Unfolding CSPT-nets Bowen Li and Maciej Koutny School of Computing Science, Newcastle University Newcastle upon Tyne NE1 7RU, United Kingdom {bowen.li,maciej.koutny}@ncl.ac.uk Abstract. Communication structured occurrence nets (csons) are the basic variant of structured occurrence nets which have been introduced to characterise the behaviours of complex evolving systems. A cson has the capability of portraying different types of interaction between sys- tems by using special elements to link with multiple (component) occur- rence nets. Communication structured place transition nets (cspt-nets) are the system-level counterpart of csons. In this paper, we investigate cspt-nets unfoldings containing representations of all the single runs of the original nets captured by csons. We develop several useful notions related to cspt-net unfoldings, and then present an algorithm for con- structing the new class of unfolding. Keywords: structured occurrence nets, place transition nets, cspt-nets, unfolding, synchronous and asynchronous communication 1 Introduction A complex evolving system consists of a large number of sub-systems which may proceed concurrently and interact with each other or with the external environ- ment while its behaviour is subject to modification by other systems. The com- munication between sub-systems may either be asynchronous or synchronous. Structured occurrence nets (sons) [8, 13, 14] are a Petri net based formalism that can be used to model the behaviours of complex evolving system. The con- cept extends that of occurrence nets [1] which are directed acyclic graphs that represent causality and concurrency information concerning a single execution of a system. In son, multiple related occurrence nets are combined by means of various formal relationships; in particular, in order to express dependencies between interacting systems. Communication structure occurrence nets (csons) are the basic variant of sons. The model has the capability of portraying dif- ferent types of interaction between systems. A cson involves occurrence nets that are connected by channel places representing synchronous or asynchronous communications. [7] introduced a system-level counterpart of csons called com- munication structured place transition nets (cspt-nets). The nets are built out of the place/transition nets (pt-nets), which are connected by channel places allowing both synchronous and asynchronous communication. The standard Petri nets unfoldings, introduced in [2, 12], are a technique supporting effective verification of concurrent systems modeled by Petri nets 208 PNSE’15 – Petri Nets and Software Engineering a0 am b0 bn a0 am ... ... ... b0 (a) (b) a0 am b0 bn ... ... ... ... a 0b 0 a 0b n amb0 ambn (c) (d) Fig. 1. Two cspt-nets (a) and (b); together with their respective standard unfoldings semantics after applying the Petri net encodings (c) and (d). (throughout this paper, Petri net related concepts, such as configuration, un- folding, merged process, will be referred to as standard ). The method relies on the concept of net unfolding which can be seen as the partial order behaviour of a concurrent system. The unfolding (or branching process) of a net is usually infinite, but for bounded Petri nets one can construct a finite complete prefix of the unfolding containing enough information to analyse important behavioural properties. [9] investigated branching processes of cspt-nets (cspt-net unfold- ings). As in the standard net theory, cspt branching processes act as a ‘bridge’ between cspt-nets and their processes captured by csons (i.e., the branching processes of a cspt-net contains a representation of all the possible single runs of the original net). In order to reduce the complexity of branching processes of cspt-nets, we adapt the notion of occurrence depth which was originally developed for merged processes [5]. In this paper, we introduce and discuss several key properties of branching processes of cspt-nets. We also present an algorithm for constructing cspt-net unfoldings, generalising the unfolding algorithm introduced in [9] which could only handle channel places with a single input and a single output transition. In particular, the new algorithm takes into account the occurrence depth of events, and fuses nodes which have same behaviours during the unfolding. In this way, the size of the resulting net can be significantly reduced when compared with the standard unfolding approach. Consider the cspt-nets shown in Figure 1(a) and (b). In (a), m transitions asynchronously communicate with b0 via a single channel place. In (b), m tran- sitions are synchronous with n transitions between two pt-nets via two channel places. Their unfolding semantics are isomorphic to the original cspt-nets (with the sizes of m + 1 events in (a) and m + n events in (b)). If one was only inter- ested in marking reachability, then one might attempt to encode a cspt-net by replacing every asynchronous channel place by a standard place and ‘glue’ tran- sitions forming a synchronous event into a single one. One would then be able to apply the standard unfolding to this Petri net based representation. However, B. Li, M. Koutny: Unfolding CSPT-nets 209 the efficiency of such an approach would suffer from the introduction of expo- nentially many new transitions, as well as the loss of the merging on channel places which is due to the exploitation of occurrence depth. In this case, the ‘replace’ encoding for (a) yields n + m events in the corresponding unfolding (c). While the ‘glue’ encoding for (b) would yield m × n events as shown in (d). The paper is organised as follows. Section 2 provides basic notions concern- ing Petri nets and their unfoldings. Section 3 presents the main concepts of communication structured net theory, including cson-nets, cspt-nets and cspt branching processes. In section 4, we discuss finite complete prefixes of cspt branching processes and related properties. The cspt unfolding algorithm is provided in Section 5. Section 6 discusses future works and concludes the paper. The technical report [10] contains proofs of formal results and an example of the algorithm run. 2 Basic Definitions We assume that the reader is familiar with the basic notions concerning Petri nets and their unfoldings, which can be found in, e.g., [1, 2, 12]. Throughout the paper, a multiset over a set X is a function µ : X → N, where N = {0, 1, 2, . . .}. A multiset may be represented by explicitly listing its elements with repetitions. For example {a, a, b} denotes the multiset such that µ(a) = 2, µ(b) = 1 and µ(x) = 0 for x ∈ X\{a, b}. PT-nets. A net is a triple N = (P, T, F ) such that P and T are disjoint sets of respectively places and transitions (collectively referred to as nodes), and F ⊆ (P × T ) ∪ (T × P ) is the flow relation. The inputs and outputs of a node x are defined as • x = {y | (y, x) ∈ F } and x• = {y | (x, y) ∈ F }. Moreover, •x• = • x∪x• . It is assumed that the inputs and outputs of a transition are nonempty sets. Two nodes, x and x0 , are in conflict if there are distinct transitions, t and t0 , such that • t ∩ • t0 6= ∅ and (t, x) ∈ F ∗ and (t0 , x0 ) ∈ F ∗ . We denote this by x # x0 . A node x is in self-conflict if x # x. A place transition net (pt-net) is a tuple PT = (P, T, F, M0 ), where (P, T, F ) is a finite net, and M0 : P → N is the initial marking (in general, a marking is a multiset of places). A step U is a non-empty P multiset of transitions of PT . It is enabled at a marking M if M (p) ≥ t∈p• U (t), for every place p. In such a case, the execution P of U leads toP a new marking M 0 given, for every p ∈ P , by M (p) = M (p) + t∈• p U (t) − t∈p• U (t). We denote this by M [U iM 0 . A 0 step sequence of PT is a sequence λ = U1 . . . Un (n ≥ 0) of steps such that there exist markings M1 , . . . , Mn satisfying M0 [U1 iM1 , . . . , Mn−1 [Un iMn . The reachable markings of PT are defined as the smallest (w.r.t. ⊆) set reach(PT ) containing M0 and such that if there is a marking M ∈ reach(PT ) and M [U iM 0 , for a step U and a marking M 0 , then M 0 ∈ reach(PT ). PT is k-bounded if, for every reachable marking M and every place p ∈ P , M ≤ k, and safe if it is 1-bounded. The markings of a safe pt-net can be treated as sets of places. Branching processes of PT-nets. A net ON = (P, T, F ), with places and transitions called respectively conditions and events, is a branching occurrence 210 PNSE’15 – Petri Nets and Software Engineering net if the following hold: (i) F is acyclic and no transition t ∈ T is in self-conflict; (ii) |• p| ≤ 1, for all p ∈ P ; and (iii)for every node x, there are finitely many y such that (y, x) ∈ F ∗ . The set of all places p with no inputs (i.e., • p = ∅) is the default initial state of ON , denoted by MON . In general, a state is any set of places. If |p• | ≤ 1, for all p ∈ P , then ON is a non-branching occurrence net. Note that in a branching occurrence net, two paths outgoing from a place will never meet again by coming to the same place (the inputs of places are at most singleton sets) nor the same transition (transitions cannot be in self-conflict). A branching process of a pt-net PT = (P, T, F, M0 ) is a pair Π = (ON , h), where ON = (P 0 , T 0 , F 0 ) is a branching occurrence net and h : P 0 ∪ T 0 → P ∪ T is a mapping, such that the following hold: (i) h(P 0 ) ⊆ P and h(T 0 ) ⊆ T ; (ii) for every e ∈ T 0 , the restriction of h to • e is a bijection between • e and • h(e), and similarly for e• and h(e)• ; (iii) the restriction of h to MON is a bijection between MON and M0 ; and (iv) for all e, f ∈ T 0 , if • e = • f and h(e) = h(f ) then e = f . There exists a maximal branching process ΠPT , called the unfolding of PT [2]. Configurations and cuts of a branching process. Let Π = (ON , h) be a branching process of a pt-net PT , and ON = (P 0 , T 0 , F 0 ). A configuration of Π is a set of events C ⊆ T 0 such that ¬(e # e0 ), for all e, e0 ∈ C, and (e0 , e) ∈ F 0+ =⇒ e0 ∈ C, for every e ∈ C. In particular, the local configuration of an event e, denoted by [e], is the set of all the events e0 such that (e0 , e) ∈ F 0∗ . The notion of a configuration captures the idea of a possible history of a concurrent system, where all events must be conflict-free, and all the predecessors of a given event must have occurred. A co-set of Π is a set of conditions B ⊆ P 0 such that, for all distinct b, b0 ∈ B, (b, b0 ) ∈/ F 0+ . Moreover, a cut of Π is any maximal (w.r.t. ⊆) co-set B. Finite configurations and cuts of Π are closely related (every marking represented in the unfolding ΠPT is reachable in PT , and every reachable marking of PT is represented in ΠPT ): – if C is a finite configuration of Π, then Cut(C) = (MON ∪ C • ) \ • C is a cut and Mark (C) = h(Cut(C)) is a reachable marking of PT ; and – if M is a reachable marking of PT , then there is a finite configuration C of ΠPT such that Mark (C) = M . 3 Structuring PT-nets In this section we recall the formal definitions concerning communication struc- tured nets theory, including cson-nets and cspt-nets. We then introduce the notion of branching processes of cspt-nets and several related properties. The new models are able to portray different kinds of communication between separate systems. One can envisage that if a given pt-net attempts to represent several interacting systems, it will be beneficial to split the model into a set of component nets, and create specific devices to represent any communication between the subsystems. In the model we are interested in communication can be synchronous or asynchronous. Usually, the former implies that a sender waits for an acknowledgment of a message before proceeding, while in the latter the sender proceeds without waiting. B. Li, M. Koutny: Unfolding CSPT-nets 211 A communication structured net is composed of a set of component nets rep- resenting separate subsystems. When it is determined that there is a potential for an interaction between subsystems, asynchronous or synchronous communi- cation link can be made between transitions (or events) in the different nets via a special element called a channel place. Two transitions (events) involved in a synchronous communication link must be executed simultaneously. On the other hand, transitions (events) involved in an asynchronous communication may be executed simultaneously, or one after the other. Similarly as in the case of pt-nets, non-branching processes cson-nets will represent single runs of cspt-nets, while branching processes will capture full execution information of the corresponding cspt-nets. CSPT-nets. By generalising the definition of [7], we first introduce an exten- sion of pt-nets which combines several such nets into one model using channel places. Definition 1 (CSPT-net). A communication structured place transition net (or cspt-net) is a tuple CSPT = (PT 1 , . . . , PT k , Q, W, M0 ) (k ≥ 1) such that each P Ti = (Pi , Ti , Fi , Mi ) is a safe (component) pt-net; Q is a finite set of channel places; M0 : Q → N is the initial S marking of the channel places; and W ⊆ (T × Q) ∪ (Q × T ), where T = Ti , is the flow relation for the channel places. It is assumed that the following are satisfied: 1. The PT i ’s and Q are pairwise disjoint. 2. For every channel place q ∈ Q, – the sets of inputs and outputs of q, • q = {t ∈ T | (t, q) ∈ W } and q • = {t ∈ T | (q, t) ∈ W } are both nonempty and, for some i 6= j, • q ⊆ Ti and q • ⊆ Tj ; and – if •q • ∩ Ti 6= ∅ then there is no reachable marking of PT i which enables a step comprising two distinct transitions in •q • .  The initial marking MCSPT of CSPT is the multiset sum of the Mi ’s (i = 0, 1, . . . , k), and a marking is in general a multiset of places, including the channel places. To simplify the presentation, in the rest of this paper we will assume that the channel places in the initial states of cspt-nets are empty. The execution semantics of CSPT is defined as for a pt-net except that a step of transitions P U is enabled at a marking M if, for every non-channel place p, M (p) ≥ t∈p• U (t) and, for every channel place q, X X M (q) + U (t) ≥ U (t) . (∗) t∈• q t∈q • The condition (∗) for step enabledness caters for synchronous behaviour as step U can use not only the tokens that are already available in channel places at marking M , but also can use the tokens deposited there by transitions from U during the execution of U . In this way, transitions from U can ‘help’ each other 212 PNSE’15 – Petri Nets and Software Engineering Fig. 2. A cspt-net with three component pt-nets. individually and synchronously pass resources (tokens) among themselves. Thus, in contrast to the step execution of a pt-net where a step consists of a number of enabled transitions, the execution of a step in a cspt-net (i.e., M [U iM 0 ) may involve synchronous communications (or interactions), where transitions execute simultaneously and behave as a transaction. Such a mode of execution is strictly more expressive than that used in pt-nets. Figure 2 shows a cspt-net which consists of three component pt-nets con- nected by a set of channel places (represented by circles with thick edges). To improve readability, the thick dashed lines indicate the flow relation W . Tran- sitions n2 and u2 are connected by a pair of empty channel places, q3 and q4 , forming a cycle. This indicates that these two transitions can only be executed synchronously. They will be filled and emptied synchronously when both n2 and u2 participate in an enabled step. On the other hand, the execution of transitions n1 and u0 can be either asynchronous (n1 occurs before u0 ), or synchronous (both of them occur simultaneously). A possible step sequence of Figure 2 is λ = {t0 , n1 }{u0 }{n2 , u2 }, where n1 and u0 perform an asynchronous communi- cation. Another step sequence λ0 = {t0 }{n1 , u0 }{n2 , u2 } shows that n1 and u0 can be also executed synchronously. Definition 1(2) means that the occurrences of transitions in • q (as well as those in q • ) are totally ordered in any execution of the corresponding component net PT i . In other words, we assume that both the output access and the input access to the channel places is sequential. This will allow us to introduce the notion of depth at which an event which accessed a channel place has occurred. Given a branching process derived for a component pt-net of a cspt-net, consider an event e such that its corresponding transition is an input (or output) of a channel place q in the cspt-net. Then the occurrence depth of such event w.r.t., the channel place q is the number of events such that they all causally precede e and their corresponding transitions are also inputs (or outputs) of the channel place q. Since the tokens flowing through channel places are based on the B. Li, M. Koutny: Unfolding CSPT-nets 213 (depthq0=1) (depthq0=2) (depthq0=1) (depthq0=2) Fig. 3. (a) A cspt-net, and (b) its branching process (event labels are shown alongside the nodes and the occurrence depths are shown in brackets). FIFO policy. The occurrence depth intuitively represents the number of tokens which have entered (or left) the channel place q before the occurrence of e. Definition 2 (occurrence depth). Let CSPT be as in Definition 1, and q ∈ Q and PT i be such that •q • ∩ Ti 6= ∅. Moreover, let Π = (ON , h) be a branching process of PT i , and e be an event of ON = (P 0 , T 0 , F 0 ) such that h(e) ∈ •q • . The depth of e in Π w.r.t. the channel place q is given by: depth Π 0 • • 0∗ q (e) = |{f ∈ T | h(f ) ∈ q ∧ (f, e) ∈ F }| . Moreover, if the process Π is clear from the context, we will write depth q (e) instead of depth Π q (e).  Proposition 1. Let Π and q ∈ Q be as in Definition 2. Moreover, let e and f be two distinct events of Π satisfying ¬(e # f ) and h(e), h(f ) ∈ •q • . Then depth q (e) 6= depth q (f ). The nets in the dashed line boxes in Figure 3(b) are two component branching processes derived from the component pt-nets of the cspt-net in Figure 3(a). The labels are shown alongside each node, and the occurrence depth of each event connected to a (unique, in this case) channel place is shown in brackets. Let us consider event e1 . Its corresponding transition t1 is the input of channel place q0 . When searching the directed path starting at the initial state and terminating at e1 , we can find another event (viz. e0 ) such that its corresponding transition is also the input of q0 . Therefore the occurrence depth of e1 , w.r.t. q0 , is depthq0 (e1 ) = 2. It intuitively represents transition t1 passing the second token to the channel. Non-branching processes of CSPT-nets. Similarly to the way in which cspt-nets are extensions of pt-nets, non-branching processes of cspt-nets are extensions of non-branching occurrence nets. Definition 3 (non-branching process of CSPT-net). Let CSPT be as in Definition 1 with M0 being empty. A non-branching process of CSPT is a tu- ple CSON = (Π1 , . . . , Πk , Q0 , W 0 , h0 ) such that each Πi = (ON i , hi ) is a non- branching process of PT i with ON i = (Pi0 , Ti0 , Fi0 ); Q0 is a set of channel places; 214 PNSE’15 – Petri Nets and Software Engineering Fig. 4. A cson-net which is a possible single run of the cspt-net of Figure 2. S 0 W 0 ⊆ (T 0 × Q0 ) ∪ (Q0 × T 0 ) where T 0 = S Ti ; and h0 S : Q0 → Q. It is assumed that the following hold, where h = h ∪ hi and F = Fi0 : 0 0 1. The ON i ’s and Q0 are pairwise disjoint. 2. For every r ∈ Q0 , – |• r| = 1 and |r• | ≤ 1; and – if e, f ∈ •r• , then depth h(r) (e) = depth h(r) (f ). 3. For every e ∈ T 0 , the restriction of h to • e ∩ Q0 is a bijection between • e ∩ Q0 and • h(e) ∩ Q, and similarly for e• ∩ Q0 and h(e)• ∩ Q. 4. The relation (@S∪ ≺)∗ ◦ ≺ ◦(≺ ∪ @)∗ over T 0 is irreflexive, where: e ≺ f if there is p ∈ Pi0 with p ∈ e• ∩ • f ; and e @ f if there is r ∈ Q0 with r ∈ e• ∩ • f . 5. h(MCSON )S= MCSPT , where MCSON is the default initial state of CSON defined as MON i .  The above definition extends that in [7] by allowing an infinite number of nodes, and therefore provides a general meaning of a single run of a cspt-net. To capture the behaviour systems with complex structure, we use the binary relation @ (weak causality) to represent a/synchronous communication between two events (see [7]). Intuitively, the original causality relation ≺ represents the ‘earlier than’ relationship on the events, and @ represents the ‘not later than’ relationship. In order to ensure the resulting causal dependencies remain consis- tent, we require the acylicity of not only each component non-branching process but also any path involving both @ and ≺. The condition involving the depth of two events accessing the same channel place means that the tokens flowing through channel places are based on the FIFO policy, so that the size of the subsequent full representation of the behaviours of a cspt-net is kept low. B. Li, M. Koutny: Unfolding CSPT-nets 215 The cson in Figure 4 shows a non-branching processes with the labels (along- side the nodes) coming from the cspt-net shown in Figure 2. It corresponds, e.g., to the step sequence λ = {t0 , n1 }{u0 }{n2 , u2 } in the original cspt-net. Branching processes of CSPT-nets. We have described two classes of structured nets, i.e., cspt-nets and csons. The former is a system-level class of nets providing representations of entire systems, whereas the latter is a behaviour- level class of nets representing single runs of such systems. In this section, we will introduce a new class of branching nets which can capture the complete behaviours of cspt-nets. Definition 4 (branching process of CSPT-net). Let CSPT be as in Defini- tion 1 with M0 being empty. A branching process of CSPT is a tuple BCSON = (Π1 , . . . , Πk , Q0 , W 0 , h0 ) such that each Πi = (ON i , hi ) is a branching process of PT i with ON i = (Pi0 , T Si , F0 i ); Q is0 a set 0 0 0 of channel places; W 0 ⊆ (T 0 × Q0 ) ∪ (Q × T ) where T =S Ti ; and h S 0 0 0 : Q → Q. It is assumed that the following 0 hold, where h = h0 ∪ hi and F 0 = Fi0 : 1. The ON i ’s and Q0 are pairwise disjoint. 2. For all r, r0 ∈ Q0 with h(r) = h(r0 ), as well as for all e ∈ •r• and f ∈ •r0• , depth h(r) (e) = depth h(r0 ) (f ) ⇐⇒ r = r0 . 3. BCSON is covered in the graph-theoretic sense by a set of non-branching processes CSON of CSPT satisfying MCSON =SMBCSON , where the default initial state MBCSON of BCSON is defined as MON i .  Using arguments similar to those used in the case of the standard net unfoldings, one can show that there is a unique maximal branching process BCSON CSPT , called the unfolding of CSPT . A branching process of a cspt-net consists of branching processes obtained from each component pt-net and a set of channel places. The default initial state MBCSON consists of the initial states in the component branching processes. In addition, Definition 4(1) means that the component branching processes are in- dependent, and all the interactions between them must be via the channel places. In particular, there is no direct flow of tokens between any pair of the compo- nent branching processes. Definition 4(2) implies that the occurrence depths of events inserting tokens to a channel place are the same, and are equal to the occurrence depths of events removing the tokens. Moreover, channel places at the same depth correspond to different channel places in the original cspt-net. Finally, Definition 4(3) specifies that the label of every input and output event of a channel place in bcson matches a corresponding transition in the original cspt-net. In general, every node and arc in the branching process belongs to at least one non-branching process of cspt-net (cson). This ensures that every event in the bcson is executable from the default initial state MBCSON (i.e., it belongs to a step enabled in some reachable marking), and every condition and channel place is reachable (i.e., it belongs to the initial state or to the post-set of some executable events). 216 PNSE’15 – Petri Nets and Software Engineering (a) (b) Fig. 5. (a) cspt-net, and (b) its branching process. Proposition 2 (safeness). Let BCSON be as in Definition 4. Then BCSON is safe when executed from the default initial state MBCSON . Note: This means that we treat BCSON as a cspt-net with the initial marking obtained by inserting a single token in each condition belonging to MBCSON , and safety means that no reachable marking contains more than one token in any condition, including the channel places. The nets in Figure 3(b) and Figure 5(b) are the branching processes of the cspt-nets showing in Figure 3(a) and Figure 5(a) respectively. We can observe that every input and output event of a channel place has the same occurrence depth which represents the token flow sequence during communication between different pt-nets. For instance, in Figure 5(b) the occurrence depths of e0 , e2 and e8 are depthq0 (e0 ) = depthq0 (e2 ) = depthq0 (e8 ) = 1. This means of that the transitions t0 and n0 were involved in a first asynchronous communication. B. Li, M. Koutny: Unfolding CSPT-nets 217 Remark 1. A bcson cannot, in general, be obtained by simply unfolding every component pt-net independently and appending the necessary channel places afterwards. Proceeding in such a way can lead to a net violating Definition 4(3). This is so because an executable transition in a component pt-net does not have to be executable within the context of the cspt-net. For example, Figure 6(b) does not show a valid branching process of the cspt-net of Figure 2. Transition n0 in the middle pt-net of Figure 2 can never be executed since t0 and t1 are in conflict, and the system is acyclic. As the result, there is no n0 -labelled event in a corresponding branching process. Note that Figure 6(a) shows a valid bcson since each event present there is executable.  4 Completeness of branching processes In this section, we introduce the concept of a complete prefix of the unfolding of a cspt-net. The prefix is a truncated part of possibly infinite unfolding which contains full reachability information about the original cspt-net. The idea is to consider global configurations of the unfolding taking into account single runs across different component pt-nets. Then we show that the final states of all the finite global configurations correspond to the reachable markings of original cspt-net. Using this result, it is possible to consider a finite truncation which is sufficient to represent all reachable markings. Global configurations. A global configuration of a bcson consists of a set of (standard) configurations, each coming from a different component branching process, joined together by channel places. Definition 5 (global configuration). Let BCSON be as in Definition 4. A global configuration of BCSON is a set of events C = C1 ∪ · · · ∪ Ck such that each Ci is a configuration of the process Πi , and the following hold: 1. • C ∩ Q0 ⊆ C • . 2. The relation (@S∪ ≺)∗ ◦ ≺ ◦(≺ ∪ @)∗ over C is irreflexive, where: e ≺ f if there is p ∈ Pi0 with p ∈ e• ∩ • f ; and e @ f if there is r ∈ Q0 with r ∈ e• ∩ • f . Moreover, if the configuration C is finite, then Fin(C) = (MBCSON ∪ C • ) \ • C is the final state of C. The set of all global configurations of BCSON will be denoted by Conf BCSON .  Definition 5(1) reflects the nature of a/synchronous communication between component (standard) configurations. Intuitively, if we start with an event of the global configuration which is an output event of a channel place, then there exists an input event of the same channel place that also belongs to the global configuration. Moreover, Definition 5(2) states that there are no asynchronous cycles in a global configuration. Proposition 3 (configuration is non-branching). Let C be a configuration as in Definition 5. Then, for all distinct e, f ∈ C, • e ∩ • f = e• ∩ f • = ∅. 218 PNSE’15 – Petri Nets and Software Engineering Proposition 4 (configuration is causally S closed). Let C be a configuration as in Definition 5. Then, for every e ∈ C, p ∈ Pi0 and p ∈ e• ∩ • f imply f ∈ C. Moreover, if r ∈ Q0 ∩ • e then there is f ∈ C such that r ∈ f • . Since in bcson we use the merging technique in the case of channel places (i.e., different events with same occurrence depth and label will link with same in- stance of channel place), it is possible for a channel place to have multiple inputs or outputs. Propositions 3 and 4 imply that global configuration are guaranteed to be non-branching and causally closed w.r.t. the flow relations F 0 and W 0 . In- deed, if a channel place has more than one input (or output) events, these events are in conflict w.r.t. the flow relation F 0 . Hence the events belong to different configurations, and each channel place in global configuration has exactly one input and no more than one output. As a result, a global configuration retains key properties of the standard configurations, and it represents a valid execution of transitions of the original cspt-net. Consider the branching process in Figure 5. It has a configuration C = {e0 , e1 , e2 , e4 , e7 } which consists of two (component) configurations C1 = {e0 , e1 } and C2 = {e2 , e4 , e7 }, whereas C 0 = {e0 , e1 , e2 , e4 } and C 00 = {e0 , e1 , e2 , e4 , e6 , e7 } are not valid configurations (C 0 has non input event for the channel place r1 , while C 00 includes two standard configurations of a single component pt-net). Each finite configuration C has a well-defined final state determined by the outputs of the events in C. Intuitively, such a state comprises the conditions and channel places on the frontier between the events of C and events out- side C. Note that a final state may contain channel places which were involved in asynchronous communications. No channel place involved in a synchronous communications can appear in Fin(C), as such channel place must provide in- put for another event. For instance, the final state of the global configuration example above is Fin(C) = {c2 , c9 }, whereas the final state of another global configuration C 000 = {e2 , e4 , e6 } is Fin(C 000 ) = {r0 , r2 , c8 } which contains two asynchronous channel places. The next result shows that a global configuration together with their outputs and the initial state form a cson representing a non-branching process of the original cspt-nets. And, similarly, the events of a non-branching process included in a branching one form a global configuration. Proposition 5. Let BCSON be as in Definition 4. 1. Let C be a global configuration as in Definition 5. Then MBCSON ∪ C ∪ C • are the nodes of a non-branching process of CSPT included in BCSON . 2. The events of any non-branching process CSON included in BCSON and satisfying MCSON = MBCSON form a global configuration. Proposition 6. Let C be a global configuration as in Definition 5. Then h(Fin(C)) is a reachable marking in the original cspt-net. By combining Propositions 5 and 6, we obtain that finite global configurations provide a faithful representation of all the reachable marking of the original cspt-net. B. Li, M. Koutny: Unfolding CSPT-nets 219 Theorem 1. Let BCSON CSPT be the unfolding of CSPT . Then M is a reach- able marking of CSPT if and only if M = h(Fin(C)), for some global configu- ration C of BCSON CSPT . Complete prefixes of CSPT-nets. A complete prefix of the unfolding of a cspt-net contains a full reachability information about the original cspt-net. Such a property is referred to as completeness. Finite complete prefixes of Petri nets were first introduced in McMillan’s seminal work in order to avoid the state explosion problem in the verification of systems modelled with Petri nets. McMillan also provided an algorithm to gen- erate a complete finite prefix of the unfolding which contains a full reachability information. Later, [3] refined McMillan’s prefix construction algorithm to avoid creating prefixes larger than necessary. The semantical meaning of completeness has been further addressed in [6], which extended it to more general properties. Basically, [6] associated complete- ness with some additional information, provided by the cut-off events which were only considered as an algorithm issue in the previous works. We can adapt the resulting notion to the current context as follows. Definition 6 (completeness). Let BCSON be as in Definition 4, and Ecut be a set of events of BCSON . Then BCSON is complete w.r.t. Ecut if the following hold: – for every reachable marking M of CSPT , there is a finite global configuration C such that C ∩ Ecut = ∅ and Fin(C) = M ; and – for each global configuration C of BCSON CSPT such that C ∩ Ecut = ∅ and, for each event e ∈/ C of BCSON CSPT such that C ∪ {e} is a global configuration of BCSON CSPT , it is the case that e belongs in BCSON . Moreover, bcson is marking complete if it satisfies the first condition.  5 Unfolding algorithm for CSPT-net We will now describe an algorithm for the construction of the unfolding of a cspt- net. A key notion used by the algorithm is that of an executable event (i.e., an event which is able to fire during some execution from the default initial state) as well as that of a reachable condition or channel place (i.e., one produced by an executable event). Note that whether an event is executable in a cspt-net is not only determined by the corresponding pt-net, but also by the behaviours of other pt-nets. This means that a component branching process in cspt unfolding may not preserve its own unfolding structure (see Remark 1 and Figure 6(a)). In other words, there may exist events which are valid extensions in the unfolding process of a component pt-net, but become invalid when considering communication. In particular, due to synchronous communication, it may be difficult to make sure that every extension is executable before appending it to the unfolding. Unlike the standard unfolding methods, an algorithm for cspt-net cannot sim- ply unfold the component branching processes adding one event at a time, and 220 PNSE’15 – Petri Nets and Software Engineering (a) (b) Fig. 6. (a) A valid cspt branching process of Figure 2 (top), and (b) an invalid one (bottom). connecting it to already existing channel places. This is because a synchronous communication in cspt unfolding forms a cycle. It is therefore impossible to add only one of the synchronised events and guarantee its executability at the same time. Similarly, adding a synchronous event set together with all related channel places in one step may also be difficult to achieve since the use of merging may produce infinitely many events which are connected to the same channel place. Instead, our idea is to design an algorithm which will sometimes generate non- executable events requiring tokens from channel places which have not yet been generated, in the anticipation that later on a suitable (possibly synchronous) events will provide such tokens. Roughly, the algorithm appends possible ex- tensions together with their output conditions one by one. A new event is first marked as non-executable. The algorithm then performs an executability check for the event after constructing its a/synchronous communications. In this way, in general we obtain an ‘over-approximating unfolding’. The final stage of the algorithm can then be used to remove all the non-executable nodes. Before providing the details of the algorithm, we introduce some auxiliary notions. In what follows, we assume that CSPT is as in Definition 1. B. Li, M. Koutny: Unfolding CSPT-nets 221 Definition 7 (local CSPT configuration). Let e ∈ C, where C is a global configuration of BCSON as in Definition 5. Then the local CSPT configuration of e in C, denoted by C[e], is defined as C[e] = {f ∈ C | (f, e) ∈ (≺ ∪ @)∗ }, where the relations ≺ and @ are as in Definition 5. Moreover, Conf (e) = {C[e] | C ∈ Conf BCSON ∧ e ∈ C} is the set of all CSPT local configurations of e.  The cspt local configuration of an event e in C is the set of events that are executed before (or together with) e. In general, it consists of a configuration comprising the standard local configuration of e together with a set of standard configurations coming from other branching processes. Note that an event may have different local cspt configurations, e.g., if one of its inputs is a channel place which has multiple input events. Each such local configuration belongs to a different non-branching process. For instance, consider a global configura- tion C = {e0 , e1 , e2 , e4 , e7 } in Figure 5. The cspt local configuration of event e0 in C is C[e0 ] = {e0 , e2 , e4 , e7 } which involves two standard local cspt con- figurations, [e0 ] and [e7 ]. Moreover, we can observe that the C[e0 ] is not the unique local configuration of e0 , as another one is C 0 [e0 ] = {e0 , e3 , e5 , e8 }, where C 0 = {e0 , e1 , e3 , e5 , e8 }. An event may even have infinitely many local configurations. Consider again the net in Figure 5. If we continue to unfold the net, we will construct infinitely many n0 and n1 labelled events with occurrence depth equal to 1. All of them are input events for q0 and q1 labelled channel places and belong to different non-branching processes. A/sync graphs. In order to improve the efficiency of unfolding procedure, checking for the existence of a local cspt configuration of an event can be reduced to the problem of exploring the causal dependencies between channel places. Below we assume that if Ci is a configuration of the unfolding of the i-th component pt-net, and e ∈ Ci and q ∈ Q are such that (h(e), q) ∈ W (or (q, h(e)) ∈ W ), then r = (q, depth q (e)) belongs to the set of implicit channel places QCi connected to Ci . Moreover, the label of r is q, and (e, r) ∈ WCi (resp. (r, e) ∈ WCi ) is the corresponding implicit arc. Definition 8 (a/sync graph). Let Ci be a configuration of the unfolding of the i-th component pt-net. Then the a/sync graph of Ci is defined as G(Ci ) = b Ci , @ (QCi , ≺ b Ci , @ b Ci ), where ≺ b Ci are two binary relations over QCi such that, for every r, r0 ∈ QCi : – r≺b Ci r0 if there are two distinct e, f ∈ Ci such that (r, e), (f, r0 ) ∈ WCi , and e precedes f within C; and – r@b Ci r0 if there is e ∈ Ci with (r, e), (e, r0 ) ∈ WCi .  G(Ci ) captures relationships between the input and output channel places of a configuration of the unfolding of an individual component system. Its nodes are the channel places involved in Ci . Moreover, r ≺ b Ci r0 if there is a path from r to r involving more than one event of Ci , and r @ 0 b Ci r0 if r is an input and r0 an output of some event in Ci . Figure 7(a) shows the unfolding of each component pt-net of Figure 2 to- gether with their input and output channel places. By exploring the relations 222 PNSE’15 – Petri Nets and Software Engineering 1 2 3 (a) C2={e2, e4} C1={e0} C3={e6, e8} C1'={e1} C2'={e3, e5} (b) Fig. 7. (a) unfoldings of three component pt-nets of Figure 2 (together with their implicit channel places), and (b) a/sync graphs of configurations derived from these unfoldings. between those channel places, we are able to generate a/sync graph for any con- figuration. For example, Figure 7(b) shows five a/sync graphs of the configura- tions derived from Figure 7(a), where the relations ≺ b Ci and @ b Ci are represented by solid arcs and thick dashed arcs, respectively. For the left-hand side pt-net Π1 , we have: G(C1 ) = ({r0 }, ∅, ∅) and G(C10 ) = ({r1 }, ∅, ∅). The a/sync graphs of the configurations in Π2 are: G(C2 ) = ({r2 , r3 , r4 , r5 }, {(r2 , r4 ), (r3 , r4 )}, {(r5 , r4 )}) and G(C20 ) = ({r6 , r7 , r8 }, ∅, {(r8 , r7 )} and for the right-hand side pt-net Π3 , we have G(C3 ) = ({r9 , r10 , r11 }, {(r9 , r11 )}, {(r10 , r11 )}). Given a set of a/sync graphs G(C1 ), . . . , G(Ck ) extracted for the k component systems, we call these graphs compatible if all inputs are produced and there is no cycle involving ≺.b Definition 9 (compatibility of a/sync graphs). Let Ci (i = 1, . . . , k) be a configuration of the unfolding of the i-th component pt-net, and G(Ci ) = b Ci , @ (QCi , ≺ b Ci ). Then C1 , . . . , Ck are compatible configurations if the following hold: 1. if (r, e) ∈ WCi then that there is j 6= i such that r ∈ QCj ; and B. Li, M. Koutny: Unfolding CSPT-nets 223 S 2. the relation S (@ b ∗◦≺ b ∪ ≺) b ∪ @) b ◦ (≺ b ∗ is irreflexive, where ≺ b = b Ci and ≺ @ b= @ b Ci .  In Figure 7, configurations C1 , C20 , C3 are compatible since the q3 -labelled input channel place r8 in G(C20 ) is present in G(C3 ) (i.e., r11 ), and the input channel places r9 , r10 (labelled by q2 and q4 respectively) in G(C3 ) are all present in G(C20 ). On the other hand, we can observe that there are no compatible config- urations which involve C2 , i.e., neither configurations C1 , C2 , C3 nor C10 , C2 , C3 are compatible. This is because the producers of r2 and r3 are in conflict in Π1 . Theorem 2. Let C1 , . . . , Ck be configurations of the unfoldings of the compo- nent pt-nets, and C = C1 ∪ · · · ∪ Ck . Then C is a global configuration if and only if C1 , . . . , Ck are compatible. Therefore, one can obtain the cspt local configurations of an event e by checking whether there are compatible configurations C1 , . . . , Ck such that e belongs to one of them. Such a task can be made efficient by working with the graphs G(C1 ), . . . , G(Ck ). In fact, one can just check those configurations which have dependencies on e. Unfolding algorithm. The unfolding algorithm we are going to present sig- nificantly differs from the existing net unfolding algorithms. The key difference is that during the unfolding procedure we will be constructing nodes and con- nections which will not necessarily be the part of the final unfolding. This is due to the presence of synchronous communication within our model. More precisely, in the net being constructed there will be executable and non-executable events and conditions. The former will definitely be included in the resulting unfold- ing, whereas the latter cannot be yet included due to the absence of event(s) which are needed for communication. If, at some later stage, the missing events are generated, then the previously non-executable event and the conditions (and channel places) it produced become executable. Although the net Unf generated by the algorithm may not strictly speaking be a branching process during its creation, we will as far as it is possible treat it as such. In particular, we will call an event e executable if e has at least one local configuration, i.e., Conf (e) 6= ∅. This happens if we have generated enough events to find at least one local cspt configuration of e in Unf . Intuitively, an executable event is the event belonging to at least one single run of a bcson. For the example net in Figure 6(b), e6 is an executable event since there exists a local cspt configuration of e6 : C[e6 ] = {e0 , e3 , e6 }, where C = {e0 , e3 , e6 }. On the other hand, event e2 is non-executable because it does not have any local configuration (we have seen the example of Figure 7 that there are no compatible configurations which involve e2 ). Therefore, Figure 7(b) is not a valid cspt branching process since according to Definition 4(3) every event in BCSON is executable. If we remove e2 together with its successors, then all events in the new net become executable indicating the net is a valid bcson (Figure 6 (a)). 224 PNSE’15 – Petri Nets and Software Engineering Proposition 7. Let e be an executable event in BCSON . Then each event ap- pearing in Conf (e) is executable. Algorithm 1 (unfolding of cspt-net) input: CSPT — cspt-net output: Unf — unfolding of BCSON nonexe ← ∅ Unf ← the empty branching process add instances of the places in the initial marking of CSPT to Unf add all possible extensions of Unf to pe while pe 6= ∅ do remove e from pe addConnections(e) if Conf (e) 6= ∅ then for all event f in configurations of Conf (e) do remove f and all its output conditions from nonexe (if present there) add all possible extensions of Unf to pe delete the nodes in nonexe together with adjacent arcs from Unf The procedure for constructing the unfolding of a cspt-net is presented as Algorithm 1. The first part of the algorithm adds conditions representing the initial mark- ing of the cspt-net being unfolded. Notice that the set nonexe of non-executable events and conditions is set to empty. It also adds possible extensions to the working set pe. The concept of a non-executable condition greatly improves the efficiency of the above algorithm since a possible extension of Unf is a pair e = (t, B) with h(e) = t where t is a transition of CSPT , and B is a set of conditions of Unf such that: – B is a co-set in one of the subnets of Unf and B ∩ nonexe = ∅; – h(B) are all the input non-channel places of t; and – (t, B) ∈ / pe and Unf contains no t-labelled event with the non-channel place inputs B. The pair (t, B) is an event used to extend bcson without considering channel places. We use the standard condition of a possible extension to choose events that can be added to a component branching process (i.e., h(B) = • t ∩ P 0 ), while constructing the related a/synchronous communications in a separate step. In such a way, the complexity of appending groups of synchronous events is significantly reduced. Note that a possible extension e has precisely determined channel place connections since the depth values are fully determined. Algorithm 2 provides the details of appending a possible extension e to bcson as well as constructing related channel place structure after removing e from pe. B. Li, M. Koutny: Unfolding CSPT-nets 225 Algorithm 2 (adding new event and a/sync connections) procedure addConnections (input: e = (t, B)) add e to Unf and nonexe create and add all the standard post-conditions of e to Unf and nonexe for all channel place q ∈ •t• do let r = (q, k) where k = depth q (e) if there is no r = (q, k) in Unf then add q-labelled channel place r to Unf and nonexe add a corresponding arc between r and e Each new extension and its output conditions are immediately marked as non- executable. The conditions in nonexe set also indicate that they are unable to be used for deciding any further possible extension. In this way we can avoid any unnecessary extension and make sure the predecessors of every new event is executable. The procedure then creates the a/synchronous communications of the input event if it is required. Given an event e, for every input or output channel place q of its corresponding transition h(e) in the original cspt-net, we search in Unf for the matching channel place (i.e., its label is q and its depth value equals to the occurrence depth of e). Then we create a direct connection if such a channel place exists. Otherwise, we add a new instance of the channel place together with the corresponding arc. After adding the implicit channel places connected to e (or creating the con- nection for those which already existed) together with the corresponding arcs, we are able to obtain the local configuration of e by looking for compatible con- figurations C1 , . . . , Ck of the component nets (which may contain non-executable events) such that e belongs to one of the Ci ’s. If e is executable (Conf (e) 6= ∅), we make all non-executable events in Conf (e) together with their post-conditions executable (see Proposition 7). We also generate new potential extensions (each such extension must use at least one of conditions which have just been made executable). Then another waiting potential extension (if any) is processed. The algorithm generally does not terminate when the original cspt-net is not acyclic, and the non-executable nodes are removed at the end of the algorithm. An example run of the algorithm is presented in the appendix. 6 Conclusions and Future Work The unfolding algorithm presented in this paper is based on standard unfold- ing method, which essentially works by appending possible extension one by one. A potentially very efficient approach for the construction of the unfolding could be to use the parallel unfolding technique [4]. One can, for example, un- fold each component branching process in parallel, by temporarily ignoring any a/synchronous issues. The procedures of appending channel places as well as executability checking (removing unnecessary events) would proceed in parallel. 226 PNSE’15 – Petri Nets and Software Engineering In future we intend to explore the generation of finite complete prefixes of cspt-nets. In the case of pt-nets, this relies on the notion of cut-off events, which are roughly events in the unfolding that produce a marking already produced by other events with smaller histories. In general, it is impossible to generate a finite complete prefix of the unfolding of a cspt-net even if the component pt-nets are safe. The reason is that the channel places linking the component pt-nets can be unbounded due to asynchronous communication. However, if all communications are synchronous, this is no longer a problem. Finally, the implementation of the cspt model and its unfolding to the son-based [11] tool are left for the future works. References 1. Best, E., Fernández, C.: Nonsequential Processes: A Petri Net View, vol. 13 of EATCS Monographs in Theoretical Computer Science. Springer-Verlag (1988) 2. Engelfriet, J.: Branching processes of Petri nets. Acta Informatica 28(6), 575–591 (1991) 3. Esparza, J., Römer, S., Vogler, W.: An improvement of McMillan’s unfolding algo- rithm. In: Formal Methods in System Design. pp. 87–106. Springer-Verlag (1996) 4. Heljanko, K., Khomenko, V., Koutny, M.: Parallelisation of the Petri net unfold- ing algorithm. In: Proceedings of the 8th International Conference on Tools and Algorithms for the Construction and Analysis of Systems. pp. 371–385. TACAS ’02, Springer-Verlag, London, UK, UK (2002) 5. Khomenko, V., Kondratyev, A., Koutny, M., Vogler, W.: Merged processes: A new condensed representation of Petri net behaviour. Acta Informatica 43(5), 307–330 (2006) 6. Khomenko, V., Koutny, M., Vogler, W.: Canonical prefixes of Petri net unfoldings. Acta Inf. 40(2), 95–118 (2003) 7. Kleijn, J., Koutny, M.: Causality in structured occurrence nets. In: Dependable and Historic Computing. vol. 6875, pp. 283–297. Springer Berlin Heidelberg (2011) 8. Koutny, M., Randell, B.: Structured occurrence nets: A formalism for aiding system failure prevention and analysis techniques. Fundamenta Informaticae 97(1), 41–91 (Jan 2009) 9. Li, B.: Branching processes of communication structured PT-nets. In: Proceed- ing. vol. 13th International Conference On Application of ConCurrency to System Design (ACSD), pp. 243–246 (2013) 10. Li, B., Koutny, M.: Unfolding cspt-nets. Tech. Rep. CS-TR-1463, School of Com- puting Science, Newcastle University (2015) 11. Li, B., Randell, B.: Soncraft user manual. Tech. Rep. CS-TR-1448, School of Com- puting Science, Newcastle University (Feb 2015) 12. McMillan, K.L., Probst, D.: A technique of state space search based on unfolding. Formal Methods in System Design 6(1), 45–65 (Jan 1995) 13. Randell, B.: Occurrence nets then and now: the path to structured occurrence nets. In: Applications and Theory of Petri Nets. pp. 1–16. Springer Berlin Heidelberg (Jun 2011) 14. Randell, B., Koutny, M.: Failure: their definition, modelling and analysis. In: The- oretical Aspects of Computing–ICTAC 2007. pp. 260–274. Springer (Sep 2007)