参数马尔可夫链中状态价值函数的分析

本研究针对参数马尔可夫链（pMC）在可达性属性验证中的复杂性问题，提出了一种新的方法来简化单调性检查。通过将单调性归结为状态间可达性概率的比较，提出的算法在不同基准测试中表现出减少模型大小和加速现有算法的潜力，具有重要的实际应用价值。