Quantitative Program Logic and Performance in Probabilistic Distributed Algorithms
In this paper we show how quantitative program logic  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 .
KeywordsProgram Logic Temporal Logic Probabilistic Choice Computation Tree Atomic Step
Unable to display preview. Download preview PDF.
- L. de Alfaro. Temporal logics for the specification of performance and reliability. Proceedings of STACS’ 97, LNCS volume 1200, 1997.Google Scholar
- W. Feller. An Introduction to Probability Theory and its Applications, volume 1. Wiley, second edition, 1971.Google Scholar
- D. Kozen. A probabilistic PDL. In Proceedings of the 15th ACM Symposium on Theory of Computing, New York, 1983. ACM.Google Scholar
- 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. ACMGoogle Scholar
- 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
- A.K. McIver. Quantitative program logic and efficiency in probabilistic distributed algorithms. Technical report. See QLE98 at http .Google Scholar
- A.K. McIver. Reasoning about efficiency within a probabilistic mucalculus. 1998. Submitted to pre-LICS98 workshop on Probabilistic Methods in Verification.Google Scholar
- Carroll Morgan. The generalised substitution language extended to probabilistic programs. In Proceedings of B’98: the Second International B Conference. See B98 at http , number 1397 in LNCS. Springer Verlag, April 1998.Google Scholar
- 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 .Google Scholar
- C.C. Morgan and A.K. McIver. Correctness proof for the randomised dining philosophers. See RDP96 at http .Google Scholar
- PSG. Probabilistic Systems Group: Collected reports. http://www.comlab.ox.ac.uk/oucl/groups/probs/bibliography.html. Google Scholar
- P. Whittle. Probability via expectations. Wiley, second edition, 1980.Google Scholar