More Web Proxy on the site http://driver.im/

research-article

Open access

Refinement algebra for probabilistic programs

Authors:

Larissa Meinicke,

Kim SolinAuthors Info & Claims

Formal Aspects of Computing, Volume 22, Issue 1

Pages 3 - 31

https://doi.org/10.1007/s00165-009-0111-1

Published: 01 January 2010 Publication History

Abstract

We identify a refinement algebra for reasoning about probabilistic program transformations in a total-correctness setting. The algebra is equipped with operators that determine whether a program is enabled or terminates respectively. As well as developing the basic theory of the algebra we demonstrate how it may be used to explain key differences and similarities between standard (i.e. non-probabilistic) and probabilistic programs and verify important transformation theorems for probabilistic action systems.

References

References

[1]

Back RJR (1989) A method for refining atomicity in parallel algorithms. In: PARLE’89 conference on parallel architectures and languages Europe. Lecture notes in computer science, vol 366, pp 199–216. Springer, Berlin

[2]

Back RJR, Kurki-Suonio R (1983) Decentralization of process nets with centralized control. In: Proceedings of the 2nd ACM SIGACT-SIGOPS symposium on principles of distributed computing. ACM Press, New York, pp 131–142

[3]

Back RJR and von Wright J Refinement calculus: a systematic introduction 1998 Berlin Springer

[4]

Back RJR and von Wright J Reasoning algebraically about loops Acta Inform 1999 36 4 295-334

[5]

Cohen E (2000) Separation and reduction. In: Mathematics of program construction. Lecture notes in computer science, vol 1837, pp 45–59. Springer, Berlin

[6]

Dijkstra EW A discipline of programming 1976 Englewood Cliffs Prentice-Hall

Digital Library

[7]

Desharnais J, Möller B, and Struth G Kleene algebra with domain ACM Trans Comput Logic 2006 7 4 798-833

Digital Library

[8]

Doeppner TW (1977) Parallel program correctness through refinement. In: ACM symposium on principles of programming languages. ACM, New York, pp 155–169

[9]

Davey BA and Priestley HA Introduction to lattices and order 1990 Cambridge Cambridge University Press

[10]

Dijkstra EW and Scholten CS Predicate calculus and program semantics 1990 Berlin Springer

Digital Library

[11]

Ehm T (2003) The Kleene algebra of nested pointer structures: theory and applications. PhD thesis, University of Augsburg, December 2003

[12]

Höfner P and Struth G Can refinement be automated? Electron Notes Theor Comput Sci 2008 201 197-222

Digital Library

[13]

Kozen D (1990) On Kleene algebras and closed semirings. In: MFCS ’90: proceedings on mathematical foundations of computer science. Lecture notes in computer science, vol 452, pp 26–47. Springer, Berlin

[14]

Kozen D A completeness theorem for Kleene algebras and the algebra of regular events Inform Comput 1994 110 2 366-390

Digital Library

[15]

Kozen D Kleene algebra with tests ACM Trans Program Lang Syst 1997 19 3 427-443

Digital Library

[16]

Lipton RJ Reduction: a method of proving properties of parallel programs Commun ACM 1975 18 12 717-721

Digital Library

[17]

Lamport L and Schneider FB Pretending atomicity 1989 Ithaca, NY, USA Technical report

Digital Library

[18]

Möller B (2004) Lazy Kleene algebra. In: Mathematics of program construction. Lecture notes in computer science, vol 3125, pp 252–273. Springer, Berlin

[19]

McIver AK, Cohen E, Morgan CC (2006) Using probabilistic Kleene algebra for protocol verification. In: Relations and Kleene algebra in computer science. Lecture notes in computer science, vol 4136, pp 296–310

[20]

Meinicke LA (2008) Transformation rules for probabilistic programs: an algebraic approach. PhD thesis, The University of Queensland, June 2008

[21]

Meinicke LA, Hayes IJ (2006) Reasoning algebraically about probabilistic loops. In: Eighth internatinal conference on formal engineering methods. Lecture notes in computer science, vol 4260.

[22]

Meinicke L and Hayes IJ Audebaud P and Paulin-Mohring C Probabilistic choice in refinement algebra Mathematics of program construction. Lecture notes in computer science, vol 5133 2008 Berlin Springer 243-267

[23]

Meinicke LA and Hayes IJ Algebraic reasoning for probabilistic action systems and while-loops Acta Inform 2008 45 5 321-382

Digital Library

[24]

Morgan C, McIver A (2001) Cost analysis of games, using program logic. In: APSEC ’01: proceedings of the eighth Asia-Pacific on software engineering conference, p 351. IEEE Computer Society, Washington

[25]

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

[26]

McIver A and Morgan C Abstraction, refinement and proof for probabilistic systems. Monographs in Computer Science 2005 Berlin Springer

Digital Library

[27]

Morgan C, McIver A, and Seidel K Probabilistic predicate transformers ACM Trans Program Lang Syst 1996 18 3 325-353

Digital Library

[28]

Meinicke L and Solin K Berghammer R, Möller B, and Struth G Reactive probabilistic programs and refinement algebra Relations and Kleene algebra in computer science. Lecture notes in computer science, vol 4988 2008 Berlin Springer 304-319

[29]

McIver A and Weber T Sutcliffe G and Voronkov A Towards automated proof support for probabilistic distributed systems Logic for programming, artificial intelligence, and reasoning, 12th international conference. Lecture notes in computer science, vol 3835 2005 Berlin Springer 534-548

[30]

Patron MC, Kozen D (2000) Certification of compiler optimizations using Kleene algebra with tests. In: Lloyd J, Dahl V, Furbach U, Kerber M, Lau K, Palamidessi C, Moniz Pereira L, Sagiv Y, Stuckey PJ (eds) Proceedings of the 1st international conference in computational logic. Lecture notes in artificial intelligence, vol 186, pp 568–582. Springer, Berlin

[31]

Solin K (2006) On two dually nondeterministic refinement algebras. In: Relations and Kleene algebra in computer science. Lecture notes in computer science, vol 4136, pp 373–387

[32]

Sere K, Troubitsyna E (1996) Probabilities in action systems. In: Proceedings of the 8th Nordic workshop on programming theory. Publishing Association, Helsinki

[33]

Solin K, von Wright J (2006) Refinement algebra with operators for enabledness and termination. In: Mathematics of program construction. Lecture notes in computer science, vol 4014, pp 397–415. Springer, Berlin (revised version to appear in Science of Computer Programming)

[34]

Takai T, Furusawa H (2006) Monodic tree Kleene algebra. In: Relations and Kleene algebra in computer science. Lecture notes in computer science, vol 4136, pp 402–416

[35]

von Wright J (2002) From Kleene algebra to refinement algebra. In: Mathematics of program construction. Lecture notes in computer science, vol 2386, pp 233–262. Springer, Berlin

[36]

von Wright J Towards a refinement algebra Sci Comput Program 2004 51 23-45

Digital Library

Cited By

Tarasyuk ATroubitsyna ELaibinis L(2015)Integrating stochastic reasoning into Event-B developmentFormal Aspects of Computing10.1007/s00165-014-0305-z27:1(53-77)Online publication date: 1-Jan-2015
https://dl.acm.org/doi/10.1007/s00165-014-0305-z
Solin K(2015)Encoding and Decoding in Refinement AlgebraRelational and Algebraic Methods in Computer Science10.1007/978-3-319-24704-5_13(209-224)Online publication date: 8-Nov-2015
https://doi.org/10.1007/978-3-319-24704-5_13
Preoteasa V(2014)Refinement algebra with dual operatorScience of Computer Programming10.1016/j.scico.2013.07.00292(179-210)Online publication date: Oct-2014
https://doi.org/10.1016/j.scico.2013.07.002
Show More Cited By

Index Terms

Refinement algebra for probabilistic programs

Index terms have been assigned to the content through auto-classification.

Recommendations

Refinement Algebra for Probabilistic Programs

We propose an abstract refinement algebra for reasoning about probabilistic programs in a total-correctness setting. The algebra is equipped with operators that determine whether a program is enabled, has certain failure or does not have certain failure,...
Refinement Algebra with Explicit Probabilism
TASE '09: Proceedings of the 2009 Third IEEE International Symposium on Theoretical Aspects of Software Engineering

Refinement algebra provides axioms for the stepwise removal of abstraction, in the form of demonic nondeterminism, in a first-order system that supports reasoning about loops. It has been extended by Solin and Meinecke to computations involving implicit ...
Enabledness and termination in refinement algebra

Refinement algebras are abstract algebras for reasoning about programs in a total correctness framework. We extend a reduct of von Wright's demonic refinement algebra with two operators for modelling enabledness and termination of programs. We show how ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image Formal Aspects of Computing

Formal Aspects of Computing Volume 22, Issue 1

Jan 2010

78 pages

ISSN:0934-5043

EISSN:1433-299X

Issue’s Table of Contents

© British Computer Society 2009.

Publisher

Springer-Verlag

Berlin, Heidelberg

Publication History

Published: 01 January 2010

Accepted: 20 December 2008

Received: 09 January 2008

Published in FAC Volume 22, Issue 1

Author Tags

Qualifiers

Research-article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

6
Total Citations
View Citations
58
Total Downloads

Downloads (Last 12 months)51
Downloads (Last 6 weeks)6

Reflects downloads up to 19 Dec 2024

Other Metrics

View Author Metrics

Citations

Cited By

Tarasyuk ATroubitsyna ELaibinis L(2015)Integrating stochastic reasoning into Event-B developmentFormal Aspects of Computing10.1007/s00165-014-0305-z27:1(53-77)Online publication date: 1-Jan-2015
https://dl.acm.org/doi/10.1007/s00165-014-0305-z
Solin K(2015)Encoding and Decoding in Refinement AlgebraRelational and Algebraic Methods in Computer Science10.1007/978-3-319-24704-5_13(209-224)Online publication date: 8-Nov-2015
https://doi.org/10.1007/978-3-319-24704-5_13
Preoteasa V(2014)Refinement algebra with dual operatorScience of Computer Programming10.1016/j.scico.2013.07.00292(179-210)Online publication date: Oct-2014
https://doi.org/10.1016/j.scico.2013.07.002
Gibbons J(2013)Unifying Theories of Programming with MonadsUnifying Theories of Programming10.1007/978-3-642-35705-3_2(23-67)Online publication date: 2013
https://doi.org/10.1007/978-3-642-35705-3_2
Solin K(2011)Normal forms in total correctness for while programs and action systemsThe Journal of Logic and Algebraic Programming10.1016/j.jlap.2011.04.00880:6(362-375)Online publication date: Aug-2011
https://doi.org/10.1016/j.jlap.2011.04.008
Preoteasa V(2011)Algebra of monotonic boolean transformersProceedings of the 14th Brazilian conference on Formal Methods: foundations and Applications10.1007/978-3-642-25032-3_10(140-155)Online publication date: 26-Sep-2011
https://dl.acm.org/doi/10.1007/978-3-642-25032-3_10

View Options

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Article

Media

Figures

Other

Tables

View Issue’s Table of Contents