Greedy-like algorithms in Kleene algebra

erschienen Mai 2003 7th Seminar Relational Methods in Computer Science and 2nd International Workshop on Applications of Kleene Algebra.
pp. 173-180, Malente, Germany, Mai 2003.
In R. Berghammer, B. Möller (eds.): Participants' Proc. 7th Seminar Relational Methods in Computer Science and 2nd International Workshop on Applications of Kleene Algebra.
Final version.

Abstract:
This paper provides an algebraic background for the formal derivation of greedy-like algorithms. Such derivations have previously been done in various frameworks including relation algebra. We propose Kleene algebra as a particularly simple alternative. Instead of converse and residuation we use modal operators that are definable in a wide class of algebras, based on domain/codomain or image/pre-image operations. By abstracting from earlier approaches we arrive at a very general theorem about the correctness of loops that covers particular forms of greedy algorithms as special cases.