\documentclass[11pt,a4paper]{article}
\usepackage[T1]{fontenc}
\usepackage{isabelle,isabellesym}
\usepackage{amssymb,ragged2e}
\usepackage{pdfsetup}

\isabellestyle{it}
\renewenvironment{isamarkuptext}{\par\isastyletext\begin{isapar}\justifying\color{blue}}{\end{isapar}}
\renewcommand\labelitemi{$*$}

\begin{document}

\title{Stone-Kleene Relation Algebras}
\author{Walter Guttmann}
\maketitle

\begin{abstract}
  We develop Stone-Kleene relation algebras, which expand Stone relation algebras with a Kleene star operation to describe reachability in weighted graphs.
  Many properties of the Kleene star arise as a special case of a more general theory of iteration based on Conway semirings extended by simulation axioms.
  This includes several theorems representing complex program transformations.
  We formally prove the correctness of Conway's automata-based construction of the Kleene star of a matrix.
  We prove numerous results useful for reasoning about weighted graphs.
\end{abstract}

\tableofcontents

\section{Synopsis and Motivation}

This document describes the following five theory files:
\begin{itemize}
\item Iterings describes a general iteration operation that works for many different computation models.
      We first consider equational axioms based on variants of Conway semirings.
      We expand these structures by generalised simulation axioms, which hold in total and general correctness models, not just in partial correctness models like the induction axioms.
      Simulation axioms are still powerful enough to prove separation theorems and Back's atomicity refinement theorem \cite{BackWright1999}.
\item Kleene Algebras form a particular instance of iterings in which the iteration is implemented as a least fixpoint.
      We implement them based on Kozen's axioms \cite{Kozen1994}, but most results are inherited from Conway semirings and iterings.
\item Kleene Relation Algebras introduces Stone-Kleene relation algebras, which combine Stone relation algebras and Kleene algebras.
      This is similar to relation algebras with transitive closure \cite{Ng1984} but allows us to talk about reachability in weighted graphs.
      Many results in this theory are useful for verifying the correctness of Prim's and Kruskal's minimum spanning tree algorithms.
\item Subalgebras of Kleene Relation Algebras studies the regular elements of a Stone-Kleene relation algebra and shows that they form a Kleene relation subalgebra.
\item Matrix Kleene Algebras lifts the Kleene star to finite square matrices using Conway's automata-based construction.
      This involves an operation to restrict matrices to specific indices and a calculus for such restrictions.
      An implementation for the Kleene star of matrices was given in \cite{Asplund2014} without proof; this is the first formally verified correctness proof.
\end{itemize}
The development is based on a theory of Stone relation algebras \cite{Guttmann2017a,Guttmann2017b}.
We apply Stone-Kleene relation algebras to verify Prim's minimum spanning tree algorithm in Isabelle/HOL in \cite{Guttmann2016c}.

Related libraries for Kleene algebras, regular algebras and relation algebras in the Archive of Formal Proofs are \cite{ArmstrongFosterStruthWeber2016,ArmstrongGomesStruthWeber2016,FosterStruth2016}.
Kleene algebras are covered in the theory \texttt{Kleene\_Algebra/Kleene\_Algebra.thy}, but unlike the present development it is not based on general algebras using simulation axioms, which are useful to describe various computation models.
The theory \texttt{Regular\_Algebras/Regular\_Algebras.thy} compares different axiomatisations of regular algebras.
The theory \texttt{Kleene\_Algebra/Matrix.thy} covers matrices over dioids, but does not implement the Kleene star of matrices.
The theory \texttt{Relation\_Algebra/Relation\_Algebra\_RTC.thy} combines Kleene algebras and relation algebras, but is very limited in scope and not applicable as we need the weaker axioms of Stone relation algebras.

\begin{flushleft}
\input{session}
\end{flushleft}

\bibliographystyle{abbrv}
\bibliography{root}

\end{document}

