Completeness and the Finite Model Property for Kleene Algebra, Reconsidered
| Authors | |
|---|---|
| Publication date | 2023 |
| Host editors |
|
| Book title | Relational and Algebraic Methods in Computer Science (RAMiCS) 2023 |
| Book subtitle | 20th International Conference, RAMiCS 2023, Augsburg, Germany, April 3–6, 2023 : proceedings |
| ISBN |
|
| ISBN (electronic) |
|
| Series | Lecture Notes in Computer Science |
| Event | Relational and Algebraic Methods in Computer Science |
| Pages (from-to) | 158-175 |
| Publisher | Cham: Springer |
| Organisations |
|
| Abstract |
Kleene Algebra (KA) is the algebra of regular expressions. Central to the study of KA is Kozen’s (1994) completeness result, which says that any equivalence valid in the language model of KA follows from the axioms of KA. Also of interest is the finite model property (FMP), which says that false equivalences always have a finite counterexample. Palka (2005) showed that, for KA, the FMP is equivalent to completeness.
We provide a unified and elementary proof of both properties. In contrast with earlier completeness proofs, this proof does not rely on minimality or bisimilarity techniques for deterministic automata. Instead, our approach avoids deterministic automata altogether, and uses Antimirov’s derivatives and the well-known transition monoid construction. Our results are fully verified in the Coq proof assistant. |
| Document type | Conference contribution |
| Language | English |
| Published at | https://doi.org/10.48550/arXiv.2212.10931 https://doi.org/10.1007/978-3-031-28083-2_10 |
| Downloads |
978-3-031-28083-2_10
(Final published version)
|
| Permalink to this page | |
