Completeness and the Finite Model Property for Kleene Algebra, Reconsidered

Tobias Kappé

doi:10.1007/978-3-031-28083-2_10

Completeness and the Finite Model Property for Kleene Algebra, Reconsidered

Tobias Kappé^*

^*Corresponding author for this work

Research output: Chapter in Book/Report/Conference proceeding › Conference Article in proceeding › Academic › peer-review

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.

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	158-175
Number of pages	18
ISBN (Electronic)	9783031280832
ISBN (Print)	9783031280825
DOIs	https://doi.org/10.1007/978-3-031-28083-2_10
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	0302-9743

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

Access to Document

10.1007/978-3-031-28083-2_10Licence: CC BY

3 Talk or presentation (not at a conference)
1 Attending an event
1 Conference contribution (without a publication)

20th International Conference on Relational and Algebraic Methods in Computer Science
Kappé, T. (Participant / Attendee)
3 Apr 2023 → 6 Apr 2023
Activity: 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 2023
Activity: 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 2023
Activity: Talk or presentation types › Talk or presentation (not at a conference) › Academic

1 Software

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

Open Access

Cite this

@inproceedings{6d23f48acee942788033488f5348c989,

title = "Completeness and the Finite Model Property for Kleene Algebra, Reconsidered",

abstract = "Kleene Algebra (KA) is the algebra of regular expressions. Central to the study of KA is Kozen{\textquoteright}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{\textquoteright}s derivatives and the well-known transition monoid construction.Our results are fully verified in the Coq proof assistant.",

author = "Tobias Kapp{\'e}",

year = "2023",

doi = "10.1007/978-3-031-28083-2_10",

language = "English",

isbn = "9783031280825",

series = "Lecture Notes in Computer Science book series",

publisher = "Springer",

pages = "158--175",

editor = "Roland Gl{\"u}ck and Luigi Santocanale and Michael Winter",

booktitle = "Relational and Algebraic Methods in Computer Science",

note = "20th International Conference on Relational and Algebraic Methods in Computer Science, RAMiCS 2023 ; Conference date: 03-04-2023 Through 06-04-2023",

}

Kappé, T 2023, Completeness and the Finite Model Property for Kleene Algebra, Reconsidered. in R Glück, L Santocanale & M Winter (eds), Relational and Algebraic Methods in Computer Science. Springer, Lecture Notes in Computer Science book series, vol. 13896, pp. 158-175, 20th International Conference on Relational and Algebraic Methods in Computer Science, Augsburg, Germany, 3/04/23. https://doi.org/10.1007/978-3-031-28083-2_10

Completeness and the Finite Model Property for Kleene Algebra, Reconsidered. / Kappé, Tobias.
Relational and Algebraic Methods in Computer Science. ed. / Roland Glück; Luigi Santocanale; Michael Winter. Springer, 2023. p. 158-175 (Lecture Notes in Computer Science book series, Vol. 13896).

Research output: Chapter in Book/Report/Conference proceeding › Conference Article in proceeding › Academic › peer-review

TY - GEN

T1 - Completeness and the Finite Model Property for Kleene Algebra, Reconsidered

AU - Kappé, Tobias

N1 - Conference code: 20

PY - 2023

Y1 - 2023

N2 - 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.

AB - 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.

U2 - 10.1007/978-3-031-28083-2_10

DO - 10.1007/978-3-031-28083-2_10

M3 - Conference Article in proceeding

SN - 9783031280825

T3 - Lecture Notes in Computer Science book series

SP - 158

EP - 175

BT - Relational and Algebraic Methods in Computer Science

A2 - Glück, Roland

A2 - Santocanale, Luigi

A2 - Winter, Michael

PB - Springer

T2 - 20th International Conference on Relational and Algebraic Methods in Computer Science

Y2 - 3 April 2023 through 6 April 2023

ER -

Completeness and the Finite Model Property for Kleene Algebra, Reconsidered

Abstract

Publication series

Conference

Access to Document

Fingerprint

Activities

20th International Conference on Relational and Algebraic Methods in Computer Science