Weak Markovian Bisimulation Congruences and Exact CTMC-Level Aggregations for Sequential Processes

The Markovian behavioral equivalences defined so far treat exponentially timed internal actions like any other action. Since an exponentially timed internal action has a nonzero duration, it can be observed whenever it is executed between a pair of exponentially timed noninternal actions. However, no difference may be noted between a sequence of exponentially timed internal actions and a single exponentially timed internal action as long as their average durations coincide. We show that Milner's construction to derive a weak bisimulation congruence for nondeterministic processes can be extended to sequential Markovian processes in a way that captures the above situation. We then prove that 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.