Complexity of Two-Variable Logic on Finite Trees
Complexity of Two-Variable Logic on Finite Trees
复制标题
DOI：
10.1145/2996796
复制
发表时间：
2013-07
期刊：
影响因子：
--
通讯作者：
Saguy Benaim;Michael Benedikt;Witold Charatonik;Emanuel Kieronski;R. Lenhardt;Filip Mazowiecki;J. Worrell-J.-Wo
中科院分区：
文献类型：
--
作者：
Saguy Benaim;Michael Benedikt;Witold Charatonik;Emanuel Kieronski;R. Lenhardt;Filip Mazowiecki;J. Worrell-J.-Wo
在一阶逻辑FO 2的双变量片段中表示的属性的验证已经在许多上下文中进行了研究。FO 2在任意结构上的可满足性问题是NEXPTIME-完全的，可满足公式具有指数大小的模型。在单词上，已知FO 2具有与一元时态逻辑相同的表达能力，可满足性再次是NEXPTIME-完全的。在有限标记有序树上，FO 2具有与XML文档的流行查询语言navigational XML相同的表达能力。先前的工作对FO 2和FO 2给出了一个2 EXPTIME界满足FO 2在树上。这项工作包含了一个全面的分析的复杂性FO 2的树木，以及模型的大小和深度。我们表明，需要不同的技术取决于所使用的词汇，无论是排名或排名的树，和编码的标签树。我们还研究了FO 2的自然限制，它的保护版本GF 2。我们的研究结果依赖于FO 2公式的模型中的类型的分析，包括用于控制不同的子树的数量，深度和证人的大小，以满足有限树上的FO 2句子的技术。
Verification of properties expressed in the two-variable fragment of first-order logic FO2 has been investigated in a number of contexts. The satisfiability problem for FO2 over arbitrary structures is known to be NEXPTIME-complete, with satisfiable formulas having exponential-sized models. Over words, where FO2 is known to have the same expressiveness as unary temporal logic, satisfiability is again NEXPTIME-complete. Over finite labelled ordered trees, FO2 has the same expressiveness as navigational XPath, a popular query language for XML documents. Prior work on XPath and FO2 gives a 2EXPTIME bound for satisfiability of FO2 over trees. This work contains a comprehensive analysis of the complexity of FO2 on trees, and on the size and depth of models. We show that different techniques are required depending on the vocabulary used, whether the trees are ranked or unranked, and the encoding of labels on trees. We also look at a natural restriction of FO2, its guarded version, GF2. Our results depend on an analysis of types in models of FO2 formulas, including techniques for controlling the number of distinct subtrees, the depth, and the size of a witness to satisfiability for FO2 sentences over finite trees.