A fundamental concept used in the area of concurrent systems modelling is conflict. In this paper, we outline two approaches leading to a conflict-concurrent model where distributed choices are resolved in a way which allows one to carry out probabilistic estimation. In particular, the concept of cluster-acyclic net is introduced to transform a net with confusion (a specific combination of conflict and concurrency which makes the probabilistic estimation problematic), into another net whose structure is free-choice which facilitates probabilistic estimation. Then the approaches of removing confusion is extended into Communication Structured Acyclic nets (csa-nets) which is so far lacked of probabilistic analysis. csanets are sets of acyclic nets which can communicate by means of synchronous and asynchronous interactions.
Communication Structured Acyclic Nets (csa-nets) are derived from Structured Occurrence Nets (SONs), which was first introduced in [1] and elaborated in [2]. csa-nets consist of multiple acyclic nets that are joined together with the objective of recording information about the behaviour of Complex Evolving Systems (CESs). [3] lists the features of a CES as being composed of wide array of (sub)systems that interact with each other and with its surrounding environment, resulting in a highly complex structure. The structure of csa-nets is suitable to represent the activities of such systems where the cognitive complexity can be reduced. For instance, [2] introduce the basic formalization of SON to represent complex fault-error-failure chains. Also, [3] shows that SON can be used to visualise and analyse behaviour of CESs and [4] demonstrates its capabilities for modelling cybercrime investigation. Previous work on SONs is related to a framework for provenance [5], timed behaviours [6], and for csa-net a SAT-based model checking proposed in [7].
One of the potential applications of csa-nets is complex crime investigation systems. In crime investigation, full information about a specific activity is, in general, not available [8]. Hence (often numerous) alternate scenarios are pursued by investigators in order to clarify the status of a crime or accident. That is because such a system is characterized as being inherent nondeterminism which originates from the lack of the ability to observe the system. To cope with this feature, investigators need to consider all the possible scenarios. However, considering all possible scenarios might result in meaningless conclusion. Thus, reasoning about what is probable along with what is possible is an essential to obtain meaningful conclusion [9]. Therefore, providing effective probabilistic estimation of different scenarios would greatly help crime investigators to find answers to crucial questions concerning the incident.
There are several works combining probabilistic reasoning and Petri nets. For example, in [10] nets were covered by so-called agents and the non-deterministic and probabilistic decisions were resolved on the basis of local information. The choice of the set of agents that were responsible for the resolution of the choices was done independently. In [11], probabilistic models have been explored for a specific variant of Petri nets. In [12], generalized Markov chains were developed as an extension of Petri nets.The paper [13] extended Mazurkiewicz equivalence to probabilistic words, which were defined as probability distribution, to describe the probabilistic net systems.
Providing a probabilistic framework for concurrent models relies on the presence of conflict transitions which can be associated with positive numerical weights, so that the conflict is resolved by taking their weights into consideration. This seems trivial when the structure of nets is restricted to free-choice. However, if it is not the case, then the probabilistic analysis for concurrent models requires to take a special case in consideration. A confusion arises when conflict and concurrency are overlapped which causes problematic probabilistic estimation. A considerable amount of literature has been published on handling confusion. For example, in [14], a confusion-free net was constructed by a recursive static decomposition of given net. Probabilities were then added to the new non-deterministic net in order to account for the conflict between transitions. Also, confusion was controlled in [15] by attaching an external event with each transition involved in confusion. Then a control sequence is chosen so that the execution of these transitions is controlled. [16] provides algorithms to detect confusion and an approach of avoiding it by enforcing a constraint of supervisory control to ensure that conflict transitions are enabled together so that confusion cannot occur in marking evolution. Time is introduced in [17] to distinguish the proprieties of weighted transitions to resolve the confusion.
A general comment which applies to the above past research is that they are all concerned with standard Petri nets. The key contribution of this paper is to find solutions for nets supporting different kinds of interprocess communication. In this paper we extend the probabilistic analysis into csa-nets which is so far lacked of such an extension. The confusion phenomena is also extended and an approach of removing it based on the technique proposed by [14] is introduced.
The paper is organised as follow. Section 2 presents acyclic nets and their properties. Clusteracyclic nets are introduced in Section 3 and it is shown how to remove confusion in such a case. Section 4 presents csa-nets and their properties. The definition of confusion is extended to csa-nets and the approach of removing it is discussed in Section 5. We conclude in Section 6.
Acyclic Petri nets are a well-established and basic model for representing system behaviour. They can be used to model synchronisation and conflict, two fundamental concepts used in the area of concurrent systems. In this section we first introduce acyclic nets and their properties. Probabilistic acyclic nets are introduced after that. In addition, the notion of confusion is discussed. We propose algorithms used for removing it in Section 3. An occurrence net [2] is an acyclic net such that | β’ π| β€ 1 and |π β’ |β€ 1, for every place π. An occurrence net describes a single execution of some concurrent system in such a way that only the details of causality and concurrency between transitions are captured.
A scenario of acnet is an occurrence net ocnet such that:
β’ π ocnet β π acnet and π ocnet = π ππππ‘ acnet βͺ post acnet (π ocnet ), and β’ pre ocnet (π‘) = pre acnet (π‘) and post ocnet (π‘) = post acnet (π‘), for every π‘ β π ocnet .
It is maximal if there is no scenario ocnet β² satisfying π ocnet β π ocnet β² . This is denoted by ocnet β scenarios(acnet) and ocnet β maxscenarios(acnet), respectively. Each scenario is identified by its transitions π β π and is given by scenario acnet (π ) = (π, π, πΉ acnet | (π Γπ )βͺ(π Γπ ) ), where π = π init acnet βͺ π β’ . Figure 1(b) shows a maximal scenario. Given an acyclic net, its execution proceeds by the occurrence (or firing) of sets of transitions. Let acnet = (π, π, πΉ ) be an acyclic net.
β’ markings(acnet) = {π | π β π } are the markings (shown by placing tokens within the circles), and We can treat individual transitions as singleton steps; e.g., a step sequence {π‘}{π’}{π€, π£}{π§} can be denoted by π‘π’{π€, π£}π§.
Well-formedness. An acyclic net acnet is well-formed if each transition occurs in at least one step sequence and the following hold, for every step sequence π 1 . . . π π β sseq(acnet):
Intuitively, a well-formed acyclic net does not have 'useless' transitions and no place is filled more than once in any given step sequence. Hence, all its behaviours can be interpreted in terms of causal histories as it is guaranteed that each transition is caused by a unique set of transitions. Each occurrence net is well-formed, and an acyclic net is well-formed iff each transition occurs in at least one scenario, and each step sequence is a step sequence of at least one scenario. Each step sequence π of a well-formed acyclic net acnet induces a scenario scenario acnet (π) = scenario acnet (π ), where π are the transitions occurring in π. Thus, different step sequences may generate the same scenario, and conversely, each scenario is generated by at least one step sequence. Moreover, two maximal step sequences generate the same scenario iff their executed transitions are identical.
Conflict, causality and concurrency. Let acnet = (π, π, πΉ ) be an acyclic net.
β’ conflset acnet (π, π‘) = {π‘} βͺ {π’ β enabled acnet (π ) | π‘# 0 π’} is the conflict set of π‘ β π enabled at a marking π .
β’ caused acnet (π₯) = {π¦ β π βͺ π | π₯πΉ + π¦} are the nodes caused by π₯ β π βͺ π .
Calculating probabilities in acyclic nets. In order to find probabilities of alternate scenarios, conflicting transitions are assigned positive numerical weights, representing the likelihood of transitions. From now on, each acyclic net has an additional (last) component π defined as a mapping from the set of transitions to positive integers. For each transition π‘, π(π‘) is its weight which in diagrams annotates the corresponding node. Also, we assume that the weights are assigned to the transitions rather than the arcs and are represented inside the boxes. In such cases the names of transitions are represented outside. Probabilities of concurrent transitions are given by the products of their weights over the sum of the weights of transitions in their conflict sets. More precisely, we define the probability of executing a transition π‘ and step π enabled at a reachable marking π as:
and P acnet (π, π ) = βοΈ π‘βπ P acnet (π, π‘) .
Consider the acyclic net acnet in Figure 2(a), where π and π are in direct conflict and have weights 6 and 3, respectively. Such a conflict can be resolved probabilistically at reachable markings π = {π 1 , π 2 } and π β² = {π 1 } by the following calculation: P acnet (π, π) = P acnet (π β² , π) = π(π)/(π(π) + π(π )) = 6/9. Note that β and π are certain transitions since no transition competes with them for a token, and so their weights are irrelevant.
There are two possible scenarios for this acyclic net: ocnet 1 = scenario({β, π, π}) and ocnet 2 = scenario({β, π, π }). Each can be executed by following different maximal step sequences:
β’ ocnet 1 has three executions: π 1 = βππ, π 2 = βππ, and π 3 = β{π, π}. Their probabilities are the same as we have:
β’ ocnet 2 has also three executions with probabilities equal to 3/9.
As a result, we can assign probabilities to the two scenarios: P acnet (ocnet 1 ) = 6/9 and P acnet (ocnet 2 ) = 3/9. Note that P acnet (ocnet 1 ) + P acnet (ocnet 2 ) = 1. A key issue is to ensure in each case that no matter which of the executions of a scenario is followed in the calculation of probabilities, the same value is obtained (in other words, all maximal step sequences generated from a scenario should have the same probability). One can then define the probability of a scenario as P acnet (ocnet) = P acnet (π), where π is any execution of ocnet. Also, in a sound probability model, the sum of the probabilities of all possible scenarios should be 1. However, the above is not always the case as acyclic nets can exhibit confusion described next.
Confusion. An interplay between conflict and concurrency can lead to a situation called confusion which interferes with the calculation of probabilities. In a symmetric confusion, executing transition π concurrent with π removes at least one transition from the conflict set of π.
In an asymmetric confusion, executing transition π concurrent with π adds a new transition to the conflict set of π [18]. Hence, the order in which one chooses to execute π and π may lead to different probabilities.
A well-formed acyclic net acnet has a confusion [14] at a reachable marking π if there are distinct transitions π, π, β such that {π, π } β enabled acnet (π ) and one of the following holds:
β’ π# 0 β# 0 π and β β enabled acnet (π ).
We then denote symconfused acnet (π, π, π, β) in the first (symmetric) case, and in the second (asymmetric) case we denote asymconfused acnet (π, π, π, β) . Proposition 1. Let acnet be a well-formed acyclic net and π be its reachable marking. If it is the case that symconfused acnet (π, π, π, β) or asymconfused acnet (π, π, π, β) holds, then we have
. However, if π 2 is executed, then the resulting probability is P acnet (π 2 ) = 3/6 ΜΈ = P acnet (π 1 ). Hence one cannot assign a probability to ocnet 1 . A similar conclusion can be reached for the acyclic net in Figure 2(c) which exhibits asymmetric confusion asymconfused acnet (π init acnet , π, π, π). A crucial property is that in a confusion-free acyclic net, conflict sets of transitions are constant for all the executions of each scenario.
1. If π and π β² are two reachable markings of acnet such that π [β© acnet π β² , then we have conflset acnet (π, π‘) = conflset acnet (π β² , π‘), for every π‘ β enabled acnet (π ) β© enabled acnet (π β² ).
2. If π and π β² are two reachable markings of ocnet β scenarios(acnet), then it is the case that conflset acnet (π, π‘) = conflset acnet (π β² , π‘), for every π‘ β enabled ocnet (π ) β© enabled ocnet (π β² ).
Hence, for confusion-free acyclic nets one can calculate probabilities of individual scenarios. Note that there are classes of nets which exclude confusion by imposing structural restrictions, e.g., free-choice nets [19].
The approach of removing confusion is based on identifying the choice points by applying the concept of clusters.
A cluster of a well-formed acyclic net acnet = (π, π, πΉ ) is a non-empty set π β π such that
The set of all clusters is denoted by clusters(acnet), and the set of all maximal clusters is denoted by maxclusters(acnet).
A maximal cluster is an equivalence class of the relation (# 0 ) * , and so the set of maximal clusters partitions the set of all transitions. Below we will consider a subclass of acyclic nets where the ordering β is a strict partial order on the set maximal of clusters.
A well-formed backward deterministic acyclic net is cluster-acyclic if the relation β on its maximal clusters is a strict partial order. Note that cluster-acyclic nets include all free-choice well-formed backward deterministic acyclic nets as well as all extended free-choice acyclic nets.
A transaction of a maximal cluster π of a well-formed backward deterministic cluster-acyclic net with a marking π β β’ π is a step π included in π such that β’ π β π . Moreover, it is maximal if there is no transaction π β² such that π β π β² , and we denote π β maxtrans(π , π ). Intuitively, a transaction is one of possible ways of executing the subnet induced by the cluster. From now on we assume that every cluster-acyclic net is well-formed and backward deterministic. Also, a cluster π = {π‘ 1 , . . . , π‘ π } can be denoted as π π‘ 1 ...π‘ π . Proposition 3. Let π be a cluster of a cluster-acyclic net acnet.
βοΈ caused(trans(π , β’ π )).
β’ π ) β maxsseq(subnet acnet (π )).
4. scenario subnetacnet(π ) (maxtrans(π , β’ π )) = maxscenarios(subnet acnet (π )).
Since the transaction of a cluster are maximal step sequences generating all maximal scenarios of the subnet induced by the cluster, one can say that the behaviour of the cluster is described by its transactions.
Consider again the confused acyclic net in Figure 2(c). Figure 3 shows its two maximal clusters, π 1 = {π, π} and π 2 = {π, π}, together with their presets. We have π 1 β π 2 and π 2 ΜΈ β π 1 , and so the net is cluster-acyclic. Moreover, we have: maxtrans(π 1 , {π 1 }) = {{π}, {π}}, maxtrans(π 2 , {π 2 , π 3 }) = {{π}, {π}}, and maxtrans(π 2 , {π 2 }) = {{π}}.
In this section, acnet = (π, π, πΉ ) is a fixed cluster-acyclic net.
The encoding of a cluster-acyclic net acnet into an confusion-free acyclic net is based on negative places. For a place π β π , its negative image is denoted by π. Moreover, the original transitions are replaced by transitions representing transactions associated with clusters. We will proceed as follows:
β’ All places of acnet together with their markings are retained. In addition, for each place π β π , an empty place π is created.
168-187 β’ All transitions of acnet are removed. Instead, for each cluster π with marking π β β’ π and all its transactions π in maxtrans(π , π ) a new transition is created. Its preset are the places in the preset of π and the negative versions of all places in ( β’ π β π ). Its postset are all the places in the postset of π and the negative versions of places caused by π which are not caused by π (when such a place π is marked, one can be sure that the original place π will never be marked).
β’ Negative places which have no influence on the behaviour are removed.
The following definition provides full details of the encoding.
The confusion-free encoding of a cluster-acyclic net acnet = (π, π, πΉ ) is an acyclic net confree(acnet) = (π β² , π β² , πΉ β² ) constructed in three steps. First, we generate:
After that we delete all places π β π such that
Crucially, for every reachable marking π , if π β π , then π / β π . Note that confree(acnet) contains no negative images of initial nor final places of acnet. Moreover, if acnet is free-choice, then confree(acnet) is isomorphic to acnet.
Figure 3(b) shows the result of our encoding for the confused cluster-acyclic net in Figure 2(c). Despite the fact that there are two transitions based on cluster π 2 and transaction π = {π}, their presets are different, as one of them is associated with marking {π 2 } and the other with {π 2 , π 3 }. Note that the two copies of the original transition π, π‘ π and π‘ β² π , never occur in the same step sequence, as π 3 and π 3 cannot receive tokens in the same execution.
The behaviour of the constructed confusion-free acyclic net is closely linked to the original one. At first, both π‘ π and π‘ π are enabled. If π‘ π is executed, π‘ π and π‘ π become enabled. Executing π‘ π , on the other hand, produces tokens in places π 6 and π 3 , which enables π‘ β² π . The only behaviour in the original net that is not preserved is the possibility of executing π before π as this execution leads to ambiguous analysis of system behaviour as π is executed before π is enabled. Thus, even though π is initially enabled, its firing is delayed until the decision between π and π is taken. Therefore, the construction steps include delay and additional causality for some transitions similarly as in [14]. Figure 4 shows another example of our translation for a confused cluster-acyclic net. In this case, there are three maximal clusters (π 1 = {π, π}, π 2 = {π, π}, and π 3 = {π₯, π¦, π§}). The acyclic nets constructed above are confusion-free.
The proposition below shows that the behaviour of the constructed confusion-free net is closely linked to the original cluster-acyclic net. To show the this, for every set of transitions π of confree(acnet), we denote π π = βοΈ {π | π‘ π ,π,π½ β π }.
Proposition 5. Let acnet be a cluster-acyclic net. Compared to the encoding in [14], we feel that the encoding in this paper is simpler because of the following:
β’ The contact-free net resulting from the encoding uses the same net model as all acyclic nets (i.e., persistent places and extended markings are not needed).
β’ The number of negative places is smaller than in [14].
β’ There is no need to use dynamic nets as an intermediate step of the construction.
β’ We expect that our encoding will be much easier to comprehend and use by practitioners with relatively limited formal methods skills.
Additionally, one of the limitations of [14] is that only the case of backward deterministic nets has been addressed. In our work not reported here, we extended the encoding to the unfolding semantics, where more general cases can be considered. We do not expect the fact that our encoding works for a subclass of cluster-acyclic nets to be limiting in practical applications. This is based on the examples modelling investigations we evaluated, and also on the fact that in case of non-compliance it is always possible to require an investigator to provide additional information to 'repair' the net, or using other source of information, e.g., timing information associated with places and transitions.
In this section the acyclic net acnet is restricted to the class of binary synchronisation acyclic nets such that, for every transition π‘ β π , | β’ π‘| β©½ 2.
Let acnet = (π, π, πΉ ) be a well-formed backward deterministic cluster-acyclic net and π β clusters(acnet). A border of π is a minimal set of non-initial places π½ β β’ π such that
The sets of all borders and transactions of π are denoted by borders(π ) and trans(π ), respectively.
) is an acyclic net confree β² (acnet) = (π β² , π β² , πΉ β² ) constructed in three steps. First, we generate: 168-187
After that we delete all places π β π such that
Figure 6: All the clusters and their associated maximal transactions for the binary synchronised acyclic net in Figure 5, where π ππ = π‘ π ππππ ,{π,π},β , etc.
with symmetric confusion. It also shows its (sub-)clusters and the corresponding borders and maximal transactions. Figure 6 shows the clusters and their correspond encoded transitions derived from the maximal transactions associated with each cluster. The maximal cluster is maxclusters(π ππππ ) with its maximal transactions maxtrans(π ππππ ) = {{π ππ }, {π ππ }, {π ππ }}. Since all the pre-places of π 1 are included together with their output transitions, borders(π 1 ) = β . All the sub-clusters with their maximal transactions are shown in Figure 6. Note that borders(π π ) = {π 3 } = borders(π π ) and π β² π , π β² π are not in conflict hence, in the encoding π 3 will be split into π 3 and π β² 3 .
Basic definitions. Communication structured acyclic nets add communication to represent the interaction among several separated subsystems [10]. Each communication structured acyclic net is a set of acyclic nets with synchronous or asynchronous communication between their transitions implemented using extra nodes called buffer places (which provided a motivation for a/syn connections discussed, e.g., in [20]). When two transitions are subject to synchronous communication, they are always executed together, but under asynchronous communication they may be executed simultaneously or one of them after the other.
A communication structured acyclic net (or csa-net) is a tuple csan = (acnet 1 , . . . , acnet π , π, π ) (π β₯ 1) such that:
β’ acnet 1 , . . . , acnet π are well-formed acyclic nets with disjoint sets of nodes. We denote:
β’ π is a finite set of buffer places disjoint from π csan βͺπ csan and π β (πΓπ csan )βͺ(π csan Γπ) is a set of arcs. We also denote π csan = π, π csan = π .
β’ For every π β π, there is π§ β π such that π§π π, and if π‘π π and ππ π’ then π‘ and π’ belong to different acnet π 's. A scenario of a csa-net csan is a cso-net cson = (ocnet 1 , . . . , ocnet π , π β² , π β² ) such that: (i)
ocnet π β scenarios(acnet π ), for every 1 β€ π β€ π; (ii) π β² β π and π β² β π ; and (iii) pre cson (π‘) = pre csan (π‘) and post cson (π‘) = post csan (π‘), for every π‘ β π cson . Moreover, cson is maximal if there is no scenario cson β² satisfying π cson β π cson β² . We denote this by ocnet β scenarios(csan) and ocnet β maxscenarios(csan), respectively. Each scenario of a csa-net csan is identified by the set of its transitions π , and denoted by scenario csan (π ). 168-187 (a) Step sequence semantics. Let csan be a csa-net.
β’ markings(csan) = {π | π β π csan βͺ π csan } are the markings and π init csan = π init csan is the default initial marking.
β’ enabled csan (π ) = {π β steps(csan) | pre csan (π ) β π βͺ (post csan (π ) β© π)} are the steps enabled at π , and a step π enabled at π can be executed yielding a new marking
Let π 0 , . . . , π π (π β₯ 0) be markings and π 1 , . . . , π π be steps of a csa-net csan such that π πβ1 [π π β© csan π π , for every 1 β€ π β€ π.
β’ π = π 0 π 1 π 1 . . . π πβ1 π π π π is a mixed step sequence from π 0 to π π and π = π 1 . . . π π is a step sequence from π 0 to π π . We denote π 0 [πβ©β© csan π π and π 0 [πβ© csan π π , respectively. Moreover, π 0 [β© csan π π denotes that π π is reachable from π 0 .
β’ If π 0 = π init csan , then π β mixsseq(csan) is a mixed step sequence, π β sseq(csan) is a step sequence, and π π is a reachable marking of csan. Also, if π cannot be extended further, it is a maximal step sequence in maxsseq(csan).
In contrast to the step sequence of an acyclic net, where a step consists only of enabled transitions, in a csa-net an enabled step π can involve a/synchronous communications. That is, it can use not only the tokens of the places within acyclic nets, but also tokens in the buffer places generated in the same step [3].
In Figure 7(a), transitions π and π are communicating asynchronously, so they can be executed together, or π then π (but not π before π). On the other hand, π and π must be executed simultaneously as they are involved in synchronous communication. Therefore, some possible maximal step sequences are {π, π}π, π{π, π}, ππ{π, π }, and {π, π}{π, π }.
168-187 (a) Calculating probabilities in csa-nets. We now extend the notion of calculating probabilities in acyclic nets to well-formed csa-nets. In order to determine probabilities of alternate scenarios, each syn-cycle π is assigned a positive numerical weight π(π). Below we assume that
, where each π(π‘ π ) is the weight of transition π‘ π as before. We then define the probability of a syn-cycle π enabled at a reachable marking π as the weight of π divided the weight of all the enabled π β² β syncycles(csan) that are in conflict with π enabled at π , and then calculate the probability of a step π composed of syn-cycles π 1 , . . . , π π :
Then the probability of π = π 1 . . . π π is P csan (π) = P csan (π 0 , π 1 ) β’ . . . β’ P csan (π πβ1 , π π ), where π 0 , . . . , π πβ1 are such that π πβ1 [π π β© csan π π , for every 1 β€ π β€ π. Figure 8 illustrates the notion of csa-nets with weights (the weights are shown inside transitions in conflict). In Figure 8(a), there are two maximal scenarios of acnet 1 involving either π΄ or π΅, and also two scenarios for acnet 2 involving either πΆ or π·. Then csan has four scenarios: cson 1 = scenario csan ({π, π, π΄, πΆ}), cson 2 = scenario csan ({π, π, π΄, π·}), cson 3 = scenario csan ({π, π, π΅, πΆ}), and cson 4 = scenario csan ({π, π, π΅, π·}). There are also five syncycles: π 1 = {π, π }, π 2 = {π΄}, π 3 = {π΅}, π 4 = {πΆ}, and π 5 = {π·}.
The probabilities of scenarios are calculated through their maximal step sequences. For example, cson 1 has three: Confusion in probabilistic csa-nets. Consider the csa-net csan in Figure 8(b). The two possible scenarios are cson 1 = scenario csan ({π΄, π·}) and cson 2 = scenario csan ({π΅, πΆ}). Note that the latter scenario is executed in a single execution step due to a synchronous communication that forms the syn-cycle π 1 = {π΅, πΆ}. In scenario csan ({π΄, π·}) transitions belong to separate syn-cycles as π 2 = {π΄} and π 3 = {π·}, and it has three different maximal step sequences: π 1 = π 2 π 3 , π 2 = π 3 π 2 , and π 3 = (π 2 βͺ π 3 ). If π 1 is executed, then the probability of π 3 is 1 (π· is in this case is a certain transition), and so we get P csan (π 1 ) = (7/10) β’ 1 = 7/10. However, if π 2 is executed, then the resulting probability is (3/5) β’ 1 = 3/5. Hence, one cannot assign probability to cson 1 . The behaviour of this net is similar to the acyclic net with symmetric confusion in Figure 2(b). Here, π΄ and π· are independent transitions, but firing any of them has influence on the conflict set of the other. For example, firing π΄ decreases the conflict set of π·, which is why confusion arises.
A well-formed csa-net csan has a confusion at a reachable marking π if there are distinct syn-cycles π 1 , π 2 , π 3 β syncycles(csan) such that π 1 , π 2 , π 1 β π 2 β enabled csan (π ), and one of the following holds:
β’ π 1 # 0 π 3 # 0 π 2 and π 3 β enabled csan (π ).
β’ π 1 # 0 π 3 and π 3 β enabled csan (π β² ) β enabled csan (π ), where π [π 2 β© csan π β² .
We then denote symconfused csan (π, π 1 , π 2 , π 3 ) in the first (symmetric) case, and in the second (asymmetric) case we denote asymconfused csan (π, π 1 , π 2 , π 3 ). If csan has no confusion at all the reachable markings, then it is confusion-free.
For the csa-net in Figure 8
In this section, we assume that a well-formed csa-net csan has a confusion. To remove the confusion from csan, it is encoded into a single acyclic net. If the result is an acyclic wellformed net whose clusters are acyclic, the approaches proposed in Section 3.1 is applied. The encoding of csan is based on expanding the underlying transitions involved in asynchronous communications. Hence, buffer places are considered as regular places. For the transitions communicate synchronously, they are always combined together as one synchronised transition. The buffer places are removed for combined synchronised transitions. The transitions of csan are removed. Instead, for each syn-cycle π of csan, a transition π π is created (graphically, we put the transitions of π inside the box representing π π ). Its preset and postset are those of syn-cycle π except those involved in synchronous communication. The encoding is done as follows:
β’ All the places of csan together with their markings are retained.
β’ Each buffer place becomes a regular place.
β’ For each syn-cycle π β syncycles(csan), transition π π is created. Its presets are the pre-places of π except the buffer places in pre csan (π) β© post csan (π). Its post-sets are the post-places of π except the buffer places in pre csan (π) β© post csan (π). β’ The original buffer places with empty pre-sets are removed.
The following definition formally captures the details of the encoding. Let csan be a well-formed csa-net. Then acyclicnet(csan) = (π, π, πΉ ) is constructed so that:
β’ pre acnet (π π ) = pre csan (π) β π csan β© pre csan (π) β© post csan (π), for every π π β π , and
After that, the original buffer places with empty pre-sets are removed and, if acyclicnet(csan) is a well-formed acyclic net whose clusters are acyclic, we apply the construction from Section 2.
Figure 9(a) illustrates the notion of asymmetric confusion in a well-formed csa-net csan. The csan is composed of two acyclic nets, acnet 1 and acnet 2 , with asynchronous communication via buffer place π 1 . There are four syn-cycles: π 1 = {π}, π 2 = {π}, π 3 = {π}, and π 4 = {π}. These syn-cycles exhibit asymmetric confusion, as we have asymconfused csan (π 1 βͺ π 4 , π 2 , π 3 ). The acyclic net in Figure 9(b) is acyclicnet(csan). Its transitions are the transitions derived from the syn-cycles in Figure 9(a). Each syn-cycle π = {π₯} is removed and instead transition π π₯ is created. Note that despite the fact that there is an asynchronous communication between π and π, and so they might be executed simultaneously, they are encoded as singleton transitions and the buffer place π 1 as a regular place. Note also that the behaviour of the constructed acyclic net is closely linked to the original csa-net. First, scenario acnet (π π , π π ) and scenario acnet (π π , π π ) can be executed in any order. The only behaviour that is not preserved is the possibility of executing {π, π} as the corresponding syn-cycles, π 2 = {π} and π 3 = {π}, are not explicitly synchronised. Note that the transformed net in Figure 9(b) is cluster-acyclic.
The following result shows that the behaviour of the constructed acyclic net is equivalent to the original csa-net. Below, for a set of transitions π of the former, π π = βοΈ {π | π π β π }.
Let csan be a well-formed csa-net, and acnet = acyclicnet(csan). The first stage of the approach of removing confusion in csan of Figure 9(a) was already presented. We now present the second and third stages. Since the transformed acyclic net is cluster-acyclic, the techniques of the confusion-free encoding in Section 3.1 can be applied. There are two maximal clusters in this case: π 9, for the cluster-acyclicity constraint hold. Therefore, it is possible to reuse the proposed approach discussed in Section 3.1 after transforming csan into acyclicnet(csan). However, there is an intuition that cluster-acyclicity constraint can be checked at the level of csa-nets. This happens when asynchronous communications between the transitions of the component acyclic nets are unidirectional, in the following sense.
The net in Figure 9(a) adheres this condition. However, if exists an aβsynchronous communication between (π, π) β π csan as it is portrayed in Figure 10(a), then the csan is not cluster-acyclic. As a result, even if this net is transformed into an acyclic net, the approach proposed previously is not applicable as it depicted in Figure 10(b). In order to solve this issue, one can construct the equivalent acyclic net differently by combining all the transitions involve in asynchronous communications into one synchronised transition. For example, the transitions (π, π) β π csan and (π, π) β π csan whose communications are asynchronous in Figure 10(a) can be translated into one synchronised transition π ππ and π ππ respectively as the semantic of asynchronous communication allows those transitions to be executed together. Figure 10(c) shows the alternative encoding of csan in (a). Proposition 10. Let csan = (acnet 1 , . . . , acnet π , π, π ) (π β₯ 1) be a well-formed csa-net such that each acnet π is cluster-acyclic and, for each 1 β€ π < πππππ, there are no π‘ β π acnet π and π’ β π acnet π such that (π‘, π’) β π 2 csan . Then acyclicnet(csan) is a cluster-acyclic.
This paper investigated two approaches of removing confusion in acyclic nets, one of which is based on the work presented in [14]. Then the proposed solution was lifted to the level of csa-nets. There are some issues regarding the approach of handling the confusion in csa-nets as the acyclicity constraint may not be satisfied due to communication, and one may address these issues by combining transitions involved in synchronous communication. In the future work, we plan to extend the current work to behavioural structured occurrence nets [2], where the dynamic behaviour of a concurrent system is represented at different levels of abstraction.
Well-formed csa-nets. A csa-net csan is well-formed if each transition occurs in at least one step sequence and the following hold, for every step sequence π 1 . . . π π β sseq(csan): (i) post csan (π‘) β© post csan (π’) = β , for every 1 β€ π β€ π and all transitions π‘ ΜΈ = π’ β π π ; and (ii)
Intuitively, a well-formed csa-net does not have 'useless' transitions and no place is filled more than once in any given step sequence. Each cso-net is well-formed, and a csa-net is well-formed iff each transition occurs in at least one scenario, and each step sequence is a step sequence of at least one scenario.
Each step sequence π of a well-formed csa-net csan induces a scenario scenario csan (π) = scenario csan (π ), where π are the transitions occurring in π. Thus, different step sequences may generate the same scenario, and conversely, each scenario is generated by at least one step sequence. Moreover, two maximal step sequences generate the same scenario iff their executed transitions are identical.
In the case of cso-nets each executed step can unambiguously represented as a disjoint union of sub-steps which cannot be further decomposed.
A syn-cycle of a cso-net cson is a maximal non-empty set of transitions π β π csan such that, for all π‘ ΜΈ = π’ β π, (π‘, π’) β π + cson . The set of all syn-cycles is denoted by syncycles(cson). The idea behind the notion of syn-cycles is to capture fully synchronous communications [10]. In Figure 7(a), there is one non-singleton syn-cycle π = {π, π }.
The set of all syn-cycles syncycles(cson) is a partition of the transition set π cson . As stated below, each step occurring in step sequences of a cso-net can be partitioned into syn-cycles (in a unique way). Proposition 6. Let π be a reachable marking of a cso-net cson and π [π β© cson π β² . Then there are π 1 , . . . , π π β syncycles(cson)
This means, for example, that all reachable markings of a cso-net can be generated by executing syn-cycles rather than all the potential steps. Moreover, the same holds for every well-formed csa-net csan and the syn-cycles of its scenarios given by syncycles(csan) = βοΈ {syncycles(cson) | cson β scenarios(csan)}.
Let π be a reachable marking of a well-formed cso-net csan and π [π β© csan π β² . Then there are π 1 , . . . , π π β syncycles(csan
Conflict in csa-net. Let csan be a well-formed csa-net.
β’ Two syn-cycles π ΜΈ = π β² β syncycles(csan) are in direct forward conflict, denoted π# 0 π β² , if pre csan (π) β© pre csan (π β² ) ΜΈ = β .
β’ The conflict set of a syn-cycle π β syncycles(csan) enabled at a marking π of csan is given as conflset csan (π, π) = {π} βͺ {π β² β enabled csan (π ) | π# 0 π β² }.