Reference. Kleene Algebra with Commutativity Conditions Is Undecidable
We prove that the equational theory of Kleene algebra with commutativity conditions on primitives (or atomic terms) is undecidable, thereby settling a longstanding open question in the theory of Kleene algebra. While this question has also been recently solved independently by Kuznetsov, our results hold even for weaker theories that do not support the induction axioms of Kleene algebra.
Cite
Cited by (1)
Kleene Algebra kappe-2025-kleene
This booklet serves as an introduction to Kleene Algebra (KA), a set of laws that can be used to study general equivalences between programs. It discusses how general programs can be modeled using regular expressions, how those expressions correspond to automata, and how this correspondence can be exploited to obtain the central result of KA, namely that an equivalence of regular expressions is true if and only if it can be proved using the laws of KA. Each chapter closes with a set of exercises to further build intuition and understanding, and there is an optional chapter that develops automata theory through the lens of coalgebra.
Cites 20 works (4 here)
With notes (4)
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.
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.
Concurrent Kleene Algebra hoare2009concurrent
Kleene algebra with tests and program schematology angus2001kleene
The theory of flowchart schemes has a rich history going back to Ianov (1960); see Manna (1974) for an elementary exposition. A central question in the theory of program schemes is scheme equivalence. Manna presents several examples of equivalence proofs that work by simplifying the schemes using various combinatorial transformation rules. In this paper we present a purely algebraic approach to this problem using Kleene algebra with tests (KAT). Instead of transforming schemes directly using combinatorial graph manipulation, we regard them as a certain kind of automaton on abstract traces. We prove a generalization of Kleene’s theorem and use it to construct equivalent expressions in the language of KAT. We can then give a purely equational proof of the equivalence of the resulting expressions. We prove soundness of the method and give a detailed example of its use.
External (16)
- On the complexity of reasoning in kleene algebra with commutativity conditions (2023)
- An algebra of alignment for relational verification (2022)
- Concurrent Kleene Algebra with Observations: From Hypotheses to Completeness (2020)
- Left-handed completeness (2020)
- Concurrent kleene algebra: Free model and completeness (2018)
- A coalgebraic decision procedure for netkat (2015)
- On Probabilistic Kleene Algebras, Automata and Simulations (2011)
- Using Probabilistic Kleene Algebra for Protocol Verification (2006)
- Introduction to Automata Theory, Languages, and Computation (2001)
- Partial Commutation and Traces (1997)
- On the complexity of reasoning in kleene algebra (1997)
- Partial derivatives of regular expressions and finite automaton constructions (1996)
- Kleene algebra with tests and commutativity conditions (1996)
- On kleene algebras and closed semirings (1990)
- On the decidability of some problems about rational subsets of free partially commutative monoids (1986)
- Transductions and Context-Free Languages (1979)