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