Reference. Weighted GKAT: Completeness and Complexity
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.
Cite
Cited by (2)
Weighted NetKAT: A Programming Language for Quantitative Network Verification suarezacevedo-2026-weighted
We introduce weighted NetKAT, a domain-specific language for modeling and verifying quantitative quantitative network properties. The language is parametric on a semiring , enabling the treatment of a wide range of quantities in a uniform way. We provide a denotational semantics and an equivalent operational semantics, the latter based on a novel model of weighted NetKAT automata ( WNKA ) capturing the stateful behavior of our language. With WNKA , we obtain a class of generic decision procedures for reasoning about quantitative safety and reachability in a fully automatic way, even in the presence of possibly unbounded iteration. We demonstrate the applicability of our framework in a case study using Internet2’s Abilene network as the underlying topology.
Outrunning Big KATs: Efficient Decision Procedures for Variants of GKAT zhang-2026-outrunning
Cites 32 works (3 here)
With notes (3)
Guarded Kleene algebra with tests: verification of uninterpreted programs in nearly linear time smolka-2019-guarded
Guarded Kleene Algebra with Tests (GKAT) is a variation on Kleene Algebra with Tests (KAT) that arises by restricting the union (+) and iteration (*) operations from KAT to predicate-guarded versions. We develop the (co)algebraic theory of GKAT and show how it can be efficiently used to reason about imperative programs. In contrast to KAT, whose equational theory is PSPACE-complete, we show that the equational theory of GKAT is (almost) linear time. We also provide a full Kleene theorem and prove completeness for an analogue of Salomaa’s axiomatization of Kleene Algebra.
Kleene algebra with tests kozen1997kleene
We introduce Kleene algebra with tests, an equational system for manipulating programs. We give a purely equational proof, using Kleene algebra with tests and commutativity conditions, of the following classical result: every while program can be simulated by a while program with at most one while loop. The proof illustrates the use of Kleene algebra with tests and commutativity conditions in program equivalence proofs.
A Completeness Theorem for Kleene Algebras and the Algebra of Regular Events KOZEN1994366
We give a finitary axiomatization of the algebra of regular events involving only equations and equational implications. Unlike Salomaa′s axiomatizations, the axiomatization given here is sound for all interpretations over Kleene algebras.
External (29)
- Coalgebraic Completeness Theorems for Effectful Process Algebras (2024)
- Probabilistic guarded kat modulo bisimilarity: Completeness and complexity (2023)
- Kleene algebra with tests for weighted programs (2023)
- Weighted programming (2022)
- Free-lattice functors weakly preserve epi-pullbacks (2021)
- Efficient and modular coalgebraic partition refinement (2020)
- Generic partition refinement and weighted tree automata (2019)
- Learning weighted automata over principal ideal domains (2019)
- Efficient coalgebraic partition refinement (2017)
- Refinement Monoids, Equidecomposability Types, and Boolean Inverse Semigroups (2017)
- Semirings and their Applications (2013)
- Handbook of Weighted Automata (2009)
- Copower functors (2009)
- Iteration semirings (2008)
- Types and coalgebraic structure (2005)
- Inductive star-semirings (2004)
- Semirings and Affine Equations over Them: Theory and Applications (2003)
- Behavioural differential equations: a coinductive calculus of streams, automata, and power series (2003)
- Coalgebras of bounded type (2002)
- Monoid-labeled transition systems (2001)
- Coalgebraic structure from weak limit preserving functors (2000)
- Universal coalgebra: a theory of systems (2000)
- Bisimulation for probabilistic transition systems: a coalgebraic approach (1999)
- Elements of the general theory of coalgebras (1999)
- The equality problem for rational series with multiplicities in the tropical semiring is undecidable (1992)
- Three partition refinement algorithms (1987)
- Verification of an alternating bit protocol by means of process algebra (1985)
- CCS expressions, finite state processes, and three problems of equivalence (1983)
- Two complete axiom systems for the algebra of regular events (1966)