Limiting Until in Ordered Tree Query Languages
Limiting Until in Ordered Tree Query Languages
复制标题
有序树查询语言中的限制直到
DOI：
10.1145/2856104
复制
发表时间：
2016
影响因子：
0.5
通讯作者：
Benedikt M
中科院分区：
文献类型：
--
作者：
Benedikt M
马克思和de Rijke已经证明，w3c XML查询语言XML的导航核心不是一阶完备的;也就是说，它不能通过导航谓词来表达一阶逻辑中可定义的每个查询。如何扩展一阶完全语言？马克思已经证明了条件XPath--带“Until”运算符的XPath扩展--是一阶完备的。完备性论证基本上利用了条件式中向上轴的存在。我们研究是否有可能获得对于有序树上的布尔查询是一阶完全的“仅向前”语言。很容易看出，时序逻辑CTL* 的一个变体是一阶完备的;该变体具有向下、向下和向下路径的路径量词，而沿着路径，人们可以检查线性时序逻辑（LTL）的任意公式。这种语言有两个主要的缺点：它需要在两个水平方向的路径量化（特别是，它需要回头看以前的兄弟节点），它需要考虑公式的LTL的任意复杂的垂直路径。最后一个与马克思的条件XPath形成鲜明对比，后者只需要检查路径上的单个Until运算符。我们研究是否可以消除这些限制中的任何一个。我们的主要结果是负面的。我们表明，如果我们限制我们的CTL* 语言，只有一个水平方向的直到操作符，那么我们失去了完整性。我们还表明，没有限制的“小”子集的LTL沿着垂直路径是足够的一阶完备性。这里的小意味着有界的“直到深度”，这是Etessami和Wilke定义的LTL公式复杂性的度量。特别是，它遵循从我们的工作，只有前向轴的条件树是不表达完整的，这扩展了由Rabinovich和Maoz证明的结果在无限无序树的背景下。
Marx and de Rijke have shown that the navigational core of the w3c XML query language XPath is not first-order complete; that is, it cannot express every query definable in first-order logic over the navigational predicates. How can one extend XPath to get a first-order complete language? Marx has shown that Conditional XPath—an extension of XPath with an “Until” operator—is first-order complete. The completeness argument makes essential use of the presence of upward axes in Conditional XPath. We examine whether it is possible to get “forward-only” languages that are first-order complete for Boolean queries on ordered trees. It is easy to see that a variant of the temporal logic CTL*is first-order complete; the variant has path quantifiers for downward, leftward, and rightward paths, while along a path one can check arbitrary formulas of Linear Temporal Logic (LTL). This language has two major disadvantages: It requires path quantification inbothhorizontal directions (in particular, it requires looking backward at the prior siblings of a node), and it requires the consideration of formulas of LTL of arbitrary complexity on vertical paths. This last is in contrast with Marx’s Conditional XPath, which requires only the checking of a single Until operator on a path. We investigate whether either of these restrictions can be eliminated. Our main results are negative ones. We show that if we restrict our CTL*language by having an Until operator in only one horizontal direction, then we lose completeness. We also show that no restriction to a “small” subset of LTL along vertical paths is sufficient for first-order completeness. Smallness here means of bounded “Until Depth,” a measure of complexity of LTL formulas defined by Etessami and Wilke. In particular, it follows from our work that Conditional XPath with only forward axes is not expressively complete; this extends results proved by Rabinovich and Maoz in the context of infinite unordered trees.
登录
查看更多内容
时态逻辑 Ehrenfeucht-Fraïssé 博弈的直到层次结构和其他应用
影响因子：
1
作者：
K. Etessami;T. Wilke
通讯作者：
T. Wilke
完整的 XML 查询语言必须有多大？
DOI：
--
发表时间：
2009
期刊：
International Conference on Database Theory
影响因子：
--
作者：
Clemens Ley;Michael Benedikt
通讯作者：
Michael Benedikt
第十二届国际数据库理论会议论文集
DOI：
--
发表时间：
2009
期刊：
影响因子：
--
作者：
Ronald Fagin
通讯作者：
Ronald Fagin
使用时态逻辑和自动机推理 XML
DOI：
10.1016/j.jal.2009.09.005
发表时间：
2008
期刊：
2008 Latin American Web Conference
影响因子：
--
作者：
L. Libkin;Cristina Sirangelo
通讯作者：
Cristina Sirangelo
论CTL的表达能力
DOI：
--
发表时间：
1999
期刊：
Proceedings. 14th Symposium on Logic in Computer Science (Cat. No. PR00158)
影响因子：
--
作者：
F. Moller;A. Rabinovich
通讯作者：
A. Rabinovich