Reasoning Algebraically About Probabilistic Loops

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


Back and von Wright have developed algebraic laws for reasoning about loops in the refinement calculus. We extend their work to reasoning about probabilistic loops in the probabilistic refinement calculus. We apply our algebraic reasoning to derive transformation rules for probabilistic action systems. In particular we focus on developing data refinement rules for probabilistic action systems. Our extension is interesting since some well known transformation rules that are applicable to standard programs are not applicable to probabilistic ones: we identify some of these important differences and we develop alternative rules where possible. In particular, our probabilistic action system data refinement rules are new.


Transformation Rule Complete Lattice Probabilistic Program Reasoning Algebraically Predicate Transformer 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    Back, R.-J., von Wright, J.: Trace refinement of action systems. In: Jonsson, B., Parrow, J. (eds.) CONCUR 1994. LNCS, vol. 836, pp. 367–384. Springer, Heidelberg (1994)CrossRefGoogle Scholar
  2. 2.
    Back, R.-J., von Wright, J.: Refinement Calculus: A Systematic Introduction. Springer, Heidelberg (1998)zbMATHGoogle Scholar
  3. 3.
    Back, R.J.R., Kurki-Suonio, R.: Decentralization of process nets with centralized control. In: Proc. of the 2nd ACM SIGACT-SIGOPS Symp. on Principles of Distributed Computing, pp. 131–142. ACM Press, New York (1983)Google Scholar
  4. 4.
    Back, R.J.R., Kurki-Suonio, R.: Distributed cooperation with action systems. ACM Trans. Program. Lang. Syst. 10(4), 513–554 (1988)zbMATHCrossRefGoogle Scholar
  5. 5.
    Back, R.J.R., von Wright, J.: Reasoning algebraically about loops. Acta Informatica 36, 295–334 (1999)zbMATHCrossRefMathSciNetGoogle Scholar
  6. 6.
    Cohen, E.: Hypotheses in Kleene algebra. Technical Report TM-ARH-023814, Belcore (1994)Google Scholar
  7. 7.
    Cohen, E.: Separation and reduction. In: Backhouse, R., Oliveira, J.N. (eds.) MPC 2000. LNCS, vol. 1837, pp. 45–59. Springer, Heidelberg (2000)CrossRefGoogle Scholar
  8. 8.
    Davey, B.A., Priestley, H.A.: Introduction to Lattices. Cambridge University Press, Cambridge (1990)zbMATHGoogle Scholar
  9. 9.
    Dijkstra, E.W.: A Discipline of Programming. Prentice Hall, Englewood Cliffs (1976)zbMATHGoogle Scholar
  10. 10.
    He, J., Seidel, K., McIver, A.: Probabilistic models for the guarded command language. Science of Computer Programming 28(2-3), 171–192 (1997)zbMATHCrossRefMathSciNetGoogle Scholar
  11. 11.
    Hurd, J.: A formal approach to probabilistic termination. In: Carreño, V.A., Muñoz, C.A., Tahar, S. (eds.) TPHOLs 2002. LNCS, vol. 2410, pp. 230–245. Springer, Heidelberg (2002)CrossRefGoogle Scholar
  12. 12.
    Kozen, D.: Kleene algebra with tests. ACM Transactions on Programming Languages and Systems 19(3), 427–443 (1997)CrossRefGoogle Scholar
  13. 13.
    McIver, A., Morgan, C.: Abstraction, Refinement and Proof for Probabilistic Systems. Monographs in Computer Science. Springer, Heidelberg (2005)zbMATHGoogle Scholar
  14. 14.
    Möller, B.: Lazy Kleene algebra. In: Kozen, D. (ed.) MPC 2004. LNCS, vol. 3125, pp. 252–273. Springer, Heidelberg (2004)CrossRefGoogle Scholar
  15. 15.
    Morgan, C.: Programming from Specifications, 2nd edn. Prentice Hall, Englewood Cliffs (1994)zbMATHGoogle Scholar
  16. 16.
    Sere, K., Troubitsyna, E.: Probabilities in action systems. In: Proc. of the 8th Nordic Workshop on Programming Theory (1996)Google Scholar
  17. 17.
    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
  18. 18.
    Troubitsyna, E.A.: Reliability assessment through probabilistic refinement. Nordic Journal of Computing, 320–342 (1999)Google Scholar
  19. 19.
    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
  20. 20.
    von Wright, J.: Towards a refinement algebra. Science of Computer Programming 51 (2004)Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2006

Authors and Affiliations

  • Larissa Meinicke
    • 1
  • Ian J. Hayes
    • 1
  1. 1.School of Information Technology and Electrical EngineeringThe University of QueenslandBrisbaneAustralia

Personalised recommendations