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).
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 diferent subsets of
gates [
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 [
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 [
The nets with localities, as already mentioned, were first introduced in [
In our previous papers, [
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 [
p1 p2 b1 b2 b0
In this section, we recall suitably adapted notions and results from [
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).
≏ is not important. ♢
In diagrams, conditions (local states) are represented by circles, events (actions) by boxes, the lfow 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 understood 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 ∈ .
Let enl = (, , , ≏, 0) be an enl≏-system. We say that enl is a state machine
enl≏-system if: 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 machine decomposable enl≏-system if 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:
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. r2 If ∈/ and ′ ∈ then | ∩ in| = 1. r3 If ∩ out ̸= ∅ then ∈ and ′ ∈/ . r4 If ∩ in ̸= ∅ then ∈/ and ′ ∈ .
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 diferent regions are based on diferent 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 if ∈ regenabled () and there is no event ̸∈ such that ≏ and ∪ {} ∈ regenabled ().
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 enlt≏s = (Rts, , ts, ≏, R0 ), 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 [
Theorem 1. Let ts be an enlst≏-system. Then enlt≏s is an enl≏-system such that ts ∼= tsenlt≏s . Moreover, the unique isomorphism between ts and tsenlt≏s is given by () = R, for every state of ts.
In this section we recall some notions and results from [
The enl-system enlt≏s 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 enlt≏s 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 [
Another source of redundancy among conditions/regions in the synthesised net are “big"
regions that are compositions of smaller regions. To define a composition operator, [
Definition 9. A region (, , ) is compatible with another region (′, ′, ′) if the following three conditions hold: 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 ∈/ ′.
♢
In [
r ⊕ r′ =df ( ∪ ′ ∖ , ∪ ′, ∪ ′ ∖ ),
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 [
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 Rts.
In [
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 ⊂ [
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′ if there is a non-trivial region r′′ such that r ⊕ r′′ = r′ [
Formally, we have the following definition of a minimal region:
A region r ∈ Rts is minimal if ∀ ̂r︀ ∈ Rts : ̂r︀ ̸≺ r.
The set of minimal regions of ts w.r.t. ≺ will be denoted by Rts.
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 r2 r5 r6 = (∅, {0}, {}) = (∅, {0}, {1, 2}) = ({1}, {1}, ∅) = ({2}, {2}, ∅) r3 r4 r7 r8 = ¯r1 = ({}, {1, 2}, ∅) = ¯r2 = ({1, 2}, {1, 2}, ∅) = ¯r5 = (∅, {0, 2}, {1}) = ¯r6 = (∅, {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 enlstsystem 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 [
Theorem 2. Every r = (, , ) ∈ Rts can be represented as a composition of minimal regions, where for each pair of diferent 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).
In this section we gather facts regarding relationships of complementary, compatible, companion and minimal regions of an enlst-system ts = (, , 0).
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 (′, ′, ′) if the following three conditions hold: 1. ∩ ′ = ∅. • ∈ 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 ∈/ ′.
♢
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 Rts,.
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:
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 ∈ Rts1 , and a companion region of r2, r′2 ∈ Rts2 , 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 ∈ Rts4 and r2 ∈ Rts1 , 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. Rts = Rts,. 2. Every r ∈ Rts can be represented as a composition of minimal regions, where each pair of diferent 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 [
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 diferent regions r, r ∈ R are strongly compatible regions. 2. ∀ ̂r︀ = (, , ̂︁) ∈ Rts : ̂r︀ ̸∈ R =⇒ (∃r ∈ R : ̂︀ ∩ ̸= ∅).
̂︀ ̂︀
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 =
enlt≏s, and is based on all non-trivial regions, is state machine decomposable (see Definition 5),
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 [
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.
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. Diferent strategies lead to diferent sets of
essential (or nearly essential) regions. Such sets of regions were called in [
As an example we can take again the enlst-system in Figure 2(a). We observe that region r4 = ¯r2 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. • Efectiveness of the strategy gauged in terms of the number of the removed regions. • Eficiency 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 ifrst 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: Rts. 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
2Reduction Rule 2 uses operator ⊕ and it was proved in [
() ts ts2,2− ts2,3− ts2,4− ts2,5− ts3,2− ts3,3− ts3,4− ts3,5− ts4,2− ts4,3− ts4,4− ts4,5−
q0 {e, f } q1 {g, h} q2 e g f h
() 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 ts2,2− in Figure 3(a).
Using the set of step transition systems ts,− ( = 2, . . . , 4; = 2, . . . , 5), we compare the efectiveness 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 rfist), 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 efectiveness 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 ⊆ Rts 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
Corollary 2. Let R = {r1, r2, . . . , r} ⊆ Rts 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 Rts. For example, for ts in Figure 2(a), we have R{0} = Rt{s0} = {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 nontrivial regions are listed below: (∅, {0}, {}) ({}, {1}, {}) ({}, {2}, ∅) ({}, {1}, {ℎ}) ({ℎ}, {2}, ∅) (∅, {0}, { }) ({ }, {1}, {}) ({ }, {1}, {ℎ}) ¯ r1 ¯ r2 ¯ r3 ¯ r4 ¯ r5 ¯ r6 ¯ r7 ¯ r8 = = = = = = = = ({}, {1, 2}, ∅) ({}, {0, 2}, {}) (∅, {0, 1}, {}) ({ℎ}, {0, 2}, {}) (∅, {0, 1}, {ℎ}) ({ }, {1, 2}, ∅) ({}, {0, 2}, { }) ({ℎ}, {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, ¯r3 = r1 ⊕ r2 = r1 ⊕ r7, where the ifrst 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 diferent 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 ts2,2− in Table 1).
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 enlstsystem 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. 3This still needs to be formally proved.