广义Büchi博弈的条件最优算法

图上的博弈为研究计算机科学中的若干核心问题（如反应式系统的验证与综合）提供了合适的框架。图上博弈最基本的目标之一是活性（或Büchi）目标，给定一个目标顶点集，要求该集合中的某个顶点被无限次访问。我们研究了广义Büchi目标（即活性目标的合取），以及两个广义Büchi目标之间的蕴含（被称为GR(1)目标），它们在计算机辅助验证的众多应用中产生。我们提出了改进的算法，并基于关于（A1）组合布尔矩阵乘法和（A2）CNF-SAT复杂度的广泛接受的假设，给出了条件超线性下界。我们考虑具有 $n$ 个顶点、$m$ 条边和带有 $k$ 个合取的广义Büchi目标的图博弈。首先，我们提出了一个运行时间为 $O(k \cdot n^2)$ 的算法，改进了先前已知的 $O(k \cdot n \cdot m)$ 和 $O(k^2 \cdot n^2)$ 最坏情况界限。在假设（A1）下，我们的算法对于稠密图是最优的。其次，我们证明了在假设（A2）下，当目标集大小为常数时，该问题的基本算法对于稀疏图是最优的。最后，我们考虑了GR(1)目标，其前件中有 $k_1$ 个合取，后件中有 $k_2$ 个合取，并提出了一个 $O(k_1 \cdot k_2 \cdot n^{2.5})$ 时间的算法，对于 $m > n^{1.5}$ 改进了先前已知的 $O(k_1 \cdot k_2 \cdot n \cdot m)$ 时间算法。