Weak Markovian Bisimilarity: Abstracting from Prioritized/Weighted Internal Immediate Actions

Markovian process calculi constitute a useful framework for reasoning about the functional and performance aspects of concurrent systems. This is achieved by means of behavioral equivalences that take into account both the action names and their exponentially distributed durations. A notable extension to the expressiveness of Markovian process calculi derives from the adoption of GSPN-like immediate actions, i.e. actions with a zero duration and equipped with a priority level and a weight. Since internal immediate actions are unobservable both from the functional viewpoint and from the performance viewpoint, in this paper we tackle the problem of defining a weak variant of Markovian bisimilarity that abstracts from such actions. We show that the proposed equivalence is a congruence and admits a sound and complete axiomatization for the class of well-prioritized process terms.