Markovian Process Algebra: Composition and Equivalence

Markovian Process Algebra (MPA) is a process algebra enhanced with exponential timing which allows the mapping of specifications on continuous time Markov chains (CTMCs). This paper introduces a compositional approach to compute the generator matrix of the CTMC underlying a MPA specification which consists of the parallel composition of finite state agents. Furthermore two different equivalence relations covering quantitative and qualitative aspects are introduced. These equivalence relations are shown to be congruences according to parallel composition of agents. 1 Introduction Process algebras enhanced with stochastic and in particular exponential timing have been proposed recently as a good modelling paradigm to combine qualitative and quantitative analysis of complex parallel and concurrent systems. Several approaches to enhance untimed process algebras by exponentially distributed delays appeared in the literature (see [1, 5, 6, 8, 9, 13, 14]). All these approaches start from an ..