arXiv:2504.17020cs.LOcs.AI2025-04

通过状态值函数分析,高效压缩参数马尔可夫链的等价类。

Analyzing Value Functions of States in Parametric Markov Chains

  • 将单调性问题转化为状态可达概率的比较
  • 实测在部分基准上减少超70%状态数
  • 可作为单调性验证的快速预处理步骤

参数马尔可夫链(pMC)用于建模概率系统中未知或部分已知的概率。尽管可达性属性的通用验证属于 coETR 完全问题,已有研究尝试通过更易验证的性质(如参数单调性)逼近解法。本文将单调性归约为:给定两个状态,其可达概率是否始终满足前者不低于后者。近期相关成果表明,该问题存在高效算法,可用于合并相同值等价类,从而保持验证结果与单调性不变。我们实现了该算法以压缩 pMC 中“平凡”等价类,实验表明:第一,在部分现有基准上实现状态数显著缩减,某些自定义基准减少超过70%;第二,该压缩显著加速了现有单调性与参数提升算法,可作为实际应用中的快速预处理步骤。

原文摘要 · Abstract (English)

Parametric Markov chains (pMC) are used to model probabilistic systems with unknown or partially known probabilities. Although (universal) pMC verification for reachability properties is known to be coETR-complete, there have been efforts to approach it using potentially easier-to-check properties such as asking whether the pMC is monotonic in certain parameters. In this paper, we first reduce monotonicity to asking whether the reachability probability from a given state is never less than that of another given state. Recent results for the latter property imply an efficient algorithm to collapse same-value equivalence classes, which in turn preserves verification results and monotonicity. We implement our algorithm to collapse "trivial" equivalence classes in the pMC and show empirical evidence for the following: First, the collapse gives reductions in size for some existing benchmarks and significant reductions on some custom benchmarks; Second, the collapse speeds up existing algorithms to check monotonicity and parameter lifting, and hence can be used as a fast pre-processing step in practice.

马尔可夫链参数化算法优化形式验证

Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品;中文卡片由大模型生成,请以原文为准。