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 inspired by the one introduced by Desharnais, Laviolette, and Tracol, and parametric with respect to an approximation error S, 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 S and steps n, and q is bisimilar to q' up-to error S' and enough steps, we prove that q' also satisfies the formula up-to a suitable error S'' and steps n. The new error S'' is computed from S, S' and the formula, and only depends linearly on n. We provide a detailed overview of our soundness proof. We extend our bisimilarity notion to families of states, thus obtaining an asymptotic equivalence on such families. We then consider an asymptotic satisfaction relation for PCTL formulae, and prove that asymptotically equivalent families of states asymptotically satisfy the same formulae.

Sound approximate and asymptotic probabilistic bisimulations for PCTL / Bartoletti, Massimo; Murgia, Maurizio; Zunino, Roberto. - In: LOGICAL METHODS IN COMPUTER SCIENCE. - ISSN 1860-5974. - 19:1(2023), pp. 2201-2230. [10.46298/lmcs-19(1:22)2023]

Sound approximate and asymptotic probabilistic bisimulations for PCTL

Maurizio Murgia;Roberto Zunino
2023-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 inspired by the one introduced by Desharnais, Laviolette, and Tracol, and parametric with respect to an approximation error S, 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 S and steps n, and q is bisimilar to q' up-to error S' and enough steps, we prove that q' also satisfies the formula up-to a suitable error S'' and steps n. The new error S'' is computed from S, S' and the formula, and only depends linearly on n. We provide a detailed overview of our soundness proof. We extend our bisimilarity notion to families of states, thus obtaining an asymptotic equivalence on such families. We then consider an asymptotic satisfaction relation for PCTL formulae, and prove that asymptotically equivalent families of states asymptotically satisfy the same formulae.
2023
1
Bartoletti, Massimo; Murgia, Maurizio; Zunino, Roberto
Sound approximate and asymptotic probabilistic bisimulations for PCTL / Bartoletti, Massimo; Murgia, Maurizio; Zunino, Roberto. - In: LOGICAL METHODS IN COMPUTER SCIENCE. - ISSN 1860-5974. - 19:1(2023), pp. 2201-2230. [10.46298/lmcs-19(1:22)2023]
File in questo prodotto:
File Dimensione Formato  
main.pdf

accesso aperto

Tipologia: Versione editoriale (Publisher’s layout)
Licenza: Creative commons
Dimensione 535.15 kB
Formato Adobe PDF
535.15 kB Adobe PDF Visualizza/Apri

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/11572/400504
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 1
  • ???jsp.display-item.citation.isi??? 0
  • OpenAlex ND
social impact