Draft:Kleene algebra with tests

Kleene algebra with tests (KAT) is an equational system that combines Kleene algebra and Boolean algebra. It was developed by Dexter Kozen in the 1990s. In 2022, Kozen received the Alonzo Church Award "for his fundamental work on developing the theory and applications" of KAT.

Definition

A Kleene algebra with tests is a Kleene algebra $(𝒦,+,\cdot ,{}^{*},0,1)$ augmented with a unary operator ${}^{-}$ on a subset $ℬ\subseteq K$ such that $(ℬ,+,\cdot ,{}^{-},0,1)$ is a Boolean algebra. This means that for $ℬ$:Template:Sfn

• $+$ is disjunction (logical "or").
• $\cdot$ is conjunction (logical "and").
• $0$ is Boolean falsehood.
• $1$ is Boolean truth.
• ${}^{-}$ is negation.

Applications

KAT was first applied to prove that a program with multiple while loops can be simulated by one with a single while loop.Template:Sfn

References

• Template:Cite journal
• Template:Cite journal
• Template:Cite journal
• Template:Cite journal
• Template:Cite journal
• Template:Cite journal
• Template:Cite journal
• Template:Cite journal
• Template:Cite journal
• Template:Cite journal
• Template:Cite journal
• Template:Cite journal
• Template:Cite journal
• Template:Cite journal
• Template:Cite journal
• Template:Cite journal