Decision Methods for Concurrent Kleene Algebra with Tests : Based on Derivative Yoshiki Nakamura Tokyo Instutute of Technology, Oookayama, Meguroku, Japan, nakamura.y.ay@m.titech.ac.jp Abstract. Concurrent Kleene Algebra with Tests (CKAT) were introduced by Peter Jipsen[Jip14]. We give derivatives for CKAT to decide word prob- lems, for example emptiness, equivalence, containment problems. These derivative methods are expanded from derivative methods for Kleene Al- gebra and Kleene Algebra with Tests[Brz64][Koz08][ABM12]. Addition- ally, we show that the equivalence problem of CKAT is in EXPSPACE. Keywords: concurrent kleene algebras with tests, series-parallel strings, Brzozowski derivative, computational complexity 1 Introduction In this paper, we assume [Jip14, theorem 1] and we use CKAT terms as expres- sions 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 , . . . de- notes a subset of T . Boolean term b and CKAT term p over T and Σ are defined by the following grammar, respectively. b := 0 | 1 | t ∈ T | b1 + b2 | b1 b2 | b1 p := b | p ∈ Σ | p1 + p2 | p1 p2 | p∗1 | p1 ∥ p2 The guarded series-parallel strings set GSΣ,T over Σ and T is a smallest set such that follows – α ∈ GSΣ,T for any α ⊆ T – α1 pα2 ∈ GSΣ,T for any α1 , α2 ⊆ T and any basic program p ∈ Σ – if w1 α, αw2 ∈ GSΣ,T , then w1 αw2 ∈ GSΣ,T . – if α1 w1 α2 , α1 w2 α2 ∈ GSΣ,T , then α1 {|w1 , w2 |}α2 ∈ GSΣ,T . Definition 1 (guarded series-parallel language). Let ⋄ and ∥ be binary operators over GSΣ,T , respectably. { They are defined as follows. w1′ αw2′ (w1 = w1′ α and w2 = αw2′ ) w1 ⋄ w2 = undef ined (o.w.) In particular, if w1 = w2 = α, then w1 ⋄ w2 = α. 2 Y. Nakamura   ′ ′ ′ ′ α1 {|w1 , w2 |}α2 (w1 = α1 w1 α2 and w2 = α1 w2 α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) = {α ⊆ T | t ∈ α} for t ∈ T – L(b) = 2T \ L(b) – L(p) = {α1 pα2 | α1 , α2 ⊆ T } for p ∈ Σ – L(p1 + p2 ) = L(p1 ) ∪ L(p2 ) – L(p1 p2 ) =∪{w1 ⋄ w2 | w1 ∈ G(p1 ) and w2 ∈ L(p2 ) and w1 ⋄ w2 is defined } – L(p∗ ) = {α0 ⋄ w1 ⋄ · · · ⋄ wn | α0 ⊆ T and w1 , . . . , wn ∈ L(p) and α0 ⋄ w1 · · · ⋄ wn is defined } n<ω – L(p1 ∥ p2 ) = {w1 ∥ w2 | w1 ∈ L(p1 ) and w2 ∈ L(p2 ) and w1 ∥ w2 is defined } ∪ We expand L to L(P ) = p∈P L(p), where P is a set of CKAT terms. Furthermore, let Lα (p) = {αw | αw ∈ L(p)}. In guarded series-parallel strings, α1 {|w1 , w2 |}α2 has commutative(i.e. α1 {|w1 , w2 |}α2 = α1 {|w2 , w1 |}α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 prob- lem, 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 fol- lows. We expand Eα and Dw to E α (P ) = p∈P Eα (p) and Dw (P ) = p∈P Dw (p), where P is a set of CKAT terms, respectively. – Eα (0) = Eα (p) = ∅ – Eα (1) = { Eα (p∗1 ) = {1} {1} (t ∈ α) – Eα (t) = ∅ (o.w.) – Eα (b) = {1} \ Eα (b) – Eα (p1 + p2 ) = Eα (p1 ) ∪ Eα (p2 ) – Eα (p1 p2 ) = Eα (p1 ∥ p2 ) = Eα (p1 )Eα (p2 ) Dw is inductively defined as follows. For w = q | {|w1′ , w2′ |} 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α′ (p1 p2 ) = Dαwα′ (p1 ){p2 } ∪ Eα (p1 )Dαwα′ (p2 ) CKAT is in EXPSPACE 3 – Dαwα′ (p∗1 ) = Dαwα′ (p1 ){p∗1 } – Dαwα′ (b) = ∅ for any boolean term b { {1} (p = q) – Dαqα′ (p) = ∅ (o.w.) – Dαqα′ (p1 ∥ p2 ) = ∅ – Dα{|w1 ,w2 |}α′ (p) = ∅ – Dα{|w1 ,w2 |}α′ (p1 ∥ p2 ) = Eα′ ((Dαw1 α′ (p1 ) ∥ Dαw2 α′ (p2 )) ∪ (Dαw1 α′ (p2 ) ∥ Dαw2 α′ (p1 ))) The left-quotient of L ⊆ GSΣ,T with regard to w ∈ GSΣ,T is the set w−1 L = {w | w ⋄ w′ ∈ L}. ′ Lemma 1. For any series-parallel string αwα′ , 1. 1 ∈ Eα (p) ⇐⇒ α ∈ Lα (p) 2. (αwα′ )−1 Lα (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α′ ∈ L(p) to check 1 ∈ 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 algo- rithm than naive derivative in computational complexity. (In naive derivative, we should memorize w1 and w2 to get Dα{|w1 ,w2 |}α′ (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 in- termediate 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 | p ∈ Σ | q1 + q2 | q1 q2 | q1∗ | q1 ∥ q2 | Dx (q1 ) We call x a derivative variable of Dx (q1 ). The efficient derivative dpr (q) is defined in Definition 4, where q is an in- termediate 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 := {|xl Tl , xr Tr |} | {|xl Tl , pr xr |} | {|pl xl , xr Tr |} | {|pl xl , pr xr |}. 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) = q∈Q dpr (q), where Q is a set ∪ of intermediate CKAT terms. We also expand joinα to joinα (Q) = q∈Q joinα (q). 4 Y. Nakamura – dx+=αw;pr′ (q) = dpr′ (dx+=αw (q)) – dx+=αw (b) = {b} – dx+=αw (p) = {p} – dx+=αw (q1 + q2 ) = dx+=αw (q1 ) ∪ dx+=αw (q2 ) – dx+=αw (q1 q2 ) = dx+=αw (q1 )dx+=αw (q2 ) – dx+=αw (q1∗ ) = dx+=αw (q1 )∗ (= {q ′∗ | q ′ ∈ dx:=αw (q1 )}) – dx+=αw (q1 ∥ q2 ) = dx+=αw (q1 ) ∥ dx+=αw (q2 ) (= {q1′ ∥ q2′ | q1′ ∈ dx+=αw (q1 ), q2′ ∈ dx+=αw (q2 )}) – 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 (q1 q2 ) = D̆αT (q1 ){q2 } ∪ Eα (q1 )D̆αT (q2 ) – D̆αT (q1∗ ) = D̆αT (q1 ){q1∗ }  (Dxl (D̆αpl (q1 )) ∥ Dxr (D̆αpr (q2 )))    ∪(Dxr (D̆αpr (q1 )) ∥ Dxl (D̆αpl (q2 ))) (T = {|pl xl , pr xr |})    (Dxl (D̆αTl (q1 )) ∥ Dxr (D̆αpr (q2 )))    ∪(D (D̆ (q )) ∥ D (D̆ (q ))) (T = {|T x , p x |}) xr αpr 1 xl αTl 2 l l r r – D̆αT (q1 ∥ q2 ) =   (D ( D̆ (q )) ∥ D ( D̆ (q )))   xl αpl 1 xr αTr 2   ∪(D ∥ αpl (q2 ))) (T = {|pl xl , Tr xr |})   x (D̆ αT (q1 )) D x (D̆  r r l  (Dxl (D̆αTl (q1 )) ∥ Dxr (D̆αTr (q2 )))    ∪(Dxr (D̆αTr (q1 )) ∥ Dxl (D̆αTl (q2 ))) (T = {|Tl xl , Tr xr |}) – joinα (b) = {b}, joinα (p) = {p} – joinα (q1 + q2 ) = joinα (q1 ) ∪ joinα (q2 ), joinα (q1 q2 ) = 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 += α{p1 x1 , p2 x2 }; x1 += α′ p3 ; x0 += α′′ p4 ) = α{p1 α′ p3 , p2 }α′′ p4 . spx1 (x0 += α{p1 x1 , p2 x2 }; x1 += α′ p3 ; x0 += α′′ p4 ) = αp1 α′ p3 ) Lemma 2. joinα′ (dpr (Dx (p))) = E α′ (Dspx (pr)α′ (p)) By Lemma 1 and Lemma 2, spx (pr)α′ ∈ L(p) ⇐⇒ 1 ∈ 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 |q| as follows. – |0| = |1| = |t| = |p| = 1 – |b| = 1 + |b| – |q1∗ | = |Dx (q1 )| = 1 + |q1 | CKAT is in EXPSPACE 5 – |q1 + q2 | = |q1 q2 | = |q1 ∥ q2 | = 1 + |q1 | + |q2 | Definition 5 (Closure). ClX is a map from a intermediate CKAT term to a set of in- termediate CKAT terms, where X is a set of intersection variables. ClX is inductively defined as follows. – ClX (a) = {a} for a = 0 | 1 | t – ClX (b) = {b} ∪ ClX (b) for any boolean term b – ClX (p) = {p, 1} – ClX (q1 + q2 ) = {q1 + q2 } ∪ ClX (q1 ) ∪ ClX (q2 ) – ClX (q1 q2 ) = {q1 q2 } ∪ ClX (q1 ){q2 } ∪ ClX (q2 ) – ClX (q1∗ ) = {q1∗ } ∪ ClX (q1 ){q1∗ } – ClX (q1 ∥ q2 ) = {q1 ∥ q2 } ∪ {Dx1 (q1′ ) ∥ Dx2 (q2′ ) | q1′ ∈ ClX (q1 ), q2′ ∈ ClX (q2 ), x1 , x2 ∈ X} – ClX (Dx (q1 )) = {Dx (q1 )} ∪ Dx (ClX (q1 )) ∪ We expand ClX to ClX (Q) = q∈Q 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 ∈ Σ – iw(q1 + q2 ) = iw(q1 q2 ) = 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(α1 pα2 ) = 1 – iw(w1 αw2 ) = max(iw(w1 α), iw(αw2 )) – iw(α1 {|w1 , w2 |}α2 ) = 1 + iw(w1 ) + iw(w2 ) Lemma 3 (closure is bounded). For any intermediate CKAT term q and any se- quence of program pr and any set of derivative variables X, where X contains any derivative variables in pr, |ClX (q)| ≤ 2 ∗ |X|2∗iw(q) ∗ |q|iw(q) Proof (Sketch). This is proved by induction on the structure of q. We only consider the case of q = q1 ∥ q2 . |ClX (q1 ∥ q2 )| ≤ 1 + |X| ∗ |ClX (q1 )| ∗ |X| ∗ |ClX (q2 )| ≤ 1 + |X|2 ∗ 2 ∗ |q1 |iw(q1 ) ∗ |X|2∗iw(q1 ) ∗ 2 ∗ |q2 |iw(q2 ) ∗ |X|2∗iw(q2 ) = 1 + 4 ∗ |X|2∗iw(q1 ∥q2 ) ∗ |q1 |iw(q1 ) ∗ |q2 |iw(q2 ) ≤ 2 ∗ |X|2∗iw(q1 ∥q2 ) ∗ (|q1 | + |q2 |)iw(q1 )+iw(q2 ) ≤ 2 ∗ |X|2∗iw(q1 ∥q2 ) ∗ |q1 ∥ q2 |iw(q1 ∥q2 ) Lemma 4 (derivative is closed). For any intermediate CKAT term q and any se- quence 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. 6 Y. Nakamura 3 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 vari- ables. By Lemma 3, |ClX (q)| ≤ 2 ∗ |q|iw(q) ∗ |X|2∗iw(q) ≤ 2 ∗ ll ∗ (1 + 3 ∗ (l − 1))2∗l . Therefore, |ClX (Dx (p1 ))| = O(2p(l) ) and |ClX (Dx (p2 ))| = 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 assign- ments 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 PSPACE- complete. Note that PSPACE-hardness is derived by [Hun73]. 4 Concluding Remarks We have given the derivative for CKAT and shown that CKAT equational the- ory 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, α{|p, ϵ|}α), can we give efficient derivative? (It become a little difficult because we have to memorize α in the case of x += α{|p1 x1 , ϵ|}. We should give another derivative to show the result like Corollary 1.) A Pseudo Code REFERENCES 7 Algorithm 1 Decide p1 = p2 , given two CKAT terms p1 and p2 Ensure: Whether p1 ̸= p2 or not?(True or False) step ⇐ 0, P1 ⇐ {Dx0 (p1 )}, P2 ⇐ {Dx0 (p2 )} while step ≤ 2|ClX (Dx0 (p1 ))| ∗ 2|ClX (Dx0 (p2 ))| do Let α be a subset of T , which is picked up nondeterministically. if joinα (P1 ) ̸= joinα (P2 ) then return T rue end if Let pr be x += αp or x += αT , which is picked up nondeterministically, where iw(pr) ≤ max(iw(p1 ), iw(p2 )). step ⇐ step + 1, P1 ⇐ dpr (P1 ), P2 ⇐ dpr (P2 ) end while return F alse References [ABM12] Ricardo Almeida, Sabine Broda, and Nelma Moreira. “Deciding KAT and Hoare Logic with Derivatives”. In: Proceedings Third Interna- tional Symposium on Games, Automata, Logics and Formal Verification, GandALF 2012, Napoli, Italy, September 6-8, 2012. 2012, pp. 127–140. [Brz64] Janusz A Brzozowski. “Derivatives of regular expressions”. In: Jour- nal of the ACM (JACM) 11.4 (1964), pp. 481–494. [Hun73] Harry B Hunt III. “On the time and tape complexity of languages I”. In: Proceedings of the fifth annual ACM symposium on Theory of com- puting. ACM. 1973, pp. 10–19. [Jip14] Peter Jipsen. “Concurrent Kleene algebra with tests”. In: Relational and Algebraic Methods in Computer Science. Springer, 2014, pp. 37–48. [Koz08] Dexter Kozen. On the Coalgebraic Theory of Kleene Algebra with Tests. Tech. rep. http://hdl.handle.net/1813/10173. Computing and Information Science, Cornell University, Mar. 2008.