Optimal Satisfiability Checking for Arithmetic \(\mu \)Calculi
Abstract
The coalgebraic \(\mu \)calculus provides a generic semantic framework for fixpoint logics with branching types beyond the standard relational setup, e.g. probabilistic, weighted, or gamebased. Previous work on the coalgebraic \(\mu \)calculus includes an exponential time upper bound on satisfiability checking, which however requires a wellbehaved set of tableau rules for the nextstep modalities. Such rules are not available in all cases of interest, in particular ones involving either integer weights as in the graded \(\mu \)calculus, or realvalued weights in combination with nonlinear 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 onestep logic, roughly described as the nestingfree nextstep fragment of the logic. The bound is realized by a generic global caching algorithm that supports onthefly satisfiability checking. Example applications include new exponentialtime upper bounds for satisfiability checking in an extension of the graded \(\mu \)calculus with polynomial inequalities (including positive Presburger arithmetic), as well as an extension of the (twovalued) probabilistic \(\mu \)calculus with polynomial inequalities.
1 Introduction
Modal fixpoint logics are a wellestablished tool in the temporal specification, verification, and analysis of concurrent systems. One of the most expressive logics of this type is the modal \(\mu \)calculus [2, 3, 20], which features explicit least and greatest fixpoint operators; roughly speaking, these serve to specify liveness properties (least fixpoints) and safety properties (greatest fixpoints), respectively. Like most modal logics, the modal \(\mu \)calculus is traditionally interpreted over relational models such as Kripke frames or labelled transition systems. The growing interest in more expressive models where transitions are governed, e.g., by probabilities, weights, or games has sparked a commensurate growth of temporal logics and fixpoint logics interpreted over such systems; prominent examples include probabilistic \(\mu \)calculi [5, 17, 24], the alternatingtime \(\mu \)calculus [1], and the monotone \(\mu \)calculus, which contains Parikh’s game logic [28]. The graded \(\mu \)calculus [21] features nextstep modalities that count successors; it is standardly interpreted over Kripke frames but, as pointed out by D’Agostino and Visser [6], graded modalities are more naturally interpreted over socalled multigraphs, where edges carry integer weights, and in fact this modification leads to better bounds on minimum model size for satisfiable formulas.
Coalgebraic logic [29, 34] has emerged as a unifying framework for modal logics interpreted over such more general models. It is based on casting the transition type of the systems at hand as a set functor, and the systems in question as coalgebras for this type functor, following the paradigm of universal coalgebra [31]; additionally, modalities are interpreted as socalled predicate liftings. The coalgebraic \(\mu \)calculus [4] caters for fixpoint logics within this framework, and essentially covers all mentioned (twovalued) examples as instances. It has been shown that satisfiability checking in a coalgebraic \(\mu \)calculus is in \(\textsc {ExpTime}\), provided that one exhibits a set of tableau rules for the modalities, socalled onestep rules, that is tractable in a suitable sense (an assumption made also in our own previous work on the flat [14] and alternationfree [16] fragments of the coalgebraic \(\mu \)calculus). Such rules are known for many important cases, notably including alternatingtime logics, the probabilistic \(\mu \)calculus even when extended with linear inequalities, and game logic [4, 22, 36]. There are, however, important cases where such rule sets are currently missing, and where there is in fact little perspective for finding suitable rules. One prominent case of this kind is graded modal logic; further cases arise when logics over systems with nonnegative real weights, such as probabilistic systems, are taken beyond linear arithmetic to include polynomial inequalities.
The object of the current paper is to fill this gap by proving a generic \(\textsc {ExpTime}\) upper bound for coalgebraic \(\mu \)calculi in the absence of tractable sets of modal tableau rules. The method we use instead is to analyse the socalled onestep satisfiability problem of the logic on a semantic level – this problem is essentially the satisfiability problem of a very small fragment of the logic, the onestep logic, which excludes not only fixpoints, but also nested nextstep modalities, with a correspondingly simplified semantics that no longer involves actual transitions. E.g. the onestep logic of the relational \(\mu \)calculus is interpreted over models essentially consisting of a set with a distinguished subset, abstracting the successors of a single state that is not itself part of the model. We have applied this principle to satisfiability checking in coalgebraic (nextstep) modal logics [35], coalgebraic hybrid logics [26], and reasoning with global assumptions in coalgebraic modal logics [23]. It also appears implicitly in work on automata for the coalgebraic \(\mu \)calculus [8], which however establishes only a doubly exponential upper bound in the case without tractable modal tableau rules.
Our main example applications are on the one hand the graded modal \(\mu \)calculus and its extension with (monotone) polynomial inequalities, including Presburger modalities, i.e. (monotone) linear inequalities, and on the other hand the extension of the (twovalued) probabilistic \(\mu \)calculus [4, 24] with (monotone) polynomial inequalities. While the graded \(\mu \)calculus as such is known to be in \(\textsc {ExpTime}\) [21], the other mentioned instances of our result are, to our best knowledge, new. At the same time, our proofs are fairly simple, even compared to specific ones, e.g. for the graded \(\mu \)calculus.
Technically, we base our results on an automatatheoretic treatment by means of standard parity automata with singly exponential branching degree (in particular on modal steps), thus precisely enabling the singly exponential upper bound, in contrast to previous work in [8] where the introduced \(\varLambda \)automata lead to doubly exponential branching on modal steps in the resulting satisfiability games. Our algorithm witnessing the singly exponential time bound is, in fact, a global caching algorithm [11, 12], and is able to decide the satisfiability of nodes onthefly, that is, possibly before the tableau is fully expanded, thus offering a perspective for practically feasible reasoning. A side result of our approach is a criterion for a polynomial bound on branching in models, which holds in all our examples.
Organization. In Sect. 2, we recall the basics of the coalgebraic \(\mu \)calculus. We outline our automatatheoretic approach in Sect. 3, and present the global caching algorithm and its runtime analysis in Sect. 4. Soundness and completeness of the algorithm are proved in Sect. 5.
2 The Coalgebraic \(\mu \)Calculus
We recall basic definitions in coalgebraic logic [29, 34] and the coalgebraic \(\mu \)calculus [4].
Semantics. As indicated above, the branching type of the underlying systems is a parameter of the framework, given by fixing a \(\mathbf {Set}\)endofunctor T. Elements of TU should be thought of as structured collections over U that serve as collections of successors of states – e.g. in the most basic example, classical relational systems, T is powerset \(\mathcal {P}\). Formulas are then interpreted over Tcoalgebras \((C,\xi )\) consisting of a set C of states and a transition function \(\xi :C\rightarrow TC\) that assigns a structured collection \(\xi (x)\in TC\) of successors (and observations) to \(x\in C\); e.g. \(\mathcal {P}\)coalgebras are just Kripke frames, as they assign a set of successors to each state. We interpret each modal operator \(\heartsuit \in \varLambda \) as a Tpredicate lifting \([\![\heartsuit ]\!]\), that is, a natural transformation \([\![\heartsuit ]\!]:\mathcal {Q}\rightarrow \mathcal {Q}\circ T^{ op }\) where \(\mathcal {Q}:\mathbf {Set}^{ op }\rightarrow \mathbf {Set}\) denotes the contravariant powerset functor. Predicate liftings thus are families of functions \([\![\heartsuit ]\!]_U:\mathcal {Q}(U)\rightarrow \mathcal {Q}(TU)\) satisfying naturality, i.e. \([\![\heartsuit ]\!]_U(f^{1}[A])= (T f)^{1}[[\![\heartsuit ]\!]_V(A)]\) for \(f:U\rightarrow V\) and \(A\subseteq V\), where \(f^{1}\) denotes preimage. E.g. the standard relational box modality is interpreted by \([\![\Box ]\!]_U(A)=\{B\in \mathcal {P}(U)\mid B\subseteq A\}\). For sets \(U\subseteq V\), we write \(\overline{U}=V\setminus U\) for the complement of U in V when V is understood from the context. We require that duality of modal operators is respected, i.e. \([\![\heartsuit ]\!]_U(A)=\overline{[\![\overline{\heartsuit }]\!]_U\overline{A}}\) for \(A\subseteq U\). To ensure existence of fixpoints, we require that all \([\![\heartsuit ]\!]\) are monotone, i.e. \(A\subseteq B\subseteq U\) implies \([\![\heartsuit ]\!]_U(A)\subseteq [\![\heartsuit ]\!]_U(B)\).
Example 1
We now detail several instances of the coalgebraic \(\mu \)calculus; for further examples, e.g. the alternatingtime \(\mu \)calculus, see [4].
 1.To obtain the standard modal \(\mu \)calculus [19] (which contains CTL as a fragment), we take \(\varLambda =\{\Diamond , \Box \}\cup P\) where P is a set of propositional atoms, seen as nullary modalities. The semantics is captured by \(TU=\mathcal {P}(U)\times \mathcal {P}(P)\), so that Tcoalgebras are Kripke models, as they assign to each state a set of successors and a set of atoms satisfied in the state. The relevant predicate liftings areand \([\![p]\!]_U=\{(B,Q)\in TU\mid p\in Q\}\), a nullary predicate lifting. Standard example formulas include the CTLformula \(\mathsf {AF}\,p=\mu X.\,(p\vee \Box X)\), which states that on all paths, p eventually holds, and the fairness formula \(\nu X.\,\mu Y.\, ((p\wedge \Diamond X)\vee \Diamond Y)\), which asserts the existence of a path on which p holds infinitely often.$$\begin{aligned}{}[\![\Diamond ]\!]_U(A)&=\{(B,Q)\in TU\mid A\cap B\ne \emptyset \}&[\![\Box ]\!]_U(A)&=\{(B,Q)\in TU\mid B\subseteq A\} \end{aligned}$$
 2.We interpret the graded \(\mu \)calculus [21] over multigraphs [6], i.e. Tcoalgebras for the multiset functor \(T=\mathcal {B}\), defined byfor sets U, V and functions \(f:U\rightarrow V\), \(\theta :U\rightarrow \mathbb {N}\cup \{\infty \}\). Thus \(\mathcal {B}\)coalgebras \((C,\xi )\) assign multisets \(\xi (x)\) to states \(x\in C\), with the intuition that x has \(y\in C\) as successor with multiplicity m if \(\xi (x)(y)=m\). We use the modal similarity type \(\varLambda =\{\langle m\rangle ,[m]\mid m\in \mathbb {N}\cup \{\infty \}\}\) and define the predicate liftings$$\begin{aligned} \mathcal {B}(U)&=\{\theta :U\rightarrow \mathbb {N}\cup \{\infty \}\}&\mathcal {B}(f)(\theta )(v)&=\textstyle \sum _{u\in U\mid f(u)=v}\theta (u) \end{aligned}$$for sets U and \(A\subseteq U\), where \(\theta (A)=\sum _{a\in A} \theta (a)\). E.g. a state satisfies \(\nu X.\,(\psi \wedge \langle 1 \rangle X)\) if it is the root of an infinite binary tree in which \(\psi \) is satisfied globally.$$\begin{aligned}{}[\![\langle m\rangle ]\!]_U(A)&=\{\theta \in \mathcal {B}(U)\mid \theta (A)>m\}&[\![[m]]\!]_U(A)&=\{\theta \in \mathcal {B}(U)\mid \theta (\overline{A})\le m\} \end{aligned}$$
 3.Similarly, the twovalued probabilistic \(\mu \)calculus [4, 24] is obtained by using the distribution functor \(T=\mathcal {D}\) that maps sets U to probability distributions over U with countable support, defined byThen Tcoalgebras are just Markov chains. We use the modal similarity type \(\varLambda =\{\langle p\rangle ,[p]\mid p\in \mathbb {Q}\cap [0,1]\}\) and define the predicate liftings$$\begin{aligned} \mathcal {D}(U)=\{d:U\rightarrow (\mathbb {Q}\cap [0,1])\mid \textstyle \sum \nolimits _{u\in U} d(u)=1\}. \end{aligned}$$for sets U and \(A\subseteq U\), where again \(d(A)=\sum _{a\in A} d(a)\).$$\begin{aligned}{}[\![\langle p\rangle ]\!]_U(A)&=\{d\in \mathcal {D}(U)\mid d(A)>p\}&[\![[p]]\!]_U(A)&=\{d\in \mathcal {D}(U)\mid d(\overline{A})\le p\}, \end{aligned}$$
 4.We interpret the graded \(\mu \)calculus with polynomial inequalities over the semantic domain from item 2 (i.e. multigraphs). We put \(\varLambda =\{L_{p,b},M_{p,b}\mid p\in \mathbb {N}_{>0}[X_1,\ldots ,X_n],b,n\in \mathbb {N}\}\) (that is, p ranges over multivariate polynomials with positive integer coefficients) and define the predicate liftingsfor sets U and \(A_1,\ldots ,A_n\subseteq U\), where \(\theta (A)=\textstyle \sum _{a\in A} \theta (a)\). This logic subsumes the Presburger \(\mu \)calculus, that is, the extension of the graded \(\mu \)calculus with (monotone) linear inequalities, which may be seen as the fixpoint variant of Presburger modal logic [7]. E.g. the formula \(\mu Y.\,(r\vee L_{2X_1+X_2^2,2}(p\wedge Y,q\wedge Y))\) says that the current state is the root of a finite tree all whose leaves satisfy r, and each of whose inner nodes has \(n_1\) children satisfying p and \(n_2\) children satisfying q where \(2n_1+n_2^2>2\). One sees an apparent coding of the logic into the graded \(\mu \)calculus, which however incurs exponential blowup.$$\begin{aligned}{}[\![L_{p, b}]\!]_U(A_1,\ldots ,A_n)&=\{\theta \in \mathcal {B}(U)\mid p(\theta (A_1),\ldots ,\theta (A_n))>b)\}\\ [\![M_{p, b}]\!]_U(A_1,\ldots ,A_n)&=\{\theta \in \mathcal {B}(U)\mid p(\theta (\overline{A_1}),\ldots ,\theta (\overline{A_n}))\le b)\}, \end{aligned}$$
 5.Similarly, we use the semantic domain from item 3, Markov chains, to obtain the probabilistic \(\mu \)calculus with polynomial inequalities [23]: We put \(\varLambda =\{L_{p,b},M_{p,b}\mid p\in \mathbb {Q}_{>0}[X_1,\ldots , X_n],b\in \mathbb {Q}_{\ge 0},n\in \mathbb {N}\}\) (i.e. p ranges over polynomials) andfor sets U and \(A_1,\ldots ,A_n\subseteq U\). This logic presumably does not encode into the probabilistic \(\mu \)calculus as in 3 above, and can express constraints on independent products of events (see also [25]). E.g. the formula \(\nu Y.\,L_{X_1X_2,0.9}(p\wedge Y,q\wedge Y)\) says roughly that two independently sampled successors of the current state will satisfy p and q, respectively, and then satisfy the same property again, with probability at least 0.9.$$\begin{aligned}{}[\![L_{p,b}]\!]_U(A_1,\ldots ,A_n)&=\{d\in \mathcal {D}(U)\mid p(d(A_1),\ldots ,d(A_n))> b\}\\ [\![M_{p,b}]\!]_U(A_1,\ldots ,A_n)&=\{d\in \mathcal {D}(U)\mid p(d(\overline{A_1}),\ldots ,d(\overline{A_n}))\le b\} \end{aligned}$$
3 Tracking Automata
We use parity automata (e.g. [13]) that track single formulas along paths through potential models to decide whether it is possible to construct a model in which all least fixpoint formulas are eventually satisfied. Formally, (nondeterministic) parity automata are tuples \(\mathsf {A}=(V,\varSigma ,\varDelta ,q_0,\alpha )\) where V is a set of nodes; \(\varSigma \) is a finite set, the alphabet; \(\varDelta \subseteq V\times \varSigma \times V\) is the transition relation assigning a set \(\varDelta (v,a)=\{u\mid (v,a,u)\in \varDelta \}\) of nodes to all \(v\in V\) and \(a\in \varSigma \); \(q_0\in V\) is the initial node; and \(\alpha :\varDelta \rightarrow \mathbb {N}\) is the priority function, assigning priorities \(\alpha (v,a,u)\in \mathbb {N}\) to transitions \((v,a,u)\in \varDelta \) (this is the standard in recent work since it yields slightly more succinct automata). If \(\varDelta \) is a (partial) functional relation, then \(\mathsf {A}\) is said to be deterministic, and we denote the corresponding partial function by Open image in new window . The automaton \(\mathsf {A}\) accepts an infinite word \(w=w_0,w_1,\ldots \in \varSigma ^\omega \) if there is a wpath through \(\mathsf {A}\) on which the highest priority that is passed infinitely often is even; formally, the language that is accepted by \(\mathsf {A}\) is defined by \(L(\mathsf {A})=\{w\in \varSigma ^\omega \mid \exists \rho \in \mathsf {run}(\mathsf {A},w).\, \max (\mathsf {Inf}(\alpha \circ \rho ))\text { is even}\}\), where \(\mathsf {run}(\mathsf {A},w)\) denotes the set of infinite sequences \((\rho _0,w_0,\rho _1),(\rho _1,w_1,\rho _2),\ldots \in \varDelta ^\omega \) such that \(\rho _0=q_0\) and where, given an infinite sequence S, \(\mathsf {Inf}(S)\) denotes the elements that occur infinitely often in S. Here, we see infinite sequences \(\rho \in U^\omega \) over some set U as functions \(\mathbb {N}\rightarrow U\) and write \(\rho _i\) to denote the ith element of \(\rho \).
We now fix a target formula \(\chi \) and put \(n_0=\chi \), \(n_1=\mathsf {size}(\chi )\). We let \(\mathbf F\) denote the FischerLadner closure [20] of \(\chi \); i.e. \(\mathbf F\) contains all formulas that can arise as subformulas when unfolding each fixpoint in \(\chi \) exactly once. We put \(k=\max \{\mathsf {ad}(\psi )\mid \psi \in \mathbf F\}\) and \(\mathsf {selections}=\mathcal {P}(\mathbf F\cap \varLambda (\mathbf F))\) (\(\mathbf F\cap \varLambda (\mathbf F)\) is the set of modal literals in \(\mathbf F\)). We have \(\mathbf F\le n\) and hence \(\mathsf {selections}\le 2^n\).
Definition 2
Remark 3
It has been noted that the standard tracking automata for alternationfree formulas are, in fact, CoBüchi automata [10, 16] and that the tracking automata for aconjunctive formulas are limitdeterministic parity automata [15]. These considerably simpler automata can be determinized to deterministic Büchi automata of size \(3^{n_0}\) and to deterministic parity automata of size \(\mathcal {O}((n_0k)!)\) and with \(2n_0k\) priorities, respectively. This observation also holds true for the tracking automata in this work so that for formulas of suitable syntactic shape, Lemma 11 below yields accordingly lower bounds on the runtime of our satisfiability checking algorithm.
4 Global Caching for the Coalgebraic \(\mu \)Calculus
We now introduce a generic global caching algorithm for satisfiability in the coalgebraic \(\mu \)calculus. Given an input formula \(\chi \), the algorithm expands the determinized and complemented tracking automaton \(\mathsf {B}_\chi \) step by step and propagates (un)satisfiability through this graph; the algorithm terminates as soon as the initial node \(v_0\) is marked as (un)satisfiable. The algorithm bears similarity to standard gamebased algorithms for \(\mu \)calculi [8, 9, 15]; however, it crucially deviates from these algorithms in the treatment of modal steps: Intuitively, our algorithm decides whether it is possible to remove some of the modal transitions as well as one of the transitions from each reachable pair \(((\psi _0\vee \psi _1),0),((\psi _0\vee \psi _1),1)\) of disjunction transitions within the automaton \(\mathsf {B}_\chi \) in such a way that the resulting subautomaton of \(\mathsf {B}_\chi \) is totally accepting, that is, accepts any word for which there is an infinite run. In doing so, it is crucial that the labels of state nodes v in the reduced automaton are onestep satisfiable, in a sense introduced next, in the set of states that are reachable from v by the remaining modal transitions. Propagating (un)satisfiability over modal transitions thus involves onestep satisfiability checking, a functorspecific problem that in many instances can be solved in time singly exponential in \(\mathsf {size}(\chi )\). In previous work [8], a variant of onestep satisfiability has been used in satisfiability games for coalgebraic \(\mu \)calculi, which however leads to a doubly exponential number of modal moves for one of the players and hence does not yield a singly exponential upper bound on satisfiability checking (unless a suitable set of tableau rules is provided).
Definition 4
Remark 5
We keep the definition of the actual onestep logic as mentioned in the introduction somewhat implicit in the above definition of the onestep satisfiability problem. One can see that it contains two layers: a purely propositional layer embodied in U, which postulates which propositional formulas over V are satisfiable; and a modal layer with nesting depth of modalities uniformly equal to 1, embodied in the set v, which specifies constraints on an element of TU.
Example 6
For the standard modal \(\mu \)calculus (Example 1.1), the onestep satisfiability problem is to decide for given \(v\subseteq \varLambda (V)\) and \(U\subseteq \mathcal {P}(V)\) whether there is \(A\in \mathcal {P}(U)\cap [\![v]\!]_1\), that is, a subset \(A\subseteq U\) such that for each \(\Diamond a\in v\), there is \(u\in A\) such that \(a\in u\), and for each \(\Box a\in v\) and each \(u\in A\), \(a\in u\). Here we have \(t(a,b)\le a\cdot 2^{b}\) where \(a=\mathsf {size}(v)\), \(b=V\). For the graded \(\mu \)calculus (Example 1.2), the onestep satisfiability problem is to decide for v, U as above whether there is a multiset \(\theta \in \mathcal {B}(U)\) such that \(\sum _{u\in U\mid a\in u}\theta (u)>m\) for each \(\langle m\rangle a\in v\) and \(\sum _{u\in U\mid a\notin u}\theta (u)\le m\) for each \([m]a\in v\).
Definition 7
(States and Prestates). A node v of \(B_\chi \) is a state if its label contains only modal literals (\(l(v)\subseteq \varLambda (\mathbf F)\)), and otherwise a prestate, in which case we fix \(\psi _v\in l(v)\setminus \varLambda (\mathbf F)\). We write \(\mathsf {states},\mathsf {prestates}\subseteq D_\chi \) for the sets of states and prestates, respectively.
We next define \(2n_0k\)ary set functions f and g that compute onestep (un)satisfiability w.r.t. their argument sets.
Definition 8
Since for states v, \(l(v)\subseteq \varLambda (\mathbf {F})\) and \(X_i(v)\subseteq \mathcal {P}(\mathbf F)\) for all i, onestep propagation steps for states are instances of the onestep satisfiability problem with \(V=\mathbf F\), solvable in time \(t(n_1,n_0)\) because \(\mathsf {size}(l(v))\le n_1\) and \(\mathbf F\le {n_0}\).
Definition 9
The set \(\mathbf {E}_G\) contains nodes \(v\in G\) for which there are choices for all disjunctions and modal transitions that are reachable from v within G (as indicated at the beginning of the section) such that the labels of all reachable states in the chosen subautomaton of \(\mathsf {B}_\chi \) are onestep satisfiable and such that on all paths through the chosen subautomaton, the highest priority that is passed infinitely often is even, the intuition being that no least fixpoint is unfolded infinitely often without being dominated. Dually, the set \(\mathbf {A}_G\) contains nodes for which there exist no such suitable choices.
We recall that \(v_0\in D_\chi \) is the initial state of the determinized and complemented tracking automaton \(\mathsf {B}_\chi \). The algorithm expands \(\mathsf {B}_\chi \) stepbystep starting from \(v_0\); for prestates u, the expansion step adds nodes according to the fixed nonmodal formula \(\psi _u\) that is to be expanded next (Definition 7), and for states, the expansion follows all (matching) selections. The order of expansion can be chosen freely, e.g. by heuristic methods. Optional intermediate propagation steps can be used judiciously to realize onthefly solving.
Algorithm 10
(Global caching). To decide the satisfiability of the input formula \(\chi \), initialize the sets of unexpanded and expanded nodes, \(U=\{v_0\}\) and \(G=\emptyset \), respectively.
 1.
Expansion: Choose some unexpanded node \(u\in U\), remove u from U, and add u to G. If u is a prestate, then add the set \(\{\delta (u,\sigma )\mid \sigma \in \varSigma \cap (\psi _u\times \{0,1\})\}\) to U. If u is a state, then add the set \(\{\delta (u,\kappa )\mid \kappa \in \mathsf {selections}\}\) to U.
 2.
Optional propagation: Compute \(\mathbf {E}_G\) and/or \(\mathbf {A}_G\). If \(v_0\in \mathbf {E}_G\), then return ‘satisfiable’, if \(v_0\in \mathbf {A}_G\), then return ‘unsatisfiable’.
 3.
If \(U\ne \emptyset \), then continue with step 1.
 4.
Final propagation: Compute \(\mathbf {E}_G\). If \(v_0\in \mathbf {E}_G\), then return ‘satisfiable’, otherwise return ‘unsatisfiable’.
Lemma 11
Algorithm 10 runs in time \(\mathcal {O}(((n_0k)!)^{4n_0k}\cdot t(n_1,n_0))\).
Proof
The loop of the algorithm expands the determinized and complemented tracking automaton node by node and hence is executed at most \(D_\chi \in \mathcal {O}(((n_0k)!)^2)\subseteq 2^{\mathcal {O}(n_0k\log n_0)}\) times. A single expansion step can be implemented in time \(\mathcal {O}(2^{n_0})\) since propositional expansion is unproblematic and for the modal expansion of a state u, all (matching) selections, of which there are (at most) \(2^{n_0}\), have to be considered. A single propagation step consists in computing two fixpoints of nesting depth \(2n_0k\) of the functions f and g over \(\mathcal {P}(D_\chi )^{2n_0k}\) and can hence be implemented in time \(2(D_\chi ^{2n_0k}\cdot t(n_1,n_0))\in \mathcal {O}(((n_0k!)^2)^{2n_0k}\cdot t(n_1,n_0)) \subseteq 2^{\mathcal {O}(n_0^2k^2\log n_0+\log (t(n_1,n_0)))}\), noting that a single computation of \(f(\mathbf {X})\) and \(g(\mathbf {X})\) for a tuple \(\mathbf {X}\in \mathcal {P}(D_\chi )^{2n_0k}\) can be implemented in time \(\mathcal {O}(t(n_1,n_0))\) – this has been noted above for states, and prestates are unproblematic. Thus the complexity of the whole algorithm is dominated by the complexity of the propagation step. \(\square \)
Corollary 12
If the onestep satisfiability problem of a coalgebraic logic can be solved in time t(a, b) exponential in \(a+b\) on inputs \(v\subseteq \varLambda (V)\), \(U\subseteq \mathcal {P}(V)\) with \(\mathsf {size}(v)=a\), \(V=b\), then the satisfiability problem of the corresponding coalgebraic \(\mu \)calculus is in \(\textsc {ExpTime}\).
Since the existence of a tractable set of tableau rules implies the required time bound on onestep satisfiability, the above result subsumes earlier bounds obtained by tableaubased approaches in [4, 15, 16]; however, it covers additional example logics for which no suitable tableau rules are known. In particular we have
Proposition 13
 1.
the standard \(\mu \)calculus,
 2.
the graded \(\mu \)calculus,
 3.
the (twovalued) probabilistic \(\mu \)calculus,
 4.
the graded \(\mu \)calculus with polynomial inequalities,
 5.
the (twovalued) probabilistic \(\mu \)calculus with polynomial inequalities.
(Tractable sets of tableau rules have previously been claimed for the graded [36] and Presburger [22] \(\mu \)calculus but have since been discovered to be flawed [23].)
Proof
It suffices to show that the respective onestep satisfiability problems can be solved on inputs \(v\subseteq \varLambda (V)\), \(U\subseteq \mathcal {P}(V)\) with \(\mathsf {size}(v)=a\) and \(V=b\) in singly exponential time in \(a+b\), i.e. in time \(t(a,b)\in 2^{p(a+b)}\) for p at most polynomial. E.g. for standard relational modalities, we have \(t(a,b)=a\cdot 2^b= 2^{b+\log a}\), see Example 6. While the bounds can be established by relatively easy arguments (e.g. using known bounds on sizes of solutions of systems of real or integer linear inequalities) for all of our remaining example logics, we import them from previous work for brevity. For the onestep satisfiability problem of graded modal logic, by [21, Lemma 1], we have \(t(a,b)\le (2\cdot 2^a+2)^{b}\le 2^{ab+2b}\); the Lemma uses counters to check joint onestep satisfiability of constraints and directly extends to the onestep satisfiability problem of graded modal logic with monotone polynomial inequalities, in which case we require n counters for each nary polynomial. The bound for (twovalued) probabilistic modal logic (with polynomial inequalities) is shown in [23, Example 7]. \(\square \)
Remark 14
We also obtain a polynomial bound on branching width in models for all our example logics simply by importing Lemma 6 and the observations in Example 7 from [23]. With the exception of the standard \(\mu \)calculus, this bound appears to be new in all our example logics. Of course, for graded and Presburger \(\mu \)calculi, polynomial branching holds only in their coalgebraic semantics, i.e. over multigraph models but not over Kripke models.
5 Soundness and Completeness
We now prove the central result, that is, the soundness and completeness of Algorithm 10. As the sets \(\mathbf {E}_G\) and \(\mathbf {A}_G\) grow monotonically with G, it suffices to prove equivalence of satisfiability and containment of the initial node \(v_0\) in \(\mathbf {E}:=\mathbf {E}_{D_\chi }\). Our program is as follows: We show that \(v_0\in \mathbf {E}\) if and only if there is a presemitableau (Definition 15) for \(\chi \) with unfolding timeouts (Definition 17), which in turn is the case if and only if \(\chi \) is satisfiable. We establish the latter equivalence by constructing a model for \(\chi \) from a given presemitableau with unfolding timeouts and, for the converse direction, extracting a presemitableau with unfolding timeouts from the model.
Definition 15
(Presemitableau). Given a ternary relation \(R\subseteq A\times B\times A\) and \(a\in A\), \(b\in B\), we generally write \(R(a)=\{a'\in A\mid \exists b\in B.\, (a,b,a')\in R\}\) and \(R(a,b)=\{a'\in A\mid (a,b,a')\in R\}\). Let \(W\subseteq D_\chi \) and put \(U=W\cap \mathsf {prestates}\) and \(V=W\cap \mathsf {states}\). Given a ternary relation \(L\subseteq W\times \varSigma \times W\), the pair (W, L) is a presemitableau for \(\chi \) if the following conditions hold: \(L\subseteq \delta \); \(T(L(v))\cap [\![l(v)]\!]_1\ne \emptyset \) for all \(v\in V\); for each \(u\in U\), there is exactly one \(b\in \{0,1\}\) such that \(L(u,(\psi _u,b))=\{\delta (u,(\psi _u,b))\}\), and for all other \(\sigma \in \varSigma \), \(L(u,\sigma )=\emptyset \); and there is no Lcycle that contains only elements from U. A path through a presemitableau is an infinite sequence \((v_0,\sigma _0),(v_1,\sigma _1),\ldots \in (W\times \varSigma )^\omega \) such that for all i, \(v_{i+1}\in L(v_i,\sigma _i)\). We denote the first state that is reachable by zero or more Lsteps from a node \(v\in W\) by \(\lceil v\rceil \) (since there is no Lcycle within U, such a state always exists).
Given a state v, the relation L of a presemitableau thus picks a set L(v) of nodes in which l(v) is onestep satisfiable; given a prestate u, L picks a single (pre)state that is obtained from u by transforming the formula \(\psi _u\).
Definition 16
(Tracking timeouts). Given a path \(\rho =(v_0,\sigma _0),(v_1,\sigma _1),\ldots \) through a presemitableau, we say that priority i occurs (at position j) in \(\rho \) if \(\beta (v_j, \sigma _j,v_{j+1})=i\), recalling that \(\beta \) is the priority function of the determinised and complemented tracking automaton \(\mathsf {B}_\chi \). Then the path \(\rho \) has tracking timeouts \(\overline{m}=(m_{2n_0k},\ldots ,m_1)\) if for each odd \(1\le i< 2n_0k\), priority i occurs at most \(m_i\) times in \(\rho \) before some priority greater than i occurs in \(\rho \). Nothing is said about the \(m_i\) for even i, which are in fact irrelevant and serve only to ease notation. A node \(w\in W\) in a presemitableau (W, L) has tracking timeouts \(\overline{m}\) if every path through (W, L) starting at w has tracking timeouts \(\overline{m}\). A presemitableau (W, L) has tracking timeouts if each \(w\in W\) has tracking timeouts \(\overline{m}\) for some \(\overline{m}\).
Intuitively, a presemitableau (W, L) has tracking timeouts if every word that encodes an infinite Lpath through W is accepted by \(\mathsf {B}_\chi \). The next definition is geared towards characterizing nonacceptance by \(\mathsf {A}_\chi \):
Definition 17
(Traces and unfolding timeouts). Let (W, L) be a graph with \(L\subseteq W\times \varSigma \times W\) and labeling function \(l:W\rightarrow \mathcal {P}(\mathbf F)\). Given an Lpath \(\rho =(v_0,\sigma _0),(v_1,\sigma _1),\ldots \) (with \((v_i,\sigma _i,v_{i+1})\in L\) for \(i\ge 0\)) and a sequence of formulas \(\varPsi =\psi _0,\psi _1,\ldots \), we say that \(\varPsi \) is a trace of \(\psi _0\) along \(\rho \) (we also say that \(\rho \) contains the trace \(\varPsi \)) if \(\psi _i\in l(v_i)\) and \(\psi _{i+1}\in \varDelta (\psi _{i},\sigma _{i})\) for all i. For i with \(\psi _i=\eta X.\psi \) for some fixpoint variable X and some formula \(\psi \), we say that \(\varPsi \) unfolds at level \(\mathsf {ad}(\psi _i)\) at position i. Then the trace \(\varPsi \) has unfolding timeout \(m\in \mathbb {N}\) for \(\psi _0\) at level j if \(\varPsi \) unfolds at most m times at level j before \(\varPsi \) unfolds at some level greater than j. The path \(\rho \) has unfolding timeouts for \(\psi _0\) at level j if there is, for all its traces \(\varPsi \) of \(\psi _0\), some m such that \(\varPsi \) has unfolding timeout m for \(\psi _0\) at level j. A node \(w\in W\) has unfolding timeouts at level j for some formula \(\psi \) if every path through (W, L) that starts at w and that contains infinitely many steps \((v_i,\sigma _i)\) such that \(\sigma _i\in \mathsf {selections}\) has unfolding timeouts for \(\psi \) at level i. (Since fixpoint variables are by assumption guarded by modal operators, it suffices to require timeouts just for such paths that contain infinitely many modal steps.) A node \(w\in W\) has unfolding timeouts \(\overline{m}=(m_k,\ldots ,m_1)\) for some formula \(\psi \) if every path through (W, L) that starts at w and that contains infinitely many steps \((v_i,\sigma _i)\) such that \(\sigma _i\in \mathsf {selections}\) has, for each odd \(1\le i\le k\), unfolding timeouts \(\overline{m}\) for \(\psi \) at level i; again the unfolding timeouts for even i, that is, for greatest fixpoints, are irrelevant. The graph (W, L) has unfolding timeouts if for each element \(w\in W\) and each formula \(\psi \in l(v)\), there is some vector \(\overline{m}\) such that w has unfolding timeouts \(\overline{m}\) for \(\psi \). We denote the set of nodes that have unfolding timeouts \(\overline{m}\) for \(\psi \) by \(\mathsf {uto}(\psi ,\overline{m})\subseteq W\).
A graph (W, L) has unfolding timeouts if for all words that encode an infinite Lpath through (W, L), all runs of the nondeterministic tracking automaton \(\mathsf {A}_\chi \) on the word are nonaccepting. We recall that a run of \(\mathsf {A}_\chi \) is accepting if it unfolds some least fixpoint infinitely often without having it dominated.
Lemma 18
Let (W, L) be a presemitableau. Then (W, L) has tracking timeouts if and only if it has unfolding timeouts.
Proof
We recall that \(\mathsf {B}_\chi \) is obtained from \(\mathsf {A}_\chi \) by determinization and subsequent complementation so that we have \(L(\mathsf {B}_\chi )=\overline{L(\mathsf {A}_\chi )}\). The result thus follows directly from the fact that having tracking timeouts means that \(\mathsf {B}_\chi \) accepts all words that encode a path in (W, L) while having unfolding timeouts means that \(\mathsf {A}_\chi \) does not accept any word that encodes a path in (W, L). \(\square \)
Lemma 19
We have \(v_0\in \mathbf {E}\) if and only if there is a presemitableau for \(\chi \) that has tracking timeouts.
Combining Lemmas 19 and 18, we obtain
Corollary 20
We have \(v_0\in \mathbf {E}\) if and only if there is a presemitableau for \(\chi \) that has unfolding timeouts.
We now show that satisfiability of \(\chi \) and the existence of a semipretableau for \(\chi \) with unfolding timeouts coincide.
Definition 21
Thus we have \(v\in [\![\psi ]\!]_{\overline{m}}\) if there is a node \(u\in W\) such that \(\lceil u\rceil =v\) and u has timeouts \(\overline{m}\) for \(\psi \). This serves to ease the proofs of the upcoming existence and truth lemmas as it anchors the timeout vector \(\overline{m}\) at the node u instead of anchoring it at the state v which may not have timeouts \(\overline{m}\) for \(\psi \) (namely, if a greatest fixpoint is unfolded on the Lpath from u to v).
Definition 22
Strongly coherent coalgebras exist over presemitableaux:
Lemma 23
(Existence). Let (W, L) be a presemitableau with set of states V. Then there is a strongly coherent coalgebra over V.
Since all least fixpoint literals are satisfied after finitely many unfolding steps in strongly coherent coalgebras with unfolding timeouts, they are models, i.e. satisfy all the formulas in their labels:
Lemma 24
Definition 25
(Timedout satisfaction). Given sets \(U\subseteq W\), a function \(f:\mathcal {P}(W)\rightarrow \mathcal {P}(W)\) and an ordinal number \(\lambda \), we define \(f^\lambda (U)=U\) if \(\lambda =0\), \(f^\lambda (U)=f(f^{\lambda '}(U))\) if \(\lambda =\lambda '+1\) and \(f^\lambda (U)=\bigcup _{k<\lambda } f^k(U)\) if \(\lambda \) is a limitordinal. The target formula \(\chi \) is clean so that it contains, for each fixpoint variable \(X\in \mathbf {V}\), at most a single fixpoint literal \(\eta X.\psi _0\) as a subformula; we denote this formula by \(\theta (X)\). Given a coalgebra \((C,\xi )\), a formula \(\psi \) and a vector \(\overline{\lambda }=(\lambda _k,\ldots ,\lambda _j)\) of ordinal numbers, we define \([\![\psi ]\!]^{\overline{\lambda }}=[\![\psi ]\!]_i\) where Open image in new window is defined, for fixpoint variables \(X_j\) that occur freely in \(\psi \) and for which we have \(\theta (X_j)=\eta X_j\psi _j\), by \(i(X_j)=([\![\psi _j]\!]^{X_j}_{i'})^{\lambda _j}(\emptyset )\) if \(\eta =\mu \) and by \(i(X_j)=[\![\nu X_j.\psi _j]\!]_{i'}\) if \(\eta =\nu \), where \(i'(X_{j'})\) is undefined for \(j'\ge j\) and where \(i'(X_{j'})=i(X_{j'})\) for \(j'<j\). Again the timeouts for greatest fixpoint variables are irrelevant and serve only to ease notation.
Definition 26

for all \(\psi \in \mathbf F\) and \(x\in C\), if \(x\notin [\![\psi ]\!]\), then \(L(x,(\psi ,b))=\emptyset \) for \(b\in \{0,1\}\); if \(x\in [\![\psi ]\!]\), then we distinguish upon the shape of \(\psi \): if \(\psi =\psi _0\vee \psi _1\), then we require \(L(x,(\psi ,b))=\{x\}\) for exactly one \(b\in \{0,1\}\) with \(x\in [\![\overline{\psi _b}]\!]^{\overline{\lambda }_{\overline{\psi }}}\) and \(L(x,(\psi ,\overline{b}))=\emptyset \), where \(\overline{1}=0\), \(\overline{0}=1\); if \(\psi =\psi _0\wedge \psi _1\) or \(\psi =\eta X.\psi _0\), then we require \(L(x,(\psi ,0))=\{x\}\).

for all \(x\in C\) and \(\kappa \in \mathsf {selections}\), we have \(L(x,\kappa )=\{y\}\) for some \(y\in A=\cap _{\heartsuit \psi \in \kappa }[\![\overline{\psi }^{\overline{\lambda }_{\heartsuit \psi }}]\!]\) if \(A\ne \emptyset \), and \(L(x,\kappa )=\emptyset \) otherwise.
Lemma 27
Every coalgebra has a strongly supporting Kripke frame.
Definition 28
Strongly supporting Kripke frames have unfolding timeouts:
Lemma 29
For all coalgebras \((C,\xi )\) with strongly supporting Kripke frame (C, L), all formulas \(\psi \) and all valuations Open image in new window , we have \([\![\psi ]\!]_i\subseteq [\![\psi ]\!]_i^L.\)
Lemma 30
(Soundness). Let \(\chi \) be satisfiable. Then a presemitableau for \(\chi \) with unfolding timeouts can be constructed over a subset of \(D_\chi \).
Proof
(Sketch). By Lemmas 27 and 29, any model of \(\chi \) has a strongly supporting Kripke frame (C, L) with unfolding timeouts. We derive a presemitableau for \(\chi \) from (C, L), inheriting unfolding timeouts. \(\square \)
Corollary 31
Our model construction moreover yields the same bound on minimum model size as in earlier work on the coalgebraic \(\mu \)calculus [4]:
Corollary 32
(Small model property). Let \(\chi \) be a satisfiable coalgebraic \(\mu \)calculus formula. Then \(\chi \) has a model of size \(\mathcal {O}(((nk)!)^2)\in 2^{\mathcal {O}(nk\log n)}\).
6 Conclusion
We have shown that the satisfiability problem of the coalgebraic \(\mu \)calculus is in \(\textsc {ExpTime}\), subject to establishing a suitable time bound on the much simpler onestep satisfiability problem. Prominent examples include the graded \(\mu \)calculus, the (twovalued) probabilistic \(\mu \)calculus, and extensions of the probabilistic and the graded \(\mu \)calculus, respectively, with (monotone) polynomial inequalities; the \(\textsc {ExpTime}\) bound appears to be new for the last two logics. We have also presented a generic satisfiability algorithm that realizes the time bound and supports global caching and onthefly solving. Moreover, we have obtained a polynomial bound on minimum branching width in models for all example logics mentioned above.
References
 1.Alur, R., Henzinger, T., Kupferman, O.: Alternatingtime temporal logic. J. ACM 49, 672–713 (2002)MathSciNetCrossRefGoogle Scholar
 2.Bradfield, J., Stirling, C.: Modal \(\mu \)calculi. In: Handbook of Modal Logic, pp. 721–756. Elsevier (2006)Google Scholar
 3.Bradfield, J., Walukiewicz, I.: The mucalculus and model checking. In: Clarke, E., Henzinger, T., Veith, H., Bloem, R. (eds.) Handbook of Model Checking, pp. 871–919. Springer, Cham (2018). https://doi.org/10.1007/9783319105758_26CrossRefzbMATHGoogle Scholar
 4.Cîrstea, C., Kupke, C., Pattinson, D.: EXPTIME tableaux for the coalgebraic \(\mu \)calculus. Log. Methods Comput. Sci. 7, 1–33 (2011)MathSciNetCrossRefGoogle Scholar
 5.Cleaveland, R., Iyer, S., Narasimha, M.: Probabilistic temporal logics via the modal \(\mu \)calculus. Theor. Comput. Sci. 342, 316–350 (2005)MathSciNetCrossRefGoogle Scholar
 6.D’Agostino, G., Visser, A.: Finality regained: a coalgebraic study of Scottsets and multisets. Arch. Math. Logic 41, 267–298 (2002)MathSciNetCrossRefGoogle Scholar
 7.Demri, S., Lugiez, D.: Presburger modal logic is PSPACEcomplete. In: Furbach, U., Shankar, N. (eds.) IJCAR 2006. LNCS (LNAI), vol. 4130, pp. 541–556. Springer, Heidelberg (2006). https://doi.org/10.1007/11814771_44CrossRefGoogle Scholar
 8.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–392. Springer, Heidelberg (2010). https://doi.org/10.1007/9783642141621_32CrossRefzbMATHGoogle Scholar
 9.Friedmann, O., Lange, M.: Deciding the unguarded modal \(\mu \)calculus. J. Appl. NonClassical Log. 23, 353–371 (2013)MathSciNetCrossRefGoogle Scholar
 10.Friedmann, O., Latte, M., Lange, M.: Satisfiability games for branchingtime logics. Log. Methods Comput. Sci. 9, 1–36 (2013)MathSciNetCrossRefGoogle Scholar
 11.Goré, R., Nguyen, L.A.: Exptime tableaux for ALC using sound global caching. J. Autom. Reason. 50, 355–381 (2013)MathSciNetCrossRefGoogle Scholar
 12.Goré, 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–219. Springer, Heidelberg (2009). https://doi.org/10.1007/9783642027161_16CrossRefzbMATHGoogle Scholar
 13.Grädel, 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/3540363874CrossRefzbMATHGoogle Scholar
 14.Hausmann, D., Schröder, 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–143. IEEE (2015)Google Scholar
 15.Hausmann, D., Schröder, 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–378. Springer, Cham (2018). https://doi.org/10.1007/9783319899633_21CrossRefGoogle Scholar
 16.Hausmann, D., Schröder, L., Egger, C.: Global caching for the alternationfree coalgebraic \(\mu \)calculus. In: Desharnais, J., Jagadeesan, R. (eds.) Concurrency Theory, CONCUR 2016. LIPIcs, vol. 59, pp. 34:1–34:15. Schloss Dagstuhl  LeibnizZentrum für Informatik (2016)Google Scholar
 17.Huth, M., Kwiatkowska, M.: Quantitative analysis and model checking. In: Logic in Computer Science, LICS 1997, pp. 111–122. IEEE (1997)Google Scholar
 18.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–286. Springer, Heidelberg (2001). https://doi.org/10.1007/3540453156_18CrossRefzbMATHGoogle Scholar
 19.Kozen, D.: Results on the propositional \(\mu \)calculus. Theor. Comput. Sci. 27, 333–354 (1983)MathSciNetCrossRefGoogle Scholar
 20.Kozen, D.: A finite model theorem for the propositional \(\mu \)calculus. Stud. Log. 47, 233–241 (1988)MathSciNetCrossRefGoogle Scholar
 21.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–437. Springer, Heidelberg (2002). https://doi.org/10.1007/3540456201_34CrossRefGoogle Scholar
 22.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–255. College Publications (2010)Google Scholar
 23.Kupke, C., Pattinson, D., Schröder, L.: Reasoning with global assumptions in arithmetic modal logics. In: Kosowski, A., Walukiewicz, I. (eds.) FCT 2015. LNCS, vol. 9210, pp. 367–380. Springer, Cham (2015). https://doi.org/10.1007/9783319221779_28CrossRefGoogle Scholar
 24.Liu, W., Song, L., Wang, J., Zhang, L.: A simple probabilistic extension of modal mucalculus. In: Yang, Q., Wooldridge, M. (eds.) International Joint Conference on Artificial Intelligence, IJCAI 2015, pp. 882–888. AAAI Press (2015)Google Scholar
 25.Mio, M.: Probabilistic modal \({\mu }\)calculus with independent product. In: Hofmann, M. (ed.) FOSSACS 2011. LNCS, vol. 6604, pp. 290–304. Springer, Heidelberg (2011). https://doi.org/10.1007/9783642198052_20CrossRefGoogle Scholar
 26.Myers, R., Pattinson, D., Schröder, L.: Coalgebraic hybrid logic. In: de Alfaro, L. (ed.) FOSSACS 2009. LNCS, vol. 5504, pp. 137–151. Springer, Heidelberg (2009). https://doi.org/10.1007/9783642005961_11CrossRefGoogle Scholar
 27.Niwinski, D., Walukiewicz, I.: Games for the \(\mu \)calculus. Theor. Comput. Sci. 163, 99–116 (1996)MathSciNetCrossRefGoogle Scholar
 28.Parikh, R.: The logic of games and its applications. Ann. Discret. Math. 24, 111–140 (1985)MathSciNetzbMATHGoogle Scholar
 29.Pattinson, D.: Coalgebraic modal logic: soundness, completeness and decidability of local consequence. Theor. Comput. Sci. 309, 177–193 (2003)MathSciNetCrossRefGoogle Scholar
 30.Piterman, N.: From nondeterministic Büchi and Streett automata to deterministic parity automata. Log. Methods Comput. Sci. 3(3:5), 1–21 (2007)MathSciNetzbMATHGoogle Scholar
 31.Rutten, J.: Universal coalgebra: a theory of systems. Theor. Comput. Sci. 249, 3–80 (2000)MathSciNetCrossRefGoogle Scholar
 32.Safra, S.: On the complexity of omegaautomata. In: Foundations of Computer Science, FOCS 1988, pp. 319–327. IEEE Computer Society (1988)Google Scholar
 33.Schröder, L.: A finite model construction for coalgebraic modal logic. J. Log. Algebr. Prog. 73, 97–110 (2007)MathSciNetCrossRefGoogle Scholar
 34.Schröder, L.: Expressivity of coalgebraic modal logic: the limits and beyond. Theor. Comput. Sci. 390(2–3), 230–247 (2008)MathSciNetCrossRefGoogle Scholar
 35.Schröder, L., Pattinson, D.: Shallow models for noniterative modal logics. In: Dengel, A.R., Berns, K., Breuel, T.M., Bomarius, F., RothBerghofer, T.R. (eds.) KI 2008. LNCS (LNAI), vol. 5243, pp. 324–331. Springer, Heidelberg (2008). https://doi.org/10.1007/9783540858454_40CrossRefGoogle Scholar
 36.Schröder, L., Pattinson, D.: PSPACE bounds for rank1 modal logics. ACM Trans. Comput. Log. 10(2), 13:1–13:33 (2009)MathSciNetCrossRefGoogle Scholar
Copyright information
Open Access This chapter is licensed under the terms of the Creative Commons Attribution 4.0 International License (http://creativecommons.org/licenses/by/4.0/), which permits use, sharing, adaptation, distribution and reproduction in any medium or format, as long as you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons license and indicate if changes were made.
The images or other third party material in this chapter are included in the chapter's Creative Commons license, unless indicated otherwise in a credit line to the material. If material is not included in the chapter's Creative Commons license and your intended use is not permitted by statutory regulation or exceeds the permitted use, you will need to obtain permission directly from the copyright holder.