Equivalence checking for weak bi-Kleene algebra

TL;DR

This paper introduces a decidable fragment of pomset automata for weak bi-Kleene algebra, linking it to series-rational expressions with bounded parallelism, and providing a new proof of their equivalence decidability.

Contribution

It characterizes a fragment of pomset automata with a decision procedure for language equivalence, connecting it to series-rational expressions and proving their equivalence is decidable.

Findings

A fragment of pomset automata admits a decision procedure for language equivalence.

This fragment corresponds exactly to series-rational expressions with bounded parallelism.

The paper provides a new proof of the decidability of equivalence for these expressions.

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.