Guarded Kleene Algebra with Tests
Date: Wed, November 04, 2020
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.
Soham Chakraborty | Relaxed Memory Concurrency and Compiler Correctness
Next: | NWO Veni on A Trustworthy and Extensible Core Language for Agda