{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,28]],"date-time":"2025-10-28T00:27:20Z","timestamp":1761611240170,"version":"3.41.0"},"reference-count":49,"publisher":"Association for Computing Machinery (ACM)","issue":"2","license":[{"start":{"date-parts":[[2009,2,1]],"date-time":"2009-02-01T00:00:00Z","timestamp":1233446400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/501100001659","name":"Deutsche Forschungsgemeinschaft","doi-asserted-by":"publisher","award":["HasCASL (KR 1191\/7-2)"],"award-info":[{"award-number":["HasCASL (KR 1191\/7-2)"]}],"id":[{"id":"10.13039\/501100001659","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Comput. Logic"],"published-print":{"date-parts":[[2009,2]]},"abstract":"<jats:p>\n            For lack of general algorithmic methods that apply to wide classes of logics, establishing a complexity bound for a given modal logic is often a laborious task. The present work is a step towards a general theory of the complexity of modal logics. Our main result is that all rank-1 logics enjoy a shallow model property and thus are, under mild assumptions on the format of their axiomatisation, in\n            <jats:italic>PSPACE<\/jats:italic>\n            . This leads to a unified derivation of tight\n            <jats:italic>PSPACE<\/jats:italic>\n            -bounds for a number of logics, including\n            <jats:italic>K<\/jats:italic>\n            ,\n            <jats:italic>KD<\/jats:italic>\n            , coalition logic, graded modal logic, majority logic, and probabilistic modal logic. Our generic algorithm moreover finds tableau proofs that witness pleasant proof-theoretic properties including a weak subformula property. This generality is made possible by a coalgebraic semantics, which conveniently abstracts from the details of a given model class and thus allows covering a broad range of logics in a uniform way.\n          <\/jats:p>","DOI":"10.1145\/1462179.1462185","type":"journal-article","created":{"date-parts":[[2009,2,25]],"date-time":"2009-02-25T14:44:30Z","timestamp":1235573070000},"page":"1-33","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":34,"title":["PSPACE bounds for rank-1 modal logics"],"prefix":"10.1145","volume":"10","author":[{"given":"LUTZ","family":"Schr\u00f6der","sequence":"first","affiliation":[{"name":"DFKI Bremen and Universit\u00e4t Bremen, Bremen, Germany"}]},{"given":"Dirk","family":"Pattinson","sequence":"additional","affiliation":[{"name":"Imperial College London, London, UK"}]}],"member":"320","published-online":{"date-parts":[[2009,3,2]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(93)90076-6"},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129502003900"},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2004.07.019"},{"key":"e_1_2_1_4_1","doi-asserted-by":"crossref","unstructured":"Blackburn P. de Rijke M. and Venema Y. 2001. Modal Logic. Cambridge University Press Cambridge.   Blackburn P. de Rijke M. and Venema Y. 2001. Modal Logic. Cambridge University Press Cambridge.","DOI":"10.1017\/CBO9781107050884"},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1137\/0213030"},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0022-0000(71)80005-3"},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF00374047"},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/322234.322243"},{"volume-title":"Modal Logic","author":"Chellas B.","key":"e_1_2_1_9_1","unstructured":"Chellas , B. 1980. Modal Logic . Cambridge University Press , Cambridge . Chellas, B. 1980. Modal Logic. Cambridge University Press, Cambridge."},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2007.06.002"},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1007\/s001530100110"},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1093\/jigpal\/8.3.265"},{"key":"e_1_2_1_13_1","volume-title":"Proceedings of the 3rd International Joint Conference on Automated Reasoning (IJCAR'06)","volume":"4130","author":"Demri S.","unstructured":"Demri , S. and Lugiez , D . 2006. Presburger modal logic is only PSPACE-complete . In Proceedings of the 3rd International Joint Conference on Automated Reasoning (IJCAR'06) , U. Furbach and N. Shankar, Eds. Lecture Notes in Artificial Intelligence , vol. 4130 . Springer, Berlin, 541--556. Full version available as Res. rep. LSV-06-15, Laboratoire Sp\u00e9cification et V\u00e9rification, Ecole Normale Sup\u00e9rieure de Cachan. Demri, S. and Lugiez, D. 2006. Presburger modal logic is only PSPACE-complete. In Proceedings of the 3rd International Joint Conference on Automated Reasoning (IJCAR'06), U. Furbach and N. Shankar, Eds. Lecture Notes in Artificial Intelligence, vol. 4130. Springer, Berlin, 541--556. Full version available as Res. rep. LSV-06-15, Laboratoire Sp\u00e9cification et V\u00e9rification, Ecole Normale Sup\u00e9rieure de Cachan."},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1016\/0022-0000(85)90001-7"},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(89)90137-0"},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/174652.174658"},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1305\/ndjfl\/1093890715"},{"volume-title":"Proceedings of the 20th International Joint Conference on Artificial Intelligence (IJCAI'07)","author":"Halpern J.","key":"e_1_2_1_18_1","unstructured":"Halpern , J. and R\u00eago , L. C . 2007. Characterizing the NP-PSPACE gap in the satisfiability problem for modal logic . In Proceedings of the 20th International Joint Conference on Artificial Intelligence (IJCAI'07) , M. M. Veloso, Ed. 2306--2311. Halpern, J. and R\u00eago, L. C. 2007. Characterizing the NP-PSPACE gap in the satisfiability problem for modal logic. In Proceedings of the 20th International Joint Conference on Artificial Intelligence (IJCAI'07), M. M. Veloso, Ed. 2306--2311."},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1016\/0004-3702(92)90049-4"},{"key":"e_1_2_1_20_1","volume-title":"Eds. Electronic Notes in Theoretical Computer Science","volume":"106","author":"Hansen H. H.","unstructured":"Hansen , H. H. and Kupke , C . 2004. A coalgebraic perspective on monotone modal logic. In Coalgebraic Methods in Computer Science, J. Ad\u00e1mek and S. Milius , Eds. Electronic Notes in Theoretical Computer Science , vol. 106 . Elsevier, Amsterdam, 121--143. Hansen, H. H. and Kupke, C. 2004. A coalgebraic perspective on monotone modal logic. In Coalgebraic Methods in Computer Science, J. Ad\u00e1mek and S. Milius, Eds. Electronic Notes in Theoretical Computer Science, vol. 106. Elsevier, Amsterdam, 121--143."},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1006\/game.1999.0788"},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1016\/S1571-0661(05)80348-2"},{"key":"e_1_2_1_23_1","volume-title":"Proceedings of the 1st International Conference on Algebra and Coalgebra in Computer Science (CALCO'05)","volume":"3629","author":"Kupke C.","unstructured":"Kupke , C. , Kurz , A. , and Pattinson , D . 2005. Ultrafilter extensions for coalgebras . In Proceedings of the 1st International Conference on Algebra and Coalgebra in Computer Science (CALCO'05) , J. L. Fiadeiro et al. Eds. Lecture Notes in Computer Science , vol. 3629 . Springer, Berlin, 263--277. Kupke, C., Kurz, A., and Pattinson, D. 2005. Ultrafilter extensions for coalgebras. In Proceedings of the 1st International Conference on Algebra and Coalgebra in Computer Science (CALCO'05), J. L. Fiadeiro et al. Eds. Lecture Notes in Computer Science, vol. 3629. Springer, Berlin, 263--277."},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(00)00125-0"},{"key":"e_1_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1137\/0206033"},{"key":"e_1_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1016\/0890-5401(91)90030-6"},{"key":"e_1_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.jlap.2005.09.006"},{"key":"e_1_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0004-3702(99)00011-9"},{"volume-title":"Proceedings of the 9th International Conference on Principles of Knowledge Representation and Reasoning (KR'04)","author":"Pacuit E.","key":"e_1_2_1_29_1","unstructured":"Pacuit , E. and Salame , S . 2004. Majority logic . In Proceedings of the 9th International Conference on Principles of Knowledge Representation and Reasoning (KR'04) , D. Dubois et al. Eds. AAAI Press, 598--605. Pacuit, E. and Salame, S. 2004. Majority logic. In Proceedings of the 9th International Conference on Principles of Knowledge Representation and Reasoning (KR'04), D. Dubois et al. Eds. AAAI Press, 598--605."},{"key":"e_1_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.5555\/646515.695982"},{"key":"e_1_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(03)00201-9"},{"key":"e_1_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1305\/ndjfl\/1094155277"},{"key":"e_1_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1093\/logcom\/12.1.149"},{"key":"e_1_2_1_34_1","unstructured":"Pauly M. 2005. On the role of language in social choice theory. Unpublished manuscript.  Pauly M. 2005. On the role of language in social choice theory. Unpublished manuscript."},{"key":"e_1_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0019-9958(63)90290-0"},{"volume-title":"Coalgebraic Methods in Computer Science (CMCS'00)","author":"R\u00f6\u00dfiger M.","key":"e_1_2_1_36_1","unstructured":"R\u00f6\u00dfiger , M. 2000. Coalgebras and modal logic . In Coalgebraic Methods in Computer Science (CMCS'00) , H. Reichel, Ed. Electronic Notes in Theoretical Computer Science, vol. 33 . Elsevier , Amsterdam. R\u00f6\u00dfiger, M. 2000. Coalgebras and modal logic. In Coalgebraic Methods in Computer Science (CMCS'00), H. Reichel, Ed. Electronic Notes in Theoretical Computer Science, vol. 33. Elsevier, Amsterdam."},{"key":"e_1_2_1_37_1","first-page":"175","article-title":"The Coalgebraic Class Specification Language CCSL","volume":"7","author":"Rothe J.","year":"2001","unstructured":"Rothe , J. , Tews , H. , and Jacobs , B. 2001 . The Coalgebraic Class Specification Language CCSL . J. Universal Comput. Sci. 7 , 175 -- 193 . Rothe, J., Tews, H., and Jacobs, B. 2001. The Coalgebraic Class Specification Language CCSL. J. Universal Comput. Sci. 7, 175--193.","journal-title":"J. Universal Comput. Sci."},{"volume-title":"Theory of Linear and Integer Programming","author":"Schrijver A.","key":"e_1_2_1_38_1","unstructured":"Schrijver , A. 1986. Theory of Linear and Integer Programming . John Wiley & amp; Sons, Chichester, UK. Schrijver, A. 1986. Theory of Linear and Integer Programming. John Wiley &amp; Sons, Chichester, UK."},{"key":"e_1_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.jlap.2006.11.004"},{"key":"e_1_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2007.09.023"},{"key":"e_1_2_1_41_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2006.44"},{"key":"e_1_2_1_42_1","volume-title":"Proceedings of the 34th International Colloquium on Automata, Languages and Programming (ICALP'07)","volume":"4596","author":"Schr\u00f6der L.","unstructured":"Schr\u00f6der , L. and Pattinson , D . 2007. Modular algorithms for heterogeneous modal logics . In Proceedings of the 34th International Colloquium on Automata, Languages and Programming (ICALP'07) L. Avge et al., Eds. Lecture Notes in Computer Science , vol. 4596 . Springer, Berlin, 459--471. Schr\u00f6der, L. and Pattinson, D. 2007. Modular algorithms for heterogeneous modal logics. In Proceedings of the 34th International Colloquium on Automata, Languages and Programming (ICALP'07) L. Avge et al., Eds. Lecture Notes in Computer Science, vol. 4596. Springer, Berlin, 459--471."},{"key":"e_1_2_1_43_1","doi-asserted-by":"publisher","DOI":"10.1093\/logcom\/11.1.85"},{"key":"e_1_2_1_44_1","volume-title":"Basic Proof Theory. Cambridge Tracts in Theoretical Computer Science","volume":"43","author":"Troelstra A. S.","unstructured":"Troelstra , A. S. and Schwichtenberg , H . 1996 . Basic Proof Theory. Cambridge Tracts in Theoretical Computer Science , vol. 43 . Cambridge University Press, Cambridge. Troelstra, A. S. and Schwichtenberg, H. 1996. Basic Proof Theory. Cambridge Tracts in Theoretical Computer Science, vol. 43. Cambridge University Press, Cambridge."},{"volume-title":"Proceedings of the 12th Annual IEEE Symposium on Logic in Computer Science (LICS'97)","author":"Turi D.","key":"e_1_2_1_45_1","unstructured":"Turi , D. and Plotkin , G . 1997. Towards a mathematical operational semantics . In Proceedings of the 12th Annual IEEE Symposium on Logic in Computer Science (LICS'97) . IEEE Computer Society Press, 280--291. Turi, D. and Plotkin, G. 1997. Towards a mathematical operational semantics. In Proceedings of the 12th Annual IEEE Symposium on Logic in Computer Science (LICS'97). IEEE Computer Society Press, 280--291."},{"key":"e_1_2_1_46_1","volume-title":"Proceedings of the 2nd International Symposium on Logical Foundations of Computer Science (LFCS'92)","volume":"620","author":"van der Hoek W.","unstructured":"van der Hoek , W. and Meyer , J . -J. 1992. Graded modalities in epistemic logic . In Proceedings of the 2nd International Symposium on Logical Foundations of Computer Science (LFCS'92) , A. Nerode and M. A. Taitslin, Eds. Lecture Notes in Computer Science , vol. 620 . Springer, Berlin, 503--514. van der Hoek, W. and Meyer, J.-J. 1992. Graded modalities in epistemic logic. In Proceedings of the 2nd International Symposium on Logical Foundations of Computer Science (LFCS'92), A. Nerode and M. A. Taitslin, Eds. Lecture Notes in Computer Science, vol. 620. Springer, Berlin, 503--514."},{"key":"e_1_2_1_47_1","doi-asserted-by":"publisher","DOI":"10.5555\/77350.77376"},{"key":"e_1_2_1_48_1","volume-title":"Eds. DIMACS Series. Discrete Mathematics and Theoretical Computer Science","volume":"31","author":"Vardi M. Y.","year":"1996","unstructured":"Vardi , M. Y. 1996 . Why is modal logic so robustly decidable&quest; In Proceedings of the DIMACS Workshop on Descriptive Complexity and Finite Models, N. Immerman and P. G. Kolaitis , Eds. DIMACS Series. Discrete Mathematics and Theoretical Computer Science , vol. 31 . American Mathematical Society, 149--184. Vardi, M. Y. 1996. Why is modal logic so robustly decidable&quest; In Proceedings of the DIMACS Workshop on Descriptive Complexity and Finite Models, N. Immerman and P. G. Kolaitis, Eds. DIMACS Series. Discrete Mathematics and Theoretical Computer Science, vol. 31. American Mathematical Society, 149--184."},{"key":"e_1_2_1_49_1","doi-asserted-by":"publisher","DOI":"10.5555\/1148961.1709593"}],"container-title":["ACM Transactions on Computational Logic"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1462179.1462185","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/1462179.1462185","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T13:30:15Z","timestamp":1750253415000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1462179.1462185"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2009,2]]},"references-count":49,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2009,2]]}},"alternative-id":["10.1145\/1462179.1462185"],"URL":"https:\/\/doi.org\/10.1145\/1462179.1462185","relation":{},"ISSN":["1529-3785","1557-945X"],"issn-type":[{"type":"print","value":"1529-3785"},{"type":"electronic","value":"1557-945X"}],"subject":[],"published":{"date-parts":[[2009,2]]},"assertion":[{"value":"2007-06-01","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2007-11-01","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2009-03-02","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}