We study the impact that different ways of resolving nondeterminism within probabilistic automata have on the properties of probabilistic behavioral equivalences. Firstly, we provide a uniform definition of structure-preserving and structure-modifying resolutions of nondeterminism, respectively generated by different families of schedulers. Secondly, we exhibit a number of anomalies arising from the excessive power of the various families of schedulers, which affect the discriminating power, the compositionality, and the backward compatibility of probabilistic trace equivalence. Thirdly, we propose to remove those anomalies by enforcing coherency within resolutions of nondeterminism. This ensures that a scheduler cannot select different continuations in equivalent states of an automaton, so that also the states to which they correspond in any resolution of the automaton have equivalent continuations.

Coherent Resolutions of Nondeterminism

Bernardo, Marco
2019

Abstract

We study the impact that different ways of resolving nondeterminism within probabilistic automata have on the properties of probabilistic behavioral equivalences. Firstly, we provide a uniform definition of structure-preserving and structure-modifying resolutions of nondeterminism, respectively generated by different families of schedulers. Secondly, we exhibit a number of anomalies arising from the excessive power of the various families of schedulers, which affect the discriminating power, the compositionality, and the backward compatibility of probabilistic trace equivalence. Thirdly, we propose to remove those anomalies by enforcing coherency within resolutions of nondeterminism. This ensures that a scheduler cannot select different continuations in equivalent states of an automaton, so that also the states to which they correspond in any resolution of the automaton have equivalent continuations.
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/11576/2674710
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 5
  • ???jsp.display-item.citation.isi??? ND
social impact