P.R.: General distributions in process algebra. In: Lectures on formal methods and performance analysis: first EEF/Euro summer school on trends in computer science

Abstract. This paper is an informal tutorial on stochastic process alge-bras, i.e., process calculi where action occurrences may be subject to a de-lay that is governed by a (mostly continuous) random variable. Whereas most stochastic process algebras consider delays determined by negative exponential distributions, this tutorial is concerned with the integration of general, non-exponential distributions into a process algebraic setting. We discuss the issue of incorporating such distributions in an interleav-ing semantics, and present some existing solutions to this problem. In particular, we present a process algebra for the specification of stochas-tic discrete-event systems modeled as generalized semi-Markov chains (GSMCs). Using this language stochastic discrete-event systems can be described in an abstract and modular way. The operational semantics of this process algebra is given in terms of stochastic automata, a novel mixture of timed automata and GSMCs. We show that GSMCs are a proper subset of stochastic automata, discuss various notions of equiva-lence, present congruence results, treat equational reasoning, and argue how an expansion law in the process algebra can be obtained. As a case study, we specify the root contention phase within the standardized IEEE 1394 serial bus protocol and study the delay until root contention reso-lution. An overview of related work on general distributions in process algebra and a discussion of trends and future work complete this tutorial.