2026-08-25T22:09:00Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:27377 2026-08-24T14:08:32Z ddc:004 open_access

GKAT with Hoare Hypotheses Rot, Jurriaan Schmid, Todd Wagemaker, Jana Kleene Algebra GKAT Hypotheses Guarded Kleene Algebra with Tests (GKAT) is a variant of Kleene algebra which allows for reasoning about simple imperative programs, and which features a decision procedure for program equivalence in nearly linear time. In the current paper, we address the challenge of reasoning under assumptions about these programs. In particular, we develop a form of Hoare hypotheses, which allow modelling basic domain knowledge on pre- and postconditions of uninterpreted basic programs, and which are well-developed for classical Kleene algebra but not yet for GKAT. We show that the resulting axiomatisation is sound and complete. We then extend Hoare hypotheses to the more general form of word hypotheses. Based on an automata-theoretic approach, we show that equivalence of GKAT under word hypotheses is efficiently decidable. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Jurriaan Rot and Todd Schmid and Jana Wagemaker 2026 Is Part Of LIPIcs, Volume 391, 37th International Conference on Concurrency Theory (CONCUR 2026) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.CONCUR.2026.46 urn:nbn:de:0030-drops-273770 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2026.46 eng https://creativecommons.org/licenses/by/4.0/legalcode