Hausmann D, Schröder L (2019)

**Publication Type:** Conference contribution

**Publication year:** 2019

**Publisher:** Springer Verlag

**Book Volume:** 11425 LNCS

**Pages Range:** 277-294

**DOI:** 10.1007/978-3-030-17127-8_16

The coalgebraic -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 -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 -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 one-step logic, 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 -calculus with polynomial inequalities (including positive Presburger arithmetic), as well as an extension of the (two-valued) probabilistic -calculus with polynomial inequalities.

Daniel Hausmann
Lehrstuhl für Informatik 8 (Theoretische Informatik)
Lutz Schröder
Lehrstuhl für Informatik 8 (Theoretische Informatik)

**APA:**

Hausmann, D., & Schröder, L. (2019). Optimal Satisfiability Checking for Arithmetic µ-Calculi. In Mikolaj Bojanczyk, Alex Simpson (Eds.), *Proceedings of the 22nd International Conference on Foundations of Software Science and Computation Structures, FoSSaCS 2019* (pp. 277-294). Springer Verlag.

**MLA:**

Hausmann, Daniel, and Lutz Schröder. "Optimal Satisfiability Checking for Arithmetic µ-Calculi." *Proceedings of the 22nd International Conference on Foundations of Software Science and Computation Structures, FoSSaCS 2019* Ed. Mikolaj Bojanczyk, Alex Simpson, Springer Verlag, 2019. 277-294.

**BibTeX:** Download