Guarded Kleene Algebra with Tests

Tobias Kappé

A Guarded Kleene Algebra with Tests (GKAT) is a type of Kleene Algebra with Tests (KAT) that arises by restricting the operators of KAT to “deterministic” (predicate-guarded) versions. This makes GKAT especially suited to reason about flow control in imperative programs. In contrast with KAT, where the equivalence problem is PSPACE-complete, we show that equivalence in GKAT can be decided in almost linear time. We also provide a full Kleene theorem and prove completeness w.r.t. a Salomaa-style axiomatization, both of which require us to develop a coalgebraic theory of GKAT.

---

Previous: Soham Chakraborty | Relaxed Memory Concurrency and Compiler Correctness
Next: | NWO Veni on A Trustworthy and Extensible Core Language for Agda