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

A Markovian bisimulation equivalence has been defined for sequential processes, which is weak in the sense that it reduces certain sequences of exponentially timed internal actions to single exponentially timed internal actions having the same average duration and execution probability as the corresponding sequences. This weak Markovian bisimulation equivalence is a congruence for sequential processes with abstraction and turns out to induce an exact CTMC-level aggregation at steady state for all the processes. Unfortunately, it is not a congruence with respect to parallel composition. In this talk, we show how to extend it to concurrent processes in a way that a reasonable tradeoff among abstraction, compositionality, and exactness is achieved. In particular, by enhancing the abstraction capability when dealing with concurrent computations, it is possible to retrieve the congruence property with respect to parallel composition, with the resulting CTMC-level aggregation being exact at steady state for a certain class of concurrent processes.