Skip to main content
SpringerLink
Log in
SpringerLink
Log in

Quantitative Program Logic and Performance in Probabilistic Distributed Algorithms

  • Conference paper
  • First Online:
Formal Methods for Real-Time and Probabilistic Systems (ARTS 1999)

Part of the book series: Lecture Notes in Computer Science ((LNCS,volume 1601))

  • 327 Accesses

Abstract

In this paper we show how quantitative program logic [14] provides a formal framework in which to promote standard techniques of program analysis to a context where probability and nondeterminism interact, a situation common to probabilistic distributed algorithms. We show that overall performance can be formulated directly in the logic and that it can be derived from local properties of components. We illustrate the methods with an analysis of performance of the probabilistic dining philosophers [10].

The work is supported by the EPSRC.

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

Access this chapter

Log in via an institution
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. M. Ben-Ari, A. Pnueli, and Z. Manna. The temporal logic of branching time. Acta Informatica, 20:207–226, 1983.

    Article  MathSciNet  MATH  Google Scholar 

  2. K. M. Chandy and J. Misra. Parallel Program Design: A Foundation. Addison-Wesley, Reading, Mass., 1988.

    MATH  Google Scholar 

  3. L. de Alfaro. Temporal logics for the specification of performance and reliability. Proceedings of STACS’ 97, LNCS volume 1200, 1997.

    Google Scholar 

  4. E.W. Dijkstra. A Discipline of Programming. Prentice Hall International, Englewood Cliffs, N.J., 1976.

    MATH  Google Scholar 

  5. W. Feller. An Introduction to Probability Theory and its Applications, volume 1. Wiley, second edition, 1971.

    Google Scholar 

  6. H. Hansson and B. Jonsson. A logic for reasoning about time and probability. Formal Aspects of Computing, 6(5):512–535, 1994.

    Article  MATH  Google Scholar 

  7. Jifeng He, K. Seidel, and A. K. McIver. Probabilistic models for the guarded command language. Science of Computer Programming, 28(2,3):171–192, January 1997.

    MathSciNet  MATH  Google Scholar 

  8. D. Kozen. A probabilistic PDL. In Proceedings of the 15th ACM Symposium on Theory of Computing, New York, 1983. ACM.

    Google Scholar 

  9. D. Kozen. Results on the propositional μ-calculus. Theoretical Computer Science, 27:333–354, 1983.

    Article  MathSciNet  MATH  Google Scholar 

  10. D. Lehmann and M. O. Rabin. On the advantages of free choice: a symmetric and fully-distributed solution to the Dining Philosophers Problem. In Proceedings of the 8th Annual ACM Symposium on Principles of Programming Languages, pages 133–138, New York, 1981. ACM

    Google Scholar 

  11. N. Lynch, I. Saias, and R. Segala. Proving time bounds for randomized distributed algorithms. Proceedings of 13th Annual Symposium on Principles of Distributed Algorithms, pages 314–323, 1994.

    Google Scholar 

  12. A.K. McIver. Quantitative program logic and efficiency in probabilistic distributed algorithms. Technical report. See QLE98 at http [18].

    Google Scholar 

  13. A.K. McIver. Reasoning about efficiency within a probabilistic mucalculus. 1998. Submitted to pre-LICS98 workshop on Probabilistic Methods in Verification.

    Google Scholar 

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

    Article  Google Scholar 

  15. Carroll Morgan. The generalised substitution language extended to probabilistic programs. In Proceedings of B’98: the Second International B Conference. See B98 at http [18], number 1397 in LNCS. Springer Verlag, April 1998.

    Google Scholar 

  16. Carroll Morgan and Annabelle McIver. A probabilistic temporal calculus based on expectations. In Lindsay Groves and Steve Reeves, editors, Proc. Formal Methods Pacific’ 97. Springer Verlag Singapore, July 1997. Available at [18].

    Google Scholar 

  17. C.C. Morgan and A.K. McIver. Correctness proof for the randomised dining philosophers. See RDP96 at http [18].

    Google Scholar 

  18. PSG. Probabilistic Systems Group: Collected reports. http://www.comlab.ox.ac.uk/oucl/groups/probs/bibliography.html.

    Google Scholar 

  19. M. Sharir, A. Pnueli, and S. Hart. Verification of probabilistic programs. SIAM Journal on Computing, 13(2):292–314, May 1984.

    Article  MathSciNet  MATH  Google Scholar 

  20. P. Whittle. Probability via expectations. Wiley, second edition, 1980.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Programming Research Group, Oxford University, UK

    Annabelle K. McIver

Authors
  1. Annabelle K. McIver
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Lehrstuhl für Informatik, University of Erlangen-Nürnberg, Martensstr. 3, D-91058, Erlangen, Germany

    Joost-Pieter Katoen

  2. Formal Methods and Tools Group, University of Twente, P.O. Box 217, 7500 AE, Enschede, The Netherlands

    Joost-Pieter Katoen

Rights and permissions

Reprints and permissions

Copyright information

© 1999 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

McIver, A.K. (1999). Quantitative Program Logic and Performance in Probabilistic Distributed Algorithms. In: Katoen, JP. (eds) Formal Methods for Real-Time and Probabilistic Systems. ARTS 1999. Lecture Notes in Computer Science, vol 1601. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-48778-6_2

Download citation

  • DOI: https://doi.org/10.1007/3-540-48778-6_2

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-66010-1

  • Online ISBN: 978-3-540-48778-4

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation