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

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.