=Paper=
{{Paper
|id=Vol-3730/paper02
|storemode=property
|title=Synthesising ENI-Systems with Interval Order Semantics
|pdfUrl=https://ceur-ws.org/Vol-3730/paper02.pdf
|volume=Vol-3730
|authors=Maciej Koutny,Marta Pietkiewicz-Koutny
|dblpUrl=https://dblp.org/rec/conf/apn/KoutnyP24
}}
==Synthesising ENI-Systems with Interval Order Semantics==
https://ceur-ws.org/Vol-3730/paper02.pdf
Synthesising ENI-Systems with Interval Order
Semantics
Maciej Koutny1,∗ , Marta Pietkiewicz-Koutny1
1 School of Computing, Newcastle University
Urban Sciences Building, 1 Science Square, Newcastle Helix, Newcastle upon Tyne, NE4 5TG, United Kingdom
Abstract
Elementary net systems with inhibitor arcs are a class of fundamental Petri net models with very simple
markings which are sets of places. Their standard semantics is based on sequences of executed transitions
or, alternatively, as labelled total orders. In this paper, we introduce semantics based on interval (partial)
orders which allows one to describe behaviours where transitions have non-atomic duration. For such
a semantical model, we consider the net synthesis problem, and show that the standard notion of a
region of transition system (providing input to the synthesis procedure) can still be applied after suitable
modifications.
1. Introduction
Petri nets are a general model of concurrent systems which emerged in the 1960’s as a counterpart
to the state machines that were used so successfully to model sequential systems. A particular
advantage of Petri nets is that the model allows one to both specify concurrent system designs, and
the behaviours of such systems. It is generally acknowledged that concepts related to fundamental
notions of concurrency theory, such as causality and independence, can be well explained using
the framework provided by Petri nets (see, e.g., [1, 2, 3, 4]). A fundamental class of Petri
nets in that respect are Elementary Net Systems (EN-systems) [5]. In this paper, we consider
EN -systems extended with inhibitor arcs which allow testing for emptiness of places, which
results in Elementary Net Systems with Inhibitor Arcs (ENI-systems) [6, 7, 8, 9].
In general, the execution semantics of Petri nets (i.e., the representation of individual runs
or observations) is captured by total orders of executed transitions (or, equivalently, by firing
sequences), or stratified orders of executed transitions where simultaneity is transitive (or, equiv-
alently, by step sequences). Having said that, it was argued by Wiener in 1914 [10] (and later,
more formally, in [11]) that any execution that can be observed by a single observer must be an
interval order, and so the most precise (qualitative) observational semantics is based on interval
orders, where simultaneity is often non-transitive.
In this paper, extending the ideas presented in [12], we first show how one can generate interval
order executions of ENI-systems in a direct way, without the need to modify the original system
International Workshop on Petri Nets and Software Engineering, June, 2024, Geneva, Switzerland
∗ Corresponding author.
" maciej.koutny@ncl.ac.uk (M. Koutny); marta.koutny@ncl.ac.uk (M. Pietkiewicz-Koutny)
0000-0003-4563-1378 (M. Koutny)
© 2024 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)
33
CEUR
ceur-ws.org
Workshop ISSN 1613-0073
Proceedings
Maciej Koutny et al. CEUR Workshop Proceedings 33–52
specification (e.g., by splitting transitions into explicit beginnings and endings) as it was done,
for example, in [13, 14, 15]. We also define Interval Reachability Graphs (IR-graphs) which
are finite generators of potentially infinite sets of interval orders defined by ENI-systems. IR-
graphs are a subclass of Interval Transition Systems (IT-systems) which differ from the standard
transition systems since instead of having their arcs labelled by executed transitions, they have
states labelled by sets of transitions (interpreted as transitions currently being executed). Then,
assuming the interval order semantics of ENI-systems, we consider the problem of synthesising
ENI -systems from given IT -systems.
We approach the new synthesis problem using the standard synthesis approach based on the
theory of regions [16, 17, 18]. If one considers sequential behaviours of nets, a transition system
is realised by a net iff it is isomorphic to the sequential reachability graph (or case graph) of this
net. Ehrenfeucht and Rozenberg investigated the realisation of transition systems by elementary
nets and produced an axiomatic characterisation of all realisable transition systems in terms of
their regions [16, 17]. As in the existing literature about Petri net synthesis, we demonstrate that
all ENI-system realisable IT-systems are characterised by suitably adapted State Separation and
Forward Closure axioms.
The paper is organised as follows. In the next section, we recall basic facts about labelled partial
orders and ENI-systems, including their standard interleaving semantics. Section 3 introduces
our first major contribution, viz. the interval order semantics of ENI-systems which does not
rely on transition splitting, and the resulting IR-graph representation. The latter is a subclass of
IT -systems generating interval orders discussed in Section 4. Section 5 comprises our second
main contribution, viz. a full characterisation of those IT-systems which can be synthesised to
ENI -systems, and a procedure to do so. Section 6 contains concluding remarks and references to
relevant literature.
2. Preliminaries
2.1. Partial orders
Labelled partial orders with domain elements representing executed actions (events) are commonly
used in concurrency theory to formalise different notions of dynamic semantics.
A (strict labelled) partial order is a triple po = ⟨X, ≺, ℓ⟩ such that X (or Xpo ) is a set, ≺ (or
≺po ) is a binary relation over X which is irreflexive and transitive, and ℓ (or ℓpo ) is a labelling for
the elements of X. The maximal elements of po are maxpo = {x ∈ X | ¬∃y ∈ X : x ≺ y}. For all
x ̸= y ∈ X, x ⌒ y if x ̸≺ y ̸≺ x, i.e., ⌒ relates unordered elements. In this paper all partial orders
are assumed to be finite.
The partial order is total whenever, for all x ̸= y ∈ X, x ≺ y or y ≺ x. Moreover, it is interval
whenever, for all x, y, z, w ∈ X, if x ≺ z and y ≺ w then x ≺ w or y ≺ z. The adjective ‘interval’
derives from the following result (c.f. [19]):
A partial order ⟨X, ≺, ℓ⟩ is interval iff there are two integer-valued mappings on X,
β and ε, such that, for all x, y ∈ X, β (x) < ε(x) and x ≺ y ⇐⇒ ε(x) < β (y).
The mappings β and ε above are usually interpreted as ‘beginnings of’ and ‘endings of’ events
represented by the elements of X.
34
Maciej Koutny et al. CEUR Workshop Proceedings 33–52
As an example, consider four transactions in the distributed environment (e.g., local computa-
tions involving multiple communications by message passing): a, b, c, and d. Moreover, suppose
that a precedes b and c precedes d. Suppose further that a does not precede d and c does not
precede b. Then, it is possible for two messages α (from d to a) and β (from b to c) to be sent
and delivered. Hence αsnd ≺ αrcv ≺ βsnd ≺ βrcv ≺ αsnd , which is impossible. Hence a precedes d
or c precede b, and so the precedence relationship between the four transactions is an interval
order.
The relevance of interval orders follows from an observation, credited to Wiener [10], that
any execution of a physical system that can be observed by a single observer must be an interval
order. It implies that the most precise observational semantics should be defined in terms of
interval orders (cf. [11]). In the area of concurrency theory, the use of interval orders can be
traced back to [20, 21, 22, 23], and processes of concurrent systems with interval order semantics
were studied in [24, 25]. Interval orders were used to investigate communication protocols in [26],
using the approach of [27]. Interval semantics (ST-semantics) was investigated for Petri nets with
read arcs [28] and was discussed in the context of distributability of concurrent systems in [29].
2.2. Elementary net systems with inhibitor arcs and their standard semantics
Definition 1 (ENI-system). An elementary net system with inhibitor arcs (or ENI-system) is a
tuple eni = ⟨P, T, F, I, m0 ⟩, where P and T are disjoint finite sets of nodes, called respectively
places and transitions, F ⊆ (T × P) ∪ (P × T ) is the flow relation, I ⊆ P × T is the set of inhibitor
arcs, and m0 ⊆ P is the initial marking (in general, any subset of places is a marking). We denote:
• For a node x, • x = {y | ⟨y, x⟩ ∈ F} and x• = {y | ⟨x, y⟩ ∈ F}.
• For a set of nodes X, • X = {• x | x ∈ X} and X • = {x• | x ∈ X}.
⋃︁ ⋃︁
• For every transition t, ◦t = {p ∈ P | ⟨p,t⟩ ∈ I}.
• und(eni) = ⟨P, T, F, ∅, m0 ⟩.
We then require that the following hold, for all transitions t and places p:
1. •t ̸= ∅ ̸= t • and •t ∩ (t • ∪ ◦t) = ∅.
2. There is a place q such that • p = q• , p• = • q, and p ∈ m0 ⇐⇒ q ∈ / m0 .
• • • •
3. If q is a place such that p = q and p = q then p ∈ m0 ⇐⇒ q ∈ m0 .
4. There is no other place q such that • p = • q, p• = q• , and ◦ p = ◦ q. ⋄
Note that Definition 1(2,3,4) is included in order to simplify Definition 2. Also, und(eni)
can be regarded as an elementary net system (or EN-system, as defined in [12]) underlying eni,
and some of the subsequent definitions introduced for eni are conservative extensions of those
provided for und(eni) in [12].
In diagrams, places are represented by circles, transitions by rectangles, the flow relation by
directed arcs, the inhibitor arcs by edges with small circles, and a marking by small black dots
drawn inside places belonging to the marking.
Example 1. Figure 1 shows an ENI-system such that, e.g., • b = {p1 , p4 }, c• = {p4 , p6 }, and
◦ d = {p }. ⋄
4
35
Maciej Koutny et al. CEUR Workshop Proceedings 33–52
p1 p3 p5
a b c d
p2 p4 p6
Figure 1: eni-system.
Until Section 4.1, we assume that eni = ⟨P, T, F, I, m0 ⟩ is a fixed ENI-system.
The basic dynamic behaviour of ENI-systems is defined by sequences of executed transitions.
Definition 2 (firing sequences of ENI-system). The firing sequences of eni, denoted by SEQeni ,
are generated as follows.
• The empty sequence λ is a firing sequence of eni, and it leads to marking marλ = m0 .
• Let σ be a firing sequence of eni leading to marking marσ , and t be a transition such that
•t ⊆ mar and ◦t ∩ mar = ∅ (t is enabled at mar ). Then σt is a firing sequence of eni
σ σ σ
leading to marking marσt = (marσ \•t) ∪ t • . ⋄
Proposition 1. Let σ ∈ SEQeni , t ∈ T , and p, q ∈ P.
1. SEQeni ⊆ SEQund(eni) .
2. If • p = q• and p• = • q, then p ∈ mσ ⇐⇒ q ∈
/ mσ .
• ◦ •
3. If t ⊆ marσ and t ∩ marσ = ∅, then t ∩ marσ = ∅.
Proof. Straightforward, from the definitions which are conservative extensions of those intro-
duced for EN-systems, and results in [12].
Example 2. Figure 1 shows an ENI-system where, intuitively, three components represented by
cyclic sub-nets progress independently, but any action shared by two components can be executed
only if both of them do so. Moreover, d can only be executed if p4 is empty. Given a marking,
a transition of an ENI-system is enabled if its pre-places are marked, and the post-places and
inhibitor places are not marked (this follows from Definitions 1 and 2, and Proposition 1). ⋄
One can also associate labelled total orders of transition occurrences with the executed in-
terleaving sequences of transitions. In what follows, the n-th occurrence of transition t will be
denoted by t (n) and called event. The labelling function ℓ in total and partial orders in this paper
maps events (occurrences of transitions) to their names.
Definition 3 (total orders of ENI-system). The total orders of eni, denoted by TPOeni , are
generated as follows.
• tpo∅ = ⟨∅, ∅, ∅⟩ is a total order of eni, and it leads to marking martpo∅ = m0 .
36
Maciej Koutny et al. CEUR Workshop Proceedings 33–52
• Let tpo = ⟨X, ≺, ℓ⟩ be a total order of eni leading to marking martpo , and t be a transition
such that •t ⊆ martpo and ◦t ∩ martpo = ∅. Then,
tpo′ = ⟨X ∪ {x}, ≺ ∪(X × {x}), ℓ ∪ {⟨x,t⟩}⟩
−1 (t)|)
is a total order of eni leading to martpo′ = (martpo \•t) ∪ t • , where x = t (1+|ℓ . ⋄
Proposition 2.
1. TPOeni ⊆ TPOund(eni) .
2. {martpo | tpo ∈ TPOeni } ⊆ {martpo | tpo ∈ TPOund(eni) }.
Proof. Straightforward, from the definitions which are conservative extensions of those intro-
duced for EN-systems, and results in [12].
There is a canonical way of associating a labelled total order with a finite sequence of transitions
σ = t1 . . .tk (k ≥ 0), namely ξ (σ ) = ⟨{x1 , . . . , xk }, ≺, ℓ⟩, where x1 ≺ · · · ≺ xk and, moreover, each
(k )
xi = ti i is such that ℓ(xi ) = ti , and ki is the number of occurrences of ti in t1 . . .ti .
Proposition 3. ξ induces a bijection between SEQeni and TPOeni .
Proof. Straightforward, from the definitions which are conservative extensions of those intro-
duced for EN-systems, and results in [12].
In what follows, we will assume that each transition of an ENI-system occurs in at least one
firing sequence, i.e., there are no dead transitions.
3. Interval order semantics of eni-systems
The standard execution semantics of ENI-systems implicitly assumes that events are executed
instantaneously (atomically), or that their duration is negligible. In the semantical model adopted
in this paper, firing of transitions is transaction-like. By this we mean that when event x based on
transition (action) t starts its execution, it removes tokens from all the places in •t, and when x
ends its execution, then the tokens present in the places in t • become available for other transitions.
It is also important to note that certain relationships between net transitions will impose additional
constraints on the relationships between their occurrences (events). In particular, if event z based
on transition v adds a token to an inhibitor place of t, then z cannot directly precede event x (based
on t), and when v removes token from an inhibitor place of t, then z must finish before x starts.
Following the approach first introduced in [12], we now define an abstract interval order
semantics for eni. Similarly as in Definitions 2 and 3, we will use an inductive approach to define
interval order semantics of ENI-systems. This leads to the following question:
Given an interval order execution ipo, resulting from extending the initial empty
interval order by events, what could we say about the interval order obtained after
starting another transition? In other words, what could we say about ipo′ derived
from ipo after starting a single event x?
37
Maciej Koutny et al. CEUR Workshop Proceedings 33–52
Our answer is based on the following key observations:
(i) All non-maximal events in ipo should precede x.
(ii) The maximal events in ipo belong to three categories: Cntd comprises events which must be
continued, Fin events which must be finished, and the remaining events may be continued
or finished. More precisely,
(a) z ∈ Cntd if ℓ(z)• ∩ ◦t ̸= ∅, and then z ⌒ipo′ x.
(b) z ∈ Fin if ℓ(z)• ∩ •t ̸= ∅ or • ℓ(z) ∩ ◦t ̸= ∅, and then z ≺ipo′ x.
(c) z ∈ maxipo \(Cntd ∪ Fin) otherwise, and then z ≺ipo′ x or z ⌒ipo′ x.
(iii) Cntd ∩ Fin = ∅ as we cannot have both z ≺ipo′ x and z ⌒ipo′ x.
Intuitively, the maximal events in ipo can be considered ‘pending’ before starting x, and can either
be finished ‘just before’ x started, or continued to be finished after the execution of x has started.
In case (a) above, z ∈ Cntd has to continue as its finishing would put a token in a place which
acts as an inhibitor for t.
In case (b) above, we have two different reasons for finishing z ∈ Fin. First, if ℓ(z)• ∩ •t ̸= ∅,
then x needs a token produced by z to start its execution (this is also required when generating
interval order semantics of EN-systems in [12]). Second, if • ℓ(z) ∩ ◦t ̸= ∅ then there is a place p
inhibiting t which is also a pre-place for ℓ(z). If we allowed z ⌒ipo′ x, then x and z would become
overlapping events and so the order of their beginnings would be undetermined in terms of the
interval order semantics; in particular, x could start before z violating the inhibitor arc constraint.
In case (c) above, z can be either terminated or continued as it has no impact on the executability
of x. This is, in fact, the source of non-determinism which is not present in the standard
interleaving execution semantics of eni.
As explained in Section 6, the above treatment of interval order executions is consistent with
the semantics of inhibitor arcs proposed in, e.g., [15], where transitions are split and each inhibitor
arc is replaced by a pair of inhibitor arcs.
3.1. Interval orders generated by eni-systems
Definition 4 (interval orders of ENI-system). The interval orders of eni, denoted by IPOeni , are
generated as follows.
• ipo∅ = ⟨∅, ∅, ∅⟩ is an interval order of eni, and it leads to marking maripo∅ = m0 .
• Let ipo = ⟨X, ≺, ℓ⟩ be an interval order of eni leading to marking maripo , and t be a
transition such that
•
t ⊆ maripo \ℓ(Cntd)• and ◦
t ∩ (maripo \ℓ(Cntd)• ) = Cntd ∩ Fin = ∅ ,
where
Cntd = {z ∈ maxipo | ℓ(z)• ∩ ◦t ̸= ∅}
Fin = {z ∈ maxipo | ℓ(z)• ∩ •t ̸= ∅ ∨ • ℓ(z) ∩ ◦t ̸= ∅} .
Then
ipo′ = ⟨X ∪ {x}, ≺ ∪ ((X \ Exec) × {x}), ℓ ∪ {⟨x,t⟩}⟩
38
Maciej Koutny et al. CEUR Workshop Proceedings 33–52
is an interval order of eni, and it leads to marking maripo′ = (maripo \•t) ∪ t • , where
−1
Cntd ⊆ Exec ⊆ maxipo \Fin and x = t (1+|ℓ (t)|) .
t:ℓ(Exec)
We also denote ipo →eni ipo′ and ipo −−−−−→eni ipo′ . ⋄
Intuitively, Cntd are the maximal events of ipo which we must ‘keep’ executing simultaneously
with x, Fin are the maximal events of ipo which must be ‘finished’ before the start of x, and Exec
are all those maximal events of ipo which we keep ‘executing’ simultaneously with x (and so
Cntd ⊆ Exec and Fin ∩ Exec = ∅). The annotation of the arc, t:ℓ(Exec), means that the move
from ipo to ipo′ has been achieved by executing transition t, while the transitions in ℓ(Exec) that
started earlier are still active.
The nondeterministic execution of t results from having 2k , where k = | maxipo \(Cntd ∪ Fin)|,
possibilities for choosing Exec.
Definition 4 extends conservatively a corresponding definition of interval order semantics
introduced for EN-systems in [12]. More precisely, inhibitor arcs only restrict the enabling of
transition t, the next to be executed, while the rest of construction remains the same. We can
therefore carry over a number of suitably adapted results established in [12].
Proposition 4. Assume the notation as in Definition 4. Then:
1. t ̸∈ ℓ(maxipo ).
2. t • ∩ maripo = ∅.
3. maxipo′ \ maxipo = {x}.
4. Cntd ⊆ maxipo′ \{x} ⊆ maxipo \Fin.
5. ℓipo′ (maxipo′ \ maxipo ) = {t}.
6. ℓipo′ (maxipo′ \{x}) = ℓ(Exec) ⊆ ℓ(maxipo \Fin).
7. If x ̸= y ∈ X are such that ℓ(x) = ℓ(y), then x ≺ y or y ≺ x.
t:V t:V
8. If ipo −→eni ipo′ and ipo −→eni ipo′′ , then ipo′ = ipo′′ .
Proposition 5.
1. IPOeni is a set of labelled interval orders.
2. TPOeni ⊆ IPOeni ⊆ IPOund(eni) .
3. {maripo | ipo ∈ IPOeni } ⊆ {marσ | σ ∈ SEQund(eni) }.
Leading to the same marking is not enough to ensure that two generated interval orders have
the same extensions. The next definition adds another requirement.
Definition 5 (extension equivalent interval orders of ENI-system). Two interval orders of eni, ipo
and ipo′ , are extension equivalent if maripo = maripo′ and ℓipo (maxipo ) = ℓipo′ (maxipo′ ).
We denote this by ipo ∼eni ipo′ . ⋄
The above relation is an equivalence relation. Moreover, the following result will be needed to
define states of ENI-systems.
t:V t:V
Proposition 6. If ipo ∼eni ipo′ and ipo −→eni ipoo , then there is ipo′o such that ipo′ −→eni ipo′o
and ipoo ∼eni ipo′o .
Proof. It follows directly from Definition 4.
39
Maciej Koutny et al. CEUR Workshop Proceedings 33–52
{p1 , p2 }
p1 p2
a b
{p2 , p3 } {p1 , p4 }
a b
a
{p3 , p4 }
p3 p4
(a) (b)
{p1 ,p2 } 1
∅ ∅
{p2 ,p3 } {p1 ,p4 } 2 3
{a} {b} {a} {b}
{p3 ,p4 } {p3 ,p4 } 4 5
{a,b} {a} {a,b} {a}
(c) (d)
Figure 2: (a) eni-system; (b) its interleaving reachability graph; (c) its ir-graph; and (d) an isomorphic
it-system.
3.2. Reachable states and interval reachability graphs
In the standard semantics of ENI-systems, one usually associates the notion of a ‘reachable system
state’ with that of the marking reached after executing a firing sequence. This, in turn, leads to
the notion of the reachability graph of an ENI-system. Such graphs can be seen, in particular, as
generators of all the firing sequences that can be executed.
As observed in [12], markings alone are insufficient to identify states of EN-systems under the
interval order semantics. A solution to this problem proposed there, and one which we adopt in
the case of ENI-systems, is to associate a state of eni with all those interval orders which lead to
the same marking, and have the same set of labels of maximal events. The reason is that all the
‘continuations’ for such interval orders are the same.
We then define the reachability graph of an ENI-system.
Definition 6 (interval reachability graph of ENI-system). The interval reachability graph (or
IR -graph) of eni is irgeni = ⟨Q, →, q0 , ι⟩, where:
40
Maciej Koutny et al. CEUR Workshop Proceedings 33–52
{p1 ,p4 }
∅
p1 p4
{p2 ,p4 } {p1 ,p5 }
a {a} {c}
p2 c {p3 ,p4 } {p2 ,p5 } {p2 ,p5 }
{b} {a,c} {a}
b
{p3 ,p5 } {p3 ,p5 } {p3 ,p5 }
p3 p5 {c} {b,c} {b}
(a) (b)
Figure 3: (a) eni-system (some of the redundant places that are required by Definition 1 are omitted);
and (b) its ir-graph.
1. Q = {stateeni (ipo) | ipo ∈ IPOeni }, where stateeni (ipo) = ⟨maripo , ℓipo (maxipo )⟩ is the state
corresponding to ipo ∈ IPOeni .
2. →= {⟨stateeni (ipo), stateeni (ipo′ )⟩ | ipo →eni ipo′ } are the arcs.
3. q0 = stateeni (ipo∅ ) is the initial state.
4. ι : Q → 2T is the labelling such that we have ι(stateeni (ipo)) = ℓipo (maxipo ), for every
ipo ∈ IPOeni . ⋄
Example 3. Figure 2 shows both interleaving reachability graph and IR-graph of the ENI-system
in Figure 2(a). In Figure 2(c), we can see that at the state ⟨{p2 , p3 }, {a}⟩ transition b is enabled
because a(1) ∈ Cntd as a• ∩ ◦ b ̸= ∅ and, therefore, according to Definition 4, • b ⊆ {p2 , p3 } \ {p3 }
is satisfied and ◦ b ∩ ({p2 , p3 } \ {p3 }) = ◦ b ∩ {p2 } = ∅ is also satisfied. So, b can join active
event a(1) and the execution leads to the state ⟨{p3 , p4 }, {a, b}⟩, where both a and b are active.
Observe also that at the state ⟨{p1 , p4 }, {b}⟩, where a is enabled, we have two possibilities. As
b(1) ∈
/ Cntd and b(1) ∈ / Fin, the new transition a can join currently active b to overlap with it, or
can wait for b to finish, and only then to start its execution. ⋄
Example 4. Note that the maximal events of ipo of a state in an IR-graph can belong to Cntd
or Fin only with respect to the new transition to be executed. This is clearly visible in the
net and IR-graph depicted in Figure 3. For example, at the state ⟨{p2 , p4 }, {a}⟩ of the IR-
graph in Figure 3(b), two transitions are enabled, viz. b and c. At this state, if we want to
execute b, a(1) ∈ Fin (a• ∩ • b ̸= ∅) and therefore b must wait for a to finish in order to start its
execution leading to ⟨{p3 , p4 }, {b}⟩, where only b is active. However, if we want to execute c at
⟨{p2 , p4 }, {a}⟩, then a(1) ∈ Cntd (a• ∩ ◦ c ̸= ∅) meaning that according to Definition 4 transition
c is indeed enabled at this state, but c can only be executed at ⟨{p2 , p4 }, {a}⟩ by joining a.
Therefore executing c at ⟨{p2 , p4 }, {a}⟩ leads to ⟨{p2 , p5 }, {a, c}⟩, where both a and c are active.
41
Maciej Koutny et al. CEUR Workshop Proceedings 33–52
a a
b b
a b c c a b c c
(a) (b) (c) (d)
Figure 4: Interval orders generated by different paths in the transition system of Figure 3(b).
Consider then the state ⟨{p2 , p5 }, {a, c}⟩. At this state, b is enabled as a(1) ∈ Fin for b, and
(1)
c ∈ / Cntd ∪ Fin for b. Hence we have two possibilities for executing b at this state: it must wait
for a to finish, but it may wait for c to finish (leading to ⟨{p3 , p5 }, {b}⟩) or may overlap with c
(leading to ⟨{p3 , p5 }, {b, c}⟩). ⋄
In the next section, we will show that irgeni is a generator of all the interval orders of eni.
4. Transition systems generating interval orders
In general, we are interested in transition systems which are capable of generating interval orders.
Definition 7 (interval transition system). An interval transition system over T (or IT-system) is
its = ⟨S, →, s0 , ι⟩, where S is a finite set of states, →⊆ S × S is the set of arcs, s0 ∈ S is the initial
state, and ι : S → 2T is the labelling of states. The following hold, for all s, r, q ∈ S:
1. All states are reachable from s0 .
2. ι(s) = ∅ iff s = s0 .
3. If s → r, then there are t ∈ T \ ι(s) and V ⊆ ι(s) such that ι(r) = V ∪ {t}.
t:V t:V t:V
We also denote s −→ r. Moreover, we denote s −→ (or s − ̸ →) if there is (resp. there is no)
t:V
r ∈ S such that s −→ r.
t:V
4. For every t ∈ T , there are u ∈ S and V ⊆ T such that u −→.
t:V t:V
5. If s −→ r and s −→ q, then r = q. ⋄
Proposition 7. irgeni is an IT-system over T .
Proof. It follows from Definitions 6 and 4, Propositions 3 and 5 as well as the assumption that
each transition of an ENI-system occurs in at least one firing sequence.
IT -systems are generators of interval orders.
Definition 8 (interval orders of IT-system). Let its = ⟨S, →, s0 , ι⟩ be an IT-system. Its interval
orders, denoted by IPOits , are the interval orders ipoπ derived from paths π originating at the
initial state. They are generated as follows:
• ipoπ = ipo∅ is the interval order generated by π = s0 .
t:V
• Let π = s0 . . . sk be a path such that ipo = ipos0 ...sk−1 = ⟨X, ≺, ℓ⟩ and sk−1 −→ sk . Then
ipoπ = ⟨X ∪ {x}, ≺ ∪ ((X \ Exec) × {x}), ℓ ∪ {⟨x,t⟩}⟩
−1 (t)|)
is interval order generated by π, where Exec = maxipo ∩ℓ−1 (V ) and x = t (1+|ℓ . ⋄
42
Maciej Koutny et al. CEUR Workshop Proceedings 33–52
Example 5. Figure 4 shows interval orders generated by different paths in the transition system
of Figure 3(b). Every state of this transition system (IR-graph) is labelled by maximal elements of
the interval order (associated with the state) obtained so far by progressing along a particular
path. Going along the two ‘outer’ paths in Figure 3(b), we obtain interval orders depicted in
Figure 4(a, b). The ‘diamond’ at the top of the IR-graph indicates that transitions a and c can
overlap and that they can do this in more than one way, but in our semantics of ENI-systems, we
can only express the fact that a started its execution before c, or the other way around. After the
diamond, which shows the simultaneity of a and c, there are two possibilities for executing b: (i)
after both a and c finished their execution (Figure 4(c)); or (ii) b can start its execution waiting
only for a to finish, but joining c which is still active and can overlap with b (Figure 4(d)). ⋄
Proposition 8. IPOeni = IPOirgeni .
Proof. Follows directly from Definitions 4 and 8 as well as Proposition 7.
4.1. Isomorphic it-systems
The standard definition of transition system isomorphism can be adapted for IT-systems as
follows.
In this section, its = ⟨S, →, s0 , ι⟩ and itso = ⟨So , →o , so0 , ιo ⟩ are fixed IT-systems.
Definition 9 (isomorphism of IT-system). its and itso are isomorphic if there is a bijection
ψ : S → So such that ψ(s0 ) = so0 , ι = ιo ◦ ψ, and s → so ⇐⇒ ψ(s) →o ψ(so ), for all s, so ∈ S.
We denote this by its ≈ itso (or its ≈ψ itso ). ⋄
Directly from Definition 9, we have:
Proposition 9. ≈ is an equivalence relation.
IT -isomorphism is validated by the following immediate result.
Proposition 10. its ≈ itso implies IPOits = IPOitso .
The next three results included below are straightforward consequences of the fact that if in
t:V
an IT-system we replace each arc s → r by a labelled arc s −→ r, where {t} = ι(r) \ ι(s) and
V = ι(r) \ {t} (and remove the mapping ι), then the result is a deterministic finite state automaton
such that each state is reachable from the initial state.
Proposition 11. If its ≈ itso then there is exactly one ψ such that its ≈ψ itso .
Proposition 12. If its ≈ψ itso and s ∈ S, then:
t:V t:V
1. s −→ r implies that there is exactly one ro ∈ So such that ψ(s) −→o ro ; moreover, ψ(r) = ro .
t:V t:V
2. ψ(s) −→o ro implies that there is exactly one r ∈ S such that s −→ r; moreover, ψ(r) = ro .
IT -system isomorphism can be established in a rather simple way.
Proposition 13. Let ψ : S → So be an injective mapping such that ψ(s0 ) = so0 , and the following
hold, for all s ∈ S, t ∈ T , and V ⊆ T :
t:V t:V
• s −→ =⇒ ψ(s) −→o .
t:V t:V
• ψ(s) −→o s′o =⇒ s −→ s′ , for some s′ ∈ S such that s′o = ψ(s′ ).
Then its ≈ψ itso .
43
Maciej Koutny et al. CEUR Workshop Proceedings 33–52
5. Synthesis
The proposed synthesis procedure will follow the approach used in, e.g., [16, 17, 18, 30, 31, 32,
7, 9], where transition systems are used as behaviour specification from which places of Petri
nets are inferred in the form of regions. In our case, transitions systems are IT-systems. They are
realisable by ENI-systems with interval order semantics when the IR-graphs of synthesised nets
are isomorphic to the initial IT-systems.
Until Definition 11, we assume that its = ⟨S, →, s0 , ι⟩ is a fixed IT-system over T .
The regions we are going to introduce will be called inh-regions.
Definition 10 (inh-region of IT-system). An inh-region of its is r = ⟨Inr , Outr , Inhr , Sr ⟩, where
t:V
Inr , Outr , Inhr ⊆ T , and Sr ⊆ S are such that the following hold, for every s −→ r:
1. t ∈ Inr iff s ∈
/ Sr and r ∈ Sr .
2. t ∈ Outr iff s ∈ Sr and r ∈/ Sr .
3. If t ∈ Outr and v ∈ Inr ∩ ι(s), then v ∈ / ι(r).
4. If t ∈ Inr and v ∈ Outr ∩ ι(s), then v ∈ / ι(r).
5. If t ∈ Inhr and s ∈ Sr , then Inr ∩ ι(s) ̸= ∅.
6. If t ∈ Inhr and v ∈ Inr ∩ ι(s), then v ∈ ι(r).
7. If t ∈ Inhr and v ∈ Outr ∩ ι(s), then v ∈ / ι(r). ⋄
There are two kinds of trivial inh-regions, ⟨∅, ∅, ∅, S⟩ and ⟨∅, ∅, T ′ , ∅⟩ (for T ′ ⊆ T ). The
set of all non-trivial inh-regions of its is denoted by Rits , and Rs = {r ∈ Rits | s ∈ Sr } are the
non-trivial inh-regions comprising a state s ∈ S. We also denote, for all t ∈ T and U ⊆ T :
♦t = {r ∈ R ♦U = ⋃︁{♦t | t ∈ U}
its | t ∈ Outr }
t ♦ = {r ∈ Rits | t ∈ Inr } U ♦ = {t ♦ | t ∈ U}
⋃︁
(1)
♢t = {r ∈ R | t ∈ Inh } .
its r
Proposition 14. If r ∈ Rits then r = ⟨Outr , Inr , ∅, S \ Sr ⟩ ∈ Rits .
Proof. It follows from Definition 10. (Note that Definition 10(5,6,7) are trivially satisfied by
r.)
The next two results relate the inh-regions involved in a transition between two states of its.
t:V
Proposition 15. Let s −→ r. Then:
1. ♦t ∩ (t ♦ ∪ ♢t) = ∅.
2. ♦t ⊆ Rs and ♦t ∩ Rr = ∅.
3. Rs \ Rr = ♦t and Rr \ Rs = t ♦ .
Proof. (1) Suppose that r ∈ ♦t ∩ t ♦ . Then t ∈ Outr ∩ Inr . Hence, by Definition 10(1,2), we have
s ∈ Sr and s ∈/ Sr , yielding a contradiction.
Suppose now that r ∈ ♦t ∩ ♢t. Then t ∈ Outr ∩ Inhr . From t ∈ Outr and Definition 10(2), we
have s ∈ Sr . Hence, as t ∈ Inhr , by Definition 10(5) we have Inr ∩ ι(s) ̸= ∅. Let v ∈ Inr ∩ ι(s) ̸= ∅.
44
Maciej Koutny et al. CEUR Workshop Proceedings 33–52
Then, by Definition 10(6), we have v ∈ ι(r). On the other hand, by t ∈ Outr and v ∈ Inr ∩ ι(s) ̸= ∅,
we have, from Definition 10(3), that v ∈/ ι(r). Hence we obtained a contradiction.
(2) It follows from Definition 10(2).
(3) We only show Rs \ Rr = ♦t as the second part can be shown in a similar way.
By part (2), ♦t ⊆ Rs \ Rr . Suppose that r ∈ Rs \ Rr , i.e., s ∈ Sr and r ∈ / Sr . Then, by
Definition 10(2), we have t ∈ Outr , and so r ∈ ♦t. Thus, Rs \ Rr ⊆ ♦t.
t:V
Proposition 16. Let s −→. Then:
1. ♦t ⊆ Rs \ cntd♦
2. ♢t ∩ (Rs \ cntd♦ ) = ∅
3. cntd ∩ fin = ∅
4. cntd ⊆ V ⊆ ι(s) \ fin
where cntd = {v ∈ ι(s) | v♦ ∩ ♢t ̸= ∅} and fin = {v ∈ ι(s) | v♦ ∩ ♦t ̸= ∅ ∨ ♦ v ∩ ♢t ̸= ∅}.
t:V
Proof. Let r be such that s −→ r.
(1) By Proposition 15(2), we have ♦t ⊆ Rs . Suppose now, to the contrary, that there is v ∈ cntd
(i.e., v ∈ ι(s) and v♦ ∩ ♢t ̸= ∅) such that v♦ ∩ ♦t ̸= ∅. Then, by v ∈ ι(s), v♦ ∩ ♢t ̸= ∅ and
Definition 10(6), v ∈ ι(r). On the other hand, by v ∈ ι(s), v♦ ∩ ♦t ̸= ∅ and Definition 10(3),
v∈ / ι(r). Hence we obtained a contradiction.
(2) If r ∈ ♢t ∩ Rs then, by Definition 10(5), there is v ∈ ι(s) such that r ∈ v♦ . Thus v ∈ cntd
and r ∈ cntd♦ . Hence ♢t ∩ Rs ⊆ cntd♦ , and so part (2) is satisfied.
(3) It follows from Definition 10(3,6,7).
(4) By Definition 10(6), cntd ⊆ ι(r). Hence, by Definition 7(3), we have cntd ⊆ V . Moreover,
by Definition 10(3,7), we have fin ⊆ ι(s) \ ι(r). Hence, by Definition 7(3), we have V ⊆
ι(s) \ fin.
We can now provide a precise definition of all those IT-systems which can be translated into
semantically equivalent ENI-systems.
Definition 11 (ENI - IT-system). its is an ENI - IT-system if the following hold, for all t ∈ T , V ⊆ T ,
and s ̸= r ∈ S:
1. t ♦ ̸= ∅ ̸= ♦t.
2. If ι(s) = ι(r), then there is r ∈ Rits such that |Sr ∩ {s, r}| = 1. (state separation)
t:V
3. If s −
̸ →, then at least one of the following holds: (forward closure)
• t ∈ ι(s)
• V ̸⊆ ι(s)
• ♦t ̸⊆ Rs \ cntd♦
• ♢t ∩ (Rs \ cntd♦ ) ̸= ∅
• cntd ∩ fin ̸= ∅
• cntd ̸⊆ V
• V ̸⊆ ι(s) \ fin
where cntd and fin are as in Proposition 16. ⋄
45
Maciej Koutny et al. CEUR Workshop Proceedings 33–52
The above three ‘axioms’ characterise the ENI-system realisable IT-systems. ‘State separation’
requires that if two distinct states of its are not distinguished by at least one inh-region, then
they are distinguished by the labels of the maximal elements of their associated interval orders.
‘Forward closure’ is a variation of similar axioms that can be found in the literature for solving
synthesis problems, e.g., [18, 30, 31, 32, 7, 9]. Note, however, that both state separation and
forward closure axioms for ENI - IT-systems differ from their standard formalisation as they do
not rely only on inh-regions, but also on sets of transitions labelling the states.
Definition 12. The tuple associated with an ENI - IT-system its is given by eniits =
⟨Rits , T, Fits , Iits , Rs0 ⟩, where:
Fits = {⟨r,t⟩ ∈ Rits × T | t ∈ Outr } ∪ {⟨t, r⟩ ∈ T × Rits | t ∈ Inr }
Iits = {⟨r,t⟩ ∈ Rits × T | t ∈ Inhr } .
⋄
Until the end of this section, we assume that eni = eniits = ⟨Rits , T, Fits , Iits , Rs0 ⟩ is the tuple
associated with an ENI - IT-system its = ⟨S, →, s0 , ι⟩, and irgeni = ⟨Q, →o , q0 , ιo ⟩ is the IR-graph
of eniits . Moreover, we use the dot-notation in the context of eniits , and the diamond-notation in
the context of its.
Referring to irgeni as the ‘IR-graph of eniits ’ is justified as eniits is a valid ENI-system.
Proposition 17.
1. eniits is an ENI-system.
2. •t = ♦t, t • = t ♦ , and ◦t = ♢t, for every t ∈ T .
3. • r = Inr and r• = Outr , for every r ∈ Rits .
Proof. Parts (2) and (3) follow from Definition 12 and Eq.(1). With this in mind, we show part
(1) in the following way:
Definition 1(1) follows from Definition 11(1) and Propositions 15(1).
Definition 1(2) follows from Propositions 14.
Definition 1(3) follows from Definitions 10(1,2) and 7(1,4) as well as the fact that the places of
eniits are nontrivial regions of its.
Definition 1(4) follows from part (3) and Definition 10.
We then obtain the second major contribution of this paper.
Theorem 1. its ≈s irgeni , where s : S → Q is such that s(s) = ⟨Rs , ι(s)⟩, for every s ∈ S.
Proof. (The aim is to show that Proposition 13 can be applied.)
By Definition 11(2), s is an injective mapping.
By Proposition 17, eni is an ENI-system and, by Definition 7(1), all the states of its are reachable
from s0 . Also all the states of irgeni are reachable from q0 , which follows from the construction
of irgeni and the inductive approach of Definition 4. Furthermore, from Definition 6(3) we have
q0 = ⟨Rs0 , ∅⟩, and from Definition 7(2) we have ι(s0 ) = ∅. Hence, s(s0 ) = q0 .
Suppose now that s ∈ S and q ∈ Q are such that q = s(s). Then there is ipo = ⟨X, ≺, ℓ⟩ ∈ IPOeni
such that
q = stateeni (ipo) = ⟨maripo , ℓipo (maxipo )⟩ = ⟨Rs , ι(s)⟩ = s(s) .
Hence maripo = Rs and ℓipo (maxipo ) = ι(s). We then prove two lemmas.
46
Maciej Koutny et al. CEUR Workshop Proceedings 33–52
t:V t:V
Lemma 2. If q −→o q′ , then there is s′ ∈ S such that s −→ s′ and q′ = s(s′ ).
t:V t:V
To prove the lemma, we observe that, by q −→o q′ , there is ipo′ ∈ IPOeni such that ipo −→eni
ipo′ and
q′ = stateeni (ipo′ ) = ⟨maripo′ , ℓipo′ (maxipo′ )⟩
and, by Definition 4, the following hold:
• •t ⊆ maripo \ℓ(Cntd)•
• ◦t ∩ (maripo \ℓ(Cntd)• ) = Cntd ∩ Fin = ∅
• ipo′ = ⟨X ∪ {x}, ≺ ∪ ((X \ Exec) × {x}), ℓ ∪ {⟨x,t⟩}⟩
• maripo′ = (maripo \•t) ∪ t •
• V = ℓ(Exec)
• Cntd ⊆ Exec ⊆ maxipo \Fin
where:
• Cntd = {z ∈ maxipo | ℓ(z)• ∩ ◦t ̸= ∅}
• Fin = {z ∈ maxipo | ℓ(z)• ∩ •t ̸= ∅ ∨ • ℓ(z) ∩ ◦t ̸= ∅}
−1
• x = t (1+|ℓ (t)|) .
Hence, by Proposition 17, maripo = Rs , and ℓipo (maxipo ) = ι(s), we have:
• ♦t ⊆ Rs \ cntd♦
• ♢t ∩ (Rs \ cntd♦ ) = cntd ∩ fin = ∅ (the second part relies also on Proposition 4(7))
• ℓipo′ (maxipo′ ) = V ∪ {t}
• maripo′ = (Rs \ ♦t) ∪ t ♦
• cntd ⊆ V ⊆ ι(s) \ fin (relies also on Proposition 4(7))
where cntd and fin are as in Proposition 16.
t:V
Hence, by Proposition 4(1) and Definition 11, there is s′ ∈ S, such that s −→ s′ . Then, by
Propositions 15(3) and 17,
maripo′ = (maripo \•t) ∪ t • = (Rs \ ♦t) ∪ t ♦ = Rs′ .
Moreover, ℓipo′ (maxipo′ ) = V ∪ {t} = ι(s′ ). Hence, q′ = stateeni (ipo′ ) = ⟨Rs′ , ι(s′ )⟩ = s(s′ ) This
concludes the proof of Lemma 2.
t:V t:V
Lemma 3. If s −→ then q −→o .
t:V
To prove the lemma, we observe that, as s −→, by Definition 7(3) and Proposition 16, we have:
• t∈/ ι(s)
• V ⊆ ι(s)
• ♦t ⊆ Rs \ cntd♦
• ♢t ∩ (Rs \ cntd♦ ) = ∅
• cntd ⊆ V ⊆ ι(s) \ fin
• cntd ∩ fin = ∅
47
Maciej Koutny et al. CEUR Workshop Proceedings 33–52
where cntd and fin are as in Proposition 16.
Hence, by Proposition 17, maripo = Rs , and ℓipo (maxipo ) = ι(s), we have:
• t∈/ ℓipo (maxipo )
• V ⊆ ℓipo (maxipo )
• •t ⊆ maripo \ℓipo (Cntd)•
• ◦t ∩ (maripo \ℓipo (Cntd)• ) = ∅
• ℓipo (Cntd) ⊆ V (which implies Cntd ⊆ ℓ−1
ipo (V ))
• V ⊆ ℓipo (maxipo ) \ ℓipo (Fin) (which implies ℓ−1
ipo (V ) ⊆ maxipo \Fin)
• ℓipo (Cntd) ∩ ℓipo (Fin) = ∅ (which implies Cntd ∩ Fin = ∅)
where:
• Cntd = {z ∈ maxipo | ℓipo (z)• ∩ ◦t ̸= ∅}
• Fin = {z ∈ maxipo | ℓipo (z)• ∩ •t ̸= ∅ ∨ • ℓipo (z) ∩ ◦t ̸= ∅} .
−1 t:V
Let Exec = ℓ−1
ipo (V ) ∩ maxipo and x = t
(1+|ℓipo (t)|)
. We then have ipo −→eni ipo′ , where:
ipo′ = ⟨X ∪ {x}, ≺ ∪ ((X \ Exec) × {x}), ℓipo ∪ {⟨x,t⟩}⟩ .
t:V t:V
Hence ipo −→eni , and so q −→o . This concludes the proof of Lemma 3.
We then observe that, from s(s0 ) = q0 and Lemma 2 and the fact that all states in Q are
reachable from q0 , it follows that Q ⊆ s(S). Hence s is well-defined mapping. It is also injective
as its is an ENI - IT-system that satisfies Definition 11 (in particular, Definition 11(2)).
The theorem then follows from Proposition 13, Lemmas 2 and 3, s(s0 ) = q0 , and the fact that
s is a well-defined injective mapping.
6. Concluding remarks
As already mentioned, our treatment of interval order semantics of ENI-systems is consistent
with the semantics of inhibitor arcs proposed in, e.g., [15], where transitions are split and each
inhibitor arc is replaced by a pair of inhibitor arcs. Consider again the ENI-system eni shown in
Figure 3(a). The construction in [15], depicted in Figure 5(a), replaces each transition t by two
transitions, Bt (the beginning of t) and Et (the end of t), connected by a place pt . Moreover, the
inhibitor arc between p2 and c is replaced by two inhibitor arcs: one between p2 and Bc , and
the other between pb and Bc . It can then be checked that all the firing sequences of the resulting
ENI -system enisplit , from the initial marking {p1 , p4 } to the marking {p3 , p5 }, generate interval
orders which can also be generated by eni (the rule applied here is that t ≺ u iff Et precedes
Bu in the firing sequence). For example, the firing sequence σ = Ba Bc Ea Bb Ec Eb generates the
interval order in Figure 4(d) since Ea precedes Bb and this is the only relationship of this kind in
σ . And, conversely, each interval order generated by eni can also be generated by enisplit . One
might be tempted to remove the inhibitor arc between pb and Bc , yielding the ENI-system eni′split
depicted in Figure 5(b). This however, would not work as eni′split generates the firing sequence
Ba Ea Bb Bc Ec Eb which corresponds to the interval order such that a ≺ b, a ≺ b and b ⌒ c. Such
48
Maciej Koutny et al. CEUR Workshop Proceedings 33–52
p1 p1
Ba Ba
pa pa
Ea Ea
p2 p4 p2 p4
Bb Bc Bb Bc
pb pc pb pc
Eb Ec Eb Ec
p3 p5 p3 p5
(a) (b)
Figure 5: (a) eni-system with split transitions corresponding to the eni-system in Figure 3(a); and (b)
eni-system with split transitions which does not correspond to the eni-system in Figure 3(a).
an interval order cannot be generated by enisplit as it corresponds also to the firing sequence
Ba Ea Bc Bb Ec Eb which is inconsistent with the inhibitor arc between pb and Bc . Note finally that
an underlying assumption of the approach in [15] is that if σ Bt Bu σ ′ is a firing sequence then so
is σ Bu Bt σ ′ .
There are two main contributions of this paper extending results first presented in [12]. First,
we introduced a direct way of generating interval order executions of ENI-systems. We then
demonstrated that such a semantics can be succintly captured using a suitable class of transition
systems (ENI - IT-systems), where paths are associated with interval orders and states are labelled
with the maximal elements of these interval orders. As in [12], ENI-systems are executed
sequentially, but there is an assumption that every transition execution takes time and may
(partially) overlap with transitions that started earlier, but have not yet finished. We then introduced
and proved correct a translation from ENI - IT-systems to ENI-systems with interval order semantics
generating isomorphic transition systems. In doing so, we demonstrated that one can adapt the
synthesis approach based on the region concept developed for the standard transition systems to
work also for the ENI - IT-systems.
It is worth mentioning that the presented approach to constructing a system from ‘interval data’
differs from other approaches pursued in the area of Petri net synthesis and process mining.
The IT-systems (including IR-graphs) do not directly show the temporal relationships between
transitions/actions, but these relationships can be inferred from them during the synthesis proce-
dure and become evident in the synthesised ENI-systems. However, these relationships are not as
49
Maciej Koutny et al. CEUR Workshop Proceedings 33–52
precise as in other approaches found in the literature, where systems are discovered/synthesised
from behavioural information about the activities that are treated as non-instantaneous (i.e., taking
some time to complete). For example, Context-Aware Temporal Network Representation (TNR)
graphs of [33] that are extracted from event logs capture the global relationships between different
non-instantaneous activities/actions and use 13 relationships to relate the intervals of any two
activities as described by Allen’s Interval Algebra [34]. In our approach, we use an abstraction
that recognises only two relationships between the intervals related to two transitions, viz. one
can precede the other or they can overlap.
In essence, the approaches of [33, 34] are semantically close to real-time semantics whereas the
approach pursued in this paper is more abstract. For similar reasons, the interval order semantics
used in this paper and the ‘interval semantics’ or ‘interval time semantics’ of, e.g., [35, 36], are
incomparable.
Acknowledgments
The authors gratefully acknowledge three anonymous referees, whose comments contributed to
the final version of this paper.
References
[1] J. Desel, W. Reisig, Place/transition Petri nets, in: W. Reisig, G. Rozenberg (Eds.), Lectures
on Petri Nets I: Basic Models, Advances in Petri Nets, the volumes are based on the
Advanced Course on Petri Nets, held in Dagstuhl, September 1996, volume 1491 of Lecture
Notes in Computer Science, Springer, 1996, pp. 122–173.
[2] K. Jensen, Coloured Petri Nets. Basic Concepts, Analysis Methods and Practical Use.
Volume 1, Basic Concepts, Monographs in Theoretical Computer Science, Springer-Verlag,
1997.
[3] C. A. Petri, Concepts of net theory, in: Mathematical Foundations of Computer Science:
Proceedings of Symposium and Summer School, Strbské Pleso, High Tatras, Czechoslo-
vakia, September 3-8, 1973, Mathematical Institute of the Slovak Academy of Sciences,
1973, pp. 137–146.
[4] W. Reisig, Understanding Petri Nets - Modeling Techniques, Analysis Methods, Case
Studies, Springer, 2013.
[5] G. Rozenberg, J. Engelfriet, Elementary net systems, in: W. Reisig, G. Rozenberg (Eds.),
Petri Nets, volume 1491 of Lecture Notes in Computer Science, Springer, 1996, pp. 12–121.
[6] R. Janicki, M. Koutny, Semantics of inhibitor nets, Information and Computation 123
(1995) 1–16.
[7] N. Busi, G. M. Pinna, Synthesis of nets with inhibitor arcs, in: A. W. Mazurkiewicz,
J. Winkowski (Eds.), CONCUR ’97: Concurrency Theory, 8th International Conference,
Warsaw, Poland, July 1-4, 1997, Proceedings, volume 1243 of Lecture Notes in Computer
Science, Springer, 1997, pp. 151–165.
[8] M. Pietkiewicz-Koutny, Synthesis of eni-systems using minimal regions, in: D. Sangiorgi,
R. de Simone (Eds.), CONCUR ’98: Concurrency Theory, 9th International Conference,
50
Maciej Koutny et al. CEUR Workshop Proceedings 33–52
Nice, France, September 8-11, 1998, Proceedings, volume 1466 of Lecture Notes in Com-
puter Science, Springer, 1998, pp. 565–580.
[9] M. Pietkiewicz-Koutny, The synthesis problem for elementary net systems with inhibitor
arcs, Fundamenta Informaticae 40 (1999) 251–283.
[10] N. Wiener, A contribution to the theory of relative position, Proc. of the Cambridge
Philosophical Society 17 (1914) 441–449.
[11] R. Janicki, M. Koutny, Structure of concurrency, Theoretical Computer Science 112 (1993)
5–52.
[12] M. Pietkiewicz-Koutny, M. Koutny, Synthesising elementary net systems with interval order
semantics, in: L. Gomes, P. Leitão, R. Lorenz, J. M. E. M. van der Werf, S. J. van Zelst
(Eds.), Joint Proceedings of the Workshop on Algorithms & Theories for the Analysis of
Event Data and the International Workshop on Petri Nets for Twin Transition co-located with
the 44th International Conference on Application and Theory of Petri Nets and Concurrency
(Petri Nets 2023), Caparica, Portugal, June 25-30, 2023, volume 3424 of CEUR Workshop
Proceedings, CEUR-WS.org, 2023.
[13] E. Best, M. Koutny, Petri net semantics of priority systems, Theoretical Computer Science
96 (1992) 175–174.
[14] W. M. Zuberek, Timed Petri nets and preliminary performance evaluation, in: J. Lenfant,
B. R. Borgerson, D. E. Atkins, K. B. Irani, D. Kinniment, H. Aiso (Eds.), Proceedings of
the 7th Annual Symposium on Computer Architecture, La Baule, France, May 6-8, 1980,
ACM, 1980, pp. 88–96.
[15] R. Janicki, X. Yin, Modeling concurrency with interval traces, Information and Computation
253 (2017) 78–108.
[16] A. Ehrenfeucht, G. Rozenberg, Theory of 2-structures, part I: clans, basic subclasses, and
morphisms, Theoretical Computer Science 70 (1990) 277–303.
[17] A. Ehrenfeucht, G. Rozenberg, Theory of 2-structures, part II: representation through
labeled tree families, Theoretical Computer Science 70 (1990) 305–342.
[18] É. Badouel, L. Bernardinello, P. Darondeau, Petri Net Synthesis, Texts in Theoretical
Computer Science. An EATCS Series, Springer, 2015.
[19] P. C. Fishburn, Intransitive indifference with unequal indifference intervals, Journal of
Mathematical Psychology 7 (1970) 144–149.
[20] L. Lamport, The mutual exclusion problem: part I - a theory of interprocess communication,
Journal of ACM 33 (1986) 313–326.
[21] L. Lamport, On interprocess communication: part i: basic formalism, Distributed Comput-
ing 1 (1986) 77–85.
[22] V. R. Pratt, Modeling concurrency with partial orders, International Journal of Parallel
Programming 15 (1986) 33–71.
[23] R. Janicki, M. Koutny, Structure of concurrency, Theoretical Computer Science 112 (1993)
5–52.
[24] R. Janicki, M. Koutny, Fundamentals of modelling concurrency using discrete relational
structures, Acta Informatica 34 (1997) 367–388.
[25] R. Janicki, X. Yin, Modeling concurrency with interval traces, Information and Computation
253 (2017) 78–108.
[26] U. Abraham, S. Ben-David, M. Magidor, On global-time and inter-process communication,
51
Maciej Koutny et al. CEUR Workshop Proceedings 33–52
in: M. Kwiatkowska, M. W. Shields, R. M. Thomas (Eds.), Semantics for Concurrency,
Proceedings, Workshops in Computing, Springer, 1990, pp. 311–323.
[27] L. Lamport, Time, clocks, and the ordering of events in a distributed system, Communica-
tions of the ACM 21 (1978) 558–565.
[28] W. Vogler, Partial order semantics and read arcs, Theoretical Computer Science 286 (2002)
33–63.
[29] R. J. v. Glabbeek, U. Goltz, J.-W. Schicke-Uffmann, On characterising distributability,
Logical Methods in Computer Science 9 (2013) 1–58.
[30] É. Badouel, L. Bernardinello, P. Darondeau, Polynomial algorithms for the synthesis of
bounded nets, in: P. D. Mosses, M. Nielsen, M. I. Schwartzbach (Eds.), TAPSOFT’95: The-
ory and Practice of Software Development, 6th International Joint Conference CAAP/FASE,
Aarhus, Denmark, May 22-26, 1995, Proceedings, volume 915 of Lecture Notes in Computer
Science, Springer, 1995, pp. 364–378.
[31] L. Bernardinello, G. D. Michelis, K. Petruni, S. Vigna, On the synchronic structure of
transition systems, in: J. Desel (Ed.), Proceedings of the International Workshop on
Structures in Concurrency Theory, STRICT 1995, Berlin, Germany, May 11-13, 1995,
Workshops in Computing, Springer, 1995, pp. 69–84.
[32] M. Mukund, Petri nets and step transition systems, International Journal of Foundations of
Computer Science 3 (1992) 443–478.
[33] A. Senderovich, M. Weidlich, A. Gal, Context-aware temporal network representation of
event logs: Model and methods for process performance analysis, Information Systems 84
(2019) 240–254.
[34] J. F. Allen, Maintaining knowledge about temporal intervals, Communications of ACM 26
(1983) 832–843.
[35] E. Pelz, Full axiomatisation of timed processes of interval-timed Petri nets, Fundamenta
Informaticae 157 (2018) 427–442.
[36] L. Popova-Zeugmann, E. Pelz, Algebraical characterisation of interval-timed Petri nets with
discrete delays, Fundamenta Informaticae 120 (2012) 341–357.
52