On Regular Paths with Counting and Data Tests

详细信息    查看全文

• 作者：Everardo Bá ; rcenas ^{iebarcenaspa@conacyt.mx}
• 关键词：Modal Logics ; XPath ; Automated Reasoning ; Data Trees ; Counting
• 刊名：Electronic Notes in Theoretical Computer Science
• 出版年：2016
• 出版时间：8 December 2016
• 年：2016
• 卷：328
• 期：Complete
• 页码：3-16
• 全文大小：256 K
• 卷排序：328

文摘

Regular path expressions represent the navigation core of the XPath query language for semi-structured data (XML), and it has been characterized as the First Order Logic with Two Variables (FO2). Data tests refers to (dis)equality comparisons on data tree models, which are unranked trees with two kinds of labels, propositions from a finite alphabet, and data values from a possibly infinite alphabet. Node occurrences on tree models can be constrained by counting/arithmetic constructors. In this paper, we identify an EXPTIME extension of regular paths with data tests and counting operators. This extension is characterized in terms of a closed under negation Presburger tree logic. As a consequence, the EXPTIME bound also applies for standard query reasoning (emptiness, containment and equivalence).