A calculus of probabilistic synchronizing processes and some applications

We propose a probabilistic calculus for parallel processes with explicit synchronization. The calculus is rather different from those already proposed in that it has a peculiar view of parallelism. In fact while on the one hand the calculus was strongly inspired by LOTOS, with which it shares explicit declaration of synchronization actions in the parallel composition operator, thus allowing for multi-party synchronization, on the other hand the semantics we propose is somehow in between Milner s SCCS and ASCCS in that independent actions are performed simultaneously, whereas synchronization is achieved by means of delay. Moreover, delay is controlled in the sense that no process can delay an action if the environment allows that action to be performed. As far as the probabilistic extension is concerned the nondeterministic choice operator of the calculus is replaced by a probabilistic one, in which the probability of behaving like a particular process is given explicitly. The operational semantics we present is based on the notion of probabilistic derivation and is given as a set of axioms and inference rules. Our model shares the main features of both of the generative and stratif1ed ones. Finally, some examples of possible applications of the calculus are shown.