Tobias Kappé ; Paul Brunet ; Bas Luttik ; Alexandra Silva ; Fabio Zanasi - Equivalence checking for weak bi-Kleene algebra

lmcs:7502 - Logical Methods in Computer Science, August 13, 2021, Volume 17, Issue 3 - https://doi.org/10.46298/lmcs-17(3:19)2021
Equivalence checking for weak bi-Kleene algebra

Authors: Tobias Kappé ; Paul Brunet ; Bas Luttik ; Alexandra Silva ; Fabio Zanasi

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.


Volume: Volume 17, Issue 3
Published on: August 13, 2021
Accepted on: May 24, 2021
Submitted on: May 24, 2021
Keywords: Computer Science - Formal Languages and Automata Theory


Share

Consultation statistics

This page has been seen 240 times.
This article's PDF has been downloaded 122 times.