{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,26]],"date-time":"2025-03-26T03:01:12Z","timestamp":1742958072050,"version":"3.40.3"},"publisher-location":"Cham","reference-count":32,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783030992521"},{"type":"electronic","value":"9783030992538"}],"license":[{"start":{"date-parts":[[2022,1,1]],"date-time":"2022-01-01T00:00:00Z","timestamp":1640995200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2022,3,29]],"date-time":"2022-03-29T00:00:00Z","timestamp":1648512000000},"content-version":"vor","delay-in-days":87,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2022]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>We study a family of <jats:italic>modal logics<\/jats:italic> interpreted on tree-like structures, and featuring <jats:italic>local quantifiers<\/jats:italic>\u00a0<jats:inline-formula><jats:alternatives><jats:tex-math>$$\\exists ^{k}p$$<\/jats:tex-math><mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\">\n                <mml:mrow>\n                  <mml:msup>\n                    <mml:mo>\u2203<\/mml:mo>\n                    <mml:mi>k<\/mml:mi>\n                  <\/mml:msup>\n                  <mml:mi>p<\/mml:mi>\n                <\/mml:mrow>\n              <\/mml:math><\/jats:alternatives><\/jats:inline-formula> that bind the proposition\u00a0<jats:italic>p<\/jats:italic> to worlds that are accessible from the current one in at most\u00a0<jats:italic>k<\/jats:italic>\u00a0steps. We consider a first-order and a second-order semantics for the quantifiers, which enables us to relate several well-known formalisms, such as <jats:italic>hybrid logics<\/jats:italic>,\u00a0<jats:inline-formula><jats:alternatives><jats:tex-math>$$\\textsf {S5Q}$$<\/jats:tex-math><mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\">\n                <mml:mrow>\n                  <mml:mi>S<\/mml:mi>\n                  <mml:mn>5<\/mml:mn>\n                  <mml:mi>Q<\/mml:mi>\n                <\/mml:mrow>\n              <\/mml:math><\/jats:alternatives><\/jats:inline-formula> and <jats:italic>graded modal logic<\/jats:italic>. To better stress these connections, we explore fragments of our logics, called herein <jats:italic>round-bounded<\/jats:italic> fragments. Depending on whether first or second-order semantics is considered, these fragments populate the hierarchy <jats:inline-formula><jats:alternatives><jats:tex-math>$${2\\textsc {NExp} \\subset 3\\textsc {NExp} \\subset \\cdots }$$<\/jats:tex-math><mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\">\n                <mml:mrow>\n                  <mml:mn>2<\/mml:mn>\n                  <mml:mi>NE<\/mml:mi>\n                  <mml:mstyle>\n                    <mml:mi>X<\/mml:mi>\n                    <mml:mi>P<\/mml:mi>\n                  <\/mml:mstyle>\n                  <mml:mo>\u2282<\/mml:mo>\n                  <mml:mn>3<\/mml:mn>\n                  <mml:mi>NE<\/mml:mi>\n                  <mml:mstyle>\n                    <mml:mi>X<\/mml:mi>\n                    <mml:mi>P<\/mml:mi>\n                  <\/mml:mstyle>\n                  <mml:mo>\u2282<\/mml:mo>\n                  <mml:mo>\u22ef<\/mml:mo>\n                <\/mml:mrow>\n              <\/mml:math><\/jats:alternatives><\/jats:inline-formula> or the hierarchy <jats:inline-formula><jats:alternatives><jats:tex-math>$${2\\textsc {AExp}_{pol} \\subset 3\\textsc {AExp}_{pol} \\subset \\cdots }$$<\/jats:tex-math><mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\">\n                <mml:mrow>\n                  <mml:mn>2<\/mml:mn>\n                  <mml:mi>AE<\/mml:mi>\n                  <mml:msub>\n                    <mml:mstyle>\n                      <mml:mi>X<\/mml:mi>\n                      <mml:mi>P<\/mml:mi>\n                    <\/mml:mstyle>\n                    <mml:mrow>\n                      <mml:mi>pol<\/mml:mi>\n                    <\/mml:mrow>\n                  <\/mml:msub>\n                  <mml:mo>\u2282<\/mml:mo>\n                  <mml:mn>3<\/mml:mn>\n                  <mml:mi>AE<\/mml:mi>\n                  <mml:msub>\n                    <mml:mstyle>\n                      <mml:mi>X<\/mml:mi>\n                      <mml:mi>P<\/mml:mi>\n                    <\/mml:mstyle>\n                    <mml:mrow>\n                      <mml:mi>pol<\/mml:mi>\n                    <\/mml:mrow>\n                  <\/mml:msub>\n                  <mml:mo>\u2282<\/mml:mo>\n                  <mml:mo>\u22ef<\/mml:mo>\n                <\/mml:mrow>\n              <\/mml:math><\/jats:alternatives><\/jats:inline-formula>, respectively. For formulae up-to modal depth <jats:italic>k<\/jats:italic>, the complexity improves by one exponential.<\/jats:p>","DOI":"10.1007\/978-3-030-99253-8_16","type":"book-chapter","created":{"date-parts":[[2022,3,28]],"date-time":"2022-03-28T20:02:48Z","timestamp":1648497768000},"page":"305-324","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Modal Logics and Local Quantifiers: A Zoo in the Elementary Hierarchy"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-0360-0725","authenticated-orcid":false,"given":"Raul","family":"Fervari","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-1104-7299","authenticated-orcid":false,"given":"Alessio","family":"Mansutti","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2022,3,29]]},"reference":[{"key":"16_CR1","doi-asserted-by":"crossref","unstructured":"Andr\u00e9ka, H., N\u00e9meti, I., van Benthem, J.: Modal languages and bounded fragments of predicate logic. Journal of Philosophical Logic 27(3), 217\u2013274 (1998)","DOI":"10.1023\/A:1004275029985"},{"key":"16_CR2","doi-asserted-by":"crossref","unstructured":"Areces, C., Blackburn, P., Marx, M.: Hybrid logics: characterization, interpolation and complexity. The Journal of Symbolic Logic 66(3), 977\u20131010 (2001)","DOI":"10.2307\/2695090"},{"key":"16_CR3","doi-asserted-by":"crossref","unstructured":"Areces, C., ten Cate, B.: Hybrid logics. In: Handbook of Modal Logic, Studies in logic and practical reasoning, vol.\u00a03, pp. 821\u2013868. North-Holland (2007)","DOI":"10.1016\/S1570-2464(07)80017-6"},{"key":"16_CR4","doi-asserted-by":"crossref","unstructured":"Areces, C., Fervari, R., Hoffmann, G.: Relation-changing modal operators. Logic Journal of the IGPL 23(4), 601\u2013627 (2015)","DOI":"10.1093\/jigpal\/jzv020"},{"key":"16_CR5","doi-asserted-by":"crossref","unstructured":"Barnaba, M.F., Caro, F.D.: Graded modalities. Studia Logica 44(2), 197\u2013221 (1985)","DOI":"10.1007\/BF00379767"},{"key":"16_CR6","doi-asserted-by":"crossref","unstructured":"Bednarczyk, B., Demri, S.: Why propositional quantification makes modal logics on trees robustly hard? In: Logic in Computer Science. pp. 1\u201313. IEEE (2019)","DOI":"10.1109\/LICS.2019.8785656"},{"key":"16_CR7","doi-asserted-by":"crossref","unstructured":"Bednarczyk, B., Demri, S., Fervari, R., Mansutti, A.: Modal logics with composition on finite forests: Expressivity and complexity. In: Logic in Computer Science. pp. 167\u2013180. ACM (2020)","DOI":"10.1145\/3373718.3394787"},{"key":"16_CR8","doi-asserted-by":"crossref","unstructured":"van Benthem, J.: An essay on sabotage and obstruction. In: Mechanizing Mathematical Reasoning. LNCS, vol.\u00a02605, pp. 268\u2013276 (2005)","DOI":"10.1007\/978-3-540-32254-2_16"},{"key":"16_CR9","unstructured":"Blackburn, P., Bra\u00fcner, T., Kofod, J.: Remarks on Hybrid Modal Logic with Propositional Quantifiers, pp. 401\u2013426. No.\u00a04 in Logic and Philosophy of Time (2020)"},{"key":"16_CR10","unstructured":"Blackburn, P., Wolter, F., van Benthem, J. (eds.): Handbook of Modal Logics, Studies in logic and practical reasoning, vol.\u00a03. Elsevier (2006)"},{"key":"16_CR11","doi-asserted-by":"crossref","unstructured":"Bozzelli, L., Molinari, A., Montanari, A., Peron, A.: On the complexity of model checking for syntactically maximal fragments of the interval temporal logic HS with regular expressions. In: GandALF\u201917. EPTCS, vol.\u00a0256, pp. 31\u201345 (2017)","DOI":"10.4204\/EPTCS.256.3"},{"key":"16_CR12","doi-asserted-by":"crossref","unstructured":"Bull, R.A.: On modal logic with propositional quantifiers. The Journal of Symbolic Logic 34(2), 257\u2013263 (1969)","DOI":"10.1017\/S0022481200094512"},{"key":"16_CR13","doi-asserted-by":"crossref","unstructured":"Calcagno, C., Cardelli, L., Gordon, A.: Deciding validity in a spatial logic for trees. In: International Workshop on Types in Languages Design and Implementation. pp. 62\u201373. ACM (2003)","DOI":"10.1145\/640136.604183"},{"key":"16_CR14","doi-asserted-by":"crossref","unstructured":"ten Cate, B., Franceschet, M.: On the complexity of hybrid logics with binders. In: Ong, L. (ed.) Computer Science Logic. pp. 339\u2013354 (2005)","DOI":"10.1007\/11538363_24"},{"key":"16_CR15","doi-asserted-by":"crossref","unstructured":"Chandra, A.K., Kozen, D.C., Stockmeyer, L.J.: Alternation. Journal of the ACM 28(1), 114\u2013133 (1981)","DOI":"10.1145\/322234.322243"},{"key":"16_CR16","doi-asserted-by":"crossref","unstructured":"Demri, S., Fervari, R.: The power of modal separation logics. Journal of Logic and Computation 29(8), 1139\u20131184 (2019)","DOI":"10.1093\/logcom\/exz019"},{"key":"16_CR17","unstructured":"Ding, Y.: On the logics with propositional quantifiers extending s5$$\\varPi $$. In: Advances in Modal Logic. pp. 219\u2013235. College Publications (2018)"},{"key":"16_CR18","doi-asserted-by":"crossref","unstructured":"Fine, K.: Propositional quantifiers in modal logic. Theoria 36, 336\u2013346 (1970)","DOI":"10.1111\/j.1755-2567.1970.tb00432.x"},{"key":"16_CR19","doi-asserted-by":"crossref","unstructured":"Fischer, M.J., Ladner, R.E.: Propositional modal logic of programs. In: ACM Symposium on Theory of Computing. p. 286\u2013294 (1977)","DOI":"10.1145\/800105.803418"},{"key":"16_CR20","unstructured":"Fischer, M.J., Rabin, M.O.: Super-exponential complexity of presburger arithmetic. In: Complexity of Computation, SIAM\u2013AMS Proceedings. pp. 27\u201341 (1974)"},{"key":"16_CR21","doi-asserted-by":"crossref","unstructured":"Hannula, M., Kontinen, J., Virtema, J., Vollmer, H.: Complexity of propositional logics in team semantic. ACM Transactions on Computational Logic 19(1), 2:1\u20132:14 (2018)","DOI":"10.1145\/3157054"},{"key":"16_CR22","unstructured":"Kaplan, D.: S5 with quantifiable propositional variables. The Journal of Symbolic Logic 35(2), \u00a0355 (1970)"},{"key":"16_CR23","unstructured":"Mansutti, A.: Reasoning with Separation Logics: Complexity, Expressive Power, Proof Systems. Ph.D. thesis, Universit\u00e9 Paris-Saclay (December 2020)"},{"key":"16_CR24","unstructured":"Mansutti, A.: Notes on kAExp(pol) problems for deterministic machines (2021)"},{"key":"16_CR25","doi-asserted-by":"crossref","unstructured":"Meier, A., Mundhenk, M., Thomas, M., Vollmer, H.: 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":"16_CR26","doi-asserted-by":"crossref","unstructured":"Prior, A.: Past, Present and Future. Oxford Books (1967)","DOI":"10.1093\/acprof:oso\/9780198243113.001.0001"},{"key":"16_CR27","doi-asserted-by":"crossref","unstructured":"Rabin, M.: Decidability of second-order theories and automata on infinite trees. Transactions of the American Mathematical Society 41, 1\u201335 (1969)","DOI":"10.1090\/S0002-9947-1969-0246760-1"},{"key":"16_CR28","doi-asserted-by":"crossref","unstructured":"de\u00a0Rijke, M.: A note on graded modal logic. Studia Logica 64(2), 271\u2013283 (2000)","DOI":"10.1023\/A:1005245900406"},{"key":"16_CR29","doi-asserted-by":"crossref","unstructured":"Schmitz, S.: Complexity hierarchies beyond elementary. ACM Transactions on Computation Theory 8(1), 3:1\u20133:36 (2016)","DOI":"10.1145\/2858784"},{"key":"16_CR30","unstructured":"Schneider, T.: The complexity of hybrid logics over restricted frame classes. Ph.D. thesis, Friedrich Schiller University of Jena (2007)"},{"key":"16_CR31","doi-asserted-by":"crossref","unstructured":"Sistla, A.P., Clarke, E.M.: The complexity of propositional linear temporal logics. Journal of the ACM 32(3), 733\u2013749 (1985)","DOI":"10.1145\/3828.3837"},{"key":"16_CR32","doi-asserted-by":"crossref","unstructured":"Yang, F., V\u00e4\u00e4n\u00e4nen, J.: Propositional logics of dependence. Annals of Pure and Applied Logic 167(7), 557\u2013589 (2016)","DOI":"10.1016\/j.apal.2016.03.003"}],"container-title":["Lecture Notes in Computer Science","Foundations of Software Science and Computation Structures"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-99253-8_16","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,3,28]],"date-time":"2022-03-28T20:07:07Z","timestamp":1648498027000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-030-99253-8_16"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022]]},"ISBN":["9783030992521","9783030992538"],"references-count":32,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-99253-8_16","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2022]]},"assertion":[{"value":"29 March 2022","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":"Munich","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Germany","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2022","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"4 April 2022","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"6 April 2022","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"25","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"fossacs2022","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/etaps.org\/2022\/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":"77","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":"23","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":"30% - 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":"9","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)"}}]}}