Revisiting Interactive Markov Chains

AbstractThe usage of process algebras for the performance modeling and evaluation of concurrent systems turned out to be convenient due to their feature of compositionality. A particularly simple and elegant solution in this field is the calculus of Interactive Markov Chains (IMCs), where the behavior of processes is just represented by Continuous Time Markov Chains extended with action transitions representing process interaction. The main advantage of IMCs with respect to other existing approaches is that a notion of bisimulation which abstracts from τ-transitions (“complete” interactions) can be defined which is a congruence. However in the original definition of the calculus of IMCs the high potentiality of compositionally minimizing the system state space given by the usage of a “weak” notion of equivalence and the elegance of the approach is somehow limited by the fact that the equivalence adopted over action transitions is a finer variant of Milner's observational congruence that distinguishes τ-divergent “Zeno” processes from non-divergent ones. In this paper we show that it is possible to reformulate the calculus of IMCs in such a way that we can just rely on simple standard observational congruence. Moreover we show that the new calculus is the first Markovian process algebra allowing for a new notion of Markovian bisimulation equivalence which is coarser than the standard one