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

ing from Prioritized/Weighted Internal Immediate Actions Marco Bernardo and Alessandro Aldini Universit`a di Urbino “Carlo Bo” – Italy 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 GSPNlike 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 bisimilarabstracts from such actions. We show that the proposed equivalence is a congruence and admits a sound and complete axiomatization for the class of well-priori...

• Type: Conference
• Year: 2007
• Where: ICTCS
• Authors: Marco Bernardo, Alessandro Aldini
• Keywords: ICTCS 2007, Immediate Actions, Internal Immediate Actions, Markovian Process Calculi, Theoretical Computer Science