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.

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