Equivalence checking for weak bi-Kleene algebra
Formal Languages and Automata Theory
2023-06-22 v5
Abstract
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.
Cite
@article{arxiv.1807.02102,
title = {Equivalence checking for weak bi-Kleene algebra},
author = {Tobias Kappé and Paul Brunet and Bas Luttik and Alexandra Silva and Fabio Zanasi},
journal= {arXiv preprint arXiv:1807.02102},
year = {2023}
}