一句话：提出求解 parity 和 Streett 目标获胜集的新算法，15 年来首次改进渐近时间复杂度。
该论文研究图与博弈图中 parity 目标和 Streett 目标获胜集的计算问题；这类问题是计算机辅助验证的核心，用于带强公平条件的封闭系统验证、开放系统验证、接口兼容性检查、规约良构性以及反应式系统合成。作者给出两个更快的获胜集算法：在 n 个顶点的博弈图中，对 parity-3（即 one-pair Streett）目标可在 O(n^{5/2}) 时间内计算获胜集；在普通图中，对 k-pair Streett 目标可在 O(n^2 + nk log n) 时间内计算获胜集。相比原有算法，这两项结果对稠密图更快，也是该问题渐近运行时间 15 年来的首次改进。
The computation of the winning set for parity objectives and for Streett objectives in graphs as well as in game graphs are central problems in computer-aided verification, with application to the verification of closed systems with strong fairness conditions, the verification of open systems, checking interface compatibility, well-formedness of specifications, and the synthesis of reactive systems. We show how to compute the winning set on $n$ vertices for (1) parity-3 (aka one-pair Streett) objectives in game graphs in time $O(n^{5/2})$ and for (2) k-pair Streett objectives in graphs in time $O(n^2 + nk \log n)$. For both problems this gives faster algorithms for dense graphs and represents the first improvement in asymptotic running time in 15 years.
@article{paperbot123,
title = {Improved Algorithms for Parity and Streett objectives},
author = {Krishnendu Chatterjee and Monika Henzinger and Veronika Loitzenbauer},
journal = {Logical Methods in Computer Science},
volume = {Volume 13, Issue 3},
year = {2017},
doi = {10.23638/lmcs-13(3:26)2017}
}