Elementary net systems (EN-systems) are a fundamental Petri net model with simple markings and simple connections between places and transitions. To enhance their modelling power, a number of extensions have been proposed such as transition probabilities or inhibitor arcs. In this paper, we consider EN-systems extended with read and mutex arcs. The resulting ENRM-systems allow one to capture a wider range of computational/dynamic systems than the original EN-systems. The standard semantical models of EN-systems and their extensions are based on sequences of executed transitions (or total orders) or sequences of sets of transitions executed simultaneously (or stratified orders). The ifrst kind of semantics does not capture simultaneity of executed transitions, and the second kind only allows a restrictive form of (transitive) simultaneity. In this paper, we introduce semantics of ENRM-systems based on interval (partial) orders which allows one to describe behaviours where transitions have non-atomic duration and the simultaneity of executed transitions does not need to be transitive. Assuming such a semantical model, we consider the net synthesis problem for ENRM-systems, and demonstrate that the standard notion of a region of a transition system (providing input to the synthesis procedure) can still be applied after suitable modifications.
Petri nets are a general model of concurrent systems which emerged as a counterpart to the state machines
that were used so successfully to model sequential systems. In particular, 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., [
The execution semantics of Petri nets (i.e., the representation of individual runs or observations) is often
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 can be argued that any execution that can be observed by a single observer must be an interval
order [
In this paper, extending the ideas presented in [
We also define Interval Reachability Graphs ( IR-graphs) which are finite generators of potentially infinite sets of interval orders defined by ENRM-systems. IR-graphs are a subclass of Interval Transition Systems (ITR-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 ENRM-systems, we consider the problem of synthesising ENRM-systems from given ITR-systems.
We approach the new synthesis problem using the standard synthesis approach based on the theory
of regions [
Though in a majority of the existing works dealing with synthesis problem(s) it was assumed that the
actions/transitions have atomic duration and are executed sequentially, there were also papers dealing
with non-atomic durations and partial order executions, e.g., [
The paper is organised as follows. In the next two sections, we recall basic facts about partial orders and introduce ENRM-systems. Section 4 presents our first contribution, viz. the interval order semantics of ENRM-systems which does not rely on transition splitting, and the resulting IR-graph representation. The latter is a subclass of ITR-systems generating interval orders discussed in Section 5. Section 6 comprises our second contribution, viz. a full characterisation of those ITR-systems which can be synthesised to ENRM-systems, and a procedure to do so. Section 7 concludes the paper.
Executions of concurrent systems can be represented by partial orders as acyclicity of events is a clear requirement resulting from physical considerations, and event precedence is transitive (this is true whether or not events are considered as instantaneous). Moreover, the simultaneity of events (corresponding to the overlapping of time intervals) amounts to the lack of ordering between events.
There are different partial order models of concurrent behaviours reeflcting, e.g., the underlying hardware and/or software. In the literature, there are three main kinds of such models, namely the total, stratified, and interval orders, as recalled below.
Let X be a finite set (of events), ≺ be a binary (precedence) relation over X , and ℓ be a labelling function for X (in this paper, labels are net transitions). Then po = ⟨X , ≺ , ℓ⟩ is called (below x, y, z, w ∈ X ): • partial order if x ̸≺ x and x ≺ y ≺ z =⇒ x ≺ z. • total order if x ̸≺ x, x ̸= y =⇒ x ≺ y ∨ y ≺ x, and x ≺ y ≺ z =⇒ x ≺ z. • stratified order if x ̸≺ x, x ̸≺ y ⊀ x ∧ x ≺ z =⇒ y ≺ z, x ≺ y ≺ z =⇒ x ≺ z, and x ̸≺ y ⊀ x ∧ z ≺ x =⇒ z ≺ y. • interval order if x ̸≺ x and x ≺ y ∧ z ≺ w =⇒ x ≺ w ∨ z ≺ y. (a) a orders which are discussed in this paper.
All total orders are stratified, all stratified orders are interval, and all interval orders are partial. The x ⊀ y
⊀
maximal elements of po = ⟨X , ≺ , ℓ⟩ are maxpo = {x ∈ X | ¬∃y ∈ X : x
≺ y}. For all x ̸= y ∈ X , x ⌒ y if
x, i.e., ⌒ relates unordered elements. Figure 1 shows examples of three different kinds of partial
The adjective in ‘interval order’ derives from an alternative definition (see [
The relevance of interval orders follows from an observation, credited to Wiener [
Interval order executions of, e.g., EN-systems can be generated by splitting each transition into a ‘begin’
followed by an ‘end’ transitions and, after executing the modified model using sequential semantics,
deriving the corresponding interval orders. However, this can also be done directly, i.e., without splitting
actions, as shown in [
In this section, we present ENRM-systems and two semantical models based on total and stratified orders. is the set of mutex arcs, and m0 ⊆ For every node x and every set of nodes X , we denote: Definition 1 (ENRM-system). An elementary net system with read and mutex arcs (or ENRM-system) is a tuple enrm = ⟨P, T, F, R, M, 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 , R ⊆ P × T is the set of read arcs, M ⊆
P × T
P is the initial marking (in general, any subset of places is a marking). • x x• ⊙ x ⊗ x x = • x ∪ ⊙ x ∪ ⊗ x = = = = {y | ⟨y, x⟩ ∈ F } {y | ⟨x, y⟩ ∈ F } {y | ⟨x, y⟩ ∈ R ∨ ⟨y, x⟩ ∈ R {y | ⟨x, y⟩ ∈ M ∨ ⟨y, x⟩ ∈ M} } • X X • ⊙ X ⊗ X
X = = = = ⋃︁{• x | x ∈ X } ⋃︁{x• | x ∈ X } ⋃︁{⊙ x | x ∈ X } ⋃︁{⊗ x | x ∈ X } = • X ∪ ⊙ X ∪ ⊗ X .
Moreover, und(enrm) = ⟨P, T, F, ∅, ∅, m0⟩. We then require, for all transitions t and places p: 1. • t ̸= ∅ ̸= t• and t• ∩ (• 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 q ̸= p such that • p = • q, p• = q• , ⊙ p = ⊙ q, and ⊗ p = ⊗ q.
The semantics of arcs ⟨x, y⟩ ∈ F in ENRM-systems is standard, i.e., as in EN-systems. The read arcs are formed when p ∈ ⊙ t and the mutex arcs are formed when p ∈ ⊗ t. Intuitively, p ∈ ⊙ t means that a marked p is needed for the execution of t, but such an execution does not change the marking of p. Similarly, p ∈ ⊗ t means that a marked p is needed for the execution of t and the execution of t does not change the p1 p2 a b marking of p; moreover, in this second case, no other transition which needs a marked p for its execution can be simultaneous with t.
Note that Definition 1(2,3,4) is included in order to simplify Definition 2. Also, und(enrm) can
be regarded as an elementary net system (EN-system) underlying enrm, and some of the subsequent
definitions introduced for enrm are conservative extensions of those provided for EN-systems in [
In diagrams, places are represented by circles, transitions by rectangles, the flow relation by directed arcs, the read arcs by edges with ⊙ as an arrowhead, the mutex arcs by edges with ⊗ as an arrowhead, and a marking by small black dots drawn inside places belonging to the marking. Figure 2 shows an ENRM-system such that, e.g., • b = {p1, p4}, c• = {p4, p6}, ⊙ d = {p4}, and ⊗ a = {p5}. Moreover, the initial marking is m0 = {p2, p3, p5}.
Until Section 5.1, we assume that enrm = ⟨P, T, F, R, M, m0⟩ is a fixed ENRM-system.
The first kind of dynamic behaviour of ENRM-systems is given using sequences of executed transitions. Definition 2 (firing sequences of ENRM-system). The firing sequences (of transitions) of enrm, denoted by SEQenrm, are generated as follows.
• The empty sequence λ is a firing sequence of enrm, and it leads to marking marλ = m0. • Let σ be a firing sequence of enrm 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 enrm leading to marking marσt = (marσ \• t) ∪ t• .
In what follows, we will assume that each transition of an ENRM-system occurs in at least one firing sequence, i.e., there are no dead transitions.
Figure 2 shows an ENRM-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 marked and a can only be executed if p5 is marked (in addition, a cannot be simultaneous with c though this feature is not relevant for the purely sequential semantics). For example, cdab is a firing sequence leading back to the initial marking.
One can also associate total orders of transition occurrences with the executed interleaving sequences of transitions. The n-th occurrence of transition t will be denoted by t(n) and called event. The labelling function ℓ in all partial orders in this paper maps events (occurrences of transitions) to their names. Definition 3 (total orders of ENRM-system). The total orders of enrm, denoted by TPOenrm, are generated as follows. • tpo∅ = ⟨∅, ∅, ∅⟩ is a total order of enrm, and it leads to marking martpo∅ = m0. • Let tpo = ⟨X , ≺ , ℓ⟩ be a total order of enrm leading to marking martpo, and t be a transition such that t ⊆ martpo. Then, tpo′ = ⟨X ∪ {x}, ≺ ∪ (X × { x}), ℓ ∪ {⟨x,t⟩}⟩ is a total order of enrm leading to martpo′ = (martpo \• t) ∪ t• , where x = t(1+|ℓ− 1(t)|).
Proposition 2. TPOenrm ⊆ TPOund(enrm) and {martpo | tpo ∈ TPOenrm} ⊆ { martpo | tpo ∈ TPOund(enrm)}.
To capture concurrent behaviour of ENRM-systems one can use sequences of sets of executed transitions (steps).
Definition 4 (step sequences of ENRM-system). The step sequences of enrm, denoted by SSEQenrm, are generated as follows.
• The empty sequence λ is a step sequence of enrm, and it leads to marking marλ = m0. • Let ξ be a step sequence of enrm leading to marking marξ , and t be a transition such that t ⊆ marξ .
Then ξ {t} is a step sequence of enrm leading to marking marξ {t} = (marξ \• t) ∪ t• . • Let ξ = ξ ′U be a step sequence of enrm leading to marking marξ , and t be a transition such that (1) • t ∪ ⊗ t ⊆ (2) ⊙ t ⊆ marξ \U • (marξ \U • ) ∪ • U (3) t ∩ ⊗ U = ∅ (4) ⊗ t ∩ U = ∅ .
Then ξ ′(U ∪ {t}) is a step sequence of enrm leading to marking marξ ′(U∪{t}) = (marξ \• t) ∪ t• .
Observe that the third item of Definition 4 contains the conditions that must be satisfied by t to be added to the step U to make a bigger step, U ∪ {t}, enabled at marξ ′ . Tokens from the places in • U are already ‘reserved’ for transitions from U (i.e., marξ ∩• U = ∅) and tokens in the places in U • are not available at marξ ′ . So, after the step sequence ξ ′, the pre-places of t and the mutex places of t must rely on the tokens that are not needed for the execution of any of the transitions from U to exclude conflicts for resources. This is captured by the inclusion in (1). The second inclusion, in (2), reflects the fact that the tokens from the places of • U , at the marking marξ ′ , can be used by t if it is connected to them by read arcs. Conflicts resulting from mutex arcs related to t or transitions from U are prevented by (3) and (4). Observe also that the condition (4) can be replaced by ⊗ t ∩ (⊗ U ∪ ⊙ U ) = ∅ as ⊗ t ∩ • U = ∅ is implied by (1).
One can also associate stratified orders of events with step sequences.
Definition 5 (stratified orders of ENRM-system). The stratified orders of enrm, denoted by SPOenrm, are generated as follows.
• spo∅ = ⟨∅, ∅, ∅⟩ is a stratified order of enrm, and it leads to marking marspo∅ = m0. • Let spo = ⟨X , ≺ , ℓ⟩ be a stratified order of enrm leading to marking marspo, and t be a transition such that t ⊆ marspo. Then spo′ = ⟨X ∪ {x}, ≺ ∪ (X × { x}), ℓ ∪ {⟨x,t⟩}⟩ is a stratified order of enrm leading to marspo′ = (marspo \• t) ∪ t• , where x = t(1+|ℓ− 1(t)|). • Let spo = ⟨X , ≺ , ℓ⟩ ̸= spo∅ be a stratified order of enrm leading to marking marspo, and t be a transition such that • t ∪ ⊗ t ⊆ ⊙ t ⊆ marspo \ℓ(maxspo)• (marspo \ℓ(maxspo)• ) ∪ • ℓ(maxspo)
t ∩ ⊗ ℓ(maxspo) = ⊗ t ∩ ℓ(maxspo) = ∅ ∅ .
Then spo′ = ⟨X ∪ {x}, ≺ ∪ ((X \ maxspo) × { x}), ℓ ∪ {⟨x,t⟩}⟩ is a stratified order of enrm leading to marspo′ = (marspo \• t) ∪ t• , where x = t(1+|ℓ− 1(t)|).
Proposition 4. SPOenrm ⊆ SPOund(enrm) and {marspo | spo ∈ SPOenrm} ⊆ { marspo | spo ∈ SPOund(enrm)}.
The above standard execution semantics of ENRM-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 consumes 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. Moreover, the read and mutex arcs impose additional constraints on the relationships between events. In particular, if event z based on transition v consumes a token from a read place of t, then z cannot directly precede event x (based on t), but when v adds a token to a read place of t, then z must finish before x starts.
Following the approach initiated in [
Given an interval order execution ipo, resulting from extending the initial empty interval order by successive events, what could we say about the interval order obtained after starting another enabled transition? In other words, what could we say about ipo′ derived from ipo after starting a single event x based on transition t? Our answer is based on the following key observations: (i) All non-maximal events in ipo must precede x. (ii) No maximal event in ipo has consumed a token that t wants to consume or exclusively reserve (i.e. z ∈ maxipo ⇒ • ℓ(z) ∩ (• t ∪ ⊗ t) = ∅). (iii) The maximal events in ipo belong to three categories: Cntd comprises events which must be continued when x starts, Fin events which must be finished before x starts, and any remaining events which may be continued or may be finished. More precisely, (a) z ∈ Cntd if • ℓ(z) ∩ ⊙ t ̸= ∅, (b) z ∈ Fin if (ℓ(z)• ∪ ⊗ ℓ(z)) ∩ t ̸= ∅ or ⊙ ℓ(z) ∩ ⊗ t ̸= ∅, (c) z ∈ maxipo \(Cntd ∪ Fin), (iv) Cntd ∩ Fin = ∅ as we cannot have both z ≺ ipo′ x and z ⌒ipo′ x. and then z ⌒ipo′ x.
and then z ≺ ipo′ x. and then z ≺ ipo′ x or z ⌒ipo′ x.
Intuitively, the maximal events in ipo can be considered ‘pending’ before starting x, and can either be ifnished ‘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 finish removing a token from a place which acts as a read place for t.
In case (b) above, we have different reasons for finishing z ∈ Fin. First, if ℓ(z)• ∩ t ̸= ∅, then x
needs a token produced by z for its execution (this is similar to the treatments in [
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 or step sequence execution semantics of enrm.
The observations we have just made lead to the following definition.
Definition 6 (interval orders of ENRM-system). The interval orders of enrm, denoted by IPOenrm, are generated as follows.
• ipo∅ = ⟨∅, ∅, ∅⟩ is an interval order of enrm, and it leads to marking maripo∅ = m0. • Let ipo = ⟨X , ≺ , ℓ⟩ be an interval order of enrm leading to marking maripo, and t be a transition such that • t ∪ ⊗ t ⊆
maripo \ℓ(Cntd)• and ⊙ t ⊆ (maripo \ℓ(Cntd)• ) ∪ • ℓ(Cntd) and Cntd ∩ Fin = ∅ , where Fin = {z ∈ maxipo | (ℓ(z)• ∪ ⊗ ℓ(z)) ∩ t ̸= ∅ ∨ ⊙ ℓ(z) ∩ ⊗ t ̸= ∅} and Cntd = {z ∈ maxipo | • ℓ(z) ∩ ⊙ t ̸= ∅}. Then, assuming that x = t(1+|ℓ− 1(t)|) and Cntd ⊆ Exec ⊆ maxipo \ Fin, ipo′ = ⟨X ∪ {x}, ≺ ∪
is an interval order of enrm leading to marking maripo′ = (maripo \• t) ∪ t• .
t:ℓ(Exec)
enrm 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 6 extends conservatively a corresponding definition of interval order semantics introduced
for EN-systems in [
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.
8. If ipo →−t:V enrm ipo′ and ipo →−t:V enrm ipo′′, then ipo′ = ipo′′ and maripo′ = maripo′′ .
Proposition 6. IPOenrm is a set of interval orders such that TPOenrm ⊆ SPOenrm ⊆ IPOenrm ⊆ IPOund(enrm) and {maripo | ipo ∈ IPOenrm} ⊆ { maripo | ipo ∈ IPOund(enrm)}.
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 7 (extension equivalent interval orders of ENRM-system). Two interval orders of enrm, ipo and ipo′, are extension equivalent if maripo = maripo′ and ℓipo(maxipo) = ℓipo′ (maxipo′ ). We denote this by ipo ∼ enrm ipo′.
Clearly, ∼ enrm is an equivalence relation. Moreover, the following result is needed to define states of ENRM-systems.
Proposition 7. If ipo ∼ enrm ipo′ and ipo →−t:V enrm ipoo, then there is ipo′o such that ipo′ →−t:V enrm ipo′o and ipoo ∼ enrm ipo′o. p1 a p4
As observed in [
We then define the reachability graph of an ENRM-system.
Definition 8 (interval reachability graph of ENRM-system). The interval reachability graph (or IR-graph) of enrm is irgenrm = ⟨Q, →, q0, ι ⟩, where: 1. Q = {stateenrm(ipo) | ipo ∈ IPOenrm}, where stateenrm(ipo) = ⟨maripo, ℓipo(maxipo)⟩ is the state corresponding to ipo ∈ IPOenrm. 2. → = {⟨stateenrm(ipo), stateenrm(ipo′)⟩ | ipo →enrm ipo′} are the arcs. 3. q0 = stateenrm(ipo∅) is the initial state. 4. ι : Q → 2T is the labelling such that ι (stateenrm(ipo)) = ℓipo(maxipo), for every ipo ∈ IPOenrm.
Figure 3(b) shows the IR-graph of enrm, the ENRM-system in Figure 3(a). It has 12 states given as follows, where ipoo is the interval partial order as in Figure 1(c): ⟨{p1, p2, p3}, ∅⟩ = stateenrm(poλ ) ⟨{p4, p2, p3}, {a}⟩ = stateenrm(poa) ⟨{p4, p5, p3}, {a}⟩ = stateenrm(poba) ⟨{p4, p2, p6}, {c}⟩ = stateenrm(poac) ⟨{p4, p2, p6}, {a}⟩ = stateenrm(poca) ⟨{p4, p5, p6}, {a, b}⟩ = stateenrm(ipoo) ⟨{p1, p5, p3}, {b}⟩ = stateenrm(pob) ⟨{p1, p2, p6}, {c}⟩ = stateenrm(poc) ⟨{p3, p4, p5}, {a, b}⟩ = stateenrm(po{a,b}) ⟨{p4, p2, p6}, {a, c}⟩ = stateenrm(po{a,c}) ⟨{p1, p5, p6}, {b}⟩ = stateenrm(pocb) ⟨{p4, p5, p6}, {a}⟩ = stateenrm(pocba).
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 4. E.g., at the state ⟨{p2, p4, p6}, {a}⟩ of the IR-graph in Figure 4(b), transitions b, c, and d are enabled. 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, p6}, {b}⟩, where only b is active. However, if we want to execute c at ⟨{p2, p4, p6}, {a}⟩, then a(1) ∈ Cntd (• a ∩ ⊙ c ̸= ∅) meaning that according to Definition 6 p1 p2 p3 a b transition c is indeed enabled at this state, but c can only be executed at ⟨{p2, p4, p6}, {a}⟩ by joining a. Therefore, executing c at ⟨{p2, p4, p6}, {a}⟩ leads to ⟨{p2, p5, p6}, {a, c}⟩, where both a and c are active. At the state ⟨{p2, p4, p6}, {a}⟩, d is also enabled. Its execution requires that a(1) ∈ Fin (a• ∩ ⊗ d ̸= ∅) and executing it leads to ⟨{p2, p4, p7}, {d}⟩, where only d is active.
Consider then ⟨{p2, p5, p6}, {a, c}⟩. At this state, b is enabled as a(1) ∈ Fin for b, and c(1) ∈/ Cntd ∪ Fin for b. Hence we have two possibilities for executing b: it must wait for a to finish, but it may wait for c to ifnish (leading to ⟨{p3, p5, p6}, {b}⟩) or may overlap with c (leading to ⟨{p3, p5, p6}, {b, c}⟩).
In the next section, we will show that irgenrm = ⟨Q, →, q0, ι ⟩ is a generator of all the interval orders of enrm. For that we need yet another result and an extension to the notation of Definition 8(2), where the annotation in →−t:V is used explicitly for ipo →−t:V enrm ipo′.
Proposition 8. For every ipo ∈ IPOenrm :
ipo →−t:V enrm ipo′ stateenrm(ipo) →−t:V q =⇒ =⇒ stateenrm(ipo) →−t:V stateenrm(ipo′) ∃ipo′ ∈ IPOenrm : ipo →−t:V enrm ipo′ ∧ q = stateenrm(ipo′) . (1)
In general, we are interested in transition systems which are capable of generating interval orders. Definition 9 (interval transition system). An interval transition system over T (or ITR-system) is itrs = ⟨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}.
We also denote s →−t:V r. Moreover, we denote s →−t:V (or s →−̸t:V ) if there is (resp. there is no) r ∈ S such that s →−t:V r. (a) a (e) a d b b (b) c ( f ) a a d c b b (c) (g) a c a b c d b (d) (h) a c a c d b b
a (i) c d b
Proposition 9. irgenrm is an ITR-system.
T such that u →−t:V .
The above proposition justifies the use of the same notations for the relations and labelling functions in irgenrm and itrs graphs.
Definition 10 (interval orders of ITR-system). Let itrs = ⟨S, →, s0, ι ⟩ be an ITR-system. Its interval orders, denoted by IPOitrs, 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. • Let π = s0 . . . sk be a path such that ipo = ipos0...sk− 1 = ⟨X , ≺ , ℓ⟩ and sk− 1 →−t:V sk. Then ipoπ = ⟨X ∪ {x}, ≺ ∪
((X \ Exec) × { x}), ℓ ∪ {⟨x, t⟩}⟩ is interval order generated by π , where Exec = maxipo ∩ ℓ− 1(V ) and x = t(1+|ℓ− 1(t)|).
Proposition 10. IPOenrm = IPOirgenrm .
The standard definition of transition system isomorphism can be adapted for ITR-systems as shown below, where itrs = ⟨S, →, s0, ι⟩ and itrs′ = ⟨S′, =⇒, s′0, ι′⟩ are fixed ITR-systems over T .
Definition 11 (isomorphism of ITR-systems). itrs and itrs′ are isomorphic if there is a bijection ψ : S → S′ such that ψ(s0) = s′0, ι = ι′ ◦ ψ, and s → r ⇐⇒ ψ(s) =⇒ ψ(r), for all s, r ∈ S.
We denote this by itrs ≈ ψ itrs′ and itrs ≈ itrs′. ⋄ Proposition 11. ≈ is an equivalence relation such that itrs ≈ itrs′ implies IPOitrs = IPOitrs′ .
The next result is consequence of the fact that if in an ITR-system we replace each arc s → r by a labelled arc s →−t:V r, where {t} = ι(r) \ ι(s) and V = ι(r) ∩ ι(s), and remove the mapping ι, then the result is a deterministic finite state automaton such that each state is reachable from the initial state. Proposition 12. If itrs ≈ itrs′ then there is exactly one ψ such that itrs ≈ ψ itrs′. Also, if s ∈ S then: 1. s →−t:V r implies that there is exactly one r′ ∈ S′ such that ψ(s) =t:⇒V r′; moreover, ψ(r) = r′. 2. ψ(s) =t:⇒V r′ implies that there is exactly one r ∈ S such that s →−t:V r; moreover, ψ(r) = r′.
The synthesis procedure introduced in this section follows the standard approach applied in [
Until Definition 13, we assume that itrs = ⟨S, →, s0, ι⟩ is a fixed ITR-system over T . The regions we are going to introduce will be called RM-regions.
Definition 12 (RM-region of ITR-system). An RM-region of itrs is r = ⟨Inr, Outr, Readr, Mutr, Sr⟩, where Inr, Outr, Readr, Mutr ⊆ T , and Sr ⊆ S are such that the following hold, for all s →−t:V r and v ∈ T : 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 ∈ Readr and s ∈/ Sr, then Outr ∩ ι(s) ̸= ∅. 6. If t ∈ Readr and v ∈ Outr ∩ ι(s), then v ∈ ι(r). 7. If t ∈ Readr and v ∈ (Inr ∪ Mutr) ∩ ι(s), then v ∈/ ι(r). 8. If t ∈ Mutr and v ∈ (Inr ∪ Readr ∪ Mutr) ∩ ι(s), then v ∈/ ι(r).
9. If t ∈ Outr and v ∈ Mutr ∩ ι(s), then v ∈/ ι(r). 10. If t ∈ Mutr then s ∈ Sr.
There are two trivial RM-regions, ⟨∅, ∅, ∅, ∅, S⟩ and ⟨∅, ∅, ∅, ∅, ∅⟩. The set of all non-trivial RMregions of itrs is denoted by Ritrs, and Rs = {r ∈ Ritrs | s ∈ Sr} are the non-trivial RM-regions comprising a state s ∈ S. We also denote, for all t ∈ T and U ⊆ T : ■ t = {r ∈ Ritrs | t ∈ Outr} ⊠ t = {r ∈ Ritrs | t ∈ Mutr} ■ U = ⋃︁{■ t | t ∈ U } t■ = {r ∈ Ritrs | t ∈ Inr}
t = {r ∈ Ritrs | t ∈ Readr} U ■ = ⋃︁{t■ | t ∈ U } t = ■ t ∪ t ∪ ⊠ t
U = ⋃︁{ t | t ∈ U } ⊠ U = ⋃︁{⊠ t | t ∈ U } .
(2) Proposition 13. If r = ⟨Inr, Outr, Readr, Mutr, Sr⟩ ∈ Ritrs then r = ⟨Outr, Inr, ∅, ∅, S \ Sr⟩ ∈ Ritrs.
To provide some intuition for Definition 12, we need to look ahead and imagine that regions will become places of the synthesised net. Then, Sr is the set of states where region/place r is marked or waiting to be marked. The transitions from Inr will deposit tokens in r (Definition 12( 1)), and transitions from Outr will be consuming tokens from r (Definition 12( 2)). As the transition t will be executing in the context of some currently active transitions, Definition 12( 3, 4, 7, 8, 9) must make sure that some previously active transitions, say v, which share parts of their environment with t, should finish their executions before t starts, respecting the properties of places in ENRM-systems and/or the need of some of the transitions to have mutually exclusive access to the token of the place/region r. Definition 12( 5) captures the situation where t is connected to place/region r by a read arc. As t is enabled at s and s ∈/ Sr (r is not marked at s), the only possibility of t ‘seeing’ a token in r is the existence of some other active transition from Outr, say v, which is in the process of consuming this token. Definition 12( 6) is then making sure that v continues its execution as t starts, so the token is not yet consumed. Finally, Definition 12( 10) guarantees that if a transition t is enabled at s and is connected to r by a mutex arc,
The next two results relate the RM-regions involved in a move between two states of itrs. transition connected to r as it was done when t ∈ Readr (see Definition 12(5,6)). then r must be marked at s (s ∈ Sr) as, with respect to place r, t cannot be ‘helped’ by any other active Proposition 14. Let s →−t:V r. Then: Proposition 15. Let s →−t:V . Then: t■ ∩ t = ∅ ■ t ⊆
Rs ■ t ∩ Rr = ∅
Rs \ Rr = ■ t
Rr \ Rs = t■ . ■ t ∪ ⊠ t ⊆ (Rs \ cntd■ ) ∪ ■ cntd cntd ∩ fin = ∅ cntd ⊆ V ⊆ ι (s) \ fin where cntd = {v ∈ ι (s) | ■ v ∩ t ̸= ∅} and fin = {v ∈ ι (s) | (v■ ∪ ⊠ v) ∩ t ̸= ∅ ∨ v ∩ ⊠ t ̸= ∅}.
We can now provide a precise definition of all those ITR-systems which can be translated into semantically equivalent ENRM-systems.
T , and s ̸= r ∈ S: Definition 13 (ENRM-ITR-system). Let itrs = ⟨S, →, s0, ι ⟩ be an ITR-system over T . Then itrs is an 1. t■ ̸= ∅ ̸= ■ t. 3. If s ↛−
t:V , then at least one of the following holds: 2. If ι (s) = ι (r), then there is r ∈ Ritrs such that |Sr ∩ {s, r}| = 1. (state separation) (forward closure) ■ t ∪ ⊠ t ⊈ (Rs \ cntd■ ) ∪ ■ cntd t ∈ ι (s) V ̸⊆ ι (s) cntd ∩ fin ̸= ∅ cntd ̸⊆ V
V ̸⊆ ι (s) \ fin where cntd and fin are as in Proposition 15.
The above three ‘axioms’ characterise the ENRM-system realisable ITR-systems. ‘State separation’
requires that if two distinct states of itrs are not distinguished by at least one RM-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., [
Definition 14.
The tuple associated with an ENRM-ITR-system itrs is given by enrmitrs = ⟨Ritrs, T, Fitrs, Ritrs, Mitrs, Rs0 ⟩, where:
Fitrs Ritrs Mitrs = = = {⟨r, t⟩ ∈ Ritrs × T | t ∈ Readr} {⟨r, t⟩ ∈ Ritrs × T | t ∈ Mutr} . {⟨r, t⟩ ∈ Ritrs × T | t ∈ Outr} ∪ {⟨t, r⟩ ∈ T ×
Until the end of this section, we assume that enrm = enrmitrs = ⟨Ritrs, T, Fitrs, Ritrs, Mitrs, Rs0 ⟩ is the tuple associated with an ENRM-ITR-system itrs = ⟨S, →, s0, ι⟩, and irgenrm = ⟨Q, →o, q0, ιo⟩ is the IRgraph of enrmitrs. Moreover, we use the circle-notation in the context of enrmitrs, and the box-notation in the context of itrs.
Referring to irgenrm as the ‘IR-graph of enrmitrs’ is justified as enrmitrs is a valid ENRM-system. Proposition 16.
1. enrmitrs is an ENRM-system. 2. • t = ■ t, t• = t■ , ⊙ t = t, and ⊗ t = ⊠ t, for every t ∈ T . 3. • r = Inr and r• = Outr, for every r ∈ Ritrs.
We then obtain the second major contribution of this paper.
Theorem 1. itrs ≈ s irgenrm, where s : S → Q is such that s(s) = ⟨Rs, ι(s)⟩, for every s ∈ S.
As already mentioned, our treatment in interval order semantics of ENRM-systems of read arcs is consistent
with that of inhibitor arcs introduced in [
We expect that the theoretical concepts and results presented in this paper and its predecessors [
The ITR-systems (including IR-graphs) do not directly show all the relationships between
transitions/actions, but these relationships can be inferred from them during the synthesis procedure and become
evident in the synthesised ENRM-systems. One can also find other treatments of non-atomic actions in
the literature. For example, Context-Aware Temporal Network Representation (TNR) graphs of [
This research was supported by the Leverhulme Trust funded grant RPG-2022-025. The authors are grateful to the anonymous referees, whose comments contributed to the final version of this paper.
The authors have not employed any Generative AI tools.