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 systems by using special elements to link with multiple (component) occurrence 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 constructing the new class of unfolding.
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
environment while its behaviour is subject to modification by other systems. The
communication between sub-systems may either be asynchronous or synchronous.
Structured occurrence nets (sons) [
The standard Petri nets unfoldings, introduced in [
am am (a)
b0 b0
bn ...
a0
am ...
b0
(throughout this paper, Petri net related concepts, such as configuration,
unfolding, 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. [
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 [
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 transitions 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 interested in marking reachability, then one might attempt to encode a cspt-net by replacing every asynchronous channel place by a standard place and ‘glue’ transitions 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, the efficiency of such an approach would suffer from the introduction of exponentially 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
concerning 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 [
We assume that the reader is familiar with the basic notions concerning Petri
nets and their unfoldings, which can be found in, e.g., [
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 multiset of transitions of PT . It is enabled at a marking M if M (p) ≥ Pt∈p• U (t), for every place p. In such a case, the execution of U leads to a new marking M 0 given, for every p ∈ P , by M 0(p) = M (p) + Pt∈•p U (t) − Pt∈p• U (t). We denote this by M [U iM 0. A step sequence of PT is a sequence λ = U1 . . . Un (n ≥ 0) of steps such that there exist markings M1, . . . , Mn satisfying M0[U1iM1, . . . , Mn−1[UniMn. 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 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 [
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
In this section we recall the formal definitions concerning communication structured 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.
A communication structured net is composed of a set of component nets representing separate subsystems. When it is determined that there is a potential for an interaction between subsystems, asynchronous or synchronous communication 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 [
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 marking of the channel places; and W ⊆ (T × Q) ∪ (Q × T ), where T = S 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 U is enabled at a marking M if, for every non-channel place p, M (p) ≥ Pt∈p• U (t) and, for every channel place q,
M (q) + X U (t) ≥ X 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 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 connected by a set of channel places (represented by circles with thick edges). To improve readability, the thick dashed lines indicate the flow relation W . Transitions 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 communication. 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
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:
depthqΠ (e) = |{f ∈ T 0 | h(f ) ∈ •q• ∧ (f, e) ∈ F 0∗}| .
Moreover, if the process Π is clear from the context, we will write depthq(e) instead of depthqΠ (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 depthq(e) 6= depthq(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 tuple CSON = (Π1, . . . , Πk, Q0, W 0, h0) such that each Πi = (ON i, hi) is a nonbranching process of PT i with ON i = (Pi0, Ti0, Fi0); Q0 is a set of channel places; W 0 ⊆ (T 0 × Q0) ∪ (Q0 × T 0) where T 0 = S Ti0; and h0 : Q0 → Q. It is assumed that the following hold, where h = h0 ∪ S hi and F 0 = S Fi0: 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 depthh(r)(e) = depthh(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 (@ ∪ ≺)∗◦ ≺ ◦(≺ ∪ @)∗ over T 0 is irreflexive, where: e ≺ f if there is p ∈ S Pi0 with p ∈ e• ∩ •f ; and e @ f if there is r ∈ Q0 with r ∈ e• ∩ •f . 5. h(MCSON ) = MCSPT , where MCSON is the default initial state of CSON defined as S MON i .
The above definition extends that in [
The cson in Figure 4 shows a non-branching processes with the labels (alongside 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 behaviourlevel 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 Definition 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, Ti0, Fi0); Q0 is a set of channel places; W 0 ⊆ (T 0 × Q0) ∪ (Q0 × T 0) where T 0 = S Ti0; and h0 : Q0 → Q. It is assumed that the following hold, where h = h0 ∪ S hi and F 0 = S Fi0:
2. For all r, r0 ∈ Q0 with h(r) = h(r0), as well as for all e ∈ •r• and f ∈ •r0•, depthh(r)(e) = depthh(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 = MBCSON , where the default initial state MBCSON of BCSON is defined as S 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 independent, 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 component 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).
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. 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
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 (@ ∪ ≺)∗◦ ≺ ◦(≺ ∪ @)∗ over C is irreflexive, where: e ≺ f if there is p ∈ S 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 • = ∅. Proposition 4 (configuration is causally closed). Let C be a configuration as in Definition 5. Then, for every e ∈ C, p ∈ S 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 instance 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. Indeed, 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 C0 = {e0, e1, e2, e4} and C00 = {e0, e1, e2, e4, e6, e7} are not valid configurations ( C0 has non input event for the channel place r1, while C00 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 outside 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 input 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 C000 = {e2, e4, e6} is Fin(C000) = {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.
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 is a reachable marking in the original cspt-net. h(Fin(C))
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. Theorem 1. Let BCSON CSPT be the unfolding of CSPT . Then M is a reachable marking of CSPT if and only if M = h(Fin(C)), for some global configuration 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
generate a complete finite prefix of the unfolding which contains a full reachability
information. Later, [
The semantical meaning of completeness has been further addressed in [
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
We will now describe an algorithm for the construction of the unfolding of a csptnet. 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 simply unfold the component branching processes adding one event at a time, and 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 nonexecutable 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 extensions 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. 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 configuration 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 configurations, [e0] and [e7]. Moreover, we can observe that the C[e0] is not the unique local configuration of e0, as another one is C0[e0] = {e0, e3, e5, e8}, where C0 = {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, depthq(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) = (QCi , ≺b Ci , @b Ci ), where ≺b Ci , @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 r0 involving more than one event of Ci, and r @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 together with their input and output channel places. By exploring the relations
C2'={e3, e5}
C3={e6, e8} between those channel places, we are able to generate a/sync graph for any configuration. For example, Figure 7(b) shows five a/sync graphs of the configurations 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) = (QCi , ≺b Ci , @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 2. the relation (@b ∪ ≺b )∗ ◦ ≺b ◦ (≺b ∪ @b )∗ is irreflexive, where @b = S @b Ci . ≺b = S ≺b Ci and
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 configurations 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 component 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 significantly differs from the existing net unfolding algorithms. The key difference is that during the unfolding procedure we will be constructing nodes and connections 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 unfolding, 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)). Proposition 7. Let e be an executable event in BCSON . Then each event appearing 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 marking 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. 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 = depthq(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 nonexecutable. 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 connection for those which already existed) together with the corresponding arcs, we are able to obtain the local configuration of e by looking for compatible configurations 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
The unfolding algorithm presented in this paper is based on standard
unfolding 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 [
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 [