We provided [15] expressions for free choice nets having “distributed choice property” which makes the nets “direct product” representable. 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 polynomial 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.
There are several different notions of acceptance to define languages for labelled
Petri nets, depending on restrictions on labelling and “final” markings [
Consider the net N of Figure 1 with G = ffr1; s1g; fr2; s2gg 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 = f(r1; s1); (r2; s2)g. For the
final marking f(r1; s1)g, its language is expressed as fsync((ab + ac) ; (ad + ae) ).
Similarly, for the final markings f(r2; s2)g 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” [
For the restricted class of direct product representable free choice nets, with
its set of final markings having product condition-we gave expressions via
product systems with matchings and product-acceptance [
Language equivalent expressions for 1-bounded nets have been given by
Grabowski [
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 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
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 2 to a set , denoted as w# , is defined by: (a( # ) if a 2 ; "# = " and (a )# = # if a 2= : Given languages L1; L2; : : : ; Lm, their synchronized shuffle L = L1k : : : kLm is defined as: w 2 L iff for all i 2 f1; : : : ; mg; w# i 2 Li.
Definition 1 (Distributed Alphabet). Let Loc denote the set f1; 2; : : : ; kg. A distribution of over Loc is a tuple of nonempty sets ( 1; 2; : : : ; k) with = S1 i k i. For each action a 2 , its locations are the set loc(a) = fi j a 2 ig. Actions a 2 such that jloc(a)j = 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 fpg, sometimes we may write it as p. 2.1
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 = fx j (x; z) 2 F g is called pre-set of z and z = fx j (z; x) 2 F g is called post-set of z. Given a set Z of nodes of N , let Z = Sz2Z z and Z = Sz2Z z .
We only consider nets in which every transition has nonempty pre- and postset. For all actions a in let Ta = ft j t 2 T and (t) = ag.
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. G 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 }(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 n t)[t and, we write this as M !t M 0 or M (t!) M 0.
A firing sequence (t1) (t2) : : : is defined by composition of labels of transition sequence t1t2 : : : fired from M0 i.e., M0 t!1 M1 t!2 : : : . 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) = f ( ) 2 j 2 T and M0 ! M; for some M 2 Gg.
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 [
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 2 T , we have j tj = 1 = jt j (N 0 is an S-net [
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 [
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 = f 1(a) j a 2 ig, 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 [
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; : : : qki 2 G and hq10; q20; : : : qk0i 2 G then fq1; q10g fq2; q20g : : : fqk; qk0g 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) 2 Fi; for p; p0 2 Pi for all i in loc(a).
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 2 [x] then s is included in [x], and – if a transition t 2 [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 [
In a labelled net N , for a free choice cluster C = (SC ; TC ) define the
alabelled transitions Ca = ft 2 TC j (t) = ag. If the net has an S-decomposition
then we associate a post-product (t) = i2loc(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
t2Ca
the post-projection of the cluster Ca[i] = Ca \ Si and the post-decomposition
postdecomp(Ca) = i2loc(a)Ca[i]. Clearly post(Ca) postdecomp(Ca). The
following definition from [
The post-products are (t1) = f(r2; s2)g and (t2) = f(r3; s3)g so post(Ca) = f(r2; s2); (r3; s3)g. 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 f(r1; s1); (r1; s2); (r2; s1)(r2; s2)g 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
satisfying 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
markings f(r1; s1); (r2; s2)g, 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
condition). Consider the labelled net system (N; (r1; s1); G)) of Figure 3, defined
over distributed alphabet = ( 1 = fa; b; cg; 2 = fa; d; eg), and where
G = f(r1; s1); (r1; s2); (r2; s1); (r2; s2)g is the set of final markings satisfying
product condition. Its two S-components with sets of places S1 = fr1; r2; r3g
and S2 = fs1; s2; s3g, are shown in Figure 4. For cluster C of r1, we have Ca =
ft1; t2; t3; t4g, Ca[
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 f(r1; s1); (r2; s2)g. 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
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; pi0i where Pi are called states, Gi Pi are final states, pi0 2 Pi is the initial state, and !i Pi i Pi is a set of local moves.
For a local move t = hp; a; p0i 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; 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 i2LocPi 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
Let )a= i2loc(a) !ia for the product system A. The set of all global moves of A is )= Sa2 )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 = i2LocGi then we say A is product system
with product-acceptance. These systems are called direct products in [
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 2 loc(a); hR[j]; a; Q[j]i 2!j , and for all j 2= 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 [
We also use a characterization of synchronous product languages [
A product system is said to have matching of labels if for all global a 2 , 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 [
Consistency of matchings is a behavioural property and to check if a
PSmatchings A has it and can be done in PSPACE [
Following property from [
start r1 start
s1 r2 a b
a c A1 r3 s2
s3 a d
a e
A2
Example 5 (Product system with matchings). Consider product system of Figure 5 and relation matching(a) = f(r1; s1)g relation. This matching is conflictequivalent 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 f(r1; s1); (r2; s2)g G1 G2, we have a PS-matchings B = (A1; A2) having subset-acceptance.
Lemma 1 presents a language not accepted by any direct product.
Lemma 1. The language L4 = f(abd + adb + abe + aeb + ace + aec + acd +
adc) (" + a)g 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 [
However, using Proposition 2 we have the following characterization of PSmatchings 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 productacceptance and, having conflict-equivalent and consistent matchings.
Lemma 2 presents a language not accepted by any synchronous product. Lemma 2. The language Ls = fabd; adb; ace; aecg (" + a) of Example 2 is not a synchronous product language.
So we have language Ls which is not accepted by any PS-matchings with subsetacceptance. This motivates the bigger class of automata over distributed alphabets, which we discuss next. 3.2
Let A = hA1; : : : ; Aki, 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 [
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. Example 6 (Product system with globals). Consider the product system of Figure 5. Let globals(a) = f ((r1 !a r2); (s1 !a s2)), ((r1 !a r3); (s1 !a s3))g. 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 f(r1; s1); (r2; s2)g G1 G2, we have a PS-globals D = (A1; A2) with subset-acceptance.
The language Ls = fabd; adb; ace; aecg (" + a)g 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 [
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 )aSS , we associate a targetconfiguration (g) = i2loc(a)post(g) \ Pi. Let post()aSS ) = f (g) j g 2)aSS g. We define post-projection of a compartment as )aSS [i] = post()aSS ) \ Pi and, post-decomposition as postdecomp()aSS ) = i2loc(a) )aSS [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 )aSS of a-globals, postdecomp()aSS ) post()aSS ).
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 globals(a) = f ((r1 !a r2); (s1 !a s2)), ((r1 !a r2); (s1 !a s3)), ((r1 !a r3); (s1 ! a s2)) ((r1 !a r3); (s1 !a s3)) } relation, we have PS-globals A0 which has product moves property. This also has same source property.
Now consider the product system B of Example 5, with f(r1; s1); (r2; s2)g G1 G2 as its final states, and having the globals(a) relation as above, we get a PS-globals B0 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.
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
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; : : : ; Aki over distribution , a net system (N = (S; T; F; ); M0; G) is constructed as follows: The set of places is S = Si Pi, The set of transitions T = Sa globals(a), for all actions a in . Define Ti = f 1(a) j a 2 ig. The labelling function labels by action a the transitions in globals(a). The flow relation is F = f(p; g); (g; q) j g 2 Ta; g[i] = hp; a; qi; i 2 loc(a)g, define Fi as its restriction to the transitions Ti for i 2 loc(a). Let M0 = fp10; : : : ; p0kg, be the initial product state and G = G as the set of final global states.
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 Definition 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 [
For the product system D of Example 6, accepting language Ls we can construct 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 [
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 [
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
amove in product system we have an a-labelled transition in the net having same
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 [
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 [
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.
Theorem 6. For a product system with conflict-equivalent, consistent matchings, and subset-acceptance, we get language equivalent free choice net with distributed choice and having a set of final markings. 5
5.1
A regular expression over alphabet is given by: s ::= 0 j 1 j a 2
i j s1 s2 j s1 + s2 j s1 The language of constant 0 is ; and that of 1 is f"g. For a symbol a 2 i, its language is Lang(a) = fag. 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.
i such that constants 0 and 1 are not in i
For each regular expression s over i, let Lang(s) be its language and its initial actions form the set Init(s) = fa j 9v 2 i and av 2 Lang(s) g which can be defined syntactically. We can syntactically check whether the empty word " 2 Lang(s).
We use derivatives of regular expressions which are known since the time of
Brzozowski [
The set of all partial derivatives Der(s) = [
Derw(s), where Der"(s) = fsg. w2 i We have derivatives Dera(ab + ac) = fb; cg and Dera(a(b + c)) = fb + cg.
A derivative d of s with action a 2 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 [
Definition 20 ([
We use partitions [
We define the prefixes P refa(B;E)(L) = fx j xay 2 L(aB;E)g and the suffixes Sufa(B;E)(L) = fy j xay 2 L(aB;E)g. 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 aducts (B; E) and (B0; E0) in a-ducts(si), define (B; E) = (B0; E0) if B = B0 and E = E0. 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 = fD[i] j i 2 loc(a)g and its set of pre-blocks as D = f D[i] j i 2 loc(a)g.
The syntax of connected expressions defined over a distribution ( 1; 2; : : : ; k) of alphabet is given below.
e ::= 0jfsync(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 = i2I 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
derivatives and semantics were given in [
The definitions of derivatives extended to connected expressions [
Dera(e) = ffsync(r1; : : : ; rk) j 8i 2 loc(a); ri 2 Dera(si); otherwise rj = sj g: 5.3
We recall some properties of connected expressions over a distribution. which
were [
Definition 22 ([
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 2 pairing(a) such that ri 2 D[i] for all i 2 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). Expression e is said to be consistent with a pairing of actions if every reachable a-site d 2 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 [
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 [
Definition 23 ([
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 (B0; E0) in a-ducts(si) with (B; E) 6= (B0; E0), if B = B0 =) E \ E0 = ;, 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 [
We use the word derivative for expressions such as d = fsync(r1; : : : ; rk) given above. The reachable derivatives are Der(e) = fd j d 2 Derx(e); x 2 g. A CEcables 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) = fw 2
j 9e0 2 Derw(e) such that " 2 Lang(ri); where e0[i] = rig.
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 = fa; b; cg; 2 = fa; d; eg) be a distributed alphabet. Let e = fsync((ab + ac) ; (ad + ae) ) be a connected expression defined over . Here, r1 = (ab + ac) and s1 = (ad + ae) . The set of derivatives of r1 is Der(r1) = fr1; r2 = br1; r3 = cr1g and for s1 it is Der(s1) = fs1; s2 = ds1; s3 = es1g. We have a-sites(r1) = r1 and Parta(r1) = fD = r1g. Similarly, a-sites(s1) = r1 and Parta(s1) = fD0 = s1g. The only possible pairing relation is pairing(a) = f(D; D0)g. We have Dera(e) = ffsync(ri; sj) j i; j 2 f2; 3gg. Expression e satisfies equal choice property.
Now we associate a cabling relation with e. The set of a-effects of D is Dera(D) = fr2; r3g. The set of a-ducts of r1 is f(D; r2); (D; r3); (D; fr2; r3g)g. The set of a-effects of D0 is Dera(D0) = fs2; s3g and the set of a-ducts of s1 is f(D0; s2); (D0; s3); (D0; fs2; s3g)g. A possible cables(a) relations for expression e is f((D; r2); (D0; s2)); ((D; r3); (D0; s3))g. 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) = ffsync(r2; s2); fsync(r3; s3)g, but expression fsync(r2; s3) is not in Dera(e), because only post-effect of D containing r2 is the set fr2g and similarly, only post-effect of D0 containing s3 is the set fs3g and there does not exist an a-cable with (D; fr2g) and (D0; fs3g) as its components. We have Der(e) = fe; (r2; s2); (r3; s3); (r1; s2); (r1; s3); (r2; s1); (r3; s1)g.
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 L1and q1 = (ad + ae) a with language L2. The set of derivatives are Der(p1) = fp1; p2 = bp1; p3 = cp1; p4 = "g and Der(q1) = fq1; q2 = dq1; q3 = eq1; q4 = "g. The partitions of a-sites is Parta(p1) = fB = fp1gg and Parta(q1) = fB0 = fq1gg. A pairing relation is pairing(a) = f(B; B0)g and wrt to that Dera(e) = ffsync(pi; qj) j i; j 2 f2; 3; 4gg. Expression e has equal choice property.
Now we associate a cabling relation with e. The set of a-effects of B is Dera(B) = fp2; p3; p4g and Dera(B0) = fq2; q3; q4g. The set of a-ducts for p1 is f(B; fp2g); (B; fp3g); (B; fp2; p4g); (B; fp3; p4g)(B; fp2; p4; p3g)g and for q1 is f(B0; q2); (B0; q3); (B0; fq2; q4g); (B0; fq3; q4g)(B0; fq2; q4; q3g)g. A cables(a) relation is f((B; p2); (B0; q2)); ((B; p3); (B0; q3)); ((B; p2); (B0; q2))g. Expression e has equal source property and its set of derivatives with respect to letter a is Dera(e) = ffsync(p2; q2); fsync(p3; q3); fsync(p4; q4)g.
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 postblocks listed in some order as (D) = i2loc(a)(D \ i), where i = fParta(si) j a 2 g. Let post(ESa) = f (D) j D 2 ESag. We define post-projection of compartment ESa as ESa[i] = post(ESia) \ i, and its post-decomposition as postdecomp(ESa) = i2loc(a)ESa[i].
Following property of connected expressions is related later to product-movesproperty 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 Example 8 does not have product derivative property with the given cabling relation f((D; r2); (D0; s2)); ((D; r3); (D0; s3))g. If we associate the cabling relation f((D; r2); (D0; s2)); ((D; r3); (D0; s3); ((D; r2); (D0; s3)); ((D; r3); (D0; s2))g 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.
Relating connected-expressions with pairings and with cables First, we show how connected expressions with equal choice and consistent pairings 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. 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
We give syntax for sum of connected expressions (SCE ) defined over a distribution ( 1; 2; : : : ; k) of alphabet .
e ::= 0je1 +
+ 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 f1; : : : ; mg.
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 (SCEpairings). An SCE-pairings e is said to have equal choice property if each component 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 SCEpairings differ even while having identical components, see that f sync(r2; s3) 2 Dera(e) (of Example 11) but it does not belong to Dera(e0).
To get a product system with globals having subset-acceptance, from a sum of
connected expression, we use an earlier result from [
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 [
Using Lemma 6, we get PS-globals with subset-acceptance, from sum of connected 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
productacceptance, was given in [
Lemma 7 (PS-globals with product-acceptance to CE-cables [
Now using Lemma 7, we get a sum of connected expressions for PS-globals with subset-acceptance. 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 [
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.
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
In this paper, we have given a language (Ls of Example 2) which can be
accepted 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”
direct product (L3 of Example 3) was given in [
We give below the summary of correspondences established for the nets, automata 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 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.