[go: up one dir, main page]
More Web Proxy on the site http://driver.im/
Skip to main content
Springer Nature Link
Log in

Probabilistic Choice in Refinement Algebra

  • Conference paper
Mathematics of Program Construction (MPC 2008)

Part of the book series: Lecture Notes in Computer Science ((LNTCS,volume 5133))

Included in the following conference series:

Abstract

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.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

Similar content being viewed by others

References

  1. Desharnais, J., Möller, B., Struth, G.: Kleene algebra with domain. ACM Transactions on Computational Logic 7(4), 798–833 (2006)

    MathSciNet  Google Scholar 

  2. Dijkstra, E.W.: A Discipline of Programming. Prentice Hall, Englewood Cliffs (1976)

    MATH  Google Scholar 

  3. Dijkstra, E.W., Scholten, C.S.: Predicate Calculus and Program Semantics. Springer, Heidelberg (1990)

    MATH  Google Scholar 

  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. Kozen, D.: Kleene algebra with tests. ACM Transactions on Programming Languages and Systems 19(3), 427–443 (1997)

    Article  Google Scholar 

  6. McIver, A., Morgan, C.: Abstraction, Refinement and Proof for Probabilistic Systems. Monographs in Computer Science. Springer, Heidelberg (2005)

    MATH  Google Scholar 

  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. 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)

    Chapter  Google Scholar 

  9. Meinicke, L., Solin, K.: Refinement algebra for probabilistic programs. Electron. Notes Theor. Comput. Sci. 201, 177–195 (2008)

    Article  Google Scholar 

  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)

    Chapter  Google Scholar 

  11. Morgan, C., McIver, A.: Cost analysis of games using program logic (2001), http://www.cse.unsw.edu.au/~carrollm/probs/bibliography.html

  12. Morgan, C., McIver, A., Seidel, K.: Probabilistic predicate transformers. ACM Transactions on Programming Languages and Systems 18(3), 325–353 (1996)

    Article  Google Scholar 

  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)

    Chapter  Google Scholar 

  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)

    Chapter  Google Scholar 

  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)

    Chapter  Google Scholar 

  16. von Wright, J.: Towards a refinement algebra. Science of Computer Programming 51, 23–45 (2004)

    Article  MATH  MathSciNet  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Department of Computer Science, Åbo Akademi, Finland

    Larissa Meinicke

  2. School of Information Technology and Electrical Engineering, The University of Queensland, Australia

    Ian J. Hayes

Authors
  1. Larissa Meinicke
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Ian J. Hayes
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Philippe Audebaud Christine Paulin-Mohring

Rights and permissions

Reprints and permissions

Copyright information

© 2008 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Meinicke, L., Hayes, I.J. (2008). Probabilistic Choice in Refinement Algebra. In: Audebaud, P., Paulin-Mohring, C. (eds) Mathematics of Program Construction. MPC 2008. Lecture Notes in Computer Science, vol 5133. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-70594-9_14

Download citation

  • DOI: https://doi.org/10.1007/978-3-540-70594-9_14

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-70593-2

  • Online ISBN: 978-3-540-70594-9

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation