Pomset automata are an operational model of weak bi-Kleene algebra, which describes program 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{kblsz21,
title = "Equivalence checking for weak bi-Kleene algebra",
author = "{Paul Brunet}, {Tobias Kappé}, {Alexandra Silva}, {Bas Luttik}, {Fabio Zanasi}",
year = 2021,
journal = "LMCS",
doi = "10.46298/lmcs-17(3:19)2021"
}
