Completeness and the finite model property for Kleene algebra, reconsidered
From MaRDI portal
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.
Cites work
- A Bialgebraic Review of Deterministic Automata, Regular Expressions and Languages
- A completeness theorem for Kleene algebras and the algebra of regular events
- A fast compiler for NetKAT
- Completeness and the finite model property for Kleene algebra, reconsidered
- Derivatives of Regular Expressions
- scientific article; zbMATH DE number 1688351 (Why is no real title available?)
- scientific article; zbMATH DE number 1696821 (Why is no real title available?)
- scientific article; zbMATH DE number 3751028 (Why is no real title available?)
- scientific article; zbMATH DE number 177804 (Why is no real title available?)
- scientific article; zbMATH DE number 3560737 (Why is no real title available?)
- scientific article; zbMATH DE number 1086671 (Why is no real title available?)
- scientific article; zbMATH DE number 3251424 (Why is no real title available?)
- scientific article; zbMATH DE number 3287733 (Why is no real title available?)
- scientific article; zbMATH DE number 3366846 (Why is no real title available?)
- Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring.
- Left-handed completeness
- Left-Handed Completeness for Kleene algebra, via Cyclic Proofs
- Modal logic
- Netkat, semantic foundations for networks
- On finite model property of the equational theory of Kleene algebras
- On the fine-structure of regular algebra
- Partial derivatives of regular expressions and finite automaton constructions
- Programming Techniques: Regular expression search algorithm
- The Böhm–Jacopini Theorem Is False, Propositionally
- Two Complete Axiom Systems for the Algebra of Regular Events
- Une remarque sur les systèmes complets d'identités rationnelles
- Universal coalgebra: A theory of systems
Cited in
(8)- Correction to: ``The model companion of the class of pseudocomplemented semilattices is finitely axiomatizable
- Concurrent Kleene algebra: free model and completeness
- The model companion of the class of pseudocomplemented semilattices is finitely axiomatizable
- A completeness theorem for nondeterministic Kleene algebras
- Left-Handed Completeness for Kleene algebra, via Cyclic Proofs
- Completeness and the finite model property for Kleene algebra, reconsidered
- An elementary proof of the FMP for Kleene algebra
- Completeness of finitely weighted Kleene algebra with tests
This page was built for publication: Completeness and the finite model property for Kleene algebra, reconsidered
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6174420)
