随机奇偶博弈的值迭代
Value Iteration for Stochastic Parity Games
浏览论文内容
中文总结 AI 辅助
针对随机奇偶博弈的定量分析，提出首个值迭代算法，该算法直接基于获胜概率的格理论表征操作，利用相关结构特性，与基于策略迭代的现有算法不同，还证明了算法的正确性和收敛性。
中文摘要 AI 辅助
我们提出了首个用于随机奇偶博弈定量分析的（有界）值迭代算法，随机奇偶博弈是用于概率验证且带有ω正则目标的基本模型。现有算法基于策略迭代，会反复为一方玩家计算最优策略并固定另一方，导致高计算成本。我们的算法直接对获胜概率的格理论表征进行操作，利用奇偶目标下（几乎确定定性）获胜状态的结构特性。我们证明了所提算法的正确性和收敛性。
英文摘要
We present the first (bounded) value iteration algorithm for the quantitative analysis of stochastic parity games, a fundamental model for probabilistic verification with $ω$-regular objectives. Existing algorithms are based on strategy iteration, which repeatedly computes optimal strategies for one player while fixing the other, leading to high computational cost. Our value iteration algorithm instead operates directly on a lattice-theoretic characterization of winning probabilities, exploiting structural properties of (almost-sure qualitative) winning states under parity objectives. We prove correctness and convergence of the proposed algorithm.
