Skip to main content

From Distributions to Probabilistic Reactive Programs

  • Conference paper
Theoretical Aspects of Computing – ICTAC 2013 (ICTAC 2013)

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

Included in the following conference series:

Abstract

We have introduced probability in the UTP framework by using functions from the state space to real numbers, which we term distributions, that are embedded in the predicates describing the different program constructs. This has allowed us to derive a probabilistic theory of designs starting from a probabilistic version of the relational theory, and continuing further down this road we can get to a theory of probabilistic reactive programs. This paper presents the route that connects these steps, and discusses the challenges lying ahead in view of a probabilistic CSP based on distributions.

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

Access this chapter

Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Bresciani, R., Butterfield, A.: Towards a UTP-style framework to deal with probabilities. Technical Report TCD-CS-2011-09, FMG, Trinity College Dublin, Ireland (August 2011)

    Google Scholar 

  2. Bresciani, R., Butterfield, A.: A probabilistic theory of designs based on distributions. In: Wolff, B., Gaudel, M.-C., Feliachi, A. (eds.) UTP 2012. LNCS, vol. 7681, pp. 105–123. Springer, Heidelberg (2013)

    Chapter  Google Scholar 

  3. Bresciani, R., Butterfield, A.: A UTP semantics of pGCL as a homogeneous relation. In: Derrick, J., Gnesi, S., Latella, D., Treharne, H. (eds.) IFM 2012. LNCS, vol. 7321, pp. 191–205. Springer, Heidelberg (2012)

    Chapter  Google Scholar 

  4. Butterfield, A. (ed.): UTP 2008. LNCS, vol. 5713. Springer, Heidelberg (2010)

    MATH  Google Scholar 

  5. Chen, Y., Sanders, J.W.: Unifying probability with nondeterminism. In: Cavalcanti, A., Dams, D.R. (eds.) FM 2009. LNCS, vol. 5850, pp. 467–482. Springer, Heidelberg (2009)

    Chapter  Google Scholar 

  6. Dijkstra, E.W.: A Discipline of Programming. Prentice-Hall (1976)

    Google Scholar 

  7. Dunne, S., Stoddart, B. (eds.): UTP 2006. LNCS, vol. 4010. Springer, Heidelberg (2006)

    MATH  Google Scholar 

  8. He, J.: A probabilistic BPEL-like language. In: Qin [Qin 2010], pp. 74–100 (2010)

    Google Scholar 

  9. Hehner, E.C.R.: Predicative programming — Part I & II. Commun. ACM 27(2), 134–151 (1984)

    Article  MathSciNet  MATH  Google Scholar 

  10. Hoare, C.A.R., He, J.: Unifying Theories of Programming. Prentice Hall International Series in Computer Science (1998)

    Google Scholar 

  11. Hoare, C.A.R.: Programs are predicates. In: Proceedings of a discussion meeting of the Royal Society of London on Mathematical Logic and Programming Languages, Upper Saddle River, NJ, USA, pp. 141–155. Prentice-Hall (1985)

    Google Scholar 

  12. He, J., Sanders, J.W.: Unifying probability. In: Dunne and Stoddart [DSO 2006], pp. 173–199 (2006)

    Google Scholar 

  13. Kozen, D.: Semantics of probabilistic programs. J. Comput. Syst. Sci. 22(3), 328–350 (1981)

    Article  MathSciNet  MATH  Google Scholar 

  14. Kozen, D.: A probabilistic PDL. J. Comput. Syst. Sci. 30(2), 162–178 (1985)

    Article  MathSciNet  MATH  Google Scholar 

  15. Mislove, M.W.: Nondeterminism and probabilistic choice: Obeying the laws. In: Palamidessi, C. (ed.) CONCUR 2000. LNCS, vol. 1877, pp. 350–365. Springer, Heidelberg (2000)

    Chapter  Google Scholar 

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

    Google Scholar 

  17. Morgan, C., McIver, A., Seidel, K., Sanders, J.W.: Refinement-oriented probability for CSP. Formal Asp. Comput. 8(6), 617–647 (1996)

    Article  MATH  Google Scholar 

  18. Morgan, C.: Of probabilistic Wp and CSP—and compositionality. In: Abdallah, A.E., Jones, C.B., Sanders, J.W. (eds.) CSP 2004. LNCS, vol. 3525, pp. 220–241. Springer, Heidelberg (2005)

    Chapter  Google Scholar 

  19. Oliveira, M., Cavalcanti, A., Woodcock, J.: A UTP semantics for Circus. Formal Asp. Comput 21(1-2), 3–32 (2009)

    Article  MATH  Google Scholar 

  20. Qin, S. (ed.): UTP 2010. LNCS, vol. 6445. Springer, Heidelberg (2010)

    MATH  Google Scholar 

Download references

Author information

Authors and Affiliations

Authors

Editor information

Editors and Affiliations

Rights and permissions

Reprints and permissions

Copyright information

© 2013 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Bresciani, R., Butterfield, A. (2013). From Distributions to Probabilistic Reactive Programs. In: Liu, Z., Woodcock, J., Zhu, H. (eds) Theoretical Aspects of Computing – ICTAC 2013. ICTAC 2013. Lecture Notes in Computer Science, vol 8049. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-39718-9_6

Download citation

  • DOI: https://doi.org/10.1007/978-3-642-39718-9_6

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-642-39717-2

  • Online ISBN: 978-3-642-39718-9

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics