Kleene Algebra with Tests

Origin. Kozen (1996). Algebraic program logic. Regular operations. Propositional tests. Foundation for program algebra.

Models. Programs as Kleene algebra elements. Tests as subalgebra. Algebraic verification. Equational reasoning. Efficient decision procedures.

Formalism.

Kleene algebra: (K, +, ·, *, 0, 1). +: choice. ·: sequential composition. *: iteration. Idempotent semiring + star.

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.

Completeness: KAT equationally complete for: Relational interpretation. Language interpretation. PSPACE-complete.

Symbols.

Metatheory. Algebraic reasoning. Completeness. Decision procedures. Equational.

Applies to. Program verification. Network routing. Compiler optimization. Security.

Limitations. No explicit state. Equational only. Extensions needed. Propositional tests.