Concurrent Probabilistic Programs, or: How to Schedule if You Must

Sergiu Hart and Micha Sharir



(Acrobat PDF file)



Abstract

Consider a finite set of processes, such that each one may use randomizations in its course of execution; these processes are running concurrently, under a fair interleaving schedule. We analyze the worst-case probability of termination, i.e., program convergence to a specified set of goal states. Several methods for computing this probability are presented, and characterizations of the special case where it is identically 1 are derived. Specializations of these characterizations to the case of deterministic and nondeterministic programs, and to the case of programs with finite state spaces, are also discussed.

Key words. concurrent probabilistic program, scheduler, fairness, program termination, Markov chains




Related papers on probabilistic programs by S. Hart, A. Pnueli and M. Sharir: