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.
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 [
There are several works combining probabilistic reasoning and Petri nets. For example, in [
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
[
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
diferent 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 [
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
3 5 ℎ 4 discussed. We propose algorithms used for removing it in Section 3.
Basic definitions. An acyclic net is a triple acnet = (, , ), where and are disjoint ifnite sets of places and transitions, respectively, and ⊆ ( × ) ∪ ( × ) is a flow relation such that: (i) is nonempty and is acyclic; and (ii) for every ∈ , there is ∈ such that . Graphically, places are represented by circles, transitions by boxes, and arcs between the nodes represent the flow relation (see, e.g., Figure 1). If needed, we denote by acnet, etc. For all ∈ ∪ , ∙ = preacnet () = { | } and ∙ = postacnet () = { | } (and for a set of nodes , ∙ = ⋃︀∈ ∙ and ∙ = ⋃︀∈ ∙ ). Moreover, aincnitet = { ∈ | ∙ = ∅} are the initial places, and acnet is backward deterministic if |∙ | ≤ 1, for every place .
An occurrence net [
A scenario of acnet is an occurrence net ocnet such that: • ocnet ⊆ acnet and ocnet = acnet ∪ postacnet (ocnet), and • preocnet () = preacnet () and postocnet () = postacnet (), 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 scenarioacnet( ) = (, , acnet|( × )∪( × )), where = aincnitet ∪ ∙ . 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 aincnitet = aincnitet is the default initial marking. • steps(acnet) = { ⊆ | ̸= ∅ ∧ ∀ ̸= ∈ : ∙ ∩ ∙ = ∅} are the steps. • enabledacnet( ) = { ∈ steps(acnet) | ∙ ⊆ } are the steps enabled at a marking , and a step enabled at can be executed yielding a new marking ′ = ( ∪ ∙ ) ∖ ∙ .
This is denoted by [ ⟩acnet ′.
Let 0, . . . , ( ≥ 0) be markings and 1, . . . , be steps of an acyclic net acnet such that − 1[⟩acnet , for every 1 ≤ ≤ . • = 011 . . . − 1 is a mixed step sequence from 0 to and = 1 . . . is a step sequence from 0 to .
We denote 0[ ⟩⟩acnet and 0[ ⟩acnet , respectively, and 0[⟩acnet denotes that is reachable from 0. • If 0 = aincnitet, then ∈ mixsseq(acnet) is a mixed step sequence, ∈ sseq(acnet) is a step sequence, and is a reachable marking of acnet. Also, if cannot be extended further, it is a maximal step sequence in maxsseq(acnet).
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): (i) ∙ ∩ ∙ = ∅, for every 1 ≤ ≤ and all ̸= ∈ ; and (ii) ∙ ∩ ∙ = ∅, for all 1 ≤ < ≤ . 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 if 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 scenarioacnet( ) = scenarioacnet( ), where are the transitions occurring in . Thus, diferent 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 if their executed transitions are identical.
Let acnet = (, , ) be an acyclic net. • ̸= ∈ are in direct (forward) conflict , denoted #0, if ∙ ∩ ∙ ̸= ∅. • conflsetacnet(, ) = {} ∪ { ∈ enabledacnet( ) | #0} is the conflict set of ∈ enabled at a marking . • causedacnet() = { ∈ ∪ | +} are the nodes caused by ∈ ∪ .
• subnetacnet( ) = (∙ ∪ ∙ , , |(∙ × )∪( × ∙ )), for every ⊆ .
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. 0 ()
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:
() Pacnet(, ) = ∑︀∈conflsetacnet(,) () and Pacnet(, ) = ∏︁ Pacnet(, ) .
∈ Then, assuming 0[1⟩acnet 1 . . . − 1[⟩acnet , we define the probability of execution = 1 . . . as Pacnet( ) = Pacnet(0, 1) · . . . · Pacnet(− 1, ).
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: Pacnet(, ) = Pacnet( ′, ) = ()/(() + ( )) = 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: ocnet1 = scenario({ℎ, , }) and ocnet2 = scenario({ℎ, , }). Each can be executed by following diferent maximal step sequences: • ocnet1 has three executions: 1 = ℎ, 2 = ℎ, and 3 = ℎ{, }. Their probabilities are the same as we have: Pacnet( 1) = 1 · (6/9) · 1 = 6/9, Pacnet( 2) = 1 · 1 · (6/9) = 6/9 and Pacnet( 3) = 1 · ((6/9) · 1) = 6/9.
• ocnet2 has also three executions with probabilities equal to 3/9.
As a result, we can assign probabilities to the two scenarios: Pacnet(ocnet1) = 6/9 and
Pacnet(ocnet2) = 3/9. Note that Pacnet(ocnet1) + Pacnet(ocnet2) = 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 Pacnet(ocnet) = Pacnet( ), 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 [
A well-formed acyclic net acnet has a confusion [
• #0ℎ and ℎ ∈ enabledacnet( ′) ∖ enabledacnet( ), where [ ⟩acnet ′.
We then denote symconfusedacnet(, , , ℎ) in the first ( symmetric) case, and in the second (asymmetric) case we denote asymconfusedacnet(, , , ℎ) .
Proposition 1. Let acnet be a well-formed acyclic net and be its reachable marking. If it is the case that symconfusedacnet(, , , ℎ) or asymconfusedacnet(, , , ℎ) holds, then we have conflsetacnet(, ) ̸= conflsetacnet( ′, ) and ∈ enabledacnet( ′), where [ ⟩acnet ′. Figure 2(b) depicts a well-formed acyclic net acnet with symmetric confusion such that we have symconfusedacnet(, , , ), where = {1, 2}. Consider the scenario ocnet1 = scenarioacnet({, , }) with three executions ( 1 = , 2 = , and 3 = {, }). The probability of 1 is Pacnet( 1) = 1 · 7/10 · 1 = 7/10. However, if 2 is executed, then the resulting probability is Pacnet( 2) = 3/6 ̸= Pacnet( 1). Hence one cannot assign a probability to ocnet1. A similar conclusion can be reached for the acyclic net in Figure 2(c) which exhibits asymmetric confusion asymconfusedacnet(aincnitet, , , ).
A crucial property is that in a confusion-free acyclic net, conflict sets of transitions are constant for all the executions of each scenario.
Proposition 2. Let acnet be a confusion-free well-formed acyclic net. 1. If and ′ are two reachable markings of acnet such that [⟩acnet ′, then we have conflsetacnet(, ) = conflsetacnet( ′, ), for every ∈ enabledacnet( ) ∩ enabledacnet( ′). 2. If and ′ are two reachable markings of ocnet ∈ scenarios(acnet), then it is the case that conflsetacnet(, ) = conflsetacnet( ′, ), for every ∈ enabledocnet( ) ∩ enabledocnet( ′).
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 [
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 × ⊆ (#0)* and if ∙ ⊆ ∙ , then ∈ . It is maximal if there is no cluster ′ such that ′ ⊂ . Moreover, ⊏ is a relation on the maximal clusters such that ⊏ ′ if caused( ) ∩ ∙ ′ ̸= ∅. 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. 1. ( × ) ∩ + = ∅. 2. caused( ) = ⋃︀ caused(trans(, ∙ )). 3. maxtrans(, ∙ ) ⊆
maxsseq(subnetacnet( )). 4. scenariosubnetacnet( )(maxtrans(, ∙ )) = maxscenarios(subnetacnet( )).
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.
• 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.
Definition 1 (encoding cluster-acyclic net). The confusion-free encoding of a cluster-acyclic net acnet = (, , ) is an acyclic net confree(acnet) = ( ′, ′, ′) constructed in three steps. First, we generate:
| ∈ maxclusters(acnet) ∧ ⊆ ∙ ∧ ∈ maxtrans(, )} • ∙ = ∪ (∙ ∖ ) and ∙ = ∙ ∪ caused( ∖ ) ∩ , for every = ,,
After that we delete all places ∈ such that ∙ = ∅ or ∙ = ∅. ◇ 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 diferent, 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 [
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 = {, , }). 1 1 2 2 () 6 7 4 5 3 3 1 2 () 4 7 6 3 5 4 5 ′ ′′ ′
The acyclic nets constructed above are confusion-free.
Proposition 4. confree(acnet) is a confusion-free acyclic net, for every cluster-acyclic net acnet. 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. 1. For every ocnet ∈ maxscenarios(acnet), there is a maximal step sequence 1 . . . of the net confree(acnet) such that 1 . . . is a maximal step sequence of ocnet. 2. If 1 . . . is a step sequence of confree(acnet), then 1 . . . is a step sequence of acnet.
Compared to the encoding in [
Additionally, one of the limitations of [
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 (∙ )∙ ∖ ⊆ ∙ . A transaction is a maximal step included in . The sets of all borders and transactions of are denoted by borders( ) and trans( ), respectively.
Definition 2 (encoding binary synchronisation cluster-acyclic net). The confusion-free encoding of a binary synchronisation cluster-acyclic net acnet = (, , ) is an acyclic net confree′(acnet) = ( ′, ′, ′) constructed in three steps. First, we generate:
| ∈ clusters(acnet) ∧ ∈ trans( ) ∧ ∈ borders( )}. 1 1 3 2 4 (sub-)cluster borders( ) trans( ) = {, , , } ∅ {{ }, { }, { }} = {} {{3}} {{ }} = {, } {{2}} {{ }, { }} = {, , } {{4}} {{ }, { }} = {, } {{1}} {{ }, { }} = {} {{3}} {{ }} = {} {{1, 4}} {{ }} • ∙ = ∙ ∪ and ∙ = ∙ ∪ caused( ∖ ) ∩ , for every = ,,
After that we delete all places ∈ such that ∙ = ∅ or ∙ = ∅. Finally, we replace each remaining place ∈ with ∙ = {1, . . . , } by new places 1 , . . . , satisfying ∙ ( ) = ∙ ◇ and ( )∙ = {}, for every 1 ≤ ≤ .
Figure 5 shows a maximal cluster of some binary synchronisation acyclic net acnet 1 1 3 3 1 3 2 3 2 2 3 2 4 1 2 4 4 1 3 1 ′ 2 2 1 3 3 3 1 2 2 4 3 2 4 3 1 ′ 2 4 ′ ′ 3 1 ′ 4 4 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 [
A communication structured acyclic net (or csa-net) is a tuple csan = (acnet1, . . . , acnet, , ) ( ≥ 1) such that: • acnet1, . . . , acnet are well-formed acyclic nets with disjoint sets of nodes. We denote: csan = acnet1 ∪ · · · ∪ acnet , for ∈ {, , , init}. • is a finite set of bufer 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 diferent acnet’s.
For all ∈ csan ∪ csan ∪ csan, we denote precsan () = { | (, ) ∈ csan ∪ csan} and postcsan () = { | (, ) ∈ csan ∪ csan} (and similarly for sets of nodes).
The csan is backward deterministic (or bdcsa-net) if the component acyclic nets are backward deterministic and | precsan ()| = 1, for every ∈ csan. Moreover, csan is a communication structured occurrence net (or cso-net) if: (i) the component acyclic nets are occurrence nets; (ii) | precsan ()| = 1 and | postcsan ()| ≤ 1, for every ∈ csan; and (iii) no place in csan belongs to a cycle in the graph of csan. A cso-net exhibits backward determinism and forward determinism providing full and unambiguous information about the causal histories of all transitions it involves. Figure 7(b) shows a cso-net.
A scenario of a csa-net csan is a cso-net cson = (ocnet1, . . . , ocnet, ′, ′) such that: (i) ocnet ∈ scenarios(acnet), for every 1 ≤ ≤ ; (ii) ′ ⊆ and ′ ⊆ ; and (iii) precson () = precsan () and postcson () = postcsan (), 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 scenariocsan( ). Figure 7(b) shows a maximal scenario for the csa-net in Figure 7(a). acnet1 • markings(csan) = { | ⊆ csan ∪ csan} are the markings and cisnaitn = cisnaint is the default initial marking. • steps(csan) = { ⊆ csan | ̸= ∅ ∧ ∀ ̸= ∈ : precsan () ∩ precsan () = ∅} are the steps. • enabledcsan( ) = { ∈ steps(csan) | precsan ( ) ⊆ ∪ (postcsan ( ) ∩ )} are the steps enabled at , and a step enabled at can be executed yielding a new marking ′ = ( ∪ postcsan ( )) ∖ precsan ( ). This is denoted by [ ⟩csan ′.
Let 0, . . . , ( ≥ 0) be markings and 1, . . . , be steps of a csa-net csan such that − 1[⟩csan , for every 1 ≤ ≤ .
• = 011 . . . − 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 = cisnaitn, 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 bufer places
generated in the same step [
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 {, }{, }. 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) postcsan () ∩ postcsan () = ∅, for every 1 ≤ ≤ and all transitions ̸= ∈ ; and (ii) postcsan () ∩ postcsan ( ) = ∅, for all 1 ≤ < ≤ .
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 if 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 scenariocsan( ) = scenariocsan( ), where are the transitions occurring in . Thus, diferent 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 if their executed transitions are identical.
Syn-cycles. In the case of cso-nets each executed step can be 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 ̸= ∈ , (, ) ∈ c+son. 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 [
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) such that = 1 ⊎ · · · ⊎ and [1 . . . ⟩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)}.
Proposition 7. Let be a reachable marking of a well-formed cso-net csan and [ ⟩csan ′. Then there are 1, . . . , ∈ syncycles(csan) with = 1 ⊎ · · · ⊎ and [1 . . . ⟩cson ′.
Let csan be a well-formed csa-net. • Two syn-cycles ̸= ′ ∈ syncycles(csan) are in direct forward conflict , denoted #0′, if precsan () ∩ precsan (′) ̸= ∅. • The conflict set of a syn-cycle ∈ syncycles(csan) enabled at a marking of csan is given as conflsetcsan(, ) = {} ∪ {′ ∈ enabledcsan( ) | #0′}. 1 4 2 5 2
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 () = (1) + · · · + (), 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, . . . , : Pcsan(, ) =
() =1 Pcsan(, ) .
∑︀′∈conflsetcsan(,) (′) Pcsan(, ⨄︀=1 ) = ∏︀ Then the probability of = 1 . . . is Pcsan( ) = Pcsan(0, 1) · . . . · Pcsan(− 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 acnet1 involving either or , and also two scenarios for acnet2 involving either or . Then csan has four scenarios: cson1 = scenariocsan({, , , }), cson2 = scenariocsan({, , , }), cson3 = scenariocsan({, , , }), and cson4 = scenariocsan({, , , }). There are also five syncycles: 1 = {, }, 2 = {}, 3 = {}, 4 = {}, and 5 = {}.
The probabilities of scenarios are calculated through their maximal step sequences. For example, cson1 has three: 1 = {, }, 2 = {, }, and 3 = {, }{, }. All with the same probability 10/48, e.g., using 1 we get Pcsan(cson1) = 1 · (5/8) · (2/6) = 10/48. Also, cson2, cson3, cson4 each has three diferent executions and their probabilities are equal as well. As a result, one can assign probabilities to the four scenarios. Pcsan(cson2) = 1· (3/8)· (2/6) = 6/48, Pcsan(cson3) = 1 · (5/8) · (4/6) = 20/48, and Pcsan(cson4) = 1 · (3/8) · (4/6) = 12/48. Note that Pcsan(cson1) + Pcsan(cson2) + Pcsan(cson3) + Pcsan(cson4) = 1.
Confusion in probabilistic csa-nets. Consider the csa-net csan in Figure 8(b). The two possible scenarios are cson1 = scenariocsan({, }) and cson2 = scenariocsan({, }). Note that the latter scenario is executed in a single execution step due to a synchronous communication that forms the syn-cycle 1 = {, }. In scenariocsan({, }) transitions belong to separate syn-cycles as 2 = {} and 3 = {}, and it has three diferent maximal step sequences: 1 = 23, 2 = 32, 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 Pcsan( 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 cson1. 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 ∈ enabledcsan( ), and one of the following holds: • 1#03#02 and 3 ∈ enabledcsan( ).
• 1#03 and 3 ∈ enabledcsan( ′) ∖ enabledcsan( ), where [2⟩csan ′. We then denote symconfusedcsan(, 1, 2, 3) in the first ( symmetric) case, and in the second (asymmetric) case we denote asymconfusedcsan(, 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(b), we have symconfusedcsan(, 1, 2, 3).
Proposition 8. Let csan be a well-formed csa-net and be its reachable marking. If it is the cae that symconfusedcsan(, 1, 2, 3) or asymconfusedcsan(, 1, 2, 3), then we have conflsetcsan(, 1) ̸= conflsetcsan( ′, 1) and 1 ∈ enabledcsan( ′), where [2⟩csan ′.
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, bufer places are considered as regular places. For the transitions communicate synchronously, they are always combined together as one synchronised transition. The bufer 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 bufer place becomes a regular place. • For each syn-cycle ∈ syncycles(csan), transition is created. Its presets are the pre-places of except the bufer places in precsan () ∩ postcsan (). Its post-sets are the post-places of except the bufer places in precsan () ∩ postcsan (). acnet1 acnet2 () 1 1 4 () 1 4 1 ′
• The original bufer 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: • = csan ∪ csan and = { | ∈ syncycles(csan)}, • preacnet ( ) = precsan () ∖ csan ∩ precsan () ∩ postcsan (), for every ∈ , and • postacnet ( ) = postcsan () ∖ csan ∩ precsan () ∩ postcsan (), for every ∈ . After that, the original bufer 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, acnet1 and acnet2, with asynchronous communication via bufer place 1. There are four syn-cycles: 1 = {}, 2 = {}, 3 = {}, and 4 = {}. These syn-cycles exhibit asymmetric confusion, as we have asymconfusedcsan(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 bufer 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, scenarioacnet( , ) and scenarioacnet( , ) 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, = ⋃︀{ | ∈ }. Proposition 9. Let csan be a well-formed csa-net, and acnet = acyclicnet(csan). 1. For every cson ∈ maxscenarios(csan), there is a maximal step sequence 1 . . . of acnet such that 1 . . . is a maximal step sequence of cson. acnet1 1 2 () 1 4 1 2 2. If 1 . . . is a step sequence of acnet, then 1 . . . is a step sequence of 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: 1 = { , } and 2 = { , } with 1 ⊏ 2. The associated maximal transactions are: maxtrans( 1, {1}) = {{ }, { }}, maxtrans( 2, {4, 1}) = {{ }, { }}, and maxtrans( 2, {4}) = {{ }}. The net in Figure 9(c) represents the third stage, which is carried out similarly to the first approach for the net in Figure 3(b).
ure 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 diferently 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 = (acnet1, . . . , 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 (, ) ∈ c2san. 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 [