图与 MDP 中 Streett 目标的近线性时间算法

基本的模型检测问题以模型和规约为输入，要求算法验证模型是否满足规约。反应式系统的两个经典模型是图和马尔可夫决策过程（MDPs）。反应式系统验证中一种基本的规约形式是强公平（又称 Streett）目标，其中给定不同类型的请求和相应的授权，要求是：对每一类型，若请求事件无限频繁地发生，则相应的授权事件也必须无限频繁地发生。所有 omega-正则目标都可表达为 Streett 目标，因此它们在验证中具有典型性。考虑具有 n 个顶点、m 条边以及带 k 对元素的 Streett 目标的图/MDP，令 b 表示请求与授权集合的 Streett 目标描述的大小。当前已知最好的算法所需时间为 $O(min(n^2, m \sqrt{m \log n}) + b \log n)$。本文中，我们给出随机化的近线性时间算法，其期望运行时间为 $\widetilde{O}(m + b)$，其中 $\widetilde{O}$ 记号隐藏了多对数因子。我们的随机化算法在输入规模上是近线性的，因此直至多对数因子均为最优。