Guarded Kleene Algebra with Tests

Tobias Kappé


Date: Wed, November 04, 2020
Time: 15:20
Room: Zoom


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 |
Next: Casper Bach Poulsen |