In the literature on Kleene algebra, a number of variants have been proposed which impose additional structure specified by a theory, such as Kleene algebra with tests (KAT) and the recent Kleene algebra with observations (KAO), or make specific assumptions about certain constants, as for instance in NetKAT. Many of these variants fit within the unifying perspective offered by Kleene algebra with hypotheses, which comes with a canonical language model constructed from a given set of hypotheses. For the case of KAT, this model corresponds to the familiar interpretation of expressions as languages of guarded strings. A relevant question therefore is whether Kleene algebra together with a given set of hypotheses is complete with respect to its canonical language model. In this paper, we revisit, combine and extend existing results on this question to obtain tools for proving completeness in a modular way. We showcase these tools by giving new and modular proofs of completeness for KAT, KAO and NetKAT, and we prove completeness for new variants of KAT: KAT extended with a constant for the full relation, KAT extended with a converse operation, and a version of KAT where the collection of tests only forms a distributive lattice.

翻译：在Kleene代数的文献中，已提出了多种变体，这些变体通过理论施加了额外结构（如带测试的Kleene代数（KAT）和近期提出的带观察的Kleene代数（KAO）），或对特定常数做出具体假设（如NetKAT）。这些变体大多适用于带假设的Kleene代数所提供的统一视角，该视角通过给定假设集构建规范语言模型。对于KAT的情形，该模型对应于将表达式解释为受防护字符串语言的常见语义。因此，一个相关问题是：Kleene代数与给定假设集是否相对于其规范语言模型是完备的？本文重新审视、整合并拓展了关于该问题的现有结果，以获取能以模块化方式证明完备性的工具。我们通过为KAT、KAO和NetKAT给出新颖的模块化完备性证明来展示这些工具，并证明KAT新变体的完备性：扩展了全关系常数的KAT、扩展了逆运算的KAT，以及测试集合仅构成分配格的KAT版本。