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.

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

Bernardo, Marco;Aldini, Alessandro
2007

Abstract

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.
File in questo prodotto:
Non ci sono file associati a questo prodotto.

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: http://hdl.handle.net/11576/1892539
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus ND
  • ???jsp.display-item.citation.isi??? ND
social impact