An Algebraic Approach to the Specification of Stochastic Systems (Extended Abstract)
Pedro R. D’Argenio, Joost-Pieter Katoen, Ed Brinksma · 1998
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 introduce and discuss in depth a stochastic process algebra (named ♤) adequate to specify and analyse those systems. In order to give semantics to ♤, we also introduce 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.