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版本。