The paper reviews GKAT, an algebraic framework with a nearly linear-time decision procedure for propositional program equivalence, and surveys open problems in its axiomatization and expressivity.
Weighted GKAT: Completeness and Complexity
1 Pith paper cite this work. Polarity classification is still indexing.
1
Pith paper citing it
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.
fields
cs.PL 1years
2025 1verdicts
CONDITIONAL 1representative citing papers
citing papers explorer
-
On Propositional Program Equivalence (extended abstract)
The paper reviews GKAT, an algebraic framework with a nearly linear-time decision procedure for propositional program equivalence, and surveys open problems in its axiomatization and expressivity.