Stochastic pi-calculus

We extend the pi-calculus, a model of concurrent processes based on the notion of naming, to cope with performance modelling. The new language is called the stochastic pi-calculus (S pi). We obtain a more expressive language than classical stochastic process algebras because S pi allows one to describe dynamically reconfigurable or mobile networks. The semantics of S pi is given in the classical structural operational approach. In order to effectively compute performance measures, we define a stratified transition system that is finitely branching. We give a transition rule to directly yield a continuous time Markov chain from an S pi specification, with no transition system manipulation.