Completeness of Finitely Weighted Kleene Algebra With Tests
Igor Sedlár
TL;DR
This work extends completeness results for finitely weighted Kleene algebras with tests (KAT(S)) to finitely valued settings under a finite copi-semiring S. It establishes language completeness with respect to weighted guarded languages and relational completeness with respect to weighted transition systems, using guarded strings and a Cayley-like construction to connect algebraic reasoning with semantic models. The results provide a solid foundation for equational reasoning about weighted programs, including upper-bound weight models, and point to future work on decidability and broader semiring generalizations. Overall, the paper strengthens the theoretical basis for reasoning about weighted computations within Kleene algebra frameworks.
Abstract
Building on Ésik and Kuich's completeness result for finitely weighted Kleene algebra, we establish relational and language completeness results for finitely weighted Kleene algebra with tests. Similarly as Ésik and Kuich, we assume that the finite semiring of weights is commutative, partially ordered and zero-bounded, but we also assume that it is integral. We argue that finitely weighted Kleene algebra with tests is a natural framework for equational reasoning about weighted programs in cases where an upper bound on admissible weights is assumed.