In earlier work [LMP11], we showed that a graph-theoretic condition called “structural cyclicity” enables us to extract syntax from a conflict-equivalent product system of automata. In this paper we have a “pairing” property in our syntax which allows us to connect to a broader class of product systems, where the conflict-equivalence is not statically fixed. These systems have been related to labelled free choice nets.
Petri nets are an excellent visual representation of concurrency. But like any graphical notation they are less amenable to syntax. For finite automata, Kleene’s regular expressions provide us with a formalism where we can switch between the graphical and the textual. For 1-bounded Petri nets, equivalent syntax has been provided by Grabowski [Gra81], Garg and Ragunath [GR92] and other authors. Here we place restrictions on this syntax in an effort to match the 1-bounded labelled free choice nets, a very well-studied subclass [Hac72] with more efficient analysis and algorithms [DE95]. It has been claimed that free choice nets can be useful in business process modelling [SH96], but our motivation is more conceptual than dictated by business concerns.
As is usual when dealing with subclasses, this turns out to be challenging. We also follow the example of finite automata and work directly with labelled nets, not relying on a renaming operator in the syntax. As in our earlier paper [LMP11], we rely on an intermediate formalism, “direct” products of automata, which are known to be weaker than 1-bounded nets [Zie87,Muk11]. There we identified a subclass called FC-products, and a graph-theoretic property called “structural cyclicity”, for which we presented an equivalent syntax which was restricted to being without nested Kleene star operators.
The improvement in this paper is that on the system side we have an enlarged subclass called FC-matching products. On the syntax side we drop the structural cyclicity condition and do not place any restriction on the Kleene stars, thus (unlike in our earlier paper) including all regular expressions. We do have global restrictions. A “pairing” condition identifies synchronizations which will take place at run-time. Assuming a communication alphabet {a, b, c}, the expression (a + a + b)(a + c + c) the a’s in the two groups of parentheses will be paired into different synchronizations. Correspondingly we have a “matching” condition in the product systems. The matching condition produces free choice nets (and the converse also holds). Our proofs go through a subclass where communications are labelled with the place from which they are issued.
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/ .
Definition 1. 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 2 ⌃ , its locations are the set loc(a) = {i | a 2 ⌃ i}. Actions a 2 ⌃ such that |loc(a)| = 1 are called local, otherwise they are called global. A regular expression over alphabet ⌃ i defining a nonempty language is given by: s ::= a 2 ⌃ i|s1 · s2|s1 + s2|s⇤1 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 associated with regular expressions which are known since the time of Brzozowski [Brz64], Mirkin [Mir66] and Antimirov [Ant96].
For each regular expression s over ⌃ i, its initial actions form the set Init(s) = {a | av 2 Lang(s) and v 2 ⌃ i⇤ } which can be defined syntactically. Similarly, we can syntactically check whether the empty word " 2 Lang(s). Next we syntactically define derivatives [Ant96].
Definition 2. Given regular expression s and symbol a, the partial derivatives of s wrt a, written Dera(s) are defined as follows.
Dera(b) = ; if a 6= b
Dera(a) = {"} Dera(s1 + s2) = Dera(s1) [ Dera(s2)
Dera(s⇤1) = Dera(s1) · s⇤1
⇢ Dera(s1) · s2 [ Dera(s2) if " 2 Lang(s1)
Dera(s1 · s2) = Dera(s1) · s2 otherwise
Inductively Deraw(s) = Derw(Dera(s)).
The set of all derivatives Der(s) = [ Derw(s).
w2 ⌃ i⇤ We have the Antimirov derivatives Dera(ab + ac) = {b, c} and Dera(a(b + c)) = {b + c}, whereas the Brzozowski a-derivative [Brz64] (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 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). We syntactically partition the a-sites of s, each set of the partition containing those coming from a common source derivative, as follows. Definition 3. For partitions X1, X2 with blocks D1, D2 containing elements d1, d2 respectively, we use the notation (X1 [ X2)[d/d1, d2] for the modified partition ((X1 [ X2) \ {D1, D2}) [ { (D1 [ D2 [ { d}) \ {d1, d2}}.
P arta(b) = ; if a 6= b P arta(a) = {{a}}
⇢ (P arta(s1) [ P arta(s2))[s1+s2/s1, s2] if a 2 Init(s1+s2) P arta(s1+s2) = P arta(s1) [ P arta(s2) otherwise ⇢ P arta(s1)[s⇤1/s1] if a 2 Init(s1) P arta(s⇤1) = P arta(s1) · s⇤1 otherwise
⇢ P arta(s1)[s1 · s2/s1] [ P arta(s2) if " 2 Lang(s1) P arta(s1 · s2) = P arta(s1) · s2 [ P arta(s2) otherwise
The next definition and the following proposition identify the key property of this partition of a-sites for this paper.
Definition 4. Given a set of derivatives D and an action a, define the prefixes P refaD(L) = {x | xay 2 L, 9 d 2 Derx(L) \ D, " 2 Deray(d)}, suffixes SufaD(L) = {y | xay 2 L, x 2 P refaD(L)}, and the relativized language LD = {xay | xay 2 L, 9 d 2 Derx(L) \ D, " 2 Deray(d)}. We say that the derivatives in set D a-bifurcate L if LD \ ⌃ ⇤ a⌃ ⇤ = P refaD(L) a SufaD(L). If D is the set of all derivatives, we say L is a-bifurcated.
Proposition 1. Every block D of the partition P arta(s) a-bifurcates Lang(s). Proof. By induction on the definition. tu
Consider a regular expression s in the context of a distribution (⌃ 1, . . . , ⌃ k), so that some of the actions are global. The following properties of expressions will be important in this paper, where the derivatives are taken for regular expressions and also for the connected expressions defined in the next section. Definition 5. 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. It has deterministic global actions if for every global action a and every a-site d 2 Der(s), |Dera(d)| = 1. It has unique global actions if it has both these properties. 3
We have a simple syntax of connected expressions. The si can be any regular expressions (of any star-height), which is different from our earlier paper [LMP11].
e ::= 0|f sync(s1, s2, . . . , sk), si over ⌃ i When e = f sync(s1, s2, . . . , sk) and I ✓ ⌃ , let the projection e#I = ⇧ i2 I si.
For the connected expression 0, we have Lang(0) = ; . For the connected expression e = f sync(s1, s2, . . . , sk), its language is given by
Lang(e) = Lang(s1)kLang(s2)k . . . kLang(sk), where the synchronized shuffle L = L1k . . . kLk is defined by
w 2 L iff for all i 2 {1, . . . , k}, w#⌃ i 2 Li.
The definitions of derivatives can be easily extended to connected expressions. 0 has no derivatives on any action. Given e = f sync(s1, s2, . . . , sk), its derivatives are defined by induction using the derivatives of the si on action a: Dera(e) = {f sync(r1, r2, . . . , rk) | 8 i 2 loc(a), ri 2 Dera(si); otherwise rj = sj }. We will use the word derivative for expressions such as d = f sync(r1, r2, . . . , rk) above (essentially tuples of derivatives of regular expressions), and d[i] for ri. The number of derivatives can be exponential in k. Define Init(d) to be those actions a such that Dera(d) is nonempty. If a 2 Init(d) we call d an a-site. The reachable derivatives are Der(e) = {d | d 2 Derx(e), x 2 ⌃ ⇤ }. For example, f sync(ab, ba) has derivatives other than the expression itself, but none of them is reachable. 3.1
We now define some properties of connected expressions over a distribution. These will ultimately lead us to construct free choice nets. All but the last property are Ptime-checkable. The last property requires Pspace since it runs over all reachable derivatives.
Definition 6. Let e = f sync(s1, s2, . . . , sk) be a connected expression over ⌃ . For a global action a, an a-pairing is a subset of tuples ⇧ i2 loc(a)P arta(si), the projections of these tuples covering the a-sites in si, such that if a block of P arta(sj ), j 2 loc(a) appears in one tuple of the pairing, it does not appear in another tuple. (For convenience we also write pairing(a) as a subset of ⇧ i2 loc(a)Der(si) which respects the partition.) We call pairing(a) equal choice if for every tuple in the pairing, the derivatives in the tuple have equal choice. We extend the definition to connected expressions. A derivative f sync(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).
Example 1. Let (⌃ 1 = {a}, ⌃ 2 = {a}). Expression f sync(aa, a) does not have a pairing. The two a’s on the left are in different blocks of the partition and they have to pair with one block on the right, which is not allowed.
Example 2. Let (⌃ 1 = {a}, ⌃ 2 = {a, b, c, d, f }). In expression e = f sync(aa, bad+ caf ) we have two blocks on the left and two blocks on the right, so we can have a pairing. But e cannot be consistent with any pairing. Example 3. Let (⌃ 1 = {a, c}, ⌃ 2 = {b, c}), ⌃ 3 = {a, b, c}). Consider this expression f sync((ac)⇤ , (bc)⇤ , (a(b + c))⇤ ). Individual regular expressions are r1 = (ac)⇤ , r2 = (bc)⇤ and r3 = (a(b + c))⇤ . Now we have r10 = Dera(r1) = c(ac)⇤ and Init(r10) = { }
c . For r3 we have, r30 = Dera(r3) = (b + c)(a(b + c))⇤ and Init(r30) = {b, c}. r10 and r30 do not have equal choice.
Proposition 2. For a connected expression e checking existence of a pairing of actions and checking whether it is equal choice can be done in polynomial time, checking consistency with a pairing of actions is in Pspace.
Proof. We have to visit each derivative of all the regular expressions to construct the a-partitions for every a. We can record their initial actions. Maximum number of Antimirov derivatives of any regular expression s is at most wd(s) + 1 [Ant96]. There are k regular expressions in e. If the number of blocks in two apartitions is not the same, there cannot be an a-pairing, otherwise there always exists an a-pairing. For an equal choice pairing, we have to count blocks whose sets of initial actions are the same, this can be done in cubic time.
On the other hand, to check consistency with a pairing of actions, we have to visit each reachable derivative, this can be done in Pspace. tu 4
Fix a distribution (⌃ 1, ⌃ 2, . . . , ⌃ k) of ⌃ . We define product systems over this. Definition 7. A sequential system over a set of actions ⌃ i is a tuple Ai = hPi, ! i, Gi, pi0i where Pi are called places, Gi ✓ Pi are final places, pi0 2 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.
A run of the sequential system Ai on word w is a sequence p0a1p1a2, . . . , anpn, from set (Pi ⇥ ⌃ i)⇤ Pi, such that p0 = pi0 and for each j 2 {1, . . . , n}, pj 1!aj pj . This run is said to be accepting if pn 2 Gi. The sequential system Ai accepts word w, if there is at least one accepting run of Ai on w. The language L = Lang(Ai) of sequential system Ai is defined as L = {w 2 ⌃ i⇤ |w is accepted by Ai}.
Given a place p of Ai, we also define relativized languages and we will extend this definition to product systems: P refap(L) = {x | xaayy 2 L, p0! x p!ay Gi}, similarly Sufap(L), Lp = {xay | xay 2 L, p0! x p ! Gi}. Say the place p a-bifurcates L if Lp = P refap(L) a Sufap(L).
Definition 8. 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 ⇧ i2 LocPi 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 relativizations LR of a language L ✓ ⌃ i⇤ consider projections to place R[i] in Ai.
The initial product state of A is R0 = (p01, . . . , p0k), while G = ⇧ i2 LocGi denotes the final states of A.
Let ) a= ⇧ i2 loc(a) ! ia. The set of global moves of A is ) = Sa2 ⌃ ) a. Then for a global move
g = hhpl1 , a, p0l1 i, hpl2 , a, p0l2 i, . . . hplm , a, p0lm ii 2) a, loc(a) = {l1, l2, . . . , lm}, we write g[i] for hpi, a, p0ii, the projection to Ai, i 2 loc(a) and pre(a) for the product states where such a move is enabled.
Please note that the set of product states as well as the global moves are not explicitly provided when a product system is given as input to some algorithm. 4.1
The first property for a product system is modelled on the free choice property of nets. It can be checked in Ptime by counting local moves with the same label. We also define another stronger property.
Definition 9. For global a 2 ⌃ , an a-matching is a subset of tuples ⇧ i2 loc(a)Pi, such that if a place p 2 Pj , j 2 loc(a) appears in one tuple, it does not appear in another tuple. We say a product state R is in an a-matching if its projection R#loc(a) is in the matching.
A product system is said to have matching of labels if for all global a 2 ⌃ , there is an a-matching such that for i, j 2 loc(a), hp, a, qi 2! i, the pre-place p is matched to a pre-place p0 such that hp0, a, q0i 2! j and such that all pre-places with a-transitions are covered by the tuples of the matching. A product system A is said to have separation of labels if for all i 2 Loc, if hp, a, p0i, hq, a, q0i 2! i then p = q.
Proposition 3. Let A = hA1, . . . , Aki be a product system over distribution ⌃ = (⌃ 1, . . . , ⌃ k). If A has separation of labels, then for every i and every global action a, Li = Lang(Ai) is a-bifurcated. If A has matching of labels, then for every i and every global action a,
Li \ ⌃ i⇤ a⌃ i⇤ =
[ R#loc(a)2 matching(a)
Proof. Let A be a product system as above with separation of labels. Let L(q) be the set of words accepted starting from any place q in Ai. If P refa(L(q)) is nonempty then L(q) is a-bifurcated, because the words containing a have to pass through a unique place. When A has a matching of labels, since the places R[i] appear in unique tuples, one can separately consider the places a-bifurcating L(q) and the required property follows. tu
The next property is necessary for product systems to represent free choice in equivalent nets. In our earlier paper [LMP11] we used the definition of an FC-product below. The definition of FC-matching product is a generalization since conflict-equivalence is not required for all a-moves uniformly but refined into smaller equivalence classes depending on the matching. Definition 10. In a product system, we say the local move hp, a, q1i 2! i is conflict-equivalent to the local move hp0, a, q10i 2! j , if for every other local move hp, b, q2i 2! i, there is a local move hp0, b, q20i 2! j and, conversely, for moves from p0 there are moves from p. If the product system has a matching of labels and we require this whenever p, p0 are related by the matching, we call the matching conflict-equivalent. A system having a conflict-equivalent matching is a weaker condition than the system being conflict-equivalent.
We call A = hA1, . . . , Aki an FC-product if for every global action a 2 ⌃ , every a-labelled move in Ai is conflict-equivalent to every a-labelled move in Aj . We call A an FC-matching product if it has a conflict-equivalent matching.
Checking that a system is an FC-product or an FC-matching product is in Ptime because one makes a pass through all transitions with the same locations, computing for each pre-place which partition it falls into.
Proposition 4. Let A be an FC-matching product system. For any i, if there exist local moves hp, a, p0i, hp, b, p00i in ! i, then loc(a) = loc(b). Proof. Since p has an outgoing a-move, p belongs to some tuple of matching(a). If j 2 loc(a), then in this tuple there exists a state q 2 Pj , which has an outgoing a-move. Since A is an FC-matching product, matching(a) is conflict-equivalent. And, as states p and q appear in a tuple of matching(a), these states are conflictequivalent. Therefore there exists a local move (q, b, q0) 2! j . This implies that j 2 loc(b). tu 4.2
Now we describe runs of 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 2 loc(a), hR[j], a, Q[j]i 2! j and for all j 2/ loc(a), R[j] = Q[j]. Let pre(a) = {R | 9 Q, R! a Q}.
A run 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 words on which the product system has an accepting run.
We use the following characterization of direct product languages, which appears in [MR02,Muk11].
Proposition 5. L = Lang(A) is the language of product system A = hA1, . . . , Aki over distribution ⌃ iff
L = {w 2 ⌃ ⇤ | 8 i 2 {1, . . . , k}, 9 ui 2 L such that w#⌃ i = ui#⌃ i }. Further L = Lang(A1)k . . . kLang(Ak).
The next definition is semantic, new to this paper and not easy to check (in Pspace). If a system has separation of labels, the property obviously holds. Definition 11. A run of A is said to be consistent with a matching of labels if for all global actions a and every prefix of the run R0)v R)a Q, the pre-places R#loc(a) are in the matching.
In this section we prove the main theorems of the paper. To place them in context of our earlier paper [LMP11], there we used a “structural cyclicity” condition which allowed a run to be split into finite parts from the initial product state to itself, since it was guaranteed to be repeated. The new idea in this paper is that runs are split up using matchings which correspond to synchronizations, what happens in between is not relevant for the connections across sequential systems. Hence extending our syntax to allow full regular expressions for the sequential systems does not affect the synchronization properties which are the main issue we are addressing. In Section 6 we outline the connections to labelled free choice nets which are detailed in another paper [PL14]. 5.1
We begin by constructing product automata for our syntactic entities. For regular expressions, this is well known. We follow the construction of Antimirov, which in polynomial time gives us a finite automaton of size O(wd(s)), using partial derivatives as states.
Now we come to connected expressions, for which we will construct a product of automata.
Lemma 1. Let e be a connected expression with unique global action sites. Then there exists a product system A with separation of labels accepting Lang(e) as its language. If e had equal choice, then A is conflict-equivalent. Proof. Let e = f sync(s1, s2, . . . , sk). Then for each si, which is a regular expression, defined over some alphabet ⌃ i, we produce a sequential system Ai over ⌃ i, using Antimirov’s derivatives, such that Lang(si) = Lang(Ai), 8 i 2 {1, . . . , k}. Next we trim it—remove places not reachable from the initial place pi0 and places from where a final state is not reachable. Now, for each global action a, we quotient Ai by merging all derivatives d such that a 2 Init(d) into a single place.
Call the resulting automaton A0i. Let p be the merged place in A0i which is now the source of all a-transitions. Clearly Lang(Ai) ✓ Lang(A0i) since no paths are removed, we show next that the inclusion in the other direction also holds, using the unique global action sites condition.
Let a be a global action. Consider a word w = x1ax2 . . . axn in Lang(A0i), where the factors x1, x2, . . . , xn do not contain the letter a. We wish to find derivatives d0, d1, . . . , dn of Ai such that dn is a final place and for every j there is a run !dj axj+1 . . .!axn dn of Ai when j > 0, and d0 !x1! ax2 . . .!axn dn when j = 0, which will show the desired inclusion.
We proceed from n downwards. For any place dn in G there is a run from dn on " 2 Lang(dn) in Ai. Inductively assume we have dj such that there is a run !dj axj+1 . . .!axn dn of Ai, so xj+1axj+2 . . . axn is in Sufa(Lang(si)) since dj is reachable from the initial place. Since there is a run p! axj p in A0i there are derivatives dj 1, cj of e, such that there is a run dj 1! axj cj in Ai (when j = 1 we get d0!x1 c1 by this argument). Since cj quotients to p, it has an a-derivative c such that c is in Deraxja(dj 1) (Derx0a(d0) when j = 1). Because dj 1 is reachable from the initial place by some v and because some final state is reachable from c, vxj 2 P refa(Lang(si)) which is nonempty. By the unique global action sites condition and Proposition 1, since xj+1 . . . axn is in Sufa(Lang(si)), vaxj axj+1 . . . axn is in Lang(si) and so xj axj+1 . . . axn is in Sufa(Lang(si)). This means that there is a run from some dj 1 on axj axj+1 . . . axn ending in a final state dn of Ai. So we have the induction hypothesis restored. If j = 1 we get d0 which quotients to p0 and has a run on w to dn in G.
So we get a product system A0 = hA01, A02, . . . , A0ki defined over ⌃ . If the expression had equal choice, this system is conflict-equivalent. Because of the quotienting A0 has separation of labels.
w 2 Lang(e) iff 8 i, w#⌃ i 2 Lang(si), by definition iff 8 i, w#⌃ i 2 Lang(A0i) iff w 2 Lang(A0), by Proposition 5.
Theorem 1. Let e = f sync(s1, . . . , sk) be a connected expression over a distribution ⌃ with a pairing of actions. Then there exists an FC-matching product system A over ⌃ , accepting Lang(e). If the expression had deterministic sites, the constructed product will have deterministic global actions. If the pairing was equal choice, the matching is conflict-equivalent. If the expression is consistent with the pairing, all runs of A will be consistent with the matching. Proof. We first rewrite e to another expression e0, construct an automaton A0 for Lang(e0), and then change it to recover an automaton for Lang(e).
Consider global action a and tuple of blocks D = ⇧ i2 loc(a)Di ✓ pairing(a). By Proposition 1 Di a-bifurcates Lang(si). We rename for all i in loc(a), the occurrences of a in si which correspond to an a in Init(Di), by the new letter aD. This is done for all global actions to obtain from e a new expression e0 = f sync(s01, . . . , s0k) over a distribution ⌃ 0, where every s0i now has the unique sites property. For any word w 2 Lang(e), there is a well-defined word w0 2 Lang(e0).
By Lemma 1 we obtain an FC-product A0 with separation of labels for Lang(e0). Say p(aD) is the pre-place for action aD in A0 . We change all the i hp(aD), aD, qi transitions to hp(aD), a, qi in all the A0i to obtain an FC-product A over the alphabet ⌃ . As w0 2 Lang(e0) = Lang(A0) is well-defined from w and, as the renaming of transition labels does not remove any paths, w is in Lang(A). Conversely, for every run on w accepted by A, because of the separation of labels property, there is a well-defined run on w0 with the label of a transition appropriately renamed depending on the source state, which is accepted by A0, hence w0 is in Lang(e0). So renaming w0 to w gives a word in Lang(e). This construction preserves determinism.
Now we refer to the pairing of actions in e. This defines for each global action a and tuple of blocks of a-sites D, a relation between pre-places of aD-moves in different components in the product A0. By the separation of labels property of A0, the tuples in the relation are disjoint, that is, the relation is functional. So for pre-places of a-moves in the product A we have a matching. If the pairing was equal choice, the matching is conflict-equivalent.
If the expression e is consistent with the pairing, all reachable a-sites are in the pairing, so we can partition Lang(e) \ ⌃ ⇤ a⌃ ⇤ using the partitions in P arta(e). Letting D range over blocks of connected expressions, each block D contributes a global action aD in the renaming, so we get an expression e0 such that for every global action aD, we have the unique a-sites property. Applying Lemma 1, we have the product system A0 with separation of labels. By Proposition 3, every Lang(A0i) is aD-bifurcated, and using the characterization of Proposition 5, Lang(A0) \ (⌃ 0)⇤ aD(⌃ 0)⇤ = P refaD (Lang(A0))aDSufaD (Lang(A0)). Since several actions aD are renamed to a and the corresponding tuples of preplaces are recorded in the matching, by Proposition 3 and Proposition 5: [ R2 matching(a)
P refaR(Lang(A)) a SufaR(Lang(A)) ✓ Lang(A) \ ⌃ ⇤ a⌃ ⇤ .
But this means that all runs of A are consistent with the matching. tu 5.2
Lemma 2. Let A be a FC-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 FC-product had deterministic global actions, then so do the regular expressions in the computed expression. If the FC-product was conflict-equivalent, the constructed expression has equal choice. Proof. Let A = hA1, . . . , Aki be an FC-product with separation of labels, where Ai is a sequential system of A with places P , initial place p0 and final places G. Kleene’s theorem gives us an expression si for the language of Ai. We claim the required connected expression is f sync(s1, . . . , sk).
Consider global action a. By separation of labels there is a single state p in Ai enabling a. For simplicity let us assume there is only one global action a enabled at p. Let Q = P \ {p}. Let T be the set of transitions excluding the a-actions enabled at p. We wish to decompose the expression si that we started with into paths which go through p and paths which do not. Depending on whether we have a sequential transition p! a p, or transitions p! a pj , pj 6= p, or a combination of these two types, we obtain an expression with the same language as si: ep =
X ep0,f + epT0,pe⇤p,pepQ,f ,
T f2 G where the expression ep,p is given by one of the following refinements, for the three cases considered above respectively: (a + epT,p), or ((X aepTj,p) + epT,p), or (a + (X aepTj,p) + epT,p).
j j The superscripts T, Q indicates that these expressions are derived, as in the McNaughton-Yamada construction [MY60], for runs which only use the states Q or transitions T . Whichever be the case, we note that we have an expression with
Q Da(ep) = {e⇤p,pep,f } as its singleton set of a-sites. If the system had deterministic global actions, the a-site would have only had one a-derivative. This idea can be easily extended to considering several global actions enabled at the same place, by considering a different refinement of si taking into account the combined possibilities. If the product system was conflict-equivalent, the a-sites are all equal choice.
But the expression si could have been obtained by considering the place p at an arbitrary point in the McNaughton-Yamada construction. Consider ep as refining some intermediate expression s0i for the place p. The expression ep may make copies of parts of s0i. This does not affect the deterministic global actions property. For c 6= a the c-sites Dc(ep) are obtained as:
Dc(ep) = [ Dc(epT0,f ) [ Dc(epT0,p) [ Dc(ep,p) · e⇤p,p · epQ,f [ Dc(epQ,f ).
f2 G That is, P artc(ep) is preserved as a single block if it formed a single block in the earlier expressions. Thus the expression si has the unique sites property. tu Theorem 2. Let A be a FC-matching product system. Then we can compute a connected expression for the language of A, where every regular expression has a pairing of actions. If the FC-product had deterministic global actions, then so do the regular expressions in the computed expression. If the matching was conflictequivalent the pairing is equal choice. If all runs of A were consistent with the matching, the expression constructed will be consistent with the pairing. Proof. Let A be a product system with a conflict-equivalent matching. Enumerate the global actions a, b, . . . . Say the a-matching has n tuples.
We construct a new product system A0 where, for the places in the j’th tuple of the a-matching, we change the label of the outgoing a-transitions to aj ; similarly for the places in tuples of the b-matching; and so on. We now have a new product system where the letter a of the alphabet has been replaced by the set {a1, . . . , an}; the letter b has been replaced by another set; and so on, obtaining a new distribution ⌃ 0. By definition of a matching, the various labels do not interfere with each other, so we have a matching with the new alphabet, conflict-equivalent if the previous one was. Runs which were consistent with the matching continue to be consistent with the new matching. Again by the definition of matching, the new system A0 has separation of labels. Hence we can apply Lemma 2.
From the lemma we get a connected expression e0 = f sync(s1, . . . , sk) for the language of A0 over ⌃ 0 where every regular expression has unique global action sites. From the proof of the lemma we get for every sequential system A0i in the product, for the global actions a1, . . . , an, tuples D0(aj ) = ⇧ i2 loc(a)Di0(aj ) which are sites for aj in the expression si, for every j. Now substitute a for every letter a1, . . . , an in the expression, each tuple D0 is isomorphic to a tuple D of sites for a in e and the sites are disjoint from one another. We let pairing(a) be the partition formed by these tuples. Do the same for b obtaining pairing(b). Repeat this process until all the global actions have been dealt with. The result is an expression e with pairing of actions. If the matching was conflict-equivalent, the pairing has equal choice.
The runs of A have to use product states in pre(a) for global action a, define L = Lang(A) \ ⌃ ⇤ a⌃ ⇤ =
[
R2 pre(a) The renaming of transitions depends on the source state, so L is isomorphic to L0 = Lang(A0)\ (X(⌃ 0)⇤ aj (⌃ 0)⇤ ) = j [ P refaj (Lang(A0))aj Sufaj (Lang(A0)).
j=1,n Keeping Proposition 5 in our hands, the lemma ensures that Lang(A0) = Lang(e0) and the expression e0 has unique aj -sites forming a block D0(j). Then L0 can be written as [ P refaDj0(j)(Lang(e0))aj SufaDj0(j)(Lang(e0)). When we rename j=1,n the aj back to a we have a partition of pairing(a) into sets D such that L =
[ D✓ pairing(a)
If all runs of A were consistent with the matching, the product states in pre(a) would all be in the matching, and we obtain that the expression e is consistent with the pairing. tu 6
Definition 12. 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. It will be convenient to define loc(t) = loc( (t)). Elements of S [ T are called nodes of N . Given a node z of net N , set •z = {x | (x, z) 2 F } is called pre-set of z and z • = {x | (z, x) 2 F } is called post-set of z. Given a set Z of nodes of N , let •Z = Sz2 Z •z and Z • = Sz2 Z z •. We only consider nets in which every transition has nonempty pre- and post-set. Definition 13. 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 . 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 |•t| = 1 = |t •| (N 0 is an S-net [DE95]), – 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 [DE95], 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 [Hac72].
Definition 14. 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 2 ⌃ 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. 6.1
Definition 15 ([DE95]). Let x be a node of a net N . The cluster of x, denoted by [x], is the minimal set of nodes contaning 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].
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.
The next definitions will turn out to be the analogue to the separation of labels property of product systems. It is checkable in linear time. Definition 16. A labelled net N = (S, T, F, ) is said to have the unique cluster property (briefly, ucp) if 8 a 2 ⌃ having |loc(a)| > 1, there exists at most one cluster in which all transitions labelled a occur. It is deterministic for synchronization if for every a, every cluster contains at most one a-labelled transition. 6.2
For our results we are only interested in 1-bounded (or condition/event) nets, where a place is either marked or not marked. Hence we define a marking as a function from the states of a net to {0, 1}.
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 •. 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. 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 17. For a labelled net system (N, M0, G), its language is defined as Lang(N, M0, G) = { ( ) 2 ⌃ ⇤ | 2 T ⇤ and M0[ iM, for some M 2 G}.
If a net (S, T, F, ) is 1-bounded and S-decomposable then a marking can be written as a k-tuple from its components S1 ⇥ S2 ⇥ . . . ⇥ Sk. It is known [Zie87,Muk11] that if we do not enforce the “direct product” condition below we get a larger subclass of languages.
Definition 18. An S-decomposable labelled net system (N, M0, G) is an S-decomposable labelled net N = (S, T, F, ) along with an initial marking M0 and a set of markings G ✓ } (S), which is a direct product: if hq1, q2, . . . qki 2 G and hq10, q20, . . . qk0i 2 G then {q1, q10} ⇥ { q2, q20} ⇥ . . . ⇥ { qk, qk0} ✓ G . 6.3
Given a product system A = hA1, A2, . . . , Aki over distribution ⌃ , we can produce a net system (N = (S, T, F, ), M0, G) as follows using a standard construction. When we construct nets from product systems with a conflict-equivalent matching of labels with respect to which all runs are consistent, we can refine the construction above to choose T 0 ✓ T and get a free choice net. Theorem 3 ([PL14]). Let (N, M0, G) be the net system constructed from product system A above. Then N is an S-decomposable net with Lang(N, M0, G) = Lang(A). Further, if A has deterministic global actions and all runs of A are consistent with a conflict-equivalent matching of labels, we can choose T 0 ✓ T such that the subnet N 0 generated by T 0 is a free choice net with deterministic synchronization and (N 0, M0, G) accepts the same language. 6.4
Even if a net is 1-bounded and S-decomposable each component need not have only one token in it, but when we say that a 1-bounded net is S-decomposable we assume that each component has one token. For live and 1-bounded free choice nets, such S-covers can be guaranteed [DE95]. Now we can prove: Theorem 4 ([PL14]). Let (N, M0, G) be a live, 1-bounded, S-decomposable labelled free choice net system with deterministic synchronization. Then one can construct a product system A with deterministic global actions, which has a conflict-equivalent matching of labels that all its runs are consistent with. Further Lang(N, M0, G) = Lang(A). In earlier work [LMP11], we showed that a graph-theoretic condition called “structural cyclicity” enables us to extract syntax from a conflict-equivalent product system. In the present work we have generalized this condition so that we can deal with a larger class of product systems with a conflict-equivalent matching. In our paper [PL14] we show a connection between free choice nets with deterministic synchronization and product systems which have these properties along with deterministic global actions. Thus we obtain a Kleene characterization for the class of labelled free choice nets with deterministic synchronization. Acknowledgements. We would like to thank the referees of the PNSE workshop for urging us to improve the presentation of the proofs of the main theorems. This led us to invent Definition 3 and correct the site properties in Definition 5.