Performance Measure Sensitive Congruences for Markovian Process Algebras

The modeling and analysis experience with process algebras has shown the necessity of extending them with priority, probabilistic internal/external choice, and time while preserving compositionality. The purpose of this paper is to make a further step by introducing a way to express performance measures, in order to allow the modeler to capture the QoS metrics of interest. We show that the standard technique of expressing stationary and transient performance measures as weighted sums of state probabilities and transition frequencies can be imported in the process algebra framework. Technically speaking, if we denote by n the number of performance measures of interest, in this paper we define a family of extended Markovian process algebras with generative master-reactive slaves synchronization mechanism called EMPAgr,n including probabilities, priorities, exponentially distributed durations, and sequences of rewards of length n. Then we show that the Markovian bisimulation equivalence ~MB,n is a congruence for EMPAgr,n which preserves the specified performance measures and we give a sound and complete axiomatization for finite EMPAgr,n terms. Finally, we present a case study conducted with the software tool TwoTowers in which we contrast the average performance of a selection of distributed algorithms for mutual exclusion modeled with EMPAgr,n.