Paper[edit]

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[edit]

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
�

Probabilistic Communication Structured Acyclic Nets[edit]

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
�