{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,10]],"date-time":"2025-10-10T07:03:17Z","timestamp":1760079797004,"version":"3.41.2"},"reference-count":27,"publisher":"Centre pour la Communication Scientifique Directe (CCSD)","license":[{"start":{"date-parts":[[2011,8,11]],"date-time":"2011-08-11T00:00:00Z","timestamp":1313020800000},"content-version":"unspecified","delay-in-days":0,"URL":"https:\/\/arxiv.org\/licenses\/nonexclusive-distrib\/1.0"}],"funder":[{"DOI":"10.13039\/100014013","name":"UK Research and Innovation","doi-asserted-by":"crossref","award":["EP\/F031173\/1"],"award-info":[{"award-number":["EP\/F031173\/1"]}],"id":[{"id":"10.13039\/100014013","id-type":"DOI","asserted-by":"crossref"}]}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"abstract":"<jats:p>The coalgebraic approach to modal logic provides a uniform framework that captures the semantics of a large class of structurally different modal logics, including e.g. graded and probabilistic modal logics and coalition logic. In this paper, we introduce the coalgebraic mu-calculus, an extension of the general (coalgebraic) framework with fixpoint operators. Our main results are completeness of the associated tableau calculus and EXPTIME decidability for guarded formulas. Technically, this is achieved by reducing satisfiability to the existence of non-wellfounded tableaux, which is in turn equivalent to the existence of winning strategies in parity games. Our results are parametric in the underlying class of models and yield, as concrete applications, previously unknown complexity bounds for the probabilistic mu-calculus and for an extension of coalition logic with fixpoints.<\/jats:p>","DOI":"10.2168\/lmcs-7(3:3)2011","type":"journal-article","created":{"date-parts":[[2014,11,14]],"date-time":"2014-11-14T13:45:24Z","timestamp":1415972724000},"source":"Crossref","is-referenced-by-count":11,"title":["EXPTIME Tableaux for the Coalgebraic mu-Calculus"],"prefix":"10.46298","volume":"Volume 7, Issue 3","author":[{"given":"Corina","family":"Cirstea","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Clemens","family":"Kupke","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Dirk","family":"Pattinson","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"25203","published-online":{"date-parts":[[2011,8,11]]},"reference":[{"key":"10.2168\/LMCS-7(3:3)2011_Bradfield:1996:EMM","doi-asserted-by":"crossref","unstructured":"J. C. Bradfield. On the expressivity of the modal mu-calculus. In C. Puech and R. Reischuk, editors,Proc. STACS 1996, volume 1046 ofLecture Notes in Computer Science, pages 479-490. Springer, 1996.","DOI":"10.1007\/3-540-60922-9_39"},{"key":"10.2168\/LMCS-7(3:3)2011_Chellas:1980:ML","doi-asserted-by":"crossref","unstructured":"B. Chellas.Modal Logic. Cambridge, 1980.","DOI":"10.1017\/CBO9780511621192"},{"key":"10.2168\/LMCS-7(3:3)2011_Cirstea:2004:CAD","doi-asserted-by":"crossref","first-page":"45","DOI":"10.1016\/j.tcs.2004.07.021","volume":"327","author":"C. Cirstea","year":"2004","journal-title":"Theoret. Comput. Sci."},{"key":"10.2168\/LMCS-7(3:3)2011_cikupa:expt09","doi-asserted-by":"crossref","unstructured":"C. Cirstea, C. Kupke, and D. Pattinson. EXPTIME tableaux for the coalgebraic\u00ce\u00bc-calculus. InProceeding of Computer Science Logic, CSL 09, volume 5771 ofLNCS, pages 179-193, 2009.","DOI":"10.1007\/978-3-642-04027-6_15"},{"key":"10.2168\/LMCS-7(3:3)2011_Cirstea:2007:MPS","doi-asserted-by":"crossref","first-page":"83","DOI":"10.1016\/j.tcs.2007.06.002","volume":"388","author":"C. Cirstea and D. Pattinson","year":"2007","journal-title":"Theoretical Computer Science"},{"key":"10.2168\/LMCS-7(3:3)2011_Cirstea:2008:CMCS","doi-asserted-by":"crossref","unstructured":"C. Cirstea and M. Sadrzadeh. Modular Games for Coalgebraic Fixed Point Logics. In J. Ad\u00e1mek and C. Kupke, editors,Coalgebraic Methods in Computer Science (CMCS'2008), volume 203 ofENTCS, 2008.","DOI":"10.1016\/j.entcs.2008.05.020"},{"key":"10.2168\/LMCS-7(3:3)2011_Emerson:1988:CTA","doi-asserted-by":"crossref","unstructured":"E. Emerson and C. Jutla. The complexity of tree automata and logics of programs. InProc. FOCS 1988, pages 328-337. IEEE, 1988.","DOI":"10.1109\/SFCS.1988.21949"},{"key":"10.2168\/LMCS-7(3:3)2011_emer:tree91","doi-asserted-by":"crossref","unstructured":"E. Emerson and C. Jutla. Tree automata, mu-calculus and determinacy. InProceedings of the 32nd IEEE Symposium on Foundations of Computer Science (FoCS'91), pages 368-377. IEEE Computer Society Press, 1991.","DOI":"10.1109\/SFCS.1991.185392"},{"issue":"1","key":"10.2168\/LMCS-7(3:3)2011_Emerson:1999:CTA","doi-asserted-by":"crossref","first-page":"132","DOI":"10.1137\/S0097539793304741","volume":"29","author":"E. A. Emerson and C. S. Jutla","year":"1999","journal-title":"SIAM J. Comput."},{"key":"10.2168\/LMCS-7(3:3)2011_Fine:1972:MPW","doi-asserted-by":"crossref","first-page":"516","DOI":"10.1305\/ndjfl\/1093890715","volume":"13","author":"K. Fine","year":"1972","journal-title":"Notre Dame J. Formal Logic"},{"key":"10.2168\/LMCS-7(3:3)2011_frla:them11","doi-asserted-by":"crossref","unstructured":"O. Friedmann and M. Lange. The modal\u00ce\u00bc-calculus caught off guard. InProceedings of the 20th International Conference on Automated Reasoning with Analytic Tableaux and Related Methods (TABLEAUX), 2011. To appear.","DOI":"10.1007\/978-3-642-22119-4_13"},{"key":"10.2168\/LMCS-7(3:3)2011_Hansen:2004:CPM","doi-asserted-by":"crossref","unstructured":"H. H. Hansen and C. Kupke. A coalgebraic perspective on monotone modal logic. In J. Ad\u00e1mek and S. Milius, editors,Coalgebraic Methods in Computer Science, volume 106 ofENTCS, pages 121-143. Elsevier, 2004.","DOI":"10.1016\/j.entcs.2004.02.028"},{"key":"10.2168\/LMCS-7(3:3)2011_jurd:small00","doi-asserted-by":"crossref","unstructured":"M. Jurdzi\u00cc\u00a4ski. Small Progress Measures for Solving Parity Games. InProceedings of the 17th Annual Symposium on Theoretical Aspects of Computer Science, STACS, volume 1770 ofLNCS, pages 290-301, 2000.","DOI":"10.1007\/3-540-46541-3_24"},{"key":"10.2168\/LMCS-7(3:3)2011_Kozen:1983:RPC","doi-asserted-by":"crossref","first-page":"333","DOI":"10.1016\/0304-3975(82)90125-6","volume":"27","author":"D. Kozen","year":"1983","journal-title":"Theoret. Comput. Sci."},{"issue":"2","key":"10.2168\/LMCS-7(3:3)2011_Kupferman:2000:ATA","doi-asserted-by":"crossref","first-page":"312","DOI":"10.1145\/333979.333987","volume":"47","author":"O. Kupferman, M. Vardi, and P. Wolper","year":"2000","journal-title":"Journal of the ACM"},{"key":"10.2168\/LMCS-7(3:3)2011_most:game91","unstructured":"A. Mostowski. Games with forbidden positions. Technical Report 78, Instytut Matematyki, Uniwersytet Gda\u00cc\u00a4ski, Poland, 1991."},{"issue":"1+2","key":"10.2168\/LMCS-7(3:3)2011_Niwinski:1996:GMC","first-page":"99","volume":"163","author":"D. Niwinski and I. Walukiewicz","year":"1996","journal-title":"Theor. Comput. Sci."},{"issue":"1","key":"10.2168\/LMCS-7(3:3)2011_Pauly:2002:MLC","doi-asserted-by":"crossref","first-page":"149","DOI":"10.1093\/logcom\/12.1.149","volume":"12","author":"M. Pauly","year":"2002","journal-title":"J. Logic Comput."},{"key":"10.2168\/LMCS-7(3:3)2011_pite:nond06","doi-asserted-by":"crossref","unstructured":"N. Piterman. From nondeterministic B\u00fcchi and Streett automata to deterministic parity automata. InProceedings of the Twentyfirst Annual IEEE Symposium on Logic in Computer Science (LICS 2006), pages 255-264. IEEE Computer Society, 2006.","DOI":"10.1109\/LICS.2006.28"},{"key":"10.2168\/LMCS-7(3:3)2011_safr:onth88","doi-asserted-by":"crossref","unstructured":"S. Safra. On the complexity of\u00f8mega-automata. InProc. 29th IEEE Symposium on the Foundations of Computer Science, pages 319-327, 1988.","DOI":"10.1109\/SFCS.1988.21948"},{"key":"10.2168\/LMCS-7(3:3)2011_Kupferman:2002:CGM","doi-asserted-by":"crossref","unstructured":"U. Sattler, O. Kupferman, and M. Y. Vardi. The complexity of the graded mu-calculus. InProc. CADE 2002, volume 2392 ofLNCS, pages 423-437. Springer, 2002.","DOI":"10.1007\/3-540-45620-1_34"},{"key":"10.2168\/LMCS-7(3:3)2011_Schroder:2006:FMC","doi-asserted-by":"crossref","unstructured":"L. Schr\u00f6der. A finite model construction for coalgebraic modal logic. In L. Aceto and A. Ing\u00f3lfsd\u00f3ttir, editors,Foundations Of Software Science And Computation Structures, volume 3921 ofLNCS, pages 157-171. Springer, 2006.","DOI":"10.1007\/11690634_11"},{"key":"10.2168\/LMCS-7(3:3)2011_Schroder:2007:CAH","unstructured":"L. Schr\u00f6der and D. Pattinson. Compositional algorithms for heterogeneous modal logics. InProc. ICALP 2007, LNCS, 2007."},{"key":"10.2168\/LMCS-7(3:3)2011_Schroder:2008:PBR","doi-asserted-by":"crossref","unstructured":"L. Schr\u00f6der and D. Pattinson. PSPACE bounds for rank-1 modal logics.ACM Trans. Compl Log., 2(10), 2008. to appear.","DOI":"10.1145\/1462179.1462185"},{"key":"10.2168\/LMCS-7(3:3)2011_Stirling:2001:MTP","doi-asserted-by":"crossref","unstructured":"C. Stirling.Modal and Temporal Properties of Processes. Texts in Computer Science. Springer, 2001.","DOI":"10.1007\/978-1-4757-3550-5"},{"issue":"4","key":"10.2168\/LMCS-7(3:3)2011_Venema:2006:AFP","doi-asserted-by":"crossref","first-page":"637","DOI":"10.1016\/j.ic.2005.06.003","volume":"204","author":"Y. Venema","year":"2006","journal-title":"Inform. Comput."},{"issue":"1-2","key":"10.2168\/LMCS-7(3:3)2011_Walukiewicz:2000:CKA","doi-asserted-by":"crossref","first-page":"142","DOI":"10.1006\/inco.1999.2836","volume":"157","author":"I. Walukiewicz","year":"2000","journal-title":"Inf. Comput."}],"container-title":["Logical Methods in Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/lmcs.episciences.org\/784\/pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/lmcs.episciences.org\/784\/pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,5,13]],"date-time":"2025-05-13T18:03:13Z","timestamp":1747159393000},"score":1,"resource":{"primary":{"URL":"https:\/\/lmcs.episciences.org\/784"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2011,8,11]]},"references-count":27,"URL":"https:\/\/doi.org\/10.2168\/lmcs-7(3:3)2011","relation":{"is-same-as":[{"id-type":"arxiv","id":"1105.2246","asserted-by":"subject"},{"id-type":"doi","id":"10.48550\/arXiv.1105.2246","asserted-by":"subject"}]},"ISSN":["1860-5974"],"issn-type":[{"type":"electronic","value":"1860-5974"}],"subject":[],"published":{"date-parts":[[2011,8,11]]},"article-number":"784"}}