=Paper=
{{Paper
|id=Vol-1591/paper11
|storemode=property
|title=Kleene Theorem for Labelled Free Choice Nets without Distributed Choice
|pdfUrl=https://ceur-ws.org/Vol-1591/paper11.pdf
|volume=Vol-1591
|authors=Ramchandra Phawade
|dblpUrl=https://dblp.org/rec/conf/apn/Phawade16
}}
==Kleene Theorem for Labelled Free Choice Nets without Distributed Choice==
https://ceur-ws.org/Vol-1591/paper11.pdf
Kleene Theorem for Labelled Free Choice Nets
without Distributed Choice
Ramchandra Phawade
Indian Institute of Technology Bombay, Powai, Mumbai 400076, India
Abstract. For 1-bounded nets, equivalent syntax have been given by
Grabowski [8], Garg and Ragunath [7] and other authors Lodaya [14].
We work with 1-bounded, labelled free choice nets given with an S-cover,
where the labels come from a distributed alphabet and S-components
of the associated S-cover respect the alphabet distribution. In earlier
work [21], we provided expressions for free choice nets having “distributed
choice property” which makes the nets “direct product” representable.
These expressions have “pairings” of blocks of derivatives–representing
automaton states–which specify how synchronizations take place.
In this work, we give equivalent syntax for a larger class of free choice
nets obtained by dropping “distributed choice property”. Hence we deal
with the nets which are not representable by direct products also. Now
“pairings” relate the tuples of blocks of derivatives and their effects–
representing automaton transitions–in our expressions.
1 Introduction
The Kleene theorem for regular expressions enables us to translate from regular
expressions to automata and back [12]. Expressions are widely used by pro-
grammers to describe languages of software components. They are thought of
as a user-friendly alternative to the finite state machines for describing software
components [11]. On the other hand they can be used for axiomatizing language
equivalence [23,13] and characterizing subclasses of automata.
Free choice nets form an important subclass of Petri nets, having pleasant
theory [24,5] and from verification point of view some of the advantages of 1-
bounded free choice nets are checking liveness is in PTIME [6,4], checking dead-
lock is NP-complete [3] and reachability problem is PSPACE-complete [3]. All
these problems are PSPACE-complete for 1-bounded nets [3].
Language equivalent expressions for 1-bounded nets have been given by
Grabowski [8], Garg and Ragunath [7] and other authors [14], where renam-
ing operator has been used in the syntax to disambiguate synchronizations. In
earlier [15,21,22] works, we have provided syntax for various subclasses of 1-
bounded free choice nets, and we have used product systems as intermediary
formalism. Since we do not use renaming operator in our syntax, our labellings
has to preserve the process stucture, i.e. same label can not be used for syn-
chronizations by different sets of processes. This also enables us to compare
expressiveness of nets with those of different classes of product automata [17].
R. Phawade: Kleene Theorem for Labelled Free Choice Nets 133
A restriction of our earlier work [19], was that of “distributed choice”. Roughly,
this says that if two transitions in a cluster of a free choice net are labelled the
same, then they cannot be used to discriminate between post-places. In this
paper we remove this restriction.
r1 s1
r1 s1
λ(t1 ) = a λ(t2 ) = a
a a a a
r2 r3 s2 s3
b c d e r2 r3 s2 s3
b c d e
Fig. 1. Free Choice Net without Fig. 2. S-cover of the net in Fig. 1
distributed choice
The Figure 1 shows an example 1-bounded labelled net which is free choice
but does not satisfy this property. A short proof [18] using a characterization
of direct product languages [17] shows that the language of this net with fi-
nal marking {r1 , s1 } is not accepted by a direct product. Its (only possible)
S-decomposition is shown in Figure 2. If we used our earlier theorems on this
example, we would get the informal expression fsync((ab + ac)∗ , (ad + ae)∗ ),
that is, the fsync (synchronization) of the two regular expressions. But this is
not what the net does, perhaps its behavior can be informally described as
(fsync(ab, ad) + fsync(ac, ae))∗ , the left choices (moves (r1 , a, r2 ) and (s1 , a, s2 ))
and the right choices (moves (r1 , a, r3 ) and (s1 , a, s3 )) separately pair up to syn-
chronize. In other words, what a net transition does has to be remembered in
the product system, and that we capture by “globals” of product system, which
are nothing but a set of–global moves–tuples of local moves. Indeed, these prod-
uct systems with globals are more expressive than direct products and are a
restricted version of Zielonka automaton [25].
In Section 2 we formally define the nets without distributed choice property
and the product systems with globals and in the subsequent section we prove
the equivalence of these two formalisms.
On the expressions side, these global moves are represented by “cables” which
are tuples of “ducts” (representing local moves in the product system which in
turn are arcs inside S-components). This syntactic machinery along with the
syntax of expressions is developed in Section 4. In previous works [21,22] we
have developed the concept of “blocks” –collection of derivatives [1]–which rep-
resents a state of an automaton or a place in the net. To represent a local move
(p, a, q) belonging to some component automaton– of a product system–in reg-
ular expression corresponding to it, we need to identify the blocks of derivatives
corresponding to source place p and target place q of the local move. While the
134 PNSE’16 – Petri Nets and Software Engineering
former part has been dealt previously [21], using the notion of “bifurcation”; it
alone is not sufficient to get a block corresponding to the target place, because
of two difficulties: first is the possibility of existence of multiple target states, for
a given source state, due to nondeterminism on local actions; and the second dif-
ficulty arises from the fact that, in some sense, bifurcation works in the forward
direction of outgoing moves and does not help in keeping the identity of target
places intact. To handle this, we introduce the notion of “funneling” in Section 4,
and the task of formally establishing the correspondence between a local move
and a duct is achieved in Lemma 4 of Section 5. In the same section we prove
equivalence between product systems with globals and expressions with cables.
Final section summarizes the work and discusses time complexities involved in
the translations.
2 Preliminaries
Let Σ be a finite alphabet and Σ ∗ be the set of all words over alphabet Σ,
including the empty word ε. A language over an alphabet Σ is a subset L ⊆ Σ ∗ .
The projection of a word(w ∈ Σ ∗ to a set ∆ ⊆ Σ, denoted as w↓∆ , is defined by
a(σ↓∆ ) if a ∈ ∆,
ε↓∆ = ε and (aσ)↓∆ =
σ↓∆ if a ∈
/ ∆.
For a set S let ℘(S) denote the set of all subsets of S. To simplify notations
sometimes we may denote a singleton set like {r} by its element r.
Definition 1 (Distributed Alphabet). Let Loc denote the set {1, 2, . . . , k}.
A distribution
S of Σ over Loc is a tuple of nonempty sets (Σ1 , Σ2 , . . . , Σk ) with
Σ = 1≤i≤k Σi . For each action a ∈ Σ, its locations are the set loc(a) = {i |
a ∈ Σi }. Actions a ∈ Σ such that |loc(a)| = 1 are called local, otherwise they
are called global.
2.1 Nets
Definition 2. A labelled net N is a tuple (S, T, F, λ), where S is a set of places,
T is a set of transitions labelled by the function λ : T → Σ and F ⊆ (T × S) ∪
(S × T ) is the flow relation.
Elements of S ∪ T are called nodes of N . Given a node z of net N , set
•
z = {x | (x, z) ∈ F } is called pre-set of z and z •S= {x | (z, x) ∈ F }Sis called
post-set of z. Given a set Z of nodes of N , let • Z = z∈Z • z and Z • = z∈Z z • .
We only consider nets in which every transition has nonempty pre- and post-
set. For all actions a in Σ let Ta = {t | t ∈ T and λ(t) = a}.
Net Systems and their Languages For our results we are only interested in
1-bounded nets, where a place is either marked or not marked. Hence we define
a marking of a net as a subset of its places.
R. Phawade: Kleene Theorem for Labelled Free Choice Nets 135
Definition 3. A labelled net system is a tuple (N, M0 , G) where N = (S, T, F, λ)
is a labelled net with M0 ⊆ S as its initial marking and a set of markings
G ⊆ ℘(S).
A transition t is enabled in a marking M if all places in its pre-set are marked
by M . In such a case, t can be fired to yield the new marking M 0 = (M \ • t) ∪ t •
and, we write this as M [tiM 0 or M [λ(t)iM 0 . A firing sequence (finite or infinite)
λ(t1 )λ(t2 ) . . . is defined by composition, from M0 [t1 iM1 [t2 i . . . For every i ≤ j,
we say that Mj is reachable from Mi . We say a net system (N, M0 ) is live if, for
every reachable marking M and every transition t, there exists a marking M 0
reachable from M which enables t.
Definition 4. For a labelled net system (N, M0 , G), its language is defined as
Lang(N, M0 , G) = {λ(σ) ∈ Σ ∗ | σ ∈ T ∗ and M0 [σiM, for some M ∈ G}.
Net Systems and its components
Definition 5. Let N 0 = (S ∩ X, T ∩ X, F ∩ (X × X)) be a subnet of net N =
(S, T, F ), generated by a nonempty set X of nodes of N . Subnet N 0 is called a
component of N if,
– For each place s of X, • s, s • ⊆ X (the pre- and post-sets are taken in N ),
– For all transitions t ∈ T , we have |• t| = 1 = |t • | (N 0 is an S-net [5]),
– Under the flow relation, N 0 is connected.
A set C of components of net N is called S-cover for N , if every place of the
net belongs to some component of C. A net is covered by components if it has an
S-cover.
Note that our notion of component does not require strong connectedness
and so it is different from notion of S-component in [5], and therefore our notion
of S-cover also differs from theirs.
Fix a distribution (Σ1 , Σ2 , . . . , Σk ) of Σ. The next definition appears in sev-
eral places for unlabelled nets, starting with [10].
Definition 6. A labelled net N = (S, T, F, λ) is called S-decomposable if,
there exists an S-cover C for N , such that for each Ti = {λ−1 (a) | a ∈ Σi }, there
exists Si such that the induced component (Si , Ti , Fi ) is in C.
Now from S-decomposability we get an S-cover for net N , since there exist
subsets S1 , S2 , . . . , Sk of places S, such that S = S1 ∪S2 ∪. . . Sk and • Si ∪Si• = Ti ,
such that the subnet (Si , Ti , Fi ) generated by Si and Ti is an S-net, where Fi is
the induced flow relation from Si and Ti .
If a net (S, T, F, λ) is 1-bounded and S-decomposable then a marking can be
written as a k-tuple from its component places S1 × S2 × . . . × Sk . As before [21],
we enforce the “direct product” condition on the set of final markings.
136 PNSE’16 – Petri Nets and Software Engineering
Definition 7. An S-decomposable labelled net system (N, M0 , G) is an S-
decomposable labelled net N = (S, T, F, λ) along with an initial marking M0 and
a set of markings G ⊆ ℘(S), which is a direct product: if hq1 , q2 , . . . qk i ∈ G
and hq10 , q20 , . . . qk0 i ∈ G then {q1 , q10 } × {q2 , q20 } × . . . × {qk , qk0 } ⊆ G.
Let t be a transition in Ta . Then by S-decomposability a pre-place and a
post-place of t belongs to each Si for all i in loc(a). Let t[i] denote the tuple
hp, a, p0 i such that (p, t), (t, p0 ) ∈ Fi , for p, p0 ∈ Pi for all i in loc(a).
Free choice nets and distributed choice
Definition 8 (Free choice nets [5]). Let x be a node of a net N . The cluster
of x, denoted by [x], is the minimal set of nodes containing x such that
– if a place s ∈ [x] then s• is included in [x], and
– if a transition t ∈ [x] then • t is included in [x].
A cluster C is called free choice (FC) if all transitions in C have the same pre-set.
A net is called free choice if all its clusters are free choice.
In a labelled net N , for a free choice cluster C = (SC , TC ) define the a-
labelled transitions Ca = {t ∈ TC | λ(t) = a}. If the net has an S-decomposition
then we associate a post-product π(t) = Πi∈loc(a) (t • ∩ Si ) with every such tran-
sition t. This is well defined since by the S-net condition
[ every transition will
have at most one post-place in Si . Let post(Ca ) = π(t). We also define the
t∈Ca
post-projection of the cluster Ca [i] = Ca • ∩ Si and the post-decomposition
postdecomp(Ca ) = Πi∈loc(a) Ca [i]. Clearly post(Ca ) ⊆ postdecomp(Ca ). The fol-
lowing definition generalized from [19,18] provides the way to direct product
representability.
Definition 9. An S-decomposable net N = (S, T, F, λ) is said to have dis-
tributed choice property if, for all a in Σ and for all free choice clusters C
of N , postdecomp(Ca ) ⊆ post(Ca ).
Example 1 (A net without distributed choice property). Consider a distributed
alphabet Σ = (Σ1 = {a, b, c}, Σ2 = {a, d, e}) and the labelled net system (N =
(S, T, F, λ), {r1 , s1 }, {{r1 , s1 }}) shown in Figure 1 defined over it. Its (only pos-
sible) S-cover having two S-components with sets of places S1 = {r1 , r2 , r3 } and
S2 = {s1 , s2 , s3 } respectively, is given in Figure 2. Since N is S-decomposable,
we can write its markings as tuples, therefore it can be alternately described as
(N, (p1 , p2 ), {(p1 , p2 )}). For the cluster C of [r1 ], we have the set of a-labelled
transitions Ca = {t1 , t2 } with its post-projections Ca [1] = {r2 , r3 } and Ca [2] =
{s2 , s3 }. So we get postdecomp(Ca ) = {(r2 , s2 ), (r2 , s3 ), (r3 , s2 ), (r3 , s3 )}. The
post-products are π(t1 ) = {(r2 , s2 )} and π(t2 ) = {(r3 , s3 )}. Therefore we have
post(Ca ) = {(r2 , s2 ), (r3 , s3 )}. Since postdecomp(Ca ) * post(Ca ), this cluster
does not have distributed choice, so the net system does not have it.
R. Phawade: Kleene Theorem for Labelled Free Choice Nets 137
Example 2 (A net with distributed choice property). Consider the labelled net
system (N, (p1 , p2 ), {(p1 , p2 )}) of Figure 3, defined over distributed alphabet Σ =
(Σ1 = {a, b, c}, Σ2 = {a, d, e}). Its two S-components with sets of places S1 =
{p1 , p3 , p4 } and S2 = {p2 , p5 }, are shown in Figure 4. For cluster C of p1 , we
have Ca = {t1 , t2 }, Ca [1] = {p3 , p4 } and Ca [2] = {p5 }, hence postdecomp(Ca ) =
{(p3 , p5 ), (p4 , p5 )}. The post-products π(t1 ) = {(p3 , p5 )} and π(t2 ) = {(p4 , p5 )}
give post(Ca ) = {(p3 , p5 ), (p4 , p5 )}. Hence postdecomp(Ca ) = post(Ca ). For all
other clusters this holds trivially, because each of them have only one transition
and only one post-place, hence the net has distributed choice.
p1 p2
p1 p2
λ(t1 ) = a λ(t2 ) = a
a a a a
p3 p4 p5
c e p3 p4 p5
b d b c d e
Fig. 3. Labelled Free Choice Net Fig. 4. S-cover of the net in Fig. 3
with distributed choice
2.2 Automata and their properties
Definition 10. A sequential system over a set of actions Σi is a finite state
automaton Ai = hPi , →i , Gi , p0i i where Pi are called places, Gi ⊆ Pi are final
places, p0i ∈ Pi is the initial place, and →i ⊆ Pi ×Σi ×Pi is a set of local moves.
Let →ia denote the set of all a-labelled moves in the sequential system Ai . For
a local move t = hp, a, p0 i of →i place p is called pre-place and p0 is called post-
place of t. The language of a sequential system is defined as usual. A set of places
X ⊆ Pi of component Ai having language L we define relativized languages:
x ay
LXa = {xay ∈ L | ∃p in X such that p0 − → p −→ Gi }, P refaX (L) = {x | xay ∈
La }, and Sufa (L) = {y | xay ∈ La }. A set of places X ⊆ Pi of component Ai
X X X
a-bifurcates L if LX a = P refa (L) · a · Sufa (L). These relativized languages
X X
and the property of a-bifurcation was [21] defined for a single place; here we
have generalized those notions to a set of places.
Remark 1. A place p of Ai a-bifurcates Lang(Ai ).
For a place p let a-targets(p)={q | hp, a, qi ∈→i } denote
S the set of its target
places. For a set X of places of Ai define a-targets(X) = p∈X a-targets(p). For
138 PNSE’16 – Petri Nets and Software Engineering
sets of places X and Y of Ai with language L, we define relativized languages:
(X,Y ) x a y
La = {xay ∈ L | ∃p ∈ X and ∃q ∈ Y such that p0 − → p − → q − → Gi },
(X,Y ) (X,Y )
Pref (X,Y
a
)
(L) = {x | xay ∈ La } and Suf (X,Y
a
)
(L) = {y | xay ∈ La }. We
(X,Y ) (X,Y )
say that (X, Y ) a-funnels language L if La = Pref a (L) · a · Suf (X,Y
a
)
(L).
Remark 2. For a set X of places of Ai with language L and a set Y ⊆ a-
targets(X), if X a-bifurcates L then the tuple (X, Y ) a-funnels L.
Using Remark 1 and Remark 2 we get the following corollary.
Corollary 1. Given a place p of Ai and a set Y ⊆ a-targets(p) the tuple (p, Y )
a-funnels L(Ai ).
Let L denote the language a
of automaton shown in Fig-
p2
ure 5. The set X = {p2 , p4 }
a-bifurcates L and the tuple a start p1 a p4 a p5 a p6
(X, {p3 }) a-funnels L. The set
p3
Z = {p1 , p3 } does not a-
bifurcate L because, for the a
word aaaaaa in L, we have Fig. 5. Automaton with Lang((aaa)∗ aaa)
aaa in Suf pa3 (L) (hence in
Suf Z p1 Z
a (L)) and ε in Pref a (L) (so in Pref a (L)), but the word ε · a · aaa ∈
/ L.
We can use the same string to see that (Z, {p1 , p2 }) do not a-funnel L.
2.3 Product Systems
Fix a distribution (Σ1 , Σ2 , . . . , Σk ) of Σ. We define product systems over this.
Definition 11. Let Ai = hPi , →i , Gi , p0i i be a sequential system over alphabet
Σi for 1 ≤ i ≤ k. A product system A over the distribution Σ = (Σ1 , . . . , Σk )
is a tuple hA1 , . . . , Ak i.
Let Πi∈Loc Pi be the set of product states of A. We use R[i] for the projection
of a product state R in Ai . The initial product state of A is R0 = (p01 , . . . , p0k ),
while G = Πi∈Loc Gi denotes the S final states of A. Let ⇒a = Πi∈loc(a) →ia . The
set of all global moves of A is ⇒= a∈Σ ⇒a . Then for a global move g in ⇒a , let
g[i] denote its i-th component–local a-move–belonging to Ai , for all i in loc(a).
Definition 12 ([22]). A product system A is said to have separation of labels
if for all i ∈ Loc, and for all global actions a, if hp, a, p0 i, hq, a, q 0 i ∈→i then p = q.
The product system shown in Figure 6, has separation of labels property.
Definition 13 ([15]). In a product system, we say the local move hp, a, q1 i ∈→i
is conflict-equivalent to the local move hp0 , a, q10 i ∈→j , if for every other local
move hp, b, q2 i ∈→i , there is a local move hp0 , b, q20 i ∈→j and, conversely, for
moves from p0 there are corresponding outgoing moves from p. We call A =
R. Phawade: Kleene Theorem for Labelled Free Choice Nets 139
hA1 , . . . , Ak i a conflict-equivalent product system if for every global action
a ∈ Σ, and for all i, j ∈ loc(a), every a-move in Ai is conflict-equivalent to every
a-move in Aj .
Let globals(a) be a subset of its global moves ⇒a , and a-global denote an
element of globals(a).
Definition 14. A product system with globals is a product system with re-
lations globals(a), for each global action a in Σ.
Now we describe runs of a product system A over some word w by associating
product states with prefixes of w: the empty word is assigned initial product state
R0 , and for every prefix va of w, if R is the product state reached after v and
Q is reached after va where, for all j ∈ loc(a), hR[j], a, Q[j]i ∈→j , and for all
j ∈/ loc(a), R[j] = Q[j]. Runs of a product system with globals, are defined
in the same way where, an additional requirement of Πj∈loc(a) (hR[j], a, Q[j]i ∈
globals(a), has to be satisfied. With abuse of notation sometimes we use pre(a)
a
to denote the set {R | ∃Q, R − → Q}. A run of a product system over word w is
said to be accepting if the product state reached after w is in G. We define the
language Lang(A) of product system A (with globals), as the words on which
the product system (with globals) has an accepting run.
The following property helps us to capture free choice property of nets.
Definition 15. A product system with globals have same source property if,
for any pair of two global moves sharing a common pre-place have the same set
of pre-places.
The product system A shown in Figure 6 has same source, as both the a-
globals in the given globals(a) relation have the same set of pre-places.
start r1 start s1
globals(a) = {
a a
((r1 −
→ r2 ), (s1 −
→ s2 )),
a b a d a
((r1 −
a
→ r3 ), (s1 −
→ s3 ))}.
a c a e
r2 r3 s2 s3
A1 A2
Fig. 6. Product system A = hA1 , A2 i used in Example 3
140 PNSE’16 – Petri Nets and Software Engineering
3 Nets and Product systems
It is easy to give a generic construction of a 1-bounded S-coverable labelled net
system from a product system with globals.
Definition 16 (Product system with globals to Net). Given a product
system A = hA1 , A2 , . . . , Ak i over distribution Σ, we can produce a net system
(N = (S, T, F, λ), M0 , G) as follows:
S
– S = Si Pi , the set of places.
– T = a globals(a), for all actions a in Σ. We also let Ti = {λ−1 (a) | a ∈ Σi }.
– The labelling function λ labels by action a the transitions in globals(a).
– The flow relation F = {(p, g), (g, q) | g ∈ Ta , g[i] = hp, a, qi, i ∈ loc(a)}. Let
Fi be its restriction to the transitions Ti for i ∈ loc(a).
– M0 = {p01 , . . . , p0k }, the initial product state.
– G = G, the set of final product states.
Since, the set of transitions of resultant net is same as the set of moves in
the product system; and construction preserves pre as well as post places, we
get one to one correspondence between reachable states of product system and
reachable markings of nets.
Lemma 1. In the construction of net system N in Definition 16, N is S-
coverable, the construction preserves language, i.e., Lang(N, M0 , G) = Lang(A).
When we apply the generic construction above to product systems, with same
source property, we get a free choice net, because any two global moves having
same set of pre-places are put into one cluster.
Theorem 1. Let (N, M0 , G) be the net system constructed from product system
A as in Definition 16. If A has same source property then N is a free choice net.
Even if a net is 1-bounded and S-coverable each component need not have
only one token in it, but when we say that a 1-bounded net is S-coverable
we assume that each component has one token. For live and 1-bounded free
choice nets, such S-covers can be guaranteed [5]. Now we describe a linear-size
construction of a product system from a net which is S-coverable.
Definition 17 (Net to product system with globals). Given (N, M0 , G) a
1-bounded S-coverable labelled net system, with N = (S, T, F, λ) the underlying
net and Ni = (Si , Ti , Fi ) the components in the S-cover, for i in {1, 2, . . . , k},
we define a product system A = hA1 , . . . , Ak i.
– Pi = Si , p0i the unique state in M0 ∩ Pi .
– →i = {hp, λ(t), p0 i | t ∈ Ti and (p, t), (t, p0 ) ∈ Fi , for p, p0 ∈ Pi }.
– So we get sequential systems Ai = hPi , →i , p0i i and the product system A =
hA1 , A2 , . . . , Ak i over alphabet Σ.
R. Phawade: Kleene Theorem for Labelled Free Choice Nets 141
[
– globals(a) = (Πi∈loc(a) t[i]).
t∈Ta
– G=G
Again we can generalize results obtained in the thesis [19].
Lemma 2. For net N , the construction of the product system A in Definition 17
above preserves language.
For each a-labelled transition of the net we get one global a-move in the
product system having same set of pre-places and post-places. And, by definition
for each global a-move in product system we have an a-labelled transition in the
net having same pre and post-places. This was ensured by “distributed choice”
property [21,19], here now ensured by construction using globals. We get one to
one correspondence between reachable states of product system and reachable
markings of the net we started with. Therefore, if we begin with the free choice
net, we get same source property in the product system obtained.
Theorem 2. Let (N, M0 , G) be a 1-bounded, S-coverable labelled free choice net
system. Then one can construct a product system A with same source property.
Example 3. From the net in Figure 1 using its S-decomposition shown in Fig-
ure 2, we get the product system of Figure 6 for the language of net. In this
example, starting with this product system we get the same net back.
4 Expressions
4.1 Regular expressions and their properties
A regular expression over alphabet Σi such that constants 0 and 1 are not in Σi
is given by:
s ::= 0 | 1 | a ∈ Σi | s1 · s2 | s1 + s2 | s∗1
The language of constant 0 is ∅ and that of 1 is {ε}. For a symbol a ∈ Σi , its
language is Lang(a) = {a}. For regular expressions s1 + s2 , s1 · s2 and s∗1 , its
languages are defined inductively as union, concatenation and Kleene star of the
component languages respectively.
As a measure of the size of an expression we will use wd(s) for its alphabetic
width—the total number of occurrences of letters of Σ in s. We will use syntactic
entities–called derivatives–associated with regular expressions which are known
since the time of Brzozowski [2], Mirkin [16] and Antimirov [1].
For each regular expression s over Σi , let Lang(s) be its language and its
initial actions form the set Init(s) = {a | ∃v ∈ Σi∗ and av ∈ Lang(s) } which can
be defined syntactically. Similarly, we can syntactically check if ε ∈ Lang(s).
Antimirov derivatives [1] are defined as given below.
142 PNSE’16 – Petri Nets and Software Engineering
Definition 18 ([1]). Given regular expression s and symbol a, the set of partial
derivatives of s with respect to a, written Dera (s) are defined as follows.
Dera (0) = ∅
Dera (1) = ∅
Dera (b) = {1} if b = a ∅ otherwise
Dera (s1 + s2 ) = Dera (s1 ) ∪ Dera (s2 )
Dera (s∗1 ) =
Dera (s1 ) · s∗1
Dera (s1 ) · s2 ∪ Dera (s2 ) if ε ∈ Lang(s1 )
Dera (s1 · s2 ) =
Dera (s1 ) · s2 otherwise
Inductively Deraw (s) = Derw (Dera (s)). [
The set of all partial derivatives Der(s) = Derw (s), where Derε (s) = {s}.
w∈Σi∗
We have the Antimirov derivatives Dera (ab + ac) = {b, c} and Dera (a(b + c)) =
{b + c}, whereas the Brzozowski a-derivative [2] (which is used for construct-
ing deterministic automata, but which we do not use in this paper) for both
expressions would be {b + c}.
A derivative d of s with global a ∈ Init(d) is called an a-site of s. An
expression is said to have equal choice if for all a, its a-sites have the same set
of initial actions. For a set D of derivatives, we collect all initial actions to form
Init(D). Two sets of derivatives have equal choice if their Init sets are same.
As in [21] we put together derivatives which may correspond to the same
state in a finite automaton.
Definition 19 ([21]). Let s be a regular expression and L = Lang(s). For a set
D of a-sites of regular expression s and an action a, we define the relativized
language LDa = {xay | xay ∈ L, ∃d ∈ Derx (s) ∩ D, ∃d ∈ Deray (d) with ε ∈
0
D
Lang(d )}, and the prefixes Pref a (L) = {x | xay ∈ LD
0
a }, and the suffixes
Suf D
a (L) = {y | xay ∈ La }. We say that the derivatives in set D a-bifurcate L
D
D
if LD D
a = Pref a (L) · a · Sufa (L).
Let Parta (s) denote a partition of the a-sites of s into blocks such that each
block (that is, element of the partition) a-bifurcates L. Earlier [21] we have given
a syntactic scheme for obtaining a partition, for which we proved the following.
Proposition 1 ([21]). Every block D of the partition P arta (s) a-bifurcates lan-
guage of a regular expression s.
In comparison with our earlier paper [21], the next Definition 20 and Propo-
sition 2 deal with “a-effects”, which are new. In addition to thinking of blocks of
the partition as places of an automaton, we can now think of blocks and their
effects as local moves.
Definition 20. Given an action a, a set of a-sites B of regular expression s
and a specified set of a-effects E ⊆ Dera (B), we define the relativized languages
(B,E)
La = {xay ∈ L | ∃d ∈ Derx (s) ∩ B, ∃d0 ∈ Dera (d) ∩ E, and
∃d00 ∈ Dery (d0 ) with ε ∈ Lang(d00 )}.
R. Phawade: Kleene Theorem for Labelled Free Choice Nets 143
(B,E) (B,E)
Also define the prefixes P refa (L) = {x | xay ∈ La } and the suffixes
(B,E) (B,E)
Sufa (L) = {y | xay ∈ La }. We say that a tuple (B, E) a-funnels L if
(B,E) (B,E)
La = P refaB (L) · a · Sufa (L).
In such a pair (B, E), if B is a block in the Parta (s) and E is a nonempty
subset of a-effects of B, then it is called as an a-duct. For an a-duct (B, E),
we define its set of initial actions Init(B, E) as Init(B, E) = Init(B), call B as
its pre-block and call E as its post-effect. For all i in loc(a) let a-ducts(si )
denote the set of all a-ducts of regular expression si . For any two a-ducts (B, E)
and (B 0 , E 0 ) in a-ducts(si ), define (B, E) = (B 0 , E 0 ) if B = B 0 and E = E 0 .
Example 4. Consider a regular expression p1 = (aaa)∗ aaa. Let L denote the lan-
guage of p1 . The set of all its derivatives is Der(p1 ) = {p1 , p2 = aa(aaa)∗ aaa, p3 =
a(aaa)∗ aaa, p4 = aa, p5 = a, p6 = ε}. All these derivatives are also shown in Fig-
ure 5. The set of a-sites of p1 consist of all its derivatives except expression p6 .
A partition of a-sites of p1 is Parta (p1 ) = {D1 = {p1 }, D2 = {p2 , p4 }, D3 =
{p3 , p5 }}. See that each block in this partition a-bifurcates language L. For tu-
ple (D2 , {p3 }) its set of a-effects is {p3 , p5 }. The tuple (D2 , {p3 }) a-funnels L
therefore it is an a-duct, having D2 as its pre-block and {p3 } as its post-effect.
Another example of an a-duct is (D3 , {p1 }).
Consider the set Z = {p1 , p3 } of derivatives of p1 . This set Z does not a-
bifurcate language L, because for the word aaaaaa in L, we have string aaa
in Suf pa3 (L) (and hence in Suf Z p1
a (L)) and we have string ε in Pref a (L) (and
Z
hence in Pref a (L)), but the word ε · a · aaa is not in L. For set Z, we have
Dera (Z) = {p2 , p4 , p1 }. Considering the same string as above, we can see that
tuple (Z, {p1 , p2 }) do not a-funnel L and is not an a-duct.
Proposition 2. Every a-duct of a regular expression s, a-funnels Lang(s).
We give following remark, using Proposition 2, for singleton set of derivatives.
Remark 3. Let r be an a-site of a regular expression s. It a-bifurcates Lang(s),
and for any of its a-effect E, tuple (r, E) a-funnels Lang(s).
Consider a regular expression s in the context of a distribution (Σ1 , . . . , Σk ),
so that some of the actions are global. The following property of expressions has
been related to an important property of product systems which enables us to
identify places coming from a cluster in the free choice net.
Definition 21 ([21]). If for all global actions a occurring in s, the partition
P arta (s) consists of a single block, then we say s has unique sites.
4.2 Connected expressions
Connected expressions over a distributed alphabet This is the syntax of
connected expressions defined over a distribution (Σ1 , Σ2 , . . . , Σk ) of alphabet Σ.
e ::= 0|fsync(s1 , s2 , . . . , sk ), where si is a regular expression over Σi
144 PNSE’16 – Petri Nets and Software Engineering
Definition 22. A connected expression e = fsync(s1 , s2 , . . . , sk ) over Σ, is said
to have equal choice if, for all global actions a in Σ and i, j in loc(a), for an
a-site r of si and an a-site r0 of sj , Init(r) = Init(r0 ).
A connected expression e = fsync(s1 , s2 , . . . , sk ) over Σ, have unique sites
if, each component regular expression si have unique sites property.
For a connected expression defined over distributed alphabet its derivatives
and semantics were given in [21], are given below. For the connected expression
0, we have Lang(0) = ∅. For the connected expression e = fsync(s1 , s2 , . . . , sk ),
its language is given as Lang(e) = Lang(s1 )kLang(s2 )k . . . kLang(sk ), where
the synchronized shuffle L = L1 k . . . kLk is defined as: w ∈ L iff for all i ∈
{1, . . . , k}, w↓Σi ∈ Li . The definition of derivatives extended to connected ex-
pressions [21] is given as follows. The expression 0 has no derivatives on any
action. Given an expression e = fsync(s1 , s2 , . . . , sk ), its derivatives are de-
fined by induction using the derivatives of the si on action a as, Dera (e) =
{fsync(r1 , . . . , rk ) | ∀i ∈ loc(a), ri ∈ Dera (si ); otherwise rj = sj }.
Connected expressions with cables We now define some properties of con-
nected expressions over a distribution. These extend the notion of pairing given
earlier, and will ultimately lead us to construct free choice nets without dis-
tributed choice.
Definition 23. Let e = fsync(s1 , s2 , . . . , sk ) be a connected expression over Σ.
For each action a in Σ, we define the set a-cables(e) = Πi∈loc(a) a-ducts(si ).
For an action a, an a-cable is an element of the set a-cables(e). A block
B of Parta (si ) appears in an a-cable D if there exists j in loc(a) and Y ⊆
Dera (B), such that D[j] = (B, Y ). For any a-cable D its set of pre-blocks is
•
D = ∪i∈loc(a) {Bi | Bi appears in D}.
For expression e, let cables(a) ⊆ a-cables(e), such that for all i in loc(a): (1) for
all (B, E) in a-ducts(si ), there exists an a-cable D in cables(a) and location j
in loc(a), such that D[j] = (B, E) (2) for all (B, E) and (B 0 , E 0 ) in a-ducts(si )
with (B, E) 6= (B 0 , E 0 ), if B = B 0 then E ∩ E 0 = ∅.
A connected expression with cables is a connected expression with relations
cables(a) of it, for each global action a in Σ.
For connected expressions with cables, its derivatives are defined as:
Definition 24. The connected expression 0 has no derivatives on any action.
For expression e = fsync(s1 , s2 , . . . , sk ), we define its derivatives on action a, by
induction, using a-ducts and the derivatives of sj as:
Dera (e) = {fsync(r1 , r2 , . . . , rk ) | rj ∈ Dera (sj ) if there exists an a-cable D in
cables(a) such that, for all j in loc(a), sj is in pre-block Bj and rj is in Xj of
a-duct D[j] = (Bj , Xj ) of sj , otherwise rj = sj }.
For expressions d = fsync(r1 , . . . , rk ) we use d[i] for ri . Define Init(d) = {a ∈
Σ | Dera (d) 6= ∅}. If a ∈ Init(d) we call d an a-site. The reachable derivatives
are Der(e) = {d | d ∈ Derx (e), x ∈ Σ ∗ }.
R. Phawade: Kleene Theorem for Labelled Free Choice Nets 145
Language of e is the set of words over Σ defined using derivatives as below.
Lang(e) = {w ∈ Σ ∗ | ∃e0 ∈ Derw (e) such that ε ∈ Lang(ri ), where e0 [i] = ri }.
So we can have next derivative on action a, if it is allowed by the cables(a)
relation. This is different from derivatives defined previously [21], when it is
necessary to take derivatives of all component regular expressions having a in
its alphabet. The number of derivatives can be exponential in k.
Definition 25. A connected expression have equal source property if for any
pair of two cables sharing a common pre-block have same set of pre-blocks.
Example 5. Let e = fsync(r1 , s1 ) be a connected expression defined over dis-
tributed alphabet Σ = (Σ1 = {a, b, c}, Σ2 = {a, d, e}), where, r1 = ((ab +
ac)(ab + ac))∗ and s1 = (((ad + ae)(ad + ae))∗ . Derivatives of components are
Der(r1 ) = {r1 , r2 = b(ab+ac)r1 , r3 = c(ab+ac)r1 , r4 = (ab+ac)r1 , r5 = br1 , r6 =
cr1 , } and Der(s1 ) = {s1 , s2 = d(ad + ae)s1 , s3 = e(ad + ae)s1 , s4 = (ad +
ae)s1 , s5 = ds1 , s6 = es1 , }. Partitions are Parta (r1 ) = {r1 , r4 } and Parta (s1 ) =
{s1 , s4 }. A set cables(a) = {d1 = ((r1 , r2 ), (s1 , s2 )), d2 = ((r1 , r3 ), (s1 , s3 )), d3 =
((r4 , r5 ), (s4 , s5 )), d4 = ((r4 , r6 ), (s4 , s6 ))}. See that each a-duct appears at least
once in this relation, and for two a-ducts d1 [1] and d2 [1] of r1 , with the same
pre-block r1 , their set of post-effects {r2 } and {r3 } are disjoint, and similarly
for a-ducts d3 [1] and d4 [1] of r1 , with the same pre-block r4 , their sets of post-
effects {r5 } and {r6 } are disjoint. Similarly this condition holds for a-ducts of
s1 . This expression do not have unique sites, as its componet expressions do not
have it. It has equal source property as • d1 = • d2 = {r1 , s1 } and • d3 = • d4 =
{r4 , s4 }. We have Dera (e) = {f sync(r2 , s2 ), f sync(r3 , s3 )}, but f sync(r2 , s3 ) is
not in Dera (e). Simplifying notation, the set of reachable derivatives is Der(e) =
{(r1 , s1 ), (r2 , s2 ), (r4 , s2 ), (r2 , s4 ), (r4 , s4 ), (r3 , s3 ), (r4 , s3 ), (r3 , s4 ), (r5 , s5 ), (r6 , s6 ),
(r5 , s1 ), (r1 , s5 ), (r6 , s1 ), (r1 , s6 )}.
5 Connected Expressions and Product Systems
In this section we prove two main theorems of the paper. For obtaining a con-
nected expression from a product system with globals defined over a distributed
alphabet, we go through an intermediate product system defined over a new
distributed alphabet, get a language equivalent intermediate expression defined
over this new alphabet using results from [22] and then finally rename this to
get an expression for language of original product system. To obtain a product
system from a connected expression we use above steps in the reverse direction.
We refer the reader to [20] for detailed proofs of Lemma 4, Lemma 6, Theorem 3.
5.1 Analysis of Expressions from Systems
In this section we produce expressions for our systems using a result from [22].
146 PNSE’16 – Petri Nets and Software Engineering
Lemma 3 ([22]). Let A be a product system with separation of labels. Then we
can compute a connected expression for the language of A, where every regular
expression has unique sites. If the product was conflict-equivalent, the constructed
expression has equal choice.
The Lemma 4, allows us to relate product systems with globals having sep-
aration of labels property defined over a distribution to connected expressions
with cables having unique sites property.
Before giving a formal proof, we present the key idea behind it. Let Ai be a
sequential automaton having an a-move (p, a, q) where a is a global action. Let
s be a regular expression for the language of Ai . Our aim is to get an a-duct
(Bp , a, Bq ) for a-move (p, a, q), where Bp is the set of derivatives of expression
s, which corresponds to place p and, similarly Bq is the set of derivatives which
corresponds to place q. If Ai has separation of labels property, then we know that
p is the unique place having outgoing a-moves in the automaton. Hence, we can
apply Lemma 3 and get the set Bp as required. Now we turn to get Bq for place
q. If q has an outgoing c-move for some global action c, then our task becomes
easy and we can apply Lemma 3 to get Bq . If c is not a global action then we
can not apply Lemma 3 directly because there might be many other places like q
which may have outgoing c-moves. Therefore, in order to make use of Lemma 3
we need to make q as a unique place. This we do so by changing alphabet of Ai in
the following way. If hq, c, ri was a c-move in Ai then we rename c by cq and we
have local move hq, cq , ri in this new automaton A0i defined over a new alphabet
and let expression s0 denote language of A0i . Now q is a unique place having
outgoing cq -moves and we can apply Lemma 3 to get a set of derivatives Bq0
of expression s0 which corresponds to place q in A0i . Now we rename back these
derivatives in Bq0 to get the set Bq which is a subset of Der(s), and corresponds to
the place q in the original automaton Ai . To show that a-move (p, a, q) is indeed
captured by (Bp , a, Bq ), we need prove that a word xay accepted by automaton
and passing through p and q should also pass through derivatives belonging to
these sets, and the reverse of this should also hold.
Lemma 4. Let Σ be a distributed alphabet. Let A be a product system over Σ
with globals, having separation of labels and same source property. Then we can
compute a connected expression e with cables for the language of A, which has
unique sites and equal source property. Moreover, for each global action a in Σ,
we produce an a-duct for each local a-move; and, one a-cable of expression e for
each global a-move of product A.
Proof. Let A = hA1 , . . . , Ak i be the given product system. The separation of
labels property of A ensures that for a global action a, and for each i in loc(a),
we have a unique place in Ai having outgoing local a-moves; but it may have
multiple places having outgoing c-moves for some local action c of Σi . And, same
source property of A ensures that these places can not have any outgoing a-move
for any global action a.
Stage 1 of proof: Now, for all local actions c in Σi , we replace each local
c-move hq, c, ri of component Ai by cq -move hq, cq , ri to get new alphabet Γi
R. Phawade: Kleene Theorem for Labelled Free Choice Nets 147
and new sequential system Hi over it. Repeating this for each sequential system
Ai we get a new product system H = hH1 , . . . , Hk i over distributed alphabet
Γ = (Γ1 , . . . , Γk ). For each global action a, the relation global(a) of product A,
remains same for product H.
Since a local action is renamed on basis of the source place of the local move
of which it is part of, this renaming is well defined. For any word w0 in Lang(Hi )
we get a unique word w in Lang(Ai ) by renaming back local action cq in w0 by
c. And in the reverse direction, for any w in Lang(Ai ) we can replace a local
action c by cq using the run of Ai on w (in the case that Ai is at place q and
some local c-move hq, c, ri is used), so this word w0 is unique. See that Γi and Σi
have same set of global actions and they differ only in local actions they have.
Therefore, for any word u0 in Lang(H) we get a unique word u in Lang(A) by
renaming local actions cq of u0 to u.
For each local action cq of Γi we have a unique place q in Hi having outgoing
cq -moves; thus, for action c (action c could be global or local) of Γi we have
one unique place in Hi having outgoing c-moves. Also, for each place of Hi we
have an action –local or global– such that the place has outgoing local moves on
that action. The product H has separation of labels property in a more general
way, as even local actions have unique places for them now; and, it has same
source property since product A has it. Since product system H has both these
properties, it is conflict-equivalent.
Stage 2 of proof: Now we can apply Lemma 3, to get a connected ex-
pression e0 = (s01 , . . . , s0k ) over alphabet Γ for language of product H and it has
unique sites property. Hence, for each (local or global) action c in Γi we have only
one block in Partc (s0i ). If place p has outgoing local a-moves hp, a, qi and hp, a, ri
in Hi , with place q having outgoing local c-moves and place r having outgoing
local d-moves; then by application of Lemma 3, we would get unique blocks
Bp0 , Bq0 , and Br0 in Parta (s0i ), Partc (s0i ) and Partd (s0i ) respectively. And each of
these blocks bifurcate Lang(s0i ). We know that the sets Bq0 and Br0 of a-effects of
block Bp0 are disjoint and their Init sets are also disjoint. Therefore, by Propo-
sition 2 each a-duct (Bp0 , Bq0 ) of s0i a-funnels Lang(s0i ).
To show the correspondence between local a-move hp, a, qi and the a-duct
(p,q) (B 0 ,Bq0 )
(Bp0 , Bq0 ) obtained as above, we need to prove that La = La p . As (p, q)
(p,q)
and (Bp0 , Bq0 ) both a-funnel language L, hence La = Pref pa (L) · a · Suf (p,q)
a (L)
0 0 0 0 0
(Bp ,Bq ) Bp (Bp ,Bq )
and La = Pref a (L) · a · Suf a (L). Since place p, as well as block Bp0 ,
B0
a-bifurcates L, we have Pref pa (L) = Pref a p (L). Therefore, it is sufficient to prove
(B 0 ,B 0 )
the equivalence Suf (p,q)a (L) = Suf a p q (L). Consider a word y in Suf (p,q) a (L)
but we have y = cq y 0 as q is the only place having outgoing cq moves. Therefore
y 0 is in Suf qa (L) and since q, as well as block Bq0 , cq -bifurcates L we have y 0
0
in Suf B q p
a (L) also. But we also have word y = cy in Suf a (L) and, hence y in
0
0 0 0
B (B ,B )
Suf a p (L). Therefore, we have cy 0 in Suf a p q (L) as required.
Hence for each local a-move (p, a, q) of sequential system Hi we have an a-
duct (Bp0 , Bq0 ) of regular expression s0i . Therefore, for each a-global of product
148 PNSE’16 – Petri Nets and Software Engineering
H we get an a-cable of connected expression e0 by taking tuple of a-ducts corre-
sponding to its component a-moves. Since product H has same source property
expression e0 has equal source property.
Stage 3 of proof: Now we rename back each local action cq by c in each of
s0i to get regular expression si over alphabet Σi . See that we had not renamed
any global action of Σ, and for such local action cq its set of locations loc(cq ) is
singleton. Hence we continue to have unique sites property for all global actions a.
Repeating this for each regular expression s0i in expression e0 , we get a connected
expression e = (s1 , . . . , sk ) over distributed alphabet Σ, having unique sites
property. Since expression e0 has equal source property expression e continues
to have it.
Now we prove the claim that renaming a derivative of s0i in this fashion, we
get derivative of si . For the base case si is obtained by renaming s0i (the fact
that ε is in Lang(s0i ) iff ε is in Lang(si ), can be proved by structural induction
on si ). Consider a word w0 = x0 ay 0 in Lang(s0i ). So there exist derivatives d0 in
Derx0 (s0i ), and r0 in Derx0 a (s0i ), and s0f in Dery0 (r0 ) such that ε is in Lang(s0f ). By
induction hypothesis we have derivative d of si obtained by renaming d0 . If action
a is global then Init(d) = Init(d0 ) and if it is local action then Init(d) is obtained
by renaming Init(d0 ). To complete the induction step, we need to prove that r is
in Derxa (si ), where x is obtained by renaming word x0 . By induction hypothesis,
derivative d is in Derx (si ), therefore it suffices to prove that derivative r, the
word obtained by renaming back r0 , is in Dera (d). This is done by structural
induction on d0 .
As a consequence of above claim, for any word w0 in Lang(s0i ) we have a
unique word w in Lang(s0i ) obtained by renaming back. In the reverse direction
also, for any w in Lang(s0i ) we get a unique word w0 in Lang(s0i ). We extend this
renaming to a set of derivatives; so for a set of derivatives B 0 ⊆ Der(s0i ) we get
the set B ⊆ Der(si ), and vice versa.
The set Xq0 of a-effects of block Bp0 , might have been a unique block of
Partcq (s0i ), but after renaming, it might not c-bifurcate Lang(si ). On the other
hand, since Bp a-bifurcates Lang(si ), pair (Bp , Xq ) of si continues to a-funnel
Lang(si ) and therefore is an a-duct of si . Hence, for each a-duct (Bp0 , Xq0 ) of s0i
we get an a-duct (Bp , Xq ) of si . As a consequence, for each a-cable of e0 we get
an a-cable of expression e.
So, for each action hp, a, qi we get an a-duct (Bp , Xq ), and for each a-global
we get an a-cable obtained by taking product of a-ducts corresponding to its
component local a-moves. Therefore, for any word u0 in Lang(e0 ) we get a unique
word u in Lang(e) and for any word v in Lang(e) we get a unique word v 0 in
Lang(e0 ). Now using equivalence Lang(H) = Lang(e0 ) along with the fact that,
the renaming used in the first step of getting product system H from A, and the
renaming used in the last step of getting expression e from e0 is well defined, we
get language equivalence of expression e and product system A. t
u
Now we use Lemma 4 to get expressions for the product systems with globals.
R. Phawade: Kleene Theorem for Labelled Free Choice Nets 149
Theorem 3. Let A be a product system with globals, having same source prop-
erty, defined over Σ. Then for the language of A, we can compute a connected
expression with cables, having equal source property.
Proof Sketch. Given product system A = hA1 , . . . , AK i may not have sepa-
ration of labels property, i.e. for a global action a, a component Ai may have
many places with outgoing local a-moves. Using globals we rename local a-moves
appropriately across all such component Ai ’s, to get a new product system H
having separation of labels property over a new distributed alphabet. Then we
apply Lemma 4 to get an expression for product H, which is renamed back to
get an expression for the language of A. t
u
5.2 Synthesis of Systems from Expressions
Using the construction of Antimirov [1], which in polynomial time gives us a finite
automaton of size O(wd(s)) for a regular expression s using partial derivatives
as states, we produce product automata for our expressions.
Lemma 5 ([22]). Let e be a connected expression with unique sites. Then there
exists a product system A with separation of labels accepting Lang(e) as its
language. If e has equal choice, then A is conflict-equivalent.
We use Lemma 5 to prove Lemma 6, which allows us to interrelate connected
expressions with cables defined over a distribution and connected expression
defined over a distributed alphabet.
Lemma 6. Let Σ be a distributed alphabet. Let e be a connected expression with
cables, having equal source property and unique sites. Then we can compute a
product system with globals for Lang(e), and having separation of labels along
with same source property. Moreover, for each a in Σ, for each a-duct we produce
one local a-move. And, for each a-cable we get one global a-move of A.
Proof Sketch. Consider a global action a and a location i in loc(a). For an
a-cable d we construct an a-global by giving a local a-move, for each a-duct
d[i] = (B, X) of si . Since B is a block in Parta (si ), we get a unique place p for
it using a-bifurcation, but X may not be a block and there may exist another
a-effect Y of B (so (B, Y ) can be a component of another a-cable d0 ), so we can
not use bifurcation directly to get a place for X. Here we employ the trick of
renaming X to X 0 so that X 0 is a block. Take a local action c in Init(X). As X
and Y are disjoint, each distinct occurrence of c in si corresponds to either X
or Y , so we rename each occurrence of c by cX to get s0i over a new alphabet Γi0 ,
and similarly X 0 from X, and B 0 from B. This renaming is well-defined. Now
X 0 is a block in the PartcX (s0i ). We construct A0i from s0i , where we get a unique
place q for X 0 also, therefore we get a local move (p, a, q) corresponding to a-duct
(B 0 , X 0 ) of s0i . Renaming back cX to c in A0i to get Ai over Σi , for language of
si , we get a local a-move (p, a, q) in Ai corresponding to a-duct (B, X). t
u
Next we present construction of products with globals having same source
property from connected expressions with cables, having equal source property.
150 PNSE’16 – Petri Nets and Software Engineering
Theorem 4. Let e be a connected expression with cables, having equal source
property, defined over Σ. Then for the language of e, we can compute a product
system with globals having same source property.
Proof. Given connected expression e may not have unique sites property. So
first, we use cables of e to do the appropriate renaming to get an expression e0
with cables, over a new alphabet Σ 0 , and having unique sites property. Now we
can apply Lemma 6 on e0 to get a product A0 with globals and having separation
of labels property, for its language. In the last part, we rename back the local
moves in A0 to get a product A with globals for the language of expression e.
Since expression e has equal source property, the set of cables(a) can be
partitioned into buckets such that two a-cables belong to a bucket iff they have
same set of pre-blocks. Because of same source property of expression e, an a-
duct can appear as a component of many a-cables belonging to same bucket. But
it can not be a component of two a-cables belonging to two different buckets.
Without loss of generality assume that loc(a) = {1, . . . , l}. Let (B1 , . . . , Bl ) be
the pre-tuple of a-cables of bucket Z of the partition of cables(a). For each i
in loc(a), replace each occurrence of letter a in expression si , corresponding to
Init(Bi ) by aZ , to get an expression s0i over alphabet Σi0 .
So we get connected expression e0 = (s01 , . . . , s0k ) over distributed alphabet
Σ = (Σ10 , . . . , Σk0 ). This expression has unique sites property, and continues to
0
have equal source property. Each a-duct of si , corresponds to some aZ -duct of
s0i , and each a-cable to some aZ -cable of e0 . Note that there might be many
aZ -cables .
For language of e0 , we get product system A0 = hA01 , . . . , A0k i by applying
Lemma 6 over distributed alphabet Σ 0 having separation of labels. For each aZ -
duct we get an aZ -move and for each aZ -cable we get an aZ -global in A0 . It has
same source property since e0 had equal source property.
Replacing each local action hp, aZ , qi of A0i by hp, a, qi we get Ai , for each i
in loc(a). We repeat this for all global actions, to get product system A over Σ.
Hence, for each aZ -global of system H, we get an a-global for system A, which
continues to have same source property. Since renamings are well defined in first
and last part of the proof we get that Lang(e) = Lang(A). t
u
Example 6. Consider the connected expression e = f sync(r1 , s1 ) of Example 5.
A cables(a) relation for e is A set cables(a) = {d1 = ((r1 , r2 ), (s1 , s2 )), d2 =
((r1 , r3 ), (s1 , s3 )), d3 = ((r4 , r5 ), (s4 , s5 )), d4 = ((r4 , r6 ), (s4 , s6 ))}. As shown in
Example 5, expression e equal source, and it does not have unique sites property.
In the construction, a-cables d1 and d2 are put into one bucket z1 and and d3
and d4 are put into bucket z2 . So the renamed expression is e0 = f sync(((a1 b +
a1 c)(a2 b+a2 c))∗ , ((a1 d+a1 e)(a2 d+a2 e))∗ ). This expression has unique sites. See
that each a-duct also gets renamed, for example after renaming a-duct (r1 , r2 )
becomes an a1 -duct (r10 , r20 ) and a-duct (s4 , s5 ) becomes an a2 -duct (s04 , s05 ),
so on. So we have two sets of cables now for two global actions a1 and a2 :
cables(a1 ) = {d01 = ((r10 , r20 ), (s01 , s02 )), d02 = ((r10 , r30 ), (s01 , s03 ))} and cables(a2 ) =
{d03 = ((r40 , r50 ), (s04 , s05 )), d04 = ((r40 , r60 ), (s04 , s06 ))}. Now applying Lemma 6 we get
R. Phawade: Kleene Theorem for Labelled Free Choice Nets 151
start r1 start s1 globals(a1 ) = {
a1 a1
((r1 −→ r2 ), (s1 −→ s2 )),
1 1
a a a1 a1
a1 a1 ((r1 −→ r3 ), (s1 −→ s3 ))}.
b r2 r3 d s2 s3 globals(a2 ) = {
c e a2 a2
b d ((r4 −→ r5 ), (s4 −→ s5 )),
c e a2 a2
((r4 −→ r6 ), (s4 −→ s6 ))}.
r4 s4
a2 a2
a2 a2
r5 r6 s5 s6
A01 A02
Fig. 7. Product system A0 = hA01 , A02 i used in Example 6
a product system which has separation of labels and same source property. So
for the a1 -duct (r10 , r20 ) we get an a1 -move (r10 , a1 , r20 ) and for a2 -duct (s04 , s05 )
we get an a2 -move (s04 , a2 , s05 ), and so forth, in the constructed A0i , where i in
{1, 2}. This intermediate product system with globals is shown in Figure 7. Now
renaming back a1 and a2 by action a in A0i s we get product system A = hA1 , A2 i
for language of e. In this example starting with this product system A, using
Theorem 3, we get the same expression back.
6 Conclusion
We use Theorem 2 and Theorem 3 to get an expression for a labelled 1-bounded
and S-coverable free choice net. The size of the intermediate product system is
linear in the size of net and size of the expression can be exponential in the
size of product system. This exponential blow up in the size is expected because
a component regular expression obtained from the corresponding component
automaton can be of exponential size [9].
Using Theorem 4 and Theorem 1 we obtain labelled free choice nets from
expression with cables and equal source property. The size of the intermediate
product system is linear in the size of connected expression, as size of each com-
ponent automaton obtained using Antimirov derivatives is linear in the size of
component regular expression [1]. The size of net obtained is linear in the size of
product system with globals. Previously [21], resultant net can have exponential
number of transitions in the size of product system.
As a next step in this direction, we want to work with free choice nets which
are labelled, where labels may not come from a distributed alphabet.
152 PNSE’16 – Petri Nets and Software Engineering
References
1. Antimirov, V.: Partial derivatives of regular expressions and finite automaton con-
structions. Theoret. Comp. Sci. 155(2), 291–319 (1996)
2. Brzozowski, J.A.: Derivatives of regular expressions. J. ACM 11(4), 481–494 (1964)
3. Cheng, A., Esparza, J., Palsberg, J.: Complexity results for 1-safe nets. Theor.
Comput. Sci. 147(1&2), 117–136 (1995)
4. Desel, J.: A proof of the rank theorem for extended free choice nets. In: Application
and Theory of Petri Nets. pp. 134–153 (1992)
5. Desel, J., Esparza, J.: Free choice Petri nets. Cambridge University Press, New
York, USA (1995)
6. Esparza, J., Silva, M.: A polynomial-time algorithm to decide liveness of bounded
free choice nets. Theoret. Comp. Sci. 102(1), 185–205 (1992)
7. Garg, V.K., Ragunath, M.: Concurrent regular expressions and their relationship
to petri nets. Theoret. Comp. Sci. 96(2), 285–304 (1992)
8. Grabowski, J.: On partial languages. Fund. Inform. IV(2), 427–498 (1981)
9. Gruber, H., Holzer, M.: Finite automata, digraph connectivity, and regular expres-
sion size. In: ICALP(2). pp. 39–50 (2008)
10. Hack, M.H.T.: Analysis of production schemata by Petri nets. Project Mac Report
TR-94, MIT (1972)
11. Hopcroft, J.E., Motwani, R., Ullman, J.D.: Introduction to automata theory, lan-
guages, and computation - international edition (2. ed). Addison-Wesley (2003)
12. Kleene, S.C.: Representation of events in nerve nets and finite automata. In: Au-
tomata studies. pp. 3–41. Princeton (1956)
13. Kozen, D.: A completeness theorem for kleene algebras and the algebra of regular
events. Inf. Comput. 110(2), 366–390 (1994)
14. Lodaya, K.: Product automata and process algebra. In: SEFM. pp. 128–136. IEEE
(2006)
15. Lodaya, K., Mukund, M., Phawade, R.: Kleene theorems for product systems. In:
DCFS, Proceedings. LNCS, vol. 6808. Springer (2011)
16. Mirkin, B.G.: An algorithm for constructing a base in a language of regular ex-
pressions. Engg. Cybern. 5, 110–116 (1966)
17. Mukund, M.: Automata on distributed alphabets. In: D’Souza, D., Shankar, P.
(eds.) Modern Applications of Automata Theory. World Scientific (2011)
18. Phawade, R.: Direct product representation of labelled free choice nets. Int. J.
Comp. Appl. 99(16), 1–8 (2014)
19. Phawade, R.: Labelled Free Choice Nets, finite Product Automata, and Expres-
sions. Ph.D. thesis, Homi Bhabha National Institute (2015)
20. Phawade, R.: Kleene theorem for labelled free choice nets without distributed
choice. Tech. rep., Indian Institute of Technology Bombay (2016), https://www.
cse.iitb.ac.in/internal/techreports/reports/TR-CSE-2016-79.pdf
21. Phawade, R., Lodaya, K.: Kleene theorems for labelled free choice nets. In: Proc.
PNSE. CEUR Workshop Proceedings, vol. 1160, pp. 75–89. CEUR-WS.org (2014)
22. Phawade, R., Lodaya, K.: Kleene theorems for synchronous products with match-
ing. Trans. on Petri nets and other models of concurrency X, 84–108 (2015)
23. Salomaa, A.: Two complete axiom systems for the algebra of regular events. J.
ACM 13(1), 158–169 (1966)
24. Thiagarajan, P., Voss, K.: In praise of free choice nets. In: European Workshop on
Applications and Theory in Petri Nets. pp. 438–454 (1984)
25. Zielonka, W.: Notes on finite asynchronous automata. Inform. Theor. Appl. 21(2),
99–135 (1987)