{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,9,11]],"date-time":"2025-09-11T18:51:05Z","timestamp":1757616665747,"version":"3.44.0"},"publisher-location":"Cham","reference-count":36,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783030171261"},{"type":"electronic","value":"9783030171278"}],"license":[{"start":{"date-parts":[[2019,1,1]],"date-time":"2019-01-01T00:00:00Z","timestamp":1546300800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2019,4,5]],"date-time":"2019-04-05T00:00:00Z","timestamp":1554422400000},"content-version":"vor","delay-in-days":94,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2019]]},"abstract":"<jats:title>Abstract<\/jats:title>\n          <jats:p>The coalgebraic <jats:inline-formula>\n              <jats:tex-math>$$\\mu $$<\/jats:tex-math>\n            <\/jats:inline-formula>-calculus provides a generic semantic framework for fixpoint logics with branching types beyond the standard relational setup, e.g. probabilistic, weighted, or game-based. Previous work on the coalgebraic <jats:inline-formula>\n              <jats:tex-math>$$\\mu $$<\/jats:tex-math>\n            <\/jats:inline-formula>-calculus includes an exponential time upper bound on satisfiability checking, which however requires a well-behaved set of tableau rules for the next-step modalities. Such rules are not available in all cases of interest, in particular ones involving either integer weights as in the graded <jats:inline-formula>\n              <jats:tex-math>$$\\mu $$<\/jats:tex-math>\n            <\/jats:inline-formula>-calculus, or real-valued weights in combination with non-linear arithmetic. In the present work, we prove the same upper complexity bound under more general assumptions, specifically regarding the complexity of the (much simpler) satisfiability problem for the underlying <jats:italic>one-step logic<\/jats:italic>, roughly described as the nesting-free next-step fragment of the logic. The bound is realized by a generic global caching algorithm that supports on-the-fly satisfiability checking. Example applications include new exponential-time upper bounds for satisfiability checking in an extension of the graded <jats:inline-formula>\n              <jats:tex-math>$$\\mu $$<\/jats:tex-math>\n            <\/jats:inline-formula>-calculus with polynomial inequalities (including positive Presburger arithmetic), as well as an extension of the (two-valued) probabilistic <jats:inline-formula>\n              <jats:tex-math>$$\\mu $$<\/jats:tex-math>\n            <\/jats:inline-formula>-calculus with polynomial inequalities.<\/jats:p>","DOI":"10.1007\/978-3-030-17127-8_16","type":"book-chapter","created":{"date-parts":[[2019,4,5]],"date-time":"2019-04-05T11:11:46Z","timestamp":1554462706000},"page":"277-294","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":4,"title":["Optimal Satisfiability Checking for Arithmetic $$\\mu $$-Calculi"],"prefix":"10.1007","author":[{"given":"Daniel","family":"Hausmann","sequence":"first","affiliation":[]},{"given":"Lutz","family":"Schr\u00f6der","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2019,4,5]]},"reference":[{"key":"16_CR1","doi-asserted-by":"publisher","first-page":"672","DOI":"10.1145\/585265.585270","volume":"49","author":"R Alur","year":"2002","unstructured":"Alur, R., Henzinger, T., Kupferman, O.: Alternating-time temporal logic. J. ACM 49, 672\u2013713 (2002)","journal-title":"J. ACM"},{"key":"16_CR2","doi-asserted-by":"crossref","unstructured":"Bradfield, J., Stirling, C.: Modal $$\\mu $$-calculi. In: Handbook of Modal Logic, pp. 721\u2013756. Elsevier (2006)","DOI":"10.1016\/S1570-2464(07)80015-2"},{"key":"16_CR3","doi-asserted-by":"publisher","first-page":"871","DOI":"10.1007\/978-3-319-10575-8_26","volume-title":"Handbook of Model Checking","author":"J Bradfield","year":"2018","unstructured":"Bradfield, J., Walukiewicz, I.: The mu-calculus and model checking. In: Clarke, E., Henzinger, T., Veith, H., Bloem, R. (eds.) Handbook of Model Checking, pp. 871\u2013919. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-10575-8_26"},{"key":"16_CR4","first-page":"1","volume":"7","author":"C C\u00eerstea","year":"2011","unstructured":"C\u00eerstea, C., Kupke, C., Pattinson, D.: EXPTIME tableaux for the coalgebraic $$\\mu $$-calculus. Log. Methods Comput. Sci. 7, 1\u201333 (2011)","journal-title":"Log. Methods Comput. Sci."},{"key":"16_CR5","doi-asserted-by":"publisher","first-page":"316","DOI":"10.1016\/j.tcs.2005.03.048","volume":"342","author":"R Cleaveland","year":"2005","unstructured":"Cleaveland, R., Iyer, S., Narasimha, M.: Probabilistic temporal logics via the modal $$\\mu $$-calculus. Theor. Comput. Sci. 342, 316\u2013350 (2005)","journal-title":"Theor. Comput. Sci."},{"key":"16_CR6","doi-asserted-by":"publisher","first-page":"267","DOI":"10.1007\/s001530100110","volume":"41","author":"G D\u2019Agostino","year":"2002","unstructured":"D\u2019Agostino, G., Visser, A.: Finality regained: a coalgebraic study of Scott-sets and multisets. Arch. Math. Logic 41, 267\u2013298 (2002)","journal-title":"Arch. Math. Logic"},{"key":"16_CR7","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"541","DOI":"10.1007\/11814771_44","volume-title":"Automated Reasoning","author":"S Demri","year":"2006","unstructured":"Demri, S., Lugiez, D.: Presburger modal logic is PSPACE-complete. In: Furbach, U., Shankar, N. (eds.) IJCAR 2006. LNCS (LNAI), vol. 4130, pp. 541\u2013556. Springer, Heidelberg (2006). https:\/\/doi.org\/10.1007\/11814771_44"},{"key":"16_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"381","DOI":"10.1007\/978-3-642-14162-1_32","volume-title":"Automata, Languages and Programming","author":"G Fontaine","year":"2010","unstructured":"Fontaine, G., Leal, R., Venema, Y.: Automata for coalgebras: an approach using predicate liftings. In: Abramsky, S., Gavoille, C., Kirchner, C., Meyer auf der Heide, F., Spirakis, P.G. (eds.) ICALP 2010, Part II. LNCS, vol. 6199, pp. 381\u2013392. Springer, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-14162-1_32"},{"key":"16_CR9","doi-asserted-by":"publisher","first-page":"353","DOI":"10.1080\/11663081.2013.861181","volume":"23","author":"O Friedmann","year":"2013","unstructured":"Friedmann, O., Lange, M.: Deciding the unguarded modal $$\\mu $$-calculus. J. Appl. Non-Classical Log. 23, 353\u2013371 (2013)","journal-title":"J. Appl. Non-Classical Log."},{"key":"16_CR10","first-page":"1","volume":"9","author":"O Friedmann","year":"2013","unstructured":"Friedmann, O., Latte, M., Lange, M.: Satisfiability games for branching-time logics. Log. Methods Comput. Sci. 9, 1\u201336 (2013)","journal-title":"Log. Methods Comput. Sci."},{"key":"16_CR11","doi-asserted-by":"publisher","first-page":"355","DOI":"10.1007\/s10817-011-9243-0","volume":"50","author":"R Gor\u00e9","year":"2013","unstructured":"Gor\u00e9, R., Nguyen, L.A.: Exptime tableaux for ALC using sound global caching. J. Autom. Reason. 50, 355\u2013381 (2013)","journal-title":"J. Autom. Reason."},{"key":"16_CR12","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"205","DOI":"10.1007\/978-3-642-02716-1_16","volume-title":"Automated Reasoning with Analytic Tableaux and Related Methods","author":"R Gor\u00e9","year":"2009","unstructured":"Gor\u00e9, R., Widmann, F.: Sound global state caching for ALC with inverse roles. In: Giese, M., Waaler, A. (eds.) TABLEAUX 2009. LNCS (LNAI), vol. 5607, pp. 205\u2013219. Springer, Heidelberg (2009). https:\/\/doi.org\/10.1007\/978-3-642-02716-1_16"},{"key":"16_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-36387-4","volume-title":"Automata Logics, and Infinite Games: A Guide to Current Research","year":"2002","unstructured":"Gr\u00e4del, E., Thomas, W., Wilke, T. (eds.): Automata Logics, and Infinite Games: A Guide to Current Research. LNCS, vol. 2500. Springer, Heidelberg (2002). https:\/\/doi.org\/10.1007\/3-540-36387-4"},{"key":"16_CR14","doi-asserted-by":"crossref","unstructured":"Hausmann, D., Schr\u00f6der, L.: Global caching for the flat coalgebraic $$\\mu $$-calculus. In: Grandi, F., Lange, M., Lomuscio, A. (eds.) Temporal Representation and Reasoning, TIME 2015, pp. 121\u2013143. IEEE (2015)","DOI":"10.1109\/TIME.2015.15"},{"key":"16_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"361","DOI":"10.1007\/978-3-319-89963-3_21","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"D Hausmann","year":"2018","unstructured":"Hausmann, D., Schr\u00f6der, L., Deifel, H.-P.: Permutation games for the weakly aconjunctive $$\\mu $$-calculus. In: Beyer, D., Huisman, M. (eds.) TACAS 2018, Part II. LNCS, vol. 10806, pp. 361\u2013378. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-89963-3_21"},{"key":"16_CR16","unstructured":"Hausmann, D., Schr\u00f6der, L., Egger, C.: Global caching for the alternation-free coalgebraic $$\\mu $$-calculus. In: Desharnais, J., Jagadeesan, R. (eds.) Concurrency Theory, CONCUR 2016. LIPIcs, vol. 59, pp. 34:1\u201334:15. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik (2016)"},{"key":"16_CR17","doi-asserted-by":"crossref","unstructured":"Huth, M., Kwiatkowska, M.: Quantitative analysis and model checking. In: Logic in Computer Science, LICS 1997, pp. 111\u2013122. IEEE (1997)","DOI":"10.1109\/LICS.1997.614940"},{"key":"16_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"276","DOI":"10.1007\/3-540-45315-6_18","volume-title":"Foundations of Software Science and Computation Structures","author":"V King","year":"2001","unstructured":"King, V., Kupferman, O., Vardi, M.Y.: On the complexity of parity word automata. In: Honsell, F., Miculan, M. (eds.) FOSSACS 2001. LNCS, vol. 2030, pp. 276\u2013286. Springer, Heidelberg (2001). https:\/\/doi.org\/10.1007\/3-540-45315-6_18"},{"key":"16_CR19","doi-asserted-by":"publisher","first-page":"333","DOI":"10.1016\/0304-3975(82)90125-6","volume":"27","author":"D Kozen","year":"1983","unstructured":"Kozen, D.: Results on the propositional $$\\mu $$-calculus. Theor. Comput. Sci. 27, 333\u2013354 (1983)","journal-title":"Theor. Comput. Sci."},{"key":"16_CR20","doi-asserted-by":"publisher","first-page":"233","DOI":"10.1007\/BF00370554","volume":"47","author":"D Kozen","year":"1988","unstructured":"Kozen, D.: A finite model theorem for the propositional $$\\mu $$-calculus. Stud. Log. 47, 233\u2013241 (1988)","journal-title":"Stud. Log."},{"key":"16_CR21","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"423","DOI":"10.1007\/3-540-45620-1_34","volume-title":"Automated Deduction\u2014CADE-18","author":"O Kupferman","year":"2002","unstructured":"Kupferman, O., Sattler, U., Vardi, M.Y.: The complexity of the graded $${\\mu }$$-calculus. In: Voronkov, A. (ed.) CADE 2002. LNCS (LNAI), vol. 2392, pp. 423\u2013437. Springer, Heidelberg (2002). https:\/\/doi.org\/10.1007\/3-540-45620-1_34"},{"key":"16_CR22","unstructured":"Kupke, C., Pattinson, D.: On modal logics of linear inequalities. In: Beklemishev, L., Goranko, V., Shehtman, V. (eds.) Advances in Modal Logic, AiML 2010, pp. 235\u2013255. College Publications (2010)"},{"key":"16_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"367","DOI":"10.1007\/978-3-319-22177-9_28","volume-title":"Fundamentals of Computation Theory","author":"C Kupke","year":"2015","unstructured":"Kupke, C., Pattinson, D., Schr\u00f6der, L.: Reasoning with global assumptions in arithmetic modal logics. In: Kosowski, A., Walukiewicz, I. (eds.) FCT 2015. LNCS, vol. 9210, pp. 367\u2013380. Springer, Cham (2015). https:\/\/doi.org\/10.1007\/978-3-319-22177-9_28"},{"key":"16_CR24","unstructured":"Liu, W., Song, L., Wang, J., Zhang, L.: A simple probabilistic extension of modal mu-calculus. In: Yang, Q., Wooldridge, M. (eds.) International Joint Conference on Artificial Intelligence, IJCAI 2015, pp. 882\u2013888. AAAI Press (2015)"},{"key":"16_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"290","DOI":"10.1007\/978-3-642-19805-2_20","volume-title":"Foundations of Software Science and Computational Structures","author":"M Mio","year":"2011","unstructured":"Mio, M.: Probabilistic modal $${\\mu }$$-calculus with independent product. In: Hofmann, M. (ed.) FOSSACS 2011. LNCS, vol. 6604, pp. 290\u2013304. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-19805-2_20"},{"key":"16_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"137","DOI":"10.1007\/978-3-642-00596-1_11","volume-title":"Foundations of Software Science and Computational Structures","author":"R Myers","year":"2009","unstructured":"Myers, R., Pattinson, D., Schr\u00f6der, L.: Coalgebraic hybrid logic. In: de Alfaro, L. (ed.) FOSSACS 2009. LNCS, vol. 5504, pp. 137\u2013151. Springer, Heidelberg (2009). https:\/\/doi.org\/10.1007\/978-3-642-00596-1_11"},{"key":"16_CR27","doi-asserted-by":"publisher","first-page":"99","DOI":"10.1016\/0304-3975(95)00136-0","volume":"163","author":"D Niwinski","year":"1996","unstructured":"Niwinski, D., Walukiewicz, I.: Games for the $$\\mu $$-calculus. Theor. Comput. Sci. 163, 99\u2013116 (1996)","journal-title":"Theor. Comput. Sci."},{"key":"16_CR28","first-page":"111","volume":"24","author":"R Parikh","year":"1985","unstructured":"Parikh, R.: The logic of games and its applications. Ann. Discret. Math. 24, 111\u2013140 (1985)","journal-title":"Ann. Discret. Math."},{"key":"16_CR29","doi-asserted-by":"publisher","first-page":"177","DOI":"10.1016\/S0304-3975(03)00201-9","volume":"309","author":"D Pattinson","year":"2003","unstructured":"Pattinson, D.: Coalgebraic modal logic: soundness, completeness and decidability of local consequence. Theor. Comput. Sci. 309, 177\u2013193 (2003)","journal-title":"Theor. Comput. Sci."},{"issue":"3:5","key":"16_CR30","first-page":"1","volume":"3","author":"N Piterman","year":"2007","unstructured":"Piterman, N.: From nondeterministic B\u00fcchi and Streett automata to deterministic parity automata. Log. Methods Comput. Sci. 3(3:5), 1\u201321 (2007)","journal-title":"Log. Methods Comput. Sci."},{"key":"16_CR31","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1016\/S0304-3975(00)00056-6","volume":"249","author":"J Rutten","year":"2000","unstructured":"Rutten, J.: Universal coalgebra: a theory of systems. Theor. Comput. Sci. 249, 3\u201380 (2000)","journal-title":"Theor. Comput. Sci."},{"key":"16_CR32","doi-asserted-by":"crossref","unstructured":"Safra, S.: On the complexity of omega-automata. In: Foundations of Computer Science, FOCS 1988, pp. 319\u2013327. IEEE Computer Society (1988)","DOI":"10.1109\/SFCS.1988.21948"},{"key":"16_CR33","doi-asserted-by":"publisher","first-page":"97","DOI":"10.1016\/j.jlap.2006.11.004","volume":"73","author":"L Schr\u00f6der","year":"2007","unstructured":"Schr\u00f6der, L.: A finite model construction for coalgebraic modal logic. J. Log. Algebr. Prog. 73, 97\u2013110 (2007)","journal-title":"J. Log. Algebr. Prog."},{"issue":"2\u20133","key":"16_CR34","doi-asserted-by":"publisher","first-page":"230","DOI":"10.1016\/j.tcs.2007.09.023","volume":"390","author":"L Schr\u00f6der","year":"2008","unstructured":"Schr\u00f6der, L.: Expressivity of coalgebraic modal logic: the limits and beyond. Theor. Comput. Sci. 390(2\u20133), 230\u2013247 (2008)","journal-title":"Theor. Comput. Sci."},{"key":"16_CR35","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"324","DOI":"10.1007\/978-3-540-85845-4_40","volume-title":"KI 2008: Advances in Artificial Intelligence","author":"L Schr\u00f6der","year":"2008","unstructured":"Schr\u00f6der, L., Pattinson, D.: Shallow models for non-iterative modal logics. In: Dengel, A.R., Berns, K., Breuel, T.M., Bomarius, F., Roth-Berghofer, T.R. (eds.) KI 2008. LNCS (LNAI), vol. 5243, pp. 324\u2013331. Springer, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-85845-4_40"},{"issue":"2","key":"16_CR36","doi-asserted-by":"publisher","first-page":"13:1","DOI":"10.1145\/1462179.1462185","volume":"10","author":"L Schr\u00f6der","year":"2009","unstructured":"Schr\u00f6der, L., Pattinson, D.: PSPACE bounds for rank-1 modal logics. ACM Trans. Comput. Log. 10(2), 13:1\u201313:33 (2009)","journal-title":"ACM Trans. Comput. Log."}],"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-17127-8_16","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,9,5]],"date-time":"2025-09-05T19:29:05Z","timestamp":1757100545000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-030-17127-8_16"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019]]},"ISBN":["9783030171261","9783030171278"],"references-count":36,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-17127-8_16","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2019]]},"assertion":[{"value":"5 April 2019","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":"Prague","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Czech Republic","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2019","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"8 April 2019","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"11 April 2019","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"22","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"fossacs2019","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/www.etaps.org\/2019\/fossacs","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}