Quantitative program logic and expected time bounds in probabilistic distributed algorithms

A. K. McIver*

*Corresponding author for this work

Research output: Contribution to journalArticle

3 Citations (Scopus)

Abstract

In this paper we show how quantitative program logic (Morgan et al., ACM Trans. Programming Languages Systems 18 (1996) 325) 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 expected time 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 expected running time of the probabilistic dining philosophers (Lehmann and Ravin, Proc 8th Annu. ACM. Symp. on principles of Programming Languages, ACM, New York, 1981, p. 133).

Original languageEnglish
Pages (from-to)191-219
Number of pages29
JournalTheoretical Computer Science
Volume282
Issue number1
DOIs
Publication statusPublished - 7 Jun 2002
Externally publishedYes

Fingerprint Dive into the research topics of 'Quantitative program logic and expected time bounds in probabilistic distributed algorithms'. Together they form a unique fingerprint.

  • Cite this