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\"{u}chi and generalized B\"{u}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).
翻译:自动结构是无限的, 由同步的有限状态自动结构代表。 本文具体涉及固定字和树( 排列/ 未排列) 的自动结构。 我们调查拉姆齐量化器的“ 定向版本 ”, 表示存在无限定向分类 。 将拉姆齐量化器的标准“ 非定向版本” 归为拉姆齐量化器的标准“ 非定向版本 ” 。 首先可以观察到拉姆西量化器和两个核查问题之间的有趣联系:(1) 与B\\\\\{u}chi和通用的B\\\\\{u}}} 定期模式检查中的条件可被视为拉姆西相对于过渡性自动图表( 其边缘关系是过渡性的) 的量化 。 我们为这三起案件( 常规、 过渡性、 双透明性) 的复杂度( ) 提供了Ramsey quanticilable 的复杂面图层, 以及 精确的变现性( ) 变现性、 变现性、 硬性、 硬性、 硬性、 硬性、 硬性、 硬性、 硬性、 硬性、 硬性、 硬性、 硬性、 硬性、 硬性、 和 硬性、 硬性、 硬性、 硬性、 硬性、 硬性、 硬性、 硬性、 硬性、 和 变的 硬性、 硬性、 硬性、 、 和 变的 硬性、 硬性、 变的 和性、 和性、 硬性、 、 等关系、 变的 变的 、 和 变的 等。