Minimising the Synthesised ENL-systems Aishah Ahmed1 , Marta Pietkiewicz-Koutny1,* 1 School of Computing, Newcastle University, Newcastle upon Tyne NE4 5TG, United Kingdom Abstract Elementary Net Systems with Localities (enl-systems) is a class of Petri nets introduced to model gals (globally asynchronous locally synchronous) systems, where some of the components might be considered as logically or physically close and acting synchronously, while others might be considered as loosely connected or residing at distant locations and communicating with the rest of the system in an asynchronous way. The specification of the behaviour of a gals system comes very often in the form of a transition system. The automated synthesis, based on regions, is an approach that allows to construct Petri net models from their transition system specifications. In our previous papers we developed algorithms and tool support for the synthesis of enl-systems from step transition systems, where arcs are labelled by steps (sets) of executed actions. In this paper we focus on the minimisation of the synthesised nets. In particular, we discuss the properties of minimal, companion, and complementary regions, and their role in the process of minimisation of enl-systems. Furthermore, we propose a strategy to eliminate redundant regions. Our theoretical results are backed by experiments (the algorithms for the minimisation are implemented within the workcraft framework). Keywords theory of concurrency, Petri nets, localities, analysis and synthesis, step sequence semantics, theory of regions, transition systems, WORKCRAFT framework 1. Introduction A number of computational systems exhibit behaviour that follows the ‘globally asynchronous locally (maximally) synchronous’ paradigm. Examples can be found in hardware design, where a vlsi chip may contain multiple clocks responsible for synchronising different subsets of gates [1], and in biologically inspired membrane systems representing cells within which biochemical reactions happen in synchronised pulses [2]. To formalise such systems, [3] introduced Place/Transition-nets with localities (ptl-nets), where each locality defines a distinct set of events which must be executed synchronously, i.e., in a maximally concurrent manner (often called local maximal concurrency). An attractive way of constructing complex computing systems is their automated synthesis from behavioural specifications given in terms of suitable transition systems. In such a case, the synthesis procedure is often based on the regions of a transition system, a notion introduced in [4], and later used to solve the synthesis problem for different classes of Petri nets [5, 6, 7, 8, 9, 10]. A comprehensive survey of the synthesis problem and region theory is presented in [11]. ATAED’22: Algorithms & Theories for the Analysis of Event Data, June 20–21, 2022, Bergen, Norway * Corresponding author. " a.ahmad@ncl.ac.uk (A. Ahmed); marta.koutny@ncl.ac.uk (M. Pietkiewicz-Koutny) © 2022 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) The vast majority of results in the area of synthesis of Petri nets use the standard transition systems, where the arcs are labelled with single events/actions, as initial specifications of systems’ behaviour. In this paper, however, we follow the approach, used in [12, 13, 14, 15, 10], employing step transition systems instead, where arcs are labelled with sets of executed events/actions. The nets with localities, as already mentioned, were first introduced in [3] using as a base a class of Place/Transition nets. The idea of actions’ localities was later adapted to Elementary Net Systems (en-systems) in [12], where a solution to the synthesis problem for enl-systems was presented. Further advances in the area of synthesising nets with localities from step transition systems are the subjects of [13, 14, 15]. The last of them, [15], concentrated on finding the rules for reducing the number of regions that are essential to synthesise enl-systems. In our previous papers, [16, 17], we developed algorithms and tool support for the synthesis of enl-systems from step transition systems. In this paper we continue the work started in [15] and focus on the minimisation of enl-systems. The nets obtained from the synthesis procedure, called saturated nets, contain many conditions that are redundant from their behaviour point of view. Removing such conditions is important to get more manageable and readable solutions to the synthesis problem. The approaches to remove redundant conditions from nets were investi- gated in the literature and implemented in several tools [18, 19]. Many synthesis procedures concentrate on returning smaller solutions based on so-called minimal regions [20, 21, 22, 23, 24]. In our approach, minimal regions, as defined for our class of step transition systems, are also important for building smaller solutions to the synthesis problem. Furthermore, in this pa- per, following [6], we are interested in the role of minimal regions in defining state-machine components of the synthesised and minimised enl-systems. Our theoretical results are backed by experiments (the algorithms for the minimisation are implemented within the workcraft framework [25, 26]). To explain the basic idea behind enl-systems, let us consider the net in Figure 1 modelling two co-located consumers and one producer residing in a remote location. In the initial state, the net can execute the singleton step {c4 }. Another enabled step is {p2 } which removes the token from b1 and puts two tokens, into b0 and b2 . In this new state, there are three enabled steps, viz. {p1 }, {c1 , c4 } and {p1 , c1 , c4 }. The last one, {p1 , c1 , c4 }, corresponds to what is usually called maximal concurrency as no more activities can be added to it without violating the constrains imposed by the available resources (represented by tokens). However, the previously enabled step {c4 } which is still resource (or token) enabled is disallowed by the control mechanism of enl-systems. It rejects a resource enabled step like {c4 } since we can add to it c1 co-located with c4 obtaining a step which is resource enabled. In other words, the control mechanism employed by enl-systems (and ptl-nets) is that of local maximal concurrency as indeed postulated by the gals systems execution rule. The paper is organised as follows. The next section recalls some basic notions concerning step transition systems as well as enl-systems and their synthesis. Section 3 recalls, from [15], three reduction rules that can be used to safely eliminate redundant regions/conditions from the synthesised nets. Section 4 defines minimal regions for the class of enlst-systems and Section 5 discusses the properties of different kinds of regions and their roles in the process of minimisation of enl-systems. Section 6 presents a strategy to eliminate redundant regions from the synthesised nets. The paper ends with a conclusion that includes some directions for future work. Proofs are omitted due to the page limit. b1 b3 c2 b5 b0 p1 p2 c1 c4 b2 b4 c3 b6 Figure 1: An enl-system modelling a system comprising one producer and two co-located consumers (the shading of boxes indicates the co-location of events they represent). 2. Preliminaries In this section, we recall suitably adapted notions and results from [12, 14, 15]. Throughout the paper, 𝐸 is a fixed finite nonempty set of events. A step is a nonempty set of events, and a co-location relation ≏ is any equivalence relation over 𝐸. For every event 𝑒 ∈ 𝐸, [𝑒]≏ is the equivalence class of ≏ to which 𝑒 belongs (i.e., the locality of 𝑒). For an event 𝑒 and a step 𝑈 , we denote 𝑒 ≏ 𝑈 whenever there is at least one event 𝑓 ∈ 𝑈 satisfying 𝑒 ≏ 𝑓 . Definition 1. A step transition system (or st-system) is a triple ts = (𝑄, 𝐴, 𝑞0 ), where 𝑄 is a nonempty finite set of states, 𝐴 ⊆ 𝑄 × (P(𝐸) ∖ {∅}) × 𝑄 is a set of transitions (arcs), and 𝑞0 ∈ 𝑄 is the initial state. ♢ In diagrams, st-systems are represented as labelled directed graphs, and singleton steps annotating transitions are denoted without brackets. To ease the presentation, we assume that each event of 𝐸 occurs in at least one of the steps labelling the transitions of ts. The set of all steps labelling transitions outgoing from 𝑞 will be denoted by allSteps 𝑞 . For a transition t = (𝑞, 𝑈, 𝑞 ′ ) ∈ 𝐴, we have therefore 𝑈 ∈ allSteps 𝑞 , and respectively call 𝑞 and 𝑞 ′ the source and target of t. Furthermore, t is thick if |𝑈 | ≥ 2. ts is called thin if, for every event 𝑒 ∈ 𝐸, there is (𝑞, {𝑒}, 𝑞 ′ ) ∈ 𝐴. A sequence of transitions (𝑞1 , 𝑈1 , 𝑞2 )(𝑞2 , 𝑈2 , 𝑞3 ) . . . (𝑞𝑘 , 𝑈𝑘 , 𝑞𝑘+1 ) is a path from 𝑞1 to 𝑞𝑘+1 . A state 𝑞 is reachable if there is a path from 𝑞0 to 𝑞. Two st-systems, ts = (𝑄, 𝐴, 𝑞0 ) and ts′ = (𝑄′ , 𝐴′ , 𝑞0′ ), are isomorphic if there is a bijection 𝑓 : 𝑄 → 𝑄′ such that 𝑓 (𝑞0 ) = 𝑞0′ and 𝐴′ = {(𝑓 (𝑞), 𝑈, 𝑓 (𝑞 ′ )) | (𝑞, 𝑈, 𝑞 ′ ) ∈ 𝐴}. We denote this by ts ∼= ts′ . Definition 2. An elementary net system with localities w.r.t. a co-location relation ≏ (or enl≏ - system) is a tuple enl = (𝐵, 𝐸, 𝐹, ≏, 𝑐0 ), where 𝐵 is a finite set of conditions such that 𝐵∩𝐸 = ∅, 𝐹 ⊆ (𝐵 × 𝐸) ∪ (𝐸 × 𝐵) is the flow relation, and 𝑐0 ⊆ 𝐵 is the initial case (in general, any 𝑐 ⊆ 𝐵 is a case). We will also say that enl is an elementary net system with localities (or enl-system) if mentioning ≏ is not important. ♢ In diagrams, conditions (local states) are represented by circles, events (actions) by boxes, the flow relation by directed arcs, and each case (global state) by tokens (small black dots) placed inside those conditions which belong to this case. Moreover, boxes representing co-located events are shaded in the same way (see Figure 1). For every event 𝑒, its pre-conditions and post-conditions are given respectively by ∙ 𝑒 = {𝑏 | (𝑏, 𝑒) ∈ 𝐹 } and 𝑒∙ = {𝑏 | (𝑒, 𝑏) ∈ 𝐹 }, and both sets are assumed to be nonempty and disjoint. The dot-notation extends to sets of events in the usual way, e.g., 𝑈 = { 𝑒 | 𝑒 ∈ 𝑈 }. Two ∙ ⋃︀ ∙ distinct events, 𝑒 and 𝑓 , are in conflict (or conflicting) if they share a pre-condition, or share a post-condition. Furthermore, we assume that there are no isolated conditions in enl. The semantics of enl is based on steps of simultaneously executed events, and can be under- stood as local maximal concurrency. We first define potential steps of enl as all nonempty sets of mutually non-conflicting events. A potential step 𝑈 is then resource enabled at a case 𝑐 if ∙ 𝑈 ⊆ 𝑐 and 𝑈 ∙ ∩ 𝑐 = ∅, and control enabled if, in addition, there is no event 𝑒 ∈ / 𝑈 such that 𝑒 ≏ 𝑈 and the step 𝑈 ∪ {𝑒} is resource enabled at 𝑐. We denote these respectively by 𝑈 ∈ resenabled (𝑐) and 𝑈 ∈ enabled (𝑐). A control enabled step 𝑈 ∈ enabled (𝑐) can be executed leading from 𝑐 to the case 𝑐′ = (𝑐 ∖ ∙ 𝑈 ) ∪ 𝑈 ∙ . We denote this by 𝑐[𝑈 ⟩𝑐′ . The set of reachable cases of enl, denoted reachenl , is the least set of cases containing 𝑐0 such that if 𝑐 ∈ reachenl and 𝑐[𝑈 ⟩𝑐′ , then 𝑐′ ∈ reachenl . The st-system generated by enl is tsenl = (reachenl , 𝐴, 𝑐0 ), where 𝐴 = {(𝑐, 𝑈, 𝑐′ ) | 𝑐 ∈ reachenl ∧ 𝑐[𝑈 ⟩𝑐′ }. enl is a net realisation of an st-system ts if tsenl ∼ = ts. To ease the presentation, we assume that enl does not have dead events, i.e., for each event 𝑒, there are 𝑐 ∈ reachenl and 𝑈 ∈ enabled (𝑐) such that 𝑒 ∈ 𝑈 . Definition 3. Let enl = (𝐵, 𝐸, 𝐹, ≏, 𝑐0 ) be an enl≏ -system. We say that enl is a state machine enl≏ -system iff: 1. ∀𝑒 ∈ 𝐸 : |∙ 𝑒| = 1 = |𝑒∙ |; 2. |𝑐0 | = 1. ♢ Definition 4. Let enl = (𝐵, 𝐸, 𝐹, ≏, 𝑐0 ) be an enl≏ -system. A subsystem of enl is an enl≏ - system enl′ = (𝐵 ′ , 𝐸 ′ , 𝐹 ′ , ≏′ , 𝑐′0 ) such that the following conditions hold: 1. 𝐵 ′ ⊆ 𝐵 and 𝐸 ′ ⊆ 𝐸; 2. ∀𝑏 ∈ 𝐵 ′ ∀𝑒 ∈ 𝐸 : ((𝑏, 𝑒) ∈ 𝐹 ∨ (𝑒, 𝑏) ∈ 𝐹 ) =⇒ 𝑒 ∈ 𝐸 ′ ; 3. 𝐹 ′ = 𝐹 ∩ ((𝐵 ′ × 𝐸 ′ ) ∪ (𝐸 ′ × 𝐵 ′ )); ≏′ = ≏ ∩ 𝐸 ′ × 𝐸 ′ and 𝑐′0 = 𝑐0 ∩ 𝐵 ′ . A subsystem enl′ is connected if the graph (𝐵 ′ ∪ 𝐸 ′ , 𝐹 ′ ) is connected. Also, point 2 above says that the subsystem enl′ is generated by the subset of conditions 𝐵 ′ of the enl≏ -system enl. ♢ Definition 5. Let enl = (𝐵, 𝐸, 𝐹, ≏, 𝑐0 ) be an enl≏ -system. We say that enl is a state ma- chine decomposable enl≏ -system iff there exists a set of connected subsystems of enl, enl𝑖 = (𝐵𝑖 , 𝐸𝑖 , 𝐹𝑖 , ≏𝑖 , 𝑐𝑖0 ) (𝑖 = 1, . . . , 𝑚), satisfying the following: 1. ∀𝑖 ∈ {1, . . . , 𝑚} : enl𝑖 is a state machine enl≏𝑖 -system; ⋃︀ ⋃︀ ⋃︀ 2. 𝐵 = 𝑖 𝐵𝑖 , 𝐸 = 𝑖 𝐸𝑖 and 𝐹 = 𝑖 𝐹𝑖 . The enl𝑖 are called state machine (or sequential) components of enl. ♢ The general synthesis problem we consider can be formulated thus: Problem 1. Given an st-system ts and a co-location relation ≏, find an effective way of checking whether there is an enl≏ -system which is a net realisation of ts. If the answer is positive construct such an enl≏ -system. ♢ The above problem can be approached by considering a link between the nodes (global states) of an st-system with the conditions (local states) of a hypothetical enl-system realising it, captured by the notion of regions with explicit input and output events. Definition 6. A region (with explicit input and output events) of an st-system ts = (𝑄, 𝐴, 𝑞0 ) is a triple r = (in, 𝑟, out) ∈ P(𝐸) × P(𝑄) × P(𝐸), such that in = 𝑜𝑢𝑡 = ∅ implies 𝑟 = 𝑄 or 𝑟 = ∅ and, for every transition (𝑞, 𝑈, 𝑞 ′ ) of ts, the following hold: r1 If 𝑞 ∈ 𝑟 and 𝑞 ′ ∈ / 𝑟 then |𝑈 ∩ out| = 1. / 𝑟 and 𝑞 ′ ∈ 𝑟 then |𝑈 ∩ in| = 1. r2 If 𝑞 ∈ r3 If 𝑈 ∩ out ̸= ∅ then 𝑞 ∈ 𝑟 and 𝑞 ′ ∈ / 𝑟. / 𝑟 and 𝑞 ′ ∈ 𝑟. r4 If 𝑈 ∩ in ̸= ∅ then 𝑞 ∈ ♢ In a region r = (in, 𝑟, out), the set in comprises events responsible for entering the set of states 𝑟, and out comprises events responsible for leaving 𝑟. Note that r̄ = (𝑜𝑢𝑡, 𝑄 ∖ 𝑟, 𝑖𝑛) is also a region (the complement of region r). In general, a region r cannot be identified only by its set of states 𝑟. However, if ts is thin, then its different regions are based on different sets of states. There are exactly two trivial regions satisfying 𝑟 = ∅ or 𝑟 = 𝑄, viz. (∅, ∅, ∅) and (∅, 𝑄, ∅). The set of all non-trivial regions of ts will be denoted by Rts and, for every state 𝑞, R𝑞 = {r ∈ Rts | 𝑞 ∈ 𝑟} is the set of all non-trivial regions (in, 𝑟, out) containing 𝑞. The sets of pre-regions and post-regions of an event 𝑒, ∘ 𝑒 and 𝑒∘ , comprise all the non-trivial regions (in, 𝑟, out) respectively satisfying 𝑒 ∈ out and 𝑒 ∈ in, viz. ∘ 𝑒 = {r ∈ Rts | 𝑒 ∈ out} and 𝑒∘⋃︀= {r ∈ Rts | 𝑒 ∈ in}. This extends in the usual way to sets of events, for example, ∘𝑈 = { ∘ 𝑒 | 𝑒 ∈ 𝑈 }. Also, we will write 𝑒 ∈ r∘ ⇐⇒ r ∈ ∘ 𝑒 and 𝑒 ∈ ∘ r ⇐⇒ r ∈ 𝑒∘ . The set of potential steps of ts comprises all nonempty sets 𝑈 of events such that ∘ 𝑒 ∩ ∘ 𝑓 = 𝑒 ∩ 𝑓 ∘ = ∅, for each pair of distinct events 𝑒, 𝑓 ∈ 𝑈 . A potential step 𝑈 is then region enabled ∘ at 𝑞 ∈ 𝑄 if ∘ 𝑈 ⊆ R𝑞 and 𝑈 ∘ ∩ R𝑞 = ∅. We denote this by 𝑈 ∈ regenabled (𝑞). Definition 7. An st-system ts is an enl step transition system w.r.t. a co-location relation ≏ (or enlst≏ -system) if the following hold: a1 Each state is reachable. a2 For every event 𝑒, both ∘ 𝑒 and 𝑒∘ are nonempty. a3 For all distinct states 𝑞 and 𝑞 ′ , R𝑞 ̸= R𝑞′ . a4 For every state 𝑞 and step 𝑈 , 𝑈 ∈ allSteps 𝑞 iff 𝑈 ∈ regenabled (𝑞) and there is no event 𝑒 ̸∈ 𝑈 such that 𝑒 ≏ 𝑈 and 𝑈 ∪ {𝑒} ∈ regenabled (𝑞). We also say that ts is an enlst-system (if mentioning ≏ is not important). ♢ One can show that the st-system generated by an enl≏ -system is an enlst≏ -system. The converse is also true, and a suitable translation is based on the regions of st-systems. Definition 8. Let ts be an enlst≏ -system. The tuple associated with ts is defined by enl≏ ts = (Rts , 𝐸, 𝐹ts , ≏, R𝑞0 ), where 𝑞0 is the initial state of ts and 𝐹ts = {(r, 𝑒) ∈ Rts × 𝐸 | r ∈ ∘ 𝑒} ∪ {(𝑒, r) ∈ 𝐸 × Rts | r ∈ 𝑒∘ }. ♢ The above construction always produces an enl≏ -system which generates an st-system isomorphic to ts (see [12]). Theorem 1. Let ts be an enlst≏ -system. Then enl≏ ∼ ts is an enl≏ -system such that ts = tsenl≏ts . Moreover, the unique isomorphism 𝜓 between ts and tsenl≏ is given by 𝜓(𝑞) = R𝑞 , for every state ts 𝑞 of ts. 3. Optimising solutions to the synthesis problem In this section we recall some notions and results from [15]. The enl-system enl≏ ts obtained from the synthesis of the enlst-system ts may contain many conditions which are redundant from the point of view of its behaviour, 𝑖.𝑒., deletion of such conditions (and their adjacent arcs) would lead to a net that generates the st-system, which is still isomorphic to ts. Suppose that we have reduced enl≏ ts in this way obtaining a sub-enl-system enl. We would like to reduce enl further by deleting a condition/region r (and its adjacent arcs) without, as before, violating the property of it being an enl-system 1 and making sure that the resultant net still generates the st-system isomorphic to ts. We denote the enl-system after such one step reduction: enlr . In [15], it was proved that complement regions are very often redundant: Reduction Rule 1. If r = (𝑖𝑛, 𝑟, 𝑜𝑢𝑡) and r̄ = (𝑜𝑢𝑡, 𝑄 ∖ 𝑟, 𝑖𝑛) are two conditions in enl and deleting r̄ leads to an enl-system, then the st-systems generated by enl and enlr̄ are isomorphic and r̄ is redundant. ♢ 1 Every enl-system enl = (𝐵, 𝐸, 𝐹, ≏, 𝑐0 ) should satisfy: ∀𝑒 ∈ 𝐸 (∙ 𝑒 ̸= ∅ ∧ 𝑒∙ ̸= ∅ ∧ ∙ 𝑒 ∩ 𝑒∙ = ∅). Another source of redundancy among conditions/regions in the synthesised net are “big" re- gions that are compositions of smaller regions. To define a composition operator, [15] introduces the concept of compatible regions. Definition 9. A region (𝑖𝑛, 𝑟, 𝑜𝑢𝑡) is compatible with another region (𝑖𝑛′ , 𝑟′ , 𝑜𝑢𝑡′ ) iff the follow- ing three conditions hold: 1. 𝑟 ∩ 𝑟′ = ∅. 2. For every 𝑒 ∈ 𝑜𝑢𝑡 exactly one of the following holds: • For all the transitions (𝑞, 𝑈, 𝑞 ′ ) such that 𝑒 ∈ 𝑈 we have 𝑞 ′ ∈ 𝑟′ . • For all the transitions (𝑞, 𝑈, 𝑞 ′ ) such that 𝑒 ∈ 𝑈 we have 𝑞 ′ ∈ / 𝑟′ . 3. For every 𝑒 ∈ 𝑖𝑛 exactly one of the following holds: • For all the transitions (𝑞, 𝑈, 𝑞 ′ ) such that 𝑒 ∈ 𝑈 we have 𝑞 ∈ 𝑟′ . • For all the transitions (𝑞, 𝑈, 𝑞 ′ ) such that 𝑒 ∈ 𝑈 we have 𝑞 ∈ / 𝑟′ . If region r is compatible with region r′ and region r′ is compatible with r we say that the two regions are compatible. ♢ In [15], it was proved that the composition of two compatible regions (defined below) is also a region. If r = (𝑖𝑛, 𝑟, 𝑜𝑢𝑡) and r′ = (𝑖𝑛′ , 𝑟′ , 𝑜𝑢𝑡′ ) are two non-trivial compatible regions of an enlst-system ts, then the following is a (possibly trivial) region of ts: df r ⊕ r′ = (𝑖𝑛 ∪ 𝑖𝑛′ ∖ 𝐻, 𝑟 ∪ 𝑟′ , 𝑜𝑢𝑡 ∪ 𝑜𝑢𝑡′ ∖ 𝐻), where 𝐻 is a set of events that belong only to steps labelling transitions hidden/buried in 𝑟 ∪ 𝑟′ (with its source in 𝑟 and its target in 𝑟′ or the other way round). The region r ⊕ r′ is called the composition of r and r′ . In [15], the following reduction rule was proved: Reduction Rule 2. If r = (𝑖𝑛, 𝑟, 𝑜𝑢𝑡), r′ = (𝑖𝑛′ , 𝑟′ , 𝑜𝑢𝑡′ ) and r ⊕ r′ are three conditions/regions in enl, then the st-systems generated by enl and enlr⊕r′ are isomorphic and r ⊕ r′ is redundant. ♢ The third reduction rule considers regions of ts = (𝑄, 𝐴, 𝑞0 ) based on the same set of states. We will call such regions companion regions. For a given set of states 𝑟, they will belong to the set denoted by R𝑟ts . In [15], it was proved that if the events contained in the set 𝑖𝑛 (𝑜𝑢𝑡) of a region r = (𝑖𝑛, 𝑟, 𝑜𝑢𝑡) can be found in the 𝑖𝑛 (𝑜𝑢𝑡) sets of other companion regions then r is redundant and can be deleted. Formally: Reduction Rule 3. Let r = (𝑖𝑛, 𝑟, 𝑜𝑢𝑡) be a condition/region of enl such that: ⋃︁ 𝑖𝑛 ⊆ {𝑖𝑛′ | (𝑖𝑛′ , 𝑟, 𝑜𝑢𝑡′ ) is condition in enl different from r} (1) ⋃︁ 𝑜𝑢𝑡 ⊆ {𝑜𝑢𝑡′ | (𝑖𝑛′ , 𝑟, 𝑜𝑢𝑡′ ) is condition in enl different from r} (2) Then the st-systems generated by enl and enlr are isomorphic and r is redundant. ♢ r1 r7 r2 r8 r1 r2 q0 {e, e1 }{e, e2 } e e1 e2 e e1 e2 q1 q2 r3 r5 r4 r6 r3 r5 r6 (𝑎) (𝑏) (𝑐) Figure 2: An enlst-system with three co-located events 𝑒, 𝑒1 and 𝑒2 (a); the enl-system resulting from its synthesis (b); and the reduced enl-system solution for (a) that uses only minimal regions (c). 4. Minimal regions For many classes of Petri nets, for which the synthesis problem was investigated, a region was defined as a subset of states of a transition system. For such classes of nets and their transition systems a minimal region was defined 𝑤.𝑟.𝑡. the set inclusion ⊂ [6, 7, 23, 27]. Also, composition of regions (as sets) was defined by using the set union operator (∪), which is both commutative and associative. The regions of enlst-systems are triples of the form: r = (𝑖𝑛, 𝑟, 𝑜𝑢𝑡). The minimal regions in this class of (step) transition systems are defined 𝑤.𝑟.𝑡. the strict pre-order ≺ on the set of regions, that utilises the idea of regions’ composition by means of ⊕: r ≺ r′ iff there is a non-trivial region r′′ such that r ⊕ r′′ = r′ [15]. Formally, we have the following definition of a minimal region: Definition 10. A region r ∈ Rts is minimal iff ∀ ̂︀r ∈ Rts : ̂︀r ̸≺ r. ♢ The set of minimal regions of ts w.r.t. ≺ will be denoted by R𝑚𝑖𝑛 ts . We observe that if a non-trivial region is non-minimal then it can be represented as a composition of two other non-trivial regions. This follows from the definition of the relation ≺ and the fact that the composition operator ⊕ is commutative, which, in turn, follows immediately from the definition of ⊕. As an example, consider the enlst-system in Figure 2(a). Its non-trivial regions are: r1 = (∅, {𝑞0 }, {𝑒}) r3 = r̄1 = ({𝑒}, {𝑞1 , 𝑞2 }, ∅) r2 = (∅, {𝑞0 }, {𝑒1 , 𝑒2 }) r4 = r̄2 = ({𝑒1 , 𝑒2 }, {𝑞1 , 𝑞2 }, ∅) r5 = ({𝑒1 }, {𝑞1 }, ∅) r7 = r̄5 = (∅, {𝑞0 , 𝑞2 }, {𝑒1 }) r6 = ({𝑒2 }, {𝑞2 }, ∅) r8 = r̄6 = (∅, {𝑞0 , 𝑞1 }, {𝑒2 }) The minimal regions of the enlst-system in Figure 2(a) are: r1 , r2 , r3 , r5 and r6 . The remaining regions are non-minimal (their set is denoted by R⊕ ts ): r4 = r5 ⊕ r6 (𝐻 = ∅); r7 = r2 ⊕ r6 (𝐻 = {𝑒2 }); r8 = r2 ⊕ r5 (𝐻 = {𝑒1 }). The reduced enl-system solution for the enlst-system in Figure 2(a) that uses only regions minimal 𝑤.𝑟.𝑡. ≺ is shown in Figure 2(c). Note that the operator ⊕ is not associative as can be shown by using, again, the example of the enlst-system in Figure 2(a). We can observe that: (r5 ⊕ r6 ) ⊕ r1 ̸= r5 ⊕ (r6 ⊕ r1 ). While r5 and r6 are compatible and their composition produces r4 (r4 = r5 ⊕ r6 ), regions r6 and r1 are not compatible, because r1 is not compatible with r6 , and they cannot be composed. Also notice that there might be two companion regions (regions based on the same set of states) such that one of them is a minimal region and the second one is a non-minimal region. See, for example, regions r3 = ({𝑒}, {𝑞1 , 𝑞2 }, ∅) and r4 = ({𝑒1 , 𝑒2 }, {𝑞1 , 𝑞2 }, ∅) of the enlst- system in Figure 2(a), where r3 is minimal and r4 is non-minimal. So, the minimality of a region cannot be decided by looking at its set of states only. The following result, about the representation of non-trivial regions, is similar to the results proved for other classes of nets (and their transition systems) that can be found in the literature: Elementary Net Systems [6], pure and bounded Place/Transition Nets [7], Safe Nets [23] or Elementary Net Systems with Inhibitor Arcs (ENI-systems) [27]. Theorem 2. Every r = (𝑖𝑛, 𝑟, 𝑜𝑢𝑡) ∈ Rts can be represented as a composition of minimal regions, where for each pair of different minimal regions in this representation, ̂︀r = (𝑖𝑛, ̂︀ 𝑟, ̂︀ 𝑜𝑢𝑡) ̂︁ and ̃︀r = (𝑖𝑛, ̃︀ 𝑟, ̃︁ 𝑟̂︀ ∩ 𝑟̃︀ = ∅. ̃︀ 𝑜𝑢𝑡), Theorem 2 and Reduction Rule 2 imply that one can construct a solution to the synthesis problem based on minimal regions 𝑤.𝑟.𝑡. the strict pre-order ≺. The consequence of the fact that the operator ⊕ is not associative, is that we cannot drop the brackets, when we represent a non-trivial region of an enlst-system as a composition of its minimal regions (for example, r = r1 ⊕ (r2 ⊕ . . . (r𝑛−2 ⊕ (r𝑛−1 ⊕ r𝑛 )) . . .), where r𝑖 (𝑖 = 1, . . . , 𝑛) are minimal regions in this representation of r). 5. Properties of regions In this section we gather facts regarding relationships of complementary, compatible, companion and minimal regions of an enlst-system ts = (𝑄, 𝐴, 𝑞0 ). Fact 1. Any pair of complementary regions of ts, r and r̄, form a pair of compatible regions and r ⊕ r̄ = (∅, 𝑄, ∅). ♢ From Fact 1 it follows that if ts has only minimal regions among non-trivial regions, then only the pairs of complementary regions can be composed resulting in a trivial region. Fact 2. Let r1 = (𝑖𝑛1 , 𝑟1 , 𝑜𝑢𝑡1 ) and r2 = (𝑖𝑛2 , 𝑟2 , 𝑜𝑢𝑡2 ) be two non-trivial compatible regions of an enlst-system ts. Then 𝑖𝑛1 ∩ 𝑖𝑛2 = ∅ and 𝑜𝑢𝑡1 ∩ 𝑜𝑢𝑡2 = ∅. Now, we introduce a notion of strong compatibility of regions. Definition 11. A region (𝑖𝑛, 𝑟, 𝑜𝑢𝑡) is strongly compatible with another region (𝑖𝑛′ , 𝑟′ , 𝑜𝑢𝑡′ ) iff the following three conditions hold: 1. 𝑟 ∩ 𝑟′ = ∅. 2. For every 𝑒 ∈ 𝑜𝑢𝑡 exactly one of the following holds: • 𝑒 ∈ in′ . • For all the transitions (𝑞, 𝑈, 𝑞 ′ ) such that 𝑒 ∈ 𝑈 we have 𝑞 ′ ∈ / 𝑟′ . 3. For every 𝑒 ∈ 𝑖𝑛 exactly one of the following holds: • 𝑒 ∈ out′ . • For all the transitions (𝑞, 𝑈, 𝑞 ′ ) such that 𝑒 ∈ 𝑈 we have 𝑞 ∈ / 𝑟′ . If region r is strongly compatible with region r′ and region r′ is strongly compatible with r we say that the two regions are strongly compatible. ♢ Fact 3. Two regions, which are strongly compatible are compatible. The composition operator defined for the strongly compatible regions (rather than compatible regions) will be denoted by ⊕𝑠 . The strict pre-order relation for the set of regions that utilises operator ⊕𝑠 instead of ⊕ will be denoted by ≺𝑠 . The set of minimal regions of ts w.r.t. ≺𝑠 will be denoted by R𝑚𝑖𝑛,𝑠 ts . The implication of Fact 3 is that Reduction Rule 2 works with strongly compatible regions (we can replace operator ⊕ by ⊕𝑠 in that rule). Also, we can strengthen Fact 1 to: Fact 4. Any pair of complementary regions of ts, r and r̄, form a pair of strongly compatible regions and r ⊕𝑠 r̄ = (∅, 𝑄, ∅). ♢ We will give examples of compatible and strongly compatible pairs of regions using the enlst-system in Figure 2(a). The pairs of regions {r1 , r4 } and {r2 , r3 } are compatible, but not strongly compatible. However, the pairs {r1 , r3 }, {r2 , r4 }, {r2 , r5 }, {r2 , r6 }, {r5 , r6 }, {r5 , r7 } and {r6 , r8 } are strongly compatible pairs of regions. Observe also that the pairs {r1 , r5 } and {r1 , r6 } are not compatible, because r1 is not compatible with neither r5 nor r6 . The next proposition shows that unlike ⊕ operator, ⊕𝑠 is associative. Proposition 1. The operator ⊕𝑠 is associative. Proposition 2. Let r1 = (𝑖𝑛1 , 𝑟1 , 𝑜𝑢𝑡1 ) and r2 = (𝑖𝑛2 , 𝑟2 , 𝑜𝑢𝑡2 ) be compatible regions of an st-system ts = (𝑄, 𝐴, 𝑞0 ), which do not satisfy the conditions to be strongly compatible regions of ts. Then there exists a companion region of r1 , r′1 ∈ R𝑟ts1 , and a companion region of r2 , r′2 ∈ R𝑟ts2 , such that r1 and r′2 are strongly compatible and r′1 and r2 are strongly compatible. Furthermore, r1 ⊕𝑠 r′2 = r′1 ⊕𝑠 r2 = r1 ⊕ r2 . To illustrate the result of Proposition 2, we can use again the enlst-system in Figure 2(a). A pair of its regions, r4 and r1 , are compatible, but not strongly compatible regions. However, there are regions r3 ∈ R𝑟ts4 and r2 ∈ R𝑟ts1 , such that r4 and r2 are strongly compatible and r3 and r1 are strongly compatible. Also, we have r4 ⊕𝑠 r2 = r3 ⊕𝑠 r1 = r4 ⊕ r1 = (∅, 𝑄, ∅). Corollary 1. Let ts = (𝑄, 𝐴, 𝑞0 ) be an enlst-system. Then 1. R𝑚𝑖𝑛 ts = R𝑚𝑖𝑛,𝑠 ts . 2. Every r ∈ Rts can be represented as a composition of minimal regions, where each pair of different minimal regions in this representation, r = (𝑖𝑛, 𝑟, 𝑜𝑢𝑡) and r′ = (𝑖𝑛′ , 𝑟′ , 𝑜𝑢𝑡′ ), is a pair of strongly compatible regions. The next result, about special families of non-trivial regions of ts, is inspired by a result proved for the class of Elementary Net Systems in [6]. We have adapted this result here to the context of enl-systems by changing one of the original conditions that a family of regions should satisfy, but the implied result is the same: a family of regions that satisfy the conditions of Theorem 3, treated as a set of conditions of the synthesised net, would generate a state machine component of this net. Points 2 and 3 of the consequent of Theorem 3 guarantee the satisfaction of Definition 3(1) and the point 1 of the consequent of Theorem 3 guarantees the satisfaction of Definition 3(2). Theorem 3. Let R = {r1 , r2 , . . . , r𝑛 } be a family of non-trivial regions of ts = (𝑄, 𝐴, 𝑞0 ), where r𝑖 = (𝑖𝑛𝑖 , 𝑟𝑖 , 𝑜𝑢𝑡𝑖 ), 𝑖 ∈ {1, . . . , 𝑛}, satisfy the following: 1. Every two different regions r𝑖 , r𝑗 ∈ R are strongly compatible regions. 2. ∀ ̂︀r = (𝑖𝑛, ̂︀ 𝑟, ̂︁ ∈ Rts : ̂︀r ̸∈ R =⇒ (∃r𝑖 ∈ R : 𝑟̂︀ ∩ 𝑟𝑖 ̸= ∅). ̂︀ 𝑜𝑢𝑡) Then: ⋃︀ 1. 𝑟𝑖 = 𝑄; 2. ∀𝑒 ∈ 𝐸 : | ∘ 𝑒 ∩ R| ≤ 1 and |𝑒∘ ∩ R| ≤ 1; 3. ∀𝑒 ∈ 𝐸 : 𝑒 ∈ ∘ r𝑖 ⇐⇒ ∃𝑗 : 𝑒 ∈ r𝑗 ∘ . The saturated enl-system that is a solution to Problem 1 for a given enlst-system ts, enl = ts , and is based on all non-trivial regions, is state machine decomposable (see Definition 5), enl≏ as due to Fact 4 every pair of complementary regions satisfies the conditions of Theorem 3 and would form a state machine component of enl. Furthermore, from Corollary 1 it follows that, similarly as for the class of Elementary Net Systems (see [6]), the enl-system obtained from enl by deleting all non-minimal regions following Reduction Rule 2 is also state machine decomposable as every region can be represented as a composition of minimal regions (w.r.t. ≺𝑠 ) and selected subsets of R𝑚𝑖𝑛 ts = R𝑚𝑖𝑛,𝑠 ts would satisfy the conditions of Theorem 3. As an example we can take the saturated enl-system synthesised from the enlst-system in Figure 2(a), shown in Figure 2(b), and its minimised version shown in Figure 2(c). The state machine components of the former enl-system are generated by the following subsets of conditions/regions: r1 ⊕𝑠 r3 = r2 ⊕𝑠 r5 ⊕𝑠 r6 = r2 ⊕𝑠 r4 = r7 ⊕𝑠 r5 = r8 ⊕𝑠 r6 = (∅, 𝑄, ∅). The minimised enl-system in Figure 2(c) has the first two state machine components from the components listed above. 6. A strategy to eliminate redundant regions The three reduction rules give conditions for deleting one of the redundant regions at a time. Therefore, we need a strategy to delete as many redundant regions as possible to obtain a net, where all (or almost all) remaining regions are needed (essential). The regions are redundant or essential only in the context of other regions. Different strategies lead to different sets of essential (or nearly essential) regions. Such sets of regions were called in [28] admissible. As an example we can take again the enlst-system in Figure 2(a). We observe that region r4 = r̄2 can be deleted according to Reduction Rule 1 (as the complement of region r2 ) or according to Reduction Rule 2 (as a non-minimal region: r4 = r5 ⊕ r6 ). When looking for a strategy for deleting redundant regions, we will take into consideration the following criteria: • Limiting as much as possible the non-determinism in the process of computing admissible regions. • Effectiveness of the strategy gauged in terms of the number of the removed regions. • Efficiency of the strategy gauged in terms of time needed to compute a set of admissible regions. Our first attempt at formulating a strategy will be based on the first criterion listed above. Reduction Rule 2 showed that all non-minimal regions are redundant 2 , so we can eliminate first the non-minimal regions. After this step, for a given enlst-system ts, we obtain from the unique set of regions, Rts , the unique set of minimal regions: R𝑚𝑖𝑛 ts . The application of Reduction Rule 1 and Reduction Rule 3 might not lead to a unique resultant set of regions. We might decide to keep certain companion regions and delete other companion regions in case of Reduction Rule 3. Similarly, we can keep both or one (random one) out of two complementary regions. As, in general, the Reduction Rule 3, leads to fewer possible choices of regions to delete, and might be even irrelevant in the case of thin step transition systems, where there are no companion regions, we might decide that this rule should be applied before the Reduction Rule 1, which can lead to many possible combinations of regions to keep/delete. This strategy, called Strategy (2,3,1), can be defined as follows: 1. Use Reduction Rule 2 to delete all non-minimal regions. 2. Use Reduction Rule 3 to delete any redundant companion regions that might be present among the minimal regions. 3. Use Reduction Rule 1 to delete any redundant complementary regions that might be present after the first two steps of the strategy. To check how good this strategy is from the second criterion point of view we consider a set of enlst-systems generated by nets composed of several sequential subsystems, where all the events are co-located. Such systems have a lot of companion regions. We will call them ts𝑐𝑜−𝑙𝑜𝑐 𝑖,𝑗 , where the index 𝑖 denotes the number of sequential subsystems, and the index 𝑗 denotes the 2 Reduction Rule 2 uses operator ⊕ and it was proved in [15] for this operator, but from Corollary 1(1) we have R𝑚𝑖𝑛 ts = R𝑚𝑖𝑛,𝑠 ts , so it does not matter whether we use ≺ and ⊕, or ≺𝑠 and ⊕𝑠 , to define the set of minimal regions. q0 e f {e, f } q1 {g, h} g h q2 (𝑎) (𝑏) Figure 3: An enlst-system ts𝑐𝑜−𝑙𝑜𝑐 2,2 with co-located events 𝑒, 𝑓 , 𝑔 and ℎ (a), and one of the possible enl-systems generating it (b). Table 1 Comparison between the effectiveness of Strategy (3,2,1) and Strategy (2,3,1), where x - y - z in the last two columns reports the number of remaining regions after the first (x), the second (y) and the third (z) stage of the strategies. ts |Q| |E| |Rts | Strategy (3,2,1) Strategy (2,3,1) ts𝑐𝑜−𝑙𝑜𝑐 2,2 3 4 16 12 - 6 - 6 8-6-6 ts𝑐𝑜−𝑙𝑜𝑐 2,3 4 6 52 28 - 10 - 10 12 - 8 - 8 ts𝑐𝑜−𝑙𝑜𝑐 2,4 5 8 160 60 - 12 - 12 16 - 10 - 10 ts𝑐𝑜−𝑙𝑜𝑐 2,5 6 10 484 124 - 26 - 26 20 - 12 - 12 ts𝑐𝑜−𝑙𝑜𝑐 3,2 3 6 30 22 - 11 - 11 15 - 11 - 11 ts𝑐𝑜−𝑙𝑜𝑐 3,3 4 9 126 66 - 20 - 20 24 - 16 - 16 ts𝑐𝑜−𝑙𝑜𝑐 3,4 5 12 510 190 - 52 - 51 33 - 21 - 21 ts𝑐𝑜−𝑙𝑜𝑐 3,5 6 15 2046 546 - 147 - 143 42 - 26 - 26 ts𝑐𝑜−𝑙𝑜𝑐 4,2 3 8 48 36 - 18 - 18 24 - 18 - 18 ts𝑐𝑜−𝑙𝑜𝑐 4,3 4 12 248 140 - 48 - 47 40 - 28 - 28 ts𝑐𝑜−𝑙𝑜𝑐 4,4 5 16 1248 540 - 165 - 159 56 - 38 - 38 ts𝑐𝑜−𝑙𝑜𝑐 4,5 6 20 6248 2108 - 532 - 508 72 - 48 - 48 number of events in each of the line-like sequential subsystem. As an example of such a step transition system we can see an enlst-system ts𝑐𝑜−𝑙𝑜𝑐2,2 in Figure 3(a). Using the set of step transition systems ts𝑖,𝑗𝑐𝑜−𝑙𝑜𝑐 (𝑖 = 2, . . . , 4; 𝑗 = 2, . . . , 5), we compare the effectiveness of region removal of Strategy (2,3,1) and Strategy (3,2,1) (Strategy (2,3,1) with the first two steps reversed). The result of this comparison is presented in Table 1. The results in Table 1 are not so surprising. The removal of non-minimal regions makes only sense in the context of all non-trivial regions (as the first step of the strategy). When removing companion regions, the algorithm processes groups of companion regions (each based on a shared set of states) separately from each other. From each group some subset of regions may be removed, at random, according to Reduction Rule 3. Once some of the minimal companion regions are removed (if we remove companion regions first), some of the regions that were previously non-minimal would become minimal as it won’t be possible to represent them as compositions of minimal regions using the remaining minimal regions. Therefore, they won’t be deleted by the Reduction Rule 2, if it is applied after Reduction Rule 3. The results in Table 1 show how great would be the loss of effectiveness if we used Strategy (3,2,1) for enlst-systems with a big number of companion regions. While the Reduction Rule 2, applied first in our strategy, can be considered as a method for eliminating non-minimal regions, non-minimal from the ‘state information’ point of view, the Reduction Rule 3 can be understood as a method for eliminating regions that are redundant from the ‘event information’ point of view. However, some subsets of companion regions will remain after the application of Reduction Rule 3, because they are essential as shown below: Fact 5. Let r = (𝑖𝑛, 𝑟, 𝑜𝑢𝑡) be a non-trivial region of ts = (𝑄, 𝐴, 𝑞0 ) and let R𝑟 ⊆ R𝑟ts be a set of its companion regions (including r) that were left after the application of the Reduction Rule 3 and let |R𝑟 | ≥ 2. Then all the regions of R𝑟 do not satisfy the same conditions of the Reduction Rule 3 (all do not satisfy condition (1) or all do not satisfy condition (2) or all do not satisfy both conditions: (1) and (2)). Corollary 2. Let R𝑟 = {r1 , r2 , . . . , r𝑛 } ⊆ R𝑟ts be a set of companion regions based on 𝑟 that were left after the application of the Reduction Rule 3. Then, for every region r𝑖 = (𝑖𝑛𝑖 , 𝑟, 𝑜𝑢𝑡𝑖 ) of R𝑟 that does not satisfy condition (1) (respectively (2)) of Reduction Rule 3 there exists a unique 𝐸𝑖 ⊆ 𝑖𝑛𝑖 (respectively 𝐸𝑖′ ⊆ 𝑜𝑢𝑡𝑖 ) with events that are not present in the 𝑖𝑛 (respectively 𝑜𝑢𝑡) sets of other regions from R𝑟 . So, companion regions of R𝑟 are ‘indexed’ by the unique subsets of events of their 𝑖𝑛 (respectively 𝑜𝑢𝑡) sets. We will call these subsets of events in-indices (respectively out-indices) of 𝑟 for the regions of R𝑟 . ♢ Notice that sets R𝑟 in Corollary 2 (and in Fact 5) might be equal to R𝑟ts . For example, for ts in {𝑞 } Figure 2(a), we have R{𝑞0 } = Rts 0 = {r1 , r2 }. Also, the indexing sets of events do not need to be singleton sets (as, for example, set {𝑒1 , 𝑒2 } for {𝑞0 } of r2 of ts in Figure 2(a)). We will further illustrate the above results using the enlst-system in Figure 3(a). Its non- trivial regions are listed below: r1 = (∅, {𝑞0 }, {𝑒}) r̄1 = ({𝑒}, {𝑞1 , 𝑞2 }, ∅) r2 = ({𝑒}, {𝑞1 }, {𝑔}) r̄2 = ({𝑔}, {𝑞0 , 𝑞2 }, {𝑒}) r3 = ({𝑔}, {𝑞2 }, ∅) r̄3 = (∅, {𝑞0 , 𝑞1 }, {𝑔}) r4 = ({𝑒}, {𝑞1 }, {ℎ}) r̄4 = ({ℎ}, {𝑞0 , 𝑞2 }, {𝑒}) r5 = ({ℎ}, {𝑞2 }, ∅) r̄5 = (∅, {𝑞0 , 𝑞1 }, {ℎ}) r6 = (∅, {𝑞0 }, {𝑓 }) r̄6 = ({𝑓 }, {𝑞1 , 𝑞2 }, ∅) r7 = ({𝑓 }, {𝑞1 }, {𝑔}) r̄7 = ({𝑔}, {𝑞0 , 𝑞2 }, {𝑓 }) r8 = ({𝑓 }, {𝑞1 }, {ℎ}) r̄8 = ({ℎ}, {𝑞0 , 𝑞2 }, {𝑓 }) The implemented tool, after applying Reduction Rule 2, will delete 8 out of 16 regions, leaving the minimal regions (r1 - r8 ). The set of minimal regions will be the same whether they are defined w.r.t. ≺ or ≺𝑠 strict pre-order (see Corollary 1(1)) as every non-minimal region that can be expressed as a composition of compatible regions can be also expressed as a composition of strongly compatible regions (see Proposition 2). For example, r̄3 = r1 ⊕𝑠 r2 = r1 ⊕ r7 , where the first two regions are strongly compatible, but the second two regions are only compatible, but not strongly compatible. The algorithm that implements Reduction Rule 3, when applied to this example, would delete two out of four regions based on the set of states {𝑞1 } leaving either r2 and r8 or r4 and r7 . The remaining pairs of companion regions, based on sets of states {𝑞0 },{𝑞1 } and {𝑞2 }, will remain as they are essential (having different in-indices or/and out-indices for the shared sets of states; see Corollary 2). The Reduction Rule 1, the last to be used in Strategy (2,3,1), is not applicable to this example as all the complementary regions of r1 - r8 were already deleted as non-minimal regions (see the results for ts𝑐𝑜−𝑙𝑜𝑐 2,2 in Table 1). 7. Conclusions In this paper we discussed the minimisation of the synthesised enl-systems and the strategy to eliminate redundant regions that involves three reduction rules. Also, we investigated the properties of minimal regions that play a crucial role in the minimisation process. We showed that synthesised and minimised nets that are based on all minimal regions (after the application of the Reduction Rule 2) do not lose the property of the saturated enl-systems of being state machine decomposable. We believe 3 that after the application of the Reduction Rule 3 this property still holds for the resultant net. However, after applying Reduction Rule 1, some synthesised enl-systems are no longer decomposable. As an example, we can take the enlst- system generated by the enl-system in Figure 1. The synthesis procedure for this example will produce a saturated net that has only minimal regions (12 regions). Some of them are redundant and can be deleted according to Reduction Rule 1. Figure 1 shows one of the possible minimised versions of this net that is not state machine decomposable. In the future work, we plan to investigate the relationship between the split of enl-systems into state machine components (based on conditions) and the split into localities (based on events). Also, we want to develop an improved algorithm implementing Reduction Rule 1, which would allow to target certain regions for deletion from the pairs of complementary regions. Acknowledgement We are grateful to the anonymous reviewers for their constructive comments, which have helped us to improve the presentation of the paper and to clarify our ideas. The first author is grateful to the National Transitional Council of Libya for funding her PhD studentship and research. References [1] S. Dasgupta, D. Potop-Butucaru, B. Caillaud, A. Yakovlev, Moving from weakly en- dochronous systems to delay-insensitive circuits, Electronic Notes in Theoretical Com- pututer Science 146 (2006) 81–103. 3 This still needs to be formally proved. [2] G. Păun, Membrane Computing: An Introduction, Natural Computing Series, Springer, 2002. [3] J. Kleijn, M. Koutny, G. Rozenberg, Towards a Petri net semantics for membrane systems, in: R. Freund, G. Paun, G. Rozenberg, A. Salomaa (Eds.), Membrane Computing, 6th International Workshop, WMC 2005, Vienna, Austria, July 18-21, 2005, Revised Selected and Invited Papers, volume 3850 of Lecture Notes in Computer Science, Springer, 2005, pp. 292–309. [4] A. Ehrenfeucht, G. Rozenberg, Partial (set) 2-structures. Part I: Basic notions and the representation problem. Part II: State spaces of concurrent systems, Acta Informatica 27 (1990) 315–368. [5] É. Badouel, P. Darondeau, Theory of regions, in: W. Reisig, G. Rozenberg (Eds.), Lectures on Petri Nets I: Basic Models, Advances in Petri Nets, volume 1491 of Lecture Notes in Computer Science, Springer, 1996, pp. 529–586. [6] L. Bernardinello, Synthesis of net systems, in: M. A. Marsan (Ed.), Application and Theory of Petri Nets 1993, 14th International Conference, Chicago, Illinois, USA, June 21-25, 1993. Proceedings, volume 691 of Lecture Notes in Computer Science, Springer, 1993, pp. 89–105. [7] 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. [8] M. Mukund, Petri nets and step transition systems, International Journal of Foundations of Computer Science 3 (1992) 443–478. [9] M. Nielsen, G. Rozenberg, P. S. Thiagarajan, Elementary transition systems, Theoretical Computer Science 96 (1992) 3–33. [10] M. Pietkiewicz-Koutny, The synthesis problem for elementary net systems with inhibitor arcs, Fundamenta Informaticae 40 (1999) 251–283. [11] É. Badouel, L. Bernardinello, P. Darondeau, Petri Net Synthesis, Texts in Theoretical Computer Science. An EATCS Series, Springer, 2015. [12] M. Koutny, M. Pietkiewicz-Koutny, Transition systems of elementary net systems with localities, in: C. Baier, H. Hermanns (Eds.), Concurrency Theory 2006, 17th International Conference, CONCUR 2006, Bonn, Germany, August 27-30, 2006. Proceedings, volume 4137 of Lecture Notes in Computer Science, Springer, 2006, pp. 173–187. [13] M. Koutny, M. Pietkiewicz-Koutny, Synthesis of elementary net systems with context arcs and localities, Fundamenta Informaticae 88 (2008) 307–328. [14] M. Koutny, M. Pietkiewicz-Koutny, Synthesis of Petri nets with localities, Scientific Annals of Computer Science 19 (2009) 1–23. [15] M. Koutny, M. Pietkiewicz-Koutny, Minimal regions of ENL-transition systems, Funda- menta Informaticae 101 (2010) 45–58. [16] A. Ahmed, M. Pietkiewicz-Koutny, Algorithms for the synthesis of elementary net systems with localities, in: M. Köhler-Bußmeier, E. Kindler, H. Rölke (Eds.), Proceedings of the International Workshop on Petri Nets and Software Engineering, PNSE 2020, Paris, France, June 24, 2020 (due to COVID-19: virtual workshop), volume 2651 of CEUR Workshop Proceedings, CEUR-WS.org, 2020, pp. 86–107. [17] A. Ahmed, M. Koutny, M. Pietkiewicz-Koutny, Synthesising elementary net systems with localities, Theoretical Computer Science 908 (2022) 123–140. [18] W. M. P. van der Aalst, B. F. van Dongen, C. W. Günther, A. Rozinat, E. Verbeek, T. Weijters, Prom: The process mining toolkit, in: A. K. A. de Medeiros, B. Weber (Eds.), Proceedings of the Business Process Management Demonstration Track (BPMDemos 2009), Ulm, Germany, September 8, 2009, volume 489 of CEUR Workshop Proceedings, CEUR-WS.org, 2009. [19] R. Bergenthum, J. Desel, R. Lorenz, S. Mauser, Synthesis of Petri nets from scenarios with viptool, in: K. M. van Hee, R. Valk (Eds.), Applications and Theory of Petri Nets, 29th International Conference, PETRI NETS 2008, Xi’an, China, June 23-27, 2008. Proceedings, volume 5062 of Lecture Notes in Computer Science, Springer, 2008, pp. 388–398. [20] R. Bergenthum, Prime miner - process discovery using prime event structures, in: Inter- national Conference on Process Mining, ICPM 2019, Aachen, Germany, June 24-26, 2019, IEEE, 2019, pp. 41–48. [21] J. Carmona, J. Cortadella, M. Kishinevsky, Genet: A tool for the synthesis and mining of Petri nets, in: Application of Concurrency to System Design 2009, 9th International Conference, ACSD 2009, Augsburg, Germany, 1-3 July 2009, IEEE Computer Society, 2009, pp. 181–185. [22] J. Cortadella, M. Kishinevsky, A. Kondratyev, L. Lavagno, A. Yakovlev, Petrify: A tool for manipulating concurrent specifications and synthesis of asynchronous controllers, IEICE Transactions on Information and Systems E80-D (1997) 315–325. [23] J. Cortadella, M. Kishinevsky, A. Kondratyev, L. Lavagno, A. Yakovlev, Logic Synthesis of Asynchronous Controllers and Interfaces, Springer Berlin Heidelberg, 2002. [24] L. L. Mannel, R. Bergenthum, W. M. P. van der Aalst, Removing implicit places using regions for process discovery, in: W. M. P. van der Aalst, R. Bergenthum, J. Carmona (Eds.), Proceedings of the International Workshop on Algorithms & Theories for the Analysis of Event Data 2020, ATAED 2020, Paris, France, June 24, 2020 (due to COVID-19: virtual workshop), volume 2625 of CEUR Workshop Proceedings, CEUR-WS.org, 2020, pp. 20–32. [25] I. Poliakov, V. Khomenko, A. Yakovlev, Workcraft - A framework for interpreted graph models, in: G. Franceschinis, K. Wolf (Eds.), Applications and Theory of Petri Nets, 30th International Conference, PETRI NETS 2009, Paris, France, June 22-26, 2009. Proceedings, volume 5606 of Lecture Notes in Computer Science, Springer, 2009, pp. 333–342. [26] Workcraft, https://workcraft.org/, 2018. [27] M. Pietkiewicz-Koutny, Synthesis of ENI-systems using minimal regions, in: D. Sangiorgi, R. de Simone (Eds.), Concurrency Theory 1998, 9th International Conference, CONCUR 1998: Nice, France, September 8-11, 1998. Proceedings, volume 1466 of Lecture Notes in Computer Science, Springer, 1998, pp. 565–580. [28] J. Desel, W. Reisig, The synthesis problem of Petri nets, Acta Informatica 33 (1996) 297–315.