An algebra-based method to associate rewards with EMPA terms

Abstract

We present a simple method to associate rewards with terms of the stochastic process algebra EMPA in order to make the specification and the computation of performance measures easier. The basic idea behind this method is to specify rewards within actions of EMPA terms, so it substantially differs from methods based on modal logic. The main motivations of this method are its ease of use as well as the possibility of defining a notion of equivalence which relates terms having the same reward, thus allowing for simplification without altering the performance index. We prove that such an equivalence is a congruence finer than the strong extended Markovian bisimulation equivalence, and we present its axiomatization.