Elementary net systems are fundamental Petri net models with very simple markings which are sets of places. Their standard semantics is based on sequences of executed transitions, which can be understood as (labelled) total orders. In this paper, we consider a newly proposed 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 a region of a transition system can still be applied.
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 [1, 2, 3, 4]. A fundamental class of Petri nets in that respect are Elementary Net systems (EN-systems) [5].
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, equivalently, by step sequences). Having said that, it was argued by Wiener in 1914 [6] (and later, more formally, in [7]) 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, using EN-systems as a system model, we first show how one can generate interval order observations of their executions in a direct way, without the need to modify the original system specification (e.g., splitting transitions into explicit beginnings and endings) as it was done, for example, in [8, 9, 10]. We also define interval reachability graphs ( IR-graphs) which can be seen as finite generators of potentially infinite sets of interval orders defined by EN-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 EN-systems, we consider the problem of synthesising EN-systems from given IT-systems.
We approach the new synthesis problem using the standard synthesis approach based on the theory of regions [11, 12, 13]. 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 the realisable transition systems in terms of regions [11, 12]. As in the existing literature about Petri net synthesis, the net realisable IT-systems are characterised by adapted State Separation and Forward Closure axioms.
Labelled partial orders with domain elements representing executed actions 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 (= Xpo) is a set, ≺ (=≺ po) is a binary relation over X which is irreflexive and transitive, and ℓ(= ℓpo) is a labelling for the elements of X . The maximal elements of po are maxpo = {x ∈ X | ¬∃y ∈ X : x ≺ y}, and nomaxpo = X \ maxpo are the non-maximal elements. For all x ̸= y ∈ X , x ⌒ y if x ̸≺ y ⊀ x.
If X = ∅ then po is the empty partial order denoted by ∅.
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.
The mappings β and ε above are usually interpreted as providing the ‘beginnings of’ and ‘endings of’ actions represented by the elements of X .
The relevance of interval orders in concurrency theory follows from an observation, credited to Wiener [6], 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. [7]).
Definition 1 (EN-system). An elementary net system (or EN-system) is a tuple en = ⟨P, T, F, 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 , and m0 ⊆ P is the initial marking (in general, any subset of places is a marking). Moreover, we have the following: p1 p2 a b
• For every node x, • x = {y | ⟨y, x⟩ ∈ F} and x• = {y | ⟨x, y⟩ ∈ F}. • For every transition t, • t ̸= ∅ ̸= t• and • t ∩ t• = ∅. • For every place p, there is a unique complement place p such that: • p = p• , p• = • p, and p ∈ m0 ⇐⇒ p ∈/ m0.
Note that the last part of Definition 1 is added to the standard one in order to simplify Definition 2.
In diagrams, places are represented by circles, transitions by rectangles, the flow relation by directed arcs, and a marking by small black dots drawn inside places belonging to the marking.
sub-nets progress independently, but any action shared by two components can be executed only if both of them do so.
The dynamic behaviour of EN-systems is introduced by defining valid sequences of executed transitions, called firing sequences .
Definition 2 (firing sequence) . Let en = ⟨P, T, F, m0⟩ be an EN-system. The firing sequences of en, denoted by SEQen, are generated as follows.
• The empty sequence λ is a firing sequence of en, and it leads to marking marλ = m0. • Let σ be a firing sequence of en leading to marking marσ , and t be a transition such that • t ⊆ marσ (t is enabled at marσ ). Then σt is a firing sequence of en leading to marking marσt = marσ \• t ∪ t• .
Note that the last part of Definition 1 implies that, for all places p ̸= q and reachable markings m, • p ̸= • q or p• ̸= q• or m(p) ̸= m(q) (markings are treated here as characteristic functions of sets they represent).
Proposition 1. Let en = ⟨P, T, F, m0⟩ be an EN-system, σ be a firing sequence of en, and t ∈ T be a transition such that • t ⊆ marσ . Then t• ∩ marσ = ∅.
Proof. Suppose that there is p ∈ P such that p ∈ t• ∩ marσ . The complement place p of p which belongs to P (Definition 1) is such that p ∈ • t ⊆ marσ . But p ∈ marσ as well, which is not possible as p and p are complementary places. Hence we obtained a contradiction.
An alternative way of defining the standard semantics of EN-systems is by associating labelled total orders of transition occurrences with the executed interleaving sequences of transitions. In what follows, the i-th occurrence of transition t will be denoted by t(i) and called event. Definition 3 (total orders of EN-system). Let en = ⟨P, T, F, m0⟩ be an EN-system. The total orders of en, denoted by TPOen, are generated as follows.
• The empty total order tpo∅ is a total order of en, and it leads to marking martpo∅ = m0. • Let tpo = ⟨X , ≺ , ℓ⟩ be a total order of en leading to marking martpo, and t be a transition such that • t ⊆ martpo. Then, tpo′ = ⟨X ∪ {x}, ≺ ∪
X × { x}, ℓ′⟩
(
– ℓ′|X = ℓ and ℓ′(x) = t.
Proposition 2. Let en = ⟨P, T, F, m0⟩ be an EN-system. Then TPOen is a set of labelled total orders.
Proof. Follows directly from the definitions.
There is a canonical way of associating a labelled total order with a finite sequence of transitions σ = t1 . . . tk (k ≥ 0), namely
seq2tpo(σ ) = ⟨{x1, . . . , xk}, ≺ , ℓ⟩ , where x1 ≺ · · · ≺ xk and, moreover, each xi = ti(ki) is such that ℓ(xi) = ti, and ki is the number of occurrences of ti in the sub-sequence t1 . . . ti.
Proposition 3. Let en = ⟨P, T, F, m0⟩ be an EN-system. Then seq2tpo induces a bijection between
Proof. Follows directly from the definitions.
The standard execution semantics of EN-systems implicitly assumes that events are executed instantaneously, or that their duration is negligible. Let us now assume that transitions are fired over intervals of arbitrary duration. Moreover, the firing of a transition t is transaction-like. By this we mean that the places in t• are locked when t starts its execution, and if the execution is ifnished, then the tokens present in these places become available for firing.
Our aim is to define an abstract interval order semantics for en in as simple as possible way. Hence, we start with the traditional way in which the firing of transitions is carried out by taking a ifring sequence t1 . . . tk. In such a view, the firings are instantaneous (or at least non-overlapping), and so they are implicitly ordered t1(m1) ≺ · · · ≺ tk(mk). Here, there exists an easy way of relating the executed transitions, which only takes into account the direct causal dependencies resulting from creating and consuming resources (tokens), viz. ti(mi) ≺ causal t j(mj) whenever ti• ∩ • t j ̸= ∅, for all 1 ≤ i < j ≤ k.
When working towards a sound interval order semantics for en in the case of interval overlapping, we could proceed by noting down the beginnings and ends of all the executed transitions and convert the ‘interval sequence’ obtained in this way into the corresponding interval order. It is crucial now to observe that, in general, the result is in no way based on the fundamental causality relationship (i.e., ≺ causal) which is inherent in EN-systems.
Similarly as in Definitions 2 and 3, we will use an inductive approach to define interval order semantics of EN-systems. This leads to the following question: Having observed a hypothetical interval order execution ipo, resulting from extending the initial empty interval order by observed events t1(m1), . . . , tk(mk), what could we say about the interval order obtained after firing of the beginning of another transition? In other words, what could we say about ipo′ derived from ipo after adding a single event x = t(n)? Our answer is based on the following key observations: (i) If v ∈ nomaxipo is a non-maximal event in ipo then, for sure, we should have v ≺ ipo′ x. (ii) If v ∈ maxipo is a maximal event in ipo such that ℓ(v)• ∩ • t ̸= ∅, then v must have terminated before x started, and we should have v ≺ ipo′ x. (iii) If v ∈ maxipo is a maximal event in ipo such that ℓ(v)• ∩ • t = ∅, then all we can be sure of is that v has not started after x finished, and so we should have either v ≺ ipo′ x or v ⌒ipo′ x. Intuitively, the maximal events in ipo can be considered ‘unfinished’ before starting x, and can either be ended ‘just before’ x started or continued to be finished after the execution of x has started. Note that the first two cases above, (i) and (ii), are deterministic. However, case (iii) is a source of non-determinism which is not present in the standard interleaving semantics of en.
In what follows, we will assume that each transition of an EN-system occurs in at least one ifring sequence, i.e., there are no dead transitions. 4.1. Interval orders generated by EN-systems Definition 4 (interval orders of EN-system). Let en = ⟨P, T, F, m0⟩ be an EN-system. The interval orders of en, denoted by IPOen, are generated as follows.
• The empty interval order ipo∅ is an interval order of en, and it leads to marking maripo∅ =
m0.
• Let ipo = ⟨X , ≺ , ℓ⟩ be an interval order of en leading to marking maripo, and t be a
transition such that • t ⊆ maripo. Then
ipo′ = ⟨X ∪ {x}, ≺ ∪
(nomaxipo ∪V ∪ W ) × { x}, ℓ′⟩
(
– ℓ′|X = ℓ and ℓ′(x) = t.
We also denote ipo →en ipo′ and ip→o− t en ipo′.
Note that in Definition 4 we need to consider all possible sets W . Even when {v ∈ maxipo | ℓ(v)• ∩ • t = ∅} = {w}, we have two possibilities: W = ∅ and W = {w}. The nondeterministic execution results from having 2|{v∈maxipo|ℓ(v)• ∩• t=∅}| choices of W .
Proposition 4. Let en = ⟨P, T, F, m0⟩ be an EN-system. If ipo →en ipo′ then there is a unique transition t such that
ℓipo′ (maxipo′ ) \ ℓipo(maxipo) = {t} and ℓipo′ (maxipo′ ) \ {t} ⊆ ℓipo(maxipo) .
Proof. Follows directly from Definition 4.
Proposition 5. Let en = ⟨P, T, F, m0⟩ be an EN-system, t ∈ T , and ipo ∈ IPOen. Moreover, let {ipo1, . . . , ipok} = {ipo′ | ip→o− t en ipo′} ̸= ∅ , where ipoi ̸= ipo j, for all 1 ≤ i < j ≤ k. Then:
{ℓipo1 (maxipo1 ) \ {t}, . . . , ℓipok (maxipok ) \ {t}} = 2(ℓipo1 (maxipo1 )∪∪· ℓipok (maxipok ))\{t} .
Proof. Follows directly from Definition 4 and Proposition 4.
Proposition 6. Let en = ⟨P, T, F, m0⟩ be an EN-system. Then IPOen is a set of labelled interval orders such that TPOen ⊆ IPOen.
Proof. Clearly, as we can always set W = maxipo \V , we have TPOen ⊆ IPOen.
To show that IPOen is a set of interval orders, we use Theorem 1. More precisely, for every ipo ∈ IPOen, we will show there exist suitable integer-valued functions βipo and εipo such that there is kipo ≥ 0 such that εipo(y) ≤ kipo, for all y ∈ nomaxipo, and εipo(z) = kipo + 1, for all z ∈ maxipo. We proceed by induction on the derivation of ipo.
In the base case there is nothing to show, and if ipo has one element x we set βipo(x) = 0 and εipo(x) = 2.
In the inductive case, we assume that ipo, x, and ipo′ are as in Definition 4. We then set βipo′ (x) = kipo + 2, εipo′ (x) = kipo + 3, and keep β and ε unchanged except for re-setting εipo′ (z) = kipo + 3, for all z ∈ maxipo′ \{x}. Moreover, kipo′ = kipo + 2.
Remark 1. The construction of interval orders in Definition 4 is not only a natural generalisation of that for the total orders of en, but it also can capture other semantics which might be used to define execution semantics of EN-systems. Below we describe some of more obvious possibilities, depending on the choice of W . (Note that the same option is taken at all the stages of an execution.) 1. W = maxipo \V . Then the construction generates all the total orders of en, as in Definition 3. 1 ∅ 5 {a,b} (d) b a 2 {a} 3 {b} 1A partial order po = ⟨X, ≺ , ℓ⟩ is stratified if {⟨x, y⟩ ∈ X × X | x ̸≺ y ̸≺ x} is an equivalence relation. 4.2. Reachable states and interval reachability graphs In the standard semantics of EN-systems, one usually associates the notion of a ‘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 EN-system. Such graphs can be seen, in particular, as generators of all the firing sequences that can be executed.
It is not difficult to see that markings alone are insufficient to identify states of EN-systems under
the interval order semantics. Consider, for example, the EN-system en depicted in Figure 3(a).
It generates two interval orders, ipo1 and ipo2, both with the domain {a(
Clearly, each ipo ∈ IPOen leads to a ‘state’. However, associating a state with each individual interval order would generate a huge (infinite) state space. This is not the way to go. It turns out that we can associate a state of en 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.
Definition 5 (equivalent interval orders). Let en = ⟨P, T, F, m0⟩ be an EN-system. Then ∼ be a binary relation on IPOen such that, for all ipo, ipo′ ∈ IPOen, we have ipo ∼ ipo′ if maripo = maripo′ and ℓipo(maxipo) = ℓipo′ (maxipo′ ).
The above relation is an equivalence relation. Moreover, as the next result states, it can be used to define system states.
Proposition 7. Let en = ⟨P, T, F, m0⟩ be an EN-system. If ipo1 ∼ ipo2 and ipo1 →en ipo′1, then there is ipo′2 such that ipo2 →en ipo′2 and ipo′1 ∼ ipo′2.
Proof. It follows directly from Definition 4.
We can then define the reachability graph of an EN-system.
Definition 6 (interval reachability graph). The interval reachability graph (or IR-graph) of an EN-system en = ⟨P, T, F, m0⟩ is irgen = ⟨Q, A, q0, i⟩, where: 1. Q = {⟨maripo, ℓipo(maxipo)⟩ | ipo ∈ IPOen} are the states. 2. A = {⟨⟨maripo, ℓipo(maxipo)⟩, ⟨maripo′ , ℓipo′ (maxipo′ )⟩⟩ | ipo →en ipo′} are the arcs. 3. q0 = ⟨m0, ∅⟩ is the initial state. 4. i : Q → 2T is the labelling such that i(q) = V , for every q = ⟨m,V ⟩ ∈ Q.
In the next section, we will show that irgen is a generator of all the interval orders of en. a b (a) (d) b c c a a c (b) c (e) b
c b a a (c) c ( f ) b b
the EN-system in Figure 3(a) using the equivalence relation on interval orders introduced in
4.3. 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. It is assumed that the following hold, for all s ∈ S:
2. ι (s) = ∅ iff s = s0. 3. If s → r, then there is t ∈ T such that ι (r) \ ι (s) = {t}, and ι (r) \ {t} ⊆ ι (s). We then also denote →s− t r.
Moreover, we denote →s− t if there is at least one r ∈ S such that →s− t r. t
5. If s → r and s → q are such that ι (r) = ι (q), then r = q. 6. If →s− t r and V ⊆ ι (r) \ {t}, then there is q ∈ S such that →s− t q and ι (q) = V ∪ {t}. 7. If →s− t r and →s− t r′ then there is r′′ ∈ S such that →s− t r′′ and ι (r′′) = ι (r) ∪ ι (r′). Proposition 8. Let en = ⟨P, T, F, m0⟩ be an EN-system. Then irgen is an IT-system over T . Proof. It follows from Definitions 4, 6 and 7 as well as Proposition 4.
Note that Definition 7(
IT-systems are generators of interval orders.
Definition 8 (interval orders of IT-system). The interval orders of an IT-system its = ⟨S, →, s0, ι ⟩, denoted by IPOits, are the interval orders ipoπ generated by its paths π originating at the initial state. They are generated as follows: • ipos0 is the empty interval order of its. • Let π = s0 . . . sk be a path in its such that ipo = ipos0...sk− 1 = ⟨X , ≺ , ℓ⟩ and sk− →1− t sk. Then ipoπ = ⟨X ∪ {x}, ≺ ∪
R × { x}, ℓ′⟩
(
– ℓ′|X = ℓ and ℓ′(x) = t.
Proposition 9. Let its = ⟨S, →, s0, ι ⟩ be an IT-system over T , t ∈ T , and s ∈ S. Moreover, let {s1, . . . , sk} = {s′ | →s− t s′} ̸= ∅ , where si ̸= s j, for all 1 ≤ i < j ≤ k. Then:
{ι (s1) \ {t}, . . . , ι (sk) \ {t}} = 2(ι(s1)∪∪· ι(sk))\{t} .
Also, for every u ∈ ι (s) \ (ι (s1) ∪ · · · ∪
ι (sk)), we have u ≺ t, where ≺ is as in Definition 8.
Proof. Follows directly from Definition 7(
Theorem 2. Let en = ⟨P, T, F, m0⟩ be an EN-system. IPOen = IPOirgen .
Proof. Follows directly from Definitions 4 and 8 as well as Proposition 8.
Definition 9. Two IT-systems, its = ⟨S, →, s0, ι ⟩ and its′ = ⟨S′, →′, s′0, ι ′⟩, are isomorphic if there is a bijection ψ : S → S′ such that: • ψ (s0) = s′0. • For all s, s′ ∈ S, s → s′ if and only if ψ (s) →′ ψ (s′).
• For every s ∈ S, ι (s) = ι ′(ψ (s)).
Our synthesis procedure follows the standard approach applied in [11, 12, 13, 15, 16, 17, 18, 19], where a transition system with its global states is used as an initial specification from which local states (places of Petri nets) are inferred in the form of regions. In our case, transitions systems are IT-systems. The verification that a given IT-system is realisable by an EN-system with interval order semantics is done by checking whether the interval reachability graph of the synthesised net is isomorphic to the initial IT-system. ⟨Inρ , Outρ , σρ ⟩, where Inρ , Outρ ⊆ following hold: Definition 10 (region). A region of an IT-system over T , its = ⟨S, →, s0, ι ⟩, is a triple ρ =
T and σρ : S → {0, 1} are such that, for every →s− t r, the 1. If t ∈ Inρ then σρ (s) = 0 and σρ (r) = 1. 2. If t ∈ Outρ then σρ (s) = 1 and σρ (r) = 0. 3. If σρ (s) = 1 and σρ (r) = 0, then t ∈ Outρ . 4. If σρ (s) = 0 and σρ (r) = 1, then t ∈ Inρ .
There are two trivial regions, ⟨∅, ∅,ˆ1︁⟩ and ⟨∅, ∅,ˆ0︁⟩, where ˆ1︁ and ˆ0︁ denote constant functions returning 1 and 0, respectively. The set of all non-trivial regions of its will be denoted by Rits. We also denote, for every t ∈ T :
t◦ = {ρ ∈ Rits | t ∈ Inρ } and ◦ t = {ρ ∈ Rits | t ∈ Outρ } .
The set of states associated with a region ρ = ⟨Inρ , Outρ , σρ ⟩ is given by Sρ = σ ρ− 1({1}). Also, we denote Rs = {ρ ∈ Rits | s ∈ Sρ }.
Proposition 10. Let its = ⟨S, →, s0, ι⟩ be an IT-system over T and t ∈ T be such that there is t s ∈ S with →s− . Then t◦ ∩ ◦ t = ∅.
Proof. Suppose →s− t s′ and ρ ∈ t◦ ∩ ◦ t. Then t ∈ Inρ ∩ Outρ . But, from Definition 10(
Proposition 11. Let its = ⟨S, →, s0, ι⟩ be an IT-system over T and →s− t s′. Then 1. ρ ∈ ◦ t implies s ∈ Sρ (σρ (s) = 1) and s′ ∈/ Sρ (σρ (s′) = 0).
2. ρ ∈ t◦ implies s ∈/ Sρ (σρ (s) = 0) and s′ ∈ Sρ (σρ (s′) = 1).
Proof. Follows directly from the definitions of t◦ and ◦ t and Definition 10(
Proof. We show Rs \ Rs′ = ◦ t as the second part can be shown in a similar way.
By Proposition 11(
Definition 11. The tuple associated with an IT-system over T , its = ⟨S, →, s0, ι⟩, is given as enits = ⟨Rits, T, Fits, Rs0 ⟩ where Fits = {(ρ,t) ∈ Rits × T | t ∈ Outρ } ∪ {(t, ρ) ∈ T × Rits | t ∈ Inρ }.
Proposition 13. Let its = ⟨S, →, s0, ι⟩ be an IT-system over T , and enits = ⟨Rits, T, Fits, Rs0 ⟩ be the tuple associated with it. Then, for every t ∈ T , • t = ◦ t and t• = t◦ .
Proof. Follows from Definition 11 and the definitions of ◦ t and t◦ .
Proposition 14. Let its = ⟨S, →, s0, ι⟩ be an IT-system over T , and ρ = ⟨Inρ , Outρ , σρ ⟩ ∈ Rits. Then ρ = ⟨Outρ , Inρ , σ ρ ⟩ ∈ Rits, where σ ρ (s) = 1 − σρ (s), for every s ∈ S.
Proof. Follows from Definition 10. (state separation) (forward closure)
The region ρ is called the complement of ρ .
Definition 12 (ENIT-system). Let its = ⟨S, →, s0, ι ⟩ be an IT-system over T . Then its is an ENIT-system over T if the following hold, for all t ∈ T and s, r ∈ S: 1. t◦ ̸= ∅ ̸= ◦ t. 2. If s ̸= r and ι (s) = ι (r), then there is a region ρ ∈ Rits such that
σρ (s) ̸= σρ (r) .
t
The above three ‘axioms’ characterise the EN-system realisable IT-systems. State separation requires that if two distinct states are not distinguished by at least one region, then they are distinguished by the labels of the maximal elements of their associated interval orders. Forward closure requires that for each action (i.e., transition label), a state at which the considered action has no occurrence is separated by a region from all states where this action occurs. While the forward closure axiom has similar form as ‘forward closure’ axioms that can be found in the literature for solving other synthesis problems [13, 15, 16, 17, 18, 19], the state separation axiom for ENIT-systems differs from its standard form as here the separation of states does not rely only on regions.
Proposition 15. Let its = ⟨S, →, s0, ι ⟩ be an ENIT-system over T . Then enits = ⟨Rits, T, Fits, Rs0 ⟩ is an EN-system.
Proof. Let t ∈ T . From Proposition 13 and Definition 12(
From Definition 7(
Proposition 16. Let its = ⟨S, →, s0, ι ⟩ be an ENIT-system over T , and en = enits = ⟨Rits, T, Fits, Rs0 ⟩ be the tuple associated with it. Then the states, arcs, and the labelling function of irgen = ⟨Q, A, q0, i⟩ are as follows: 1. Q = {⟨Rs, ι (s)⟩ | s ∈ S}. 2. A = {⟨⟨Rs, ι (s)⟩, ⟨Rs′ , ι (s′)⟩⟩ | s → s′}.
3. For every s ∈ S, i(⟨Rs, ι (s)⟩) = ι (s).
Proof. First, from Proposition 15 it follows that en is an EN-system. Note also that from
Definition 7(
Now we show that ⟨q, q′⟩ ∈ A and q = ⟨Rs, ι(s)⟩, for some s ∈ S, imply that there is s′ ∈ S such
that s → s′ and q′ = ⟨Rs′ , ι(s′)⟩. By ⟨q, q′⟩ ∈ A we have, from Definition 6(
From Proposition 13, we have then that ◦ t = {ρ ∈ Rits | t ∈ Outρ } ⊆ Rs and t◦ ∩ Rs = ∅ (t◦ = {ρ ∈ Rits | t ∈ Inρ }) .
Therefore, we have that for all ρ ∈ Rits:
1. t ∈ Outρ implies σρ (s) = 1 and
2. t ∈ Inρ implies σρ (s) = 0.
t
So, from Definition 12(
Therefore (see Definition 7(
maripoq′ = (maripoq \• t) ∪ t• = (Rs \ ◦ t) ∪ t◦ = Rs′ .
Hence maripoq′ = Rs′ .
If there are several states like s′, then the last conclusion will be true for all of them.
Furthermore, we have ℓipoq (maxipoq ) = ι(s). If in irgen we have several ‘children’ of the vertex q = ⟨Rs, ι(s)⟩ such that →q− t qi (1 ≤ i ≤ k) and q′ is one of them, then from Proposition 5 we have that their ℓipoqi (maxipoqi ) will form the set of all subsets of the set
ℓipoq (maxipoq ) \ {u ∈ T | the execution of t must follow the execution of u} .
From Proposition 9 we have that the ‘children’ of the vertex s in its (si such that →s− t si) will be labelled with the sets of transitions that are subsets of the same set of transitions as ℓipoq (maxipoq ) = ι(s) and so we will have the same number of children of q in irgen and children of s in its. Hence, if q′ is one of the qi’s then we will be able to find s′ among the si’s such that ℓipoq′ (maxipoq′ ) = ι(s′).
So, we proved that
Q ⊆ {⟨ Rs, ι(s)⟩ | s ∈ S} and A ⊆ {⟨⟨ Rs, ι(s)⟩, ⟨Rs′ , ι(s′)⟩⟩ | s → s′} .
We now prove the reverse inclusions. By Definitions 6(
By Definition 7(
From Definition 6(
If we have many ‘children’ of s in its (si such that →s− t si) and s′ is one of them, then the conclusion maripo′ = Rs′ will be true for all of them. Furthermore, we can use Propositions 5 and 9 to find the ‘child’ of the state ⟨Rs, ι(s)⟩ ∈ Q in irgen such that ℓipo′ (maxipo′ ) = ι(s′). Hence, we have ⟨Rs′ , ι(s′)⟩ ∈ Q and ⟨⟨Rs, ι(s)⟩, ⟨Rs′ , ι(s′)⟩⟩ ∈ A.
Finally, we observe that part (
Theorem 3. Let its = ⟨S, →, s0, ι⟩ be an ENIT-system over T , and en = enits = ⟨Rits, T, Fits, Rs0 ⟩ be the tuple associated with it. Then its is isomorphic to the IR-graph of en, irgen = ⟨Q, A, q0, i⟩. Moreover, the unique isomorphism ψ between its and irgen is given by ψ(s) = ⟨Rs, ι(s)⟩, for every s ∈ S.
Proof. Note that, by Proposition 16(
By Proposition 16(
We then observe that, by Proposition 16(
In this paper, we introduced a new class of transition systems (interval transition systems, or IT-systems) whose paths are associated with interval partial orders and labelled with the maximal elements of these interval orders. Also, we demonstrated how EN-systems can generate interval orders and produce their interval reachability graphs. In this paper, EN-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 not yet finished. We provided an axiomatisation of IT-systems that can be synthesised to EN-systems with interval order semantics (Definition 12 of ENIT-system). We showed that there is a possibility to adapt the synthesis approach based on the concept of regions of standard sequential transition systems to work also for the ENIT-systems.
Our approach to constructing a system from ‘interval data’ differs from other approaches pursued in the area of Petri net synthesis and process mining.
As already mentioned, in this paper we proposed a solution to the problem of synthesising EN-systems from IT-systems, whose states are labelled by sets of currently active transitions (there might be more than one), and whose arcs are implicitly labelled by single transitions representing new actions/activities responsible for the changes of states. As with any type of initialised transition systems, they capture the behaviour a system starting from its initial state and show its progress from state to state when transitions are executed.
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 procedure and become evident in the synthesised EN-systems. However, these relationships are not as 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 [20] 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 [21]. 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. As a result, at every state of an IT-system, a new active transition can follow the previously active transitions or join some of them to form a new set of active transitions.
In essence, the approaches of [20, 21] 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., [22, 23], are incomparable.
The authors gratefully acknowledge three anonymous referees, whose comments significantly contributed to the final version of this paper.