### Abstract

These files contain a formalisation of variants of Kleene algebras and their most important models as axiomatic type classes in Isabelle/HOL. Kleene algebras are foundational structures in computing with applications ranging from automata and language theory to computational modeling, program construction and verification.

We start with formalising dioids, which are additively idempotent semirings, and expand them by axiomatisations of the Kleene star for finite iteration and an omega operation for infinite iteration. We show that powersets over a given monoid, (regular) languages, sets of paths in a graph, sets of computation traces, binary relations and formal power series form Kleene algebras, and consider further models based on lattices, max-plus semirings and min-plus semirings. We also demonstrate that dioids are closed under the formation of matrices (proofs for Kleene algebras remain to be completed).

On the one hand we have aimed at a reference formalisation of variants of Kleene algebras that covers a wide range of variants and the core theorems in a structured and modular way and provides readable proofs at text book level. On the other hand, we intend to use this algebraic hierarchy and its models as a generic algebraic middle-layer from which programming applications can quickly be explored, implemented and verified.

### License

BSD License

### Topics

- Computer science/Programming languages/Logics
- Computer science/Automata and formal languages
- Mathematics/Algebra

### Session Kleene_Algebra

- Signatures
- Dioid
- Dioid_Models
- Matrix
- Conway
- Kleene_Algebra
- Kleene_Algebra_Models
- Omega_Algebra
- Omega_Algebra_Models
- DRA
- PHL_KA
- PHL_DRA
- Finite_Suprema
- Formal_Power_Series
- Inf_Matrix

### Used by

- Modal quantales, involutive quantales, Dedekind Quantales
- Quantales
- Kleene Algebras with Domain
- Binary Multirelations
- Regular Algebras
- Relation Algebra
- Kleene Algebra with Tests and Demonic Refinement Algebras

## Cite

×

Kleene_Algebra-AFP

    @article{Kleene_Algebra-AFP,
      author  = {Alasdair Armstrong and Georg Struth and Tjark Weber},
      title   = {Kleene Algebra},
      journal = {Archive of Formal Proofs},
      month   = {January},
      year    = {2013},
      note    = {\url{https://isa-afp.org/entries/Kleene_Algebra.html},
                 Formal proof development},
      ISSN    = {2150-914x},
    }

Download

## Download

× Download latest

Older releases:

- Sep 13, 2023 : Isabelle2023
- Oct 27, 2022 : Isabelle2022
- Dec 14, 2021 : Isabelle2021-1
- Feb 23, 2021 : Isabelle2021
- Apr 18, 2020 : Isabelle2020
- Jun 11, 2019 : Isabelle2019
- Aug 16, 2018 : Isabelle2018
- Oct 10, 2017 : Isabelle2017
- Dec 17, 2016 : Isabelle2016-1
- Feb 22, 2016 : Isabelle2016
- May 27, 2015 : Isabelle2015
- Aug 28, 2014 : Isabelle2014
- Dec 11, 2013 : Isabelle2013-2
- Nov 17, 2013 : Isabelle2013-1
- Mar 2, 2013 : Isabelle2013
- Feb 16, 2013 : Isabelle2013
- Jan 16, 2013 : Isabelle2012