TY - JOUR
T1 - Quantitative program logic and expected time bounds in probabilistic distributed algorithms
AU - McIver, A. K.
PY - 2002/6/7
Y1 - 2002/6/7
N2 - 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).
AB - 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).
UR - http://www.scopus.com/inward/record.url?scp=0037036275&partnerID=8YFLogxK
U2 - 10.1016/S0304-3975(01)00049-4
DO - 10.1016/S0304-3975(01)00049-4
M3 - Article
AN - SCOPUS:0037036275
SN - 0304-3975
VL - 282
SP - 191
EP - 219
JO - Theoretical Computer Science
JF - Theoretical Computer Science
IS - 1
ER -