kad.bbl
\begin{thebibliography}{}

\bibitem[\protect\citeauthoryear{Aarts}{Aarts}{1992}]{Aarts92}
{\sc Aarts, C.~J.} 1992.
\newblock Galois connections presented calculationally.
\newblock M.S.\ thesis, Eindhoven University of Technology, Department of
  Mathematics and Computing Science.

\bibitem[\protect\citeauthoryear{Abrial}{Abrial}{1996}]{Abrial96}
{\sc Abrial, J.-R.} 1996.
\newblock {\em The B-Book}.
\newblock Cambridge University Press.

\bibitem[\protect\citeauthoryear{Apt and Olderog}{Apt and
  Olderog}{1997}]{AptOlderog97}
{\sc Apt, K.-R.} {\sc and} {\sc Olderog, E.-R.} 1997.
\newblock {\em Verification of Sequential and Concurrent Programs\/}, 2nd ed.
\newblock Springer.

\bibitem[\protect\citeauthoryear{Birkhoff}{Birkhoff}{1984}]{Birkhoff84}
{\sc Birkhoff, G.} 1984.
\newblock {\em Lattice Theory}. Colloquium Publications, vol.~25.
\newblock American Mathematical Society.
\newblock Reprint.

\bibitem[\protect\citeauthoryear{Bull and Segerberg}{Bull and
  Segerberg}{1984}]{BullSegerberg84}
{\sc Bull, R.} {\sc and} {\sc Segerberg, K.} 1984.
\newblock Basic modal logic.
\newblock In {\em Handbook of Philosophical Logic}, {D.~Gabbay} {and}
  {F.~Guenthner}, Eds. Vol.~II. D. Reidel, Chapter II.1, 1--88.

\bibitem[\protect\citeauthoryear{Chellas}{Chellas}{1980}]{Chellas80}
{\sc Chellas, B.~F.} 1980.
\newblock {\em Modal Logic: An Introduction}.
\newblock Cambridge University Press.

\bibitem[\protect\citeauthoryear{Cohen}{Cohen}{1994}]{Cohen94a}
{\sc Cohen, E.} 1994.
\newblock Hypotheses in {K}leene algebra.
\newblock Unpublished manuscript.

\bibitem[\protect\citeauthoryear{Cohen}{Cohen}{2000}]{Cohen00}
{\sc Cohen, E.} 2000.
\newblock Separation and reduction.
\newblock In {\em Proc. of Mathematics of Program Construction, 5th
  International Conference, MPC 2000}, {R.~Backhouse} {and} {J.~N. Oliveira},
  Eds. LNCS, vol. 1837. Springer, 45--59.

\bibitem[\protect\citeauthoryear{Conway}{Conway}{1971}]{Conway71}
{\sc Conway, J.~H.} 1971.
\newblock {\em Regular Algebra and Finite State Machines}.
\newblock Chapman and Hall.

\bibitem[\protect\citeauthoryear{Crvenkovi\v{c}, Dolinka, and
  \'{E}sik}{Crvenkovi\v{c} et~al\mbox{.}}{2000}]{CrvenkovicDolinkaEsik00}
{\sc Crvenkovi\v{c}, S.}, {\sc Dolinka, I.}, {\sc and} {\sc \'{E}sik, Z.} 2000.
\newblock The variety of {K}leene algebras with conversion is not finitely
  based.
\newblock {\em Theoretical Computer Science\/}~{\em 230}, 235--245.

\bibitem[\protect\citeauthoryear{Desharnais and M{\"o}ller}{Desharnais and
  M{\"o}ller}{2001}]{DesharnaisMoeller01}
{\sc Desharnais, J.} {\sc and} {\sc M{\"o}ller, B.} 2001.
\newblock Characterizing determinacy in {K}leene algebras.
\newblock {\em Information Sciences\/}~{\em 139,\/}~3--4, 253--273.

\bibitem[\protect\citeauthoryear{Desharnais, M{\"o}ller, and Tchier}{Desharnais
  et~al\mbox{.}}{2000}]{DesharnaisMoellerTchier00}
{\sc Desharnais, J.}, {\sc M{\"o}ller, B.}, {\sc and} {\sc Tchier, F.} 2000.
\newblock {K}leene under a demonic star.
\newblock In {\em Algebraic Methodology and Software Technology}, {T.~Rus}, Ed.
  LNCS, vol. 1816. Springer, 355--370.

\bibitem[\protect\citeauthoryear{Dijkstra}{Dijkstra}{1976}]{Dijkstra76}
{\sc Dijkstra, E.~W.} 1976.
\newblock {\em A Discipline of Programming}.
\newblock Prentice Hall.

\bibitem[\protect\citeauthoryear{Ehm, M{\"o}ller, and Struth}{Ehm
  et~al\mbox{.}}{2003}]{EhmMolStr03}
{\sc Ehm, T.}, {\sc M{\"o}ller, B.}, {\sc and} {\sc Struth, G.} 2003.
\newblock {K}leene modules.
\newblock In {\em Participants' Proceedings 7th RelMiCS/2nd Kleene Workshop,
  Malente, May 12--17, 2003}, {R.~Berghammer} {and} {B.~M{\"o}ller}, Eds.
  Universit\"at Kiel, Germany, 21--27.

\bibitem[\protect\citeauthoryear{Eilenberg}{Eilenberg}{1974}]{Eilenberg74}
{\sc Eilenberg, S.} 1974.
\newblock {\em Automata, Languages and Machines}. Vol.~A.
\newblock Academic Press.

\bibitem[\protect\citeauthoryear{Fischer and Ladner}{Fischer and
  Ladner}{1979}]{FischerLadner79}
{\sc Fischer, J.~M.} {\sc and} {\sc Ladner, R.~F.} 1979.
\newblock Propositional dynamic logic of regular programs.
\newblock {\em J. Comput. System Sci.\/}~{\em 18,\/}~2, 194--211.

\bibitem[\protect\citeauthoryear{Gaubert and Plus}{Gaubert and
  Plus}{1997}]{MaxPlus}
{\sc Gaubert, S.} {\sc and} {\sc Plus, M.} Jan. 1997.
\newblock Methods and applications of (max,+) linear algebra.
\newblock Tech. Rep. RR-3088, INRIA- Rocquencourt.

\bibitem[\protect\citeauthoryear{Goldblatt}{Goldblatt}{1985}]{Goldblatt85}
{\sc Goldblatt, R.} 1985.
\newblock An algebraic study of well-foundedness.
\newblock {\em Studia Logica\/}~{\em 44,\/}~4, 422--437.

\bibitem[\protect\citeauthoryear{Harel, Kozen, and Tiuryn}{Harel
  et~al\mbox{.}}{2000}]{HarelKozenTiuryn00}
{\sc Harel, D.}, {\sc Kozen, D.}, {\sc and} {\sc Tiuryn, J.} 2000.
\newblock {\em Dynamic Logic}.
\newblock MIT Press.

\bibitem[\protect\citeauthoryear{Hoare and von Karger}{Hoare and von
  Karger}{1995}]{HoarevKarger95}
{\sc Hoare, C. A.~R.} {\sc and} {\sc von Karger, B.} 1995.
\newblock Sequential calculus.
\newblock {\em Information Processing Letters\/}~{\em 53,\/}~3, 123--130.

\bibitem[\protect\citeauthoryear{Hollenberg}{Hollenberg}{1997}]{Hollenberg97}
{\sc Hollenberg, M.} 1997.
\newblock Equational axioms of test algebra.
\newblock In {\em Computer Science Logic, 11th International Workshop, CSL
  '97}, {M.~Nielsen} {and} {W.~Thomas}, Eds. LNCS, vol. 1414. Springer,
  295--310.

\bibitem[\protect\citeauthoryear{Kozen}{Kozen}{1979a}]{Kozen79b}
{\sc Kozen, D.} 1979a.
\newblock On the duality of dynamic algebras and {K}ripke models.
\newblock In {\em Workshop on Logic of Programs}, {E.~Engeler}, Ed. LNCS, vol.
  125. Springer, 1--11.

\bibitem[\protect\citeauthoryear{Kozen}{Kozen}{1979b}]{Kozen79}
{\sc Kozen, D.} 1979b.
\newblock A representation theorem for $\ast$-free {PDL}.
\newblock Tech. Rep. RC7864, IBM.

\bibitem[\protect\citeauthoryear{Kozen}{Kozen}{1994a}]{Kozen94}
{\sc Kozen, D.} 1994a.
\newblock A completeness theorem for {K}leene algebras and the algebra of
  regular events.
\newblock {\em Information and Computation\/}~{\em 110,\/}~2, 366--390.

\bibitem[\protect\citeauthoryear{Kozen}{Kozen}{1994b}]{Kozen94b}
{\sc Kozen, D.} 1994b.
\newblock On action algebras.
\newblock In {\em Logic and Information Flow}, {J.~van Eijck} {and}
  {A.~Visser}, Eds. MIT Press, 78--88.

\bibitem[\protect\citeauthoryear{Kozen}{Kozen}{1997}]{Kozen97}
{\sc Kozen, D.} 1997.
\newblock Kleene algebra with tests.
\newblock {\em Trans. Programming Languages and Systems\/}~{\em 19,\/}~3,
  427--443.

\bibitem[\protect\citeauthoryear{Kozen}{Kozen}{2001}]{Kozen01}
{\sc Kozen, D.} 2001.
\newblock On {H}oare logic and {K}leene algebra with tests.
\newblock {\em Trans. Computational Logic\/}~{\em 1,\/}~1, 60--76.

\bibitem[\protect\citeauthoryear{Kozen and Smith}{Kozen and
  Smith}{1996}]{KozenSmith96}
{\sc Kozen, D.} {\sc and} {\sc Smith, F.} 1996.
\newblock Kleene algebra with tests: Completeness and decidability.
\newblock In {\em Proc. of 10th International Workshop on Computer Science
  Logic (CSL'96)}, {D.~van Dalen} {and} {M.~Bezem}, Eds. LNCS, vol. 1258.
  Springer, 244--259.

\bibitem[\protect\citeauthoryear{Kuich}{Kuich}{1997}]{Kuich97}
{\sc Kuich, W.} 1997.
\newblock Semirings and formal power series: Their relevance to formal
  languages and automata.
\newblock In {\em Handbook of Formal Language Theory}, {G.~Rozenberg} {and}
  {A.~Salomaa}, Eds. Vol.~I. Springer-Verlag, 609--677.

\bibitem[\protect\citeauthoryear{Loeckx and Sieber}{Loeckx and
  Sieber}{1987}]{LoeckxSieber87}
{\sc Loeckx, J.} {\sc and} {\sc Sieber, K.} 1987.
\newblock {\em The Foundations of Program Verification\/}, 2nd ed.
\newblock Wiley Teubner.

\bibitem[\protect\citeauthoryear{M{\"o}ller}{M{\"o}ller}{1999}]{Moeller99}
{\sc M{\"o}ller, B.} 1999.
\newblock {T}yped {K}leene algebras.
\newblock Tech. Rep. 1999-08, Universit\"at Augsburg, Institut f\"ur
  Informatik.

\bibitem[\protect\citeauthoryear{M{\"o}ller and Struth}{M{\"o}ller and
  Struth}{2003a}]{MolStrGreedy03}
{\sc M{\"o}ller, B.} {\sc and} {\sc Struth, G.} 2003a.
\newblock {G}reedy-like algorithms in {K}leene algebra.
\newblock In {\em Participants' Proceedings 7th RelMiCS/2nd Kleene Workshop,
  Malente, May 12--17, 2003}, {R.~Berghammer} {and} {B.~M{\"o}ller}, Eds.
  Universit\"at Kiel, Germany, 173--180.

\bibitem[\protect\citeauthoryear{M{\"o}ller and Struth}{M{\"o}ller and
  Struth}{2003b}]{MolStrPC03}
{\sc M{\"o}ller, B.} {\sc and} {\sc Struth, G.} June 2003b.
\newblock Modal {K}leene algebra and partial correctness.
\newblock Tech. Rep. 2003-08, Universit\"at Augsburg, Institut f\"ur
  Informatik.

\bibitem[\protect\citeauthoryear{Mulvey}{Mulvey}{1986}]{Mulvey86}
{\sc Mulvey, C.} 1986.
\newblock $\&$.
\newblock {\em Rend. Circ. Math. Palermo\/}~{\em 2,\/}~12, 99--104.

\bibitem[\protect\citeauthoryear{N{\'e}meti}{N{\'e}meti}{1981}]{Nemeti81}
{\sc N{\'e}meti, I.} 1981.
\newblock Dynamic algebras of programs.
\newblock In {\em Proc. FCT'81 --- Fundamentals of Computation Theory}. LNCS,
  vol. 117. Springer, 281--291.

\bibitem[\protect\citeauthoryear{Pratt}{Pratt}{1988}]{Pratt88}
{\sc Pratt, V.} 1988.
\newblock Dynamic logic as a well-behaved fragment of relation algebras.
\newblock In {\em Conference on Algebra and Computer Science}, {D.~Pigozzi},
  Ed. LNCS, vol. 425. Springer, 77--110.

\bibitem[\protect\citeauthoryear{Pratt}{Pratt}{1990}]{Pratt90}
{\sc Pratt, V.} 1990.
\newblock Action logic and pure induction.
\newblock In {\em Logics in AI, European Workshop, JELIA'90}, {J.~van Eijck},
  Ed. LNCS, vol. 478. Springer, 97--110.

\bibitem[\protect\citeauthoryear{Pratt}{Pratt}{1991}]{Pratt91}
{\sc Pratt, V.} 1991.
\newblock Dynamic algebras: Examples, constructions, applications.
\newblock {\em Studia Logica\/}~{\em 50}, 571--605.

\bibitem[\protect\citeauthoryear{Schmidt and Str{\"o}hlein}{Schmidt and
  Str{\"o}hlein}{1993}]{SchmidtStroehlein93}
{\sc Schmidt, G.~W.} {\sc and} {\sc Str{\"o}hlein, T.} 1993.
\newblock {\em Relations and Graphs: Discrete Mathematics for Computer
  Scientists}.
\newblock EATCS Monographs on Theoretical Computer Science. Springer.

\bibitem[\protect\citeauthoryear{Spivey}{Spivey}{1988}]{Spivey88}
{\sc Spivey, J.~M.} 1988.
\newblock {\em Understanding Z}.
\newblock Cambridge University Press.

\bibitem[\protect\citeauthoryear{Trnkova and Reiterman}{Trnkova and
  Reiterman}{1987}]{TrnkovaReiterman87}
{\sc Trnkova, V.} {\sc and} {\sc Reiterman, J.} 1987.
\newblock Dynamic algebras with tests.
\newblock {\em J. Comput. System Sci.\/}~{\em 35}, 229--242.

\bibitem[\protect\citeauthoryear{von Wright}{von Wright}{2002}]{vWright02}
{\sc von Wright, J.} 2002.
\newblock From {K}leene algebra to refinement algebra.
\newblock In {\em Mathematics of Program Construction, 6th International
  Conference, MPC 2002}, {B.~M{\"o}ller} {and} {E.~Boiten}, Eds. LNCS, vol.
  2386. Springer, 233--262.

\bibitem[\protect\citeauthoryear{Yetter}{Yetter}{1990}]{Yetter90}
{\sc Yetter, D.} 1990.
\newblock Quantales and (non-commutative) linear logic.
\newblock {\em J. Symbolic Logic\/}~{\em 55,\/}~1, 41--64.

\end{thebibliography}
