PCTL的声音近似和渐近概率双模拟
摘要：关于PCTL和其宽松语义的近似细致相似性的准确性的问题，我们进行了研究。为此，我们考虑了一个灵感来自Desharnais，Laviolette，和Tracol引入的相似性概念，并且参数化了近似误差$delta$和深度$n$。基本上，我们的准确性定理证明了当状态$q$满足给定的公式，误差为$delta$和步数为$n$时，且$q$和$q'$近似误差$delta'$并且步数足够多时，我们证明$q'$也以适当的误差$delta"$和步数$n$满足该公式。新的误差$delta"$由$delta$，$delta'$和公式计算得出，并且仅在$n$上线性依赖。我们详细介绍了我们的准确性证明。我们将我们的相似性概念扩展到状态的集合，从而获得了这些集合上的渐近等价性。然后，我们考虑了PCTL公式的渐近满足关系，并证明渐近等价的状态集合渐近满足相同的公式。
作者：Massimo Bartoletti, Maurizio Murgia, Roberto Zunino
论文ID：2111.03117
分类：Logic in Computer Science
分类简称：cs.LO
提交时间：2023-06-22