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

Marco Bernardo
(University of Urbino)

We have recently defined a weak Markovian bisimulation equivalence in an integrated-time setting, which reduces sequences of exponentially timed internal actions to individual 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 considered processes. However, it is not a congruence with respect to parallel composition. In this paper, we show how to generalize the equivalence in a way that a reasonable tradeoff among abstraction, compositionality, and exactness is achieved for concurrent processes. We will see that, by enhancing the abstraction capability in the presence of 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 only for a certain subset of the considered processes.

In Herbert Wiklicky and Mieke Massink: Proceedings 10th Workshop on Quantitative Aspects of Programming Languages and Systems (QAPL 2012), Tallinn, Estonia, 31 March and 1 April 2012, Electronic Proceedings in Theoretical Computer Science 85, pp. 122–136.
Published: 3rd July 2012.

ArXived at: http://dx.doi.org/10.4204/EPTCS.85.9 bibtex PDF
References in reconstructed bibtex, XML and HTML format (approximated).
Comments and questions to: eptcs@eptcs.org
For website issues: webmaster@eptcs.org