TY - JOUR

T1 - Canonical finite models of Kleene algebra with tests

AU - Uramoto, Takeo

N1 - Publisher Copyright:
© 2015 Elsevier Inc.

PY - 2016/6

Y1 - 2016/6

N2 - 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.

AB - 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.

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

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

U2 - 10.1016/j.jlamp.2015.11.001

DO - 10.1016/j.jlamp.2015.11.001

M3 - Article

AN - SCOPUS:85074240261

VL - 85

SP - 595

EP - 616

JO - Journal of Logical and Algebraic Methods in Programming

JF - Journal of Logical and Algebraic Methods in Programming

SN - 2352-2208

IS - 4

ER -