# Kleene algebra with commutativity conditions is undecidable

arXiv: https://arxiv.org/abs/2411.15979 · HTML: https://mlsanity.com/paper/2411.15979/

## Key facts

- No citing papers in the map yet (data through 14 Oct 2026).
- Builds on 3 of its 21 references that are in the map.
- First posted on arXiv 24 Nov 2024.

## Builds on (most cited first, 3 of 3)

- [Concurrent Kleene Algebra with Observations: from Hypotheses to Completeness](https://mlsanity.com/paper/2002.09682/) (2020)
- [On Incorrectness Logic and Kleene Algebra with Top and Tests](https://mlsanity.com/paper/2108.07707/) (2021)
- [An algebra of alignment for relational verification](https://mlsanity.com/paper/2202.04278/) (2022)

## Abstract (arXiv)

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.