Kleene Theorem for Labelled Free Choice Nets without Distributed Choice

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 effectsrepresenting automaton transitions-in our expressions.

Introduction

The Kleene theorem for regular expressions enables us to translate from regular expressions to automata and back [ 12 ]. Expressions are widely used by programmers 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 1bounded free choice nets are checking liveness is in PTIME [ 6,4 ], checking deadlock 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 renaming operator has been used in the syntax to disambiguate synchronizations. In earlier [ 15,21,22 ] works, we have provided syntax for various subclasses of 1bounded 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 synchronizations by different sets of processes. This also enables us to compare expressiveness of nets with those of different classes of product automata [ 17 ].

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

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 final 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 synchronize. 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 product 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 represents 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 regular 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 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 difficulty 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 of Σ over Loc is a tuple of nonempty sets (Σ1, Σ2, . . . , Σk) with Σ = S1≤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 • = {x | (z, x) ∈ F } is called post-set of z. Given a set Z of nodes of N , let •Z = Sz∈Z •z and Z • = Sz∈Z z •.

We only consider nets in which every transition has nonempty pre- and postset. 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. 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[t1iM1[t2i . . . 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 several 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. Definition 7. An S-decomposable labelled net system (N, M0, G) is an Sdecomposable 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, . . . qki ∈ G and hq10, q20, . . . qk0i ∈ 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, p0i 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 alabelled 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 transition 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 following 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 distributed 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 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. 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. 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. a p1 a p4 p2 p5 a a p1 Definition 10. A sequential system over a set of actions Σi is a finite state automaton Ai = hPi, →i, Gi, pi0i where Pi are called places, Gi ⊆ Pi are final places, pi0 ∈ 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, p0i of →i place p is called pre-place and p0 is called postplace 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:

LaX = {xay ∈ L | ∃p in X such that p0 −→ p −a→y Gi}, P refaX (L) = {x | xay ∈ x LaX }, and SufaX (L) = {y | xay ∈ LaX }. A set of places X ⊆ Pi of component Ai a-bifurcates L if LaX = P refaX (L) · a · SufaX (L). These relativized languages 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 the set of its target places. For a set X of places of Ai define a-targets(X) = Sp∈X a-targets(p). For sets of places X and Y of Ai with language L, we define relativized languages: L(aX,Y ) = {xay ∈ L | ∃p ∈ X and ∃q ∈ Y such that p0 −→x p −→a q −→y Gi}, Pref (aX,Y )(L) = {x | xay ∈ L(aX,Y )} and Suf (aX,Y )(L) = {y | xay ∈ L(aX,Y )}. We say that (X, Y ) a-funnels language L if L(aX,Y ) = Pref (aX,Y )(L) · a · Suf (aX,Y )(L). Remark 2. For a set X of places of Ai with language L and a set Y targets(X), if X a-bifurcates L then the tuple (X, Y ) a-funnels L. ⊆ aUsing 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 Figure 5. The set X = {p2, p4} p2 a-bifurcates L and the tuple a start p1 a p4 a p5 a p6 (X, {p3}) a-funnels L. The set Z = {p1, p3} does not a- p3 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 aZ (L)) and ε in Pref pa1 (L) (so in Pref aZ (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, pi0i be a sequential system over alphabet Σi for 1 ≤ i ≤ k. A product system A over the distribution Σ = (Σ1, . . . , Σk) is a tuple hA1, . . . , Aki.

Let Πi∈LocPi 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∈LocGi denotes the final states of A. Let ⇒a= Πi∈loc(a) →ia. The set of all global moves of A is ⇒= Sa∈Σ ⇒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, p0i, hq, a, q0i ∈→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, q1i ∈→i is conflict-equivalent to the local move hp0, a, q10i ∈→j , if for every other local move hp, b, q2i ∈→i, there is a local move hp0, b, q20i ∈→j and, conversely, for moves from p0 there are corresponding outgoing moves from p. We call A = hA1, . . . , Aki 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 relations 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 aglobals in the given globals(a) relation have the same set of pre-places. start r1 start

s1 r2 a b

a c A1 r3 s2

s3 a d

a e A2 (g(lor1ba−→als(ra2))=,(s{1 −→aa s2)),

a ((r1 −→ r3), (s1 −→ s3))}.

Fig. 6. Product system A = hA1, A2i used in Example 3 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, . . . , Aki over distribution Σ, we can produce a net system (N = (S, T, F, λ), M0, G) as follows: – S = Si Pi, the set of places. – T = Sa 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 = {p10, . . . , 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 Scoverable, 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, . . . , Aki.

– Pi = Si, pi0 the unique state in M0 ∩ Pi. – →i= {hp, λ(t), p0i | t ∈ Ti and (p, t), (t, p0) ∈ Fi, for p, p0 ∈ Pi}. 0 – So we get sequential systems Ai = hPi, →i, pi i and the product system A = hA1, A2, . . . , Aki over alphabet Σ. – globals(a) = – G = G [ (Πi∈loc(a)t[i]).

t∈Ta

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 Figure 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 4.1

Expressions

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 | s1∗

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 s1∗, 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 derivativesa–ssociated 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. 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(s1∗) = Dera(s1) · s1∗

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 constructing 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 LaD = {xay | xay ∈ L, ∃d ∈ Derx(s) ∩ D, ∃d0 ∈ Deray(d) with ε ∈ Lang(d0)}, and the prefixes Pref aD(L) = {x | xay ∈ LaD}, and the suffixes Suf aD(L) = {y | xay ∈ LaD}. We say that the derivatives in set D a-bifurcate L if LaD = Pref aD(L) · a · SufaD(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 language of a regular expression s.

In comparison with our earlier paper [ 21 ], the next Definition 20 and Proposition 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 L(aB,E) = {xay ∈ L | ∃d ∈ Derx(s) ∩ B, ∃d0 ∈ Dera(d) ∩ E, and ∃d00 ∈ Dery(d0) with ε ∈ Lang(d00)}.

Also define the prefixes Sufa(B,E)(L) = {y | xay ∈ L(aB,E)}. We say that a tuple (B, E) a-funnels L if L(aB,E) = P refaB(L) · a · Sufa(B,E)(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 (B0, E0) in a-ducts(si), define (B, E) = (B0, E0) if B = B0 and E = E0.

P refa(B,E)(L) = {x | xay ∈ L(aB,E)} and the suffixes Example 4. Consider a regular expression p1 = (aaa)∗aaa. Let L denote the language 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 Figure 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 tuple (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 abifurcate language L, because for the word aaaaaa in L, we have string aaa in Suf pa3 (L) (and hence in Suf aZ (L)) and we have string ε in Pref pa1 (L) (and hence in Pref aZ (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 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 = L1k . . . kLk is defined as: w ∈ L iff for all i ∈ {1, . . . , k}, w↓Σi ∈ Li. The definition of derivatives extended to connected expressions [ 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 defined 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 connected expressions over a distribution. These extend the notion of pairing given earlier, and will ultimately lead us to construct free choice nets without distributed 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 (B0, E0) in a-ducts(si) with (B, E) 6= (B0, E0), if B = B0 then E ∩ E0 = ∅.

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 ∈ Σ∗}.

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 distributed 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 posteffects {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 connected 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 ]. 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 separation 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 A0 . Now q is a unique place having i 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 A0 . Now we rename back these i 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, . . . , Aki 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 and new sequential system Hi over it. Repeating this for each sequential system Ai we get a new product system H = hH1, . . . , Hki 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 expression 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 Proposition 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 (Bp0,Bq0). As (p, q) (Bp0, Bq0) obtained as above, we need to prove that L(ap,q) = La and (Bp0, Bq0) both a-funnel language L, hence L(ap,q) = Pref pa(L) · a · Suf (ap,q)(L) and L(aBp0,Bq0) = Pref aBp0 (L) · a · Suf a

(Bp0,Bq0)(L). Since place p, as well as block Bp0, a-bifurcates L, we have Pref pa(L) = Pref aBp0 (L). Therefore, it is sufficient to prove (Bp0,Bq0)(L). Consider a word y in Suf (ap,q)(L) the equivalence Suf (ap,q)(L) = Suf a but we have y = cqy0 as q is the only place having outgoing cq moves. Therefore y0 is in Suf qa(L) and since q, as well as block Bq0, cq-bifurcates L we have y0 in Suf aB0q(L) also. But we also have word y = cy0 in Suf pa(L) and, hence y in Suf aBp0 (L). Therefore, we have cy0 in Suf a (Bp0,Bq0)(L) as required.

Hence for each local a-move (p, a, q) of sequential system Hi we have an aduct (Bp0, Bq0) of regular expression s0i. Therefore, for each a-global of product H we get an a-cable of connected expression e0 by taking tuple of a-ducts corresponding 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 = x0ay0 in Lang(s0i). So there exist derivatives d0 in Derx0 (s0i), and r0 in Derx0a(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 B0 ⊆ 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 v0 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. tu Now we use Lemma 4 to get expressions for the product systems with globals. Theorem 3. Let A be a product system with globals, having same source property, 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 separation 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.

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 X0 so that X0 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 X0 from X, and B0 from B. This renaming is well-defined. Now X0 is a block in the PartcX (s0i). We construct A0i from s0i, where we get a unique place q for X0 also, therefore we get a local move (p, a, q) corresponding to a-duct (B0, X0) 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). tu

Next we present construction of products with globals having same source property from connected expressions with cables, having equal source property. 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 aduct 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 Σ0.

i

So we get connected expression e0 = (s01, . . . , s0k) over distributed alphabet Σ0 = (Σ10, . . . , Σk0). This expression has unique sites property, and continues to 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, . . . , A0ki 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). tu 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(((a1b + a1c)(a2b+a2c))∗, ((a1d+a1e)(a2d+a2e))∗). This expression has unique sites. See that each a-duct also gets renamed, for example after renaming a-duct (r1, r2) sboecoonm. eSsoanwea1h-advuecttw(ro10,sre20ts) oafndcaab-ldesucntow(s4f,osr5)twboecgolmobeasl aanctaio2n-dsuac1t a(sn04d, sa052):, 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 start b r2

a2 r5

r1 a1 b r4

A01 a1 c a2 r3 r6 c

start d s2

a2 s5

s1 a1 d s4

A02 a1 e a2 s3 s6 e globals(a1) = {

a1 a1 ((r1 −→ r2), (s1 −→ s2)),

a1 a1 ((r1 −→ r3), (s1 −→ s3))}. globals(a2) = {

a2 a2 ((r4 −→ r5), (s4 −→ s5)),

a2 a2 ((r4 −→ r6), (s4 −→ s6))}.

Fig. 7. Product system A0 = hA01, A02i 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 A0 , where i in i {1, 2}. This intermediate product system with globals is shown in Figure 7. Now renaming back a1 and a2 by action a in A0 s we get product system A = hA1, A2i 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 component 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.

References

1. Antimirov , V.: Partial derivatives of regular expressions and finite automaton constructions . 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 expression 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, languages, and computation - international edition (2 . ed). Addison-Wesley ( 2003 )

12. Kleene , S.C. : Representation of events in nerve nets and finite automata . In: Automata 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 expressions . 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 Expressions . 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 matching . 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 )