A modified completeness theorem of KAT and decidability of term reducibility

Research output: Chapter in Book/Report/Conference proceedingConference 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 ∧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.

Original languageEnglish
Title of host publicationRelational and Algebraic Methods in Computer Science - 14th International Conference, RAMiCS 2014, Proceedings
PublisherSpringer Verlag
Pages83-100
Number of pages18
ISBN (Print)9783319062501
DOIs
Publication statusPublished - 2014
Externally publishedYes
Event14th International Conference on Relational and Algebraic Methods in Computer Science, RAMiCS 2014 - Marienstatt, Germany
Duration: Apr 28 2014May 1 2014

Publication series

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

Conference

Conference14th International Conference on Relational and Algebraic Methods in Computer Science, RAMiCS 2014
CountryGermany
CityMarienstatt
Period4/28/145/1/14

All Science Journal Classification (ASJC) codes

  • Theoretical Computer Science
  • Computer Science(all)

Fingerprint Dive into the research topics of 'A modified completeness theorem of KAT and decidability of term reducibility'. Together they form a unique fingerprint.

Cite this