=Paper=
{{Paper
|id=Vol-3430/paper9
|storemode=property
|title=Hierarchical Simulation of Timed Behaviours of Structured Occurrence Nets
|pdfUrl=https://ceur-ws.org/Vol-3430/paper9.pdf
|volume=Vol-3430
|authors=Salma Alharbi
|dblpUrl=https://dblp.org/rec/conf/apn/Alharbi23
}}
==Hierarchical Simulation of Timed Behaviours of Structured Occurrence Nets==
https://ceur-ws.org/Vol-3430/paper9.pdf
Hierarchical Simulation of Timed Behaviours of
Structured Occurrence Nets
Salma Alharbi1
1
School of Computing, Newcastle University
Science Square, Newcastle upon Tyne, NE4 5TG, United Kingdom
Abstract
The typical notation for recording the behaviour of an asynchronous system is some form
of a directed acyclic graph. The formalism of structured occurrence nets (so-nets) can play
an important role in the representation of complex evolving system behaviours. so-nets are
sets of related occurrence nets, employing different types of formally defined relations and
supporting various types of abstraction, which represent the detail of the concurrency and
causality relations between executed events. The aim of this paper is to present theoretical
underpinnings, new algorithms, and prototype software implementation for hierarchical and
abstraction-based analyses and simulations of timed behaviours of complex evolving systems
using so-nets.
1. Introduction
An occurrence net is an acyclic net that provides a complete and unambiguous record of
all the causal dependencies among the events involved, including both backward (more
than one arrow incoming to a place) and forward non-determinism (more than one arrow
outgoing from a place). It represents a singular ‘causal history’ and has a single final
marking. A structured occurrence net (so-net) is an extension of an occurrence net [1],
and it illustrates causality and concurrency information for a single system execution
involving a number of occurrence nets which interact by synchronous and asynchronous
communication. so-nets were created in order to characterise the behaviour of evolving
systems of systems. It should be stressed that so-nets are not meant to be models of
concurrent systems, but rather models of their observed behaviours. In particular, an
so-net can be created and analysed without knowing the structure and components of
the actual system which generated an observed behaviours.
The importance of structure in helping designers to cope with design complexity is
well-accepted, especially in the software engineering domain and in the hardware design
domain. The effective use of structuring notations greatly reduces the cognitive complexity
of designs, and the resources involved in their representation and manipulation. The
purpose of a system design is to define how a system will behave. Notations for recording
actual or potential system behaviour have not attracted levels of interest comparable
PNSE’23, International Workshop on Petri Nets and Software Engineering, June, 2023, Lisbon, Portugal
" s.alharbi2@newcastle.ac.uk (S. Alharbi)
© 2023 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)
143
Salma Alharbi CEUR Workshop Proceedings 143–165
to those for system design notations. This is probably because detailed records of the
behaviour of complex systems are mainly used out of sight within tools for system
visualisation, verification, synthesis and failure analysis, rather than in documents and
user interfaces [2].
Time simulation is a powerful tool used in many fields to model and analyse the
behaviour of complex systems over time, such as crimes and accidents. In criminal
investigations, time simulation may be an effective technique since it enables investigators
to piece together the sequence of events that led to a crime. Investigators may better
grasp the circumstances leading up to a crime by simulating time, which can be useful in
identifying suspects and acquiring evidence. Structured occurrence net (or so-nets) is an
extension of the notion of an occurrence net, which is a directed acyclic graph [1] that
captures causality and concurrency information about a single execution of a system.
so-nets can play an important role in the representation of complex evolving systems
(ce-systems) behaviours. Representing date-time information about such systems is
important. Timed so-nets are based on groups of associated timed occurrence nets and
are designed for reasoning about related events and causality with time information that
is uncertain or missing in evolving systems. When modelling a system based on time,
such as accidents or crimes, it is important to identify the order in which events have
happened and to identify the duration of the events. However, the temporal information
that is known about an occurrence is often inaccurate or lacking. For instance, although
it may not be able to pinpoint a certain date-time (such as [2022/11/04 05:05:05]) at
which a robbery happened, it could be possible to provide temporal boundaries such as
(earliest start and latest start).
The contribution of this paper is a novel tool-supported formalism (timed so-nets
and timed simulation) for modelling and reasoning about concurrent events with un-
certain or missing time information in developing systems. It is built on collections of
connected timed occurrence nets. Timed simulation tool for criminal investigations to
help investigators reconstruct the timeline of events related to a crime.
This paper is aimed to address the theoretical underpinnings, which will be described in
the subsequent sections. Section 2 gives a background about so-nets, search description
and research question. The notation of timed so-net (based on discrete time intervals),
and algorithms for estimating and increasing the precision of date-time intervals using
default duration intervals and redundant time information are given in Section 3. A
simulation of timed behaviour using duration intervals is given in Section 4. Support for
date-timed so-nets and simulation of the time is provided by the soncraft tool, which
is described in Section 5. Conditions for checking the consistency of date-time intervals
and algorithms are defined in the Appendix.
2. Background
Occurrence nets (or o-nets) represent single executions of computing systems, providing
details of the concurrency and causality relations between executed events.
An o-net is a triple onet = (𝐶, 𝐸, 𝐹 ), where 𝐶 and 𝐸 are finite disjoint sets of conditions
144
Salma Alharbi CEUR Workshop Proceedings 143–165
𝑂𝑁 ↑ 1
𝑉 𝑒𝑟1.0 𝑈 𝑝𝑑𝑎𝑡𝑒𝑠 𝑉 𝑒𝑟2.0
𝑐0 𝑒0 𝑐1 𝑒1 𝑐2
𝐴𝑠𝑦𝑛𝑐ℎ𝑟𝑜𝑛𝑜𝑢𝑠 𝑞0
𝑞1 𝑞2
𝑆𝑦𝑛𝑐ℎ𝑟𝑜𝑛𝑜𝑢𝑠 𝑂𝑁1 𝑂𝑁2
𝑐3 𝑒2 𝑐4 𝑒3 𝑐5 𝑐0 𝑒0 𝑐1 𝑐2 𝑒1 𝑐3
(𝑎) (𝑏)
Figure 1: cso-net (a); and bson-net portraying a system (off-line) update (b).
and events (referred to as the nodes), and 𝐹 ⊆ (𝐶 × 𝐸) ∪ (𝐸 × 𝐶) is the flow relation.
The inputs and outputs of a node 𝑥 are ∙ 𝑥 = {𝑦 | (𝑦, 𝑥) ∈ 𝐹 } and 𝑥∙ = {𝑦 | (𝑥, 𝑦) ∈ 𝐹 }. For
𝑋 ⊆ 𝐶 ∪ 𝐸, ∙ 𝑋 and 𝑋 ∙ are the sets of all inputs and outputs of the nodes in 𝑋. Also,
we assume:
• For all 𝑐 ∈ 𝐶: |∙ 𝑐| ≤ 1 and |𝑐∙ | ≤ 1.
• For all 𝑒 ∈ 𝐸: |∙ 𝑒| ≥ 1 and |𝑒∙ | ≥ 1.
• The causality relation ≺ over 𝐸 is acyclic, where 𝑒 ≺ 𝑓 if 𝑒∙ ∩ ∙ 𝑓 ̸= ∅.
In an o-net, a marking is any set of conditions. The initial and final markings are
𝑀0onet = {𝑐 ∈ 𝐶 | ∙ 𝑐 = ∅} and 𝑀fin
onet = {𝑐 ∈ 𝐶 | 𝑐∙ = ∅}, respectively. An o-net can be
executed by firing sets of events; this execution follows the standard Petri net step
semantics. (We also will omit details of execution of other so-nets described in this
section.)
The paper [3] used communication structured occurrence nets (or cso-nets) to represent
communication between different subsystems. A cso-net is a set of o-nets connected
by special nodes called channel places. Figure 1 shows a cso-net with two o-nets
communicating synchronously (events 𝑒1 and 𝑒3 are always executed simultaneously) and
asynchronously (events 𝑒0 and 𝑒2 can be executed simultaneously, or 𝑒2 is executed after
𝑒0 ).
A phase of o-net is a non-empty set of conditions, each phase is a fragment of an
o-net beginning with a cut and ending with a cut (a maximal set of causally unrelated
conditions) which follows it in the causal sense, including all the conditions occurring
between these cuts. In [3], a phase decomposition is a sequence of phases from the initial
state to the final state, and whenever one phase ends, its maximal cut is the starting
point of the successive one (minimal cut).
A cso-net is a tuple cson = (onet1 , . . . , onet𝑘 , 𝑄, 𝑊 ), where each onet𝑖 = (𝐶𝑖 , 𝐸𝑖 , 𝐹𝑖 ) is
an o-net (we denote C = 𝑘𝑖=1 𝐶𝑖 , E = 𝑘𝑖=1 𝐸𝑖 and F = 𝑘𝑖=1 𝐹𝑖 ), 𝑄 is a set of channel
⋃︀ ⋃︀ ⋃︀
places, and 𝑊 ⊆ (𝑄 × E) ∪ (E × 𝑄). It is assumed that:
• The onet𝑖 ’s and 𝑄 are mutually disjoint.
• The inputs and outputs of 𝑞 ∈ 𝑄, ∙ 𝑞 = {𝑒 ∈ E | (𝑒, 𝑞) ∈ 𝑊 } and 𝑞 ∙ = {𝑒 ∈ E | (𝑞, 𝑒) ∈
𝑊 }, belong to distinct component onet𝑖 ; and |∙ 𝑞| = 1 and |𝑞 ∙ | ≤ 1.
• The relation (⊏ ∪ ≺)* ∘ ≺ ∘ (≺ ∪ ⊏)* over E is irreflexive, where: 𝑒 ≺ 𝑓 if there is
𝑐 ∈ C with 𝑐 ∈ 𝑒∙ ∩ ∙ 𝑓 ; and 𝑒 ⊏ 𝑓 if there is 𝑞 ∈ 𝑄 with 𝑞 ∈ 𝑒∙ ∩ ∙ 𝑓 .
145
Salma Alharbi CEUR Workshop Proceedings 143–165
Intuitively, the original causality relation ≺ represents the ‘earlier than’ relationship of
the events, and ⊏ represents the ‘not later than’ relationship. The inputs and outputs of
a node are extended to include channel places.
A marking of cson is a set of conditions and channel places. The initial marking is
𝑀0cson = 𝑀0onet1 ∪ · · · ∪ 𝑀0onet𝑘 and the final marking is 𝑀fin cson = 𝑀 onet1 ∪ · · · ∪ 𝑀 onet𝑘 . In
fin fin
a cso-net, a step is a set of events which may come from one of more component o-nets.
In Figure 1(a), event 𝑒1 and 𝑒3 communicate synchronously due to a cycle involving
channel places 𝑞1 and 𝑞2 . In diagrams, such a situation may also be represented by
a single channel place with undirected edges between events, e.g., as for 𝑒0 and 𝑒1 in
Figure 12.
Behavioural structured occurrence nets (or bso-nets) model activities of evolving
systems [3]. An execution history is represented on two different levels: the lower level,
which is used to indicate behavioural details, and the upper level, which is used to
represent the stages (phases) of system evolution. Thus a bso-net provides details about
the evolution of a system. Figure 1 shows an example of bso-net representing a system
update. A version change brought on by an update event is represented at the top level.
The lower level reveals the behaviour of the system before and after the update [3].
Let cson be cso-net as above, and cson↑ = (onet↑1 , . . . , onet↑𝑚 , 𝑄↑ , 𝑊 ↑ ) be a disjoint
cso-net such that each onet↑𝑖 = (𝐶𝑖↑ , 𝐸𝑖↑ , 𝐹𝑖↑ ) is line-like (i.e., it can be represented as a
↑ ↑ ↑
chain 𝑐1 𝑒1 . . . 𝑒𝑙−1 𝑐𝑙 ). In addition, let C↑ = 𝑚 𝑖=1 𝐶𝑖 , E = 𝑖=1 𝐸𝑖 , and F = 𝑖=1 𝐹𝑖 . A
⋃︀ ↑ ⋃︀𝑚 ↑ ⋃︀𝑚
bso-net is a tuple bson = (cson, cson↑ , 𝛽) such that 𝛽 ⊆ C × C↑ , and the following hold:
1. For every onet𝑖 , there exists exactly one onet↑𝑗 satisfying 𝛽(𝐶𝑖 ) ∩ 𝐶𝑗↑ ̸= ∅.
2. For every onet↑𝑗 represented by a chain 𝜉onet↑ = 𝑐1 𝑒1 . . . 𝑒𝑙−1 𝑐𝑙 , the sequence
𝑗
𝜋1 𝜋2 . . . 𝜋𝑙 = 𝛽 −1 (𝑐1 ) . . . 𝛽 −1 (𝑐𝑙 ) is a concatenation of phase decompositions of differ-
ent o-nets in cson. For all 𝑐𝑗 and 𝑒𝑗 occurring in the chain 𝜉onet↑ , 𝜋(𝑐𝑗 ) = 𝜋𝑗 and
𝑗
causal(𝑒𝑗 ) = ∙ (𝑀 𝑎𝑥𝛽 −1 (∙ (𝑒𝑗 )) ) × {𝑒𝑗 } ∪ {𝑒𝑗 } × (∙ 𝑀 𝑖𝑛𝛽 −1 (𝑝𝑜𝑠𝑡(𝑒𝑗 )) ).
3. The relation (⊏ ∪ ≺ ∪ ◁)* ∘ (≺ ∪◁) ∘ (≺ ∪ ⊏ ∪◁)* over E ∪ E↑ is irreflexive, where:
𝑒 ≺ 𝑓 if there is 𝑐 ∈ C ∪ C↑ with 𝑐 ∈ 𝑒∙ ∩ ∙ 𝑓 ; 𝑒 ⊏ 𝑓 if there is 𝑞 ∈ 𝑄 ∪ 𝑄↑ with
𝑞 ∈ 𝑒∙ ∩ ∙ 𝑓 ; and 𝑒 ▷ 𝑓 if (𝑒, 𝑓 ) ∈ 𝑒′ ∈𝐸 ↑ causal(𝑒′ ).
⋃︀
↑
The initial marking 𝑀0bson of bso-net is 𝑀0cson together with 𝑀0onet𝑖 for each 𝑖 such that
↑
𝛽(𝑀0onet𝑖 ) ∩ 𝑀0cson ̸= ∅. The final marking 𝑀fin
bson is defined similarly.
𝐴 𝑇 𝑎𝑘𝑒 𝑡𝑟𝑎𝑖𝑛
𝐿𝑜𝑛𝑑𝑜𝑛 𝑇 𝑎𝑘𝑒 𝑡𝑟𝑎𝑖𝑛 𝐸𝑑𝑖𝑛𝑏𝑢𝑟𝑔ℎ 𝐴 𝐴 𝐴
𝐿𝑜𝑛𝑑𝑜𝑛 𝐸𝑑𝑖𝑛𝑏𝑢𝑟𝑔ℎ
𝐵 𝐴𝐵 𝐴𝐵
𝐿𝑜𝑛𝑑𝑜𝑛 𝑇 𝑎𝑘𝑒𝑓 𝑙𝑖𝑔ℎ𝑡 𝐸𝑑𝑖𝑛𝑏𝑢𝑟𝑔ℎ 𝑇 𝑎𝑘𝑒 𝑓 𝑙𝑖𝑔ℎ𝑡
𝐵 𝐵 𝐵
(𝑎) (𝑏)
Figure 2: (a) Multiple scenarios modelled by two o-nets, and (b) ao-net.
146
Salma Alharbi CEUR Workshop Proceedings 143–165
Figure 3: The relationship among unknown and known time values and duration [4].
A bso-net consists of two cso-nets connected by a behavioural relation 𝛽. In the
above, (1) implies that each phase points to exactly one condition of the upper level, and
(2) means that each upper level condition maps to a single phase of a lower level o-net .
The ordering of the upper level conditions must match that of the phase decompositions
of the lower level o-net.
In [3] an extension of so-nets, called alternative structured occurrence nets (or ao-nets),
was introduced to facilitate the modelling of alternative behaviours, as shown by the
example in Figure 2(a). Using the so-net concept, the activities of a person travelling to
a destination in different ways would need to be represented by two distinct o-nets, (A
and B), where each one represents a unique scenario. Since these two o-nets represent the
same system, modelling in this way results in several duplicate states. An improvement
for such a case is shown in Figure 2(b), where the two o-nets of Figure 2(a) are essentially
combined into a single structure [3].
Let 𝐴𝑆 = {𝐴1 , . . . , 𝐴𝜙 } be a set of alternative scenarios. A tagged occurrence net (or
ton-net) is a tuple tagon = (𝐶, 𝐸, 𝐹, 𝜗) where 𝐶 and 𝐸 are disjoint sets of respectively
conditions and events (collectively referred to as the nodes), 𝐹 ⊆ (𝐶 × 𝐸) ∪ (𝐸 × 𝐶) is the
flow relation, and 𝜗 : 𝐶 ∪ 𝐸 ∪ 𝐹 → 2𝐴𝑆 ∖ {∅} is a mapping, such that, for each 𝐴 ∈ 𝐴𝑆,
tagon(𝐴) = (𝐶(𝐴), 𝐸(𝐴), 𝐹 (𝐴)) is an o-net , where for 𝑋 ∈ {𝐶, 𝐸, 𝐹 }, 𝑋(𝐴) is the set of
all 𝑥 ∈ 𝑋 such that 𝐴 ∈ 𝜗(𝑥). The initial marking 𝑀0tagon , final marking 𝑀fin tagon
, input and
output of a node 𝑥, i.e., 𝑥 and 𝑥 , in ton-nets are defined in the same way as in o-nets.
∙ ∙
tagon(𝐴) tagon(𝐴)
It is further assumed that for all 𝐴 ∈ 𝐴𝑆, 𝑀0tagon = 𝑀0 tagon
and 𝑀fin = 𝑀fin .
We define two nodes, 𝑥 and 𝑦, as being alternatively related (or conflicting) if there are
distinct events, 𝑒 and 𝑓 , such that ∙ 𝑒 ∩ ∙ 𝑓 ̸= ∅ and (𝑒, 𝑥) ∈ 𝐹 * and (𝑓, 𝑦) ∈ 𝐹 * (denoted by
𝑥#𝑦). They are causally related if (𝑥, 𝑦) ∈ 𝐹 + or (𝑦, 𝑥) ∈ 𝐹 + . A block of the ton-net is a
non-empty set 𝐵 ∈ (𝐶 ∪ 𝐸) such that 𝐵 ∩ 𝐶 = ∙ (𝐵 ∩ 𝐸) ∩ (𝐵 ∩ 𝐸)∙ , (∙ 𝐵 ∖ 𝐵) × (𝐵 ∙ ∖ 𝐵) ⊆≺,
and for all 𝑒, 𝑓 ∈ (𝐵 ∩ 𝐸), ¬(𝑒#𝑓 ).
Essentially, a ton-net can be regarded as an overlay of multiple o-nets, each being
tagged by a symbol 𝐴 in 𝐴𝑆 representing a unique scenario. This is specified by the
mapping 𝜗. Thus each element in a ton-net is tagged by one or more tags to indicate to
which scenarios it belongs. The tagging is not completely arbitrary; all the elements with
the same tag form a valid o-net (i.e., tagon(𝐴)). This represents the behavioural report
of what has happened from the point of view of one of the possible scenarios 𝐴 ∈ 𝐴𝑆,
and thus a step sequence portrays a valid system execution with respect to a particular
scenario.
In [4] timed structured occurrence nets (or tso-nets) are based on groups of associated
147
Salma Alharbi CEUR Workshop Proceedings 143–165
D:10-20 D:10-20
T:0900-1000 T:1030-1100 T:0900-1000 T:1005-1100
(𝑎) (𝑏)
𝑐1 𝑒1 𝑐2 𝑐1 𝑒1 𝑐2
Figure 4: The time information of two o-nets
timed o-nets and are designed for reasoning about related events and causality with time
information that is uncertain or missing. When modelling a system based on time, such
as accidents or crimes, it is important to identify the order in which events have happened
and to identify the duration of the events. Each node (condition, event and channel
place) has a start time (𝑇𝑠 ), finish time (𝑇𝑓 ) and duration (𝐷). As shown in Figure 3, all
time values have bounded uncertainty represented via specified times intervals ([𝑇𝑠,𝑙 , 𝑇𝑠,𝑢 ])
and [𝑇𝑓,𝑙 , 𝑇𝑓,𝑢 ]). In addition, the duration has bounded uncertainty represented via a
specified duration interval ([𝐷𝑙 , 𝐷𝑢 ]).
As shown in Figure 4, the time interval information is specified in each arc and prefixed
by ‘𝑇 :’. The time information represents the finish time of the source of the node in
addition to the start time of the destination node. The duration interval is prefixed by
‘𝐷 :’ ([3]).
3. Time model
In a time-based system, it is critical to establish the order in which events have fired and
the duration intervals between them in order to determine, e.g., eliminate improbable
hypothesised scenarios.
The way in which time is represented in our model (using dates, etc.) is much more
practical for supporting, e.g., crime investigations than the previous number-based
attempts. The notations and definitions below are adapted from [4].
We assume that each node (condition, event) in so-net has a start date (𝑇𝑠 ) and
finish date (𝑇𝑓 ), and that each date and time event has a bounded uncertainty that
is represented by a specified earliest and latest date-time interval. ([𝑇𝑠,𝑒 , 𝑇𝑠,𝑙 ]) and
([𝑇𝑓,𝑒 , 𝑇𝑓,𝑙 ] respectively). Also, each node has a duration (𝐷) with a bounded uncertainty
represented by a specified early and late duration interval ([𝐷𝑒 , 𝐷𝑙 ]), and a calculated
earliest (shortest) and latest (longest) duration between the start date and end date of
each node ([𝐷𝑒 , 𝐷𝑙 ]).
Notation. Let 𝑛 be a node in a so-net. The early and late date-time start interval of 𝑛
is denoted by 𝐼𝑠𝑛 = [𝑇𝑠,𝑒 𝑛 , 𝑇 𝑛 ], where 𝑇 𝑛 ≤ 𝑇 𝑛 are the earliest and latest date-time start,
𝑠,𝑙 𝑠,𝑒 𝑠,𝑙
respectively. The early and late date-time finish interval of 𝑛 is denoted by 𝐼𝑓𝑛 = [𝑇𝑓,𝑒 𝑛 , 𝑇 𝑛 ],
𝑓,𝑙
where 𝑇𝑓,𝑒 ≤ 𝑇𝑓,𝑙 are the earliest and latest date-time start, respectively. The constraint
𝑛 𝑛
(𝑇𝑠𝑛 ) ≤ (𝑇𝑓𝑛 ) states that the start time of 𝑛 must be at or earlier than the finish time of 𝑛.
The start and finish time intervals of 𝑛 should satisfy the following conditions in order
to assure consistency with this constraint: 𝑇𝑠,𝑒 𝑛 ≤ 𝑇 𝑛 ∧ 𝑇 𝑛 ≤ 𝑇 𝑛 . The early and late
𝑓,𝑒 𝑠,𝑙 𝑓,𝑙
duration interval of 𝑛 are denoted by 𝐼𝑑 = [𝐷𝑒 , 𝐷𝑙𝑛 ] where 0 ≤ 𝐷𝑒𝑛 ≤ 𝐷𝑙𝑛 are the earliest
𝑛 𝑛
148
Salma Alharbi CEUR Workshop Proceedings 143–165
Figure 5: Line-like o-net with a date and time interval.
and latest duration intervals.
Time consistency in line-like o-nets. In line-like o-nets, each event has exactly one
input condition and one output condition, and each condition has at most one input and
output event. Then, for any two directly connected nodes (i.e., a condition that ends
in an event or an event that starts a condition), we assume that the finish time of the
source node is equal to the start time of the destination node. Consequently, we have
𝐼𝑓𝑛1 = 𝐼𝑠𝑛2 , for every (𝑛1 , 𝑛2 ) ∈ 𝐹 (1)
The information regarding node 𝑛 is node consistent if and only if
[𝑇𝑠,𝑒 + 𝐷𝑒 , 𝑇𝑠,𝑙 + 𝐷𝑙 ] ∩ [𝑇𝑓,𝑒 , 𝑇𝑓,𝑙 ] ≠ ∅
[𝑇𝑓,𝑒 − 𝐷𝑙 , 𝑇𝑓,𝑙 − 𝐷𝑒 ] ∩ [𝑇𝑠,𝑒 , 𝑇𝑠,𝑙 ] = ̸ ∅ (2)
[𝑚𝑎𝑥(0, 𝑇𝑓,𝑒 − 𝑇𝑠,𝑙 ), 𝑇𝑓,𝑙 − 𝑇𝑠,𝑒 ] ∩ [𝐷𝑒 , 𝐷𝑙 ] ̸= ∅
For example, the first part of Condition (2) verifies the bounds are consistent (i.e., overlap)
with the specified finish date and time interval of 𝑛. A line-like o-net is time consistent
if and only if every node 𝑛, in the o-net is node consistent and the flow relation of the
o-net satisfies Condition (1).
For example, consider the line-like o-nets shown in Figure 5. The date and time intervals
are shown above each node (with the prefixes Estart and Lstart representing the early and
late start date and time intervals, respectively), and the early, late finish date and time
intervals (with Efinish and Lfinish representing the early and late finish date and time
intervals). In addition, the duration interval of the event node is prefixed by Eduration
and Lduration in the format (𝑌 :Year, 𝑀 :Month, 𝐷:Day, 𝐻:Hour, Min:𝑀 𝑖𝑛𝑢𝑡𝑒, 𝑆:Second).
Using Condition (2) above, it can be observed that the time information in event 𝑒0 in
Figure 5(a) is inconsistent. Its estimated finish time-interval is [𝑇𝑠,𝑒 + 𝐷𝑒 , 𝑇𝑠,𝑙 + 𝐷𝑙 ] =
[Efinish : 2022/10/02 12 : 00 : 00, Lfinish : 2022/10/02 15 : 00 : 00], and its specified finish
time-interval is [Efinish : 2022/10/02 13 : 00 : 00, Lfinish : 2022/10/02 14 : 00 : 00]. In
contrast, event 𝑒0 in Figure 5(b) is node consistent.
Time consistency in cso-nets. In [3], a cso-net captures communication between
different subsystems. Communication between events is represented using special nodes
149
Salma Alharbi CEUR Workshop Proceedings 143–165
Figure 6: Two cso-nets with different runs of 𝑒0 and 𝑒1 .
called channel place that behave similarly to conditions. In asynchronous communication,
the sending event 𝑒 executes either before, or simultaneously with, the receiving event 𝑒′ ,
and the two events are linked by an asynchronous channel place that records information
about the communication using a condition. In synchronous communication, the two
communicating events execute simultaneously and are linked by two synchronous channel
places as explained in section 2.
Figure 6 shows how date and time information in a cso-net can reveal the behaviour
of events during asynchronous communication. In Figure 6(a) events 𝑒0 and 𝑒1 have the
same start and finish date and time intervals, which indicates that the two events are
executed simultaneously. In Figure 6(b) the date and time intervals are different which
indicates that 𝑒0 executes earlier than 𝑒1 .
Time consistency in bso-nets. The verification of date and time consistency in bso-
nets involves verifying time consistency between o-nets at various levels of abstraction
using the behavioural 𝛽 and causal relationships. The assumption made, for the sake of
simplicity, is that all abstraction levels have the same date, time origin and granularity.
Given a bso-net, let causal𝑈 be the binary relation consisting of the causally related
pairs of events: causal𝑈 = {causal(𝑒) | 𝑒 ∈ E}, where E is the set of events in the o-nets
⋃︀
of the bso-net. The time information of causal𝑈 is date and time consistent if and only
if the following condition is satisfied:
𝑔
∀(𝑔, ℎ) ∈ causal𝑈 : (𝑇𝑠,𝑒
𝑔 ℎ
≤ 𝑇𝑠,𝑒 ∧ 𝑇𝑠,𝑙 ℎ
≤ 𝑇𝑠,𝑙 ) (3)
For all conditions 𝑐𝑖 , 𝑐′𝑖 ∈ C (C is the set of conditions in the o-nets of the bso-net)
with (𝑐𝑖 , 𝑐′𝑖 ) ∈ 𝛽 and 𝑐𝑖 belonging to the initial condition of the lower level o-net of the
150
Salma Alharbi CEUR Workshop Proceedings 143–165
bso-net, the following must be true:
𝑐′
𝐼𝑠𝑐𝑖 = 𝐼𝑠 𝑖 (4)
In addition, for all conditions 𝑐𝑡 , 𝑐′𝑡 with (𝑐𝑡 , 𝑐′𝑡 ) ∈ 𝛽 and 𝑐𝑡 belonging to the final condition
of the lower level o-net of the bso-net, the following must hold:
𝑐′
𝐼𝑓𝑐𝑡 = 𝐼𝑓 𝑡 (5)
Condition (3) states that there are two events, 𝑔 and ℎ, the start date and time of event
𝑔 must be the same as, or precede, the start date and time of event ℎ. The initial and
end states of the bso-net are constrained by conditions (4) and (5): the start and (finish)
date and time of a lower level o-net must coincide with the start and (finish) date and
time of its corresponding upper level condition.
Figure 7 shows that the post-modified system’s (𝑐4 ) start time interval and the pre-
modified system’s (𝑐3 ) completion time interval are the same as their respective higher
level conditions.
Estimating date-time and duration intervals. Investigations of, e.g., crimes and acci-
dents, typically encounter situations where time information is missing or unavailable. In
such cases, it is often required to estimate the time information that would have filled
the gaps. Therefore, a missing interval of the node can be estimated if the other two
intervals are specified:
[𝑇𝑠,𝑒 , 𝑇𝑠,𝑙 ] = [𝑇𝑓,𝑒 − 𝐷𝑙 , 𝑇𝑓,𝑙 − 𝐷𝑒 ]
[𝑇𝑓,𝑒 , 𝑇𝑓,𝑙 ] = [𝑇𝑠,𝑒 + 𝐷𝑒 , 𝑇𝑠,𝑙 + 𝐷𝑙 ] (6)
[𝐷𝑒 , 𝐷𝑙 ] = [𝑚𝑎𝑥(0, 𝑇𝑓,𝑒 − 𝑇𝑠,𝑙 , 𝑇𝑓,𝑙 − 𝑇𝑠,𝑒 )].
In situations where both date and time intervals of a node are missing, it is necessary to
use a specified time interval from another node. The next section describes algorithms
that were adapted from [4] for estimating the missing time intervals of the nodes in
so-net using the following two approaches: the first approach is to estimate the intervals
of an individual node, and the second approach is to estimate the intervals of all the
nodes of the so-net.
Estimating finish date-time intervals. Algorithms 1 and 2 adapted from [4] describe
the structure of estimatEfinish, which computes the finish time interval of a node 𝑛 using
the causal functions and are outlined below.
Figure 7: bso-net portraying system (off-line) update.
151
Salma Alharbi CEUR Workshop Proceedings 143–165
Algorithm 1 Estimation finish time interval of a node using causal relation
1: procedure estimate early, late Finish(Node 𝑛)
2: 𝑅𝐵𝑜𝑢𝑛𝑑𝑎𝑟𝑦 := ∅ ◁ nearest right nodes of 𝑛 with specified early, late finish date
and time intervals
3: 𝑅𝑆𝑒𝑐𝑡𝑜𝑟 := 𝑛 ◁ nodes on paths from 𝑛 to 𝑅𝐵𝑜𝑢𝑛𝑑𝑎𝑟𝑦 nodes
4: 𝑓 𝑖𝑛𝑑𝑅𝑖𝑔ℎ𝑡𝐵𝑜𝑢𝑛𝑑𝑎𝑟𝑦(𝑛, 𝑅𝐵𝑜𝑢𝑛𝑑𝑎𝑟𝑦, 𝑅𝑆𝑒𝑐𝑡𝑜𝑟)
5: 𝑏𝑎𝑐𝑘𝑤𝑎𝑟𝑑𝐵𝐹 𝑆𝐷𝑎𝑡𝑒𝑠(𝑛, 𝑅𝐵𝑜𝑢𝑛𝑑𝑎𝑟𝑦, 𝑅𝑆𝑒𝑐𝑡𝑜𝑟)
6: procedure findRightBoundary(𝑁 𝑜𝑑𝑒 𝑛, 𝑆𝑒𝑡 𝐵𝑜𝑢𝑛𝑑𝑎𝑟𝑦, 𝑆𝑒𝑐𝑡𝑜𝑟)
7: 𝑊 𝑜𝑟𝑘𝑖𝑛𝑔 := 𝑛 ◁ nodes used for forward boundary searching
8: while 𝑊 𝑜𝑟𝑘𝑖𝑛𝑔 ̸= ∅ do
9: 𝑁 𝑒𝑥𝑡𝑊 𝑜𝑟𝑘𝑖𝑛𝑔 := ∅ ◁ nodes with unspecified early and late finish time
intervals
10: for all 𝑚 ∈ 𝑊 𝑜𝑟𝑘𝑖𝑛𝑔 do
11: if 𝑐𝑎𝑢𝑠𝑎𝑙𝑃 𝑜𝑠𝑡𝑠𝑒𝑡(𝑚) = ∅ then
12: add 𝑚 to 𝐵𝑜𝑢𝑛𝑑𝑎𝑟𝑦
13: else
14: for all 𝑛𝑑 ∈ 𝑐𝑎𝑢𝑠𝑎𝑙𝑃 𝑜𝑠𝑡𝑠𝑒𝑡(𝑚) do
15: add 𝑛𝑑 to 𝑆𝑒𝑐𝑡𝑜𝑟
16: if 𝑛𝑑.𝐸𝑓 𝑖𝑛𝑖𝑠ℎ.𝑠𝑝𝑒𝑐𝑖𝑓 𝑖𝑒𝑑 ∧ 𝑛𝑑.𝐿𝑓 𝑖𝑛𝑖𝑠ℎ.𝑠𝑝𝑒𝑐𝑖𝑓 𝑖𝑒𝑑 then
17: add 𝑛𝑑 to 𝑏𝑜𝑢𝑛𝑑𝑎𝑟𝑦
18: else
19: add 𝑛𝑑 to 𝑁 𝑒𝑥𝑡𝑊 𝑜𝑟𝑘𝑖𝑛𝑔
20: remove 𝑚 from 𝑤𝑜𝑟𝑘𝑖𝑛𝑔
21: 𝑊 𝑜𝑟𝑘𝑖𝑛𝑔 := 𝑁 𝑒𝑥𝑡𝑊 𝑜𝑟𝑘𝑖𝑛𝑔
• Given a node 𝑛 with an unspecified early and late finish date and time intervals
perform forward breadth first search (BFS) using the findRightBoundary procedure
to identify the nodes with a specified early and late finish date and time interval
that are nearest to 𝑛, see Figure 8.
• Using the identified nodes, perform the backwardBFSDates (BFS) procedure to
calculate the unspecified early and late date, time and duration intervals of the
nodes causally-related to 𝑛 (lines 6-7, 11-14). To increase the precision, recalculate
the intervals (lines 15-17), until node 𝑛 is reached.
Estimating finish time interval for ao-nets. In ao-nets, each condition has zero or more
input and output events. A condition can have multiple input and output events that are
different in different scenarios [5]. Algorithm 3 describes procedure estimateEarlyFinish,
which computes the finish date-time interval of a node 𝑛 using causal relations, as follows:
• Conduct a forward depth-first search (DFS) for a node 𝑛 with an undetermined
early finish date-time interval to find all paths that start at 𝑛 and end to the closest
node with a specified early finish date-time interval.
• For each path in ao-net, apply Equation (6) to compute a possible early finish
date-time interval of 𝑛, where 𝐼𝑓,𝑒 𝑛 is the specified early finish date-time interval
152
Salma Alharbi CEUR Workshop Proceedings 143–165
Algorithm 2 Estimation finish time interval of a node using causal relation
1: procedure backwardBFSDates 𝑁 𝑜𝑑𝑒 𝑛, 𝑆𝑒𝑡 𝐵𝑜𝑢𝑛𝑑𝑎𝑟𝑦, 𝑆𝑒𝑐𝑡𝑜𝑟(
)
2: 𝑊 𝑜𝑟𝑘𝑖𝑛𝑔 := 𝐵𝑜𝑢𝑛𝑑𝑎𝑟𝑦 ◁ nodes used for backward estimation of time intervals
3: while 𝑊 𝑜𝑟𝑘𝑖𝑛𝑔 ̸= 𝑛 do
4: 𝑁 𝑒𝑥𝑡𝑊 𝑜𝑟𝑘𝑖𝑛𝑔 := ∅ ◁ nodes with unspecified date, time and duration intervals
5: for all 𝑚 ∈ 𝑤𝑜𝑟𝑘𝑖𝑛𝑔 do
6: if ¬𝑚.𝐸𝑑𝑢𝑟𝑎𝑡𝑖𝑜𝑛.𝑠𝑝𝑒𝑐𝑖𝑓 𝑖𝑒𝑑 ∧ ¬𝑚.𝐿𝑑𝑢𝑟𝑎𝑡𝑖𝑜𝑛.𝑠𝑝𝑒𝑐𝑖𝑓 𝑖𝑒𝑑 then
7: 𝑚.𝐸𝑑𝑢𝑟𝑎𝑡𝑖𝑜𝑛, 𝑚.𝐿𝑑𝑢𝑟𝑎𝑡𝑖𝑜𝑛 := 𝑑𝑒𝑓 𝑎𝑢𝑙𝑡𝐷𝑢𝑟𝑎𝑡𝑖𝑜𝑛
8: for all 𝑛𝑑 ∈ 𝑐𝑎𝑢𝑠𝑎𝑙𝑃 𝑟𝑒𝑠𝑒𝑡(𝑚) ∩ 𝑆𝑒𝑐𝑡𝑜𝑟 do
9: add 𝑛𝑑 to 𝑁 𝑒𝑥𝑡𝑊 𝑜𝑟𝑘𝑖𝑛𝑔
10: 𝑛𝑑.𝑣𝑖𝑠𝑖𝑡𝑠 := 𝑛𝑑.𝑣𝑖𝑠𝑖𝑡𝑠 + 1
11: if ¬𝑛𝑑.𝐸𝑓 𝑖𝑛𝑖𝑠ℎ.𝑠𝑝𝑒𝑐𝑖𝑓 𝑖𝑒𝑑 ∧ 𝑚.𝐸𝑓 𝑖𝑛𝑖𝑠ℎ.𝑠𝑝𝑒𝑐𝑖𝑓 𝑖𝑒𝑑 then
12: 𝑛𝑑.𝐸𝑓 𝑖𝑛𝑖𝑠ℎ := 𝑚.𝐸𝑓 𝑖𝑛𝑖𝑠ℎ − 𝑚.𝐿𝑑𝑢𝑟𝑎𝑡𝑖𝑜𝑛
13: if ¬𝑛𝑑.𝐿𝑓 𝑖𝑛𝑖𝑠ℎ.𝑠𝑝𝑒𝑐𝑖𝑓 𝑖𝑒𝑑 ∧ 𝑚.𝐿𝑓 𝑖𝑛𝑖𝑠ℎ.𝑠𝑝𝑒𝑐𝑖𝑓 𝑖𝑒𝑑 then
14: 𝑛𝑑.𝐿𝑓 𝑖𝑛𝑖𝑠ℎ := 𝑚.𝐿𝑓 𝑖𝑛𝑖𝑠ℎ − 𝑚.𝐸𝑑𝑢𝑟𝑎𝑡𝑖𝑜𝑛
15: else if 𝑚.𝐸𝑓 𝑖𝑛𝑖𝑠ℎ.𝑠𝑝𝑒𝑐𝑖𝑓 𝑖𝑒𝑑 ∧ 𝑚.𝐿𝑓 𝑖𝑛𝑖𝑠ℎ.𝑠𝑝𝑒𝑐𝑖𝑓 𝑖𝑒𝑑 then
16: 𝑛𝑑.𝐸𝑓 𝑖𝑛𝑖𝑠ℎ := 𝑛𝑑.𝐸𝑓 𝑖𝑛𝑖𝑠ℎ ∩ (𝑚.𝐸𝑓 𝑖𝑛𝑖𝑠ℎ − 𝑚.𝐿𝑑𝑢𝑟𝑎𝑡𝑖𝑜𝑛)
17: 𝑛𝑑.𝐿𝑓 𝑖𝑛𝑖𝑠ℎ := 𝑛𝑑.𝐿𝑓 𝑖𝑛𝑖𝑠ℎ ∩ (𝑚.𝐿𝑓 𝑖𝑛𝑖𝑠ℎ − 𝑚.𝐸𝑑𝑢𝑟𝑎𝑡𝑖𝑜𝑛)
18: for all 𝑛𝑑 ∈ 𝑁 𝑒𝑥𝑡𝑊 𝑜𝑟𝑘𝑖𝑛𝑔 do
19: if 𝑛𝑑.𝑣𝑖𝑠𝑖𝑡𝑠 = 𝑐𝑎𝑢𝑠𝑎𝑙𝑃 𝑜𝑠𝑡𝑠𝑒𝑡(𝑛𝑑) then
20: for all 𝑛𝑑𝑜𝑢𝑡 ∈ 𝑐𝑎𝑢𝑠𝑎𝑙𝑃 𝑜𝑠𝑡𝑠𝑒𝑡(𝑛𝑑) do
21: if ¬𝑛𝑑𝑜𝑢𝑡.𝐸𝑠𝑡𝑎𝑟𝑡.𝑠𝑝𝑒𝑐𝑖𝑓 𝑖𝑒𝑑 ∧ 𝑛𝑑𝑜𝑢𝑡.𝐸𝑓 𝑖𝑛𝑖𝑠ℎ.𝑠𝑝𝑒𝑐𝑖𝑓 𝑖𝑒𝑑 then
22: 𝑛𝑑𝑜𝑢𝑡.𝐸𝑠𝑡𝑎𝑟𝑡 := 𝑛𝑑.𝐸𝑓 𝑖𝑛𝑖𝑠ℎ
23: 𝑛𝑑𝑜𝑢𝑡.𝐸𝑑𝑢𝑟𝑎𝑡𝑖𝑜𝑛 := 𝑛𝑑𝑜𝑢𝑡.𝐸𝑑𝑢𝑟𝑎𝑡𝑖𝑜𝑛 ∩ 𝑛𝑑𝑜𝑢𝑡.𝐸𝑓 𝑖𝑛𝑖𝑠ℎ −
𝑛𝑑𝑜𝑢𝑡.𝐿𝑠𝑡𝑎𝑟𝑡
24: if ¬𝑛𝑑𝑜𝑢𝑡.𝐿𝑠𝑡𝑎𝑟𝑡.𝑠𝑝𝑒𝑐𝑖𝑓 𝑖𝑒𝑑 ∧ 𝑛𝑑𝑜𝑢𝑡.𝐿𝑓 𝑖𝑛𝑖𝑠ℎ.𝑠𝑝𝑒𝑐𝑖𝑓 𝑖𝑒𝑑 then
25: 𝑛𝑑𝑜𝑢𝑡.𝐿𝑠𝑡𝑎𝑟𝑡 := 𝑛𝑑.𝐿𝑓 𝑖𝑛𝑖𝑠ℎ
26: 𝑛𝑑𝑜𝑢𝑡.𝐿𝑑𝑢𝑟𝑎𝑡𝑖𝑜𝑛 := 𝑛𝑑𝑜𝑢𝑡.𝐿𝑑𝑢𝑟𝑎𝑡𝑖𝑜𝑛 ∩ 𝑛𝑑𝑜𝑢𝑡.𝐿𝑓 𝑖𝑛𝑖𝑠ℎ −
𝑛𝑑𝑜𝑢𝑡.𝐸𝑠𝑡𝑎𝑟𝑡
27: else
28: remove 𝑛𝑑 from 𝑁 𝑒𝑥𝑡𝑊 𝑜𝑟𝑘𝑖𝑛𝑔
29: 𝑊 𝑜𝑟𝑘𝑖𝑛𝑔 := 𝑁 𝑒𝑥𝑡𝑊 𝑜𝑟𝑘𝑖𝑛𝑔
of the last node in each path and 𝐼𝐷𝑙𝑛 is the late duration of the last node in each
path (default late duration interval is used for nodes with unspecified late duration
interval).
Figure 9 shows that a forward DFS is used to find all paths from 𝑒0 to the nearest
node with a specified early finish date-time interval. More specifically, the first path
is (𝑐0 , 𝑒0 , 𝑐1 , 𝑒1 , 𝑐2 , 𝑒3 ) and the second path (𝑐0 , 𝑒0 , 𝑐1 , 𝑒2 , 𝑐4 , 𝑒4 ), the ao-net contains two
specified early finish date-time interval:
𝑒3
• The early finish date-time interval of the node 𝑒3 in the first scenario is: 𝐼𝑓,𝑒 =
153
Salma Alharbi CEUR Workshop Proceedings 143–165
Algorithm 3 Estimation finish date interval of a node with alternative using causal
relation
1: procedure estimate early, late Finish(Node 𝑛)
2: Input:𝐴𝑙𝑡𝑒𝑟𝑛𝑎𝑡𝑖𝑣𝑒𝑂𝑁 (𝐴𝑂𝑁 )
3: Output:𝐴𝑙𝑡𝑒𝑟𝑛𝑎𝑡𝑖𝑣𝑒𝑂𝑁 (𝐴𝑂𝑁 ) with estimated finish date-time interval of
all nodes in each scenario
4: 𝑃 𝑜𝑠𝑠𝑖𝑏𝑙𝑒𝑇 𝑖𝑚𝑒𝑠 := ∅ ◁ possible finish date-time intervals from forward search
5: 𝑣𝑖𝑠𝑖𝑡𝑒𝑑 :=<>
6: add 𝑛 to 𝑣𝑖𝑠𝑖𝑡𝑒𝑑
7: 𝑓 𝑜𝑟𝑤𝑎𝑟𝑑𝐷𝐹 𝑆𝐷𝑎𝑡𝑒(𝑣𝑖𝑠𝑖𝑡𝑒𝑑)
8: procedure forwardDFSDate((𝐿𝑖𝑠𝑡 𝑣𝑖𝑠𝑖𝑡𝑒𝑑))
9: for all 𝑛 ∈ 𝑐𝑎𝑢𝑠𝑎𝑙𝑃 𝑜𝑠𝑡𝑠𝑒𝑡(𝑣𝑖𝑠𝑖𝑡𝑒𝑑.𝑙𝑎𝑠𝑡) do
10: 𝐼 := 𝑛𝑢𝑙𝑙 ◁ possible finish date intervals
11: 𝑛 𝑛
if 𝐼𝑓,𝑒 .𝑠𝑝𝑒𝑐𝑖𝑓 𝑖𝑒𝑑 ∧ 𝐼𝑓,𝑙 .𝑠𝑝𝑒𝑐𝑖𝑓 𝑖𝑒𝑑 then
12: 𝐼 :=𝐼𝑓,𝑒
𝑛 − 𝐼𝑛 , 𝐼𝑛 − 𝐼𝑛
𝐷𝑙 𝑓,𝑙 𝐷𝑒 ◁ Eqn 6
13: add 𝐼 to 𝑃 𝑜𝑠𝑠𝑖𝑏𝑙𝑒𝑇 𝑖𝑚𝑒𝑠
14: else if 𝑛 ∈/ 𝑣𝑖𝑠𝑖𝑡𝑒𝑑 then
15: add 𝑛 to 𝑣𝑖𝑠𝑖𝑡𝑒𝑑
16: forwardDFSDates(𝑣𝑖𝑠𝑖𝑡𝑒𝑑)
17: remove 𝑣𝑖𝑠𝑖𝑡𝑒𝑑.𝑙𝑎𝑠𝑡
[2022/11/04 05:05:05] and the late duration interval of the node 𝑒3 in the first
𝑒3
scenario is 𝐼𝐷 𝑙
= [Lduration: 𝑌 1𝑀 1𝐷1𝐻1𝑀 𝑖𝑛1𝑆1], which is subtracted from the
specified early finish date-time interval of 𝑒3 using Equation 6.
Figure 8: Estimation for early start
154
Salma Alharbi CEUR Workshop Proceedings 143–165
Figure 9: Estimating ao-net early start
• Another possible early finish date-time interval is calculated using the second
scenario. The early finish date-time interval of the node 𝑒4 in the second scenario
𝑒4
is: 𝐼𝑓,𝑒 = [2022/11/23 06:06:06] and the late duration interval of the node 𝑒4 in
𝑒4
the second scenario is 𝐼𝐷 𝑙
= [Lduration: 𝑌 1𝑀 1𝐷1𝐻1𝑀 𝑖𝑛1𝑆1]. Figure 9 shows
the table for possible times estimations of the early finish date-time interval for 𝑒0
using the first and second scenarios. Figure 10 shows the table for possible times
estimations result for each scenario separately.
4. Hierarchical Simulation of Timed Behaviours
Simulation is a crucial problem-solving technique for tackling a variety of real-world
problems, and can be used to analyse and explain the behaviour of a system. In a
real-time simulation, the simulation is run in discrete time with constant steps, also
known as fixed step simulation, as time moves forward in equal duration of time [2].
Time simulation in so-nets. Every activity in a system has a time duration interval
which is different from zero, and we make the added assumption that all activities complete
in a finite amount of time. We will assume that every transition takes a bounded, non-zero
amount of time to fire. In the semantics of non-timed o-nets, transitions can fire at any
time after they are enabled, removing input token and creating output token. When
firing durations are included, the o-net semantic is changed. Each transition has a time
associated with it. When a transition becomes enabled, it removes the input token
immediately but does not create the output token until the firing duration has finished.
155
Salma Alharbi CEUR Workshop Proceedings 143–165
Figure 10: Estimating ao-net early start for each scenario.
(𝐴) (𝐵) (𝐶)
𝑐0 𝑐0 𝑐0
𝐸𝐷 : 𝑌 10𝑀 1𝐷1𝐻1𝑀 𝑖𝑛1𝑆1 𝐸𝐷 : 𝑌 10𝑀 1𝐷1𝐻1𝑀 𝑖𝑛1𝑆1
𝑐1 𝑒0 𝑐2 𝑐1 𝑒0 𝑐2 𝑐1 𝑒0 𝑐2
Figure 11: Time Transition firing.
Time transition firing. In tso-nets, an enabled transition is fired in three ‘conceptual’
steps: the first (immediate) step removes tokens from the input places, the second (tem-
poral) step holds the tokens for the duration of the firing time, and the third (immediate)
step moves tokens to all of the transition’s output places. For example, as shown in
Figure 11 early duration interval is displayed in 𝑒0 as 𝐸𝐷:𝑌 10, 𝑀 1, 𝐷1, 𝐻1, 𝑀 𝑖𝑛1, 𝑆1
which represent Year, Month, Day, Hour, Minute, Second respectively.
Time in synchronous so-nets. As shown in Figure 12, the cso-net with two o-nets
and synchronous communication. It shows that 𝑒0 and 𝑒1 are enabled and have the
same duration intervals, which indicates that the two events are executed simultaneously.
Therefore, after firing 𝑒0 or 𝑒1 the transitions will hold the tokens for duration of the
firing time, and then moves tokens to all of the transition’s output places.
Interval-timed acyclic net. The simulation of timed behaviours of CESs in meaningful
ways so that, for example, an incident (crime) investigator can use them effectively. The
main feature of interval-timed acyclic nets (described below) which are used for simulation
after working out the timings of transitions, is that transitions which are enabled need to
start immediately their enabling, and the firing lasts some time within an interval. Thus,
the startfiring and the endfiring of a transition are considered as two distinct events [6].
156
Salma Alharbi CEUR Workshop Proceedings 143–165
The firing of an enabled transition in timed simulation is composed of two ‘conceptual’
steps; the first calculates duration of the firing time, and the second one starts to
countdown the time units of the duration for the enabled transition [6]. Below N is the
set of non-negative integers, and N+ = N ∖ {0}.
Definition 1 (interval-timed acyclic net). An interval-timed acyclic net (or ita-net) is
a quadruple itanet = (𝑃, 𝑇, 𝐹, 𝐼) such that (𝑃, 𝑇, 𝐹 ) is a well-formed acyclic net, and
𝐼 : 𝑇 → {[𝑛, 𝑚] | 𝑛, 𝑚 ∈ N+ ∧ 𝑛 ≤ 𝑚} is its interval function.
For every 𝑡 ∈ 𝑇 , we denote 𝐼(𝑡) = [sfd(𝑡), lfd(𝑡)], calling sfd(𝑡) and lfd(𝑡) the shortest
firing duration and the longest firing duration of 𝑡, respectively.
Definition 2 (state of ita-net). A state of an ita-net itanet = (𝑃, 𝑇, 𝐹, 𝐼) is a pair
𝑆 = (𝑀, ℎ) such that 𝑀 ⊆ 𝑃 and ℎ ⊆ 𝑇 × N is the clock relation. The initial state of
itanet is 𝑀itanet
init = (𝑀 init
(𝑃,𝑇,𝐹 ) , ∅). All states of itanet are denoted by states(itanet).
The pair (𝑡, 0) ∈ ℎ means that 𝑡 has just finished its activity, and (𝑡, 𝑘) ∈ ℎ with 𝑘 > 0
means that 𝑡 has still 𝑘 time units to finish. Moreover, if there is no 𝑘 such that (𝑡, 𝑘) ∈ ℎ,
then 𝑡 is inactive.
Definition 3 (state change rules). Let 𝑆 = (𝑀, ℎ) be a state of an ita-net itanet =
(𝑃, 𝑇, 𝐹, 𝐼). The following are possible state-changing events:
𝑈
• Startfire events: 𝑆 −
→ (𝑀 ∖ ∙ 𝑈, ℎ ∪ {(𝑡, 𝑘𝑡 ) | 𝑡 ∈ 𝑈 }), where 𝑈 is a maximal step
+
enabled at 𝑀 , and sfd(𝑡) ≤ 𝑘𝑡 (𝑡) ≤ lfd(𝑡), for every 𝑡 ∈ 𝑈 .
𝑉
• Endfire events: 𝑆 −
→ (𝑀 ∪ 𝑉 ∙ , ℎ ∖ {(𝑡, 0) | 𝑡 ∈ 𝑉 }), where 𝑉 = {𝑡 | (𝑡, 0) ∈ ℎ}.
−
✓
• Tick events: 𝑆 −
→ (𝑀, {(𝑡, 𝑘 − 1) | (𝑡, 𝑘) ∈ ℎ}).
𝑈 :𝑉 𝑉 𝑈 ✓
• Global events: 𝑆 −−→ 𝑆 ′ , provided that: 𝑆 −
→ 𝑆 ′′ − → 𝑆 ′ , for some states 𝑆 ′′
→ 𝑆 ′′′ −
± − +
and 𝑆 ′′′ .
𝑐0 (𝐴) 𝑐0 (𝐵) 𝑐0 (𝐶)
𝐸𝐷 : 𝑌 10𝑀 1𝐷1𝐻1𝑀 𝑖𝑛1𝑆1 𝐸𝐷 : 𝑌 10𝑀 1𝐷1𝐻1𝑀 𝑖𝑛1𝑆1 𝐸𝐷 : 𝑌 10𝑀 1𝐷1𝐻1𝑀 𝑖𝑛1𝑆1
𝑒0 𝑐2 𝑒0 𝑐2 𝑒0 𝑐2
𝑐1 𝑐1 𝑐1
𝑐3 𝑐3 𝑐3
𝑞1 𝑞1 𝑞1
𝐸𝐷 : 𝑌 10𝑀 1𝐷1𝐻1𝑀 𝑖𝑛1𝑆1 𝐸𝐷 : 𝑌 10𝑀 1𝐷1𝐻1𝑀 𝑖𝑛1𝑆1 𝐸𝐷 : 𝑌 10𝑀 1𝐷1𝐻1𝑀 𝑖𝑛1𝑆1
𝑒1 𝑐5 𝑒1 𝑐5 𝑒1 𝑐5
𝑐4 𝑐4 𝑐4
Figure 12: Time in synchronous communication.
157
Salma Alharbi CEUR Workshop Proceedings 143–165
𝑈 :𝑉
Clearly, a global event 𝑆 −−→ 𝑆 ′ may be such that 𝑈 = 𝑉 = ∅, in which case only the
±
tick event has an effect. If, in addition, 𝑆 = (𝑀, ∅), then also the tick event has no effect
and 𝑆 = 𝑆 ′ and 𝑀 is a terminal marking of acnet.
Definition 4 (time semantics). The time step sequence semantics of itanet is defined
through sequences of global events:
𝑈 :𝑉 𝑈 :𝑉 𝑈𝑛−1 :𝑉𝑛−1
(𝑀itanet
init
=)𝑆0 −−
1 1 2 2
−→ 𝑆1 −−−→ . . . −−−−−−−→ 𝑆𝑛 .
± ± ±
Algorithm 4 allows to simulate the timed behaviours for o-net the (line 6 and 7) check
if the intervals late start and early finish are specified for the transition node and then
calculate the early duration interval for the event. Line 10 displays the duration above the
event with colours for each time unit (Year:red, Month:magenta, Day:blue, Hour:green,
Minute:purple, Second:cyan). Lines 11 and 12 start firing using the duration interval.
1. Check if latest start time and earliest finish time of 𝑡 are specified.
2. Calculate the shortest firing duration then display the time units of 𝑡 Eduration:
Y, M, D, H, Min, S denoted by Year, Month, Day, Hour, Minute and Second
respectively.
3. Remove the token from the pre-place to enabled transition 𝑡 to holds the token for
the duration of the firing time, then the timer will start by decrementing the time
unit.
4. If the time units are finished then the token moves automatically to the transition
post-place
Maximal events (firing steps). The time simulation for a maximal enabled events of
multiple o-nets, the maximal sets of firable transitions are selected so that the enabled
transitions in those sets must all fire simultaneously, and the firing of each transition
takes a specific amount of time. Algorithm 5 implements maximal events (firing steps),
line (6-8) check if the late start and early finish intervals are specified in the enabled
transitions then calculate the early duration interval and associate it with each transition.
Line (12-14) start firing simultaneously all the enabled transitions using the early duration
interval.
In Figure 13, we have scenarios A, B and C with a set of enabled transitions that
have different duration interval for each transition. The early duration interval ED is
associated with each transition 𝑡, the firing of the transition 𝑡 takes exactly ED time
units 𝐸𝐷 : 𝑌, 𝑀, 𝐷, 𝐻, 𝑀 𝑖𝑛, 𝑆. When a transition starts to fire then its time units start
to countdown 𝐼(𝑡). If there is a conflict between several enabled maximal sets, the choice
is arbitrarily solved.
Simulation of the o-nets and ao-nets is illustrated in Figure 13. We have two sequences
of maximal steps: 𝜎1 can fire {𝑎𝑠𝑡 , 𝑐𝑠𝑡 , 𝑔𝑠𝑡 }, then {𝑔𝑓 𝑖𝑛 , ✓} after that 𝑔 finish firing and ℎ
can start firing, {ℎ𝑠𝑡 }; and 𝜎2 can fire {𝑎𝑠𝑡 , 𝑐𝑠𝑡 , 𝑒𝑠𝑡 } another possible maximal steps can
fire in Figure 13, {𝑎𝑓 𝑖𝑛 , ✓}, after that a finish firing and b can start firing {𝑏𝑠𝑡 }, where 𝑠𝑡
indicates the start of firing and 𝑓 𝑖𝑛 is the finish of firing.
158
Salma Alharbi CEUR Workshop Proceedings 143–165
Algorithm 4 Timed Simulation algorithm of ON
1: Inputs:
𝑂𝑁 − Occurrence Net with time intervals
𝑀 − current marking
2: Output:𝑂𝑁 with a step enabled and time units
3: 𝑈 := 𝑎 𝑠𝑡𝑒𝑝 of ON
4: for all 𝑡 ∈ T do
5: if ∙ 𝑡 ⊆ 𝑀 then ◁ 𝑡 is ON-enabled
6: 𝑡 .𝑠𝑝𝑒𝑐𝑖𝑓 𝑖𝑒𝑑 ∧ 𝐼 𝑡 .𝑠𝑝𝑒𝑐𝑖𝑓 𝑖𝑒𝑑 then
if 𝐼𝑙,𝑠 𝑒,𝑓
7: 𝑡 := 𝐼 𝑡 − 𝐼 𝑡
𝐼𝑒,𝑑 𝑒,𝑓 𝑙,𝑠
8: display duration in 𝑡
9: add 𝑡 to 𝑈
10: for all t ∈ 𝑈 do
11: if 𝑡 ∈ 𝑈 has time units then
12: 𝑡 − 𝑓 𝑖𝑟𝑖𝑛𝑔 according to its time units
13: if 𝑡 its time units = 0 then
14: 𝑡−executed
15: 𝑡−calculate new state
5. Implementation
workcraft [7] is a tool that provides a flexible common underpinning for graph-based
models. Its plug-in, soncraft, provides some initial facilities for entering, editing,
Algorithm 5 Timed Simulation algorithm for maximal sets of enabled transitions
1: Inputs:
𝑂𝑁 − set of scenarios (ONs) with time intervals
𝑀 − current marking
2: Output:𝑂𝑁 set of maximal steps (ONs) and time units
3: array set of 𝑚𝑎𝑥𝑒𝑛𝑎𝑏𝑙𝑒𝑑𝑈 := []
4: for all 𝑡 ∈ T do
5: for all ∙ 𝑡 ⊆ 𝑀 do ◁ 𝑡 is ON-enabled
6: 𝑡 𝑡
if 𝐼𝑙,𝑠 .𝑠𝑝𝑒𝑐𝑖𝑓 𝑖𝑒𝑑 ∧ 𝐼𝑒,𝑓 .𝑠𝑝𝑒𝑐𝑖𝑓 𝑖𝑒𝑑 then
7: 𝑡 := 𝐼 𝑡 − 𝐼 𝑡
𝐼𝑒,𝑑 𝑒,𝑓 𝑙,𝑠
8: display duration in 𝑡
9: add 𝑡 to set of 𝑚𝑎𝑥𝑒𝑛𝑎𝑏𝑙𝑒𝑑𝑈
10: for all t ∈ set of 𝑚𝑎𝑥𝑒𝑛𝑎𝑏𝑙𝑒𝑑𝑈 do
11: if 𝑡 ∈ set of 𝑚𝑎𝑥𝑒𝑛𝑎𝑏𝑙𝑒𝑑𝑈 has time units then
12: 𝑡 − 𝑠𝑡𝑎𝑟𝑡𝑓 𝑖𝑟𝑖𝑛𝑔 according to its time units
13: if 𝑡 its time units = 0 then
14: 𝑡−executed
15: 𝑡−calculate new state
159
Salma Alharbi CEUR Workshop Proceedings 143–165
Figure 13: Firing maximal enabled events.
validating and simulating three types of so-net structures, namely, cso-nets, bso-nets
and tso-nets abstractions. We have implemented date-time intervals for events and
conditions and their analysis in soncraft. In this section, we present the implementation
of the date-based tools and the time simulation tool.
Time setting tool. The time setting tool shown in Figures 14 and 15 is an
interface for specifying date-time and duration intervals of event and condition
nodes in a so-net model. The early and late duration is specifying as follows
(𝑌 :Year, 𝑀 :Month, D:Day, H:Hour, Min:Minute, S:Second). Users can manually set the
date information for a selected event in the date panel. For each manually input date,
the tool verifies whether or not the date or time is well-defined for each event in the
so-net model. Moreover, for each node, the date is checked.
Date consistency checking tool. The date consistency checking is a tool that provides
consistency checking for the time information specified for events in the so-net model.
Figure 16 shows the tool performing a consistency check for o-net models. The result
displays the time information checking task when a node has complete, partial or
empty time information, as in Figure 17. Moreover, nodes with a date information and
inconsistency error from any o-net are shown. Figure 17 shows one event with a date
inconsistency error. For example, the error message involves event 𝑒0 and shows that its
start date (Estart: 2022/10/04 06:20:02, Lstart: 2022/10/04 06:20:02) is greater than its
end date (Efinish: 2022/10/03 00:00:00, Lfinish: 2022/10/03 00:00:00); in addition, the
consistency verification also checks the consistency for cso-net and bso-net models.
160
Salma Alharbi CEUR Workshop Proceedings 143–165
Timed simulation tool. Each event in the so-net has an early and late duration interval,
which were used to simulate the time of the event. In the time simulation tool we have
implemented two buttons to simulate the duration of the event: early time simulation
button, and late time simulation button, see Figure 18.
The simulation function in the so-net plugin can be activated by clicking on the early
time simulation button in the editor tools panel. The initial marking is automatically
set, and all enabled events are highlighted Figure 19. The timed simulation is then
conducted manually by clicking the enabled event after which the calculation for the early
event duration starts, displaying the result above each event. As shown in Figure 20, a
countdown then begins; the durations have different colours for each time unit (Year:red,
Month:magenta, Day:blue, Hour:green, Minute:purple, Second:cyan)
6. Concluding Remarks
The concept of a timed so-nets has been introduced in this paper in order to represent
and analyse causally connected events and concurrent occurrences in developing systems
with ambiguous or lacking temporal information. In addition, we presented a timed
simulation tool for, e.g., criminal investigations to help investigators reconstruct the
timeline of events and analyse the behaviour of the systems.
The future work will add multi-level modelling and embedding time granularity. A key
problem of handling complexity when large datasets are involved will be addressed by
developing hierarchical approach to simulation based on behavioural abstractions.
References
[1] E. Best, R. Devillers, Sequential and concurrent behaviour in Petri net theory,
Theoretical Computer Science 55 (1987) 87–136.
[2] J. Banks, Introduction to simulation, in: P. A. Farrington, H. B. Nembhard,
D. T. Sturrock, G. W. Evans (Eds.), Proceedings of the 31st conference on Winter
simulation: Simulation - a bridge to the future, WSC 1999, Phoenix, AZ, USA,
December 05-8, 1999, Volume 1, WSC, 1999, pp. 7–13.
Figure 14: Time property setter.
161
Salma Alharbi CEUR Workshop Proceedings 143–165
Figure 15: Calendar to set date.
Figure 16: Date consistency.
[3] B. Li, Visualisation and Analysis of Complex Behaviours using Structured Occurrence
Nets, Ph.D. thesis, School of Computing Science, Newcastle University, 2017.
[4] 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,
Figure 17: o-net with date consistency checking.
162
Salma Alharbi CEUR Workshop Proceedings 143–165
Figure 18: Buttons for time simulation.
Figure 19: Enabled event to simulate the time.
Figure 20: Year, Month, Day, Hour, Minute and Second.
2016, volume 1591 of CEUR Workshop Proceedings, CEUR-WS.org, 2016, pp. 35–55.
[5] M. Koutny, B. Randell, Structured occurrence nets: A formalism for aiding system
failure prevention and analysis techniques, Fundamenta Informaticae 97 (2009)
41–91.
[6] E. Pelz, Timed processes of interval-timed Petri nets, in: B. Schlingloff (Ed.),
Proceedings of the 25th International Workshop on Concurrency, Specification and
Programming, Rostock, Germany, September 28-30, 2016, volume 1698 of CEUR
Workshop Proceedings, CEUR-WS.org, 2016, pp. 13–24.
[7] I. Poliakov, V. Khomenko, A. Yakovlev, Workcraft - A framework for interpreted
graph models, in: G. Franceschinis, K. Wolf (Eds.), Applications and Theory of Petri
163
Salma Alharbi CEUR Workshop Proceedings 143–165
Nets, 30th International Conference, PETRI NETS 2009, Paris, France, June 22-26,
2009. Proceedings, volume 5606 of Lecture Notes in Computer Science, Springer,
2009, pp. 333–342.
[8] 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.
[9] B. Randell, Incremental construction of structured occurrence nets, Technical Report,
School of Computing, Newcastle University, 2013.
[10] B. Li, B. Randell, A. Bhattacharyya, T. Alharbi, M. Koutny, Soncraft: A tool
for construction, simulation, and analysis of structured occurrence nets, in: 18th
International Conference on Application of Concurrency to System Design, ACSD
2018, Bratislava, Slovakia, June 25-29, 2018, IEEE Computer Society, 2018, pp.
70–74.
[11] J. Kawises, W. Vatanawood, Formalizing time Petri nets with metric temporal
logic using promela, in: M. Nakamura, H. Hirata, T. Ito, T. Otsuka, S. Okuhara
(Eds.), 20th IEEE/ACIS International Conference on Software Engineering, Artificial
Intelligence, Networking and Parallel/Distributed Computing, SNPD 2019, Toyama,
Japan, July 8-11, 2019, IEEE, 2019, pp. 162–166.
[12] J. Euzenat, A. Montanari, Time granularity, in: M. Fisher, D. M. Gabbay, L. Vila
(Eds.), Handbook of Temporal Reasoning in Artificial Intelligence, volume 1 of
Foundations of Artificial Intelligence, Elsevier, 2005, pp. 59–118.
[13] T. Alharbi, M. Koutny, Visualising data sets in structured occurrence nets, in:
D. Moldt, E. Kindler, H. Rölke (Eds.), Proceedings of the International Workshop
on Petri Nets and Software Engineering (PNSE’18), co-located with the39th Interna-
tional Conference on Application and Theory of Petri Nets and Concurrency Petri
Nets 2018 and the 18th International Conference on Application of Concurrency to
System Design ACSD 2018, Bratislava, Slovakia, June 24-29, 2018, volume 2138 of
CEUR Workshop Proceedings, CEUR-WS.org, 2018, pp. 121–132.
[14] T. Alshammari, Towards automatic extraction of events for SON modelling, in:
M. Köhler-Bussmeier, D. Moldt, H. Rölke (Eds.), Petri Nets and Software Engineering
2022 co-located with the 43rd International Conference on Application and Theory of
Petri Nets and Concurrency (PETRI NETS 2022), Bergen, Norway, June 20th, 2022,
volume 3170 of CEUR Workshop Proceedings, CEUR-WS.org, 2022, pp. 188–201.
[15] M. Alahmadi, Master channel places for communication structured acyclic nets, in:
M. Köhler-Bussmeier, E. Kindler, H. Rölke (Eds.), Proceedings of the International
Workshop on Petri Nets and Software Engineering 2021 co-located with the 42nd
International Conference on Application and Theory of Petri Nets and Concurrency
(PETRI NETS 2021), Paris, France, June 25th, 2021 (due to COVID-19: virtual
conference), volume 2907 of CEUR Workshop Proceedings, CEUR-WS.org, 2021, pp.
233–240.
[16] N. Almutairi, M. Koutny, Verification of communication structured acyclic nets
using SAT, in: M. Köhler-Bussmeier, E. Kindler, H. Rölke (Eds.), Proceedings
164
Salma Alharbi CEUR Workshop Proceedings 143–165
of the International Workshop on Petri Nets and Software Engineering 2021 co-
located with the 42nd International Conference on Application and Theory of Petri
Nets and Concurrency (PETRI NETS 2021), Paris, France, June 25th, 2021 (due
to COVID-19: virtual conference), volume 2907 of CEUR Workshop Proceedings,
CEUR-WS.org, 2021, pp. 175–194.
[17] N. Almutairi, Probabilistic communication structured acyclic nets, in: M. Köhler-
Bussmeier, D. Moldt, H. Rölke (Eds.), Petri Nets and Software Engineering 2022
co-located with the 43rd International Conference on Application and Theory of
Petri Nets and Concurrency (PETRI NETS 2022), Bergen, Norway, June 20th, 2022,
volume 3170 of CEUR Workshop Proceedings, CEUR-WS.org, 2022, pp. 168–187.
A. Checking Consistency
Algorithm 6 first verifies Concurrent Consistency with respect to the late finish date and
time interval of the input places of the given event, then with respect to the early start
date and time intervals of the output places of the event, then invokes nodeConsistency
for the basic consistency checking of the event itself.
In Algorithm 7 asynchronous consistency function is invoked only if a so-net contains
a communication relation. The function applies two conditions for asynchronous and
synchronous-based checking. Formally, let 𝑞 be a channel place and let 𝑒, 𝑒′ be the
input and output events of 𝑞 respectively. The date information of 𝑞 is defined to be
a/synchronously consistent if and only if the following conditions are satisfied: 𝐼𝑓,𝑙
𝑒 = 𝐼𝑞
𝑠,𝑒
′ 𝑞
and 𝐼𝑠,𝑒
𝑒 =𝐼 .
𝑓,𝑙
In Algorithm 8, the behavioural consistenc function in line 4 verifies the consistency
of all binary relations in causal𝑈 , lines 7 and 9 verify the restrictions on the initial and
final places of the bso-net. The return value of the function is all the nodes which are
behaviourally inconsistent.
In ao-nets, each event has at least one input condition and at least one output condition,
and each condition has zero or more input and output events. A condition in ao-net can
have multiple input and output events that are in different scenarios. The verification of
the consistency of the alternative o-nets ensures that each condition is in at least one
scenario. Algorithm 9 displays the alternativeConsistency function in line 2. It states
that the early start date and time interval of 𝑐 is the same as the late finish date and
time interval of an input event 𝑒, line 4 states that the late finish date and time intervals
of 𝑐 are the same as the early start date and time intervals of an output event 𝑒′ .
165
Salma Alharbi CEUR Workshop Proceedings 143–165
Algorithm 6 Concurrent consistency
1: function:Boolean concurrent consistency (Event 𝑒)
2: for 𝑐 ∈ ∙ 𝑒 do
3: if 𝑐.𝐿𝑓 𝑖𝑛𝑖𝑠ℎ ̸= 𝑒.𝐸𝑠𝑡𝑎𝑟𝑡 then
4: return 𝐹 𝐴𝐿𝑆𝐸
5: for 𝑐 ∈ 𝑒∙ do
6: if 𝑐.𝐸𝑠𝑡𝑎𝑟𝑡 ̸= 𝑒.𝐿𝑓 𝑖𝑛𝑖𝑠ℎ then
7: return 𝐹 𝐴𝐿𝑆𝐸
return 𝑛𝑜𝑑𝑒𝐶𝑜𝑛𝑠𝑖𝑠𝑡𝑒𝑛𝑐𝑦(𝑒)
Algorithm 7 A/Synchronous consistency
1: function:Boolean asynchronous consistency(Channel place 𝑞)
2: if 𝑞.𝑖𝑛𝑝𝑢𝑡.𝐿𝑓 𝑖𝑛𝑖𝑠ℎ ̸= 𝑞.𝐸𝑠𝑡𝑎𝑟𝑡 ∨ 𝑞.𝑜𝑢𝑡𝑝𝑢𝑡.𝐸𝑠𝑡𝑎𝑟𝑡 ̸= 𝑞.𝐿𝑓 𝑖𝑛𝑖𝑠ℎ then
3: return 𝐹 𝐴𝐿𝑆𝐸
4: return 𝑛𝑜𝑑𝑒𝐶𝑜𝑛𝑠𝑖𝑠𝑡𝑒𝑛𝑐𝑦(𝑞)
Algorithm 8 behavioural consistency
1: function:Boolean behavioural consistency (Relation 𝑐𝑎𝑢𝑠𝑎𝑙𝑈 )
2: 𝑅𝑒𝑠𝑢𝑙𝑡 := ∅ ◁ behaviourally inconsistent nodes
3: for (𝑒1 , 𝑒2 )∈ 𝑐𝑎𝑢𝑠𝑎𝑙𝑈 do
4: if 𝑒1 .𝐸𝑠𝑡𝑎𝑟𝑡.𝑙𝑜𝑤𝑒𝑟 > 𝑒2 .𝐸𝑠𝑡𝑎𝑟𝑡.𝑙𝑜𝑤𝑒𝑟 ∨ 𝑒1 .𝐿𝑠𝑡𝑎𝑟𝑡.𝑢𝑝𝑝𝑒𝑟 > 𝑒2 .𝐿𝑠𝑡𝑎𝑟𝑡.𝑢𝑝𝑝𝑒𝑟 then
5: add 𝑒1 , 𝑒2 𝑡𝑜 𝑅𝑒𝑠𝑢𝑙𝑡
6: for 𝑐 ∈ C do
7: if ∙ 𝑐 = ∅ ∧ 𝑐.𝐸𝑠𝑡𝑎𝑟𝑡 ̸= 𝛽(𝑐).𝐸𝑠𝑡𝑎𝑟𝑡 then
8: add 𝑐 to 𝑅𝑒𝑠𝑢𝑙𝑡
9: else if 𝑐∙ = ∅ ∧ 𝑐.𝐿𝑓 𝑖𝑛𝑖𝑠ℎ ̸= 𝛽(𝑐).𝐿𝑓 𝑖𝑛𝑖𝑠ℎ then
10: add 𝑐 to 𝑅𝑒𝑠𝑢𝑙𝑡
11: return 𝑅𝑒𝑠𝑢𝑙𝑡
Algorithm 9 Alternative consistency
1: function:Boolean alternative consistency (Condition 𝑐)
2: if 𝑒.𝑖𝑛𝑝𝑢𝑡.𝐿𝑓 𝑖𝑛𝑖𝑠ℎ ̸ = 𝑐.𝐸𝑠𝑡𝑎𝑟𝑡 then
3: return 𝐹 𝐴𝐿𝑆𝐸
4: if 𝑒.𝑜𝑢𝑡𝑝𝑢𝑡.𝐸𝑠𝑡𝑎𝑟𝑡 ̸ = 𝑐.𝐿𝑓 𝑖𝑛𝑖𝑠ℎ then
5: return 𝐹 𝐴𝐿𝑆𝐸
166