A theory of Stochastic systems. Part II: Process algebra

Abstract

This paper introduces (pronounce spades), a stochastic process algebra for discrete-event systems, that extends traditional process algebra with timed actions whose delay is governed by general (a.o. continuous) probability distributions. The operational semantics is defined in terms of stochastic automata, a model that uses clocks—like in timed automata—to symbolically represent randomly timed systems, cf. the accompanying paper [P.R. D’Argenio, J.-P. Katoen, A theory of stochastic systems. Part I: Stochastic automata. Inf. Comput. (2005), to appear]. We show that stochastic automata and are equally expressive, and prove that the operational semantics of a term up to -conversion of clocks, is unique (modulo symbolic bisimulation). (Open) probabilistic and structural bisimulation are proven to be congruences for , and are equipped with an equational theory. The equational theory is shown to be complete for structural bisimulation and allows to derive an expansion law.