TY - GEN

T1 - A modified completeness theorem of KAT and decidability of term reducibility

AU - Uramoto, Takeo

PY - 2014

Y1 - 2014

N2 - Kleene algebra with tests (KAT) was introduced by Kozen as an extension of Kleene algebra (KA). The decidability of equational formulas p = q and Horn formulas ∧ipi = qi → p = q in KAT has been studied so far by several researchers. Continuing this line of research, this paper studies the decidability of existentially quantified equational formulas ∃q ∈ P. (p = q) in KAT, where P is a fixed collection of KAT terms. A new completeness theorem of KAT is proved, and via the completeness theorem, the decision problem of ∃q ∈ P. (p = q) is reduced to a certain membership problem of regular languages, to which a pseudo-identity- based decision method is applicable. Based on this reduction, an instance of the problem is studied and shown to be decidable.

AB - Kleene algebra with tests (KAT) was introduced by Kozen as an extension of Kleene algebra (KA). The decidability of equational formulas p = q and Horn formulas ∧ipi = qi → p = q in KAT has been studied so far by several researchers. Continuing this line of research, this paper studies the decidability of existentially quantified equational formulas ∃q ∈ P. (p = q) in KAT, where P is a fixed collection of KAT terms. A new completeness theorem of KAT is proved, and via the completeness theorem, the decision problem of ∃q ∈ P. (p = q) is reduced to a certain membership problem of regular languages, to which a pseudo-identity- based decision method is applicable. Based on this reduction, an instance of the problem is studied and shown to be decidable.

UR - http://www.scopus.com/inward/record.url?scp=84901707367&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=84901707367&partnerID=8YFLogxK

U2 - 10.1007/978-3-319-06251-8_6

DO - 10.1007/978-3-319-06251-8_6

M3 - Conference contribution

AN - SCOPUS:84901707367

SN - 9783319062501

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 83

EP - 100

BT - Relational and Algebraic Methods in Computer Science - 14th International Conference, RAMiCS 2014, Proceedings

PB - Springer Verlag

T2 - 14th International Conference on Relational and Algebraic Methods in Computer Science, RAMiCS 2014

Y2 - 28 April 2014 through 1 May 2014

ER -