Kleene Algebra (KA) is a useful tool for proving that two programs are equivalent. Because KA's equational theory is decidable, 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. Both 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 novel 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 a new 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.

翻译：克莱因代数（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的定理。与早期方法不同，该证明不依赖于自动机的最小性或互模拟性，而是通过变换自动机来表示所涉及的正则表达式。