一句话：刻画了 pomset 自动机中语言等价可判定的片段，并证明其恰对应系列有理表达式。
本文研究弱双 Kleene 代数的等价性检查问题。该代数用于描述可将执行分叉为多个并行线程、待线程完成后汇合为单线程的程序。作者以 pomset 自动机作为其操作模型，刻画了一类能够对语言等价性给出判定过程的 pomset 自动机片段，并证明该片段恰好对应于系列有理表达式，即在有理表达式上增加有界并行算子所得的表达式。作为推论，他们给出了系列有理表达式等价性可判定的一个新证明。
Pomset automata are an operational model of weak bi-Kleene algebra, which describes programs that can fork an execution into parallel threads, upon completion of which execution can join to resume as a single thread. We characterize a fragment of pomset automata that admits a decision procedure for language equivalence. Furthermore, we prove that this fragment corresponds precisely to series-rational expressions, i.e., rational expressions with an additional operator for bounded parallelism. As a consequence, we obtain a new proof that equivalence of series-rational expressions is decidable.
@article{paperbot1285,
title = {Equivalence checking for weak bi-Kleene algebra},
author = {Tobias Kappé and Paul Brunet and Bas Luttik and Alexandra Silva and Fabio Zanasi},
journal = {Logical Methods in Computer Science},
volume = {Volume 17, Issue 3},
year = {2021},
doi = {10.46298/lmcs-17(3:19)2021}
}