  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 $\delta$, 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 $\delta$ and steps $n$, and $q$ is
bisimilar to $q'$ up-to error $\delta'$ and enough steps, we prove that $q'$
also satisfies the formula up-to a suitable error $\delta"$ and steps $n$. The
new error $\delta"$ is computed from $\delta$, $\delta'$ 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.
