Reference. Domain Reasoning in TopKAT
TopKAT is the algebraic theory of Kleene algebra with tests (KAT) extended with a top element. Compared to KAT, one pleasant feature of TopKAT is that, in relational models, the top element allows us to express the domain and codomain of a relation. This enables several applications in program logics, such as proving under-approximate specifications or reachability properties of imperative programs. However, while TopKAT inherits many pleasant features of KATs, such as having a decidable equational theory, it is incomplete with respect to relational models. In other words, there are properties that hold true of all relational TopKATs but cannot be proved with the axioms of TopKAT. This issue is potentially worrisome for program-logic applications, in which relational models play a key role. In this paper, we further investigate the completeness properties of TopKAT with respect to relational models. We show that TopKAT is complete with respect to (co)domain comparison of KAT terms, but incomplete when comparing the (co)domain of arbitrary TopKAT terms. Since the encoding of under-approximate specifications in TopKAT hinges on this type of formula, the aforementioned incompleteness results have a limited impact when using TopKAT to reason about such specifications.
Cite
Cited by (1)
Outrunning Big KATs: Efficient Decision Procedures for Variants of GKAT zhang-2026-outrunning
Cites 41 works (5 here)
With notes (5)
On incorrectness logic and Kleene algebra with top and tests zhang-2022-on
Kleene algebra with tests (KAT) is a foundational equational framework for reasoning about programs, which has found applications in program transformations, networking and compiler optimizations, among many other areas. In his seminal work, Kozen proved that KAT subsumes propositional Hoare logic, showing that one can reason about the (partial) correctness of while programs by means of the equational theory of KAT. In this work, we investigate the support that KAT provides for reasoning about incorrectness, instead, as embodied by O’Hearn’s recently proposed incorrectness logic. We show that KAT cannot directly express incorrectness logic. The main reason for this limitation can be traced to the fact that KAT cannot express explicitly the notion of codomain, which is essential to express incorrectness triples. To address this issue, we study Kleene Algebra with Top and Tests (TopKAT), an extension of KAT with a top element. We show that TopKAT is powerful enough to express a codomain operation, to express incorrectness triples, and to prove all the rules of incorrectness logic sound. This shows that one can reason about the incorrectness of while-like programs by means of the equational theory of TopKAT.
Guarded Kleene algebra with tests: verification of uninterpreted programs in nearly linear time smolka-2019-guarded
Guarded Kleene Algebra with Tests (GKAT) is a variation on Kleene Algebra with Tests (KAT) that arises by restricting the union (+) and iteration (*) operations from KAT to predicate-guarded versions. We develop the (co)algebraic theory of GKAT and show how it can be efficiently used to reason about imperative programs. In contrast to KAT, whose equational theory is PSPACE-complete, we show that the equational theory of GKAT is (almost) linear time. We also provide a full Kleene theorem and prove completeness for an analogue of Salomaa’s axiomatization of Kleene Algebra.
NetKAT: Semantic foundations for networks anderson2014netkat
Recent years have seen growing interest in high-level languages for programming networks. But the design of these languages has been largely ad hoc, driven more by the needs of applications and the capabilities of network hardware than by foundational principles. The lack of a semantic foundation has left language designers with little guidance in determining how to incorporate new features, and programmers without a means to reason precisely about their code. This paper presents NetKAT, a new network programming language that is based on a solid mathematical foundation and comes equipped with a sound and complete equational theory. We describe the design of NetKAT, including primitives for filtering, modifying, and transmitting packets; union and sequential composition operators; and a Kleene star operator that iterates programs. We show that NetKAT is an instance of a canonical and well-studied mathematical structure called a Kleene algebra with tests (KAT) and prove that its equational theory is sound and complete with respect to its denotational semantics. Finally, we present practical applications of the equational theory including syntactic techniques for checking reachability, proving non-interference properties that ensure isolation between programs, and establishing the correctness of compilation algorithms.
Kleene algebra with tests kozen1997kleene
We introduce Kleene algebra with tests, an equational system for manipulating programs. We give a purely equational proof, using Kleene algebra with tests and commutativity conditions, of the following classical result: every while program can be simulated by a while program with at most one while loop. The proof illustrates the use of Kleene algebra with tests and commutativity conditions in program equivalence proofs.
A Completeness Theorem for Kleene Algebras and the Algebra of Regular Events KOZEN1994366
We give a finitary axiomatization of the algebra of regular events involving only equations and equational implications. Unlike Salomaa′s axiomatizations, the axiomatization given here is sound for all interpretations over Kleene algebras.
External (36)
- An Algebra of Alignment for Relational Verification (2023)
- Completeness theorems for kleene algebra with tests and top (2023)
- On the complexity of kleene algebra with domain (2023)
- Finding real bugs in big programs with incorrectness logic (2022)
- Completeness theorems for kleene algebra with top (2022)
- Domain semirings united (2021)
- On Algebra of Program Correctness and Incorrectness (2021)
- On tools for completeness of kleene algebra with hypotheses (2021)
- Concurrent Kleene Algebra with Observations: From Hypotheses to Completeness (2020)
- Left-handed completeness (2020)
- Free Kleene algebras with domain (2020)
- An Under-Approximate Relational Logic (2020)
- Incorrectness logic (2020)
- Local Reasoning About the Presence of Bugs: Incorrectness Separation Logic (2020)
- Kleene algebra with hypotheses (2019)
- Concurrent kleene algebra: Free model and completeness (2018)
- On the Positive Calculus of Relations with Transitive Closure (2018)
- Equational Theories of Abnormal Termination Based on Kleene Algebra (2017)
- Developments in concurrent kleene algebra (2016)
- On the expressive power of kleene algebra with domain (2015)
- Kat + b! (2014)
- Axiomatizability of positive algebras of binary relations (2011)
- Reverse Hoare Logic (2011)
- Internal axioms for domain semirings (2011)
- Automated Reasoning in Kleene Algebra (2007)
- Kleene algebra with domain (2006)
- Modal kleene algebra and applications – a survey (2004)
- On the complexity of reasoning in kleene algebra (2002)
- On hoare logic and kleene algebra with tests (2000)
- Kleene algebra with tests: Completeness and decidability (1997)
- The Complexity of Kleene Algebra with Tests (1996)
- Kleene algebra with tests and commutativity conditions (1996)
- Hypotheses in kleene algebra (1995)
- Algebraic Approaches to Program Semantics (1986)
- A Course in Universal Algebra (1981)
- On the calculus of relations (1941)