=Paper=
{{Paper
|id=Vol-2138/paper4
|storemode=property
|title=Kleene Theorems for Free Choice Nets Labelled with Distributed Alphabets
|pdfUrl=https://ceur-ws.org/Vol-2138/paper4.pdf
|volume=Vol-2138
|authors=Ramchandra Phawade
|dblpUrl=https://dblp.org/rec/conf/apn/Phawade18
}}
==Kleene Theorems for Free Choice Nets Labelled with Distributed Alphabets==
https://ceur-ws.org/Vol-2138/paper4.pdf
Kleene Theorems for Free Choice Nets Labelled
with Distributed Alphabets
Ramchandra Phawade
Indian Institute of Technology Dharwad, Dharwad 580011, India
Email: prb@iitdh.ac.in
Abstract. We provided [15] expressions for free choice nets having “dis-
tributed choice property” which makes the nets “direct product” repre-
sentable. In a recent work [14], we gave equivalent syntax for a larger class
of free choice nets obtained by dropping “distributed choice property”.
In both these works, the classes of free choice nets were restricted by a
“product condition” on the set of final markings. In this paper we do away
with this restriction and give expressions for the resultant classes of nets
which correspond to free choice “synchronous products” and “Zielonka
automata”. For free choice nets with distributed choice property, we give
an alternative characterization which uses properties checkable in poly-
nomial time.
Free choice nets we consider are 1-bounded, S-coverable, and are labelled
with distributed alphabets, where S-components of the associated S-cover
respect the given alphabet distribution.
1 Introduction
There are several different notions of acceptance to define languages for labelled
Petri nets, depending on restrictions on labelling and “final” markings [12]. The
language of a net with an initial marking and a finite set of final markings, is
called L-type language [7]. One goal of this work is to give syntax of expressions
for L-type languages for various subclasses of 1-bounded, free choice nets labelled
with distributed alphabets. One advantage of using distributed alphabet is that
we can see free choice nets as products of automata [11], enabling us to write
expressions for the nets using components. This also enables us to compare
expressiveness of nets and products of automata. We construct expressions for
L-type languages of free choice nets via “free choice Zielonka automata”.
Consider the net N of Figure 1 with G = {{r1 , s1 }, {r2 , s2 }} as its set of final
markings, with its decomposition into finite state machines in Figure 2. Because
this net is decomposable, its markings can be written in tuple form, where each
s-component has a place in the tuple: for example G = {(r1 , s1 ), (r2 , s2 )}. For the
final marking {(r1 , s1 )}, its language is expressed as fsync((ab + ac)∗ , (ad + ae)∗ ).
Similarly, for the final markings {(r2 , s2 )} equivalent expression is fsync((ab +
ac)∗ a, (ad + ae)∗ a). In general, if the places involved in the final markings form
a “product ”, then its language is specified by taking product of component
expressions, using “free choice Zielonka automata with product-acceptance” [15]
78 PNSE’18 – Petri Nets and Software Engineering
r1 s1
r1 s1
a 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
as intermediary. Even though r1 and s2 participate in final markings, marking
{r1 , s2 } does not belong to G, hence set G do not form a product. The language L
of net system (N, G) can be described by, fsync((ab+ac)∗ , (ad+ae)∗ )+fsync((ab+
ac)∗ a, (ad+ae)∗ a). The key idea is ability to express the language of net as union
of language of nets having product condition on final set of markings. This closure
under union may not be always possible for restricted classes of languges defined
over a distributed alphabet. For example, union of “direct product” languages
L1 = {ca, cb} and L2 = {caa, cbb} defined over Σ1 = {c, a} and Σ2 = {c, b}
respectively, is not expressible as a “direct product language”. But this language
is accepted by “synchronous products”: the direct products extended with subset-
acceptance.
For the restricted class of direct product representable free choice nets, with
its set of final markings having product condition-we gave expressions via prod-
uct systems with matchings and product-acceptance [15, 16]. As a second goal,
we develop syntax for free choice nets with distributed choice, now extended
with subset-acceptance. For a net in this class also, its language can be ex-
pressed as union of languages accepted by product system with matchings and
product-acceptance. This union is accepted by product systems with matching
and extended with subset-acceptance (“free choice synchronous products”). As a
third contribution, we develop an alternate characterization of this class of nets,
via “free choice Zielonka automata with product-moves”.
Language equivalent expressions for 1-bounded nets have been given by
Grabowski [5], Garg and Ragunath [4] and other authors [8], where renaming
operator has been used in the syntax to disambiguate synchronizations. We have
chosen to not use this operator and to also exploit the S-decompositions of nets.
The syntax for smaller sublclasses of nets such “marked graphs” and “free choice
nets with initial markings as feedback vertex set” has been given earlier [9, 13].
Rest of the paper is organized as follows. In the next section, we begin with
preliminaries on distributed alphabets and nets. In Section 3 we define product
systems with globals and subset-acceptance, and show that their languages can
be expressed as union of languages accepted by product systems with globals and
product-acceptance. The following section relates these product systems to nets.
In Section 5 we develop syntax of expressions for product systems with subset
Phawade et.al.: Kleene Theorems for Labelled Free Choice Nets 79
acceptance, and next section establishes the correspondence between various
classes of product systems and expressions. In last section we conclude, with a
overview of established correspondences between all three formalisms.
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 ∈/ ∆.
Given languages L1 , L2 , . . . , Lm , their synchronized shuffle L = L1 k . . . kLm is
defined as: w ∈ L iff for all i ∈ {1, . . . , m}, w↓Σi ∈ Li .
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.
A global action is global in the locations in which it occurs. For a set S let ℘(S)
denote the set of all its susbets. For singleton sets like {p}, sometimes we may
write it as p.
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}.
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.
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 produce the new marking M 0 = (M \• t)∪t •
t λ(t)
− M 0 or M −−→ M 0 .
and, we write this as M →
80 PNSE’18 – Petri Nets and Software Engineering
A firing sequence λ(t1 )λ(t2 ) . . . is defined by composition of labels of tran-
t1 t2
sition sequence t1 t2 . . . fired from M0 i.e., M0 −→ M1 −→ . . . . In such a firing
sequence, we say that Mj is reachable from Mi , for every i ≤ j. 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 −
→ M, for some M ∈ G}.
Net Systems and its components Here we define components of net. Our
notion of component does not require strong connectedness and so it is different
from notion of S-component in [3], and therefore our notion of S-cover also
differs from theirs.
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 [3]),
– 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.
Fix a distribution (Σ1 , Σ2 , . . . , Σk ) of Σ. We define s-decomposition [6] of a
net into sequential components.
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 . We give below
the “product” condition on the set of final markings of a net system which is
known [17, 11] to restrict classes of languages.
Definition 7. An S-decomposable labelled net system with product-acceptance
(N, M0 , G) is an S-decomposable labelled net N = (S, T, F, λ) with an initial
marking M0 and a set of markings G ⊆ ℘(S), which is a 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).
Phawade et.al.: Kleene Theorems for Labelled Free Choice Nets 81
2.2 Free choice nets and their properties
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].
The set of all a-labelled transitions along with places r1 and s1 form a cluster
of the net shown in Figure 4.
Definition 8 (Free choice nets [3]). 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
t∈Ca
the 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 from [16, 15] provides the way to direct product representability.
Definition 9 (distributed choice property). An S-decomposable free choice
net N = (S, T, F, λ) is said to have distributed choice property (DCP) if, for all
a in Σ and for all free choice clusters C of N , postdecomp(Ca ) ⊆ post(Ca ).
r1 s1
r1 s1
a a a a
a a a a a a a a
r2 r3 s2 s3 r2 s2
r3 s3
b c d e
b c d e
Fig. 3. Labelled Free Choice Net Fig. 4. S-cover of the net in Fig. 3
system with distributed choice
Example 1 (Free choice net system without distributed choice and having product-
acceptance). Consider a distributed alphabet Σ = (Σ1 = {a, b, c}, Σ2 = {a, d, e})
and the labelled net system N shown in Figure 1 and labelled over Σ. Its (only
82 PNSE’18 – Petri Nets and Software Engineering
possible) 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. 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 )} so 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.
With the set of final markings {(r1 , s1 ), (r1 , s2 ), (r2 , s1 )(r2 , s2 )} satisfying
product condition, the language Lp accepted by this net system is r∗ [ε + a +
ab + ad] where r = (a(bd + db) + a(ce + ec)).
Example 2 (Free choice net system without distributed choice and not satisfy-
ing product condition of the set of final markings). Consider the net system of
Example 1 whose underlying net is shown in Figure 1. With set of final mark-
ings {(r1 , s1 ), (r2 , s2 )}, which do not satisfy product condition, the language Ls
accepted by this net system is r∗ [ε + a] where r = (a(bd + db) + a(ce + ec)).
Example 3 (A net with distributed choice property and product acceptance con-
dition). Consider the labelled net system (N, (r1 , s1 ), G)) of Figure 3, defined
over distributed alphabet Σ = (Σ1 = {a, b, c}, Σ2 = {a, d, e}), and where
G = {(r1 , s1 ), (r1 , s2 ), (r2 , s1 ), (r2 , s2 )} is the set of final markings satisfying
product condition. Its two S-components with sets of places S1 = {r1 , r2 , r3 }
and S2 = {s1 , s2 , s3 }, are shown in Figure 4. For cluster C of r1 , we have Ca =
{t1 , t2 , t3 , t4 }, Ca [1] = {r2 , r3 } and Ca [2] = {s2 , s3 }, hence postdecomp(Ca ) =
{(r2 , s2 )(r2 , s3 )(r3 , s2 )(r3 , s3 )}. The post-products for transitions are π(t1 ) =
{(r1 , s2 )}, π(t2 ) = {(r2 , s3 )}, π(t3 ) = {(r3 , s2 )}, π(t4 ) = {(r3 , s3 )}, giving us
post(Ca ) = {(r2 , s2 )(r2 , s3 )(r3 , s2 )(r3 , s3 )}. Therefore we have 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.
Language L3 accepted by the net system is r∗ [ε + a + a(b + c) + a(d + e)] where
r = (a(bd + db) + a(be + eb) + a(cd + dc) + a(ce + ec)).
Example 4 (A net with distributed choice and subset-acceptance). Consider the
net system of Example 3, with the underlying net shown in Figure 3 with set of
final markings {(r1 , s1 ), (r2 , s2 )}. The language L4 accepted by this net system
is r∗ [ε + a] where r = (a(bd + db) + a(be + eb) + a(cd + dc) + a(ce + ec)).
3 Product systems
We define product systems over a fixed distribution (Σ1 , Σ2 , . . . , Σk ) of Σ. First
we define sequential systems.
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 states, Gi ⊆ Pi are final
states, p0i ∈ Pi is the initial state, and →i ⊆ Pi × Σi × Pi is a set of local moves.
Phawade et.al.: Kleene Theorems for Labelled Free Choice Nets 83
For a local move t = hp, a, p0 i of →i state p is called pre-state sometimes
denoted by pre(t) and p0 is called post-state of t, sometimes denoted by post(t).
This notation is extended to a set of local moves as well.
Let →ia denote the set of all a-labelled moves in the sequential system Ai .
The language of a sequential system is defined as usual.
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 , and R↓I for the projection to I ⊆ Loc. The initial
product state of A is R0 = (p01 , . . . , p0k ). The final states of A are denoted by G.
3.1 Direct products
Let ⇒a = S Πi∈loc(a) →ia for the product system A. The set of all global moves of
A is ⇒= a∈Σ ⇒a . This move is global within the set of component sequential
machines where label a occurs. Then for a global move g in ⇒a , we define its
set of pre-states pre(g) as the set of pre-states of all its component a-moves. The
set of post-states post(g) as the set of post-states of all its component a-moves;
and, let g[i] denote its i-th component–local a-move–belonging to Ai , for all i in
loc(a).
When final states of A are G = Πi∈Loc Gi then we say A is product system
with product-acceptance. These systems are called direct products in [11]. And, if
G ⊆ Πi∈Loc Gi then A is a product system with subset-acceptance, these systems
are called synchronous products in [11].
The runs of a product system A over some word w are described 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]. 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, as the set of words on which the product system
has an accepting run. The set of languages accepted by direct (resp. synchronous)
products is called direct (resp. synchronous) product languages.
We use a characterization from [11] of languages accepted by direct products.
Proposition 1. L is a direct product language defined over distributed alphabet
Σ iff L = {w ∈ Σ ∗ | ∀i ∈ {1, . . . , k}, ∃ui ∈ L such that w↓Σi = ui ↓Σi }.
If L = Lang(A) for direct product A = hA1 , . . . , Ak i defined over distributed
alphabet Σ then L = Lang(A1 )k . . . kLang(Ak ).
We also use a characterization of synchronous product languages [11].
Proposition 2. A language over distributed alphabet Σ is accepted by a product
system with subset-acceptance if and only if it can be expressed as a finite union
of direct product languages.
84 PNSE’18 – Petri Nets and Software Engineering
Definition 12 (PS-matchings [15]). For global a ∈ Σ, matching(a) is a sub-
set of tuples Πi∈loc(a) Pi such that for all i in loc(a), projection of these tuples
is the set of all pre-states of a-moves in →ai , and if a state p ∈ Pi appears in
one tuple, it does not appear in another tuple. We say a product state R is in
matching(a) if its projection R↓loc(a) is in the matching.
A product system is said to have matching of labels if for all global a ∈ Σ,
there is a suitable matching(a). Such a system is denoted by PS-matchings.
We have PS-matchings with product-acceptance, if the set of final product states
of it is a product of final states of component machines, or PS-matchings with
subset-acceptance, if the set of final product states is a subset of product of
final states of individual components.
A run of PS-matchings A is said to be consistent with a matching of labels [15]
v a
if for all global actions a and every prefix of the run R0 ⇒R⇒Q, the pre-states
R↓loc(a) are in the matching.
Consistency of matchings is a behavioural property and to check if a PS-
matchings A has it and can be done in PSPACE [15, 16].
Following property from [15] is used to capture free choice property.
Definition 13 (conflict-equivalent matchings for PS-matchings). 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 corre-
sponding outgoing moves from p. For global action a, its matching(a) is called
conflict-equivalent matching, if whenever p, p0 are related by the matching(a),
their outgoing local a-moves are conflict-equivalent.
start r1 start s1
Figure 5, shows a product system
a b a d defined over a distributed alpha-
a c a e bet Σ = (Σ1 = {a, b, c}, Σ2 =
{a, d, e}). It has two components
A1 ,and A2 with final states G1 =
r2 r3 s2 s3
{r1 , r2 } and, G2 = {s1 , s2 }, respec-
A1 A2 tively.
Fig. 5. Product system (A1 , A2 )
Example 5 (Product system with matchings). Consider product system of Fig-
ure 5 and relation matching(a) = {(r1 , s1 )} relation. This matching is conflict-
equivalent and the system is consistent with this matching relation.
We have a PS-matchings A = (A1 , A2 ) with product acceptance condition, if
its set of final states is G1 ×G2 . With the set of final states as {(r1 , s1 ), (r2 , s2 )} ⊆
G1 × G2 , we have a PS-matchings B = (A1 , A2 ) having subset-acceptance.
Phawade et.al.: Kleene Theorems for Labelled Free Choice Nets 85
Lemma 1 presents a language not accepted by any direct product.
Lemma 1. The language L4 = {(abd + adb + abe + aeb + ace + aec + acd +
adc)∗ (ε + a)} from Example 4 is not accepted by any direct product.
We know that the class of synchronous product languages is strictly larger than
the class of direct product languages [11]. With the matching relations this re-
lationship is preserved. The PS-matchings B of Example 5 accepts language L4
which by Lemma 1, is not accepted by any direct product. Hence, the class of lan-
guages accepted by PS-matchings with subset acceptance condition, is strictly
larger, than the class of languages accepted by PS-matchings with product-
acceptance.
However, using Proposition 2 we have the following characterization of PS-
matchings with subset-acceptance.
Corollary 1. A language L is accepted by a product system with subset-acceptance
and, having conflict-equivalent and consistent matchings if and only if L can be
expressed as a finite union of languages accepted by product system with product-
acceptance and, having conflict-equivalent and consistent matchings.
Lemma 2 presents a language not accepted by any synchronous product.
Lemma 2. The language Ls = {abd, adb, ace, aec}∗ (ε + a) of Example 2 is not
a synchronous product language.
So we have language Ls which is not accepted by any PS-matchings with subset-
acceptance. This motivates the bigger class of automata over distributed alpha-
bets, which we discuss next.
3.2 Product systems with globals
Let A = hA1 , . . . , Ak i, be a product system over the distribution Σ = (Σ1 , . . . , Σk )
and, 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 (PS-globals) is a product system
with relations globals(a), for each global action a in Σ.
With subset-acceptance condition these systems are called Asynchronous (or
Zielonka) automaton [17, 11]. Runs of a product system with globals, are defined
in the same way as for the direct products, with an additional requirement of
a
Πj∈loc(a) (hR[j], a, Q[j]i ∈ globals(a), to be satisfied when R −
→ Q is to be taken.
a
With abuse of notation sometimes we use pre(a) to denote the set {R | ∃Q, R − →
Q}. Following property [14] is used to capture free choiceness, in product systems
with globals.
Definition 15 (same source property). A product system with globals have
same source property if, any two global moves share a pre-state then their sets of
pre-states are same.
86 PNSE’18 – Petri Nets and Software Engineering
Example 6 (Product system with globals). Consider the product system of Fig-
a a a a
ure 5. Let globals(a) = { ((r1 − → r2 ), (s1 −
→ s2 )), ((r1 −
→ r3 ), (s1 −
→ s3 ))}. This
system has same source property.
With the given globals(a) we have a PS-globals C = (A1 , A2 ) with product
acceptance condition, if its set of final states is G1 × G2 . And, for the set of final
states {(r1 , s1 ), (r2 , s2 )} ⊆ G1 × G2 , we have a PS-globals D = (A1 , A2 ) with
subset-acceptance.
The language Ls = {abd, adb, ace, aec}∗ (ε + a)} of Lemma 2, is accepted by
product system with globals D of Example 6 with same source property.
Product systems with globals and product-acceptance are not considered
in [11]. We give in Lemma 3, a characterization of class of languages accepted
by product systems with globals and having subset-acceptance, in terms of PS-
globals and product-acceptance.
Lemma 3. A language is accepted by a PS-globals with subset-acceptance if and
only if it can be expressed as a finite union of languages accepted by PS-globals
with product-acceptance.
In the construction, transition structure of local components is preserved, and
so the global moves, so we have Corollary 2, which is used to get syntax for
product systems with subset acceptance condition.
Corollary 2. A language L is accepted by a PS-globals with subset-acceptance
and having same source property if and only if L can be expressed as a finite
union of languages accepted by PS-globals with product-acceptance and same
source property.
In a product system with globals and having same source property, global
moves for an action a can be partitioned into different compartments : two global
a-moves belong to same compartment if they have the same set of pre-states.
For any a-global g of a same source compartment ⇒SS a , we associate a target-
configuration π(g) = Πi∈loc(a) post(g) ∩ Pi . Let post(⇒SS SS
a ) = {π(g) | g ∈⇒a }.
SS SS
We define post-projection of a compartment as ⇒a [i] = post(⇒a ) ∩ Pi and,
SS
post-decomposition as postdecomp(⇒SS a ) = Πi∈loc(a) ⇒a [i].
Definition 16. A product system with globals and having same source property,
is said to have product moves property, if for all a in Σ, and for all same
source compartments ⇒SS SS SS
a of a-globals, postdecomp(⇒a ) ⊆ post(⇒a ).
Product systems C and D of Example 6 do not have product moves property.
Product system of Example 7 has product moves property.
Example 7 (Product system with globals and product moves property). Consider
product system A of Example 5 where the set of final states is G1 × G2 . With
a a a a a a
globals(a) = { ((r1 − → r2 ), (s1 −
→ s2 )), ((r1 −
→ r2 ), (s1 −
→ s3 )), ((r1 −
→ r3 ), (s1 −
→
a a
s2 )) ((r1 − → s3 )) } relation, we have PS-globals A0 which has product
→ r3 ), (s1 −
moves property. This also has same source property.
Phawade et.al.: Kleene Theorems for Labelled Free Choice Nets 87
Now consider the product system B of Example 5, with {(r1 , s1 ), (r2 , s2 )} ⊆
G1 × G2 as its final states, and having the globals(a) relation as above, we get
a PS-globals B 0 with subset acceptance condition, having product moves and
same source property.
A product system with globals is said to be live, if for any global move g
and any reachable product state R, there exists a product state Q such that g
is enabled at Q.
3.3 Relating product systems with matchings and globals
First we show in Theorem 1 how to construct a product system with consistent
and conflict-equivalent matchings from a PS-globals with same source property.
Theorem 1. Let Σ be a distributed alphabet and A be a product system with
globals defined over it.Then we can construct a product system B with matchings,
linear in the size of product system A with globals such that,
1. if A has same source property then B has conflict-equivalent matchings,
2. in addition, if A is live then
(a) B is consistent with matchings, and
(b) Lang(A) = Lang(B).
Now, from a PS-matchings with consistent and conflict-equivalent matchings
we construct a product system with globals having same source property.
Theorem 2. Let Σ be a distributed alphabet and let B be a product system with
conflict equivalent and consistent matchings. Then for the language of B we can
construct a product system A with globals over Σ having same source and product
moves property. The constructed product system A with globals is exponential in
the size of system B having matching of labels.
4 Nets and Product systems
We first present a generic construction of a 1-bounded S-coverable labelled net
systems, from product systems with globals.
Definition 17 (PS-globals to nets). Given a PS-globals A = hA1 , . . . , Ak i
over distribution Σ, a net system S (N = (S, T, F, λ), M0 , G) is constructed
S as fol-
lows: The set of places is S = i Pi , The set of transitions T = a globals(a),
for all actions a in Σ. Define Ti = {λ−1 (a) | a ∈ Σi }. The labelling func-
tion λ labels by action a the transitions in globals(a). The flow relation is
F = {(p, g), (g, q) | g ∈ Ta , g[i] = hp, a, qi, i ∈ loc(a)}, define Fi as its restriction
to the transitions Ti for i ∈ loc(a). Let M0 = {p01 , . . . , p0k }, be the initial product
state and G = G as the set of final global states.
88 PNSE’18 – Petri Nets and Software Engineering
We get one to one correspondence between reachable states of product system
and reachable markings of nets because the set of transitions of resultant net is
same as the set of global moves in the product system, and construction preserves
pre as well as post places.
Lemma 4. The constructed net system N from a PS-globals A, as in Defini-
tion 17, is S-coverable and Lang(N, M0 , G) = Lang(A). The size of constructed
net is linear in the size of product system.
Applying 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 3. Let (N, M0 , G) be the net system constructed from PS-globals A
as in Definition 17.
– If A has same source property then N is a free choice net,
– In addition if A has product moves property, then N has distributed choice.
In the construction, if the product system has subset-acceptance then we get
a net with a set of final markings, which may not have product condition. Since
A has subset-acceptance, we generalize the results obtained in [14].
For the product system D of Example 6, accepting language Ls we can con-
struct the net system of Example 2.
In the case that the product system A has matchings, transitions of net
constructed are reachable global moves of system A [15, 16].
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 [3]. Now we describe a linear-size
construction of a product system from a net which is S-coverable.
Definition 18 (nets to PS-globals). Given a 1-bounded labelled and an S-
coverable net system (N, M0 , G), 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, as follows. Take Pi = Si , and p0i the unique
state in M0 ∩ Pi . Define local moves →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 prod-
uct system A = hA1 , A2 , . . . , Ak i over alphabet Σ. Global moves are globals(a) =
{Πi∈loc(a) t[i] | t ∈ Ta }. And, the set of final states is G = G.
Lemma 5. From net system N with a final set of markings, the construction of
the PS-globals A in Definition 18 above preserves language. The product system
A is linear in the size of net, and product system has subset-acceptance.
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, for each global a-
move in product system we have an a-labelled transition in the net having same
Phawade et.al.: Kleene Theorems for Labelled Free Choice Nets 89
pre and post-places. 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 a free choice net, we get same source property in the product
system obtained. And, for each transition in the net we have a global trasition
hence, A has product moves property if the net has distributed choice.
Theorem 4. Let (N, M0 , G) be a 1-bounded, and an S-coverable labelled net with
a set of final markings G. Then
– if N has free choice property, then constructed product system A with globals,
has same source property,
– in addition, if the net has distributed choice, then A has product moves.
In construction of Definition 18, we start with a net having distributed choice
and a final set of markings then we get product system with matching with
subset acceptance condition. Note that in this case we do not have to construct
globals [15, 16].
For the net system of Example 2 and accepting language Ls we can construct
the product system D of Example 6.
Therefore, we generalize the results from [15, 16].
Theorem 5. For a 1-bounded, S-coverable labelled net having distributed choice
and given with a set of final markings. Then one can construct a product system
with conflict-equivalent and consistent matchings and having subset-acceptance.
Given below is the reverse direction.
Theorem 6. For a product system with conflict-equivalent, consistent match-
ings, and subset-acceptance, we get language equivalent free choice net with dis-
tributed choice and having a set of final markings.
5 Expressions
First we define regular expressions and its derivatives.
5.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.
90 PNSE’18 – Petri Nets and Software Engineering
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. We can syntactically check whether the empty word
ε ∈ Lang(s).
We use derivatives of regular expressions which are known since the time of
Brzozowski [2], Mirkin [10] and Antimirov [1].
Definition 19 (Antimirov derivatives [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) = {ε} 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 derivatives Dera (ab + ac) = {b, c} and Dera (a(b + c)) = {b + c}.
A derivative d of s with action a ∈ Init(d) is called an a-site of s. An expres-
sion 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 [15] we put together derivatives which may correspond to the same
state in a finite automaton.
Definition 20 ([15]). 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
0
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 a }, and the suffixes
Suf D D
a (L) = {y | xay ∈ La }. We say that the derivatives in set D a-bifurcate
D D
L if LDa = Pref a (L) a Suf a (L).
We use partitions [15] of the a-sites of s into blocks such that each block (that
is, element of the partition) a-bifurcates L. For an action a, let Parta (s) denote
such a partition. In addition to thinking of blocks of the partition as places of
an automaton, we can think of blocks and their effects as local moves.
Definition 21 ([14]). 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 )}.
Phawade et.al.: Kleene Theorems for Labelled Free Choice Nets 91
(B,E) (B,E)
We 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 . Given an a-duct d = (B, E) its post-effect E is sometimes denoted by d •
and its pre-block B can be denoted as • d. For a collection of ducts z, the set of all
their post-effects (resp. pre-blocks) is denoted as z • (resp. • z). In a similar way,
we define the set of post-effects of an a-cable D, as D • = {D[i] • | i ∈ loc(a)}
and its set of pre-blocks as • D = {• D[i] | i ∈ loc(a)}.
5.2 Connected expressions over a distributed alphabets
The syntax of connected expressions defined over a distribution (Σ1 , Σ2 , . . . , Σk )
of alphabet Σ is given below.
e ::= 0|fsync(s1 , s2 , . . . , sk ), where si is a regular expression over Σi
When e = fsync(s1 , s2 , . . . , sk ) and I ⊆ Loc, let the projection e↓I = Πi∈I si .
A connected expression e = fsync(s1 , s2 , . . . , sk ) over Σ, is said to have equal
choice if, for all global actions a in Σ and for any i, j in loc(a), any a-site of si
have same Init set as of any a-site of sj .
For a connected expression defined over distributed alphabet its deriva-
tives and semantics were given in [15], and are given as follows. For the con-
nected expression 0, we have Lang(0) = ∅. For the connected expression e =
fsync(s1 , . . . , sk ), its language is Lang(e) = Lang(s1 )kLang(s2 )k . . . kLang(sk ).
The definitions of derivatives extended to connected expressions [15] is as
follows. The expression 0 has no derivatives on any action. Given an expres-
sion e = fsync(s1 , s2 , . . . , sk ), its derivatives are defined by induction using the
derivatives of the si on action a:
Dera (e) = {fsync(r1 , . . . , rk ) | ∀i ∈ loc(a), ri ∈ Dera (si ); otherwise rj = sj }.
5.3 Connected expressions with pairings
We recall some properties of connected expressions over a distribution. which
were [15], useful in construction of free choice nets.
Definition 22 ([15]). Let e = fsync(s1 , s2 , . . . , sk ) be a connected expression
over Σ. For a global action a, pairing(a) is a subset of tuples Πi∈loc(a) Parta (si )
such that the projection of these tuples includes all the blocks of Parta (si ), and
92 PNSE’18 – Petri Nets and Software Engineering
if a block of Parta (sj ), j ∈ loc(a) appears in one tuple of the pairing, it does not
appear in another tuple. (For convenience we also write pairing(a) as a subset
of Πi∈loc(a) Der(si ) which respects the partition.) We call pairing(a) equal choice
if for every tuple in the pairing, the blocks of derivatives in the tuple have equal
choice.
Derivatives for connected expressions with pairing are defined as follows. A
derivative fsync(r1 , . . . , rk ) is in pairing (a) if there is a tuple D ∈ pairing(a)
such that ri ∈ D[i] for all i ∈ loc(a). For convenience we may write a derivative
as an element of pairing(a). Expression e is said to have (equal choice) pairing of
actions if for all global actions a, there exists an (equal choice) pairing(a). Ex-
pression e is said to be consistent with a pairing of actions if every reachable a-site
d ∈ Der(e) is in pairing(a). Expression e is said to have equal choice property if
it has equal choice pairing of actions for all global actions a in Σ.
Given a connected expression e with pairings, checking if it is consistent with
pairing of actions can be done in PSPACE [15, 16].
5.4 Connected expression with cables (CE-cables)
We give some properties of connected expressions over a distribution, which
extend the notion of pairing, and have been related to product systems with
globals [14].
Definition 23 ([14]). 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).
We say that a block B of Parta (si ) appears in an a-cable D if there exists j
in loc(a) and there exists Y ⊆ Dera (B) such that D[j] = (B, Y ), i.e. if B is a
pre-block of a component a-duct of D. For any a-cable D, its set of pre-blocks
•
D = ∪i∈loc(a) {Bi | Bi appears in D}, i.e. the set of pre-blocks of all the of its
component a-ducts.
For expression e, let cables(a) ⊆ a-cables(e), such that for all i in loc(a)
1. Each block B in Parta (si ), appears in at least one a-cable of it.
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 =⇒ E ∩ E 0 = ∅, i.e. if any two distinct a-ducts of si appearing in it
have same pre-block then, they must have disjoint post-effects.
A connected expression with cables (CE-cables) is a connected expression with
relations cables(a) of it, for each global action a in Σ.
Derivatives of a connected expression with cables are [14] defined as fol-
lows. The CE-cables 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 }.
Phawade et.al.: Kleene Theorems for Labelled Free Choice Nets 93
We use the word derivative for expressions such as d = fsync(r1 , . . . , rk ) given
above. The reachable derivatives are Der(e) = {d | d ∈ Derx (e), x ∈ Σ ∗ }. A CE-
cables is said to have equal source property if for any pair of two cables sharing a
common pre-block have same set of pre-blocks. 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. The number of derivatives may be exponential in k.
Example 8 (CE-pairings and CE-cables). Let Σ = (Σ1 = {a, b, c}, Σ2 = {a, d, e})
be a distributed alphabet. Let e = fsync((ab + ac)∗ , (ad + ae)∗ ) be a con-
nected expression defined over Σ. Here, r1 = (ab + ac)∗ and s1 = (ad + ae)∗ .
The set of derivatives of r1 is Der(r1 ) = {r1 , r2 = br1 , r3 = cr1 } and for
s1 it is Der(s1 ) = {s1 , s2 = ds1 , s3 = es1 }. We have a-sites(r1 ) = r1 and
Parta (r1 ) = {D = r1 }. Similarly, a-sites(s1 ) = r1 and Parta (s1 ) = {D0 = s1 }.
The only possible pairing relation is pairing(a) = {(D, D0 )}. We have Dera (e) =
{fsync(ri , sj ) | i, j ∈ {2, 3}}. Expression e satisfies equal choice property.
Now we associate a cabling relation with e. The set of a-effects of D is
Dera (D) = {r2 , r3 }. The set of a-ducts of r1 is {(D, r2 ), (D, r3 ), (D, {r2 , r3 })}.
The set of a-effects of D0 is Dera (D0 ) = {s2 , s3 } and the set of a-ducts of s1
is {(D0 , s2 ), (D0 , s3 ), (D0 , {s2 , s3 })}. A possible cables(a) relations for expression
e is {((D, r2 ), (D0 , s2 )), ((D, r3 ), (D0 , s3 ))}. See that each block in the Parta (r1 )
and Parta (s1 ) appears at least once in the cables(a) relation. And two a-ducts
of r1 appearing in this relation, have same pre-block D, we have that their set
of post-effects r2 and r3 are disjoint. This condition also holds for a-ducts of s1 .
For both a-cables set of pre-blocks is identical, therefore cables(a) satisfies
equal source property. We have Dera (e) = {fsync(r2 , s2 ), fsync(r3 , s3 )}, but ex-
pression fsync(r2 , s3 ) is not in Dera (e), because only post-effect of D containing
r2 is the set {r2 } and similarly, only post-effect of D0 containing s3 is the set {s3 }
and there does not exist an a-cable with (D, {r2 }) and (D0 , {s3 }) as its compo-
nents. We have Der(e) = {e, (r2 , s2 ), (r3 , s3 ), (r1 , s2 ), (r1 , s3 ), (r2 , s1 ), (r3 , s1 )}.
Another such example of connected expression with pairings (resp. cables) is
given below.
Example 9 (CE-pairings). Let e = fsync((ab+ac)∗ a, (ad+ae)∗ a) be a connected
expression defined over Σ. Let p1 = (ab + ac)∗ a with language L1 and q1 = (ad +
ae)∗ a with language L2 . The set of derivatives are Der(p1 ) = {p1 , p2 = bp1 , p3 =
cp1 , p4 = ε} and Der(q1 ) = {q1 , q2 = dq1 , q3 = eq1 , q4 = ε}. The partitions of
a-sites is Parta (p1 ) = {B = {p1 }} and Parta (q1 ) = {B 0 = {q1 }}. A pairing
relation is pairing(a) = {(B, B 0 )} and wrt to that Dera (e) = {fsync(pi , qj ) |
i, j ∈ {2, 3, 4}}. Expression e has equal choice property.
Now we associate a cabling relation with e. The set of a-effects of B is
Dera (B) = {p2 , p3 , p4 } and Dera (B 0 ) = {q2 , q3 , q4 }. The set of a-ducts for
p1 is {(B, {p2 }), (B, {p3 }), (B, {p2 , p4 }), (B, {p3 , p4 })(B, {p2 , p4 , p3 })} and for q1
94 PNSE’18 – Petri Nets and Software Engineering
is {(B 0 , q2 ), (B 0 , q3 ), (B 0 , {q2 , q4 }), (B 0 , {q3 , q4 })(B 0 , {q2 , q4 , q3 })}. A cables(a) re-
lation is {((B, p2 ), (B 0 , q2 )), ((B, p3 ), (B 0 , q3 )), ((B, p2 ), (B 0 , q2 ))}. Expression e
has equal source property and its set of derivatives with respect to letter a is
Dera (e) = {fsync(p2 , q2 ), fsync(p3 , q3 ), fsync(p4 , q4 )}.
Now we give two new properties of connected expressions. In a connected
expression with cables and having equal source property, cables for an global
action a can be partitioned into different compartments : two a-cables belong to
same compartment if they have equal source. For any such a-cable D belonging to
an equal source compartment ESa of a-cables, we can associate a set of its post-
blocks listed in some order as π(D) = Πi∈loc(a) (D • ∩χi ), where χi = {Parta (si ) |
a ∈ Σ}. Let post(ESa ) = {π(D) | D ∈ ESa }. We define post-projection of
compartment ESa as ESa [i] = post(ESia ) ∩ χi , and its post-decomposition as
postdecomp(ESa ) = Πi∈loc(a) ESa [i].
Following property of connected expressions is related later to product-moves-
property of direct products and hence to distributed-choice of nets.
Definition 24 (product derivatives property). A connected expression with
cables and having equal source property, is said to have product derivatives
property, if for all a in Σ, and for all equal source compartments ESa of a-cables
postdecomp(ESa ) ⊆ post(ESa ).
Example 10. The connected expression e = fsync((ab + ac)∗ , (ad + ae)∗ ) of Ex-
ample 8 does not have product derivative property with the given cabling rela-
tion {((D, r2 ), (D0 , s2 )), ((D, r3 ), (D0 , s3 ))}. If we associate the cabling relation
{((D, r2 ), (D0 , s2 )), ((D, r3 ), (D0 , s3 ), ((D, r2 ), (D0 , s3 )), ((D, r3 ), (D0 , s2 ))} with e
then it has product derivative property.
Definition 25. A connected expression e is action-live if for all actions a in
Σ, from any reachable derivative of e, we can reach an a-derivative of e.
5.5 Relating connected-expressions with pairings and with cables
First, we show how connected expressions with equal choice and consistent pair-
ings can be seen as connected expression with cables and having equal source
and product-derivatives property.
Theorem 7. Let Σ be a distributed alphabet and e be a connected expression
having equal choice and consistent pairing of actions, defined over Σ. Then for
the language of e, we can construct a connected expression e0 with cables having
equal source and product derivatives property. The constructed expression e0 with
cables is exponential in the size of expression e with pairings.
Now we give a language preserving construction of connected expression with
equal choice and consistent pairings from a CE-cables having equal source and
product-derivatives property.
Phawade et.al.: Kleene Theorems for Labelled Free Choice Nets 95
Theorem 8. Let Σ be a distributed alphabet and e0 be a connected expression
with cables defined over it.Then we can construct a connected expression e with
pairings linear in the size of e0 . And, if e0 has equal source then e has equal choice
property. In addition, if e0 is action-live then if e0 has product moves property
then e has consistency of pairing. Lang(e) = Lang(e0 ).
5.6 Sum of Connected Expressions (SCE)
We give syntax for sum of connected expressions (SCE ) defined over a distribution
(Σ1 , Σ2 , . . . , Σk ) of alphabet Σ.
e ::= 0|e1 + · · · + em , where ei is a connected expression (CE) over Σ
For an SCE e its semantics is given as follows: For the SCE 0, we have
Lang(0) = ∅. For the SCE e = e1 +e2 , · · · , em , its language is given as Lang(e) =
Lang(e1 ) ∪ Lang(e2 ) ∪ · · · ∪ Lang(sm ). The definitions of derivatives extended
to SCEs is as given below. The expression 0 has no derivatives on any action.
Derivative of an SCE with respect to a letter a is defined as: Dera (e) = Dera (e1 )∪
Dera (e2 ) ∪ · · · ∪ Dera (sm ). Inductively Deraw (e) = Derw (Dera (e)). The set of all
derivatives Der(e) is union of sets of derivatives of e with respect to all words w
in Σi∗ for all i in {1, . . . , m}.
Definition 26 (SCE with pairings)). An SCE e = e1 + · · · + em where each
ei is a CE-pairings, is called a sum of connected expressions with pairing (SCE-
pairings). An SCE-pairings e is said to have equal choice property if each com-
ponent CE-pairings ei of the sum also has it.
Example 11. The expression e = e1 + e2 where e1 = fsync((ab + ac)∗ , (ad + ae)∗ )
is the CE-pairings of Example 8 and e2 = fsync((ab + ac)∗ a, (ad + ae)∗ a) is the
CE-pairings of Example 9 is an SCE-pairings with equal choice property, as both
e1 and e2 have it.
Definition 27 (SCE with cables)). An SCE e = e1 + · · · + em where each
ei is a CE-cables, then e is called a sum of connected expressions with cables
(SCE-cables). An SCE-cables e is said to have equal source property if each
component CE-cables ei of the sum also has it. An SCE-cables e has product
derivatives property if each component CE-cables ei of the sum has it.
Example 12. The expression e0 = e3 +e4 where e3 = fsync((ab+ ac)∗ , (ad+ ae)∗ )
is the CE-cables of Example 8 and e4 = fsync((ab + ac)∗ a, (ad + ae)∗ a) is the
CE-cables of Example 9.
As an example of how derivatives of SCE-cables from derivatives of SCE-
pairings differ even while having identical components, see that f sync(r2 , s3 ) ∈
Dera (e) (of Example 11) but it does not belong to Dera (e0 ).
96 PNSE’18 – Petri Nets and Software Engineering
6 Connected Expressions and Product Systems
To get a product system with globals having subset-acceptance, from a sum of
connected expression, we use an earlier result from [14], where construction of
PS-globals with product-acceptance was given from a CE-cables.
For each set of derivatives (pre-blocks and after-effects), of a component
regular expression, we constructed an unique state of local component, which
gives us product moves property in the constructed product system if we have
product derivatives property for given CE-cables.
Lemma 6 (CE-cables to PS-globals with product-acceptance [14]). Let
e be a CE-cables, defined over a distribution Σ. Then for the language of e, we
can compute a PS-globals with product-acceptance linear in the size of expression
e. Further, if e had equal-source, then system A has same source property; and,
if e had product-derivatives then A has product moves property.
Using Lemma 6, we get PS-globals with subset-acceptance, from sum of con-
nected expressions.
Theorem 9 (SCE-cables to PS-globals with subset-acceptance). Let e
be an sum of connected expression defined over Σ. Then we can construct a
PS-globals A with subset-acceptance for the language of e. If e had equal source
property, then has same source property. In addition, if e has product derivatives
property then A has product moves property.
Example 13. For SCE-cables e0 of Example 12, we can construct PS-globals with
same source property and subset-acceptance D of Example 6, accepting language
Ls , using Theorem 9.
A language preserving, construction of connected expressions with equal
source property, from a PS-globals with same source property and product-
acceptance, was given in [14]. Since each local state–whether a source state or a
target state of local move–is mapped uniquely to a set of derivatives of compo-
nent regular expression, we have product-derivatives property for the expression,
if the product system had product-moves property.
Lemma 7 (PS-globals with product-acceptance to CE-cables [14]). Let
Σ be a distributed alphabet and, A be a product system with globals and product-
acceptance, defined over Σ. For the language of A, we can construct a connected
expression e with cables, exponential in the size of the given product system.
Further, if product system has same source property then connected expression
with cables has equal source property, in addition, if it has product-moves property
then connected expression with cables has product-derivatives property.
Now using Lemma 7, we get a sum of connected expressions for PS-globals
with subset-acceptance.
Phawade et.al.: Kleene Theorems for Labelled Free Choice Nets 97
Theorem 10 (PS-globals with subset-acceptance to SCE-cables). Let A
be a product system with globals and subset-acceptance, defined over distribution
Σ. For the language of A, we can construct a sum of connected expression e with
cables. And, if product system has same source property then e has equal source
property. Also, in addition, if A has product moves property then e has product
derivatives property.
Example 14. For a PS-globals with same source property and subset-acceptance
D of Example 6, accepting language Ls , we can construct an SCE-cables e0 of
Example 12 using Theorem 10.
Using equivalence of PS-matchings with product-acceptance and CE-cables,
from [15, 16], and Corollary 1 we get language equivalent SCE-pairings for PS-
matchings with subset-acceptance, and vice-versa.
Theorem 11 (PS-matchings with subset-acceptance to SCE-pairings).
Let A be a product system with conflict-equivalent and consistent matchings,
having subset-acceptance. For the language of A, we can construct a sum of
connected expression e with equal choice and consistent pairings.
We have the reverse translation given as below.
Theorem 12 (SCE-pairings to PS-matchings with subset-acceptance).
Let Σ be a distributed alphabet and a sum of connected expression e defined
over it, with equal choice and consistent pairings. Then for its language we can
construct a product system with conflict-eauivalent and consistent matchings,
having subset-acceptance.
7 Conclusion
In this paper, we have given a language (Ls of Example 2) which can be ac-
cepted by “free choice” Zielonka automata. This language is not accepted by any
synchronous product or direct product. We have also given a language (L4 of
Example 4) which can be accepted by a “free choice” synchronous product and
not by any direct product. A language which can be accepted by “free choice” di-
rect product (L3 of Example 3) was given in [15]. With this we have a hierarchy
of labelled free choice nets similar to automata over distributed alphabets. In
addition we have defined Zielonka automata with product acceptance condition
and its “free choice” restriction. We have given language (Lp of Example 1) of
this class. We used this intermediate automata to obtain Kleene theorem for
“free choice” Zielonka automata.
We give below the summary of correspondences established for the nets, au-
tomata over distributed alphabets and expressions. To get an expression, for the
language of a labelled 1-bounded and S-coverable free choice net (with or without
distributed choice) having a finite set of final markings, we use Theorem 4 and
Theorem 10. In the reverse direction, we use Theorem 9 to get product sytem
98 PNSE’18 – Petri Nets and Software Engineering
with subset acceptance from expressions and then Theorem 3 to get a language
equivalent free choice net system.
If the labelled free choice net had distributed choice and has a finite set of
final markings, we have an alternate syntax for it. We first use Theorem 5 to get
equivalent product system, and then Theorem 11, to get equivalent expressions
for the product system constructed. In the reverse direction, we use Theorem 12
and then Theorem 6.
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. Desel, J., Esparza, J.: Free choice Petri nets. Cambridge University Press, New
York, USA (1995)
4. Garg, V.K., Ragunath, M.: Concurrent regular expressions and their relationship
to petri nets. Theoret. Comp. Sci. 96(2), 285–304 (1992)
5. Grabowski, J.: On partial languages. Fundam. Inform. 4(2), 427–498 (1981)
6. Hack, M.H.T.: Analysis of production schemata by Petri nets. Project Mac Report
TR-94, MIT (1972)
7. Jantzen, M.: Language theory of petri nets. In: ACPN. LNCS, vol. 254 (1987)
8. Lodaya, K.: Product automata and process algebra. In: SEFM. IEEE (2006)
9. Lodaya, K., Mukund, M., Phawade, R.: Kleene theorems for product systems. In:
DCFS, Proceedings. LNCS, vol. 6808. Springer (2011)
10. Mirkin, B.G.: An algorithm for constructing a base in a language of regular ex-
pressions. Engg. Cybern. 5, 110–116 (1966)
11. Mukund, M.: Automata on distributed alphabets. In: D’Souza, D., Shankar, P.
(eds.) Modern Applications of Automata Theory. World Scientific (2011)
12. Petersen, J.L.: Computation sequence sets. Journal of Computing and Systems
Science 13(1), 1–24 (1976)
13. Phawade, R.: Labelled Free Choice Nets, finite Product Automata, and Expres-
sions. Ph.D. thesis, Homi Bhabha National Institute (2015)
14. Phawade, R.: Kleene theorems for labelled free choice nets without distributed
choice. In: Cabac, L., Kristensen, L.M., Rölke, H. (eds.) Proc. PNSE. CEUR Work-
shop Proceedings, vol. 1591, pp. 132–152. CEUR-WS.org (2016)
15. Phawade, R., Lodaya, K.: Kleene theorems for labelled free choice nets. In: Moldt,
D., Rölke, H. (eds.) Proc. PNSE. CEUR Workshop Proceedings, vol. 1160, pp.
75–89. CEUR-WS.org (2014)
16. Phawade, R., Lodaya, K.: Kleene theorems for synchronous products with match-
ing. Transactions on Petri nets and other models of concurrency X, 84–108 (2015)
17. Zielonka, W.: Notes on finite asynchronous automata. Inform. Theor. Appl. 21(2),
99–135 (1987)