论文标题
自动结构上的拉姆西量词：复杂性和验证的应用
Ramsey Quantifiers over Automatic Structures: Complexity and Applications to Verification
论文作者
论文摘要
自动结构是无限结构，由同步有限状态自动机有限地表示。本文涉及有限单词和树（排名/不合格）的自动结构。我们研究了Ramsey量化器的“定向版本”，该量词表达了无限的定向集团的存在。这包含Ramsey量词的标准“无向版本”。首先观察到拉姆西量化词与验证中的两个问题之间的有趣联系：（1）在常规模型检查中使用Büchi和广义的Büchi条件的可及性可以看作是对传递自动图上的Ramsey定量（即，其边缘关系是传递性的），（2）（2）（2）量化的量化性关系（A.K.A. A.K.A. A.K.A. A.K.A. A.K.A. A.K.A. A.K.A. A.K.A. A.K.A. A.K.A. A.K.A. A.K.A.图（即，其边缘关系是传递的补充）。在这三种情况下，我们在NL和EXP之间提供了Ramsey量化器的全面复杂性格局（一般，及物，共转移）。反过来，这会以精确的复杂性（例如，验证子树/平面前缀重写）以及对树自动关系的可分解性。我们还获得了基本简单的证明，例如，对于单词自动关系（由DFAS给出），用于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).
