Kleene Algebra (KA) is a useful tool for proving that two programs are equivalent by reasoning equationally. Because it abstracts from the meaning of primitive programs, KA's equational theory is decidable, so it integrates well with interactive theorem provers. This raises the question: which equations can we (not) prove using the laws of KA? Moreover, which models of KA are complete, in the sense that they satisfy exactly the provable equations? Kozen (1994) answered these questions by characterizing KA in terms of its language model. Concretely, equivalences provable in KA are exactly those that hold for regular expressions. Pratt (1980) observed that KA is complete w.r.t. relational models, i.e., that its provable equations are those that hold for any relational interpretation. A less known result due to Palka (2005) says that finite models are complete for KA, i.e., that provable equivalences coincide with equations satisfied by all finite KAs. Phrased contrapositively, the latter is a finite model property (FMP): any unprovable equation is falsified by a finite KA. These results can be argued using Kozen's theorem, but the implication is mutual: given that KA is complete w.r.t. finite (resp. relational) models, Palka's (resp. Pratt's) arguments show that it is complete w.r.t. the language model. We embark on a study of the different complete models of KA, and the connections between them. This yields a fourth result subsuming those of Palka and Pratt, namely that KA is complete w.r.t. finite relational models. Next, we put an algebraic spin on Palka's techniques, which yield an elementary proof of the finite model property, and by extension, of Kozen's and Pratt's theorems. In contrast with earlier approaches, this proof relies not on minimality or bisimilarity of automata, but rather on representing the regular expressions involved in terms of transformation automata.

翻译：Kleene代数（KA）是通过等式推理证明两个程序等价的实用工具。由于对基本程序含义进行抽象，KA的等式理论是可判定的，因此能与交互式定理证明器良好结合。这引发了一个问题：哪些等式能（或不能）通过KA定律证明？此外，哪些KA模型在满足所有可证等式意义上是完备的？Kozen（1994）通过语言模型刻画KA回答了这些问题：KA中可证的等价关系恰为对正则表达式成立的那些。Pratt（1980）观察到KA关于关系模型是完备的，即其可证等式恰为对任意关系解释成立的那些。Palka（2005）的一个鲜为人知的结果表明，有限模型对KA是完备的——可证等价关系与所有有限KA满足的等式一致。用逆否命题表述即有限模型性质（FMP）：任何不可证等式都会被某个有限KA证伪。这些结论可通过Kozen定理论证，但蕴涵关系是相互的：给定KA关于有限（或关系）模型完备，Palka（或Pratt）的论证表明其关于语言模型完备。本文系统研究KA的不同完备模型及其相互联系，由此得到涵盖Palka与Pratt结果的第四个结论：KA关于有限关系模型是完备的。进而对Palka方法进行代数化处理，给出有限模型性质的初等证明，并由此导出Kozen定理与Pratt定理的证明。与现有方法不同，本证明不依赖于自动机的最小性或互模拟性质，而是通过变换自动机表示所涉及的正则表达式。