Towards automatic derivation of performance measures from PEPA models

Stochastic process algebras, such as PEPA, provide a novel approach to performance modelling. As well as facilitating a compositional approach, process algebra models focus on a system's behaviour rather than its state space. Classical process algebras are complemented by modal and temporal logics which concisely express possible model behaviours. These logics are widely used during functional analysis to aid in the verication of system behaviour. During performance analysis we seek to evaluate rather than simply verify the behaviour of a system, and for performance models based on continuous time Markov processes, reward structures are commonly used for this purpose. In this paper we describe a combination of these techniques|the PEPA reward language and its use to derive performance measures from PEPA models. The reward language is based on a modal logic which characterises specic behaviours within the PEPA model and may be used to develop a reward structure over the underlying Markov process. A prototype implementation exists within the PEPA Workbench.