A stochastic non-deterministic temporal concurrent constraint calculus

We propose sntcc, a stochastic extension of the ntcc calculus, a model of temporal concurrent constraint programming with the capability of modeling asynchronous and non-deterministic timed behavior. We argue that such an extension is needed to faithfully model concurrent systems in real-life situations. We provide a suitable temporal logic and proof system for sntcc and illustrate how to use them for proving properties of stochastic systems. We argue that this modeling strategy of using explicit stochastic constructs within the calculus provides a "runnable specification" for a wide variety of stochastic systems that eases the task of formally reasoning about them. We give examples of specifications in sntcc and use the extended linear temporal logic for proving properties about them.