ion-based analyses and simulations of timed behaviours of complex evolving systems using so-nets.
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 efective 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 uncertain 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.
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 ( ) 1 3 ℎ 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, • 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.) 0).
The paper [3] used communication structured occurrence nets (or cso-nets) to represent communication between diferent 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 an o-net (we denote C = ⋃︀ places, and ⊆ ( × E) ∪ (E × =1 , E = ⋃︀
=1 and F = ⋃︀ ). It is assumed that:
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 =1 ), is a set of channel • The onet ’s and are mutually disjoint.
}, belong to distinct component onet ; and |∙ | = 1 and | ∙ | ≤ 1. 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 = 0 onet1 ∪ · · · ∪ 0 onet and the final marking is fin cson = fin onet1 ∪ · · · ∪ fin onet . In 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
Behavioural structured occurrence nets (or bso-nets) model activities of evolving systems [3]. An execution history is represented on two diferent 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: ∈ ∙ ∩ ∙ ; and ▷
if (, ) ∈ ⋃︀ ′∈ ↑ causal( ′). 1. For every onet , there exists exactly one onet↑ satisfying ( ) ∩ ↑ ̸= ∅. 2. For every onet↑ represented by a chain onet↑ = 1 1 . . . −1 , the sequence 3. The relation (⊏ ∪ ≺ ∪ ◁)* ∘ ( ≺ ∪ ◁ ) ∘ (
≺ ∪ ⊏ ∪◁ )* over E ∪ E↑ is irreflexive, where: ≺ if there is ∈ C ∪ C↑ with ∈ ∙ ∩ ∙ ; ⊏ if there is ∈ ∪ ↑ with ( 0
onet ) ∩ 0cson↑ ̸= ∅. The final marking fin The initial marking 0bson of bso-net is 0cson↑ together with 0 bson is defined similarly.
onet for each such that ℎ ( ) ℎ ℎ ( ) ℎ
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 diferent 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 lfow relation, and : ∪ ∪
→ 2 ∖ { ∅} is a mapping, such that, for each ∈ tagon( ) = ( ( ), ( ), ( )) is an o-net , where for all ∈ such that ∈ ( ). The initial marking 0
∈ {, , tagon, final marking fin }, ( ) is the set of tagon, input and output of a node , i.e., ∙ and ∙ , in ton-nets are defined in the same way as in o-nets.
It is further assumed that for all ∈ , 0 tagon = 0 tagon( ) and fin tagon = fin tagon( ).
We define two nodes, and , as being alternatively related (or conflicting) if there are
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 1
T:0900-1000
T:1030-1100 D:10-20 2 ( ) 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]).
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 ifnish 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 ([ , ]). where ,
≤ ( ) ≤ ( ) states that the start time of
Notation. Let be a node in a so-net. The early and late date-time start interval of is denoted by = [ , , , ], where ,
≤ , respectively. The early and late date-time finish interval of is denoted by = [ , , , ], are the earliest and latest date-time start, , are the earliest and latest date-time start, respectively. The constraint 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 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) ∈ The information regarding node is node consistent if and only if [
[ , 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 [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 diferent subsystems. Communication between events is represented using special nodes (1) (2) 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. 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 diferent which indicates that 0 executes earlier than 1.
Time consistency in bso-nets. The verification of date and time consistency in bsonets 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) bso-net, the following must be true: (4) (5) (6) of the lower level o-net of the bso-net, the following must hold: In addition, for all conditions , ′ with ( , ′ ) ∈ and belonging to the final condition 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. 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 accidents, 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: [ , , , ] = [ , − , , −
] [ , , , ] = [ , + , , +
] [ , ] = [
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.
= ′ = ′ • 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 = [2022/11/23 06:06:06] and the late duration interval of the node 4 in is: , the second scenario is 4 = [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 diferent 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 ifring 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.
( )
( )
( )
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 (temporal) 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 ifring 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 efectively. 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].
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. ∪ ∙ , ℎ ∖ { (, 0) | ∈ }), where = { | (, 0) ∈ ℎ }.
0 1 3 4 0 1 ( ) 2 5
{(, − 1) | (, ) ∈ ℎ }). • Global events: −−:→ ′, provided that: −→ ′′ −→ ′′′ −→✓ ′, for some states ′′ ± − + 0 1 3 4
( ) 0
2 1
5 ( ) 2 5 Clearly, a global event −−:→ ′ may be such that = = ∅, in which case only the ± tick event has an efect. If, in addition, = (, ∅), then also the tick event has no efect and = ′ and is a terminal marking of acnet.
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 diferent 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 ifre 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. Algorithm 4 Timed Simulation algorithm of ON
Inputs: − current marking
− Occurrence Net with time intervals with a step enabled and time units then ◁ is ON-enabled if ∈ has time units then − if its time units = 0 then
according to its time units 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 − current marking
− set of scenarios (ONs) with time intervals Output: set of maximal steps (ONs) and time units ◁ is ON-enabled 1: 2: 5: 6: 7: 8: 9: 11: 12: 13: 14: 1: 2: 5: 6: 7: 8: 9: 11: 12: 13: 14: 3: := 4: for all ∈ T do of ON
then if ∙ ⊆ if
. , 10: for all t ∈
do , := , add to display duration in − ,
∧ ,
. 15: −calculate new state
−executed
Inputs: 3: array set of 4: for all ∈ T do for all ∙ if , ⊆ . 10: for all t ∈ set of if ∈ set of −
15: −calculate new state −executed
do , := , − ,
display duration in add to set of
∧ , if its time units = 0 then
do has time units then according to its time units
then 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.
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 diferent colours for each time unit ( Year :red, Month:magenta, Day:blue, Hour :green, Minute:purple, Second:cyan)
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. [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.
[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,
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. Schlinglof (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
of the International Workshop on Petri Nets and Software Engineering 2021
colocated with the 42nd International Conference on Application and Theory of Petri
Nets and Concurrency
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 ifnal 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 diferent 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 ′. 2 4 6 1 3 1 3 : 4 : 5 : 6 : 7 : 8 : 9 : 1 : 2 : 3 : 4 : 5 : g r t m 6
C n u r n c n i t n B o e n o c r e E l o i h
A f n t o B o e n s n h o o s o s s e c C i . r t r r t r . ∨ l o i h e a i u a c n i t n f n t o B o e n e a i u a c n i t n y f
r o i i , e 2 . . a d d ) ∅ ∈ > C d a 1 , t t 1 0 : 1 1 : r e t u r n i f i f . . r l
A B o t h t t