=Paper=
{{Paper
|id=None
|storemode=property
|title=The Label Splitting Problem
|pdfUrl=https://ceur-ws.org/Vol-725/paper02.pdf
|volume=Vol-725
|dblpUrl=https://dblp.org/rec/conf/apn/Carmona11
}}
==The Label Splitting Problem==
https://ceur-ws.org/Vol-725/paper02.pdf
The Label Splitting Problem
J. Carmona
Universitat Politècnica de Catalunya, Spain
jcarmona@lsi.upc.edu
Abstract. The theory of regions was introduced by Ehrenfeucht and
Rozenberg in the early nineties to explain how to derive (synthesize)
an event-based model from an automaton. To be applicable, the theory
relies on stringent conditions on the input automaton. Although some re-
laxation on these restrictions has been done in the last decade, in general
not every automaton can be synthesized while preserving its behavior. A
crucial step for a non-synthesizable automaton is to transform it in order
to satisfy the synthesis conditions. This paper revisits label splitting, a
technique to satisfy the synthesis conditions through renaming of prob-
lematic labels. For the first time, the problem is formally characterized
and its optimality addressed.
1 Introduction
The synthesis problem [4] consists in building a Petri net [8] that has a behav-
ior equivalent to a given automaton (transition system). The problem was first
addressed by Ehrenfeucht and Rozenberg [5] introducing regions to model the
sets of states that characterize marked places in the Petri net. The theory is
applicable to elementary transition systems, a proper subclass where additional
conditions are required, and for which the synthesis produces a Petri net with
isomorphic behavior. These restrictions were significantly relaxed in [3], introduc-
ing the subclass of excitation-closed transition systems, where not isomorphism
but bisimilarity is guaranteed. The theory of this paper is within the subclass of
excitation-closed transition systems.
When synthesis conditions do not hold, the Petri net derived might represent
a proper superset of the initial behavior [1], and therefore any faithful use of
such Petri net is rather limited. To overcome this problem, one might force
the synthesis conditions by transforming the initial transition system. The work
in [3] was the first in addressing this problem, introducing label splitting as
a technique that can be applied when excitation-closure is not satisfied. The
technique is based on relabeling the transitions of a particular event in the
transition system with new copies of the same event, thus preserving the event
name but considering each new copy as a new event with respect to the synthesis
conditions. However, [3] only presented the technique as a heuristic to progress
into excitation-closure.
The new copies produced by the label splitting technique increase the com-
plexity of the Petri net derived: each new copy will be transformed into a tran-
sition, and hence the label splitting problem is to find an optimal sequence of
22
splittings that induces the minimal number of transitions in the derived Petri
net.
The label splitting technique presented in this paper is a particular one: it is
defined on the sets of states computed when searching for regions in state-based
synthesis methods [1, 3]. These sets, called essential, are the building blocks
used in this paper to decide the labels to split. The methods for label splitting
in the aforementioned work also use the essential sets for label splitting, but as
described previously, only in a heuristic manner.
In summary, this paper presents a novel view on the label splitting technique.
First, we show how label splitting for excitation closure is nothing else than
computing the optimal coloring of a graph, i.e., the chromatic number. Second,
we characterize the conditions under which an optimal label splitting can be
derived to accomplish excitation closure. Finally, we present an algorithm that
can be used when excitation closure can not been attained by a single application
of the label splitting technique presented in this paper. This algorithm is based on
a relaxation of the label splitting problem that can be mapped into the weighted
set cover problem.
For the sake of clarity, the theory of this paper will be presented for the
class of safe (1-bounded) Petri nets. The contribution can be extended with no
substantial change for the class of general (k-bounded) Petri nets.
2 Preliminaries
2.1 Finite transition systems and Petri nets
Definition 1 (Transition system). A transition system is a tuple
(S, E, A, sin ), where S is a set of states, E is an alphabet of actions, such
that S ∩ E = ∅, A ⊆ S × E × S is a set of (labeled) transitions, and sin is the
initial state.
e
We use s → s as a shortcut for (s, e, s ) ∈ A, and we denote its transitive
∗ ∗
closure as →. A state s is said to be reachable from state s if s → s . Let
TS = (S, E, A, sin ) be a transition system. We consider connected transition
systems that satisfy the following axioms: i) S and E are finite sets, ii) every
event has an occurrence: ∀e ∈ E : ∃(s, e, s ) ∈ A, and iii) every state is reachable
∗
from the initial state: ∀s ∈ S : sin → s.
Definition 2 (Petri net [8]). A Petri net is a tuple PN = (P, T, F, M0 ) where
P and T represent finite disjoint sets of places and transitions, respectively, and
F ⊆ (P × T ) ∪ (T × P ) is the flow relation. The initial marking M0 ⊆ P defines
the initial state of the system.
For a node n (place or transition) of a Petri net, •n (n•) is the predecessor
(successor) set of n in F . A transition t ∈ T is enabled in a marking M iff •t ⊆ M .
The firing of t results in a new marking M , with one less token in •t and one more
token in t•. A marking M is reachable from M if there is a sequence of firings
23
σ = t1 t2 . . . tn that transforms M into M , denoted by M [σ M . A sequence of
transitions σ = t1 t2 . . . tn is a feasible sequence if M0 [σ M , for some M . The set
of all markings reachable from the initial marking M0 is called its Reachability
Set. The Reachability Graph of a Petri net PN (RG(PN)) is a transition system
in which the set of states is the Reachability Set, the events are the transitions
t
of the net and a transition (M1 , t, M2 ) exists if and only if M1 → M2 .
2.2 Regions and synthesis
The theory of regions provides a way to go from transition systems to Petri
nets. We now review this theory (the interested reader can refer to [1, 3–5, 7] for
a complete overview). Let S be a subset of the states of a transition system,
S ⊆ S. If s ∈ S and s ∈ S , then we say that transition (s, a, s ) enters S .
If s ∈ S and s ∈ S , then transition (s, a, s ) exits S . Otherwise, transition
(s, a, s ) does not cross S .
Definition 3. Let TS = (S, E, A, sin ) be a transition system. Let S ⊆ S be a
subset of states and e ∈ E be an event. The following conditions (in the form of
predicates) are defined for S and e:
in(e, S ) ≡ ∃(s, e, s ) ∈ A : s, s ∈ S
out(e, S ) ≡ ∃(s, e, s ) ∈ A : s, s ∈ S
nocross(e, S ) ≡ ∃(s1 , e, s2 ) ∈ A : s1 ∈ S ⇔ s2 ∈ S
enter(e, S ) ≡ ∃(s1 , e, s2 ) ∈ A : s1 ∈ S ∧ s2 ∈ S
exit(e, S ) ≡ ∃(s1 , e, s2 ) ∈ A : s1 ∈ S ∧ s2 ∈ S
Note that nocross(e, S ) = in(e, S ) ∨ out(e, S ). We will abuse the notation
and will use nocross(e, S , (s1 , e, s2 )) to denote a transition (s1 , e, s2 ) that makes
the predicate nocross(e, S ) to hold, and the same for the rest of predicates.
The notion of a region is central for the synthesis of Petri nets. Intuitively,
each region is a set of states that corresponds to a place in the synthesized Petri
net, so that every state in the region models the marking of the place.
Definition 4 (Region). A set of states r ⊆ S in transition system TS =
(S, E, A, sin ) is called a region if the following two conditions are satisfied for
each event e ∈ E:
– (i) enter(e, r) ⇒ ¬nocross(e, r) ∧ ¬exit(e, r)
– (ii) exit(e, r) ⇒ ¬nocross(e, r) ∧ ¬enter(e, r)
A region is a subset of states in which all transitions labeled with the same
event e have exactly the same “entry/exit” relation. This relation will become
the successor/predecessor relation in the Petri net. The event may always be
either an enter event for the region (case (i) in the previous definition), or
always be an exit event (case (ii)), or never “cross” the region’s boundaries,
i.e. each transition labeled with e is internal or external to the region, where
24
r2 r1
s1 a b
Minimal Regions
a b r 1 = { s1, s2 }
s2 r3 r4
s3 r 2 = { s1, s3 }
b a d r 3 = { s2, s4 } c
s4 c r 4 = { s3, s4 } r5
r = { s5 }
5
s5 d
(a) (b) (c)
Fig. 1. (a) transition system, (b) minimal regions, (c) synthesis applying Algorithm of
Figure 3.
the antecedents of neither (i) nor (ii) hold. The transition corresponding to the
event will be successor, predecessor or unrelated with the corresponding place
respectively. Examples of regions are reported in Figure 1: from the transition
system of Figure 1(a), some regions are enumerated in Figure 1(b). For instance,
for region r2 , event a is an exit event, event d is an entry event while the rest of
events do not cross the region. Let r and r be regions of a transition system. A
region r is said to be a subregion of r if r ⊂ r. A region r is a minimal region if
there is no other region r which is a subregion of r. Going back to the example
of Figure 1, in Figure 1(b) we report the set of minimal regions. Each transition
system TS = (S, E, A, sin ) has two trivial regions: the set of all states, S, and
the empty set. The set of non-trivial regions of TS will be denoted by RTS .
A region r is a pre-region of event e if there is a transition labeled with
e which exits r. A region r is a post-region of event e if there is a transition
labeled with e which enters r. The sets of all pre-regions and post-regions of e
are denoted with ◦ e and e◦ , respectively. By definition it follows that if r ∈ ◦ e,
then all transitions labeled with e exit r. Similarly, if r ∈ e◦ , then all transitions
labeled with e enter r.
The computation of the minimal regions is crucial for the synthesis methods
in [1, 3]. It is based on the notion of excitation region [6].
Definition 5 (Excitation region). The excitation region of an event e, ER(e),
is the set of states in which e is enabled, i.e.
ER(e) = {s | ∃s : (s, e, s ) ∈ A}
In Fig. 1(a), the set ER(c) = {s4} is an example of an excitation region1 . The
set of minimal regions sufficient for synthesis can be generated from the ERs of
the events in a transition system in the following way: starting from the ER of
1
Excitation regions are not regions in the terms of Definition 4. The term is used for
historical reasons. For instance, ER(c) is not a region.
25
1
d a b d a b1 c b2
7 2 5 b b2 a
b d b1
c c cd c b1
d 3 d d d
6
b b2
(a) (b) d (c)
4
Fig. 2. (a) transition system (only numbers of states are shown), (b) ECTS by label-
splitting, (c) synthesized Petri net.
each event, set expansion is performed on those events that violate the region
condition (a pseudocode of the expansion algorithm is given in Figure 10 in [3]).
The following lemma characterizes the states to be added in the expansion of
ERs:
Lemma 1 (Essential states to become a region [3]). Let TS =
(S, E, A, sin ) be a transition system. Let r ⊂ S be a set of states such that r
is not a region. Let r ⊆ S be a region such that r ⊂ r . Let e ∈ E be an event
that violates some of the conditions for r to be a region. The following predicates
hold:
1. in(e, r) ∧ [enter(e, r) ∨ exit(e, r)] =⇒
{s|∃s ∈ r : (s, e, s ) ∈ A ∨ (s , e, s) ∈ A} ⊆ r
2. enter(e, r) ∧ exit(e, r) =⇒
{s|∃s ∈ r : (s, e, s ) ∈ A ∨ (s , e, s) ∈ A} ⊆ r
3. out(e, r) ∧ enter(e, r) =⇒
[{s|∃s ∈ r : (s, e, s ) ∈ A} ⊆ r ] ∨ [{s|∃s ∈ r : (s , e, s) ∈ A} ⊆ r ]
4. out(e, r) ∧ exit(e, r) =⇒
[{s|∃s ∈ r : (s , e, s) ∈ A} ⊆ r ] ∨ [{s|∃s ∈ r : (s, e, s ) ∈ A} ⊆ r ]
Hence, in cases 1 and 2 above, the violating event e is converted into a
nocross event, where only one way of expanding r is possible. On the contrary,
in case 3 (4) there are two possibilities for expansion, depending on whether the
violating event will be converted into an enter or nocross (exit or nocross)
event. In summary, set expansion to legalize violating events in a set of states
generates a binary exploration tree. An example of such tree can be found in [3],
Fig.12(b). The following definition formalizes the notion of essential set:
Definition 6 (Essential set of an event). Let TS = (S, E, A, sin ) be a tran-
sition system, and event e ∈ E. Essential(e) is the set of sets of states found by
inductive application of Lem. 1, with initial set ER(e).
Notice that Essential(e) ⊆ P(S), and ∀Si ∈ Essential(e) :
ER(e) ⊆ Si . For instance, in Fig. 2(a) Essential(c) = {ER(c) =
{s2, s5}, {s1, s2, s5, s7}, {s2, s3, s5, s6}}. The two states different from ER(c) in
Essential(c) are computed according to case 4 in Lem. 1 on event b.
26
Algorithm: Petri net synthesis
– For each event e ∈ E generate a transition labeled with e in the Petri net;
– For each minimal region ri ∈ RTS generate a place ri ;
– Place ri contains a token in the initial marking iff the corresponding
region ri contains the initial state of TS sin ;
– The flow relation is as follows: e ∈ ri • iff ri is a pre-region of e
and e ∈ •ri iff ri is a post-region of e, i.e.,
FTS = {(r, e)|r ∈ RTS ∧ e ∈ E ∧ r ∈ ◦ e}
def
∪{(e, r)|r ∈ RTS ∧ e ∈ E ∧ r ∈ e◦ }
Fig. 3. Algorithm for Petri net synthesis from [7].
The procedure given by [7] to synthesize a Petri net, NTS =
(RTS , E, FTS , Rsin ), from an elementary transition system2 , TS = (S, E, A, sin ),
is illustrated in Figure 3. Notice that only minimal regions are required in the
algorithm [4]. An example of the application of the algorithm is shown in Fig-
ure 1. The initial transition system and the set of minimal regions is reported
in Figures 1(a) and (b), respectively. The synthesized Petri net is shown in Fig-
ure 1(c).
2.3 Excitation-closed transition systems
Definition 7 (Excitation-closed transition systems). A transition system
TS = (S, E, A, sin ) is excitation-closed (ECTS) if it satisfies the following two
axioms:
– Excitation closure (EC): For each event a: r∈ ◦ a r = ER(a)
– Event effectiveness: For each event a: ◦ a = ∅
The synthesis algorithm in Figure 3 applied to an ECTS derives a Petri net
with reachability graph bisimilar to the initial transition system [3]. When the
transition system is not excitation closed, then it must be transformed to enforce
that property. One possible strategy is to represent every event by multiple
transitions with the same label. This technique is called label splitting. Figure 2
illustrates the technique. The initial transition system, shown in Figure 2(a),
is not an ECTS: the event c is not EC (the only minimal region that contains
ER(c) is {s2, s3, s5, s6}, which does not makes the EC axiom of Def. 7 to hold).
The transition system is transformed by splitting the event b into the events b1
and b2 , as shown in Figure 2(b), resulting in an ECTS. The synthesized Petri
net, with two transitions for event b is shown in Figure 2(c). The reachability
2
Elementary transition systems are a proper subclass of the transition systems con-
sidered in this paper, were additional conditions to the ones presented in Section 2.1
are required.
27
bisimilar (abstracting event instances)
split−morphic bisimilar
Reachability
TS TS’ Petri Net Graph
Label Synthesis Behavior
Splitting
Fig. 4. Relationship between the different objects if label splitting is applied.
graph of the Petri net of Fig. 2(c) is split-morphic [3] to the transition system
of Fig. 2(a): there exist a surjective mapping between the sets of events, where
different instances of the same event (a1 , a2 , . . .) are mapped to the only one
event a. If we abstract away the label indexes, the equivalence relation defined is
bisimilarity. Fig. 4 shows the relationships between the original transition system,
the transformed one obtained through label splitting, and the reachability graph
of the synthesized Petri net.
Hence in Petri net synthesis label splitting might be crucial for the existence
of a Petri net with bisimilar behavior. The following definition describes the
general application of label splitting:
Definition 8 (Label splitting). Let TS = (S, E, A, sin ) be a transition system.
The splitting of event e ∈ E derives a transition system TS = (S, E , A , sin ),
with E = E − {e} ∪ {e1 , . . . , en }, and such that every transition (s1 , e, s2 ) ∈ A
corresponds to exactly one transition (s1 , ei , s2 ), and the rest of transitions for
events different from e in A are preserved in A .
Label splitting is a powerful transformation which always guarantees exci-
tation closure: any TS can be converted into one where every transition has a
different label. By definition, the obtained TS is ECTS but the size of the de-
rived Petri net is equal to the size of the obtained ECTS. In this paper we aim at
reducing the number of splittings, thus reducing the size of the Petri net derived.
The work presented in this paper considers a particular application of the la-
bel splitting technique which is based on converting a set into a region, described
in the next section. By restricting the transformation, we are able to determine
these situations where a minimal set of labels is enough to guarantee excitation
closure.
3 Optimal label splitting to attain a region
In this section the following problem is addressed: given a transition system
TS = (S, E, A, sin ) and a set of states S ⊆ S which is not a region, determine
the minimal number of label splittings to be applied in order to S become
a region. This is a crucial step for the technique presented in the following
section to satisfy the ECTS condition. The main contribution of this section is
28
1 (3, b, 4) (3, b, 4)
b
7 2 5 b
b (2, b, 7) (6, b, 1) (2, b, 7) (6, b, 1)
3 6
b
4 (5, b, 1) (5, b, 1)
(a) (b) (c)
Fig. 5. (a) Projection of the transition system of Fig. 2(a) for the transitions on event
b and set of states {s2 , s5 }, (b) GG(b, {s2 , s5 }), (c) coloring.
to show that the problem might be reduced to compute the chromatic number
of a graph [9].
First we introduce the concept of gradient graph:
Definition 9 (Gradient Graph). Given a transition system TS =
(S, E, A, sin ), a set S ⊆ S and an event e ∈ E, the gradient graph of e with re-
spect to S in TS, denoted as GG(e, S ) = (Ae , M ) is an undirected graph defined
as:
– Ae = {(s, x, s )|(s, x, s ) ∈ A ∧ x = e}, is the set of nodes
– M = {(v, v )|v, v ∈ Ae ∧
[(enter(e, S , v) ∧ (nocross(e, S , v ) ∨ exit(e, S , v ))) ∨
(exit(e, S , v) ∧ (nocross(e, S , v ) ∨ enter(e, S , v )))]}, is the set of edges.
Informally, the gradient graph contains as nodes the transitions of an event
e, and an edge exist between two nodes if they satisfy different predicates on set
S . For instance, the gradient graph on event b and set of states S = {s2 , s5 } in
the transition system of Fig. 2(a) is shown in Fig. 5(b) (for the sake of clarity
we show in Fig. 5(a) the transitions on event b from Fig. 2(a)).
A graph G = (V, E) is k-colourable if there exists an assignment
α : V → {1, 2, . . . k} for which any pair of nodes v, v ∈ V such that (v, v ) ∈ E
satisfy α(v) = α(v ). The chromatic number, χ(G), of a graph G is the mini-
mum k for which G is k-colourable [9]. The rest of the section shows the relation
between the chromatic number and the optimal label splitting to attain a region.
Definition 10 (Label splitting as gradient graph coloring). Given a
transition system TS = (S, E, A, sin ), the label splitting of event e according
to a coloring α of the gradient graph GG(e, S ) derives the transition system
TS = (S, E , A , sin ) where E = E − {e} ∪ {e1 , . . . , en }, with {e1 , . . . , en } being
the colors defined by the coloring of GG(e, S ). Every transition (s, e, s ) of event
e is transformed into (s, eα((s,e,s )) , s ), whilst the rest of transitions of events in
E − {e} are preserved in A .
For instance, the label splitting of the transition system of Fig. 2(a) according
to the coloring shown in Fig. 5(c) of GG(b, {s2 , s5 }) is shown on Fig. 2(b).
29
Proposition 1. Given a transition system TS = (S, E, A, sin ) and the gradient
graph GG(e, S ). If event e is split in accordance with a χ(GG(e, S ))-coloring
of GG(e, S ) then the new events {e1 , . . . , eχ(GG(e,S )) } inserted satisfy the region
condition on S (c.f., Def. 4)).
Proof. By contradiction: assume there exists ei ∈ {e1 , . . . , eχ(GG(e,S )) } such that
conditions of Def. 4 do not hold. Without loss of generality, we assume that there
exist (s1 , ei , s2 ) and (s1 , ei , s2 ) for which predicates enter(ei , S , (s1 , ei , s2 )) and
nocross(ei , S , (s1 , ei , s2 )) hold (the other cases can be proven similarly). But
then the nodes (s1 , ei , s2 ) and (s1 , ei , s2 ) are connected by an edge, but they are
assigned the same color ei . Contradiction. 2
Corollary 1. Given a transition system TS = (S, E, A, sin ) and a set S ⊆ S. If
every event e is split according to the colors required for achieving χ(GG(e, S )),
then S is a region in the resulting transition system.
Proof. It follows from iterative application of Prop. 1. 2
In the following theorem we abuse the notation and extend the χ operator
to sets of states:
Theorem 1. Given a transition system TS = (S, E, A, sin ) and a set S ⊆ S,
let χ(S ) = χ(GG(e1 , S )) + . . . + χ(GG(en , S )), with E = {e1 , . . . , en }. Then
χ(S ) is a lower bound to the number of labels needed to make S to be a region.
Proof. By contradiction: if there is a k < χ(S ) such that only k labels are
needed to convert S into region, then there is an event e ∈ E for which less
than χ(GG(e, S )) labels are used to split e for satisfying the conditions of Def. 4.
This leads to a contradiction to the chromatic number of the graph GG(e, S ). 2
The theory of this section represents the core idea for the label splitting
technique of this paper. The next section shows how apply it to attain ECTSs.
4 Optimal label splitting on essential sets for synthesis
Given a non-ECTS, the following question arises: is there an algorithm to trans-
form it into an ECTS with a minimal number of label splittings? This section
addresses this problem, deriving sufficient conditions under which a positive an-
swer can be given. As was done in previous work [3], in this paper we will restrict
the theory to a particular application of the label splitting: instead of an arbi-
trary instantiation of Def. 8 which may split an event of a transition system in
peculiar way, we will only consider the splittings used to convert essential sets
into regions (Def. 10), technique which has been shown in the previous section.
We will tackle the problem in two phases: first, we will show how the EC for
a given event can be achieved by using the essential sets found in the expansion
of the ER of an event, defined in Lem. 1. Then we will show the conditions
under which the strategy can be applied in the general case, i.e. considering the
30
whole set of non-EC events. We start by defining the set of states that both are
included in the intersection of pre-regions of an event but are not included in
the excitation region:
Remainder(e) = ( q) \ ER(e)
q∈ ◦ e
Clearly, event e is EC if and only if Remainder(e) = ∅ (cf., Def. 7).
For the definitions and theorems below, we assume a context transition sys-
tem TS = (S, E, A, sin ), and use W itness(e) to denote the sets of essential sets of
an event e such that, if they are converted into regions, Remainder(e) becomes
empty. Formally:
Definition 11 (Witness set of an event). Let TS = (S, E, A, sin ) be a tran-
sition system, and event e ∈ E. Witness(e) is defined as follows:
C = {S1 , . . . , Sk } ∈ W itness(e) ⇐⇒ ∀Si ∈ C : Si ∈ Essential(e) ∧
( q∈( ◦ e ∪ C) q) \ ER(e) = ∅
Finally, if C = {S1 , . . . , Sk }, we abuse the notation and use χ(C) to denote
χ(GG(e1 , S1 ) ∪ . . . ∪ GG(e1 , Sk )) + . . . + χ(GG(en , S1 ) ∪ . . . ∪ GG(en , Sk )), with
E = {e1 , . . . , en }. The union operator on gradient graphs is defined as GG(e, S1 )∪
. . . ∪ GG(e, Sk ) = (Ae , M1 ∪ . . . ∪ Mk ), with Ae and Mi being the nodes and edges
of the graph GG(e, Si ), respectively c.f., Def. 93 .
First, we start by describing the minimal strategy to make an event to satisfy
its excitation closure:
Proposition 2. Let C = {S1 , . . . , Sk } ∈ W itness(e) such that χ(C) is minimal,
i.e., ∀C ∈ W itness(e) : χ(C) ≤ χ(C ). Then, if only label splitting on essential
sets (Def. 10) is considered, χ(C) is the minimal number of labels needed to make
Remainder(e) = ∅.
Proof. The minimality of χ(C) guarantees that, by using label splitting on es-
sential sets, the minimal number of labels has been used in the coloring of the
gradient graphs of each event for each set in C. 2
Given a non-ECTS, the optimal label splitting problem on essential sets is to
determine the sets to convert into regions in order to reduce the set Remainder
to the empty set for each non-EC event, using minimal number of labels.
Definition 12 (Optimal label splitting on essential sets). Given the
non-EC events e1 . . . ek ∈ E, define the universe U as W itness(e1 ) ∪
. . . ∪ W itness(ek ). The optimal label splitting problem is to determine sets
S1 , . . . , Sn ⊆ U such that ∀1 ≤ i ≤ k : ∃C ∈ W itness(ei ) : C ⊆ {S1 , . . . , Sn } and
where χ(S1 , . . . , Sn ) is minimal.
3
We only consider the union of gradient graphs of the same event.
31
s0 s0 s0
n n n n n1 n2
s1 s2 s1 s2 s1 s2
c c c c c1 c2
s3 s4 s3 s4 s3 s4
a e e a a e1 e2 a a1 e1 e2 a2
s5 s6 s7 s8 s5 s6 s7 s8 s5 s6 s7 s8
b b b
s9 s9 s9
(a) (b) (c)
Fig. 6. (a) Initial transition system: all the events but b are EC, (b) the splitting of e
leads to new events e1 and e2 not satisfying the EC property, (c) the final ECTS, where
all events have been split.
Notice that Def. 12 is defined on the set of all essential sets of the non-
EC events, searching for a set of essential sets which both has minimal number
of labels and ensures EC for these events. An interesting result guarantees EC
preservation for those events that both satisfy initially the EC and were not split:
Proposition 3. Let e ∈ E be such that Remainder(e) = ∅ and it has not
been selected for splitting. Then Remainder(e) = ∅ in the new transition system
obtained after label splitting.
Proof. Label splitting preserves the set of regions: the predicates of Def. 4 that
hold on each region will also hold if some event is split. Hence, the witness set
of regions that ensures Remainder(e) = ∅ is still valid after label splitting. 2
However, label splitting may break events for which the excitation closure
was satisfied or attained. Unfortunately, the new events appearing might not
satisfy the excitation closure property as the following example demonstrates.
Example 1. In the transition system of Figure 6(a) events n, c, a and e are EC, as
demonstrated by their witness: W itness(n) = {{s0}}, W itness(c) = {{s1, s2}},
W itness(a) = W itness(e) = {{s3, s4}}. However, b is not EC, and the splitting
required for b to be EC is done on the essential set {s6}, which requires to
split the EC event e, resulting in the transition system of Fig. 6(b). The new
events e1 and e2 arising from the splitting of e are not EC. This requires further
splittings, which as in the case of b, force the splitting of EC events resulting
in new events that are not EC. Four iterations are required to attain the ECTS
shown in Fig. 6(c).
This example invalidates any label splitting strategy that aims at reaching
excitation closure in just one iteration of the synthesis process: in general, when
the splitting of some event is applied, its ER is divided into several ERs for which
there might be no witness which guarantee the EC of these new events arising.
32
Importantly, the label splitting technique preserves the regions, but new regions
might be necessary for the new events arising from a splitting. Therefore, any
label splitting technique must be an iterative method (see next section for such
a method). However, if the new labels inserted do not incur excitation closure
problems, the presented technique guarantees the optimal label splitting:
Theorem 2. Let TS = (S, E , A , sin ) be the transition system reached af-
ter splitting labels on non-EC events e1 , . . . ek in transition system TS =
(S, E, A, sin ), using the strategy from Def. 12. Then, if the new events appearing
are EC, the number of splittings performed is minimal and TS is ECTS.
Proof. The minimality of the strategy used in Def. 12 ensures that no less split-
tings are possible to make e1 , . . . ek EC. Moreover, the assumption implies that
the new events arising from the splitting are EC. Finally, Prop. 3 guarantees that
EC events that were not split are still EC. The set of events E is partitioned
into these three sets, and therefore TS is ECTS. 2
5 A greedy algorithm for iterative label splitting
The optimization problem for optimal label splitting presented in the previous
section is hard to tackle: considering the global optimal label splitting through
local achievement of EC for every non-EC event. However, if some relaxations are
done, the problem can be seen as an instance of the weighted set cover (WSC)
problem [2]. This section shows how to cast the problem into an WSC setting
and depicts an algorithm for label splitting that iterates until excitation closure
is attained. Unfortunately, for a set of witness elements S1 , . . . , Sn , the equality
χ(S1 , . . . , Sn ) = χ(S1 ) + . . . + χ(Sn ) (1)
does not hold in general, e.g., imagine that some Si , Sj satisfy Si ∩ Sj = ∅: in
that situation one may be counting twice the labels (colors) needed in the right
part of the equality of (1). That prevents an exact mapping of the label splitting
optimization problem into the WSC setting. However, one may allow this impre-
cision for the sake of having an efficient manner to derive good candidates. The
following model maps the optimization problem of Def. 12 into an ILP problem,
whose solution provides candidates that, although potentially suboptimal, might
represent good candidates for label splitting in practice:
min C∈W χ(C) · XC (2)
s.t.
∀e ∈ e1 . . . ek : C∈W itness(e) XC ≥ 1
XC ∈ {0, 1}
where e1 . . . ek ∈ E are the set of non-EC events and W = W itness(e1 ) ∪ . . . ∪
W itness(ek ). A solution to the ILP model (2) will then minimize the sum of the
cost of the witness selected for each non-EC event.
33
Algorithm 1: IterativeSplittingAlgorithm
Input: Transition system TS = (S, E, A, sin )
Output: Excitation-closed transition system TS = (S, E , A , sin ) bisimilar to
TS
1 begin
2 TS = TS
3 R = GenerateMinimalRegions(TS)
4 while not (ExcitationClosed(TS ,R)) do
5 W = CollectWitnesses(TS )
6 (S1 , . . . , Sn ) = Solution ILP model (2)
7 TS = SplitLabels(TS , S1 , . . . , Sn )
8 R = R ∪ {S1 , . . . , Sn }
9 end
10 end
Algorithm 1 presents the iterative strategy to derive an ECTS. It first com-
putes the minimal regions of the initial transition system. Then the main loop of
the technique starts by collecting the witnesses for non-EC events of the current
transition system, which are provided in the set W (line 5). Then the cover for
the non-EC events is computed by solving the ILP model (2) in line 6. Notice
that for the sake of clarity of the algorithm, we provide in line 6 the sets that
form the cover instead of providing the particular witness selected for each event
(i.e., given a solution C1 , . . . , Ck of model (2), {S1 , . . . , Sn } = 1≤i≤k Ci ). In line
7 the splitting of labels corresponding to χ(S1 , . . . , Sn ) is performed, ensuring
that sets S1 , . . . , Sn become regions. The new regions are appended to the regions
found so far (which are still regions, see proof of Prop. 3), and the excitation
closure is re-evaluated to check convergence.
Although the presented iterative technique is not guaranteed to provide the
optimal, the improvements with respect to the previous (also non-optimal) ap-
proaches [1, 3] are:
– the whole set of non-EC events are considered in every iteration: in previous
work only one is considered, and
– for every non-EC event, the necessary splittings are applied to attain excita-
tion closure: on the previous work, only one of the splittings was applied.
Hence the macro technique presented in this section is meant to speed-up the
achievement of the excitation closure, when compared to the micro techniques
presented in the literature.
6 Discussion and conclusions
This paper has presented a fresh look at the problem of label splitting, by relating
it to some of the well-known NP-complete problems like chromatic number or
34
set covering. In a restricted application of label splitting based on essential sets,
optimality is guaranteed if certain conditions hold.
For the sake of clarity, we have restricted the theory to safe Petri nets. The
extension to k-bounded Petri nets can be done by adapting the notion of gradient
graph to use gradients (see [1] for the formal definition of gradient) instead of
the predicates required in Def. 4. Given a multiset r which is not a k-bounded
region, the essential sets will be those multisets r ≥ r such that the number of
gradients for some event has decreased, i.e., r is a sound step towards deriving
a region from multiset r. Finally, the excitation closure definition for the general
case should be the one described in [1], and the witness of an event defined
accordingly.
As a future work, addressing the general problem with unrestricted applica-
tion of splitting (i.e., not using essential sets but instead arbitrary selections of
labels to split) might be an interesting direction to follow. Also, incorporating
the presented techniques into our synthesis tool [1] will be considered.
References
1. J. Carmona, J. Cortadella, and M. Kishinevsky. New region-based algorithms for
deriving bounded Petri nets. IEEE Transactions on Computers, 59(3):371–384,
2009.
2. T. H. Cormen, C. Stein, R. L. Rivest, and C. E. Leiserson. Introduction to Algo-
rithms. McGraw-Hill Higher Education, 2001.
3. J. Cortadella, M. Kishinevsky, L. Lavagno, and A. Yakovlev. Deriving Petri nets
from finite transition systems. IEEE Transactions on Computers, 47(8):859–882,
Aug. 1998.
4. J. Desel and W. Reisig. The synthesis problem of Petri nets. Acta Inf., 33(4):297–
315, 1996.
5. A. Ehrenfeucht and G. Rozenberg. Partial (Set) 2-Structures. Part I, II. Acta
Informatica, 27:315–368, 1990.
6. M. Kishinevsky, A. Kondratyev, A. Taubin, and V. Varshavsky. Concurrent Hard-
ware: The Theory and Practice of Self-Timed Design. John Wiley and Sons, London,
1993.
7. M. Nielsen, G. Rozenberg, and P. Thiagarajan. Elementary transition systems.
Theoretical Computer Science, 96:3–33, 1992.
8. C. A. Petri. Kommunikation mit Automaten. PhD thesis, Bonn, Institut für Instru-
mentelle Mathematik, 1962. (technical report Schriften des IIM Nr. 3).
9. D. B. West. Introduction to Graph Theory. Prentice-Hall, 1996.
35