Guarded Kleene Algebra with Tests: Coequations, Coinduction, and Completeness

TL;DR

This paper explores the algebraic and coalgebraic properties of Guarded Kleene Algebra with Tests (GKAT), establishing semantics, behavioral characterizations, and completeness results for its axioms.

Contribution

It develops both operational and denotational semantics for GKAT, characterizes its behaviors via coequations, and proves soundness and completeness of its axioms.

Findings

Semantics for GKAT expressions are shown to coincide.

A coequation captures the automata behaviors of GKAT.

Axioms are proven sound and complete for the semantics.

Abstract

Guarded Kleene Algebra with Tests (GKAT) is an efficient fragment of KAT, as it allows for almost linear decidability of equivalence. In this paper, we study the (co)algebraic properties of GKAT. Our initial focus is on the fragment that can distinguish between unsuccessful programs performing different actions, by omitting the so-called early termination axiom. We develop an operational (coalgebraic) and denotational (algebraic) semantics and show that they coincide. We then characterize the behaviors of GKAT expressions in this semantics, leading to a coequation that captures the covariety of automata corresponding to behaviors of GKAT expressions. Finally, we prove that the axioms of the reduced fragment are sound and complete w.r.t. the semantics, and then build on this result to recover a semantics that is sound and complete w.r.t. the full set of axioms.