Generalising KAT to verify weighted computations

TL;DR

This paper extends Kleene algebra with tests (KAT) to weighted and graded settings, enabling reasoning about programs with non-bivalent tests and weighted transitions, and introduces new algebraic structures and semantics.

Contribution

It introduces graded Kleene algebra with tests (GKAT) and an idempotent variant (I-GKAT), expanding KAT's expressiveness for weighted and graded program analysis.

Findings

Defined four new algebraic structures over residuated lattices.

Encoded graded propositional Hoare logic in I-GKAT.

Discussed program equivalence proofs in a graded context.

Abstract

Kleene algebra with tests (KAT) was introduced as an algebraic structure to model and reason about classic imperative programs, i.e. sequences of discrete transitions guarded by Boolean tests. This paper introduces two generalisations of this structure able to express programs as weighted transitions and tests with outcomes in non necessarily bivalent truth spaces: graded Kleene algebra with tests (GKAT) and a variant where tests are also idempotent (I-GKAT). On this context, and in analogy to Kozen's encoding of Propositional Hoare Logic (PHL) in KAT [22], we discuss the encoding of a graded PHL in I-GKAT and of its while-free fragment in GKAT. Moreover, to establish semantics for these structures four new algebras are defined: FSET(T), FREL(K,T) and FLANG(K,T) over complete residuated lattices K and T, and M(n,A) over a GKAT or I-GKAT A. As a final exercise, the paper discusses some program equivalence proofs in a graded context.