arXiv:2504.17020v2 宣布类型: replace-cross 摘要: 参数马尔可夫链(pMC)用于建模具有未知或部分已知概率的概率系统。尽管(通用)pMC可达性质的验证已知是coETR完全的，但仍有人试图通过询问pMC在某些参数下的单调性的方式来接近这一问题。在这篇论文中，我们首先将单调性归约为询问从给定状态到达的概率是否从未小于另一个给定状态的概率。对于后一性质的最近结果暗示了一个高效的算法来压缩同值等价类，而这些等价类的压缩又保留了验证结果和单调性。我们实现了该算法来压缩pMC中的“平凡”等价类，并展示了以下实验证据：首先，压缩在一些现有基准测试中减少了规模，在一些自定义基准测试中实现了显著的规模缩减；其次，压缩加速了检查单调性和参数提升的现有算法，因此可以在实践中用作快速预处理步骤。