一句话：提出模块化证明 Kleene 代数带假设完备性的工具，并用于 KAT、KAO、NetKAT 及新变体。
本文研究带假设的 Kleene 代数相对其规范语言模型的完备性问题。KAT、KAO、NetKAT 等变体都可纳入这一统一框架，核心问题是：给定假设后，代数等式是否恰好刻画对应语言模型。作者重新审视、组合并扩展现有完备性结果，提出模块化证明工具。用这些工具，文章为 KAT、KAO 和 NetKAT 给出新的模块化完备性证明，并证明若干新变体的完备性：加入全关系常数的 KAT、加入 converse 运算的 KAT，以及测试集仅构成分配格的 KAT。结果展示了该框架的统一性与可扩展性。
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.
@article{paperbot2761,
title = {On Tools for Completeness of Kleene Algebra with Hypotheses},
author = {Damien Pous and Jurriaan Rot and Jana Wagemaker},
journal = {Logical Methods in Computer Science},
volume = {Volume 20, Issue 2},
year = {2024},
doi = {10.46298/lmcs-20(2:8)2024}
}