Weak Markovian bisimulation congruences and exact CTMC-level aggregations for concurrent processes

Abstract. The Markovian behavioral equivalences defined so far treat exponentially timed internal actions like any other action. Since an expo-nentially timed internal action has a nonzero duration, it can be observed whenever it is executed between a pair of exponentially timed noninter-nal actions. However, no difference may be noted at steady state between a sequence of exponentially timed internal actions and a single exponen-tially timed internal action as long as their average durations coincide. We show that Milner’s construction to derive a weak bisimulation con-gruence for nondeterministic processes can be extended to sequential Markovian processes in a way that captures the above situation. The resulting weak Markovian bisimulation congruence admits a sound and complete axiomatization, induces an exact CTMC-level aggregation at steady state, and is decidable in polynomial time for finite-state processes having no cycles of exponentially timed internal actions.