TY  - JOUR
IS  - 3
N1  - This work is licensed under the Creative Commons Attribution License. To view a copy of this license, visit https://creativecommons.org/licenses/by/4.0/
VL  - 17
AV  - public
Y1  - 2021/08/13/
SP  - 19:1
EP  - 19:53
TI  - Equivalence checking for weak bi-Kleene algebra
A1  - Kappé, T
A1  - Brunet, P
A1  - Luttik, B
A1  - Silva, A
A1  - Zanasi, F
JF  - Logical Methods in Computer Science
UR  - https://doi.org/10.46298/lmcs-17(3:19)2021
N2  - 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.
ID  - discovery10063343
ER  -