Concurrent Kleene Algebra with Tests (CKAT) were introduced by Peter Jipsen[Jip14]. We give derivatives for CKAT to decide word problems, for example emptiness, equivalence, containment problems. These derivative methods are expanded from derivative methods for Kleene Algebra and Kleene Algebra with Tests[Brz64][Koz08][ABM12]. Additionally, we show that the equivalence problem of CKAT is in EXPSPACE.
In this paper, we assume [Jip14, theorem 1] and we use CKAT terms as expressions of guarded series-parallel language.
Let be a set of basic program symbols p1; p2; : : : and T a set of basic boolean test symbols t1; t2; , where we assume that \ T = ∅. Each 1; 2; : : : denotes a subset of T . Boolean term b and CKAT term p over T and are defined by the following grammar, respectively.
T and any basic program p 2 w1 ⋄ w2 = w1′ w2′ undef ined (o:w:) (w1 = w1′ and w2 = w2′) In particular, if w1 = w2 = , then w1 ⋄ w2 = . 8 > 1fjw1′; w2′jg 2 (w1 = 1w1′ 2 and w2 = 1w2′ 2) w1 ∥ w2 = <
(w1 = w2 = ) >:undef ined (o:w:)
L is a map from CKAT terms over and T to this concrete model by – L(0) = ∅, L(1) = 2T – L(t) = f T j t 2 g for t 2 T – L(b) = 2T n L(b) – L(p) = f 1p 2 j 1; 2 T g for p 2 – L(p1 + p2) = L(p1) [ L(p2) – L(p1p2) = fw1 ⋄ w2 j w1 2 G(p1) and w2 2 L(p2) and w1 ⋄ w2 is defined g – L(p ) = ∪ f 0 ⋄ w1 ⋄ ⋄ wn j 0 T and w1; : : : ; wn 2 L(p) and 0 ⋄ w1 n<! – L(p1 ∥ p2) = fw1 ∥ w2 j w1 2 L(p1) and w2 2 L(p2) and w1 ∥ w2 is defined g We expand L to L(P ) = ∪p2P L(p), where P is a set of CKAT terms. Furthermore, let L (p) = f w j w 2 L(p)g. ⋄ wn is defined g
In guarded series-parallel strings, 1fjw1; w2jg 2 has commutative(i.e. 1fjw1; w2jg 2 = 1fjw2; w1jg 2). We define p1 = p2 for two CKAT terms p1 and p2 as L(p1) = L(p2) (by means of [Jip14, Theorem 1]). 2 The Brzozowski derivative for CKAT Now, we give the naive derivative for CKAT. Derivative has applications to many language theoretic problems (e.g. membership problem, emptiness problem, equivalence problem, and so on).
Definition 2 (Naive Derivative). We define E and Dw. They are maps from a CKAT term to a set of CKAT terms, respectively. E is inductively defined as follows. We expand E and Dw to E (P ) = ∪p2P E (p) and Dw(P ) = ∪p2P Dw(p), where P is a set of CKAT terms, respectively.
– E (0) = E (p) = ∅ – E (1) = E (p1) = f1g – E (t) = {f1g (t 2 )
(o:w:) ∅ – E (b) = f1g n E (b) – E (p1 + p2) = E (p1) [ E (p2) – E (p1p2) = E (p1 ∥ p2) = E (p1)E (p2)
For w = q j fjw1′; w2′jg and any series-parallel string w′, – D w ′w′ ′′ (p) = D ′w′ ′′ (D w ′ (p)) – D w ′ (p1 + p2) = D w ′ (p1) [ D w ′ (p2) – D w ′ (p1p2) = D w ′ (p1)fp2g [ E (p1)D w ′ (p2) – D w ′ (p1) = D w ′ (p1)fp1g – D w ′ (b) = ∅ for any boolean term b – D q ′ (p) =
∅ – D q ′ (p1 ∥ p2) = ∅ {f1g (p = q) (o:w:) – D fjw1;w2jg ′ (p) = ∅ – D fjw1;w2jg ′ (p1 ∥ p2) = E ′ ((D w1 ′ (p1) ∥ D w2 ′ (p2)) [ (D w1 ′ (p2) ∥ D w2 ′ (p1)))
GS ;T with regard to w 2 GS ;T is the set w 1L =
fw′ j w ⋄ w′ 2 Lg.
Lemma 1. For any series-parallel string w ′, 1. 1 2 E (p) () 2 L (p) 2. ( w ′) 1L (p) = L ′ (D w ′ (p)) Proof (Sketch). 1. is proved by induction on the size of p.
2. is proved by double induction on the size of w and the size of p.
We can decide whether w ′ 2 L(p) to check 1 2 E ′ (D w ′ (p)) by Lemma 1. We now define efficient derivative. This derivative is another definition of derivative for CKAT. This derivative is useful for giving more efficient algorithm than naive derivative in computational complexity. (In naive derivative, we should memorize w1 and w2 to get D fjw1;w2jg ′ (p). In particular, the size of w1 and w2 can be double exponential size of input size in equivalence problem.) We expand CKAT terms to express efficient derivative. We say these terms intermediate CKAT terms. Intermediate CKAT term is defined as following. Definition 3 (intermediate CKAT term). Intermediate CKAT term is defined by the following grammar.
q := b j p 2
j q1 + q2 j q1q2 j q1 j q1 ∥ q2 j Dx(q1)
The efficient derivative dpr(q) is defined in Definition 4, where q is an intermediate CKAT term, pr is a sequence of assignments formed x += p or x += T (The sequence of assignments pr is formed x1 += term1; : : : ; xm += termm.) and T is formed by the following grammar. T := fjxlTl; xrTrjg j fjxlTl; prxrjg j fjplxl; xrTrjg j fjplxl; prxrjg. Intuitively, dx+= w(: : : Dx(q) : : : ) means (: : : Dx(D w(join (q))) : : : ).
Definition 4. The efficient derivative dpr(q) is inductively defined as follows, where we assume that any derivative variable occurred in T are different. To define dpr(q), we also define D w and join . We expand dpr to dpr(Q) = ∪q2Q dpr(q), where Q is a set of intermediate CKAT terms. We also expand join to join (Q) = ∪q2Q join (q). – dx+= w;pr′ (q) = dpr′ (dx+= w(q)) – dx+= w(b) = fbg – dx+= w(p) = fpg – dx+= w(q1 + q2) = dx+= w(q1) [ dx+= w(q2) – dx+= w(q1q2) = dx+= w(q1)dx+= w(q2) – dx+= w(q1 ) = dx+= w(q1)
(= fq′ j q′ 2 dx:= w(q1)g) – dx+= w(q1 ∥ q2) = dx+= w(q1) ∥ dx+= w(q2)
(= fq1′ ∥ q2′ j q1′ 2 dx+= w(q1); q2′ 2 dx+= w(q2)g) – dx+= w(Dy(q1)) = Dy(dx+= w(q1)) – dx+= w(Dx(q1)) = Dx(D w(join (q1))) – D p(q) = D p(q) – D T (b) = D T (p) = ∅ – D T (q1 + q2) = D T (q1) [ D T (q2) – D T (q1q2) = D T (q1)fq2g [ E (q1)D T (q2) – D T (q1 ) = D T (q1)fq1 g >8(Dxl (D pl (q1)) ∥ Dxr (D pr (q2))) > > >>>[(Dxr (D pr (q1)) ∥ Dxl (D pl (q2))) (T = fjplxl; prxrjg) > >>>(Dxl (D Tl (q1)) ∥ Dxr (D pr (q2))) > > <>[(Dxr (D pr (q1)) ∥ Dxl (D Tl (q2))) (T = fjTlxl; prxrjg) >(Dxl (D pl (q1)) ∥ Dxr (D Tr (q2))) > > >>>[(Dxr (D Tr (q1)) ∥ Dxl (D pl (q2))) (T = fjplxl; Trxrjg) > >>>(Dxl (D Tl (q1)) ∥ Dxr (D Tr (q2))) > > > :[(Dxr (D Tr (q1)) ∥ Dxl (D Tl (q2))) (T = fjTlxl; Trxrjg) – join (b) = fbg, join (p) = fpg – join (q1 + q2) = join (q1) [ join (q2), join (q1q2) = join (q1)join (q2) – join (q1 ∥ q2) = join (q1) ∥ join (q2) – join (q1 ) = join (q1) – join (Dy(q)) = E (join (q))
Efficient derivative is essentially equal to the derivative of Definition 1. Let spx(pr) be the string corresponded to x of pr. (For example, spx0 (x0 += fp1x1; p2x2g; x1 += ′p3; x0 += ′′p4) = fp1 ′p3; p2g ′′p4. spx1 (x0 += fp1x1; p2x2g; x1 += ′p3; x0 += ′′p4) = p1 ′p3) Lemma 2. join ′ (dpr(Dx(p))) = E ′ (Dspx(pr) ′ (p))
By Lemma 1 and Lemma 2, spx(pr) ′ 2 L(p) () 1 2 join ′ (dpr(Dx(p))). Therefore, we can use effective derivative instead of naive derivative.
Next, we define the size of a intermediate CKAT term q, denoted by jqj as follows.
– j0j = j1j = jtj = jpj = 1 – jbj = 1 + jbj – jq1 j = jDx(q1)j = 1 + jq1j Definition 5 (Closure). ClX is a map from a intermediate CKAT term to a set of intermediate CKAT terms, where X is a set of intersection variables. ClX is inductively defined as follows.
– ClX (a) = fag for a = 0 j 1 j t – ClX (b) = fbg [ ClX (b) for any boolean term b – ClX (p) = fp; 1g – ClX (q1 + q2) = fq1 + q2g [ ClX (q1) [ ClX (q2) – ClX (q1q2) = fq1q2g [ ClX (q1)fq2g [ ClX (q2) – ClX (q1 ) = fq1 g [ ClX (q1)fq1 g – ClX (q1 ∥ q2) = fq1 ∥ q2g [ fDx1 (q1′) ∥ Dx2 (q2′) j q1′ 2 ClX (q1); q2′ 2
ClX (q2); x1; x2 2 Xg – ClX (Dx(q1)) = fDx(q1)g [ Dx(ClX (q1)) We expand ClX to ClX (Q) = ∪q2Q ClX (q), where Q is a set of intermediate CKAT terms. ClX is a closed operator. In other words, ClX satisfies (1) Q ClX (Q), (2) Q1 Q2 ) ClX (Q1) ClX (Q2) and (3) ClX (ClX (Q)) = ClX (Q). We also define the intersection width iw(q) over intermediate CKAT terms and iw(w) over GI ;T as follows.
– iw(b) = iw(p) = 1 for any boolean term b and any basic program p 2 – iw(q1 + q2) = iw(q1q2) = max(iw(q1); iw(q2)) – iw(q1 ) = iw(Dx(q1)) = iw(q1) – iw(q1 ∥ q2) = 1 + iw(q1) + iw(q2) – iw( ) = 1 for any T – iw( 1p 2) = 1 – iw(w1 w2) = max(iw(w1 ); iw( w2)) – iw( 1fjw1; w2jg 2) = 1 + iw(w1) + iw(w2) Lemma 3 (closure is bounded). For any intermediate CKAT term q and any sequence of program pr and any set of derivative variables X, where X contains any derivative variables in pr, jClX (q)j 2 jXj2 iw(q) q iw(q) j j Proof (Sketch). This is proved by induction on the structure of q. We only consider the case of q = q1 ∥ q2. jClX (q1 ∥ q2)j 1 + jXj jClX (q1)j jXj jClX (q2)j 1 + jXj2 2 jq1jiw(q1) jXj2 iw(q1) = 1 + 4 jXj2 iw(q1∥q2) jq1jiw(q1)
jq2jiw(q2) 2 jXj2 iw(q1∥q2) (jq1j + jq2j)iw(q1)+iw(q2) 2 jXj2 iw(q1∥q2) jq1 ∥ q2jiw(q1∥q2) 2 jq2jiw(q2) jXj2 iw(q2) Lemma 4 (derivative is closed). For any intermediate CKAT term q and any sequence of program pr and any set of derivative variables X, where X contains any derivative variables in pr,
dpr(q) ClX (q) Proof (Sketch). This is proved by double induction on the size of pr and the size of q.
CKAT equational theory is in EXPSPACE By Lemma 1 and Lemma 2, L(p1) = L(p2) iff join ′ (dpr(Dx(p1))) = join ′ (dpr(Dx(p2))) for any pr and any ′. Thus we find some pr such that join ′ (dpr(Dx(p1))) ̸= join ′ (dpr(Dx(p2))) to decide p1 ̸= p2. We must consider all the patterns of pr at first glance. But, we need not to check if pr is too long. We are enough to check the cases of iw(sp(pr)) max(iw(p1); iw(p2))( l) by the following Lemma 5. Lemma 5. If iw(sp(pr)) > iw(q), dpr(q) = ∅.
By Lemma 5, we are enough to check the case of iw(sp(pr)) max(iw(p1); iw(p2)) l. By iw(sp(pr)) l, We are enough to prepare 1 + 3 (l 1) derivative variables. By Lemma 3, jClX (q)j 2 jqjiw(q) jXj2 iw(q) 2 ll (1 + 3 (l 1))2 l. Therefore, jClX (Dx(p1))j = O(2p(l)) and jClX (Dx(p2))j = O(2p(l)), where p(l) is a polynomial function of l.
We can give a nondeterministic algorithm. We nondeterministically select the syntax of pr. (pr is x += p or x += T .) If there exists a sequent of assignments pr and ′ such that join ′ (dpr(Dx(p1))) ̸= join ′ (dpr(Dx(p2))), p1 ̸= p2. Otherwise, p1 = p2. (See Algorithm 1 if you know more details.)
It holds the Theorem 1 by this algorithm.
Theorem 1. CKAT equivalence problem is in EXPSPACE.
Corollary 1. if iw(p) is a fixed parameter, then CKAT equivalence problem is PSPACEcomplete.
Note that PSPACE-hardness is derived by [Hun73]. 4
Concluding Remarks We have given the derivative for CKAT and shown that CKAT equational theory is in EXPSPACE. We finish with the following some of our future works. – Is this equivalence problem EXPSPACE-complete? (We expect that this claim is T rue.) – If we allow ϵ (for example, fjp; ϵjg ), can we give efficient derivative? (It become a little difficult because we have to memorize in the case of x += fjp1x1; ϵjg. We should give another derivative to show the result like Corollary 1.)
Algorithm 1 Decide p1 = p2, given two CKAT terms p1 and p2
T , which is picked up nondeterministically, where [ABM12] [Hun73] [Koz08]