PCTL 的可靠近似与渐近概率互模拟
计算机科学中的逻辑
2023-06-22 v7
摘要
我们解决了建立关于 PCTL 及其松弛语义的近似互模拟可靠性的问题。为此，我们考虑了一种受 Desharnais、Laviolette 和 Tracol 提出的概念启发的互模拟概念，该概念参数化于近似误差 以及沿轨迹的观测深度 。本质上，我们的可靠性定理确立了：当状态 在误差 和步数 下满足给定公式，且 与 在误差 和足够步数下互模拟时，我们证明 也在合适的误差 和步数 下满足该公式。新的误差 由 、 和该公式计算得出，且仅线性依赖于 。我们提供了可靠性证明的详细概述。我们将互模拟概念扩展到状态族，从而获得了此类状态族上的渐近等价性。然后，我们考虑了 PCTL 公式的渐近满足关系，并证明了渐近等价的状态族渐近地满足相同的公式。
引用
@article{arxiv.2111.03117,
title = {Sound approximate and asymptotic probabilistic bisimulations for PCTL},
author = {Massimo Bartoletti and Maurizio Murgia and Roberto Zunino},
journal= {arXiv preprint arXiv:2111.03117},
year = {2023}
}