A modified completeness theorem of KAT and decidability of term reducibility

Takeo Uramoto

doi:10.1007/978-3-319-06251-8_6

A modified completeness theorem of KAT and decidability of term reducibility

Takeo Uramoto

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

1 Citation (Scopus)

Abstract

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 ∧_ip_i = q_i → 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.

Original language	English
Title of host publication	Relational and Algebraic Methods in Computer Science - 14th International Conference, RAMiCS 2014, Proceedings
Publisher	Springer Verlag
Pages	83-100
Number of pages	18
ISBN (Print)	9783319062501
DOIs	https://doi.org/10.1007/978-3-319-06251-8_6
Publication status	Published - 2014
Externally published	Yes
Event	14th International Conference on Relational and Algebraic Methods in Computer Science, RAMiCS 2014 - Marienstatt, Germany Duration: Apr 28 2014 → May 1 2014

Publication series

Name	Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume	8428 LNCS
ISSN (Print)	0302-9743
ISSN (Electronic)	1611-3349

Conference

Conference	14th International Conference on Relational and Algebraic Methods in Computer Science, RAMiCS 2014
Country/Territory	Germany
City	Marienstatt
Period	4/28/14 → 5/1/14

All Science Journal Classification (ASJC) codes

Theoretical Computer Science
Computer Science(all)

Access to Document

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

Cite this

Uramoto, T. (2014). A modified completeness theorem of KAT and decidability of term reducibility. In Relational and Algebraic Methods in Computer Science - 14th International Conference, RAMiCS 2014, Proceedings (pp. 83-100). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 8428 LNCS). Springer Verlag. https://doi.org/10.1007/978-3-319-06251-8_6

A modified completeness theorem of KAT and decidability of term reducibility. / Uramoto, Takeo.
Relational and Algebraic Methods in Computer Science - 14th International Conference, RAMiCS 2014, Proceedings. Springer Verlag, 2014. p. 83-100 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 8428 LNCS).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

Uramoto, T 2014, A modified completeness theorem of KAT and decidability of term reducibility. in Relational and Algebraic Methods in Computer Science - 14th International Conference, RAMiCS 2014, Proceedings. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 8428 LNCS, Springer Verlag, pp. 83-100, 14th International Conference on Relational and Algebraic Methods in Computer Science, RAMiCS 2014, Marienstatt, Germany, 4/28/14. https://doi.org/10.1007/978-3-319-06251-8_6

Uramoto T. A modified completeness theorem of KAT and decidability of term reducibility. In Relational and Algebraic Methods in Computer Science - 14th International Conference, RAMiCS 2014, Proceedings. Springer Verlag. 2014. p. 83-100. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). doi: 10.1007/978-3-319-06251-8_6

Uramoto, Takeo. / A modified completeness theorem of KAT and decidability of term reducibility. Relational and Algebraic Methods in Computer Science - 14th International Conference, RAMiCS 2014, Proceedings. Springer Verlag, 2014. pp. 83-100 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).

@inproceedings{2792f92ba49944cba86de7b6384f20ac,

title = "A modified completeness theorem of KAT and decidability of term reducibility",

abstract = "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.",

author = "Takeo Uramoto",

year = "2014",

doi = "10.1007/978-3-319-06251-8_6",

language = "English",

isbn = "9783319062501",

series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",

publisher = "Springer Verlag",

pages = "83--100",

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

address = "Germany",

note = "14th International Conference on Relational and Algebraic Methods in Computer Science, RAMiCS 2014 ; Conference date: 28-04-2014 Through 01-05-2014",

}

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 -

A modified completeness theorem of KAT and decidability of term reducibility

Abstract

Publication series

Conference

All Science Journal Classification (ASJC) codes

Access to Document

Other files and links

Fingerprint

Cite this