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.