Stochastic process algebras meet Eden

Abstract

Process algebras represent an appropriate mechanism to formally specify concurrent systems. In order to get a thorough knowledge of these systems, some external formalism must be used. In this paper we propose an integrated framework where a (non-trivial) process algebra is combined with a (concurrent) functional language. Specifically, we consider a stochastic process algebra featuring value passing where distributions are not restricted to be exponential. In order to study properties of these specifications, we translate them into functional programs written in Eden. This functional language is very suitable for concurrent programming. On the one hand, it presents the usual features of modern functional languages. On the other hand, it allows the execution of concurrent processes. We present an example showing how specifications can be translated into Eden and how quantitative properties can be studied.