一句话：证明了带测试与顶元素的 Kleene 代数的两个完备性定理，并给出二元关系等式理论的 PSpace 算法。
本文研究带测试与顶元素的 Kleene 代数（KAT with top）的完备性。在该签名下，守卫字符串语言与二元关系模型的等式理论原本一致，但加入表示全元素的 top 常数后不再相同：全关系比全语言满足更多定律。作者证明这些额外定律可由单条附加公理推出，并表明若将关系模型推广为 top 只是最大元素而非全关系的关系子代数，则两个等式理论重新一致。证明借助闭语言模型与归约，相对于正则事件代数的任意公理化；其中一种构造把有限幺半群可识别性扩展到守卫字符串语言，从而得到二元关系等式理论的 PSpace 算法。
We prove two completeness results for Kleene algebra with tests and a top element, with respect to guarded string languages and binary relations. While the equational theories of those two classes of models coincide over the signature of Kleene algebra, this is no longer the case when we consider an additional constant ``top'' for the full element. Indeed, the full relation satisfies more laws than the full language, and we show that those additional laws can all be derived from a single additional axiom. We recover that the two equational theories coincide if we slightly generalise the notion of relational model, allowing sub-algebras of relations where top is a greatest element but not necessarily the full relation. We use models of closed languages and reductions in order to prove our completeness results, which are relative to any axiomatisation of the algebra of regular events. For one of our constructions, we extend the concept of finite monoid recognisability to guarded-string languages; this device makes it possible to obtain a PSpace algorithm for the equational theory of binary relations.
@article{paperbot2722,
title = {Completeness Theorems for Kleene algebra with tests and top},
author = {Damien Pous and Jana Wagemaker},
journal = {Logical Methods in Computer Science},
volume = {Volume 20, Issue 3},
year = {2024},
doi = {10.46298/lmcs-20(3:27)2024}
}