Vol-3170/paper10
Jump to navigation
Jump to search
Paper
| Paper | |
|---|---|
 edit
| |
| description | |
| id | Vol-3170/paper10 |
| wikidataid | Q117351470βQ117351470 |
| title | Probabilistic Communication Structured Acyclic Nets |
| pdfUrl | https://ceur-ws.org/Vol-3170/paper10.pdf |
| dblpUrl | https://dblp.org/rec/conf/apn/Almutairi22 |
| volume | Vol-3170βVol-3170 |
| session | β |
Probabilistic Communication Structured Acyclic Nets
Probabilistic Communication Structured Acyclic Nets
Nadiyah Almutairi1
1
School of Computing, Newcastle University
Science Square, Newcastle Helix, Newcastle upon Tyne NE4 5TG, U.K.
Abstract
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. csa-
nets are sets of acyclic nets which can communicate by means of synchronous and asynchronous inter-
actions.
Keywords
Petri net, acyclic net, communication structured acyclic net, conflict, confusion, cluster-acyclic net.
1. Introduction
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
PNSEβ22, International Workshop on Petri Nets and Software Engineering, Bergen, Norway, 2022
" n.m.r.almutairi2@newcastle.ac.uk (N. Almutairi)
Β© 2022 Copyright for this paper by its authors. Use permitted under Creative Commons License Attribution 4.0 International (CC BY 4.0).
CEUR
Workshop
Proceedings
http://ceur-ws.org
ISSN 1613-0073 CEUR Workshop Proceedings (CEUR-WS.org)
168
οΏ½Nadiyah Almutairi CEUR Workshop Proceedings 168β187
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. Cluster-
acyclic 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.
2. Acyclic Petri nets
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
169
οΏ½Nadiyah Almutairi CEUR Workshop Proceedings 168β187
π π
π1 π3 π4 π1 π3 π4
β β
π0 π0
π π π
π2 π5 π2 π5
(π) π (π) π
Figure 1: Acyclic net with initial marking (a), and one of its maximal scenarios (b).
discussed. We propose algorithms used for removing it in Section 3.
Basic definitions. An acyclic net is a triple acnet = (π, π, πΉ ), where π and π are disjoint
finite 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 π₯ β π βͺ π , β π₯ = pre βοΈacnet (π₯) βοΈ and π₯β = postacnet (π₯)init= {π§ | π₯πΉ π§} (and
= {π§ | π§πΉ π₯} β for a
set of nodes π, π = π₯βπ π₯ and π = π₯βπ π₯ ). Moreover, πacnet = {π β π | β π = β
}
β β β
are the initial places, and acnet is backward deterministic if |β π| β€ 1, for every place π.
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
β’ 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
init βͺ π β . Figure 1(b) shows a maximal scenario.
π = πacnet
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 πacnet
init = π init is the default initial marking.
acnet
β’ 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 β€ π β€ π.
170
οΏ½Nadiyah Almutairi CEUR Workshop Proceedings 168β187
β’ π = π0 π1 π1 . . . ππβ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 = πacnet init , 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
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
scenarioacnet (π) = scenarioacnet (π ), 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.
β’ π‘ ΜΈ= π’ β π 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 scenar-
ios, 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.
171
οΏ½Nadiyah Almutairi CEUR Workshop Proceedings 168β187
π π4
π2 π π1 π 4
1 π1
π0 β 7
π0 π
1 6 π π π3 π
π1 1
π π2 3 6 7
(π) (π)
(π) π π π2 π
3 3 3
Figure 2: Acyclic nets with weights: backward deterministic (a), with symmetric confusion (b), and
with asymmetric confusion (c).
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 (π, π‘) = βοΈ and Pacnet (π, π ) = Pacnet (π, π‘) .
π’βconflsetacnet (π,π‘) π(π’) π‘βπ
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 reach-
able 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 different maximal step se-
quences:
β’ 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 en-
sure 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.
172
οΏ½Nadiyah Almutairi CEUR Workshop Proceedings 168β187
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, exe-
cuting 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 {π, π } β enabledacnet (π ) and one of the following holds:
β’ π#0 β#0 π and β β enabledacnet (π ).
β’ π#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 (πacnet init , π, π, π).
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 [19].
3. Cluster-acyclic nets
The approach of removing confusion is based on identifying the choice points by applying the
concept of clusters.
173
οΏ½Nadiyah Almutairi CEUR Workshop Proceedings 168β187
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 }) = {{π}}.
3.1. Removing confusion from cluster-acyclic net (Approach A)
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.
174
οΏ½Nadiyah Almutairi CEUR Workshop Proceedings 168β187
π
1
π4
π4
π
π1
π
2 π3
π3 π‘π π‘β²π
π π1
(π) π π2 π‘π
π2 (π)
π3
π π‘π π‘π
Figure 3: (a) maximal clusters with their presets of the acyclic net in Figure 2(c), (b) encoding the
cluster-acyclic net of into a confusion-free acyclic net with negative place, where: π‘π = π‘π
1 ,{π},{π1 } ,
π‘π = π‘π
1 ,{π},{π1 } , π‘π = π‘π
2 ,{π},{π2 ,π3 } , π‘π = π‘π
2 ,{π},{π2 ,π3 } , and π‘β²π = π‘π
2 ,{π},{π2 } .
β’ 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 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 π‘π ,
175
οΏ½Nadiyah Almutairi CEUR Workshop Proceedings 168β187
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 = {π₯, π¦, π§}).
π4
π‘β²π§
π6
π6
π‘β²β²π§
π
1 π‘π
π
3 π1 π4
π
π1 π4 π‘π π‘π¦
π π₯ π2 π5
π
2 π3
π5 π‘π π‘π₯π§
π π¦
π2 π‘π
π3
π π5
π7 π§ π‘β²π₯π§
(π) (π) π7
Figure 4: (a) acyclic net with two types of confusion and its encoding to confusion-free acyclic net (b),
where: π‘π = π‘π
1 ,{π},{π1 } , π‘π = π‘π
1 ,{π},{π1 } , π‘π = π‘π
2 ,{π},{π2 } , π‘π = π‘π
2 ,{π},{π2 } , π‘π₯π§ = π‘π
3 ,{π₯,π§},{π3 ,π4 ,π5 } ,
π‘π¦ = π‘π
3 ,{π¦},{π3 ,π4 ,π5 } , π‘β²π₯π§ = π‘π
3 ,{π₯,π§},{π3 ,π4 ,π5 } , π‘π§ = π‘π
3 ,{π§},{π3 ,π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 [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).
176
οΏ½Nadiyah Almutairi CEUR Workshop Proceedings 168β187
β’ 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.
3.2. Removing confusion from cluster-acyclic net (Approach B)
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 }} {{ππ }}
Figure 5: A maximal cluster π
ππππ of a binary synchronisation acyclic net, and the borders and maximal
transactions of π
ππππ and its sub-clusters (all places are assumed to be non-initial).
177
οΏ½Nadiyah Almutairi CEUR Workshop Proceedings 168β187
β’ β π‘ = β π
βͺ π½ 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 π3 π2 π4 π1 π3 π2 π4
π π π π πππ πππ πππ
π
ππππ
π1 π3 π2 π1 π3 π2
π4
β² ππ
π π π πππ
π
πππ
π1 π3 π1 π3
π2
π π ππ ππβ²
π
ππ
π3 π2 π4
π3 π2 π4
π1
π π ππ ππ
π
ππ
π3 π1 π2
π3 π2
π4
π ππβ²
π
π
π2 π4 π3
π2 π4
π ππβ²
π
π
π1 π1 π3
π ππβ²
π
π
Figure 6: All the clusters and their associated maximal transactions for the binary synchronised acyclic
net in Figure 5, where πππ = π‘π
ππππ ,{π,π},β
, etc.
178
οΏ½Nadiyah Almutairi CEUR Workshop Proceedings 168β187
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 .
4. Communication structured acyclic nets
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 mo-
tivation 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 = (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 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.
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).
179
οΏ½Nadiyah Almutairi CEUR Workshop Proceedings 168β187
acnet1 π2 acnet1
π1 π π π4 π1 π4
β π3 β π3
π π π π
π1 π2 π3 π1 π2 π3
acnet2 acnet2
β π π β π π
π5 π6 π7 π5 π6 π7
(a) (b)
Figure 7: csa-net with initial marking (a), and cso-net with initial marking (b).
Step sequence semantics. Let csan be a csa-net.
β’ markings(csan) = {π | π β πcsan βͺ πcsan } are the markings and πcsan
init = π init is the
csan
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 β€ π β€ π.
β’ π = π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 = πcsan
init , 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 {π, π}{π, π }.
180
οΏ½Nadiyah Almutairi CEUR Workshop Proceedings 168β187
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 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 scenariocsan (π) =
scenariocsan (π ), 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.
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 π‘ ΜΈ= π’ β π, (π‘, π’) β π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) such that π = π1 β Β· Β· Β· β ππ and π [π1 . . . ππ β©cson π β² .
This means, for example, that all reachable markings of a cso-net can be generated by ex-
ecuting 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 π β² .
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 precsan (π) β© precsan (π β² ) ΜΈ= β
.
β’ The conflict set of a syn-cycle π β syncycles(csan) enabled at a marking π of csan is
given as conflsetcsan (π, π) = {π} βͺ {π β² β enabledcsan (π ) | π#0 π β² }.
181
οΏ½Nadiyah Almutairi CEUR Workshop Proceedings 168β187
acnet1 acnet1
5 7 π2
π1 π2 π3 π1
π΄ π΄
π
π΅ π΅
3 3 π3
(a) π1 π2 π1 π2 (b)
acnet2 acnet2
2 2 π6
π4 π5 π6 π4
πΆ πΆ
π
π· π·
4 3 π7
Figure 8: Probabilistic communication structured acyclic nets.
Calculating probabilities in csa-nets. We now extend the notion of calculating probabil-
ities 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 (π, π) = βοΈ β² Pcsan (π, π=1 ππ ) = π=1 Pcsan (π, ππ ) .
π β² βconflsetcsan (π,π) π(π )
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 syn-
cycles: π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 different 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
182
οΏ½Nadiyah Almutairi CEUR Workshop Proceedings 168β187
that the latter scenario is executed in a single execution step due to a synchronous commu-
nication that forms the syn-cycle π1 = {π΅, πΆ}. In scenariocsan ({π΄, π·}) 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 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 #0 π3 #0 π2 and π3 β enabledcsan (π ).
β’ π1 #0 π3 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 π β² .
5. Removing confusion from csa-nets
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 well-
formed 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 precsan (π) β© postcsan (π). Its post-sets are the
post-places of π except the buffer places in precsan (π) β© postcsan (π).
183
οΏ½Nadiyah Almutairi CEUR Workshop Proceedings 168β187
acnet1
π
π1 π
1
π
ππ
π1
π1 π
2 π
(π) (π) ππ ππ (π) π‘ ππ π‘ππβ²
acnet2 π1
π1 π4 π‘ ππ
π
π4 π4 π1
π ππ π‘ππ π‘ ππ
Figure 9: Confused csa-net (a), its equivalent acyclic net (b), and its confusion-free acyclic net (c).
β’ 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:
β’ π = πcsan βͺ πcsan and π = {ππ | π β syncycles(csan)},
β’ preacnet (ππ ) = precsan (π) β πcsan β© precsan (π) β© postcsan (π), for every ππ β π , and
β’ postacnet (ππ ) = postcsan (π) β πcsan β© precsan (π) β© postcsan (π), for every ππ β π .
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, acnet1 and acnet2 , 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 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 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, 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.
184
οΏ½Nadiyah Almutairi CEUR Workshop Proceedings 168β187
acnet1
ππ π1
π
π1
ππ π1 π1
π π1 πππ
(π) ππ
(π) π2 π1 (π)
acnet2 π4
π4 πππ
π ππ
π4
π ππ π2 ππ π2
Figure 10: csa-net (a), its encoding into acyclic net which is not cluster-acyclic (b), and another
encoding (c).
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 ap-
plied. 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 Fig-
ure 9(c) represents the third stage, which is carried out similarly to the first approach for the
net in Figure 3(b).
Asynchronous communication and csa-net acyclicity. Consider again the nets in Fig-
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 com-
munication 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 = (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
185
οΏ½Nadiyah Almutairi CEUR Workshop Proceedings 168β187
2 . Then acyclicnet(csan) is a cluster-acyclic.
π’ β πacnetπ such that (π‘, π’) β πcsan
6. Conclusion
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.
References
[1] B. Randell, M. Koutny, Failures: Their definition, modelling and analysis, in: C. B.
Jones, Z. Liu, J. Woodcock (Eds.), Theoretical Aspects of Computing - ICTAC 2007, 4th
International Colloquium, Macau, China, September 26-28, 2007, Proceedings, volume
4711 of Lecture Notes in Computer Science, Springer, 2007, pp. 260β274.
[2] M. Koutny, B. Randell, Structured occurrence nets: A formalism for aiding system failure
prevention and analysis techniques, Fundam. Inform. 97 (2009) 41β91.
[3] B. Li, Visualisation and analysis of complex behaviours using structured occurrence nets,
2017.
[4] T. Alharbi, Analysing and visualizing big data sets of crime investigations using structured
occurrence nets (PhD thesis), 2016.
[5] P. Missier, B. Randell, M. Koutny, Modelling provenance using structured occurrence
networks, in: P. Groth, J. Frew (Eds.), Provenance and Annotation of Data and Processes -
4th International Provenance and Annotation Workshop, IPAW 2012, Santa Barbara, CA,
USA, June 19-21, 2012, Revised Selected Papers, volume 7525 of Lecture Notes in Computer
Science, Springer, 2012, pp. 183β197.
[6] A. Bhattacharyya, B. Li, B. Randell, Time in structured occurrence nets, in: L. Cabac,
L. M. Kristensen, H. RΓΆlke (Eds.), Proceedings of the International Workshop on Petri Nets
and Software Engineering 2016, ToruΕ, Poland, June 20-21, 2016, volume 1591 of CEUR
Workshop Proceedings, CEUR-WS.org, 2016, pp. 35β55.
[7] N. Almutairi, M. Koutny, Verification of communication structured acyclic nets using
SAT, in: M. KΓΆhler-Bussmeier, E. Kindler, H. RΓΆlke (Eds.), Proceedings of the International
Workshop on Petri Nets and Software Engineering 2021, volume 2907 of CEUR Workshop
Proceedings, CEUR-WS.org, 2021, pp. 175β194.
[8] M. Koutny, B. Randell, Structured occurrence nets: incomplete, contradictory and uncertain
failure evidence, Technical Report, School of Computing Science, Newcastle University,
2009.
[9] D. Koller, N. Friedman, Probabilistic graphical models: principles and techniques, MIT
press, 2009.
[10] J.-P. Katoen, D. Peled, Taming Confusion for Modeling and Implementing Probabilistic
186
οΏ½Nadiyah Almutairi CEUR Workshop Proceedings 168β187
Concurrent Systems, volume 7792 of Lecture Notes in Computer Science, Springer, Berlin,
2013, pp. 411β430.
[11] D. Varacca, H. VΓΆlzer, G. Winskel, Probabilistic event structures and domains, Theor.
Comput. Sci. 358 (2006) 173β199.
[12] S. Abbes, A. Benveniste, True-concurrency probabilistic models: Markov nets and a law of
large numbers, Theor. Comput. Sci. 390 (2008) 129β170.
[13] D. Varacca, M. Nielsen, Probabilistic Petri nets and Mazurkiewicz equivalence, 2003.
[14] R. Bruni, H. C. Melgratti, U. Montanari, Concurrency and probability: Removing confusion,
compositionally, CoRR abs/1710.04570 (2017).
[15] X. Chen, Z. Li, N. Wu, A. Al-Ahmari, E.-T. A.M., E. Abouel Nasr, Confusion diagnosis
and avoidance of discrete event systems using supervisory control, IEEJ Transactions on
Electrical and Electronic Engineering 11 (2015) n/aβn/a.
[16] X. Chen, Z. Li, N. Wu, A. M. Al-Ahmari, A. M. El-Tamimi, E. S. Abouel Nasr, Confusion
avoidance for discrete event systems by P/E constraints and supervisory control, IMA
Journal of Mathematical Control and Information 33 (2014) 309β332.
[17] R. D. Bamberg, Non-Deterministic Generalised Stochastic Petri Nets Modelling and Analy-
sis, 2012.
[18] X. Chen, Z. Li, N. Wu, A. M. Al-Ahmari, A. M. El-Tamimi, E. S. Abouel Nasr, Confusion
avoidance for discrete event systems by P/E constraints and supervisory control, IMA
Journal of Mathematical Control and Information 33 (2016) 309β332.
[19] J. Desel, J. Esparza, Free Choice Petri Nets, volume 40 of Cambridge Tracts in Theoretical
Science, Springer, 1995.
[20] J. Kleijn, M. Koutny, M. Pietkiewicz-Koutny, Regions of Petri nets with a/sync connections,
Theor. Comput. Sci. 454 (2012) 189β198.
187
οΏ½