Kleene Algebra with Tests
Origin. Kleene (1956) introduced regular events; Conway (1971) gave the algebraic treatment. Dexter Kozen's "A completeness theorem for Kleene algebras and the algebra of regular events" (1994) fixed the axioms now standard, and "Kleene algebra with tests" (TOPLAS, 1997) added the Boolean subalgebra that turns the structure into a program logic. Kozen and Smith (1996) established the free model; Kozen (2000) showed KAT subsumes propositional Hoare logic.
Models. A program is an element of a Kleene algebra and a condition is an element of a Boolean subalgebra of it, so control flow and its guards live in one equational theory. Verification becomes equational reasoning: a Hoare triple is an identity, and proving a program correct is proving two terms equal. The intended interpretations are binary relations on a state space and sets of guarded strings; the axioms are complete for both, so a proof in the algebra is a proof about programs.
Formalism.
Kleene algebra: (K, +, ·, *, 0, 1). +: choice. ·: sequential composition. *: iteration. Idempotent semiring + star. Natural order: p ≤ q iff p + q = q.
Star axioms: 1 + p·p* ≤ p*. 1 + p*·p ≤ p*. q + p·r ≤ r → p*·q ≤ r. q + r·p ≤ r → q·p* ≤ r.
Tests: Boolean subalgebra B ⊆ K. b ∈ B: test. b̄: complement of b. b · b̄ = 0.
Conditional: if b then p else q = b·p + b̄·q. Defined algebraically. Tests as guards.
While: while b do p = (b·p)*·b̄. Loop encoding. Star + test.
Hoare triple encoding: {b} p {c} ≡ b·p·c̄ = 0. Or equivalently: b·p ≤ p·c. Algebraic Hoare logic.
Free model — guarded strings: A guarded string alternates atoms of B with atomic programs: α₀ p₁ α₁ p₂ ... pₙ αₙ. The free KAT on given atomic programs and tests is the algebra of sets of guarded strings. Two terms are KAT-equal iff they denote the same set.
The two intended models: Relational: elements are binary relations on states,
- is union, · composition, * reflexive transitive closure, tests are subsets of the identity. Language: elements are sets of guarded strings. Complete for both.
*-continuity: p·q*·r = sup_n p·qⁿ·r. An infinitary condition, not an equation. Every *-continuous Kleene algebra is a Kleene algebra; the converse fails.
Completeness: KAT equationally complete for: Relational interpretation. Language interpretation. PSPACE-complete.
Symbols.
| Symbol | Unicode | Name | Meaning |
|---|---|---|---|
| * | — | Kleene star | Iteration: zero or more times |
| · | U+00B7 | Middle dot | Sequential composition |
| + | — | Plus sign | Nondeterministic choice |
| 0, 1 | — | Constants | Failure; the empty action |
| ≤ | U+2264 | Less-than or equal to | Natural order, defined by p + q = q |
| b̄ | — | Test complement | Boolean negation of a test |
| B | — | Boolean subalgebra | The tests |
| K | — | Carrier | The set of program elements |
| ⊆ | U+2286 | Subset of or equal to | B ⊆ K |
| ∈ | U+2208 | Element of | Membership of a test in B |
| → | U+2192 | Rightwards arrow | Implication in the quasi-equational star rules |
| = | U+003D | Equals sign | Equational identity, the judgment KAT proves |
| ≡ | U+2261 | Identical to | Definitional equivalence of the Hoare encoding |
| {b} p {c} | — | Hoare triple | Encoded as b·p·c̄ = 0 |
| α | U+03B1 | Greek small alpha | An atom of the Boolean subalgebra |
| sup | — | Supremum | Least upper bound in the *-continuity condition |
Metatheory. Kozen (1994) proved his axioms complete for the equational theory of regular expressions, and the same axioms are complete for the relational model, so an identity holds of all binary-relation interpretations exactly when it holds of all regular languages. Kozen and Smith (1996) extended this to KAT with guarded strings as the free model: two KAT terms are provably equal precisely when they denote the same set of guarded strings. Deciding an equation is PSPACE-complete, matching regular expression equivalence (Stockmeyer and Meyer). Kozen (2000) showed that every relationally valid rule of propositional Hoare logic is derivable in KAT, so Hoare logic is a proper subsystem of an equational theory, and that propositional Hoare logic is itself PSPACE-complete. The induction rules are quasi-equational rather than equational, and this is necessary: Redko (1964) proved the algebra of regular events has no finite purely equational axiomatization.
Applies to. Program verification and compiler optimization, where a transformation is an identity. Network configuration analysis, via NetKAT. Static analysis and dataflow. Protocol and security reasoning. The algebraic counterpart of propositional dynamic logic.
Limitations. Tests are propositional, so the algebra sees the control-flow skeleton and never the data: there are no variables, no assignments and no way to say that a test's truth depends on what a program wrote, which is why KAT captures propositional Hoare logic exactly and first-order Hoare logic not at all. Reasoning is equational, so partial correctness is expressible as an identity while termination and total correctness are not, iteration being an unbounded join with no well-foundedness condition attached. Adding hypotheses is worse than adding axioms: Kozen showed the universal Horn theory of Kleene algebra is Π¹₁-complete, so equational reasoning under assumptions about the atomic programs is not merely intractable but not recursively enumerable, and only special forms of hypothesis can be eliminated. The finite axiomatization depends on the quasi-equational induction rules; by Redko's theorem no purely equational finite basis exists.
© 2026 Lingenic LLC