b

This paper proposes a compositional approach to the spec-i cation and analysis of stochastic discrete-event systems. We present a process algebra that allows one to specify generalised semi-Markov processes (GSMPs) in a compo-sitional way. The semantics of this process algebra is given in terms of stochastic automata, an extension of automata with clocks that are basically random variables of continu-ous or discrete nature. We show that GSMPs are a proper subset of stochastic automata and provide some example laws that are useful for the verication of such models