Jurriaan Rot

Kleene Algebras and Bisimulation-up-to

The axioms of Kleene Algebra (KA) are complete for language
equivalence of regular expressions, and consequently one
can prove KA identities by showing that certain
regular expressions represent the same language. Language
equivalence of regular expressions can be shown coinductively
by establishing bisimilarity of associated deterministic automata.

Bisimulation-up-to is a family of enhancements of the bisimulation
proof method for processes, which has recently been generalized
to the theory of coalgebras. We apply bisimulation-up-to to
regular expressions, and derive a simplified proof technique
for equations in KA.