Abstract
We describe a set of simple features that are sufficient in order to make the satisfiability problem of logics interpreted on trees Tower-hard. We exhibit these features through an Auxiliary Logic on Trees (ALT), a modal logic that essentially deals with reachability of a fixed node inside a forest and features modalities from sabotage modal logic to reason on submodels. After showing that ALT admits a Tower-complete satisfiability problem, we prove that this logic is captured by four other logics that were independently found to be Tower-complete: two-variables separation logic, quantified computation tree logic, modal logic of heaps and modal separation logic. As a by-product of establishing these connections, we discover strict fragments of these logics that are still non-elementary.
Chapter PDF
Similar content being viewed by others
References
T. Antonopoulos and A. Dawar. Separating graph logic from MSO. In Foundations of Software Science and Computational Structures, volume 5504 of LNCS, pages 63–77. Springer, 2009.
A. Artale, R. Kontchakov, V. Ryzhikov, and M. Zakharyaschev. The complexity of clausal fragments of LTL. In Logic for Programming, Artificial Intelligence, and Reasoning, volume 8312 of LNCS, pages 35–52. Springer, 2013.
G. Aucher, P. Balbiani, L. Fariñas del Cerro, and A. Herzig. Global and local graph modifiers. Electronic Notes in Theoretical Computer Science, 231:293–307, 2009.
G. Aucher, J. van Benthem, and D. Grossi. Sabotage modal logic: Some model and proof theoretic aspects. In Logic, Rationality, and Interaction, volume 9394 of LNCS, pages 1–13. Springer, 2015.
B. Bednarczyk and S. Demri. Why propositional quantification makes modal logics on trees robustly hard? In Logic in Computer Science, pages 1–13. IEEE, 2019.
J. Berdine, B. Cook, and S. Ishtiaq. Slayer: Memory safety for systems-level code. In Computer-Aided Verification, volume 6806 of LNCS, pages 178–183. Springer, 2011.
L. Bozzelli, A. Molinari, A. Montanari, and A. Peron. On the complexity of model checking for syntactically maximal fragments of the interval temporal logic HS with regular expressions. In Games, Automata, Logics, and Formal Verification, volume 256 of EPTCS, pages 31–45, 2017.
L. Bozzelli, A. Molinari, A. Montanari, A. Peron, and P. Sala. Interval vs. point temporal logic model checking: an expressiveness comparison. In Foundations of Software Technology and Theoretical Computer Science, volume 65 of LIPIcs, pages 26:1–26:14. Schloss Dagstuhl–Leibniz-Zentrum fuer Informatik, 2016.
R. Brochenin, S. Demri, and E. Lozes. On the almighty wand. Information and Computation, 211:106–137, 2012.
C. Calcagno, T. Dinsdale-Young, and P. Gardner. Adjunct elimination in context logic for trees. Information and Computation, 208:474–499, 2010.
C. Calcagno, D. Distefano, J. Dubreil, D. Gabi, P. Hooimeijer, M. Luca, P. W. O’Hearn, I. Papakonstantinou, J. Purbrick, and D. Rodriguez. Moving fast with software verification. In Nasa Formal Methods, volume 9058 of LNCS, pages 3–11. Springer, 2015.
C. Calcagno, H. Yang, and P. W. O’Hearn. Computability and complexity results for a spatial assertion language for data structures. In Foundations of Software Technology and Theoretical Computer Science, volume 2245 of LNCS, pages 108–119. Springer, 2001.
E. M. Clarke. The Birth of Model Checking, pages 1–26. Springer, 2008.
E. M. Clarke and E. A. Emerson. Design and synthesis of synchronization skeletons using branching time temporal logic. In Logics of Programs, volume 131 of LNCS, pages 52–71. Springer, 1982.
B. Courcelle. Graph structure and monadic second-order logic: Language theoretical aspects. In Automata, Languages and Programming, volume 5125 of LNCS, pages 1–13. Springer, 2008.
A. Dawar, P. Gardner, and G. Ghelli. Adjunct elimination through games in static ambient logic. In Foundations of Software Technology and Theoretical Computer Science, volume 3328 of LNCS, pages 211–223. Springer, 2004.
S. Demri and M. Deters. Two-variable separation logic and its inner circle. Transactions on Computational Logic, 16:15:1–15:36, 2015.
S. Demri and R. Fervari. On the complexity of modal separation logics. In Advances in Modal Logic, pages 179–198. College Publications, 2018.
S. Demri, D. Galmiche, D. Larchey-Wendling, and D. Méry. Separation logic with one quantified variable. Theoretical Computer Science, 61:371–461, 2017.
S. Demri, E. Lozes, and A. Mansutti. The effects of adding reachability predicates in propositional separation logic. In Foundations of Software Science and Computational Structures, volume 10803 of LNCS, pages 476–493. Springer, 2018.
R. Fervari. Relation-Changing Modal Logics. PhD thesis, 2014.
K. Fine. Propositional quantifiers in modal logic. Theoria, 36:336–346, 1970.
M. J. Fischer and R. E. Ladner. Propositional dynamic logic of regular programs. Journal of Computer and System Sciences, 18:194 – 211, 1979.
V. Goranko. Temporal logics of computations. Lecture Notes from ESSLLI’00, 2000.
V. Goranko, A. Montanari, and G. Sciavicco. A road map of interval temporal logics and duration calculi. Journal of Applied Non-Classical Logics, 14:9–54, 2004.
V. Goranko and S. Passy. Using the universal modality: Gains and questions. Journal of Logic and Computation, 2:5–30, 1992.
S. A. Kripke. Semantical considerations on modal logic. Acta Philosophica Fennica, 16:83–94, 1963.
F. Laroussinie and N. Markey. Quantified CTL: expressiveness and complexity. Logical Methods in Computer Science, 10, 2014.
L. Libkin. Elements of Finite Model Theory. Texts in Theoretical Computer Science. An EATCS Series. Springer, 2004.
E. Lozes. Adjuncts elimination in the static ambient logic. Electronic Notes in Theoretical Computer Science, 96:51–72, 2004.
A. Mansutti. Extending propositional separation logic for robustness properties. In Foundations of Software Technology and Theoretical Computer Science, pages 42:1–42:23. Schloss Dagstuhl–Leibniz-Zentrum fuer Informatik, 2018.
D. A. Martin. Borel determinacy. Annals of Mathematics, 102:363–371, 1975.
A. Meier, M. Mundhenk, M. Thomas, and H. Vollmer. The complexity of satisfiability for fragments of CTL and CTL\(^*\). Electronic Notes in Theoretical Computer Science, 223:201–213, 2008.
B. C. Moszkowski. Reasoning About Digital Circuits. PhD thesis, 1983.
P. W. O’Hearn and D. J. Pym. The logic of bunched implications. Bulletin of Symbolic Logic, 5:215–244, 1999.
M. O. Rabin. Decidability of second-order theories and automata on infinite trees. Transactions of the American Mathematical Society, 41:1–35, 1969.
J. C. Reynolds. Separation logic: A logic for shared mutable data structures. In Logic in Computer Science, pages 55–74. IEEE, 2002.
S. Schmitz. Complexity hierarchies beyond elementary. ransactions on Computation Theory, 8:3:1–3:36, 2016.
A. P. Sistla and E. M. Clarke. The complexity of propositional linear temporal logics. Journal of the Association for Computing Machinery, 32:733–749, 1985.
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Open Access This chapter is licensed under the terms of the Creative Commons Attribution 4.0 International License (http://creativecommons.org/licenses/by/4.0/), which permits use, sharing, adaptation, distribution and reproduction in any medium or format, as long as you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons license and indicate if changes were made.
The images or other third party material in this chapter are included in the chapter's Creative Commons license, unless indicated otherwise in a credit line to the material. If material is not included in the chapter's Creative Commons license and your intended use is not permitted by statutory regulation or exceeds the permitted use, you will need to obtain permission directly from the copyright holder.
Copyright information
© 2020 The Author(s)
About this paper
Cite this paper
Mansutti, A. (2020). An Auxiliary Logic on Trees: on the Tower-Hardness of Logics Featuring Reachability and Submodel Reasoning. In: Goubault-Larrecq, J., König, B. (eds) Foundations of Software Science and Computation Structures. FoSSaCS 2020. Lecture Notes in Computer Science(), vol 12077. Springer, Cham. https://doi.org/10.1007/978-3-030-45231-5_24
Download citation
DOI: https://doi.org/10.1007/978-3-030-45231-5_24
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-030-45230-8
Online ISBN: 978-3-030-45231-5
eBook Packages: Mathematics and StatisticsMathematics and Statistics (R0)