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.