具有测试和顶部的Kleene代数的完备性定理
摘要：具有测试和顶元的Kleene代数与受保护的字符串语言和二元关系的完备性有两个结果。尽管这两个模型类的等式理论在Kleene代数的签名上相同，但当我们考虑一个额外的常数“top”表示完整元素时，情况就不再是这样了。事实上，完全关系满足比完全语言更多的定律，我们证明这些附加定律都可以从一个额外的公理中推导出来。如果我们稍微泛化关系模型的概念，允许顶是一个最大元素但不一定是完整关系的子代数，那么我们得到这两个等式理论是相同的。我们使用封闭语言和归约模型来证明我们的完备性结果，这些结果相对于正则事件代数的任何公理化。对于我们的一个构造，我们将有限幺环可识别的概念扩展到了受保护字符串语言；这个设备使得我们可以得到一个用于二元关系的等式理论的PSpace算法。
作者：Damien Pous, Jana Wagemaker
论文ID：2304.07190
分类：Formal Languages and Automata Theory
分类简称：cs.FL
提交时间：2023-04-17