一句话：提出参数化近似概率互模拟，证明其对 PCTL 松弛语义可靠，并扩展为状态族的渐近等价。
论文研究近似概率互模拟相对于 PCTL 及其松弛语义的可靠性问题。作者受 Desharnais 等人工作启发，定义一种由近似误差 δ 和迹上观察深度 n 参数化的互模拟；若状态 q 在误差 δ 与 n 步内满足公式，且 q 与 q' 在误差 δ' 与足够步数下互模拟，则证明 q' 也以由 δ、δ' 和公式计算出的误差 δ''、相同 n 步内满足该公式，且 δ'' 对 n 仅线性依赖。作者概述可靠性证明，并将概念推广到状态族，得到渐近等价，进而定义 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 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.
@article{paperbot2227,
title = {Sound approximate and asymptotic probabilistic bisimulations for PCTL},
author = {Massimo Bartoletti and Maurizio Murgia and Roberto Zunino},
journal = {Logical Methods in Computer Science},
volume = {Volume 19, Issue 1},
year = {2023},
doi = {10.46298/lmcs-19(1:22)2023}
}