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.; Murgia, M.; Zunino, R.. - ELETTRONICO. - 13271 LNCS:(2022), pp. 35-52. (Intervento presentato al convegno COORDINATION tenutosi a Lucca nel 13-17, June 2022) [10.1007/978-3-031-08143-9_3].

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

#### 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.
##### Scheda breve Scheda completa Scheda completa (DC)
2022
Coordination Models and Languages
Springer Nature Switzerland
Springer Cham
978-3-031-08145-3
978-3-031-08143-9
Bartoletti, M.; Murgia, M.; Zunino, R.
A Sound Up-to- n, δ Bisimilarity for PCTL / Bartoletti, M.; Murgia, M.; Zunino, R.. - ELETTRONICO. - 13271 LNCS:(2022), pp. 35-52. (Intervento presentato al convegno COORDINATION tenutosi a Lucca nel 13-17, June 2022) [10.1007/978-3-031-08143-9_3].
File in questo prodotto:
File
paper coordination 2022 - publisher.pdf

Solo gestori archivio

Tipologia: Versione editoriale (Publisher’s layout)
Dimensione 321.78 kB
main.pdf

Open Access dal 15/06/2023

Tipologia: Post-print referato (Refereed author’s manuscript)
Utilizza questo identificativo per citare o creare un link a questo documento: `https://hdl.handle.net/11572/360882`