{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,19]],"date-time":"2026-02-19T23:48:15Z","timestamp":1771544895336,"version":"3.50.1"},"reference-count":55,"publisher":"IEEE","license":[{"start":{"date-parts":[[2019,6,1]],"date-time":"2019-06-01T00:00:00Z","timestamp":1559347200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/ieeexplore.ieee.org\/Xplorehelp\/downloads\/license-information\/IEEE.html"},{"start":{"date-parts":[[2019,6,1]],"date-time":"2019-06-01T00:00:00Z","timestamp":1559347200000},"content-version":"stm-asf","delay-in-days":0,"URL":"https:\/\/doi.org\/10.15223\/policy-029"},{"start":{"date-parts":[[2019,6,1]],"date-time":"2019-06-01T00:00:00Z","timestamp":1559347200000},"content-version":"stm-asf","delay-in-days":0,"URL":"https:\/\/doi.org\/10.15223\/policy-037"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2019,6]]},"DOI":"10.1109\/lics.2019.8785656","type":"proceedings-article","created":{"date-parts":[[2019,8,6]],"date-time":"2019-08-06T01:15:55Z","timestamp":1565054155000},"page":"1-13","source":"Crossref","is-referenced-by-count":6,"title":["Why Propositional Quantification Makes Modal Logics on Trees Robustly Hard?"],"prefix":"10.1109","author":[{"given":"Bartosz","family":"Bednarczyk","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Stephane","family":"Demri","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"263","reference":[{"key":"ref39","first-page":"1","article-title":"On a decision method in restricted second-order arithmetic","author":"b\u00fcchi","year":"1960","journal-title":"Logic Methodology and Philosophy of Science"},{"key":"ref38","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-59126-6_7"},{"key":"ref33","first-page":"1","article-title":"Decidability of second-order theories and automata on infinite trees","volume":"41","author":"rabin","year":"1969","journal-title":"Transactions of the American Mathematical Society"},{"key":"ref32","author":"molinari","year":"2019","journal-title":"Model checking The interval way"},{"key":"ref31","doi-asserted-by":"publisher","DOI":"10.4204\/EPTCS.256.3"},{"key":"ref30","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9781139236119"},{"key":"ref37","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45656-2_15"},{"key":"ref36","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0025774"},{"key":"ref35","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9781107050884"},{"key":"ref34","doi-asserted-by":"publisher","DOI":"10.1016\/S0019-9958(84)80047-9"},{"key":"ref28","article-title":"Hybrid branching-time logics","volume":"abs 708 1723","author":"weber","year":"2007","journal-title":"CoRR"},{"key":"ref27","article-title":"Narcissists, stepmothers and spies","volume":"53","author":"marx","year":"2002","journal-title":"Workshop on Description Logics (DL '02) ser CEUR Workshop Proceedings"},{"key":"ref29","doi-asserted-by":"publisher","DOI":"10.1093\/logcom\/2.1.5"},{"key":"ref2","doi-asserted-by":"publisher","DOI":"10.1111\/j.1755-2567.1970.tb00432.x"},{"key":"ref1","first-page":"257","article-title":"On modal logic with propositional quantifiers","volume":"34","author":"bull","year":"1969","journal-title":"JSL"},{"key":"ref20","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2015.07.015"},{"key":"ref22","doi-asserted-by":"publisher","DOI":"10.1016\/j.artint.2018.07.004"},{"key":"ref21","first-page":"886","article-title":"A semantical analysis of second-order propositional modal logic","author":"belardinelli","year":"2016","journal-title":"AAAI-16"},{"key":"ref24","doi-asserted-by":"publisher","DOI":"10.1093\/logcom\/9.2.135"},{"key":"ref23","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-45138-9_58"},{"key":"ref26","doi-asserted-by":"publisher","DOI":"10.2307\/2695090"},{"key":"ref25","doi-asserted-by":"publisher","DOI":"10.1093\/jigpal\/8.5.653"},{"key":"ref50","doi-asserted-by":"publisher","DOI":"10.1145\/800070.802186"},{"key":"ref51","first-page":"437","article-title":"The complexity of temporal logic model checking","author":"schnoebelen","year":"2003","journal-title":"AIML'02"},{"key":"ref55","first-page":"1:1","article-title":"On temporal and separation logics (invited paper)","volume":"120","author":"demri","year":"2018","journal-title":"TIME'18 ser LIPIcs"},{"key":"ref54","first-page":"179","article-title":"On the complexity of modal separation logics","author":"demri","year":"2018","journal-title":"AiML'18"},{"key":"ref53","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4613-8601-8"},{"key":"ref52","author":"segerberg","year":"1971","journal-title":"An essay in classical modal logic (three vols )"},{"key":"ref10","author":"sistla","year":"1983","journal-title":"Theoretical Issues in the Design and Verification of Distributed Systems"},{"key":"ref11","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(87)90008-9"},{"key":"ref40","doi-asserted-by":"publisher","DOI":"10.1305\/ndjfl\/1093634729"},{"key":"ref12","first-page":"26","author":"meyer","year":"1973","journal-title":"Weak second order theory of successor is not elementary-recursive"},{"key":"ref13","doi-asserted-by":"publisher","DOI":"10.2168\/LMCS-10(4:17)2014"},{"key":"ref14","first-page":"28: 1","article-title":"On the expressiveness of QCTL","volume":"59","author":"david","year":"2016","journal-title":"CONCUR'16 ser LIPIcs"},{"key":"ref15","doi-asserted-by":"publisher","DOI":"10.1145\/2858784"},{"key":"ref16","doi-asserted-by":"publisher","DOI":"10.1023\/B:LOGI.0000021744.10237.d0"},{"key":"ref17","doi-asserted-by":"publisher","DOI":"10.1016\/j.ic.2014.12.020"},{"key":"ref18","doi-asserted-by":"publisher","DOI":"10.1016\/S0020-0190(01)00260-5"},{"key":"ref19","doi-asserted-by":"publisher","DOI":"10.1109\/TIME.2003.1214891"},{"key":"ref4","doi-asserted-by":"publisher","DOI":"10.2178\/jsl\/1190150147"},{"key":"ref3","first-page":"355","article-title":"S5 with quantifiable propositional variables","volume":"35","author":"kaplan","year":"1970","journal-title":"JSL"},{"key":"ref6","doi-asserted-by":"publisher","DOI":"10.1305\/ndjfl\/1094155276"},{"key":"ref5","first-page":"29","article-title":"Knowledge and the logic of local propositions","author":"engelhardt","year":"1998","journal-title":"TARK'98"},{"key":"ref8","doi-asserted-by":"publisher","DOI":"10.1305\/ndjfl\/1039724892"},{"key":"ref7","doi-asserted-by":"publisher","DOI":"10.1305\/ndjfl\/1040067314"},{"key":"ref49","author":"stockmeyer","year":"1974","journal-title":"The Complexity of Decision Problems in Automata Theory and Logic"},{"key":"ref9","doi-asserted-by":"publisher","DOI":"10.1007\/s10992-005-9012-9"},{"key":"ref46","doi-asserted-by":"publisher","DOI":"10.1305\/ndjfl\/1093890715"},{"key":"ref45","doi-asserted-by":"publisher","DOI":"10.1137\/0204006"},{"key":"ref48","doi-asserted-by":"publisher","DOI":"10.1093\/logcom\/11.1.85"},{"key":"ref47","doi-asserted-by":"publisher","DOI":"10.1007\/BF00379767"},{"key":"ref42","first-page":"331","article-title":"The convenience of tilings","volume":"187","author":"van emde boas","year":"1997","journal-title":"Complexity Logic and Recursion Theory"},{"key":"ref41","first-page":"240","article-title":"Quantified propositional G&#x00F6;del logics","volume":"1955","author":"baaz","year":"2000","journal-title":"LPAR '00 ser LNCS"},{"key":"ref44","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(80)90037-7"},{"key":"ref43","doi-asserted-by":"publisher","DOI":"10.1145\/322234.322243"}],"event":{"name":"2019 34th Annual ACM\/IEEE Symposium on Logic in Computer Science (LICS)","location":"Vancouver, BC, Canada","start":{"date-parts":[[2019,6,24]]},"end":{"date-parts":[[2019,6,27]]}},"container-title":["2019 34th Annual ACM\/IEEE Symposium on Logic in Computer Science (LICS)"],"original-title":[],"link":[{"URL":"http:\/\/xplorestaging.ieee.org\/ielx7\/8765678\/8785654\/08785656.pdf?arnumber=8785656","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,7,19]],"date-time":"2022-07-19T20:18:53Z","timestamp":1658261933000},"score":1,"resource":{"primary":{"URL":"https:\/\/ieeexplore.ieee.org\/document\/8785656\/"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019,6]]},"references-count":55,"URL":"https:\/\/doi.org\/10.1109\/lics.2019.8785656","relation":{},"subject":[],"published":{"date-parts":[[2019,6]]}}}