We tackle the problem of establishing the soundness of approximate bisimilarity with respect to PCTL and its relaxed semantics. To this purpose, we consider a notion of bisimilarity similar to the one introduced by Desharnais, Laviolette, and Tracol, which is parametric with respect to an approximation error δ, and to the depth n of the observation along traces. Essentially, our soundness theorem establishes that, when a state q satisfies a given formula up-to error δ and steps n, and q is bisimilar to q′ up-to error δ′ and enough steps, we prove that q′ also satisfies the formula up-to a suitable error δ′ ′ and steps n. The new error δ′ ′ is computed from δ, δ′ and the formula, and only depends linearly on n. We provide a detailed overview of our soundness proof.

A Sound Up-to- n, δ Bisimilarity for PCTL

Bartoletti M.;
2022-01-01

Abstract

We tackle the problem of establishing the soundness of approximate bisimilarity with respect to PCTL and its relaxed semantics. To this purpose, we consider a notion of bisimilarity similar to the one introduced by Desharnais, Laviolette, and Tracol, which is parametric with respect to an approximation error δ, and to the depth n of the observation along traces. Essentially, our soundness theorem establishes that, when a state q satisfies a given formula up-to error δ and steps n, and q is bisimilar to q′ up-to error δ′ and enough steps, we prove that q′ also satisfies the formula up-to a suitable error δ′ ′ and steps n. The new error δ′ ′ is computed from δ, δ′ and the formula, and only depends linearly on n. We provide a detailed overview of our soundness proof.
2022
978-3-031-08145-3
978-3-031-08143-9
Approximate bisimulation
PCTL
Probabilistic processes
File in questo prodotto:
File Dimensione Formato  
main.pdf

Solo gestori archivio

Descrizione: Articolo principale
Tipologia: versione pre-print
Dimensione 458.17 kB
Formato Adobe PDF
458.17 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/11584/341472
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 1
  • ???jsp.display-item.citation.isi??? 1
social impact