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.
An Algebra-Based Method to Associate Rewards with EMPA Terms
Bernardo, Marco
1997
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.I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
