The definition of behavioural preorders over process terms as the maximal (pre-)congruences induced by basic observables has proven to be a useful technique to define various preorders and equivalences in the non-probabilistic setting. In this paper, we consider probabilistic observables to define an observational semantics for a probabilistic pro- cess calculus. The resulting pre-congruence is proven to coincide with a probabilistic may preorder, which, in turn, corresponds to a natural probabilistic extension of the may testing preorder of De Nicola and Hennessy.

Basic observables for probabilistic may testing

Massink M
2007

Abstract

The definition of behavioural preorders over process terms as the maximal (pre-)congruences induced by basic observables has proven to be a useful technique to define various preorders and equivalences in the non-probabilistic setting. In this paper, we consider probabilistic observables to define an observational semantics for a probabilistic pro- cess calculus. The resulting pre-congruence is proven to coincide with a probabilistic may preorder, which, in turn, corresponds to a natural probabilistic extension of the may testing preorder of De Nicola and Hennessy.
2007
Istituto di Scienza e Tecnologie dell'Informazione "Alessandro Faedo" - ISTI
978-0-7695-2883-0
D.2.4 Software and Program verification
68Q85 Models and methods for concurrent and distributed computing
Probabilistic Automata
Process Algebra
Probabilistic Testing Theory
File in questo prodotto:
File Dimensione Formato  
prod_91746-doc_3365.pdf

solo utenti autorizzati

Descrizione: QEST2007
Tipologia: Versione Editoriale (PDF)
Dimensione 276.26 kB
Formato Adobe PDF
276.26 kB Adobe PDF   Visualizza/Apri   Richiedi una copia

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/20.500.14243/57639
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 4
  • ???jsp.display-item.citation.isi??? 4
social impact