Since the seminal paper by Bloom, Fokkink and van Glabbeek, the Divide and Congruence technique allows for the derivation of compositional properties of nondeterministic processes from the SOS-based decomposition of their modal properties. In an earlier paper, we extended their technique to deal also with quantitative aspects of process behavior: we proved the (pre)congruence property for strong (bi)simulations on processes with nondeterminism and probability. In this paper we further extend our decomposition method to favor compositional reasoning with respect to probabilistic weak semantics. In detail, we consider probabilistic branching and rooted probabilistic branching bisimilarity, and we propose logical characterizations for them. These are strongly based on the modal operator (epsilon) which combines quantitative information and weak semantics by introducing a sort of probabilistic lookahead on process behavior. Our enhanced method will exploit distribution specifications, an SOS-like framework defining the probabilistic behavior of processes, to decompose this particular form of lookahead. We will show how we can apply the proposed decomposition method to derive congruence formats for the considered equivalences from their logical characterizations. (C) 2019 Elsevier B.V. All rights reserved.

Probabilistic divide & congruence: Branching bisimilarity

Tini S.
2020-01-01

Abstract

Since the seminal paper by Bloom, Fokkink and van Glabbeek, the Divide and Congruence technique allows for the derivation of compositional properties of nondeterministic processes from the SOS-based decomposition of their modal properties. In an earlier paper, we extended their technique to deal also with quantitative aspects of process behavior: we proved the (pre)congruence property for strong (bi)simulations on processes with nondeterminism and probability. In this paper we further extend our decomposition method to favor compositional reasoning with respect to probabilistic weak semantics. In detail, we consider probabilistic branching and rooted probabilistic branching bisimilarity, and we propose logical characterizations for them. These are strongly based on the modal operator (epsilon) which combines quantitative information and weak semantics by introducing a sort of probabilistic lookahead on process behavior. Our enhanced method will exploit distribution specifications, an SOS-like framework defining the probabilistic behavior of processes, to decompose this particular form of lookahead. We will show how we can apply the proposed decomposition method to derive congruence formats for the considered equivalences from their logical characterizations. (C) 2019 Elsevier B.V. All rights reserved.
2020
http://www.journals.elsevier.com/theoretical-computer-science/
Congruence formats; Modal decomposition; Nondeterministic probabilistic transition systems; Probabilistic branching bisimulation; SOS
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/2084530
 Attenzione

L'Ateneo sottopone a validazione solo i file PDF allegati

Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 7
  • ???jsp.display-item.citation.isi??? 6
social impact