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.
License
Topics
Session Stone_Kleene_Relation_Algebras
- Iterings
- Kleene_Algebras
- Kleene_Relation_Algebras
- Kleene_Relation_Subalgebras
- Matrix_Kleene_Algebras