Extended Markovian Process Algebra

EMPA enhances the expressiveness of classical process algebras by integrating functional and performance descriptions of concurrent systems. This is achieved by offering, besides passive actions (useful for pure nondeterminism), actions whose duration is exponentially distributed as well as immediate actions (useful for performance abstraction), parametrized by priority levels (hence prioritized choices) and weights (hence probabilistic choices). In order to analyze an EMPA term, from its integrated semantic model (a transition system labeled on both action types and action durations) we derive a functional semantic model (a transition system labeled on action types only) and a performance semantic model (a Markov chain). We show that an integrated analysis, i.e. a notion of equivalence on the integrated semantic model, is not only convenient but also necessary to achieve compositionality.