Probabilistic branching bisimilarity allows us to compare process behaviour with respect to their branching structure and probabilistic features, while abstracting away from those computation steps that can be marked as irrelevant to the analysis at hand. To the best of our knowledge, in the context of nondeterministic probabilistic processes, no proof of probabilistic branching bisimilarity being an equivalence has been provided so far. Since, as happened in the fully nondeterministic case, some researchers are using such a result by taking it for granted, we decided to dedicate this note to a formal proof of it. More precisely, we extend and adapt the proof strategy used by Basten in the fully nondeterministic case. Thus, we introduce the probabilistic analogue to the notion of semi-branching bisimilarity and to van Glabbeek and Weijland's Stuttering Lemma to prove that probabilistic branching bisimilarity is indeed an equivalence relation.

Raiders of the lost equivalence: Probabilistic branching bisimilarity

Tini S.
2020-01-01

Abstract

Probabilistic branching bisimilarity allows us to compare process behaviour with respect to their branching structure and probabilistic features, while abstracting away from those computation steps that can be marked as irrelevant to the analysis at hand. To the best of our knowledge, in the context of nondeterministic probabilistic processes, no proof of probabilistic branching bisimilarity being an equivalence has been provided so far. Since, as happened in the fully nondeterministic case, some researchers are using such a result by taking it for granted, we decided to dedicate this note to a formal proof of it. More precisely, we extend and adapt the proof strategy used by Basten in the fully nondeterministic case. Thus, we introduce the probabilistic analogue to the notion of semi-branching bisimilarity and to van Glabbeek and Weijland's Stuttering Lemma to prove that probabilistic branching bisimilarity is indeed an equivalence relation.
2020
Equivalence relations; Formal semantics; Nondeterministic probabilistic processes; Probabilistic branching bisimilarity; Semi-branching bisimilarity
Castiglioni, V.; Tini, S.
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: https://hdl.handle.net/11383/2087851
 Attenzione

Attenzione! I dati visualizzati non sono stati sottoposti a validazione da parte dell'ateneo

Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 5
  • ???jsp.display-item.citation.isi??? 4
social impact