Canonical finite models of Kleene algebra with tests

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