一句话：研究自动结构上有向 Ramsey 量词的复杂度，建立 NL 至 EXP 图景，并用于验证问题。
自动结构由同步有限自动机有限表示，本文关注有限词与树上的自动结构。研究表达无限有向团的“有向版”Ramsey 量词，其涵盖标准无向版。作者发现其与验证的联系：正则模型检测中 Büchi/广义 Büchi 可达性可视为传递自动图上的 Ramsey 量化；自动关系的 monadic decomposability 可视为余传递自动图上的 Ramsey 量化。论文给出一般、传递、余传递三类情形的完整复杂度图景，均介于 NL 与 EXP 之间，并由此获得子树/平坦前缀重写验证、树自动关系上的 monadic decomposability 等精确复杂度结果，也简化了词自动关系（DFA）上 monadic decomposability 的 NL 复杂度证明。
Automatic structures are infinite structures that are finitely represented by synchronized finite-state automata. This paper concerns specifically automatic structures over finite words and trees (ranked/unranked). We investigate the “directed version” of Ramsey quantifiers, which express the existence of an infinite directed clique. This subsumes the standard “undirected version” of Ramsey quantifiers. Interesting connections between Ramsey quantifiers and two problems in verification are firstly observed: (1) reachability with Büchi and generalized Büchi conditions in regular model checking can be seen as Ramsey quantification over transitive automatic graphs (i.e., whose edge relations are transitive), (2) checking monadic decomposability (a.k.a. recognizability) of automatic relations can be viewed as Ramsey quantification over co-transitive automatic graphs (i.e., the complements of whose edge relations are transitive). We provide a comprehensive complexity landscape of Ramsey quantifiers in these three cases (general, transitive, co-transitive), all between NL and EXP. In turn, this yields a wealth of new results with precise complexity, e.g., verification of subtree/flat prefix rewriting, as well as monadic decomposability over tree-automatic relations. We also obtain substantially simpler proofs, e.g., for NL complexity for monadic decomposability over word-automatic relations (given by DFAs).
DOI 原文 · arXiv · PDF（开放获取） · DBLP
@inproceedings{BergstrasserGLZ22,
title = {Ramsey Quantifiers over Automatic Structures: Complexity and Applications to Verification},
author = {Pascal Bergsträßer and Moses Ganardi and Anthony W. Lin and Georg Zetzsche},
booktitle = {LICS},
year = {2022},
doi = {10.1145/3531130.3533346}
}