On the Expressive Power of Kleene Algebra with Domain

TL;DR

This paper demonstrates that Kleene algebras with domain are more expressive than those with tests, particularly for propositional Hoare logic, highlighting their superior theoretical capabilities.

Contribution

It establishes the greater expressive power of Kleene algebras with domain over Kleene algebras with tests, especially in the context of propositional Hoare logic.

Findings

Kleene algebras with domain are more expressive than Kleene algebras with tests.

Antidomain semirings surpass test semirings in expressiveness.

Kleene algebras with domain can represent propositional Hoare logic effectively.

Abstract

It is shown that antidomain semirings are more expressive than test semirings and that Kleene algebras with domain are more expressive than Kleene algebras with tests. It is also shown that Kleene algebras with domain are expressive for propositional Hoare logic whereas Kleene algebras with tests are not.