一句话：提出更快的符号算法计算 MDP 的最大端分量分解，给出符号操作与空间权衡，解决长期开放问题。
论文研究概率验证的核心问题：计算马尔可夫决策过程（MDP）的最大端分量（MEC）分解，它推广了图的强连通分量分解与马尔可夫链的闭回归集。在限制为集合操作与一步邻域计算等符号操作的模型下，经典算法需 O(n^2) 次符号操作和 O(1) 空间，已知另一算法需 O(n√m) 次操作和 O(√m) 空间，能否突破 O(n^2) 操作为开放问题。作者提出新符号算法，仅需 ~O(n^{1.5}) 次操作与 ~O(√n) 空间，并可参数化权衡：对 0<ε<2，以 ~O(n^{2-ε}) 次操作和 ~O(n^ε) 空间求解。该技术还用于 MDP 上 ω-正则（奇偶）目标的几乎必然获胜区域，将时间-空间乘积从 ~O(n^2 d) 改进至 ~O(n^2)。
We present a faster symbolic algorithm for the following central problem in probabilistic verification: Compute the maximal end-component (MEC) decomposition of Markov decision processes (MDPs). This problem generalizes the SCC decomposition problem of graphs and closed recurrent sets of Markov chains. The model of symbolic algorithms is widely used in formal verification and model-checking, where access to the input model is restricted to only symbolic operations (e.g., basic set operations and computation of one-step neighborhood). For an input MDP with n vertices and m edges, the classical symbolic algorithm from the 1990s for the MEC decomposition requires O(n2) symbolic operations and O(1) symbolic space. The only other symbolic algorithm for the MEC decomposition requires O(n√m ) symbolic operations and O(√m ) symbolic space. The main open question has been whether the worst-case O(n2) bound for symbolic operations can be beaten for MEC decomposition computation. In this work, we answer the open question in the affirmative. We present a symbolic algorithm that requires ~O( n1.5) symbolic operations and ~O( √n ) symbolic space. Moreover, the parametrization of our algorithm provides a trade-off between symbolic operations and esymbolic space: for all 02 - ∈) symbolic operations and ~O( n∈) symbolic space (~O(·) hides poly-logarithmic factors).Using our techniques we also present faster algorithms for computing the almost-sure winning regions of ω-regular objectives for MDPs. We consider the canonical parity objectives for ω-regular objectives, and for parity objectives with d-priorities we present an algorithm that computes the almost-sure winning region with ~O( n2 - ∈) symbolic operations and ~O( n∈) symbolic space, for all 02· d) symbolic operations and O(log n) symbolic space; or (b) O(n√m ·d) symbolic operations and ~O( √m ) symbolic space. Thus we improve the time-space product from ~O( n2·d ) to ~O( n2).
@inproceedings{paperbot6200,
title = {Symbolic Time and Space Tradeoffs for Probabilistic Verification},
author = {Krishnendu Chatterjee and Wolfgang Dvorak and Monika Henzinger and Alexander Svozil},
booktitle = {LICS},
year = {2021},
doi = {10.1109/lics52264.2021.9470739}
}