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.

翻译：我们解决了关于PCTL及其松弛语义的近似互模拟可靠性的问题。为此，我们借鉴Desharnais、Laviolette和Tracol提出的互模拟概念，引入一种参数化依赖于近似误差δ和轨迹观测深度n的互模拟关系。本质上，我们的可靠性定理表明：当状态q在误差δ和步数n内满足给定公式，且q与q'在误差δ'和足够步数内互模拟时，可证明q'在适当误差δ"和步数n内也满足该公式。新误差δ"由δ、δ'及公式共同计算得出，且仅与n呈线性关系。我们详细阐述了该可靠性证明的全过程。将互模拟概念扩展至状态族，进而获得此类状态族上的渐近等价关系。随后考虑PCTL公式的渐近满足关系，并证明渐近等价的状态族渐近满足相同的公式。