Pith. sign in

REVIEW 1 cited by

Weighted GKAT: Completeness and Complexity

Not yet reviewed by Pith; the record is open.

Re-run · record.json Download PDF Read on arXiv ↗

This paper has not been read by Pith yet. Machine review is queued; the pith claim, tier, and objections will appear here once it completes.

SPECIMEN: schema-true, not a live event

T0 review · schema-true

One-sentence machine reading of the paper's core claim.

pith:XXXXXXXX · record.json · timestamp

arxiv 2504.20385 v1 pith:A36QRWRV submitted 2025-04-29 cs.LO cs.FLcs.PL

Spencer Van Koevering , Wojciech Różowski , Alexandra Silva This is my paper · ORCID
classification cs.LOcs.FLcs.PL
keywords weightedwgkatalgebraautomataaxiomatizationbisimulationbranchingcomplete
verification ladder T0 review T1 audit T2 compute T3 formal
0 comments
read the original 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.

Discussion (0). Continue with ORCID to comment.

Forward citations

Cited by 1 Pith paper

Reviewed papers in the Pith corpus that reference this work. Sorted by Pith novelty score. Full citation record

  1. On Propositional Program Equivalence (extended abstract)

    cs.PL 2025-07 conditional novelty 2.0 of 10

    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.

Pith tools