弱双Kleene代数的等价性检查
摘要：Pomset 自动机是弱双Kleene代数的操作模型，描述了可以将执行分叉为并行线程的程序，在完成后，执行可以合并为单个线程恢复。我们表征了一种Pomset自动机的子集，该子集允许进行语言等价性的决策过程。此外，我们证明了此子集与序列有理表达式完全对应，即具有有限并行性操作符的有理表达式。作为一种后果，我们得到了一种新的证明序列有理表达式的等价性是可判定的。
作者：Tobias Kapp''e and Paul Brunet and Bas Luttik and Alexandra Silva and Fabio Zanasi
论文ID：1807.02102
分类：Formal Languages and Automata Theory
分类简称：cs.FL
提交时间：2023-06-22