An Algebraic Approach to the Specification of Stochastic

We introduce a framework to study stochastic systems, i.e. systems in which the time of occurrence of activities is a general random variable. We intro-duce and discuss in depth a stochastic process algebra (named) adequate to specify and analyse those systems. In order to give semantics to, we also in-troduce a model that is an extension of traditional automata with clocks which are basically random variables: the stochastic automata model. We show that this model and are equally expressive. Although stochastic automata are adequate to analyse systems since they are finite objects, they are still too coarse to serve as concrete semantic objects. Therefore, we introduce a type of probabilistic transition system that can deal with arbitrary probability spaces. In addition, we give a finite axiomatisation for that is sound for the several semantic notions we deal with, and complete for the finest of them. Moreover, an expansion law is straightforwardly derived