Article

Future-Looking Logics on Data Words and Trees

Authors:

Diego Figueira,

Luc SegoufinAuthors Info & Claims

MFCS '09: Proceedings of the 34th International Symposium on Mathematical Foundations of Computer Science 2009

Pages 331 - 343

https://doi.org/10.1007/978-3-642-03816-7_29

Published: 20 August 2009 Publication History

Abstract

In a data word or a data tree each position carries a label from a finite alphabet and a data value from an infinite domain.

Over data words we consider the logic ${\sf LTL}^{\downarrow}_{1}(\rm F)$, that extends LTL( F) with one register for storing data values for later comparisons. We show that satisfiability over data words of ${\sf LTL}^{\downarrow}_{1}(\rm F)$ is already non primitive recursive. We also show that the extension of ${\sf LTL}^{\downarrow}_{1}(\rm F)$ with either the backward modality F ¹ or with one extra register is undecidable. All these lower bounds were already known for ${\sf LTL}^{\downarrow}_{1}({\rm X,F})$ and our results essentially show that the X modality was not necessary.

Moreover we show that over data trees similar lower bounds hold for certain fragments of Xpath.

Cited By

View all

Demri SQuaas K(2021)Concrete domains in logicsACM SIGLOG News10.1145/3477986.34779888:3(6-29)Online publication date: 28-Jul-2021
https://dl.acm.org/doi/10.1145/3477986.3477988
Eberhart CKlin BBouyer P(2019)History-dependent nominal μ-calculusProceedings of the 34th Annual ACM/IEEE Symposium on Logic in Computer Science10.5555/3470152.3470194(1-13)Online publication date: 24-Jun-2019
https://dl.acm.org/doi/10.5555/3470152.3470194
Baelde DLick ASchmitz SSuciu DSkritek SKoch C(2019)Decidable XPath Fragments in the Real WorldProceedings of the 38th ACM SIGMOD-SIGACT-SIGAI Symposium on Principles of Database Systems10.1145/3294052.3319685(285-302)Online publication date: 25-Jun-2019
https://dl.acm.org/doi/10.1145/3294052.3319685
Show More Cited By

Recommendations

Marrying words and trees
PODS '07: Proceedings of the twenty-sixth ACM SIGMOD-SIGACT-SIGART symposium on Principles of database systems

Traditionally, data that has both linear and hierarchical structure, such as annotated linguistic data, is modeled using ordered trees and queried using tree automata. In this paper, we argue that nested words and automata over nested words offer a ...
Isomorphism of regular trees and words

The computational complexity of the isomorphism problem for regular trees, regular linear orders, and regular words is analyzed. A tree is regular if it is isomorphic to the prefix order on a regular language. In case regular languages are represented ...
Marrying Words and Trees
AMAST 2008: Proceedings of the 12th international conference on Algebraic Methodology and Software Technology

We discuss the model of <em>nested words</em>for representation of data with both a linear ordering and a hierarchically nested matching of items. Examples of data with such dual linear-hierarchical structure include annotated linguistic data, ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

MFCS '09: Proceedings of the 34th International Symposium on Mathematical Foundations of Computer Science 2009

August 2009

757 pages

ISBN:9783642038150

Co-chair:
Rastislav Královič
Department of Computer Science, Faculty of Mathematics, Physics and Informatics, Comenius University, Research partially funded by grant APVV 0433-06, Bratislava, Slovakia
,
Editor:
Damian Niwiński
Members of EACSL Jury for the Ackermann Award,

Publisher

Springer-Verlag

Berlin, Heidelberg

Publication History

Published: 20 August 2009

Qualifiers

Article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

14
Total Citations
View Citations
0
Total Downloads

Downloads (Last 12 months)0
Downloads (Last 6 weeks)0

Reflects downloads up to 03 Mar 2025

Other Metrics

View Author Metrics

Citations

Cited By

View all

Demri SQuaas K(2021)Concrete domains in logicsACM SIGLOG News10.1145/3477986.34779888:3(6-29)Online publication date: 28-Jul-2021
https://dl.acm.org/doi/10.1145/3477986.3477988
Eberhart CKlin BBouyer P(2019)History-dependent nominal μ-calculusProceedings of the 34th Annual ACM/IEEE Symposium on Logic in Computer Science10.5555/3470152.3470194(1-13)Online publication date: 24-Jun-2019
https://dl.acm.org/doi/10.5555/3470152.3470194
Baelde DLick ASchmitz SSuciu DSkritek SKoch C(2019)Decidable XPath Fragments in the Real WorldProceedings of the 38th ACM SIGMOD-SIGACT-SIGAI Symposium on Principles of Database Systems10.1145/3294052.3319685(285-302)Online publication date: 25-Jun-2019
https://dl.acm.org/doi/10.1145/3294052.3319685
Lick A(2019)A Hypersequent Calculus with Clusters for Data Logic over OrdinalsAutomated Reasoning with Analytic Tableaux and Related Methods10.1007/978-3-030-29026-9_10(166-184)Online publication date: 3-Sep-2019
https://dl.acm.org/doi/10.1007/978-3-030-29026-9_10
Figueira D(2018)Satisfiability of Xpath on data treesACM SIGLOG News10.1145/3212019.32120215:2(4-16)Online publication date: 30-Apr-2018
https://dl.acm.org/doi/10.1145/3212019.3212021
Abriola SFigueira DFigueira S(2017)Logics of Repeating Values on Data Trees and Branching Counter SystemsProceedings of the 20th International Conference on Foundations of Software Science and Computation Structures - Volume 1020310.1007/978-3-662-54458-7_12(196-212)Online publication date: 22-Apr-2017
https://dl.acm.org/doi/10.1007/978-3-662-54458-7_12
Schmitz S(2016)Complexity Hierarchies beyond ElementaryACM Transactions on Computation Theory10.1145/28587848:1(1-36)Online publication date: 3-Feb-2016
https://dl.acm.org/doi/10.1145/2858784
Carapelle CFeng SFernández Gil OQuaas K(2014)Satisfiability for MTL and TPTL over Non-monotonic Data WordsProceedings of the 8th International Conference on Language and Automata Theory and Applications - Volume 837010.1007/978-3-319-04921-2_20(248-259)Online publication date: 10-Mar-2014
https://dl.acm.org/doi/10.1007/978-3-319-04921-2_20
Figueira DHull RFan W(2013)On XPath with transitive axes and data testsProceedings of the 32nd ACM SIGMOD-SIGACT-SIGAI symposium on Principles of database systems10.1145/2463664.2463675(249-260)Online publication date: 22-Jun-2013
https://dl.acm.org/doi/10.1145/2463664.2463675
Demri SFigueira DPraveen M(2013)Reasoning about Data Repetitions with Counter SystemsProceedings of the 2013 28th Annual ACM/IEEE Symposium on Logic in Computer Science10.1109/LICS.2013.8(33-42)Online publication date: 25-Jun-2013
https://dl.acm.org/doi/10.1109/LICS.2013.8
Show More Cited By

Abstract

Cited By

Recommendations

Marrying words and trees

Isomorphism of regular trees and words

Marrying Words and Trees

Comments

Information

Published In

Publisher

Publication History

Qualifiers

Contributors

Other Metrics

Bibliometrics

Article Metrics

Other Metrics

Citations

Cited By

View options

Share

Share this Publication link

Share on social media

Affiliations