Stochastic processes as concurrent constraint programs

This paper describes a stochastic concurrent constraint language for the description and programming of concurrent probabilistic systems. The language can be viewed both as a calculus for describing and reasoning about stochastic processes and as an executable language for simulating stochastic processes. In this language programs encode probability distributions over (potentially infinite) sets of objects. We illustrate the subtleties that arise from the interaction of constraints, random choice and recursion. We describe operational semantics of these programs (programs are run by sampling random choices), denotational semantics of programs (based on labeled transition systems and weak probabilistic bisimulation), and prove soundness theorems. We show that Probabilistic cc is conservative over cc, thus justifying the design of Probabilistic cc. We use the semantic study to illustrate a novel use of probability to analyze a problem stated without reference to probability, namely the problem of indeterminacy in synchronous programs.