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.^[1]

Definition

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

$+$ 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.^[3]

Notes

^ "Previous Awards". EACSL. Archived from the original on 2024-07-27. Retrieved 18 November 2024.
^ Kozen 1996a, p. 17.
^ Kozen 1996a, pp. 20–28.

References

Kozen, Dexter (March 1996a). "Kleene algebra with tests and commutativity conditions". Tools and Algorithms for the Construction and Analysis of Systems. 1055: 14–33. doi:10.1007/3-540-61042-1_35.
Kozen, Dexter; Smith, Frederick (September 1996b). "Kleene algebra with tests: Completeness and decidability" (PDF). Computer Science Logic. 1258: 244–259. doi:10.1007/3-540-63172-0_43.
Kozen, Dexter (May 1997). "Kleene algebra with tests". ACM Transactions on Programming Languages and Systems. 19 (3): 427–443. doi:10.1145/256167.256195.
Kozen, Dexter (July 2000). "On Hoare logic and Kleene algebra with tests". ACM Transactions on Computational Logic. 1 (1): 60–76. doi:10.1145/343369.343378.
Pous, Damien (July 2013). "Kleene Algebra with Tests and Coq Tools for While Programs". Interactive Theorem Proving. 7998: 180–196. arXiv:1302.1737. doi:10.1007/978-3-642-39634-2_15.
Grathwohl, Niels Bjørn Bugge; Kozen, Dexter; Mamouras, Konstantinos (14 July 2014). "KAT + B!" (PDF). CSL-LICS '14: Proceedings of the Joint Meeting of the Twenty-Third EACSL Annual Conference on Computer Science Logic (CSL) and the Twenty-Ninth Annual ACM/IEEE Symposium on Logic in Computer Science (LICS): 1–10. doi:10.1145/2603088.2603095.
Pous, Damien (14 January 2015). "Symbolic Algorithms for Language Equivalence and Kleene Algebra with Tests". POPL '15: Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages: 357–368. arXiv:1407.3213. doi:10.1145/2676726.2677007.
Armstrong, Alasdair; Gomes, Victor B. F.; Struth, Georg (April 2016). "Building program construction and verification tools from algebraic principles". Formal Aspects of Computing. 28 (2): 265–293. doi:10.1007/s00165-015-0343-1.
Uramoto, Takeo (June 2016). "Canonical finite models of Kleene algebra with tests". Journal of Logical and Algebraic Methods in Programming. 85 (4): 595–616. doi:10.1016/j.jlamp.2015.11.001.
Jipsen, Peter; Moshier, M. Andrew (June 2016). "Concurrent Kleene algebra with tests and branching automata". Journal of Logical and Algebraic Methods in Programming. 85 (4): 637–652. doi:10.1016/j.jlamp.2015.12.005.
Smolka, Steffen; Foster, Nate; Hsu, Justin; Kappé, Tobias; Kozen, Dexter; Silva, Alexandra (January 2020). "Guarded Kleene algebra with tests: verification of uninterpreted programs in nearly linear time". Proceedings of the ACM on Programming Languages. 4 (POPL): 1–28. doi:10.1145/3371129.
Zhang, Cheng; de Amorim, Arthur Azevedo; Gaboardi, Marco (16 January 2022). "On incorrectness logic and Kleene algebra with top and tests". Proceedings of the ACM on Programming Languages. 6 (POPL): 1–30. doi:10.1145/3498690.
Greenberg, Michael; Beckett, Ryan; Campbell, Eric (9 June 2022). "Kleene algebra modulo theories: a framework for concrete KATs". PLDI 2022: Proceedings of the 43rd ACM SIGPLAN International Conference on Programming Language Design and Implementation: 594–608. doi:10.1145/3519939.3523722.
Peng, Yuxiang; Ying, Mingsheng; Wu, Xiaodi (9 June 2022). "Algebraic reasoning of Quantum programs via non-idempotent Kleene algebra". PLDI 2022: Proceedings of the 43rd ACM SIGPLAN International Conference on Programming Language Design and Implementation: 657–670. arXiv:2110.07018. doi:10.1145/3519939.3523713.
Sedlár, Igor (May 2023). "Kleene Algebra With Tests for Weighted Programs". 2023 IEEE 53rd International Symposium on Multiple-Valued Logic: 111–116. arXiv:2303.00322. doi:10.1109/ISMVL57333.2023.00031.
Feng, Hui; Bonsangue, Marcello (8 April 2024). "Concurrent NetKAT with Ports". SAC '24: Proceedings of the 39th ACM/SIGAPP Symposium on Applied Computing: 1722–1730. doi:10.1145/3605098.3636048.

[award-1] "Previous Awards". EACSL. Archived from the original on 2024-07-27. Retrieved 18 November 2024.

[FOOTNOTEKozen1996a17-2] Kozen 1996a, p. 17.

[FOOTNOTEKozen1996a20–28-3] Kozen 1996a, pp. 20–28.

[1]

[2]

[3]