Weighted GKAT: Completeness and Complexity
arXiv:2504.20385
Abstract
We propose Weighted Guarded Kleene Algebra with Tests (wGKAT), an uninterpreted weighted programming language equipped with branching, conditionals, and loops. We provide an operational semantics for wGKAT using a variant of weighted automata and introduce a sound and complete axiomatization. We also provide a polynomial time decision procedure for bisimulation equivalence.
ICALP 2025. 51 pages, 2 figures