{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,7,30]],"date-time":"2025-07-30T16:53:25Z","timestamp":1753894405127,"version":"3.41.2"},"reference-count":0,"publisher":"Centre pour la Communication Scientifique Directe (CCSD)","license":[{"start":{"date-parts":[[2024,7,23]],"date-time":"2024-07-23T00:00:00Z","timestamp":1721692800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"abstract":"<jats:p>The coalgebraic $\\mu$-calculus provides a generic semantic framework for\nfixpoint logics over systems whose branching type goes beyond the standard\nrelational setup, e.g. probabilistic, weighted, or game-based. Previous work on\nthe coalgebraic $\\mu$-calculus includes an exponential-time upper bound on\nsatisfiability checking, which however relies on the availability of tableau\nrules for the next-step modalities that are sufficiently well-behaved in a\nformally defined sense; in particular, rule matches need to be representable by\npolynomial-sized codes, and the sequent duals of the rules need to absorb cut.\nWhile such rule sets have been identified for some important cases, they are\nnot known to exist in all cases of interest, in particular ones involving\neither integer weights as in the graded $\\mu$-calculus, or real-valued weights\nin combination with non-linear arithmetic. In the present work, we prove the\nsame upper complexity bound under more general assumptions, specifically\nregarding the complexity of the (much simpler) satisfiability problem for the\nunderlying one-step logic, roughly described as the nesting-free next-step\nfragment of the logic. The bound is realized by a generic global caching\nalgorithm that supports on-the-fly satisfiability checking. Notably, our\napproach directly accommodates unguarded formulae, and thus avoids use of the\nguardedness transformation. Example applications include new exponential-time\nupper bounds for satisfiability checking in an extension of the graded\n$\\mu$-calculus with polynomial inequalities (including positive Presburger\narithmetic), as well as an extension of the (two-valued) probabilistic\n$\\mu$-calculus with polynomial inequalities.<\/jats:p>","DOI":"10.46298\/lmcs-20(3:9)2024","type":"journal-article","created":{"date-parts":[[2024,7,23]],"date-time":"2024-07-23T11:10:12Z","timestamp":1721733012000},"source":"Crossref","is-referenced-by-count":0,"title":["Coalgebraic Satisfiability Checking for Arithmetic $\\mu$-Calculi"],"prefix":"10.46298","volume":"Volume 20, Issue 3","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-0935-8602","authenticated-orcid":false,"given":"Daniel","family":"Hausmann","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-3146-5906","authenticated-orcid":false,"given":"Lutz","family":"Schr\u00f6der","sequence":"additional","affiliation":[]}],"member":"25203","published-online":{"date-parts":[[2024,7,23]]},"container-title":["Logical Methods in Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/lmcs.episciences.org\/13967\/pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/lmcs.episciences.org\/13967\/pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,7,24]],"date-time":"2024-07-24T07:15:39Z","timestamp":1721805339000},"score":1,"resource":{"primary":{"URL":"https:\/\/lmcs.episciences.org\/10532"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,7,23]]},"references-count":0,"URL":"https:\/\/doi.org\/10.46298\/lmcs-20(3:9)2024","relation":{"has-preprint":[{"id-type":"arxiv","id":"2212.11055v3","asserted-by":"subject"},{"id-type":"arxiv","id":"2212.11055v2","asserted-by":"subject"},{"id-type":"arxiv","id":"2212.11055v1","asserted-by":"subject"}],"is-same-as":[{"id-type":"arxiv","id":"2212.11055","asserted-by":"subject"},{"id-type":"doi","id":"10.48550\/arXiv.2212.11055","asserted-by":"subject"}]},"ISSN":["1860-5974"],"issn-type":[{"type":"electronic","value":"1860-5974"}],"subject":[],"published":{"date-parts":[[2024,7,23]]},"article-number":"10532"}}