Communication Structure Acyclic Nets (CSA-nets) are a Petri net-based model used to represent the execution behaviour of Complex Evolving Systems (CESs). CSA-nets consist of sets of acyclic nets that communicate with each other through a set of buffer places. However, this can generate an excessive number of buffer places, making the model hard to visualize and analyse. Additionally, having several components that perform similarly can result in the development of a complicated model. This paper introduces two extensions for CSA-nets, which are used to depict the relationships between interacting systems' components represented by sets of acyclic nets. Specifically, it introduces a way of folding buffer places to address the issue of a large number of buffer places. In addition, it introduces parameterisations for CSA-nets using multi-coloured tokens to extend places to accept multiple tokens distinguished by parameters. The combination of these techniques should lead to improved visualization and analysis of large and complex CSA-nets. We apply mechanisms found in the domain of coloured Petri nets.
Today’s world is associated with large amounts of data stored in servers, hard drives, and the cloud, among other places. Regardless of the discipline, modern technologies need to be able to process this data, whether it relates to education, health, crime, or anything else. In particular, there are enormous amounts of data available, and this quantity is only going to continue to grow due to advances in digital sensors, communications, and storage that generate vast amounts of data. This needs the integration and interaction of several subsystems, including data storage, processing, analysis, and visualization, among others.
A complex evolving system (CES) is composed of a large number of subsystems that interact
with each other concurrently. Such a system is often characterized by a dynamically changing
structure and features, as well as having intricate and large behavioral patterns. In other words,
when new features are added, the behavior of the entire system may be affected. That is, these
systems are highly complex in terms of interpreting their behavior and visualizing it [
Structured occurrence nets (SONs)[
The particular formal model used in this paper is communication structured acyclic nets
(CSA-nets) and is used in [
One example of CES systems where there is a large amount of data is cybercrime investigation.
In such cybercrime applications, the generated data is of high importance, and high-quality
analysis is needed. Proper visualization of CSA-nets with a large amount of data would result
in a much better understanding for the investigators and the possibility of linking crime events
and locations with data representations that help detect crime. This is done through extracting
valuable knowledge from large and complex data and identifying useful information from a
variety of data sources. A major specific benefit to cybercrime investigation is that such analysis
allows early detection of crimes, hence crime prevention. The current work is an attempt in this
direction, i.e., visualization improvement [
CSA-nets visualization framework allows for the analysis of complex systems. The hurdle is that managing large amounts of data is not an easy task. In other words, with the high number of components (acyclic nets), there is a large number of buffer places leading to difficult analysis and visualization. What also adds to this complexity is that CSA-nets are limited to presenting only one token in a transition at any given time, which, in turn, limits its ability to represent, e.g., p1 d e
p4 p2 p5
q1 p7 a b c p3 p6 p8 q2
several similar processes at the same time. In general, system parameterisation is used to examine how changing input parameters affects the output of a system. By defining a set of different parameters, one can obtain a corresponding set of different outputs without the need to rebuild the system model every time. This advantage allows for the preparation of the system model once and its execution several times, providing insights into the relationship between inputs and outputs. It also simplifies the system tracing process by automatically changing the results of one parameter when other parameters are changed.
This paper aims to improve the visualization of CSA-nets by addressing two issues. First, it
extends the work done in [
This section presents notions related to acyclic nets and communication structured acyclic nets. An acyclic net is a triple acnet = (P, T, F ), where P(= Pacnet) and T (= Tacnet) are disjoint finite sets of places and transitions, respectively, and F (= Facnet) is the flow relation included in (P × T ) ∪ (T × P) such that: (i) P is nonempty; (ii) F is acyclic; and (iii) for every t ∈ T , there are p, q ∈ P such that pFt and tF q. For every node x ∈ P ∪ T ,
preacnet (x) = {z | zF x} and postacnet (x) = {z | xF z} and similarly for sets of nodes.
The markings of acnet, denoted by markings(acnet), are the subsets of P. Hence, the nets we are dealing with are safe. 1 The default initial marking is Maincintet = {p ∈ P | preacnet (p) = ∅}, and the steps are
steps(acnet) = {U ∈ 2T | ∀t ̸= u ∈ U : preacnet (t) ∩ preacnet (u) = ∅} .
Graphically, places are represented by circles, transitions by boxes, arcs between the nodes represent the flow relation, and markings are indicated by black tokens placed inside the corresponding circles.
yield M′ = (M ∪ postacnet (U )) \ preacnet (U ).
To capture the behaviour of acyclic nets (and other nets later on), we use step sequences, involving reachable markings and executed steps. Let (Maincintet =)M0, M1 . . . , Mk (k ≥ 0) be markings and U1, . . . ,Uk be steps of acnet such that we have Mi− 1[Ui⟩acnet Mi, for every 1 ≤ i ≤ k. Then
µ = M0U1M1 . . . Mk− 1UkMk is a mixed step sequence of acnet. This is denoted by µ ∈ mixsseq(acnet).
A basic consistency criterion applied to acyclic nets is well-formedness, and acnet is wellformed if the following hold, for every M0U1M1 . . . Mk− 1UkMk ∈ mixsseq(acnet): • postacnet (t) ∩ postacnet (u) = ∅, for every 1 ≤ i ≤ k and all t ̸= u ∈ Ui.
• postacnet (Ui) ∩ postacnet (Uj) = ∅, for all 1 ≤ i < j ≤ k.
Intuitively, in a step sequence of a well-formed acyclic net, no place receives a token more than once. This ensures an unambiguous representation of causality in the behaviour of acnet. Note that well-formedness is stronger than safeness. In particular, it prevents the same transition from executing more than once. So, having an acyclic net represents a single execution, meaning that each transition can only be executed once.
A communication structured acyclic net (or CSA-net) is a tuple csan = (acnet1, . . . , acnetn, Q,W ) (n > 1) such that: 1. acnet1, . . . , acnetn are well-formed acyclic nets with disjoint sets of nodes (i.e., places and transitions). We also denote: 1t ̸= u ∈ Umeans t, u ∈ Uand t ̸= u
Pcsan Tcsan Fcsan = = =
Pacnet1 ∪ · · · ∪ Tacnet1 ∪ · · · ∪ Facnet1 ∪ · · · ∪
Pacnetn Tacnetn
Facnetn .
3. W ⊆ (Q × Tcsan) ∪ (Tcsan × Q) is a set of arcs. 4. For every buffer place q: (i) there is at least one transition t such that tW q; and (ii) if tW q and qWu then transitions t and u belong to different component acyclic nets.
That is, in addition to requiring the disjointness of the component acyclic nets and the buffer places, it is required that buffer places pass tokens between different acyclic nets. For a node x ∈ Pcsan ∪ Tcsan ∪ Qcsan, precsan (x) = postcsan (x) = {y | y Fcsan x ∨ yW x} {y | x Fcsan y ∨ xW y}} denote the direct predecessors and successors of x, respectively.
initial marking is Mcinsaitn = Maincintet1 ∪ · · · ∪ Maincintetn , and the steps are: steps(csan) = {U ∈ 2Tcsan | ∀t ̸= u ∈ U : precsan (t) ∩ precsan (u) = ∅} .
A step U of csan is enabled at marking M if It can then be executed and yield precsan (U ) ⊆
M ∪ (postcsan (U ) ∩ Q).
M′ = (M ∪ postcsan (U ) \ precsan (U ).
Note that here enabling a step amounts to having all input places belonging to the component acyclic nets present in a global state. Moreover, if an input buffer place is not present, then it must be an output place of a transition belonging to the step. Such a mechanism allows one to synchronise transitions coming from different component acyclic nets. The same mechanism of simultaneous output to and input from a place is not available within the component acyclic nets.
The dynamic behaviour of csan is captured by mixed step sequences, as follows. Let (Mcinsaitn =)M0, M1 . . . , Mk (k ≥ 0) be markings and U1, . . . ,Uk be steps of csan such that we have
µ = M0U1M1 . . . Mk− 1UkMk is a mixed step sequence of csan. This is denoted by µ ∈ mixsseq(csan).
Again, a basic consistency criterion is well-formedness, and csan is well-formed if the following hold, for every M0U1M1 . . . Mk− 1UkMk ∈ mixsseq(csan): • postcsan (t) ∩ postcsan (u) = ∅, for every 1 ≤ i ≤ k and all t ̸= u ∈ Ui.
• postcsan (Ui) ∩ postcsan (Uj) = ∅, for all 1 ≤ i < j ≤ k.
Example 1. Figure 1 shows a CSA-net. Some of its mixed step sequences are: µ1 µ2 µ3 = = = {p1, p7}{d}{p2, p5, p7}{a, b, c}{p3, p6, p8}{e}{p4, p8} {p1, p7}{d}{p2, p5, p7}{a}{p3, q1, p5, p7}{b, c}{p3, p6, p8}{e}{p4, p8} {p1, p7}{d}{p2, p5, p7}{a, b}{p3, q1, p6, q2, p7}{e}{, q1, q2, p4, p7}{c}{p4, p8}.
The concept of parameterisation has gained significant attention in the field of system modelling,
as it provides a means to monitor a system’s operation under different conditions. Prior to the
use of parameterisation, investigating systems under different conditions was a difficult task. In
order to address this issue, [
Addressing large scale problems, characterised by a large amount of data, as one unit is a
difcfiult task and makes the model under investigation hard to interpret and visualise. So, the
one proposed solution is to tackle such a problem by dividing it into smaller units that can
later be put together to form the entire system. In the meantime, modelling is needed to better
understand larger systems. This is because modelling reduces debugging time and allows the
reuse of frequently used components (like events and conditions) which, in turn, saves time
and effort. Moreover, modelling assures the validity of the system as modules that have been
extensively tested in one environment are likely to run in a similar environment as expected, so
reuse increases the reliability of accuracy. This is known as parameterisation concept [
More recently, the modeling of biological systems has become a challenging problem due to the
large-scale data involved. As a result, Petri nets have been used to model biological systems. This
is accomplished by representing a group of similarly behaving components as one component,
with each of these components being represented by a specific color, thereby distinguishing them.
This provides a compact representation of a complex system while maintaining its semantic
meaning. Additionally, the colored Petri net has another significant advantage, as adding a new
component is an easy task by simply adding a new color. With these benefits in mind, colored
Petri nets have been successfully employed in discriminating metabolites, modeling multicellular
systems, and analyzing spatial diffusion in biological systems [
Another direction of applying colored Petri nets is to focus on concurrent systems. However,
concurrent systems often involve a vast amount of highly detailed data, which can be
overwhelming. Moreover, every single step is usually described in detail, which can be distracting for
the modeler. To address this, animation graphics have been employed for visualization, which
provides more appropriate feedback [
This section will extend the work done in [
Figure 3 presents another example of using master buffer places. The image shows a wellstructured display, which avoids any crossing of the arcs adjacent to the original buffer places. This improves the representation of the CSA-net. Introducing a single master buffer place, however, may lead to unwanted crossing of arcs, as illustrated in Figure 3. If a single master buffer place is added to the CSA-net in Figure 3, the crossing would be unavoidable unless placed ‘outside’ the outline of the underlying occurrence nets, which is generally unacceptable, since the individual acyclic nets would be too large to fit in a single screen. One way to address this issue is to generate multiple master buffer places, as shown in Figure 3. This raises an interesting problem of determining the number and placement of the master buffer places automatically or semi-automatically to optimize the visualization of CSA-nets. This problem is the subject of our ongoing study.
With the above in mind, we are able to improve the visualization of CSA-nets by folding the set of buffer places into master buffer places. In this section, we will use the same concept of folding to fold the components of CSA-nets while preserving their main rules (as being acyclic). For example, Figure 4 depicts a parameterised version of a very simple acyclic nets where two concurrent parts are folded (collapsed) into a single parameterised structure. Clearly, the two parts have the same net structure. Thus, the idea is to determine the set of components that are behaving identically, and then represent them as a single substructure. This uses typed parameters to achieve the desired effect through passing tokens to parameterised transition. That is, this process can allow for the reuse of the model multiple times and increase comprehension, making larger systems under investigation easier to handle. (Formally, ι (r1) = {p1, p3}, ι (t1) = {a, b} and ι (r2) = {p2, p4}.) This extension can have positive effect on the model in both increasing the abstraction and visualisation of the model under investigation.
In this section, we provide a full formalisation of the approach proposed in this paper. We first introduce parameterised acyclic nets, and then parameterised communication structured acyclic nets.
We first introduce a parameterised version of acyclic nets. Definition 1 (parameterised acyclic net). A parameterised acyclic net (or PA-net) is a tuple pacnet = (P, T, F, acnet, ι, col), where: • acnet = (P′, T ′, F′) is a well-formed acyclic net, and col is a finite set of colours (or parameters). • P (P ̸= ∅) and T are disjoint finite sets of places and transitions, respectively. • F ⊆ (P × T ) ∪ (T × P) is a flow relation .
• ι : P ∪ T → 2P′∪T ′ \ {∅} is a node annotation mapping.
We denote, for all x ∈ P ∪ T , p ∈ P′, and u ∈ T ′: prepacnet (x) = {z | zFx} postpacnet (x) = {z | xFz} We then assume that the following hold. prepacnet (u, p) = ι(p) ∩ preacnet (u) postpacnet (u, p) = ι(p) ∩ postacnet (u) . 1. (P ∪ T ) ∩ (P′ ∪ T ′) = ∅, ⋃︁ ι(P) = P′, and ⋃︁ ι(T ) = T ′. 2. For all t ∈ T and u ∈ ι(t) we have the following, where ⨄︁ is assumed to be applied to non-empty sets:2 3. If u ∈ T ′ and R ⊆ P are such that preacnet (u) = postacnet (u) = ⨄︁{prepacnet (u, p) | p ∈ prepacnet (t)} ⨄︁{postpacnet (u, p) | p ∈ postpacnet (t)} .
preacnet (u) = ⨄︂{prepacnet (u, p) | p ∈ R} then there is t ∈ T such that u ∈ ι(t) and prepacnet (t) = R. 4. For every p ∈ P,
ι(p) \ Maincintet = ⋃︂{postpacnet (u, p) | u ∈ ⋃︂ ι(prepacnet (p))} . 5. For every p ∈ Paincnitet, there is exactly one place pinit ∈ P such that p ∈ ι(pinit).
Note that we do not assume that F is acyclic since the acyclity of the behaviour of acnet will lead to the acyclicity of the behaviour of pacnet.
Example 2. Figure 4 shows a parameterised acyclic net
pacnet = (P, T, F, acnet, ι, col) such that and
acnet = ({p1, p2, p3, p4}, {a, b}, {(p1, a), (a, p2), (p3, b), (b, p4)}), P = {r1, r2} ι(r1) = {p1, p3} col = {1, 2}.
T = {t} ι(t) = {a, b}
F = {(r1,t), (t, r2)} ι(r2) = {p2, p4} We then have, for example, prepacnet (a, r1) = {p1} and postpacnet (b, r2) = {p4}. 2Thus, for example, {prepacnet (u, p) | p ∈ prepacnet (t)} is a partition of preacnet (u). p1 p3 a b p2 p4
specifies the places of acnet which can be ‘present’ in p ∈ P in the executions of pacnet. Definition 1(2) means that, for each mode u ∈ ι(t), the arcs incoming to t ‘deliver’ the input places of u, and similarly for the output arcs. Definition 1(3) means that, for any potential distribution of the ‘preset’ of u ∈ Tacnet, there is a transition t ∈ T with the mode u which can input this distribution of the preset. Definition 1(4) states that ι(p) is determined by the modes of the input transitions.
To capture the behaviour of pacnet, we will use parameterised places and transitions: Ppacnet = Tpacnet = {(p, r, c) ∈ P′ × P × col | p ∈ ι(r)} {(u,t, c) ∈ T ′ × T × col | u ∈ ι(t)} Intuitively, (p, r, c) is an instance of place p of the original acyclic net coloured by c, which resides in the place r of pacnet. (Another way of interpreting (p, r, c) is that it represents coloured token (p, c) present in the place r.) Similarly, (u,t, c) represents mode in which transition t operates as if it were transition u of the original acyclic net coloured by c. Moreover, we denote for (u,t, c) ∈ Tpacnet (and similarly for subsets of Tpacnet): prepacnet ((u,t, c)) = ⋃︁{preacnet (u, p) × { p} × { c} | p ∈ prepacnet (t) ∧ c ∈ col} postpacnet ((u,t, c)) = ⋃︁{postacnet (u, p) × { p} × { c} | p ∈ postpacnet (t) ∧ c ∈ col} . Intuitively, prepacnet ((u,t, c)) and postpacnet ((u,t, c)) determine the tokens which transition t in mode u consumes and produces when fired.
Example 3. For the PAN-net in Figure 4 we have, for example, prepacnet ((a,t, 1)) = {(p1, r1, 1)} and prepacnet ((b,t, 2)) = {(p4, r2, 2)}.
The markings of pacnet, denoted by markings(pacnet), are the subsets of Ppacnet. The default initial marking is:
Mpinaictnet = {(p, pinit, c) | p ∈ Maincintet ∧ c ∈ col}. (1)
M(r) = {(p, c) | (p, r, c) ∈ M} = {(p1, c1), . . . , (pk, ck)}, and in the diagrams place p1:c1, . . . , pk:ck inside p. In other words, p1:c1, . . . , pk:ck are coloured tokens present in p at marking M. Moreover, each place p of pacnet is annotated by p:ι(p), and each transition t by ι(t). The same convention is used for the channel places and CSA-nets later on. We also say that M is colour-safe if M(r) ∩ M(s) = ∅, for all r ̸= s ∈ P. Note that Mpinaictnet is colour-safe.
The steps of pacnet, denoted by steps(pacnet), are:
steps(pacnet) = {U ∈ 2Tpacnet | ∀t ̸= u ∈ U : prepacnet (t) ∩ prepacnet (u) = ∅} .
yield
M′ = (M ∪ postpacnet (U )) \ prepacnet (U ).
This is denoted by M[U ⟩pacnet M′. Let (Mpinaictnet =)M0, M1 . . . , Mk (k ≥ 0) be markings and
M. It can then be executed and is a mixed step sequence of pacnet. This is denoted by µ ∈ mixsseq(pacnet). Moreover, µ is well-formed if the following hold: • postpacnet (t) ∩ postpacnet (u) = ∅, for every 1 ≤ i ≤ k and all t ̸= u ∈ Ui.
• postpacnet (Ui) ∩ postpacnet (Uj) = ∅, for all 1 ≤ i < j ≤ k.
Example 4. The initial marking of the PA-net Figure 4 is
Mpinaictnet = {(p1, r1, 1), (p1, r1, 2), (p3, r1, 1), (p3, r1, 2)}.
Two of its mixed step sequences are: where:
Mpinaictnet {(a,t, 2)} M1 {(b,t, 2), (b,t, 1)} M2 {(a,t, 1)} M3 Mpinaictnet {(b,t, 1), (a,t, 2)} M4 {(a,t, 1), (b,t, 2)} M3,
To express full consistency between the behaviour of pacnet and that of the underlying acyclic net acnet, we need a notion of projection of the steps and markings of pacnet onto the steps and markings of acnet.
For every subset X of Ppacnet ∪ Tpacnet and c ∈ col, X ↓ c = {x | (x, y, c) ∈ X }. Moreover, for every sequence ξ = X1 . . . Xk of subsets of Ppacnet ∪ Tpacnet, we denote ξ ↓ c = X1 ↓ c . . . Xk ↓ c. Example 5. Let µ1 be as in Example 4. Then µ1 ↓ 1 µ1 ↓ 2 = = {p1, p3} ∅ {p1, p3} {b} {p1, p4} {a} {p2, p4} {p1, p3} {a} {p2, p3} {b} {p2, p4} {a} {p2, p4}.
Note that both µ1 ↓ 1 and µ1 ↓ 2 are mixed step sequences of the original acyclic net. Proposition 1. Let pacnet be as in Definition 1.
1. If µ ∈ mixsseq(pacnet) then µ is well-formed and µ ↓ c ∈ mixsseq(acnet), for every c ∈ col. 2. If µc ∈ mixsseq(acnet), for every c ∈ col, are sequences of the same length, then there is µ ∈ mixsseq(pacnet) such that µ ↓ c = µc, for every c ∈ col.
Proof. (1) Let µ = M0U1M1 . . . Mk− 1UkMk and c ∈ col. The result is proven by induction on k.
If k = 0 then µ = M0 = Mpinaictnet. Then µ is well-formed and µ ↓ c ∈ mixsseq(acnet) follow from Definition 1(5) and Eq. (1).
The inductive case follows from the well-formedness of acnet, Definition 1(3), and, for every (u,t, c) ∈ Tpacnet, prepacnet ((u,t, c)) ↓ c = preacnet (u) and postpacnet ((u,t, c)) ↓ c = postacnet (u). Also, it is important that the tokens an modes of firing in different colours do not interfere with each other.
(2) Follows by a straightforward induction on the common length of the mixed step sequences. Again, it is important that the tokens an modes of firing in different colours do not interfere with each other. Moreover, Definition 1(3) ensures that a u ∈ T ′ can be ‘executed’ with parameter c ∈ col when M is a colour-safe marking of pacnet such that preacnet (u) ⊆ M ↓ c.
The assumption that the mixed step sequences have the same length can be easily satisfied by adding extra empty steps to the ‘shorter’ ones.
Proposition 1(1) means that the behaviour of pacnet is well-formed and based on the behaviour of acnet. Conversely, Proposition 1(2) means that all the behaviours of acnet are represented by the behaviours of pacnet. 4.2. Parameterised communication structured acyclic net We now introduce a parameterised version of communication structured acyclic nets. Since the definitions closely follow those in the previous section, we keep explanations short. Definition 2. A parameterised communication structured acyclic net (or PCSA-net) is a tuple pcsan = (pacnet1, . . . , pacnetn, Q,W, Q′,W ′, ι′, col) (n ≥ 1) such that: • pacneti = (Pi, Ti, Fi, acneti, ιi, col), for 1 ≤ i ≤ n, are parameterised acyclic nets. • csan = (acnet1, . . . , acnetn, Q,W ) is a well-formed csa-net. • Q′ is a set of (master) buffer places, and W ′ ⊆ Q′ × T ∪ T × Q′, where T = T1 ∪ · · · ∪ Tn, is a set of arcs adjacent to these places. • ι′ : Q′ → 2Q \ {∅} is an annotation mapping such that Q = ⨄︁{ι(q) | q ∈ Q′}. For every q ∈ Q, qpcsan will denote the unique channel place in Q′ such that q ∈ ι′(qpcsan). We also assume that the sets of nodes of pacnet1, . . . , pacnetn, Q, Q′ are pairwise disjoint and
W ′ = {(x, y) ∈ Q′ × T ∪ T × Q′ | (ι(x) × ι(y)) ∩ W ̸= ∅}, where ι = ι1 ∪ · · · ∪
ιn ∪ ι′.
Example 6. Figure 5 shows an example of PCSA-net.
We also denote P = P1 ∪ · · · ∪ and u ∈ Tcsan, we denote:
Pn ∪ Q′ and F = F1 ∪ · · · ∪
Fn ∪ W ′, and, for all x ∈ P ∪ T , p ∈ P, prepcsan (x) postpcsan (x) = = {z | zF x} {z | xF z} prepcsan (u, p) postpcsan (u, p) = = ι (p) ∩ precsan (u) ι (p) ∩ postcsan (u) Proposition 2. For all t ∈ Tpcsan and u ∈ ι (t): ⨄︁{prepcsan (u, p) | p ∈ prepcsan (t)} ⨄︁{postpcsan (u, p) | p ∈ postpcsan (t)} c p4 precsan (u) postcsan (u) p1 = = a (a) (b) p2 p5 p7
q1 r5:{p5} r7:{p7} β p3 p6 p8 q2 r6:{p6}
The idea of Definition 2 is similar to that of parameterised acyclic net, and so the following notations are close to those introduced before :
Tpcsan = Tpacnet1 ∪ · · · ∪
Tpacnet1 and Ppcsan = Ppacnet1 ∪ · · · ∪
Ppacnet1 ∪ Q˜︁ Tpacneti : where Q˜︁ = {(q, qpcsan, c) | q ∈ Q ∧ c ∈ col}. Moreover, we denote, for all 1 ≤ i ≤ n and (u,t, c) ∈ prepcsan ((u,t, c)) = postpcsan ((u,t, c)) = prepacneti ((u,t, c)) ∪ {(q, qpcsan, c) ∈ Q˜︁ | qWu} postpacneti ((u,t, c)) ∪ {(q, qpcsan, c) ∈ Q˜︁ | uW q}
The markings of pcsan, denoted by markings(pcsan), are the subsets of Ppcsan. The default initial marking is
Mpincistan = Mpinaictnet1 ∪ · · · ∪
Mpinaictnetn and the steps are
steps(pcsan) = {U ∈ 2Tpcsan | ∀t ̸= u ∈ U : prepcsan (t) ∩ prepcsan (u) = ∅} .
A step U of pcsan is enabled at marking M if It can then be executed and yield prepcsan (U ) ⊆
M ∪ (postpcsan (U ) ∩ Q˜︁).
M′ = (M ∪ postpcsan (U ) \ prepcsan (U ).
This is denoted by M[U ⟩pcsan M′. Let (Mpincistan =)M0, M1 . . . , Mk (k ≥ 0) be markings and U1, . . . ,Uk be steps of pcsan such that we have Mi− 1[Ui⟩pcsan Mi, for every 1 ≤ i ≤ k. Then is a mixed step sequence of pcsan. This is denoted by µ ∈ mixsseq(pcsan). Moreover, µ is well-formed if the following hold: • postpcsan (t) ∩ postpcsan (u) = ∅, for every 1 ≤ i ≤ k and all t ̸= u ∈ Ui.
• postpcsan (Ui) ∩ postpcsan (Uj) = ∅, for all 1 ≤ i < j ≤ k.
We also use the same notion of projection as for parameterised acyclic nets, and then obtain a result showing a full consistency between the behaviour of a PCSA-net and its underlying CSA-net. Proposition 3. Let pcsan be as in Definition 2.
1. If µ ∈ mixsseq(pcsan) then µ is well-formed and µ ↓ c ∈ mixsseq(csan), for every c ∈ col. 2. If µc ∈ mixsseq(csan), for every c ∈ col, are sequences of the same length, then there is µ ∈ mixsseq(pcsan) such that µ ↓ c = µc, for every c ∈ col.
Proof. The proof is similar to that of Proposition 1. s1:{p1} α {d} t1
Example 7. Figure 5(a) represents the original model in where two acyclic nets (the upper one exhibits concurrency and the lower exhibits alternative) communicate through two buffer places. Figure 5(b) shows the corresponding representation of Figure 5(a) after parameterising. That is, ι(r1) = {p1} and ι(t1) = {a} in the upper acyclic net, while ι(r7) = {p7} and ι(t5) = {e, f } in the lower acyclic net. In other words, ι(t5) specifies different ‘modes’ of the execution of transitions e and f for each mode u ∈ ι(t5), the arcs incoming to transition {t5} ‘deliver’ the input places of u, and similarly for the output arc.
Example 8. Figure 6 depicts a parameterised version of CSA-net of Figure1 after folding both acyclic nets. More specifically, s2 parameterised places p2 and p5, while t2 parameterised transition a and b. In other words, ι(s2) specifies the places which can be ‘present’ in s2 in the executions of pacnet. This process allows for both places and transitions to accept more than one tokens (parameters) which can enhance both visualisation and analysis of the models under investigation.
This paper introduced two extensions for CSA-nets using the concepts of folding and parameterisation. The analysis and visualisation of CSA-nets is not an easy task, especially for large and complex systems. Thus, this paper proposed the parameterisation technique by collapsing original components of CSA-nets to parameteric ones. This technique aims to extend both conditions and events to accept more than one token to be distinguished using the passed parameter. This can contribute to improving visualisation and increase the ability to understand models under investigation.
Future work will consider other form of folding, e.g., merging together entire components of acyclic nets and subsequently the extension to behaviour structured acyclic nets. We will implement the aforementioned extensions in SONCRAFT. In addition, the extension work will consider the behaviour structured acyclic nets. Both directions of future work aim to be implemented in SONCRAFT. Moreover, we will apply these concepts and extension to cybercrime scenarios to analyse and visualise such systems by CSA-nets.
I would like to thank the reviewers for their insightful comments on the submitted paper.