{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,9,22]],"date-time":"2026-09-22T11:22:36Z","timestamp":1790076156529,"version":"4.0.1"},"publisher-location":"Cham","reference-count":39,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783030452308","type":"print"},{"value":"9783030452315","type":"electronic"}],"license":[{"start":{"date-parts":[[2020,1,1]],"date-time":"2020-01-01T00:00:00Z","timestamp":1577836800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2020]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>We describe a set of simple features that are sufficient in order to make the satisfiability problem of logics interpreted on trees <jats:sc>Tower<\/jats:sc>-hard. We exhibit these features through an <jats:italic>Auxiliary Logic on Trees<\/jats:italic> (), 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  admits a <jats:sc>Tower<\/jats:sc>-complete satisfiability problem, we prove that this logic is captured by four other logics that were independently found to be <jats:sc>Tower<\/jats:sc>-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.<\/jats:p>","DOI":"10.1007\/978-3-030-45231-5_24","type":"book-chapter","created":{"date-parts":[[2020,4,17]],"date-time":"2020-04-17T10:02:53Z","timestamp":1587117773000},"page":"462-481","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["An Auxiliary Logic on Trees: on the Tower-Hardness of Logics Featuring Reachability and Submodel Reasoning"],"prefix":"10.1007","author":[{"given":"Alessio","family":"Mansutti","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2020,4,17]]},"reference":[{"key":"24_CR1","doi-asserted-by":"crossref","unstructured":"T.\u00a0Antonopoulos and A.\u00a0Dawar. Separating graph logic from MSO. In Foundations of Software Science and Computational Structures, volume 5504 of LNCS, pages 63\u201377. Springer, 2009.","DOI":"10.1007\/978-3-642-00596-1_6"},{"key":"24_CR2","doi-asserted-by":"crossref","unstructured":"A.\u00a0Artale, R.\u00a0Kontchakov, V.\u00a0Ryzhikov, and M.\u00a0Zakharyaschev. The complexity of clausal fragments of LTL. In Logic for Programming, Artificial Intelligence, and Reasoning, volume 8312 of LNCS, pages 35\u201352. Springer, 2013.","DOI":"10.1007\/978-3-642-45221-5_3"},{"key":"24_CR3","doi-asserted-by":"crossref","unstructured":"G.\u00a0Aucher, P.\u00a0Balbiani, L.\u00a0Fari\u00f1as del Cerro, and A.\u00a0Herzig. Global and local graph modifiers. Electronic Notes in Theoretical Computer Science, 231:293\u2013307, 2009.","DOI":"10.1016\/j.entcs.2009.02.042"},{"key":"24_CR4","doi-asserted-by":"crossref","unstructured":"G.\u00a0Aucher, J.\u00a0van Benthem, and D.\u00a0Grossi. Sabotage modal logic: Some model and proof theoretic aspects. In Logic, Rationality, and Interaction, volume 9394 of LNCS, pages 1\u201313. Springer, 2015.","DOI":"10.1007\/978-3-662-48561-3_1"},{"key":"24_CR5","doi-asserted-by":"crossref","unstructured":"B.\u00a0Bednarczyk and S.\u00a0Demri. Why propositional quantification makes modal logics on trees robustly hard? In Logic in Computer Science, pages 1\u201313. IEEE, 2019.","DOI":"10.1109\/LICS.2019.8785656"},{"key":"24_CR6","doi-asserted-by":"crossref","unstructured":"J.\u00a0Berdine, B.\u00a0Cook, and S.\u00a0Ishtiaq. Slayer: Memory safety for systems-level code. In Computer-Aided Verification, volume 6806 of LNCS, pages 178\u2013183. Springer, 2011.","DOI":"10.1007\/978-3-642-22110-1_15"},{"key":"24_CR7","doi-asserted-by":"crossref","unstructured":"L.\u00a0Bozzelli, A.\u00a0Molinari, A.\u00a0Montanari, and A.\u00a0Peron. 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\u201345, 2017.","DOI":"10.4204\/EPTCS.256.3"},{"key":"24_CR8","unstructured":"L.\u00a0Bozzelli, A.\u00a0Molinari, A.\u00a0Montanari, A.\u00a0Peron, and P.\u00a0Sala. Interval vs. point temporal logic model checking: an expressiveness comparison. In Foundations of Software Technology and Theoretical Computer Science, volume\u00a065 of LIPIcs, pages 26:1\u201326:14. Schloss Dagstuhl\u2013Leibniz-Zentrum fuer Informatik, 2016."},{"key":"24_CR9","doi-asserted-by":"crossref","unstructured":"R.\u00a0Brochenin, S.\u00a0Demri, and E.\u00a0Lozes. On the almighty wand. Information and Computation, 211:106\u2013137, 2012.","DOI":"10.1016\/j.ic.2011.12.003"},{"key":"24_CR10","doi-asserted-by":"crossref","unstructured":"C.\u00a0Calcagno, T.\u00a0Dinsdale-Young, and P.\u00a0Gardner. Adjunct elimination in context logic for trees. Information and Computation, 208:474\u2013499, 2010.","DOI":"10.1016\/j.ic.2009.02.013"},{"key":"24_CR11","doi-asserted-by":"crossref","unstructured":"C.\u00a0Calcagno, D.\u00a0Distefano, J.\u00a0Dubreil, D.\u00a0Gabi, P.\u00a0Hooimeijer, M.\u00a0Luca, P.\u00a0W. O\u2019Hearn, I.\u00a0Papakonstantinou, J.\u00a0Purbrick, and D.\u00a0Rodriguez. Moving fast with software verification. In Nasa Formal Methods, volume 9058 of LNCS, pages 3\u201311. Springer, 2015.","DOI":"10.1007\/978-3-319-17524-9_1"},{"key":"24_CR12","doi-asserted-by":"crossref","unstructured":"C.\u00a0Calcagno, H.\u00a0Yang, and P.\u00a0W. O\u2019Hearn. 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\u2013119. Springer, 2001.","DOI":"10.1007\/3-540-45294-X_10"},{"key":"24_CR13","doi-asserted-by":"crossref","unstructured":"E.\u00a0M. Clarke. The Birth of Model Checking, pages 1\u201326. Springer, 2008.","DOI":"10.1007\/978-3-540-69850-0_1"},{"key":"24_CR14","doi-asserted-by":"crossref","unstructured":"E.\u00a0M. Clarke and E.\u00a0A. Emerson. Design and synthesis of synchronization skeletons using branching time temporal logic. In Logics of Programs, volume 131 of LNCS, pages 52\u201371. Springer, 1982.","DOI":"10.1007\/BFb0025774"},{"key":"24_CR15","doi-asserted-by":"crossref","unstructured":"B.\u00a0Courcelle. Graph structure and monadic second-order logic: Language theoretical aspects. In Automata, Languages and Programming, volume 5125 of LNCS, pages 1\u201313. Springer, 2008.","DOI":"10.1007\/978-3-540-70575-8_1"},{"key":"24_CR16","doi-asserted-by":"crossref","unstructured":"A.\u00a0Dawar, P.\u00a0Gardner, and G.\u00a0Ghelli. Adjunct elimination through games in static ambient logic. In Foundations of Software Technology and Theoretical Computer Science, volume 3328 of LNCS, pages 211\u2013223. Springer, 2004.","DOI":"10.1007\/978-3-540-30538-5_18"},{"key":"24_CR17","doi-asserted-by":"crossref","unstructured":"S.\u00a0Demri and M.\u00a0Deters. Two-variable separation logic and its inner circle. Transactions on Computational Logic, 16:15:1\u201315:36, 2015.","DOI":"10.1145\/2724711"},{"key":"24_CR18","unstructured":"S.\u00a0Demri and R.\u00a0Fervari. On the complexity of modal separation logics. In Advances in Modal Logic, pages 179\u2013198. College Publications, 2018."},{"key":"24_CR19","doi-asserted-by":"crossref","unstructured":"S.\u00a0Demri, D.\u00a0Galmiche, D.\u00a0Larchey-Wendling, and D.\u00a0M\u00e9ry. Separation logic with one quantified variable. Theoretical Computer Science, 61:371\u2013461, 2017.","DOI":"10.1007\/s00224-016-9713-1"},{"key":"24_CR20","doi-asserted-by":"crossref","unstructured":"S.\u00a0Demri, E.\u00a0Lozes, and A.\u00a0Mansutti. The effects of adding reachability predicates in propositional separation logic. In Foundations of Software Science and Computational Structures, volume 10803 of LNCS, pages 476\u2013493. Springer, 2018.","DOI":"10.1007\/978-3-319-89366-2_26"},{"key":"24_CR21","unstructured":"R.\u00a0Fervari. Relation-Changing Modal Logics. PhD thesis, 2014."},{"key":"24_CR22","doi-asserted-by":"crossref","unstructured":"K.\u00a0Fine. Propositional quantifiers in modal logic. Theoria, 36:336\u2013346, 1970.","DOI":"10.1111\/j.1755-2567.1970.tb00432.x"},{"key":"24_CR23","doi-asserted-by":"crossref","unstructured":"M.\u00a0J. Fischer and R.\u00a0E. Ladner. Propositional dynamic logic of regular programs. Journal of Computer and System Sciences, 18:194 \u2013 211, 1979.","DOI":"10.1016\/0022-0000(79)90046-1"},{"key":"24_CR24","unstructured":"V.\u00a0Goranko. Temporal logics of computations. Lecture Notes from ESSLLI\u201900, 2000."},{"key":"24_CR25","doi-asserted-by":"crossref","unstructured":"V.\u00a0Goranko, A.\u00a0Montanari, and G.\u00a0Sciavicco. A road map of interval temporal logics and duration calculi. Journal of Applied Non-Classical Logics, 14:9\u201354, 2004.","DOI":"10.3166\/jancl.14.9-54"},{"key":"24_CR26","unstructured":"V.\u00a0Goranko and S.\u00a0Passy. Using the universal modality: Gains and questions. Journal of Logic and Computation, 2:5\u201330, 1992."},{"key":"24_CR27","unstructured":"S.\u00a0A. Kripke. Semantical considerations on modal logic. Acta Philosophica Fennica, 16:83\u201394, 1963."},{"key":"24_CR28","doi-asserted-by":"crossref","unstructured":"F.\u00a0Laroussinie and N.\u00a0Markey. Quantified CTL: expressiveness and complexity. Logical Methods in Computer Science, 10, 2014.","DOI":"10.2168\/LMCS-10(4:17)2014"},{"key":"24_CR29","doi-asserted-by":"crossref","unstructured":"L.\u00a0Libkin. Elements of Finite Model Theory. Texts in Theoretical Computer Science. An EATCS Series. Springer, 2004.","DOI":"10.1007\/978-3-662-07003-1"},{"key":"24_CR30","doi-asserted-by":"crossref","unstructured":"E.\u00a0Lozes. Adjuncts elimination in the static ambient logic. Electronic Notes in Theoretical Computer Science, 96:51\u201372, 2004.","DOI":"10.1016\/j.entcs.2004.04.021"},{"key":"24_CR31","unstructured":"A.\u00a0Mansutti. Extending propositional separation logic for robustness properties. In Foundations of Software Technology and Theoretical Computer Science, pages 42:1\u201342:23. Schloss Dagstuhl\u2013Leibniz-Zentrum fuer Informatik, 2018."},{"key":"24_CR32","doi-asserted-by":"crossref","unstructured":"D.\u00a0A. Martin. Borel determinacy. Annals of Mathematics, 102:363\u2013371, 1975.","DOI":"10.2307\/1971035"},{"key":"24_CR33","doi-asserted-by":"crossref","unstructured":"A.\u00a0Meier, M.\u00a0Mundhenk, M.\u00a0Thomas, and H.\u00a0Vollmer. The complexity of satisfiability for fragments of CTL and CTL$$^*$$. Electronic Notes in Theoretical Computer Science, 223:201\u2013213, 2008.","DOI":"10.1016\/j.entcs.2008.12.040"},{"key":"24_CR34","unstructured":"B.\u00a0C. Moszkowski. Reasoning About Digital Circuits. PhD thesis, 1983."},{"key":"24_CR35","doi-asserted-by":"crossref","unstructured":"P.\u00a0W. O\u2019Hearn and D.\u00a0J. Pym. The logic of bunched implications. Bulletin of Symbolic Logic, 5:215\u2013244, 1999.","DOI":"10.2307\/421090"},{"key":"24_CR36","doi-asserted-by":"crossref","unstructured":"M.\u00a0O. Rabin. Decidability of second-order theories and automata on infinite trees. Transactions of the American Mathematical Society, 41:1\u201335, 1969.","DOI":"10.2307\/1995086"},{"key":"24_CR37","unstructured":"J.\u00a0C. Reynolds. Separation logic: A logic for shared mutable data structures. In Logic in Computer Science, pages 55\u201374. IEEE, 2002."},{"key":"24_CR38","doi-asserted-by":"crossref","unstructured":"S.\u00a0Schmitz. Complexity hierarchies beyond elementary. ransactions on Computation Theory, 8:3:1\u20133:36, 2016.","DOI":"10.1145\/2858784"},{"key":"24_CR39","doi-asserted-by":"crossref","unstructured":"A.\u00a0P. Sistla and E.\u00a0M. Clarke. The complexity of propositional linear temporal logics. Journal of the Association for Computing Machinery, 32:733\u2013749, 1985.","DOI":"10.1145\/3828.3837"}],"container-title":["Lecture Notes in Computer Science","Foundations of Software Science and Computation Structures"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-45231-5_24","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,1,7]],"date-time":"2021-01-07T14:03:27Z","timestamp":1610028207000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-030-45231-5_24"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2020]]},"ISBN":["9783030452308","9783030452315"],"references-count":39,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-45231-5_24","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2020]]},"assertion":[{"value":"17 April 2020","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"FoSSaCS","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Foundations of Software Science and Computation Structures","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Dublin","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Ireland","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2020","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"25 April 2020","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"30 April 2020","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"23","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"fossacs2020","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/www.etaps.org\/2020\/fossacs","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Single-blind","order":1,"name":"type","label":"Type","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"EasyChair","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"98","order":3,"name":"number_of_submissions_sent_for_review","label":"Number of Submissions Sent for Review","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"31","order":4,"name":"number_of_full_papers_accepted","label":"Number of Full Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"0","order":5,"name":"number_of_short_papers_accepted","label":"Number of Short Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"32% - The value is computed by the equation \"Number of Full Papers Accepted \/ Number of Submissions Sent for Review * 100\" and then rounded to a whole number.","order":6,"name":"acceptance_rate_of_full_papers","label":"Acceptance Rate of Full Papers","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"3","order":7,"name":"average_number_of_reviews_per_paper","label":"Average Number of Reviews per Paper","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"12","order":8,"name":"average_number_of_papers_per_reviewer","label":"Average Number of Papers per Reviewer","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"Yes","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"The conference could not take place due to the COVID-19 pandemic. There was an online event on July 2, 2020.","order":10,"name":"additional_info_on_review_process","label":"Additional Info on Review Process","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}