Canonical finite models of Kleene algebra with tests

Research output: Contribution to journalArticlepeer-review

1 Citation (Scopus)


Kleene algebra with tests (KAT) was introduced by Kozen as an extension of Kleene algebra (KA). So far, the decidability of equational formulas (p=q) and Horn formulas (∧ipi=qi→p=q) in KAT has been investigated by several authors. Continuing this line of research, the current paper studies the decidability of existentially quantified equational formulas ∃q∈P.(p=q) in KAT, where P is a fixed collection of KAT terms and plays a role as a parameter of this decision problem. To design a systematic strategy of deciding problems of this form, given in this paper is an effective procedure of constructing from each KAT term p a finite KAT model K(p) that will be called the canonical finite model of the KAT term p. Applications of this construction are presented, proving the decidability of ∃q∈P.(p=q) for several non-trivial P.

Original languageEnglish
Pages (from-to)595-616
Number of pages22
JournalJournal of Logical and Algebraic Methods in Programming
Issue number4
Publication statusPublished - Jun 2016
Externally publishedYes

All Science Journal Classification (ASJC) codes

  • Theoretical Computer Science
  • Software
  • Logic
  • Computational Theory and Mathematics


Dive into the research topics of 'Canonical finite models of Kleene algebra with tests'. Together they form a unique fingerprint.

Cite this