彼得里自动机
摘要：Kleene代数公理在语言模型和二进制关系模型中是完备的。特别地，在二进制关系模型中，如果两个正则表达式能识别相同的语言，那么它们在该模型中是普遍等价的。我们考虑Kleene寓言，即在二进制关系模型中自然的Kleene代数，带有两个额外的操作和一个常量：交集、逆和全关系。虽然正则语言在这些操作下是封闭的，但上述特征破坏了。我们从文献中综合几个结果，给出了一种用有向和标记图的语言来描述的特征。受Petri网的启发，我们设计了一种有限自动机模型，Petri自动机，可以识别这样的图。我们证明了关于这个自动机模型的Kleene定理：Petri自动机能够识别的图的集合正好是我们考虑的扩展正则表达式可以定义的图的集合。Petri自动机使我们能够获得无单位元的关系Kleene格的可判定性，也即由带有交集的正则表达式的二进制关系生成的等式理论，但是禁止使用单位元。这种限制用于确保相应的图是无环的。事实上，我们还证明了这个决策问题是EXPSPACE完全的。
作者：Paul Brunet and Damien Pous
论文ID：1702.01804
分类：Logic in Computer Science
分类简称：cs.LO
提交时间：2023-06-22