paperbot · PL 论文追踪

全部论文 待读 收藏

P2 Succinct progress measures for solving parity games

求解奇偶博弈的简洁进度测度
LICS 2017 32nd Annual ACM/IEEE Symposium on Logic in Computer Science (LICS)2017匹配度 2/10 · 该论文研究奇偶博弈的准多项式时间求解算法,属于逻辑、自动机与形式化验证的基础理论,与用户核心方向(面向 ML/Agentic 程序的静态分析、LLM 改进静态分析/形式化验证、浮点程序分析、贝叶斯程序分析)没有直接交集。仅与形式化验证的理论基础有较弱关联,且不涉及 LLM/Agent 或工程落地。引用 104 inbox
Marcin Jurdziński, Ranko Lazić
crossref: 2026-09-12dblp: 2026-09-12arxiv: 2026-09-12

AI 速览

一句话:提出基于进度测度的准多项式时间奇偶博弈求解算法,将空间需求从准多项式降至近线性。

奇偶博弈求解长期是逻辑与验证中的核心问题,此前最优算法仅为温和次指数;Calude 等人的突破首次给出准多项式时间算法,但空间开销为准多项式。本文提出一种基于进度测度(progress measures)的替代准多项式时间算法,其核心是一个新的有序树编码概念,以及用有界自适应多计数器证明的简洁树编码结果。新算法在保持准多项式时间的同时,将所需空间从准多项式降到近线性。两个树编码工具本身也具有独立意义。评估主要通过理论算法分析与复杂度证明,而非实验。

问题
奇偶博弈求解此前最优算法仅为温和次指数,而首个准多项式时间算法需要准多项式空间。
方法
提出基于 progress measures 的准多项式时间算法,并引入有序树编码与用有界自适应多计数器证明的简洁树编码结果。
评估
通过理论复杂度分析证明算法保持准多项式时间,并将空间需求降至近线性。
原文摘要(Abstract)

The recent breakthrough paper by Calude et al. has given the first algorithm for solving parity games in quasi-polynomial time, where previously the best algorithms were mildly subexponential. We devise an alternative quasi-polynomial time algorithm based on progress measures, which allows us to reduce the space required from quasi-polynomial to nearly linear. Our key technical tools are a novel concept of ordered tree coding, and a succinct tree coding result that we prove using bounded adaptive multi-counters, both of which are interesting in their own right.

链接与引用

DOI 原文 · arXiv · PDF(开放获取) · DBLP

BibTeX
@inproceedings{JurdzinskiL17,
  title = {Succinct progress measures for solving parity games},
  author = {Marcin Jurdziński and Ranko Lazić},
  booktitle = {LICS},
  year = {2017},
  doi = {10.1109/lics.2017.8005092}
}