Greedy-Like Algorithms in Modal Kleene Algebra

  • Bernhard Möller
  • Georg Struth
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 3051)


This study provides an algebraic background for the formal derivation of greedy-like algorithms. We propose Kleene algebra as a particularly simple alternative to previous approaches such as relation algebra. 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.


Idempotent semiring Kleene algebra image and preimage operation modal operators confluence Geach formula program development and analysis 


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    Bird, R.S., de Moor, O.: Algebra of programming. Prentice Hall, Englewood Cliffs (1997)zbMATHGoogle Scholar
  2. 2.
    Curtis, S.A.: A relational approach to optimization problems. D.Phil. Thesis. Technical Monograph PRG-122, Oxford University Computing Laboratory (1996)Google Scholar
  3. 3.
    Desharnais, J., Möller, B., Struth, G.: Kleene algebra with domain. Technical Report 2003-07, Universität Augsburg, Institut für Informatik (2003)Google Scholar
  4. 4.
    Durán, J.E.: Transformational derivation of greedy network algorithms from descriptive specifications. In: Boiten, E.A., Möller, B. (eds.) MPC 2002. LNCS, vol. 2386, pp. 40–67. Springer, Heidelberg (2002)CrossRefGoogle Scholar
  5. 5.
    Freyd, P., Scedrov, A.: Categories, allegories. North-Holland, Amsterdam (1990)zbMATHGoogle Scholar
  6. 6.
    Helman, P., Moret, B.M.E., Shapiro, H.D.: An exact characterization of greedy structures. SIAM Journal on Discrete Mathematics 6, 274–283 (1993)zbMATHCrossRefMathSciNetGoogle Scholar
  7. 7.
    Korte, B., Lovász, L., Schrader, R.: Greedoids. Springer, Heidelberg (1991)zbMATHGoogle Scholar
  8. 8.
    Kozen, D.: A completeness theorem for Kleene algebras and the algebra of regular events. Information and Computation 110, 366–390 (1994)zbMATHCrossRefMathSciNetGoogle Scholar
  9. 9.
    Kozen, D.: Kleene algebra with tests. Transactions on Programming Languages and Systems 19, 427–443 (1997)CrossRefGoogle Scholar
  10. 10.
    Möller, B.: Derivation of graph and pointer algorithms. In: Möller, B., Schuman, S., Partsch, H. (eds.) Formal Program Development. LNCS, vol. 755, pp. 123–160. Springer, Heidelberg (1993)Google Scholar
  11. 11.
    Möller, B., Struth, G.: Modal Kleene algebra and partial correctness. Technical Report 2003-08, Universität Augsburg, Institut für Informatik (2003)Google Scholar
  12. 12.
    Popkorn, S.: First steps in modal logic. Cambridge University Press, Cambridge (1994)zbMATHGoogle Scholar
  13. 13.
    Struth, G.: Calculating Church-Rosser proofs in Kleene algebra. In: de Swart, H. (ed.) RelMiCS 2001. LNCS, vol. 2561, pp. 276–290. Springer, Heidelberg (2002)CrossRefGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2004

Authors and Affiliations

  • Bernhard Möller
    • 1
  • Georg Struth
    • 1
  1. 1.Institut für InformatikUniversität AugsburgAugsburgGermany

Personalised recommendations