Probabilistic Choice in Refinement Algebra

  • Larissa Meinicke
  • Ian J. Hayes
Part of the Lecture Notes in Computer Science book series (LNCS, volume 5133)


The term refinement algebra refers to a set of abstract algebras, similar to Kleene algebra with tests, that are suitable for reasoning about programs in a total-correctness framework. Abstract algebraic reasoning also works well when probabilistic programs are concerned, and a general refinement algebra that is suitable for such programs has been defined previously. That refinement algebra does not contain features that are specific to probabilistic programs. For instance, it does not include a probabilistic choice operator, or probabilistic assertions and guards (tests), which may be used to represent correctness properties for probabilistic programs. In this paper we investigate how these features may be included in a refinement algebra. That is, we propose a new refinement algebra in which probabilistic choice, and probabilistic guards and assertions may be expressed. Two operators for modelling probabilistic enabledness and termination are also introduced.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    Desharnais, J., Möller, B., Struth, G.: Kleene algebra with domain. ACM Transactions on Computational Logic 7(4), 798–833 (2006)MathSciNetGoogle Scholar
  2. 2.
    Dijkstra, E.W.: A Discipline of Programming. Prentice Hall, Englewood Cliffs (1976)zbMATHGoogle Scholar
  3. 3.
    Dijkstra, E.W., Scholten, C.S.: Predicate Calculus and Program Semantics. Springer, Heidelberg (1990)zbMATHGoogle Scholar
  4. 4.
    Hehner, E.C.R.: Probabilistic Predicative Programming. In: Kozen, D. (ed.) MPC 2004. LNCS, vol. 3125, pp. 169–185. Springer, Heidelberg (2004)Google Scholar
  5. 5.
    Kozen, D.: Kleene algebra with tests. ACM Transactions on Programming Languages and Systems 19(3), 427–443 (1997)CrossRefGoogle Scholar
  6. 6.
    McIver, A., Morgan, C.: Abstraction, Refinement and Proof for Probabilistic Systems. Monographs in Computer Science. Springer, Heidelberg (2005)zbMATHGoogle Scholar
  7. 7.
    Meinicke, L., Hayes, I.J.: Algebraic reasoning for probabilistic action systems and while-loops. DOI: 10.1007/s00236-008-0073-4. Accepted to Acta Informatica (March 2008)Google Scholar
  8. 8.
    Meinicke, L., Solin, K.: Reactive probabilistic programs and refinement algebra. In: Berghammer, R., Möller, B., Struth, G. (eds.) Relations and Kleene Algebra in Computer Science. LNCS, vol. 4988, pp. 304–319. Springer, Heidelberg (2008)CrossRefGoogle Scholar
  9. 9.
    Meinicke, L., Solin, K.: Refinement algebra for probabilistic programs. Electron. Notes Theor. Comput. Sci. 201, 177–195 (2008)CrossRefGoogle Scholar
  10. 10.
    Morgan, C., McIver, A.: Cost analysis of games using program logic. In: APSEC 2001: Proceedings of the Eighth Asia-Pacific on Software Engineering Conference, p. 351. IEEE Computer Society, Washington (2001)CrossRefGoogle Scholar
  11. 11.
    Morgan, C., McIver, A.: Cost analysis of games using program logic (2001),
  12. 12.
    Morgan, C., McIver, A., Seidel, K.: Probabilistic predicate transformers. ACM Transactions on Programming Languages and Systems 18(3), 325–353 (1996)CrossRefGoogle Scholar
  13. 13.
    Solin, K.: On Two Dually Nondeterministic Refinement Algebras. In: Schmidt, R.A. (ed.) RelMiCS/AKA 2006. LNCS, vol. 4136, pp. 373–387. Springer, Heidelberg (2006)CrossRefGoogle Scholar
  14. 14.
    Solin, K., von Wright, J.: Refinement Algebra with Operators for Enabledness and Termination. In: Uustalu, T. (ed.) MPC 2006. LNCS, vol. 4014, pp. 397–415. Springer, Heidelberg (2006)CrossRefGoogle Scholar
  15. 15.
    von Wright, J.: From Kleene Algebra to Refinement Algebra. In: Boiten, E.A., Möller, B. (eds.) MPC 2002. LNCS, vol. 2386, pp. 233–262. Springer, Heidelberg (2002)CrossRefGoogle Scholar
  16. 16.
    von Wright, J.: Towards a refinement algebra. Science of Computer Programming 51, 23–45 (2004)zbMATHCrossRefMathSciNetGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2008

Authors and Affiliations

  • Larissa Meinicke
    • 1
  • Ian J. Hayes
    • 2
  1. 1.Department of Computer ScienceÅbo AkademiFinland
  2. 2.School of Information Technology and Electrical EngineeringThe University of QueenslandAustralia

Personalised recommendations