Activities per year
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 wellknown transition monoid construction.
Our results are fully verified in the Coq proof assistant.
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 wellknown transition monoid construction.
Our results are fully verified in the Coq proof assistant.
Original language  English 

Title of host publication  Relational and Algebraic Methods in Computer Science 
Editors  Roland Glück, Luigi Santocanale, Michael Winter 
Publisher  Springer 
Pages  158175 
Number of pages  18 
ISBN (Electronic)  9783031280832 
ISBN (Print)  9783031280825 
DOIs  
Publication status  Published  2023 
Event  20th International Conference on Relational and Algebraic Methods in Computer Science  Augsburg, Germany Duration: 3 Apr 2023 → 6 Apr 2023 Conference number: 20 
Publication series
Series  Lecture Notes in Computer Science book series 

Volume  13896 
ISSN  03029743 
Conference
Conference  20th International Conference on Relational and Algebraic Methods in Computer Science 

Abbreviated title  RAMiCS 2023 
Country/Territory  Germany 
City  Augsburg 
Period  3/04/23 → 6/04/23 
Fingerprint
Dive into the research topics of 'Completeness and the Finite Model Property for Kleene Algebra, Reconsidered'. Together they form a unique fingerprint.Activities

20th International Conference on Relational and Algebraic Methods in Computer Science
Kappé, T. (Participant / Attendee)
3 Apr 2023 → 6 Apr 2023Activity: Attending or organising an event types › Attending an event › Academic

Completeness and the Finite Model Property for Kleene Algebra, Reconsidered
Kappé, T. (Speaker)
4 Apr 2023Activity: Talk or presentation types › Conference contribution (without a publication) › Academic

Completeness and the Finite Model Property for Kleene Algebra, Reconsidered
Kappé, T. (Speaker)
6 Sept 2023Activity: Talk or presentation types › Talk or presentation (not at a conference) › Academic
Research output
 1 Software

Completeness and the Finite Model Property for Kleene Algebra, Reconsidered (Coq formalization)
Kappé, T., 21 Dec 2022Research output: Nontextual form › Software › Academic
Open Access