Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Weighted GKAT: Completeness and Complexity

Spencer Van Koevering, Wojciech Różowski, Alexandra Silva

TL;DR

This work introduces Weighted GKAT (wGKAT), a GKAT-inspired language with semiring-weighted branching, directed at reasoning about deterministic, uninterpreted programs with weighted control flow. It develops a coalgebraic operational semantics via weighted automata, proves a sound and complete axiomatization for bisimulation equivalence, and provides a polynomial-time decision procedure for checking bisimilarity. The completeness relies on a Salomaa-style system of equations and the Uniqueness Axiom, under a class of semirings that are positive, refinement, and Conway, enabling a robust semantic foundation and tractable verification. The framework enables modeling of costs, probabilities, and other quantitative aspects, with concrete applications like optimal ski-rental analysis and potential extensions to NetKAT-like networks.

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.

Weighted GKAT: Completeness and Complexity

TL;DR

This work introduces Weighted GKAT (wGKAT), a GKAT-inspired language with semiring-weighted branching, directed at reasoning about deterministic, uninterpreted programs with weighted control flow. It develops a coalgebraic operational semantics via weighted automata, proves a sound and complete axiomatization for bisimulation equivalence, and provides a polynomial-time decision procedure for checking bisimilarity. The completeness relies on a Salomaa-style system of equations and the Uniqueness Axiom, under a class of semirings that are positive, refinement, and Conway, enabling a robust semantic foundation and tractable verification. The framework enables modeling of costs, probabilities, and other quantitative aspects, with concrete applications like optimal ski-rental analysis and potential extensions to NetKAT-like networks.

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.
Paper Structure (15 sections, 97 equations, 2 figures)

This paper contains 15 sections, 97 equations, 2 figures.

Table of Contents

  1. Coalgebra
  2. Introduction
  3. Syntax
  4. Operational Semantics
  5. Operational semantics of Expressions
  6. Characterizing Equivalence
  7. Axioms
  8. Derivable facts
  9. Completeness
  10. Fundamental Theorem
  11. Solutions to Systems of Equations
  12. Bisimilarity implies Provable Equivalence
  13. Decidability and Complexity
  14. Related Work
  15. Conclusion

Figures (2)

  • Figure 1: Syntax of wGKAT
  • Figure 2: The axiomatization of wGKAT bisimulation equivalence. In these statements we let $e,f,g \in \textbf{\upshape{Exp}}, b,c \in \textbf{\upshape{BExp}}, v\in\textbf{\upshape{Out}}, \alpha \in \text{\upshape{At}}, p \in \textbf{\upshape{Act}},\; r,s,t,u \in \textbf{S}$. $1$ and $0$ weights refer to the multiplicative and additive identity in the chosen semiring.