=Paper=
{{Paper
|id=Vol-1454/ramics15-st_1-8
|storemode=property
|title=Decision Methods for Concurrent Kleene Algebra with Tests: Based on Derivative
|pdfUrl=https://ceur-ws.org/Vol-1454/ramics15-st_1-8.pdf
|volume=Vol-1454
}}
==Decision Methods for Concurrent Kleene Algebra with Tests: Based on Derivative==
https://ceur-ws.org/Vol-1454/ramics15-st_1-8.pdf
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.