A cyclic proof system for Guarded Kleene Algebra with Tests (full version)

TL;DR

The paper develops a cyclic, non-well-founded proof system $\mathsf{SGKAT}$ for Guarded Kleene Algebra with Tests ($GKAT$), a deterministic fragment of Kleene Algebra with Tests. It proves soundness and shows that all proofs can be made finite-state with a quadratic bound on the number of sequents, enabling regular cyclic proofs. Completeness is established via a proof-search procedure that runs in $\mathsf{coNLOGSPACE}$, giving an $\mathsf{NLOGSPACE}$ upper bound for the GKAT language-inclusion problem. The approach uses atom-annotated sequents and prioritised, invertible rules to avoid hypersequents (unlike in the Kleene Algebra setting) and yields a tight complexity bound that improves upon the KA case, with potential for extensions to inequational axiomatisations and broader completeness results.

Abstract

Guarded Kleene Algebra with Tests (GKAT for short) is an efficient fragment of Kleene Algebra with Tests, suitable for reasoning about simple imperative while-programs. Following earlier work by Das and Pous on Kleene Algebra, we study GKAT from a proof-theoretical perspective. The deterministic nature of GKAT allows for a non-well-founded sequent system whose set of regular proofs is complete with respect to the guarded language model. This is unlike the situation with Kleene Algebra, where hypersequents are required. Moreover, the decision procedure induced by proof search runs in NLOGSPACE, whereas that of Kleene Algebra is in PSPACE.