# Coalgebraic Satisfiability Checking
for Arithmetic $\mu$-Calculi

Daniel Hausmann  University of Gothenburg, Sweden<EMAIL_ADDRESS>and
Lutz Schröder  Friedrich-Alexander-Universität Erlangen-Nürnberg, Germany
<EMAIL_ADDRESS>
###### Abstract.

The coalgebraic $\mu$-calculus provides a generic semantic framework for
fixpoint logics over systems whose branching type goes beyond the standard
relational setup, e.g. probabilistic, weighted, or game-based. Previous work
on the coalgebraic $\mu$-calculus includes an exponential-time upper bound on
satisfiability checking, which however relies on the availability of tableau
rules for the next-step modalities that are sufficiently well-behaved in a
formally defined sense; in particular, rule matches need to be representable
by polynomial-sized codes, and the sequent duals of the rules need to absorb
cut. While such rule sets have been identified for some important cases, they
are not known to exist in all cases of interest, in particular ones involving
either integer weights as in the graded $\mu$-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. Notably, our
approach directly accommodates unguarded formulae, and thus avoids use of the
guardedness transformation. Example applications include new exponential-time
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 (two-valued) probabilistic
$\mu$-calculus with polynomial inequalities.

###### Key words and phrases:

$\mu$-calculus, satisfiability checking, coalgebra, probabilistic transition
systems, weighted transition systems, tableaux

##  1\. Introduction

Modal fixpoint logics are a well-established 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 [Koz83, BS06,
BW18], 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 [CIN05, HK97, CKP11a, LSWZ15], the alternating-
time $\mu$-calculus [AHK02], and the monotone $\mu$-calculus, which contains
Parikh’s game logic [Par85]. The graded $\mu$-calculus [KSV02] features next-
step modalities that count successors; it is standardly interpreted over
Kripke frames but, as pointed out by D’Agostino and Visser [DV02], graded
modalities are more naturally interpreted over so-called multigraphs, where
edges carry integer weights, and in fact this modification leads to better
bounds on minimum model size for satisfiable formulae.

Coalgebraic logic [Pat03] 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 [Rut00]; additionally, modalities are interpreted as so-
called _predicate liftings_ [Pat03, Sch08]. The _coalgebraic $\mu$-calculus_
[CKP11a] caters for fixpoint logics within this framework, and essentially
covers all mentioned (two-valued) examples as instances. It has been shown
that satisfiability checking in a given instance of the coalgebraic
$\mu$-calculus is in ExpTime, _provided_ that one exhibits a set of tableau
rules for the modalities, so-called _one-step rules_ , that is _one-step
tableau complete_ (a condition that, in the dual setting of sequent calculi,
translates into the requirement that the rule absorb cut [SP09, PS10]) and
moreover _tractable_ in a suitable sense (an assumption made also in our own
previous work on the flat [HS15] and alternation-free [HSE16] fragments of the
coalgebraic $\mu$-calculus). Such rules are known for many important cases,
notably including alternating-time logics, the probabilistic $\mu$-calculus
even when extended with linear inequalities, and the monotone $\mu$-calculus
[SP09, KP10, CKP11a]. There are, however, important cases where such rule sets
are currently missing, and where there is in fact little perspective for
finding suitable rules. Prominent cases of this kind are the graded
$\mu$-calculus and more expressive logics over integer weights featuring,
e.g., Presburger arithmetic111One-step tableau-complete sets of rules for the
graded $\mu$-calculus and more generally for the Presburger $\mu$-calculus
have been claimed in earlier work [SP09, KP10] but have since turned out to be
in fact incomplete [KPS22]; see also Remark 35.. Further cases arise when
logics over systems with non-negative 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
ExpTime upper bound for coalgebraic $\mu$-calculi even in the absence of
tractable sets of modal tableau rules. The method we use instead is to analyse
the so-called _one-step 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 _one-step logic_ , which excludes not only
fixpoints, but also nested next-step modalities, with a correspondingly
simplified semantics that no longer involves actual transitions. E.g. the one-
step logic of the standard relational $\mu$-calculus is interpreted over
models essentially consisting of a set with a distinguished subset, which
abstracts the successors of a single state (which is not itself part of the
model). We have applied this principle to satisfiability checking in
coalgebraic (next-step) modal logics [SP08], coalgebraic hybrid logics
[MPS09], and reasoning with global assumptions in coalgebraic modal logics
[KPS15, KPS22]. It also appears implicitly in work on automata for the
coalgebraic $\mu$-calculus [FLV10], which however establishes only a doubly
exponential upper bound in the case without tractable modal tableau rules.

Our main result states roughly that if the satisfiability problem of the one-
step logic is in ExpTime under a particular stringent measure of input size,
then satisfiability in the corresponding instance of the coalgebraic
$\mu$-calculus is in ExpTime. Since the criteria on rule sets featuring in
previous work on the coalgebraic $\mu$-calculus imply the ExpTime bound on
satisfiability checking in the one-step logic, this result subsumes previous
complexity estimates for the coalgebraic $\mu$-calculus [CKP+11b]. Our leading
example applications are on the one hand the graded $\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 (two-valued) probabilistic $\mu$-calculus [CKP11a, LSWZ15]
with (monotone) polynomial inequalities. While the graded $\mu$-calculus as
such is known to be in ExpTime [KSV02], 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 automata-theoretic 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 using _$\Lambda$ -automata_ [FLV10]
where modal steps in satisfiability games have doubly exponential branching
degree. Our algorithm witnessing the singly exponential time bound is, in
fact, a global caching algorithm [GW09, GN13]. As such, it is able to decide
the satisfiability of nodes on-the-fly, 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 singly-exponential bound on
minimum model size for satisfiable formulae in _all_ coalgebraic
$\mu$-calculi, calculated only in terms of the size of the parse tree of the
formula and its alternation depth (again, the best previously known bound for
the case without tractable modal tableau rules was doubly exponential
[FLV10]). This bound is new even in the case of the graded $\mu$-calculus. Of
course, in this case it holds only over multigraphs, again illustrating the
smoothness of multigraph semantics – over Kripke frames, it is clearly not
true as the model size can depend exponentially on numbers occurring in a
formula when these are coded in binary. Moreover, we identify a criterion for
a polynomial bound on branching in models, which holds in all our examples.

This paper extends a previous conference publication [HS19]. Besides providing
full proofs and additional background material, we also make do without the
problematic guardedness transformation (cf. [BFL15, KMV20]) and directly
establish our results for the unguarded coalgebraic $\mu$-calculus. On a
technical level, we rebase large parts of the development on newly introduced
notions of model checking game and satisfiability game for the unguarded
coalgebraic $\mu$-calculus, obtaining streamlined proofs.

### Organization

In Section 2, we recall the basics of coalgebra, coalgebraic logic, and the
coalgebraic $\mu$-calculus. We discuss the automata-theoretic approach and
model checking games in Section 3, and present the one-step logic as well as
the global caching algorithm and its runtime analysis in Section 4. Soundness
and completeness of the algorithm are proved in Section 5.

##  2\. The Coalgebraic $\mu$-Calculus

We recall basic definitions in coalgebra [Rut00], coalgebraic logic [Pat03,
Sch08], and the coalgebraic $\mu$-calculus [CKP11a]. While we do repeat
definitions of some categorical terms, we assume some familiarity with basic
category theory (e.g. [AHS90]).

### Coalgebra

The semantics of our logics will be based on transition systems in a general
sense, which we abstract as coalgebras for a type functor. The most basic
example are relational transition systems, or Kripke frames, which are just
pairs $(C,R)$ consisting of a set $C$ of _states_ and a binary _transition
relation_ $R\subseteq C\times C$. We may equivalently view such a structure as
a map of type $\xi\colon C\to\mathcal{P}C$ (where $\mathcal{P}$ denotes the
powerset functor and we omit brackets around functor arguments following
standard convention, while we continue to use brackets in uses of powerset
that are not related to functoriality), via a bijective correspondence that
maps $R\subseteq X\times X$ to the map $\xi_{R}\colon C\to\mathcal{P}C$ given
by $\xi_{R}(c)=\\{d\mid(c,d)\in R\\}$ for $c\in C$; that is, $\xi_{R}$ assigns
to each state $c$ a collection of some sort, in this case a set, of successor
states. The essence of _universal coalgebra_ [Rut00] is to base a general
theory of state-based systems on encapsulating this notion of _collections of
successors_ in a functor, for our purposes on the category $\mathsf{Set}$ of
sets and maps. We recall that such a functor
$F\colon\mathsf{Set}\to\mathsf{Set}$ assigns to each set $U$ a set $FU$, and
to each map $f\colon U\to V$ a map $Ff\colon FU\to FX$, preserving identities
and composition. As per the intuition given above, $FU$ should be understood
as consisting of some form of collections of elements of $U$. An _$F$
-coalgebra_ $(C,\xi)$ then consists of a set $C$ of _states_ and a _transition
map_ $\xi\colon C\to FC$, understood as assigning to each state $c$ a
collection $\xi(c)\in FC$ of successors. As indicated above, a basic example
is $F=\mathcal{P}$ (with $\mathcal{P}f(Y)=f[Y]$ for $f\colon U\to Y$), in
which case $F$-coalgebras are relational transition systems. To see just one
further example now, the _discrete distribution functor_ $\mathcal{D}$ is
given on sets $U$ by $\mathcal{D}U$ being the set of all discrete probability
distributions on $U$. We represent such distributions by their _probability
mass functions_ , i.e. functions $d\colon U\to({\mathbb{Q}}\cap[0,1])$ such
that $\sum_{u\in U}d(u)=1$, understood as assigning to each element of $U$ its
probability. (Note that the _support_ $\\{u\in U\mid d(u)>0\\}$ of $d$ is then
necessarily at most countable.) By abuse of notation, we also write $d$ for
the induced discrete probability measure on $U$, i.e. $d(Y)=\sum_{y\in Y}d(y)$
for $Y\in\mathcal{P}(U)$. The action of $\mathcal{D}$ on maps $f\colon U\to V$
is then given by $\mathcal{D}f(d)(Z)=d(f^{-1}[Z])$ for $d\in\mathcal{D}U$ and
$Z\in\mathcal{P}(V)$, i.e. $\mathcal{D}f$ takes image measures. A
$\mathcal{D}$-coalgebra $\xi\colon C\to\mathcal{D}C$ assigns to each state
$x\in C$ a distribution $\xi(x)$ over successor states, so
$\mathcal{D}$-coalgebras are Markov chains.

### Coalgebraic logic

The fundamental abstraction that underlies coalgebraic logic is to encapsulate
the semantics of next-step modalities in terms of _predicate liftings_. As a
basic example, consider the standard diamond modality $\Diamond$, whose
semantics over a transition system $(C,R)$ is given by

$c\models\Diamond\phi\quad\text{iff}\quad\exists d.\,(c,d)\in R\land
d\models\phi$

(where $\phi$ is a formula in some ambient syntax whose semantics is assumed
to be already given by induction). We can rewrite this definition along the
correspondence between transition systems and $\mathcal{P}$-coalgebras
$\xi\colon C\to\mathcal{P}C$ described above, obtaining

$\displaystyle c\models\Diamond\phi$
$\displaystyle\quad\text{iff}\quad\xi(c)\cap{[\\![\phi]\\!]}\neq\emptyset$
$\displaystyle\quad\text{iff}\quad\xi(c)\in\\{Y\in\mathcal{P}C\mid
Y\cap{[\\![\phi]\\!]}\neq\emptyset\\}$

where ${[\\![\phi]\\!]}=\\{d\in C\mid d\models\phi\\}$ denotes the _extension_
of $\phi$ in $(C,\xi)$. We can see the set $\\{Y\in\mathcal{P}C\mid
Y\cap{[\\![\phi]\\!]}\neq\emptyset\\}$ as arising from the application of a
set operation ${[\\![\Diamond]\\!]}$ to the set ${[\\![\phi]\\!]}$, thought of
as a predicate on $C$: For a predicate $P$ on $C$, we put

$\displaystyle{[\\![\Diamond]\\!]}(P)=\\{Y\in\mathcal{P}C\mid Y\cap
P\neq\emptyset\\}$

and then have

$c\models\Diamond\phi\quad\text{iff}\quad\xi(c)\in{[\\![\Diamond]\\!]}({[\\![\phi]\\!]}).$

Notice that the operation ${[\\![\Diamond]\\!]}$ turns predicates on $C$ into
predicates on $\mathcal{P}C$, so we speak of a _predicate lifting_.

Generally, the notion of predicate lifting is formally defined as follows. The
_contravariant powerset_ functor
$\mathcal{Q}\colon\mathsf{Set}^{\mathit{op}}\to\mathsf{Set}$ is given by
$\mathcal{Q}U=\mathcal{P}U$ for sets $U$, and by
$\mathcal{Q}f\colon\mathcal{Q}V\to\mathcal{Q}U$, $\mathcal{Q}f(Z)=f^{-1}[Z]$,
for $f\colon U\to V$. We think of $\mathcal{Q}U$ as consisting of predicates
on $U$. Then, an _$n$ -ary predicate lifting_ for $F$ is a natural
transformation

$\lambda\colon\mathcal{Q}^{n}\to\mathcal{Q}\circ F^{\mathit{op}}$

between functors $\mathsf{Set}^{\mathit{op}}\to\mathsf{Set}$. Here, we write
$\mathcal{Q}^{n}$ for the functor given by
$\mathcal{Q}^{n}U=(\mathcal{Q}U)^{n}$. Also, recall that $F^{\mathit{op}}$ is
the functor $\mathsf{Set}^{\mathit{op}}\to\mathsf{Set}^{\mathit{op}}$ that
acts like $F$ on both sets and maps. Unravelling this definition, we see that
a predicate lifting $\lambda$ is a family of maps

$\lambda_{U}\colon(\mathcal{Q}U)^{n}\to\mathcal{Q}(FU),$

indexed over all sets $U$, subject to the _naturality_ condition requiring
that the diagram

${(\mathcal{Q}V)^{n}}$${\mathcal{Q}(FV)}$${(\mathcal{Q}U)^{n}}$${\mathcal{Q}(FU)}$$\scriptstyle{\lambda_{V}}$$\scriptstyle{\mathcal{Q}(f)^{n}}$$\scriptstyle{\mathcal{Q}(Ff)}$$\scriptstyle{\lambda_{U}}$

commutes for all $f\colon U\to V$. Explicitly, this amounts to the equality

$\lambda_{U}(f^{-1}[Z_{1}],\dots,f^{-1}[Z_{n}])=(Ff)^{-1}\lambda_{V}(Z_{1},\dots,Z_{n})$

for predicates $Z_{1},\dots,Z_{n}\in\mathcal{Q}(V)$. It is easily checked that
this condition does hold for the unary predicate lifting
$\lambda={[\\![\Diamond]\\!]}$ as defined above. As examples of predicate
liftings for the above-mentioned discrete distribution functor $\mathcal{D}$,
consider the unary predicate liftings $\lambda^{b}$, indexed over
$b\in{\mathbb{Q}}\cap[0,1]$, given by

$\lambda^{b}_{U}(Y)=\\{d\in\mathcal{D}U\mid d(Y)>b\\},$

which induce next-step modalities ‘with probability more than $b$’ (see also
Example 2.2). Again, the naturality condition is readily checked. Further
instances are discussed in Example 2.

### Fixpoints

We recall basic results on fixpoints, and fix some notation. Recall that by
the Knaster-Tarski fixpoint theorem, every monotone function $f\colon X\to X$
on a complete lattice $X$ (such as a powerset lattice $X=\mathcal{P}(Y)$) has
a least fixpoint $\mu f$ and a greatest fixpoint $\nu f$, and indeed $\mu f$
is the least prefixpoint and, dually, $\nu f$ is the greatest postfixpoint of
$f$. Here, $x\in X$ is a prefixpoint (postfixpoint) of $f$ if $f(x)\leq x$
($x\leq f(x)$). We use $\mu$ and $\nu$ also as binders in expressions $\mu
X.\,E$ or $\nu X.\,E$ where $E$ is an expression, in an informal sense,
possibly depending on the parameter $X$, thus denoting $\mu f$ and $\nu f$,
respectively, for the function $f$ that maps $X$ to $E$. By the Kleene
fixpoint theorem, if $X$ is finite, then we can compute $\mu f$ as the point
$f^{n}(\bot)$ at which the ascending chain $\bot\leq f(\bot)\leq
f^{2}(\bot)\dots$ becomes stationary; dually, we compute $\nu f$ as the point
$f^{n}(\top)$ at which the descending chain $\top\leq f(\top)\leq
f^{2}(\top)\dots$ becomes stationary. More generally, this method can be
applied to unrestricted $X$ by extending the mentioned chains to ordinal
indices, taking suprema or infima, respectively, in the limit steps [CC79].

### The coalgebraic $\mu$-calculus

Next-step modalities interpreted as predicate liftings can be embedded into
ambient logical frameworks of various levels of expressiveness, such as plain
modal next-step logics [SP08, SP09] or hybrid next-step logics [MPS09]. The
_coalgebraic $\mu$-calculus_ [CKP11a] combines next-step modalities with a
Boolean propositional base and fixpoint operators, and thus serves as a
generic framework for temporal logics.

The syntax of the coalgebraic $\mu$-calculus is parametric in a _modal
similarity type_ $\Lambda$, that is, a set of modal operators with assigned
finite arities, possibly including propositional atoms as nullary modalities.
_We fix a modal similarity type $\Lambda$ for the rest of the paper._ We
assume that $\Lambda$ is closed under duals, i.e., that for each modal
operator $\heartsuit\in\Lambda$, there is a _dual_
$\overline{\heartsuit}\in\Lambda$ (of the same arity) such that
$\overline{\overline{\heartsuit}}=\heartsuit$ for all $\heartsuit\in\Lambda$.
Let $\mathbf{V}$ be a countably infinite set of _fixpoint variables_
$X,Y,\dots$. Formulae $\phi,\psi,\dots$ of the _coalgebraic $\mu$-calculus_
(over $\Lambda$) are given by the grammar

$\displaystyle\psi,\phi::=\bot\mid\top\mid\psi\wedge\phi\mid\psi\vee\phi\mid\heartsuit(\phi_{1},\dots,\phi_{n})\mid
X\mid\neg X\mid\mu X.\,\phi\mid\nu X.\,\phi\qquad$

where $\heartsuit\in\Lambda$, $X\in\mathbf{V}$, and $n$ is the arity of
$\heartsuit$. We require that negated variables $\neg X$ do not occur in the
scope of $\mu X$ or $\nu X$. As usual, $\mu$ and $\nu$ take least and greatest
fixpoints, respectively. We write $\phi[\psi/X]$ for the formula obtained by
substituting $\psi$ for $X$ in $\phi$. Full negation is not included but can
be defined as usual (in particular,
$\neg\heartsuit\phi=\overline{\heartsuit}\neg\phi$, and moreover $\neg\mu
X.\,\phi=\nu X.\,\neg\phi[\neg X/X]$ and dually; one easily checks that the
restriction on occurrences of negated variables is satisfied in the resulting
formula). Throughout, we use $\eta\in\\{\mu,\nu\\}$ as a placeholder for
fixpoint operators; we briefly refer to formulae of the form $\eta X.\,\phi$
as _fixpoints_ or _fixpoint literals_. We follow the usual convention that the
scope of a fixpoint extends as far to the right as possible. Fixpoint
operators _bind_ their fixpoint variables, so that we have standard notions of
bound and free fixpoint variables; we write $\mathsf{FV}(\phi)$ and
$\mathop{\mathsf{BV}}(\phi)$ for the sets of free and bound variables,
respectively, that occur in a formula $\phi$. A formula $\phi$ is closed if it
contains no free fixpoint variables, i.e. $\mathsf{FV}(\phi)=\emptyset$. (Note
in particular that closed formulae do not contain negated fixpoint variables,
and hence no negation at all.) We assume w.l.o.g. that fixpoints are
_irredundant_ , i.e. use their fixpoint variable at least once. In _guarded_
formulae, all occurrences of fixpoint variables are separated by at least one
modal operator from their binding fixpoint operator. Guardedness is a wide-
spread assumption although the actual blowup incurred by the transformation of
unguarded into guarded formulae depends rather subtly on the notion of formula
size [BFL15, KMV20]. We do _not_ assume guardedness in this work, see also
Remark 15. For $\heartsuit\in\Lambda$, we denote by
$\mathsf{size}(\heartsuit)$ the length of a suitable representation of
$\heartsuit$; for natural or rational numbers indexing $\heartsuit$ (cf.
Example 2), we assume binary representation. The _length_ $|\psi|$ of a
formula is its length over the alphabet
$\\{\bot,\top,\wedge,\vee\\}\cup\Lambda\cup\mathbf{V}\cup\\{\eta
X.\mid\eta\in\\{\mu,\nu\\},X\in\mathbf{V}\\}$, while the _size_
$\mathsf{size}(\psi)$ of $\psi$ is defined by counting
$\mathsf{size}(\heartsuit)$ for each $\heartsuit\in\Lambda$ (and $1$ for all
other operators).

The semantics of the coalgebraic $\mu$-calculus, on the other hand, is
parametrized by the choice of a functor $F\colon\mathsf{Set}\to\mathsf{Set}$
determining the branching type of systems, as well as predicate liftings
interpreting the modalities, as indicated in the above summary of coalgebraic
logic. That is, we interpret each modal operator $\heartsuit\in\Lambda$ as an
$n$-ary predicate lifting

${[\\![\heartsuit]\\!]}\colon\mathcal{Q}^{n}\to\mathcal{Q}\circ
F^{\mathit{op}}$

for $F$, where $n$ is the arity of $\heartsuit$, extending notation already
used in our lead-in example on the semantics of the diamond modality
$\Diamond$. To ensure existence of fixpoints, we require that all
$[\\![\heartsuit]\\!]$ are _monotone_ , i.e. whenever $A_{i}\subseteq
B_{i}\subseteq U$ for all $i=1,\dots,n$, where $n$ is the arity of
$\heartsuit$, then
$[\\![\heartsuit]\\!]_{U}(A_{1},\dots,A_{n})\subseteq[\\![\heartsuit]\\!]_{U}(B_{1}.\dots,B_{n})$.

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 the assignment of predicate liftings to modalities respects duality, i.e.

$[\\![\overline{\heartsuit}]\\!]_{U}(A_{1},\dots,A_{n})=\overline{[\\![\heartsuit]\\!]_{U}(\overline{A_{1}},\dots,\overline{A_{n}})}$

for $n$-ary $\heartsuit\in\Lambda$ and $A_{1},\dots,A_{n}\subseteq U$.

We interpret formulae over $F$-coalgebras $\xi\colon C\to FC$. A _valuation_
is a partial function $i:\mathbf{V}\rightharpoonup\mathcal{P}(C)$ that assigns
sets $i(X)$ of states to fixpoint variables $X$. Given $A\subseteq C$ and
$X\in\mathbf{V}$, we write $i[X\mapsto A]$ for the valuation given by
$(i[X\mapsto A])(X)=A$ and $(i[X\mapsto A])(Y)=i(Y)$ for $Y\neq X$. We write
$\epsilon$ for the empty valuation (i.e. $\epsilon$ is undefined on all
variables). For a list $X_{1},\dots,X_{n}$ of distinct variables, we write
$\eta[X_{1}\mapsto A_{1},\dots,X_{n}\mapsto A_{n}]$ for $\eta[X_{1}\mapsto
A_{1}]\dots[X_{n}\mapsto A_{n}]$, and $[X_{1}\mapsto A_{1},\dots,X_{n}\mapsto
A_{n}]$ for $\epsilon[X_{1}\mapsto A_{1},\dots,X_{n}\mapsto A_{n}]$. The
_extension_ $[\\![\phi]\\!]_{i}\subseteq C$ of a formula $\phi$ in $(C,\xi)$,
under a valuation $i$ such that $i(X)$ is defined for all
$X\in\mathsf{FV}(\phi)$, is given by the recursive clauses

$\displaystyle[\\![\bot]\\!]_{i}$ $\displaystyle=\emptyset$
$\displaystyle[\\![\top]\\!]_{i}$ $\displaystyle=C$
$\displaystyle[\\![X]\\!]_{i}$ $\displaystyle=i(X)$ $\displaystyle[\\![\neg
X]\\!]_{i}$ $\displaystyle=C\setminus i(X)$
$\displaystyle[\\![\phi\land\psi]\\!]_{i}$
$\displaystyle=[\\![\phi]\\!]_{i}\cap[\\![\psi]\\!]_{i}$
$\displaystyle[\\![\phi\lor\psi]\\!]_{i}$
$\displaystyle=[\\![\phi]\\!]_{i}\cup[\\![\phi]\\!]_{i}$
$\displaystyle[\\![\heartsuit(\phi_{1},\dots,\phi_{n})]\\!]_{i}$
$\displaystyle=\xi^{-1}[[\\![\heartsuit]\\!]_{C}([\\![\phi_{1}]\\!]_{i}.\dots,[\\![\phi_{n}]\\!]_{i})]$
$\displaystyle[\\![\mu X.\,\phi]\\!]_{i}$ $\displaystyle=\mu
A.\,[\\![\phi]\\!]_{i[X\mapsto A]}$ $\displaystyle[\\![\nu X.\,\phi]\\!]_{i}$
$\displaystyle=\nu A.\,[\\![\phi]\\!]_{i[X\mapsto A]}$

(using notation introduced in the fixpoint paragraph above). Thus we have
$x\in[\\![\heartsuit(\psi_{1},\dots,\psi_{n})]\\!]_{i}$ if and only if
$\xi(x)\in[\\![\heartsuit]\\!]_{C}([\\![\psi_{1}]\\!]_{i},\dots,[\\![\psi_{n}]\\!]_{i})$.
By monotonicity of predicate liftings and the restrictions on occurrences of
negated variables, one shows inductively that the functions occurring in the
clauses for $\mu X.\,\phi$ and $\nu X.\,\phi$ are monotone, so the
corresponding extremal fixpoints indeed exist according to the Knaster-Tarski
fixpoint theorem. By an evident substitution lemma, we obtain that the
extension is invariant under _unfolding_ of fixpoints, i.e.

$[\\![\eta X.\,\psi]\\!]_{i}=[\\![\psi[\eta X.\,\psi/X]]\\!]_{i}.$

For closed formulae $\psi$, the valuation $i$ is irrelevant, so we write
$[\\![\psi]\\!]$ instead of $[\\![\psi]\\!]_{i}$. A state $x\in C$ _satisfies_
a closed formula $\psi$ (denoted $x\models\psi$) if $x\in[\\![\psi]\\!]$. A
closed formula $\chi$ is _satisfiable_ if there is a coalgebra $(C,\xi)$ and a
state $x\in C$ such that $x\models\chi$.

For readability, we restrict the further technical development to unary
modalities, noting that all proofs generalize to higher arities by just
writing more indices; in fact, we will liberally use higher arities in
examples.

######  Example .

We proceed to discuss instances of the coalgebraic $\mu$-calculus, focusing
mainly on cases where no tractable set of modal tableau rules is known
(details on this point are in Remark 35). Examples where such rule sets are
available, including the alternating-time $\mu$-calculus, have been provided
by Cîrstea et al. [CKP11a].

  1. (1)

The _relational modal $\mu$-calculus_ [Koz83] (which contains CTL as a
fragment), has $\Lambda=\\{\Diamond,\Box\\}\cup P\cup\\{\neg a\mid a\in P\\}$
where $P$ is a set of propositional atoms, seen as nullary modalities, and
$\Diamond,\Box$ are unary modalities. The modalities $\Diamond$ and $\Box$ are
mutually dual ($\overline{\Diamond}=\Box$, $\overline{\Box}=\Diamond$), and
the dual of $a\in P$ is $\neg a$. The semantics is defined over _Kripke
models_ , which are coalgebras for the functor $F$ given on sets $U$ by
$FU=(\mathcal{P}U)\times\mathcal{P}(P)$ – an $F$-coalgebra assigns to each
state a set of successors and a set of atoms satisfied in the state. The
relevant predicate liftings are

$\displaystyle[\\![\Diamond]\\!]_{U}(A)$ $\displaystyle=\\{(B,Q)\in FU\mid
A\cap B\neq\emptyset\\}$ $\displaystyle[\\![\Box]\\!]_{U}(A)$
$\displaystyle=\\{(B,Q)\in FU\mid B\subseteq A\\}$
$\displaystyle[\\![a]\\!]_{U}$ $\displaystyle=\\{(B,Q)\in FU\mid a\in Q\\}$
$\displaystyle(a\in P)$ $\displaystyle[\\![\neg a]\\!]_{U}$
$\displaystyle=\\{(B,Q)\in FU\mid a\notin Q\\}$

(of course, the predicate liftings for $a\in P$ and $\neg a$ are nullary, i.e.
take no argument predicates). Standard example formulae include the CTL-
formula $\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.

  2. (2)

The two-valued _probabilistic $\mu$-calculus_ [CKP11a, LSWZ15] (not to be
confused with the real-valued probabilistic $\mu$-calculus [HK97, MM07]) is
modelled using the distribution functor $\mathcal{D}$ as discussed above;
recall in particular that $\mathcal{D}$-coalgebras are Markov chains. To avoid
triviality (see Remark 2), we include propositional atoms, i.e. we work with
coalgebras for the functor $F=\mathcal{D}\times\mathcal{P}(P)$ for a set $P$
of propositional atoms as in the previous item. We use the modal similarity
type $\Lambda=\\{\langle b\rangle,[b]\mid b\in\mathbb{Q}\cap[0,1]\\}\cup
P\cup\\{\neg a\mid a\in P\\}$, with $\langle b\rangle$ and $[b]$ mutually
dual, and again with $a\in P$ and $\neg a$ mutually dual; we interpret these
modalities by the predicate liftings

$\displaystyle[\\![\langle b\rangle]\\!]_{U}(A)$ $\displaystyle=\\{(d,Q)\in
FU\mid d(A)>b\\}$ $\displaystyle[\\![[b]]\\!]_{U}(A)$
$\displaystyle=\\{(d,Q)\in FU\mid d(U\setminus A)\leq b\\}$
$\displaystyle[\\![a]\\!]_{U}$ $\displaystyle=\\{(d,Q)\in FU\mid a\in Q\\}$
$\displaystyle[\\![\neg a]\\!]_{U}$ $\displaystyle=\\{(d,Q)\in FU\mid a\notin
Q\\}$

for sets $U$ and $A\subseteq U$ (so $[\\![\langle b\rangle]\\!]$ applies the
above-mentioned predicate liftings $\lambda^{b}$ to the
$\mathcal{D}$-component of $F$); that is, a state satisfies $\langle
b\rangle\phi$ if the probability of reaching a state satisfying $\phi$ in the
next step is more than $b$, and a state satisfies $[b]\phi$ if the probability
of reaching a state not satisfying $\phi$ in the next step is at most $b$. For
example, the formula

$\phi=\nu X.\,\mathsf{safe}\land\langle 0.95\rangle X$

expresses that the system is safe and will reach a state in which $\phi$ holds
again with probability more than $0.95$.

  3. (3)

Similarly, we interpret the _graded $\mu$-calculus_ [KSV02] over _multigraphs_
[DV02], in which states are connected by directed edges that are annotated
with non-negative integer _multiplicities_. Multigraphs correspond to
coalgebras for the _multiset functor_ $\mathcal{B}$, defined on sets $U$ by

$\mathcal{B}(U)=\\{\beta:U\to\mathbb{N}\cup\\{\infty\\}\\}.$

We view $d\in\mathcal{B}(U)$ as an integer-valued measure on $U$, and for
$V\subseteq U$ employ the same notation $d(V)=\sum_{x\in V}d(x)$ as in the
case of probability distributions. In this notation, we can, again, define
$\mathcal{B}f$, for $f\colon U\to V$, as taking image measures, i.e.
$\mathcal{B}f(d)(W)=d(f^{-1}[W])$ for $W\subseteq V$. A
$\mathcal{B}$-coalgebra $\xi\colon C\to\mathcal{B}C$ assigns a multiset
$\xi(x)$ to each state $x\in C$, which we may read as indicating that given
states $x,y\in C$, there is an edge from $x$ to $y$ with multiplicity
$\xi(x)(y)$. We use the modal similarity type $\Lambda=\\{\langle
m\rangle,[m]\mid m\in\mathbb{N}\cup\\{\infty\\}\\}$, with $\langle m\rangle$
and $[m]$ mutually dual, and define the predicate liftings

$\displaystyle[\\![\langle m\rangle]\\!]_{U}(A)$
$\displaystyle=\\{\beta\in\mathcal{B}U\mid\beta(A)>m\\}$
$\displaystyle[\\![[m]]\\!]_{U}(A)$
$\displaystyle=\\{\beta\in\mathcal{B}U\mid\beta(U\setminus A)\leq m\\}$

for sets $U$ and $A\subseteq U$. For instance, somewhat informally speaking, a
state satisfies $\nu X.\,(\psi\wedge\langle 1\rangle X)$ if it is the root of
an infinite binary tree in which all states satisfy $\psi$.

  4. (4)

The _probabilistic $\mu$-calculus with polynomial inequalities_ [KPS15]
extends the probabilistic $\mu$-calculus (item 2) by introducing, in addition
to propositional atoms as in item 2, mutually dual _polynomial modalities_
$\langle p\rangle,[p]$ for $n\in{\mathbb{N}}$,
$p\in\mathbb{Q}[X_{1},\ldots,X_{n}]$ (the set of polynomials in variables
$X_{1},\dots,X_{n}$ with rational coefficients) such that $p$ is monotone on
$[0,1]$ in all variables (in particular this holds when all coefficients of
non-constant monomials in $p$ are non-negative, but also, e.g.,
$X_{1}-\frac{1}{2}X_{1}^{2}-\frac{1}{4}$ is monotone on $[0,1]$). These
modalities are interpreted by predicate liftings defined by

$\displaystyle[\\![\langle p\rangle]\\!]_{U}(A_{1},\ldots,A_{n})$
$\displaystyle=\\{(d,Q)\in FU\mid p(d(A_{1}),\ldots,d(A_{n}))>0\\}$
$\displaystyle[\\![[p]]\\!]_{U}(A_{1},\ldots,A_{n})$
$\displaystyle=\\{(d,Q)\in FU\mid
p(d(\overline{A_{1}}),\ldots,d(\overline{A_{n}}))\leq 0\\}$

for sets $U$ and $A_{1},\ldots,A_{n}\subseteq U$. Of course, the polynomial
modalities subsume the modalities mentioned in item 2, explicitly via $\langle
b\rangle=\langle X_{1}-b\rangle$ and $[b]=[X_{1}-b]$. Polynomial inequalities
over probabilities have received some previous interest in probabilistic
logics (e.g. [FHM90, GJLS17]), in particular as they can express constraints
on independent events (and hence play a role analogous to independent products
as used in the real-valued probabilistic $\mu$-calculus [Mio11]). E.g. the
formula

$\nu Y.\,\langle X_{1}X_{2}-0.9\rangle(\mathsf{ready}\land
Y,\mathsf{idle}\land Y)$

says roughly that two independently sampled successors of the current state
will satisfy $\mathsf{ready}$ and $\mathsf{idle}$, respectively, and then
satisfy the same property again, with probability more than $0.9$.

We note that polynomial inequalities clearly increase the expressiveness of
the logic strictly, not only in comparison to the logic with operators
$\langle b\rangle$, $[b]$ as in item 2 but also w.r.t. the logic with only
linear inequalities: The restrictions on probability distributions imposed by
linear inequalities on probabilities are rational polytopes, so already
$\langle X_{1}^{2}+X_{2}^{2}-1\rangle(a,c)$ is not expressible using only
linear inequalities.

  5. (5)

Similarly, the _graded $\mu$-calculus with polynomial inequalities_ extends
the graded $\mu$-calculus with more expressive modalities $\langle
p\rangle,[p]$, again mutually dual, where in this case $n\in{\mathbb{N}}$,
$p\in{\mathbb{Z}}[X_{1},\ldots,X_{n}]$ (that is, $p$ ranges over multivariate
polynomials with integer coefficients). Again, we restrict polynomials to be
monotone in all variables; for technical simplicity, we do in this case in
fact require that all coefficients of non-constant monomials are non-negative.
To avoid triviality, we correspondingly require the coefficient $b_{0}$ of the
constant monomial to be non-positive; we refer to the number $-b_{0}$ as the
_index_ of the modality. These modalities are interpreted by the predicate
liftings

$\displaystyle[\\![\langle p\rangle]\\!]_{U}(A_{1},\ldots,A_{n})$
$\displaystyle=\\{\beta\in\mathcal{B}U\mid
p(\beta(A_{1}),\ldots,\beta(A_{n}))>0)\\}$
$\displaystyle[\\![[p]]\\!]_{U}(A_{1},\ldots,A_{n})$
$\displaystyle=\\{\beta\in\mathcal{B}U\mid
p(\beta(\overline{A_{1}}),\ldots,\beta(\overline{A_{n}}))\leq 0)\\}.$

This logic subsumes the _Presburger $\mu$-calculus_, that is, the extension of
the graded $\mu$-calculus with linear inequalities (with non-negative
coefficients), which may be seen as the fixpoint variant of _Presburger modal
logic_ [DL06]. E.g. the formula

$\mu Y.\,(a\lor\langle 3X_{1}+X_{2}^{2}-10\rangle(c\land Y,a\land Y))$

says that the current state is the root of a finite tree all whose leaves
satisfy $a$, and each of whose inner nodes has $n_{1}$ children satisfying $c$
and $n_{2}$ children satisfying $a$ where $3n_{1}+n_{2}^{2}-10>0$. The index
of the modality $\langle 3X_{1}+X_{2}^{2}-10\rangle$ is $10$.

Unlike in the probabilistic case (item 4), polynomial inequalities do not
increase the expressiveness of the graded $\mu$-calculus (item 3): Given a
polynomial $p\in{\mathbb{Z}}[X_{1},\dots,X_{n}]$, one can just replace
$\langle p\rangle(\phi_{1},\dots,\phi_{n})$ with the disjunction of all
formulae $\bigwedge_{i=1}^{n}\langle m_{i}-1\rangle\phi_{i}$ over all
solutions $(m_{1},\dots,m_{n})$ of $p(X_{1},\dots,X_{n})>0$ that are minimal
w.r.t. the componentwise ordering of ${\mathbb{N}}^{n}$. As theses minimal
solutions form an antichain in ${\mathbb{N}}^{n}$, there are only finitely
many of them [Lav76], so the disjunction is indeed finite. However, the blowup
of this translation is exponential in the binary size of the coefficient of
the constant monomial and in $n$: For instance, even the linear inequality
$X_{1}+\dots+X_{n}-nb>0$ has, by a somewhat generous estimate, at least
$(b+1)^{n-1}$ minimal solutions (one for each assignment of numbers between
$0$ and $b$ to the variables $X_{1},\dots,X_{n-1}$; more precisely, the number
of minimal solutions is the number $\binom{n+nb}{n-1}=\binom{n+nb}{nb+1}$ of
weak compositions of $nb+1$ into $n$ parts), which is exponential both in $n$
and in the binary size of $b$ (in which the polynomial itself has linear size
when $n$ is fixed). Therefore, this translation does not allow inheriting an
exponential-time upper complexity bound on satisfiability checking from the
graded $\mu$-calculus.

  6. (6)

Coalgebraic logics in general combine along functor composition, and
essentially all their properties including their algorithmic treatment
propagate; the arising composite logics are essentially typed sublogics of the
fusion, to which we refer as _multi-sorted coalgebraic logics_ [SP11]. E.g. a
logic for Markov decision processes or simple Segala systems, seen in the
simplest (in particular, single-label) version as coalgebras for the composite
functor $\mathcal{P}\circ\mathcal{D}$, have nondeterministic modalities
$\Diamond,\Box$ as well as probabilistic modalities such as $\langle
p\rangle$, $[p]$ (items 1 and 4), and distinguish two sorts of
_nondeterministic_ and _probabilistic_ formulae, respectively, with
$\Diamond,\Box$ taking probabilistic formulae as arguments and producing
nondeterministic formulae, and with $\langle p\rangle$, $[p]$ working the
other way around (so that, e.g., $\langle X^{2}-0.5\rangle\Diamond\top$ is a
probabilistic formula while $\Diamond\top\land\langle
X^{2}-0.5\rangle\Diamond\top$ is not a formula). Two further particularly
pervasive and basic functors are $(-)^{A}$, which represents indexing of
transitions (and modalities) over a fixed set $A$ of actions or labels, and
$(-)\times\mathcal{P}(P)$, which represents state-dependent valuations for a
set $P$ of propositional atoms as featured already in items 1 and 2. Our
results will therefore cover modular combinations of these features with the
logics discussed above, e.g. logics for labelled Markov chains or Markov
decision processes. We refrain from repeating the somewhat verbose full
description of the framework of multi-sorted coalgebraic logic. Instead, we
will consider only the fusion of logics in the following – since, as indicated
above, multi-sorted logics embed into the fusion [SP11], this suffices for
purposes of algorithmic satisfiability checking. We discuss the fusion of
coalgebraic logics in Remarks 4 and 36.

We remark that the modalities in items 4 and 5 are less general than in the
corresponding next-step logics [FHM90, GJLS17, DL06, KPS15] in that the
polynomials involved are restricted to be monotone; e.g. they do not support
statements of the type ‘$\phi$ is more probable than $\psi$’. This is owed to
their use in fixpoints, which requires modalities to be monotone as indicated
above.

Coalgebraic logics relate closely to a generic notion of behavioural
equivalence, which generalizes bisimilarity of transition systems. A
_morphism_ $h\colon(C,\xi)\to(D,\zeta)$ of $F$-coalgebras is a map $h\colon
C\to D$ such that the square

${C}$${D}$${FC}$${FD}$$\scriptstyle{h}$$\scriptstyle{\xi}$$\scriptstyle{\zeta}$$\scriptstyle{Fh}$

commutes. For instance, a morphism of $\mathcal{P}$-coalgebras, i.e. of
transition systems or Kripke frames, is precisely what is known as a bounded
morphism or a $p$-morphism. States $x\in C$, $y\in D$ in coalgebras $(C,\xi)$,
$(D,\zeta)$ are _behaviourally equivalent_ if there exist a coalgebra
$(E,\theta)$ and morphisms $g\colon(C,\xi)\to(E,\theta)$,
$h\colon(D,\zeta)\to(E,\theta)$ such that $g(x)=h(y)$. This notion
instantiates to standard equivalences in our running examples; e.g. as
indicated above, states in (labelled) transition systems are behaviourally
equivalent iff they are bisimilar in the usual sense [AM89], and states in
labelled Markov chains are behaviourally equivalent iff they are
probabilistically bisimilar [RdV99], [BSdV04].

In view of the definition of behavioural equivalence via morphisms of
coalgebras, we can phrase invariance of the coalgebraic $\mu$-calculus under
behavioural equivalence, generalizing the well-known bisimulation invariance
of the relational $\mu$-calculus, as invariance under coalgebra morphisms.
Formally, this takes the following shape:

######  Lemma 1 (Invariance under behavioural equivalence).

Let $h\colon(C,\xi)\to(D,\zeta)$ be a morphism of coalgebras, let $\phi$ by a
coalgebraic $\mu$-calculus formula, and let
$i:\mathbf{V}\rightharpoonup\mathcal{P}(D)$ be a valuation. Then

$[\\![\phi]\\!]_{h^{-1}i}=h^{-1}[\\![\phi]\\!]_{i}$

where $h^{-1}i$ denotes the valuation given by $h^{-1}i(X)=h^{-1}[i(X)]$.

(A similar statement has been shown for the single-variable fragment of the
coalgebraic $\mu$-calculus, with essentially the same proof [SV18]; we include
the proof here for definiteness.)

######  Proof 2.1.

By induction on $\phi$. The case for variables is trivial, the Boolean cases
are straightforward, and the case for modalities is by naturality of predicate
liftings (cf. [Pat04, Sch08]). Since we have $\nu X.\,\phi\equiv\neg\mu
X.\,\neg\phi[\neg X/X]$ semantically, and since formulae satisfying the claim
are clearly closed under negation, it suffices to carry out the induction step
for least fixpoints $\mu X.\,\phi$. We generally write
$[\\![\phi]\\!]^{X}_{i}$ for the function given by
$[\\![\phi]\\!]^{X}_{i}(A)=[\\![\phi]\\!]^{X}_{i[X\mapsto A]}$, and use the
above-mentioned fact that we can approximate $[\\![\mu
X.\,\phi]\\!]_{h^{-1}i}=\mu[\\![\phi]\\!]^{X}_{h^{-1}i}$ from below as the
union of the chain of sets
$U_{\alpha}=([\\![\phi]\\!]_{h^{-1}i}^{X})^{\alpha}(\emptyset)$, indexed over
ordinals $\alpha$; that is, $[\\![\mu
X.\,\phi]\\!]_{h^{-1}i}=\bigcup_{\alpha}U_{\alpha}$ where $U_{0}=\emptyset$,
$U_{\alpha+1}=[\\![\phi]\\!]_{h^{-1}i}^{X}(U_{\alpha})$, and
$U_{\alpha}=\bigcup_{\beta<\alpha}U_{\beta}$ for limit ordinals $\alpha$.
Similarly, $[\\![\mu X.\,\phi]\\!]_{i}=\bigcup_{\alpha}V_{\alpha}$ for
$V_{\alpha}=([\\![\phi]\\!]_{i}^{X})^{\alpha}(\emptyset)$. By commutation of
preimage with unions, we are done once we show that

$U_{\alpha}=h^{-1}V_{\alpha}.$

We proceed by a further induction on $\alpha$. The induction base $\alpha=0$,
and the limit step is, again, by commutation of preimage with unions. For
successor ordinals $\alpha+1$, we calculate as follows:

$\displaystyle U_{\alpha+1}$
$\displaystyle=[\\![\phi]\\!]_{h^{-1}i}^{X}(U_{\alpha})$
$\displaystyle=[\\![\phi]\\!]_{h^{-1}i}^{X}(h^{-1}[V_{\alpha}])$ (inner IH)
$\displaystyle=h^{-1}[[\\![\phi]\\!]_{i}^{X}(V_{\alpha})]$ (outer IH)
$\displaystyle=h^{-1}[V_{\alpha+1}].$

######  Remark 2.

As indicated in Example 2.2, Markov chains are coalgebras for the discrete
distribution functor $\mathcal{D}$. The reason why we immediately extended
Markov chains with propositional atoms is that in plain Markov chains, all
states are behaviourally equivalent and therefore satisfy the same formulae of
any coalgebraic $\mu$-calculus interpreted over Markov chains: Since for any
singleton set $1$, $\mathcal{D}1$ is again a singleton, we have a unique
$\mathcal{D}$-coalgebra structure on $1$, and every $\mathcal{D}$-coalgebra
has a unique morphism into this coalgebra. This collapse under behavioural
equivalence is avoided by adding propositional atoms.

######  Remark 3.

One important consequence of the invariance of the coalgebraic $\mu$-calculus
under coalgebra morphisms according to Lemma 1 is that the multigraph
semantics of the graded $\mu$-calculus as per Example 2.3 (and its extension
with polynomial inequalities introduced in Example 2.5) is equivalent to the
more standard Kripke semantics, i.e. the semantics over
$\mathcal{P}$-coalgebras [KSV02]. We can obtain the latter from the
definitions in Example 2.3 by converting Kripke frames into multigraphs in the
expected way, i.e. by regarding transitions in the given Kripke frame as
transitions with multiplicity $1$ in a multigraph. The conversion shows
trivially that every formula that is satisfiable over (finite) Kripke frames
is also satisfiable over (finite) multigraphs. The converse is shown by
converting a given multigraph into a Kripke model that has copies of states
and transitions according to the multiplicity of transitions in the
multigraph. The arising Kripke frame, converted back into a multigraph as
described previously, has a coalgebra morphism into the original multigraph,
implying by Lemma 1 that the copies satisfy the same formulae as the original
multigraph states. Details are given in [SV18, Lemma 2.4].

######  Remark 4 (Fusion).

The standard term _fusion_ refers to a form of combination of logics, in
particular modal logics, where the ingredients of both logics are combined
disjointly and essentially without semantic interaction, but may then be
intermingled in composite formulae. In the framework of coalgebraic logic,
this means that the fusion of coalgebraic logics with modal similarity types
$\Lambda_{i}$ interpreted over functors $F_{i}$, $i=1,2$, is formed by taking
the disjoint union $\Lambda$ of $\Lambda_{1}$ and $\Lambda_{2}$ (assuming
w.l.o.g. that $\Lambda_{1}$ and $\Lambda_{2}$ are disjoint to begin with) as
the modal similarity type, and by interpreting modalities over the product
functor $F=F_{1}\times F_{2}$ (with the product of functors computed
componentwise, e.g. $FX=F_{1}X\times F_{2}X$ for sets $X$). The predicate
lifting ${[\\![\heartsuit]\\!]}^{F}$ interpreting $\heartsuit\in\Lambda_{i}$
over $F$, for $i=1,2$, is given by

${[\\![\heartsuit]\\!]}^{F}_{X}(A)=\\{(t_{1},t_{2})\in F_{1}X\times F_{2}X\mid
t_{i}\in{[\\![\heartsuit]\\!]}^{F_{i}}_{X}(A)\\}$

where ${[\\![\heartsuit]\\!]}^{F_{i}}$ is the predicate lifting for $F_{i}$
interpreting $\heartsuit$ in the respective component logic. For example, the
fusion of the standard relational modal $\mu$-calculus (Example 2.1) and the
probabilistic $\mu$-calculus with polynomial inequalities (Example 2.4) allows
for unrestricted use of non-deterministic modalities $\Diamond,\Box$ and
probabilistic modalities $\langle p\rangle$, $[p]$ in formulae such as
$\Diamond\top\land\langle X^{2}-0.5\rangle\Diamond\top$, instead of only the
alternating discipline imposed by the two-sorted logic for Markov decision
processes described in Example 2.6; such formulae are interpreted over
coalgebras for the functor $\mathcal{P}\times\mathcal{D}$, in which every
state has both nondeterministic and probabilistic successors.

### Closure and Alternation Depth

A key measure of the complexity of a formula is its _alternation depth_ ,
which roughly speaking describes the maximal number of alternations between
$\mu$ and $\nu$ in chains of dependently nested fixpoints. The treatment of
this issue is simplified if one excludes reuse of fixpoint variables:

######  Definition 5.

A closed formula $\phi$ is _clean_ if each fixpoint variable appears in at
most one fixpoint operator in $\phi$.

_We fix a clean closed target formula $\chi$ for the remainder of the paper_,
and define the following syntactic notions relative to this target formula.
Given $X\in\mathop{\mathsf{BV}}(\chi)$, we write $\theta(X)$ for the unique
subformula of $\chi$ of the shape $\eta X.\,\psi$. We say that a fixpoint
variable $X$ is an _$\eta$ -variable_, for $\eta\in\\{\mu,\nu\\}$, if
$\theta(X)$ has the form $\eta X.\,\psi$. As indicated, the formal definition
of alternation depth simplifies within clean formulae (e.g., [Wil01, KMV20]):

######  Definition 6 (Alternation depth).

For $X,Y\in\mathop{\mathsf{BV}}(\chi)$, we write $Y\prec X$ if $\theta(Y)$ is
a subformula of $\theta(X)$, and $Y\prec_{\mathsf{dep}}X$ if additionally
$X\in\mathsf{FV}(\theta(Y))$. A _dependency chain_ in $\chi$ is a chain of the
form

$X_{n}\prec_{\mathsf{dep}}X_{n-1}\prec_{\mathsf{dep}}\dots\prec_{\mathsf{dep}}X_{0}\qquad(n\geq
0);$

the _alternation number_ of the chain is $k+1$ if $k$ is the number of indices
$i\in\\{0,\dots,n-1\\}$ such that $X_{i}$ is a $\mu$-variable iff $X_{i+1}$ is
a $\nu$-variable (i.e. the chain toggles between $\mu$\- and $\nu$-variables
at $i$). The _alternation depth_ $\mathsf{ad}(X)$ of a variable
$X\in\mathop{\mathsf{BV}}(\chi)$ is the maximal alternation number of
dependency chains as above ending in $X_{0}=X$, and the _alternation depth_ of
$\chi$ is $\mathsf{ad}(\chi):=\max\\{\mathsf{ad}(X)\mid
X\in\mathop{\mathsf{BV}}(\chi)\\}$.

(In particular, the alternation depth of $\chi$ is $0$ if $\chi$ does not
contain any fixpoints, and $1$ if $\chi$ is _alternation-free_ , i.e. no
$\nu$-variable occurs freely in $\theta(X)$ for a $\mu$-variable $X$, and vice
versa.)

######  Example 7.

The formula $\nu X.\,(\mu Y.\ a\lor\Diamond Y)\land\Box X$ (in the relational
modal $\mu$-calculus) has alternation depth $0$, i.e. is alternation-free. The
formula $\nu X.\,\Box(\mu Y.\ X\lor\Diamond Y)$ has alternation depth $1$, as
witnessed by the alternating chain $Y\prec_{\mathsf{dep}}X$.

In the automata-theoretic approach to checking for infinite deferrals,
automata states will be taken from the Fischer-Ladner closure of $\chi$ in the
usual sense [Koz83], in which subformulae of $\chi$ are expanded into closed
formulae by means of fixpoint unfolding:

######  Definition 8.

The _Fischer-Ladner closure_ $\mathbf{F}$ of $\chi$ is the least set of
formulae containing $\chi$ such that

$\displaystyle\phi\land\psi\in\mathbf{F}$
$\displaystyle\implies\phi,\psi\in\mathbf{F}$
$\displaystyle\phi\lor\psi\in\mathbf{F}$
$\displaystyle\implies\phi,\psi\in\mathbf{F}$
$\displaystyle\heartsuit\phi\in\mathbf{F}$
$\displaystyle\implies\phi\in\mathbf{F}$ $\displaystyle\eta
X.\,\phi\in\mathbf{F}$ $\displaystyle\implies\phi[\eta
X.\,\phi/X]\in\mathbf{F}.$

(One should note that although $\chi$ is clean, the elements of $\mathbf{F}$
will in general fail to be clean, as fixpoint unfolding of $\eta X.\,\phi$ as
per the last clause may create multiple copies of $\eta X.\,\phi$.)

Furthermore, we let $\mathsf{sub}(\chi)$ denote the set of subformulae of
$\chi$; unlike formulae in $\mathbf{F}$, formulae in $\mathsf{sub}(\chi)$ may
contain free fixpoint variables. The _innermost_ free fixpoint variable in a
subformula of $\chi$ is the one whose binder lies furthest to the right in
$\chi$. Each $\phi\in\mathsf{sub}(\chi)$ induces a formula
$\theta^{*}(\phi)\in\mathbf{F}$, which is obtained by repeatedly transforming
$\phi$, in each step substituting the innermost fixpoint variable $X$
occurring in the present formula with $\theta(X)$ [Koz83]. E.g. for $\chi=\mu
X.\,\nu Y.\,Y\vee\heartsuit X$, we have $Y\vee\heartsuit
X\in\mathsf{sub}(\chi)$, $\theta(X)=\chi$ and $\theta(Y)=\nu
Y.\,Y\vee\heartsuit X$, and thus

$\displaystyle\theta^{*}(Y\vee\heartsuit X)$
$\displaystyle=\theta^{*}(\theta(Y)\vee\heartsuit(X))$
$\displaystyle=\theta^{*}((\nu Y.\,Y\vee\heartsuit X)\vee\heartsuit(X))$
$\displaystyle=(\nu Y.\,Y\vee\heartsuit\theta(X))\vee\heartsuit\theta(X)$
$\displaystyle=(\nu Y.\,Y\vee\heartsuit\chi)\vee\heartsuit\chi.$

######  Lemma 9.

[Koz83] The function $\theta^{*}\colon\mathsf{sub}(\chi)\to\mathbf{F}$ is
surjective; in particular, the cardinality of $\mathbf{F}$ is at most the
number of subformulae of $\chi$.

##  3\. Tracking Automata and Model Checking Games

Generally, the main problem in model constructions for temporal logics and the
associated satisfiability checking procedures is to ensure that the unfolding
of least fixpoints does not lead to infinite deferrals, i.e. that least
fixpoints are indeed eventually satisfied. We use _parity automata_ (e.g.
[GTW02]) that track single formulae along paths through potential models to
detect infinite deferrals.

Recall that a _(nondeterministic) parity automaton_ is a tuple

$\mathsf{A}=(V,\Sigma,\Delta,q_{\mathsf{init}},\alpha)$

where $V$ is a set of _nodes_ ; $\Sigma$ is a finite set, the _alphabet_ ;
$\Delta\subseteq V\times\Sigma\times V$ is the _transition relation_ ;
$q_{\mathsf{init}}\in V$ is the _initial node_ ; and $\alpha:V\to\mathbb{N}$
is the _priority function_ , which assigns priorities $\alpha(v)\in\mathbb{N}$
to states $v\in V$. We write $\Delta(v,a)=\\{u\mid(v,a,u)\in\Delta\\}$ for
$v\in V$, $a\in\Sigma$. If $\Delta$ is a (partial) functional relation, then
$\mathsf{A}$ is said to be _deterministic_ , and we denote the corresponding
partial function by $\delta:V\times\Sigma\rightharpoonup V$. The automaton
$\mathsf{A}$ _accepts_ an infinite word
$w=w_{0},w_{1},\ldots\in\Sigma^{\omega}$ if there is a $w$-path 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\Sigma^{\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
$(q_{\mathsf{init}},w_{0},q_{1}),(q_{1},w_{1},q_{2}),\ldots\in\Delta^{\omega}$
(starting in the initial state $q_{\mathsf{init}}$).

Recall moreover that we are working with a fixed clean closed target formula
$\chi$. We put

$n_{0}=|\chi|,\quad n_{1}=\mathsf{size}(\chi),\quad k=\mathsf{ad}(\phi).$

The states of the tracking automaton for $\chi$ will be the elements of the
Fischer-Ladner closure $\mathbf{F}$ of $\chi$ (cf. Section 2); in particular,
$|\mathbf{F}|\leq n_{0}$.

######  Definition 10.

Given a set $Z$, we write

$\Lambda(Z)=\\{\heartsuit z\mid\heartsuit\in\Lambda,z\in Z\\},$

and refer to elements of $\Lambda(Z)$ as _modal literals_ (over $Z$).

In particular, $\mathbf{F}\cap\Lambda(\mathbf{F})$ is the set of modal
literals in $\mathbf{F}$. We put

$\mathsf{selections}=\mathcal{P}(\mathbf{F}\cap\Lambda(\mathbf{F})),$

and indeed refer to elements of this set as _selections_ , with a view to
using selections as letters for modal steps in our automata construction.
Furthermore, we let
$\mathbf{F}_{\vee}=\\{\psi\vee\chi\mid\psi\vee\chi\in\mathbf{F}\\}$ denote the
set of disjunctive formulae contained in $\mathbf{F}$, and put

$\displaystyle\mathsf{choices}=\\{\tau:\mathbf{F}_{\vee}\to\mathbf{F}\mid\forall(\psi\vee\chi)\in\mathbf{F}_{\vee}.\,\tau(\psi\vee\chi)\in\\{\psi,\chi\\}\\};$

that is, $\mathsf{choices}$ consists of _choice functions_ that pick disjuncts
from disjunctions. These choice functions will be used as letters for
propositional steps in the tracking automaton. We note
$|\mathsf{selections}|,|\mathsf{choices}|\leq 2^{n_{0}}$.

######  Definition 11 (Tracking automaton).

The _tracking automaton_ for $\chi$ is the nondeterministic parity automaton
$\mathsf{A}_{\chi}=(\mathbf{F},\Sigma,\Delta,q_{\mathsf{init}},\alpha)$ where
$q_{\mathsf{init}}=\chi$, $\Sigma=\mathsf{choices}\cup\mathsf{selections}$,
and for $\psi\in\mathbf{F}$, $\tau\in\mathsf{choices}$ and
$\kappa\in\mathsf{selections}$,

$\displaystyle\Delta(\psi,\tau)$
$\displaystyle=\begin{cases}\emptyset&\text{if $\psi\in\\{\top,\bot\\}$}\\\
\tau(\psi)&\text{if $\psi\in\mathbf{F}_{\vee}$}\\\
\\{\psi_{0},\psi_{1}\\}&\text{if $\psi=\psi_{0}\wedge\psi_{1}$}\\\
\\{\psi_{1}[\psi/X]\\}&\text{if $\psi=\eta X.\,\psi_{1}$}\\\
\\{\psi\\}&\text{if $\psi=\heartsuit\psi_{0}$ for some
$\heartsuit\in\Lambda$}\end{cases}$ $\displaystyle\Delta(\psi,\kappa)$
$\displaystyle=\begin{cases}\\{\psi_{0}\\}&\text{if
$\psi=\heartsuit\psi_{0}\in\kappa$ for some $\heartsuit\in\Lambda$}\\\
\emptyset&\text{otherwise}\end{cases}$

Propositional tracking along a choice function $\tau\in\mathsf{choices}$ thus
follows the choice of $\tau$ for disjunctions; the only nondeterministic
states are conjunctions, for which both conjuncts are tracked; fixpoint
literals $\eta X.\,\psi_{1}$ are tracked to their unfolding
$\psi_{1}[\psi/X]$; modal literals are left unchanged by propositional
tracking steps. A modal literal $\psi=\heartsuit\psi_{0}$ is only tracked (to
$\psi_{0}$) through a selection $\kappa$ if $\heartsuit\psi_{0}\in\kappa$,
i.e. if $\kappa$ selects $\heartsuit\psi_{0}$ to be tracked.

The priority function $\alpha$ is derived from the alternation depths of
variables, counting only unfoldings of fixpoints (i.e. all other formulae have
priority 1) and ensuring that least fixpoints receive even priority and
greatest fixpoints receive odd priority. That is, we put

$\displaystyle\alpha(\mu X.\phi)$ $\displaystyle=2\cdot\mathsf{ad}(X)$
$\displaystyle\alpha(\nu X.\phi)$ $\displaystyle=2\cdot\mathsf{ad}(X)-1$
$\displaystyle\alpha(\psi)$ $\displaystyle=1$ if $\psi$ is not a fixpoint
literal.

Intuitively, words from $\Sigma^{\omega}$ encode infinite paths through
coalgebras $(C,\xi)$ in which states $x\in C$ are labelled with sets $l(x)$ of
formulae, where letters $\kappa\in\mathsf{selections}$ encode modal steps from
states $x\in C$ with label $l(x)$ to states $y\in C$ with label
$\\{\psi\mid\heartsuit\psi\in\kappa\cap l(x)\\}$ (while propositional steps
track formulae within the label $l(x)$ of a state $x$ without moving to a
different state). In this view, the automaton is built to accept

$L(\mathsf{A}_{\chi})=\mathsf{BadBranch}_{\chi}$

where $\mathsf{BadBranch}_{\chi}$ is the set of infinite words that encode a
path on which a least fixpoint formula $\psi$ is unfolded infinitely often
without being dominated by any outer fixpoint formula $\phi$, i.e. one with
$\mathsf{ad}(\phi)>\mathsf{ad}(\psi)$. Here, we use the term _dominated_ to
indicate both the greater alternation depth of $\phi$ and the fact that $\phi$
is also unfolded infinitely often. Letters $\tau\in\mathsf{choices}$ choose
disjuncts from disjunctions, and for conjunctions $\psi_{0}\wedge\psi_{1}$,
the tracking automaton is nondeterministic, reflecting the fact that
infinitely unfolded fixpoints can reside either in $\psi_{0}$ or in
$\psi_{1}$.

######  Remark 12.

The above definition of tracking automata deviates from the one we used in
earlier work [HS19] in two respects: We now attach priorities to the states of
the automaton rather than to its transitions; and we have changed
propositional tracking in such a way that composite propositional formulae are
always processed when present. Both choices serve mainly to ease and clarify
the presentation.

The automaton $\mathsf{A}_{\chi}$ has size $n_{0}$ and priorities $1$ to $k$.
Using a standard construction (e.g. [KKV01]), we transform
$\mathsf{\mathsf{A}_{\chi}}$ into an equivalent Büchi automaton of size
$n_{0}k$. Then we determinize the Büchi automaton using, e.g., the
Safra/Piterman-construction [Saf88, Pit07] and obtain an equivalent
deterministic parity automaton with priorities $0$ to $2n_{0}k-1$ and of size
$\mathcal{O}(((n_{0}k)!)^{2})$. Finally we complement this parity automaton by
increasing every priority by 1, obtaining a deterministic parity automaton

$\mathsf{B}_{\chi}=(D_{\chi},\Sigma,\delta,q_{\mathsf{init}},\Omega)$ (1)

of size $\mathcal{O}(((n_{0}k)!)^{2})$ and with $2n_{0}k$ priorities such that

$\displaystyle
L(\mathsf{B}_{\chi})=\overline{L(\mathsf{A}_{\chi})}=\overline{\mathsf{BadBranch}_{\chi}}=:\mathsf{GoodBranch}_{\chi},$

i.e. $\mathsf{B}_{\chi}$ is a deterministic parity automaton that accepts the
words that encode paths along which satisfaction of least fixpoints is never
deferred indefinitely.

We refer to $\mathsf{B}_{\chi}$ as the _co-determinized tracking automaton_
and define a labelling function

$l^{A}\colon D_{\chi}\to\mathcal{P}(\mathbf{F})$

that maps each state of $\mathsf{B}_{\chi}$ (e.g. a Safra tree) to the set of
formulae that occur in it. That is, the labelling function forgets the
structuring of the set of formulae in macrostates. In all
(history-)determinization procedures that we refer to in this work, labels in
this sense evolve under transitions like macrostates in the standard powerset
construction, i.e. we have

$l^{A}(\delta(q,a))=\bigcup\\{\Delta(\psi,a)\mid\psi\in
l^{A}(q)\\}\qquad\text{for $q\in D_{\chi}$, $a\in\Sigma$,
$\psi\in\mathbf{F}$.}$ (2)

In particular,

$l^{A}(\delta(q,\kappa))=\\{\psi\mid\heartsuit\psi\in\kappa\cap
l^{A}(q)\\}\qquad\text{for $q\in D_{\chi}$, $\kappa\in\mathsf{selections}$}.$
(3)

######  Remark 13.

It has been noted that for the relational $\mu$-calculus, tracking automata
for _aconjunctive_ formulae are _limit-deterministic_ parity automata [HSD18].
These considerably simpler automata can be determinized to deterministic
parity automata of size $\mathcal{O}((n_{0}k)!)$ and with $2n_{0}k$ priorities
[EKRS17, HSD18], an observation that can also be used for the tracking
automata in this work. For aconjunctive formulae, Lemma 32 below yields a
correspondingly lower bound on the runtime of our satisfiability checking
algorithm.

It has also been shown that tracking automata for _guarded_ and _alternation-
free_ formulae can be seen as Co-Büchi automata [FLL13] so that the simpler
determinization procedure for Co-Büchi automata [MH84] can be used for such
formulae. However, in our setting the tracking automata have to correctly deal
with unguarded fixpoint variables and hence assign priorities greater than $1$
exclusively to fixpoint formulae (for instance priority $2$ is assigned to
formulae of the shape $\mu X.(\psi\vee\Diamond X)$ but priority $1$ is
assigned to formulae of the shape $\psi\vee\Diamond(\mu X.(\psi\vee\Diamond
X))$ even though the latter formula arises by unfolding the fixpoint in the
former formula) so that our tracking automata are not immediately Co-Büchi
automata when the target formula is alternation-free. Having said that, it
indeed is possible to use Co-Büchi automata for _unguarded_ alternation-free
formulae, namely by separating local and global tracking and using two
different automata, one being a reachability automaton used for detecting
infinite local unfolding of unguarded least fixpoint formulae and the other
being a Co-Büchi automaton used for detecting global deferral of guarded least
fixpoints; this method has been described in [EJ99]. We refrain from
introducing this more involved setup here, so for the moment, our results do
not immediately allow the use of Co-Büchi methods for unguarded alternation-
free formulae.

######  Remark 14.

_History-deterministic_ automata [HP06] allow a limited amount of non-
determinism but still can easily be complemented and combined with a game
arena to obtain a game (and hence have been introduced under the name _good-
for-games automata_). They allow nondeterministic transitions under the
condition that all nondeterministic choices in an accepting run can be
resolved by looking only at the history of the run so far. Intuitively, the
non-determinism in history-deterministic automata cannot make guesses about
the future of runs. It follows from the results by Henzinger and Piterman
[HP06] that instead of full determinization of $\mathsf{A}_{\chi}$, it
suffices to turn $\mathsf{A}_{\chi}$ into an equivalent history-deterministic
automaton, which then can be complemented and used instead of
$\mathsf{B}_{\chi}$ in the global caching algorithm below. For general
formulae, $\mathsf{A}_{\chi}$ is a parity automaton and can be history-
determinized by first transforming to a Büchi automaton and then using the
method for history-determinization of Büchi automata described in [HP06]. This
method is conceptually simpler than full determinization of Büchi automata by
the Safra-Piterman construction and avoids constructing Safra-trees, even
though it does not reduce the number of states in the obtained automaton in
comparison to full determinization.

######  Remark 15 (Tracking automata for unguarded formulae).

A tableau-based method for deciding satisfiability of unguarded formulae of
the relational $\mu$-calculus has beein introduced by Friedmann and Lange
[FL13]. The method augments states in the tracking automaton with an
additional bit indicating _activity_ of formulae (meaning that the respective
formula has been manipulated by the last transition of the tracking
automaton), doubling the size of the tracking automaton. The acceptance
condition of the tracking automaton then is modified in order to accept only
such branches that contain some trace that is both infinitely often active and
on which some least fixpoint is unfolded infinitely often without being
dominated. As the propositional tableau rules in [FL13] manipulate one
propositional formula at a time, one also needs to introduce an additional
tableau rule in order to ensure fairness of unfolding of unguarded fixpoint
formulae.

In the current work we define propositional transitions of the tracking
automaton $A_{\chi}$ in such a way that all propositional formulae are
processed whenever a single propositional letter $\tau\in\mathsf{choices}$ is
read. Hence fairness of fixpoint unfolding is inherent to our method.
Moreover, the only inactive transitions (i.e. transitions that do not
manipulate the tracked formula) in $A_{\chi}$ are transitions of the shape
$(\heartsuit\psi,\tau,\heartsuit\psi)$ for some modal literal
$\heartsuit\psi$. Since $\Omega(\heartsuit\psi)=1$, all accepting runs of
$A_{\chi}$ are active by construction. Thus our method readily handles
unguarded formulae without requiring an activity bit.

### Model Checking Games

It will be technically convenient to use a game characterization of
$\mu$-calculus semantics. Recall that parity games are infinite-duration two-
player games, played by the _existential_ and the _universal_ player. A parity
game is given by a tuple

$\mathsf{G}=(V_{\forall},V_{\exists},E,v_{0},\Omega)$

where $V=V_{\forall}\cup V_{\exists}$ is a set of _nodes_ , partitioned
disjointly into the set $V_{\exists}$ of nodes owned by the existential player
and the set $V_{\forall}=V\setminus V_{\exists}$ of nodes owned by the
universal player; $E\subseteq V\times V$ is the set of _moves_ ; $v_{0}$ is an
_initial node_ and $\Omega:V\to\mathbb{N}$ is the _priority function_ , which
assigns priorities $\Omega(v)\in\mathbb{N}$ to states $v\in V$. We write
$E(v)=\\{v^{\prime}\in V\mid(v,v^{\prime})\in E\\}$ for $v\in V$. A play $\pi$
is a maximal path through $(V,E)$, i.e. $\pi$ is either infinite or ends in a
node $v$ such that $E(v)=\emptyset$. A play $\pi$ is winning for the
existential player if it is finite and ends with the universal player being
stuck, or if it is infinite and the highest priority that is visited
infinitely often on $\pi$ is even; otherwise, $\pi$ is winning for the
universal player. Formally, $\pi$ is _winning_ for the existential player if
either $\pi=v_{0},v_{1},\ldots,v_{n}$ is finite and $v_{n}\in V_{\forall}$, or
$\pi$ is infinite and $\max(\mathsf{Inf}(\Omega\circ\pi))$ is even, where,
given an infinite sequence $S$, $\mathsf{Inf}(S)$ denotes the set of elements
that occur infinitely often in $S$. In writing $\Omega\circ\pi$, we see
infinite sequences, such as $\pi$, as functions on $\mathbb{N}$. A _strategy_
for the existential player is a partial function
$s:V^{*}V_{\exists}\rightharpoonup V$ such that
$(v_{n},s(v_{0},v_{1},\ldots,v_{n}))\in E$ for all partial plays
$v_{0},v_{1},\ldots,v_{n}\in V^{*}V_{\exists}$ on which $s$ is defined. A play
$\pi=v_{0},v_{1},\ldots$ is _compatible_ with (or _follows_) a strategy $s$
for the existential player if $v_{n+1}=s(v_{0},\ldots,v_{n})$ (in particular,
$s(v_{0},\ldots,v_{n})$ is defined) for all $i$ such that $v_{n}\in
V_{\exists}$ and $v_{n}$ is not the last node in $\pi$. A strategy $s$ is
_history-free_ if $s(v_{0},\ldots,v_{n-1},v_{n})$ depends only on $v_{n}$;
then $s$ is a partial function from $V_{\exists}$ to $V$. The existential
player wins a node $v\in V$ if there is a strategy $s$ such that every play
that starts at $v$ and is compatible with $s$ is won by the existential
player; similar notions of (winning) strategies for the universal player are
defined dually. The game $\mathsf{G}$ is won by the player that wins $v_{0}$.

######  Lemma 16 ([Mar75, EJ91]).

Parity games are history-free determined, that is, every node is won by
(exactly) one of the two players, and then there is a history-free strategy
that wins the node for the respective player.

Given a parity game $\mathsf{G}$ with set of nodes $V$ and a set $W\subseteq
V$, we let $\mathsf{win}^{\exists}_{W}$ and $\mathsf{win}^{\forall}_{W}$
denote the set of nodes for which the respective player has a winning strategy
in $\mathsf{G}$ such that every play that is compatible with the strategy
remains within $W$. Nodes $v\in W$ such that
$v\notin\mathsf{win}^{\exists}_{W}\cup\mathsf{win}^{\forall}_{W}$ are
undetermined (w.r.t. $W$); for such $v$, neither player has a strategy that
wins $v$ while staying in $W$. As parity games are determined, we always have
$V=\mathsf{win}^{\exists}_{V}\cup\mathsf{win}^{\forall}_{V}$. We write
$\mathsf{win}^{\exists}$ for $\mathsf{win}^{\exists}_{V}$ and
$\mathsf{win}^{\forall}$ for $\mathsf{win}^{\forall}_{V}$.

Winning regions in parity games are clearly invariant under bisimulation (e.g.
[CKW18]). Explicitly, given parity games
$\mathsf{G}=(V_{\forall},V_{\exists},E,\Omega)$,
$\mathsf{G}^{\prime}=(V^{\prime}_{\forall},V^{\prime}_{\exists},E^{\prime},\Omega)$
(we elide initial nodes), a relation $R\subseteq V\times V^{\prime}$ is a
_bisimulation_ if whenever $(v,u)\in R$, then $v$ and $u$ are owned by the
same player; $\Omega(v)=\Omega^{\prime}(u)$; and the following conditions on
moves hold:

  * •

_forth_ : Whenever $(v,v^{\prime})\in E$, then there exists $(u,u^{\prime})\in
E^{\prime}$ such that $(v^{\prime},u^{\prime})\in R$; and

  * •

_back_ : Whenever $(u,u^{\prime})\in E^{\prime}$,then there exists
$(v,v^{\prime})\in E$ such that $(v^{\prime},u^{\prime})\in R$.

As usual, a _bounded morphism_ $f\colon\mathsf{G}\to\mathsf{G}^{\prime}$ is a
map $f\colon V\to V^{\prime}$ whose graph is a bisimulation.

######  Lemma 17.

Let $\mathsf{G}=(V_{\forall},V_{\exists},E,\Omega)$,
$\mathsf{G}^{\prime}=(V^{\prime}_{\forall},V^{\prime}_{\exists},E^{\prime},\Omega)$
be parity games, and let $R\subseteq V\times V^{\prime}$ be a bisimulation.
Given $(v_{0},u_{0})\in R$, $\exists$ wins $v_{0}$ in $\mathsf{G}$ iff
$\exists$ wins $u_{0}$ in $\mathsf{G}^{\prime}$.

We give a proof for the sake of self-containedness:

######  Proof 3.1.

By symmetry, it suffices to prove ‘only if’. Let $s$ be a history-free
strategy for $\exists$ that wins $v_{0}$. Then $\exists$ wins $u_{0}$ by means
of a history-dependent strategy $s^{\prime}$ that, on nodes $u$ in
$\mathsf{G}^{\prime}$, maintains the invariant that there is a node $v$ in
$\mathsf{G}$ such that $(v,u)\in R$; the history dependence is due to the node
$u$ being kept in memory, and we write $s^{\prime}(v,u)$ for the move in
$\mathsf{G}^{\prime}$ recommended by $s^{\prime}$ when in node $u$, with $v$
witnessing the invariant. The invariant holds initially by assumption. At a
node $u\in V^{\prime}$, and given $v\in V$ as in the invariant, we distinguish
cases on the joint ownership of $v$ and $u$. If $v\in V_{\forall}$ and $u\in
V^{\prime}_{\forall}$, then $\forall$’s move in $\mathsf{G}^{\prime}$
preserves the invariant by the back condition. If $v\in V_{\exists}$ and $u\in
V^{\prime}_{\exists}$, then by the forth condition, we can pick
$s^{\prime}(v,u)$ in $\mathsf{G}^{\prime}$ in such a way that $s(v)$ witnesses
the invariant.

It remains to show that $s^{\prime}$ is winning; so let
$\pi=u_{0},u_{1},\dots$ be a play in $\mathsf{G}^{\prime}$ that follows
$s^{\prime}$. By the invariant, we obtain a sequence
$\overline{\pi}=v_{0},v_{1},\dots$ of nodes in $\mathsf{G}$ such that
$(v_{i},u_{i})\in R$ for all $i$, and by the way the $v_{i}$ have been picked
above, $\overline{\pi}$ is a play in $\mathsf{G}$ that follows $s$, and hence
is won by $\exists$. Since $\Omega(v_{i})=\Omega^{\prime}(u_{i})$ for all $i$,
it follows that $\exists$ wins $\pi$.

We next provide a parity game characterization of formula satisfaction. This
characterization highlights the close relationship between satisfaction of
fixpoints and (non-)acceptance of runs in the tracking automaton
$\mathsf{A}_{\chi}$.

######  Definition 18 (Model checking games).

Given a coalgebra $(C,\xi)$, the _model checking game_
$\mathsf{G}_{\chi,(C,\xi)}=(V_{\exists},V_{\forall},E,\Omega)$ for $\chi$ over
$(C,\xi)$ is a parity game with sets of nodes $V=V_{\exists}\cup V_{\forall}$
defined by

$\displaystyle V_{\exists}$ $\displaystyle=C\times\mathbf{F}_{\exists}$
$\displaystyle V_{\forall}$
$\displaystyle=(C\times\mathbf{F}_{\forall})\cup(\mathcal{P}(C)\times\mathbf{F}).$

Here, $\mathbf{F}_{\exists}$ consists of those formulae in $\mathbf{F}$ that
are disjunctions, modal literals, fixpoint literals, or $\bot$, while
$\mathbf{F}_{\forall}=\mathbf{F}\setminus\mathbf{F}_{\exists}$ consists of
those formulae in $\mathbf{F}$ that are conjunctions or $\top$. The moves and
priorities in the game are given by the following table (the ownership of
nodes is already defined, and mentioned in the table only for readability)

node | owner |  set of allowed moves | priority
---|---|---|---
$(x,\psi)$ |  $\exists$/$\forall$ |  $\\{(x,\phi)\in\\{x\\}\times\Delta(\psi,\tau)\mid\tau\in\mathsf{choices}\\}$ | $\alpha(\psi)-1$
$(x,\heartsuit\psi)$ | $\exists$ |  $\\{(D,\phi)\in\mathcal{P}(C)\times\Delta(\heartsuit\psi,\kappa)\mid\kappa\in\mathsf{selections},\xi(x)\in[\\![\heartsuit]\\!]D\\}$ | $0$
$(D,\psi)$ | $\forall$ |  $\\{(x,\psi)\mid x\in D\\}$ | $0$

Thus the existential player can move from $(x,\psi_{1}\vee\psi_{2})$ to
$(x,\psi_{i})$ for any $i\in\\{1,2\\}$; each such move is witnessed by any
$\tau\in\mathsf{choices}$ such that $\tau(\psi_{1}\vee\psi_{2})=\psi_{i}$. The
universal player can move from $(x,\psi_{1}\wedge\psi_{2})$ to $(x,\psi_{i})$
for any $i\in\\{1,2\\}$. For fixpoint literals $\psi=\eta X.\,\phi$, the
existential player moves from $(x,\psi)$ to $(x,\phi[\psi/X])$. For modalities
$\heartsuit\psi$, the existential player can move from $(x,\heartsuit\psi)$ to
$(D,\psi)$ for any set $D\subseteq C$ such that
$\xi(x)\in[\\![\heartsuit]\\!]D$; each such move is witnessed by any
$\kappa\in\mathsf{selections}$ such that $\heartsuit\psi\in\kappa$, hence
$\Delta(\heartsuit\psi,\kappa)=\\{\psi\\}$. The universal player in turn can
challenge satisfaction of $\psi$ at any state $x\in D$ contained in the set
$D$ provided by the existential player by moving from $(D,\psi)$ to
$(x,\psi)$. The definition of $\Omega$ implies that the only nodes with non-
zero priority are those of the form $(x,\eta X.\,\psi)$, with $\Omega(x,\eta
X.\,\psi)$ being even if $\eta=\nu$, and odd if $\eta=\mu$.

For technical purposes, we introduce a variant of the model checking game, the
_subformula model checking game_ $\mathsf{G}^{\mathsf{sub}}_{\chi,(C,\xi)}$.
The nodes of $\mathsf{G}^{\mathsf{sub}}_{\chi,(C,\xi)}$ have the same shape as
those of $\mathsf{G}_{\chi,(C,\xi)}$ except that subformulae occur in nodes of
$\mathsf{G}^{\mathsf{sub}}_{\chi,(C,\xi)}$ wherever elements of $\mathbf{F}$
occur in nodes of $\mathsf{G}_{\chi,(C,\xi)}$. The ownership, priorities, and
outgoing moves of nodes are defined in
$\mathsf{G}^{\mathsf{sub}}_{\chi,(C,\xi)}$ in the same way as in
$\mathsf{G}_{\chi,(C,\xi)}$, in particular for nodes of the form $(x,\psi)$
follow the same cases according to the outermost connective of $\psi$, except
for the following provisos: Given a variable $X$ such that $\theta(X)=\eta
X.\,\psi$, nodes of the shape $(x,\eta X.\,\psi)$ or $(x,X)$ receive priority
$\Omega(x,\theta^{*}(X))=\alpha(\theta^{*}(X))-1$ and belong to $\exists$, who
has only one move, to $(x,\psi)$.

We note that the two versions of the model checking games are bisimilar, and
hence equivalent (Lemma 17):

######  Lemma 19.

The assignment $f(x,\psi)=(x,\theta^{*}(\psi))$,
$f(D,\psi)=(D,\theta^{*}(\psi))$ defines a bounded morphism
$f\colon\mathsf{G}^{\mathsf{sub}}_{\chi,(C,\xi)}\to\mathsf{G}_{\chi,(C,\xi)}$.

######  Proof 3.2.

It is clear that $f$ preserves priorities and node ownership. We check the
conditions on moves, restricting attention to the only cases where the games
differ appreciably, viz., fixpoint literals and fixpoint variables. At such
nodes, however, the outgoing moves are uniquely determined in both games, so
we just have to show that $f$ preserves these moves.

So let $X$ be a fixpoint variable, with $\theta(X)=\eta X.\,\psi$. The unique
move from both $(x,X)$ and $(x,\eta X.\,\psi)$ in
$\mathsf{G}^{\mathsf{sub}}_{\chi,(C,\xi)}$ leads to $(x,\psi)$. Since
$\theta^{*}(X)=\theta^{*}(\eta X.\psi)$, $(X,x)$ and $(X,\eta X.\,\psi)$ are
mapped to the same node under $f$, and this node has the form $(x,\eta
X.\psi^{\prime})$ where $\psi^{\prime}$ is obtained from $\psi$ by
successively substituting free fixpoint variables $Y$ with $\theta(Y)$
innermost first, but skipping the actual innermost variable $X$ in $\psi$; so
$\theta^{*}(\psi)=\theta^{*}(\psi[\eta X.\psi/X])=\psi^{\prime}[\eta
X.\psi^{\prime}/X])$. From $(x,\eta X.\psi^{\prime})$, $\exists$’s unique move
in $\mathsf{G}_{\chi,(C,\xi)}$ thus leads to $(x,\psi^{\prime}[\eta
X.\psi^{\prime}/X]=(x,\theta^{*}(\psi))=f(x,\psi)$, as required.

The model checking game $\mathsf{G}_{\chi,(C,\xi)}$ is very similar to the one
considered by Cîrstea et al. [CKP+11b], one notable difference being that we
do not assume guardedness. On the other hand, the subformula model checking
game $\mathsf{G}^{\mathsf{sub}}_{\chi,(C,\xi)}$ resembles a game that was
considered by Venema [Ven06] but which, again, assumes guardedness and
moreover works with a version of the coalgebraic $\mu$-calculus based on the
coalgebraic cover modality [Mos99] instead of on predicate liftings. Indeed,
the proof of correctness given by Cîrstea et al. is largely by reference to
Venema’s proof, an argument that is formally justified by our Lemma 19. Due to
the mentioned guardedness issue, we opt to present a full correctness proof of
our game. A central role in this proof is played by timeouts that measure how
often least fixpoints are unfolded in a given model:

######  Definition 20 (Satisfaction under timeouts).

We assume that the fixpoint variables in $\chi$ are $X_{1},\dots,X_{k}$, in
order of their occurrence in $\chi$ (with $X_{1}$ being leftmost), and fix
designators $\psi_{j}$ such that $\theta(X_{j})$ has the form $\eta
X_{j}.\,\psi_{j}$ for the rest of the section.

A _timeout vector_ $\overrightarrow{m}=(\lambda_{1},\ldots,\lambda_{j})$ of
length $j$ consists of $j$ ordinal numbers $\lambda_{i}$. The set of timeout
vectors is totally ordered by lexicographic ordering, that is,
$(\lambda_{1},\ldots,\lambda_{j})<(\lambda^{\prime}_{1},\ldots,\lambda^{\prime}_{j})$
if and only if there is $1\leq i\leq j$ such that
$\lambda_{i}<\lambda^{\prime}_{i}$ and
$\lambda_{i^{\prime}}=\lambda^{\prime}_{i^{\prime}}$ for all $1\leq
i^{\prime}<i$. When comparing timeout vectors of different lengths, we regard
shorter vectors as smaller than longer vectors as usual. Given a timeout
vector $\overrightarrow{m}=(\lambda_{1},\ldots,\lambda_{j})$, we define the
valuation $i_{\lambda_{1},\ldots,\lambda_{j}}$ on $\\{X_{1},\dots,X_{j}\\}$
recursively by
$i_{\lambda_{1},\ldots,\lambda_{j}}(X_{i})=i_{\lambda_{1},\ldots,\lambda_{j-1}}(X_{i})$
for $i<j$, and

$\displaystyle
i_{\lambda_{1},\ldots,\lambda_{j}}(X_{j})=\begin{cases}\emptyset&X_{j}\text{ a
$\mu$-variable},\;\lambda_{j}=0\\\
[\\![\psi_{j}]\\!]_{i_{\lambda_{1},\ldots,\lambda_{j-1},\lambda^{\prime}_{j}}}&X_{j}\text{
a $\mu$-variable},\;\lambda_{j}=\lambda^{\prime}_{j}+1\\\
\bigcup_{\lambda<\lambda_{j}}i_{\lambda_{1},\ldots,\lambda_{j-1},\lambda}(X_{j})&X_{j}\text{
a $\mu$-variable},\;\lambda_{j}\text{ a limit ordinal}\\\ [\\![\nu
X_{j}.\,\psi_{j}]\\!]_{i_{\lambda_{1},\ldots,\lambda_{j-1}}}&X_{j}\text{ a
$\nu$-variable},\end{cases}$

where the index vector $(\lambda_{1},\dots,\lambda_{j})$ serves as a
termination measure. Notice that entries $\lambda_{j}$ corresponding to
$\nu$-variables $X_{j}$ are never used in the above definition; they are
present only for ease of notation. If there is some timeout vector
$\overrightarrow{m}$ such that $x\in[\\![\psi]\\!]_{i_{\overrightarrow{m}}}$,
then there also is a minimal such $\overrightarrow{m}$ (w.r.t. lexicographic
ordering). We write $\overrightarrow{m}_{x,\psi}$ for this minimal timeout
vector.

By monotonicity, we have $x\in[\\![\psi]\\!]_{i_{\overrightarrow{m}}}$ for
every $\overrightarrow{m}\geq\overrightarrow{m}_{x,\psi}$. Notice also that in
minimal timeout vectors $\overline{m}=(\lambda_{1},\dots,\lambda_{k})$, the
purely formal components $\lambda_{j}$ corresponding to $\nu$-variables
$X_{j}$ are always $0$, since the valuation $i_{\overline{m}}$ does not depend
on them.

Given a coalgebra $(C,\xi)$, a formula $\psi$, a valuation $i$ of the fixpoint
variables, and a fixpoint variable $X$ that occurs freely in $\psi$, we define
the function $[\\![\psi]\\!]^{X}_{i}:\mathcal{P}(C)\to\mathcal{P}(C)$ by
$[\\![\psi]\\!]^{X}_{i}(A)=[\\![\psi]\\!]_{i[X\mapsto A]}$ (so $[\\![\mu
X.\,\psi]\\!]_{i}$ is the least fixpoint of $[\\![\psi]\\!]^{X}_{i}$). Recall
that for $f:\mathcal{P}(C)\to\mathcal{P}(C)$, the repeated application
$f^{\lambda}(A)$ of $f$ to $A\subseteq C$ is defined by $f^{0}(A)=A$,
$f^{\lambda+1}(A)=f(f^{\lambda}(A))$, and
$f^{\lambda}(A)=\bigcup_{\lambda^{\prime}<\lambda}f^{\lambda^{\prime}}(A)$ if
$\lambda$ is a limit ordinal. Now suppose that $X_{j}$ is a $\mu$-variable. As
mentioned in Section 2, we have $[\\![\mu
X_{j}.\,\psi_{j}]\\!]_{i_{\lambda_{1},\ldots,\lambda_{j-1}}}=([\\![\psi_{j}]\\!]^{X_{j}}_{i_{\lambda_{1},\ldots,\lambda_{j-1}}})^{|C|}(\emptyset)$.
We claim that

$\displaystyle([\\![\psi_{j}]\\!]^{X_{j}}_{i_{\lambda_{1},\ldots,\lambda_{j-1}}})^{\lambda}(\emptyset)=i_{\lambda_{1},\ldots,\lambda_{j-1},\lambda}(X_{j})$

for all ordinal numbers $\lambda$. The proof is by transfinite induction on
$\lambda$. The induction base and the limit step are straightforward; the
successor step is as follows:

$\displaystyle([\\![\psi_{j}]\\!]^{X_{j}}_{i_{\lambda_{1},\ldots,\lambda_{j-1}}})^{\lambda+1}(\emptyset)$
$\displaystyle=[\\![\psi_{j}]\\!]_{i_{\lambda_{1},\ldots,\lambda_{j-1}}}^{X_{j}}(([\\![\psi_{j}]\\!]^{X_{j}}_{i_{\lambda_{1},\ldots,\lambda_{j-1}}})^{\lambda}(\emptyset))$
$\displaystyle=[\\![\psi_{j}]\\!]_{i_{\lambda_{1},\ldots,\lambda_{j-1}}}^{X_{j}}(i_{\lambda_{1},\dots,\lambda_{j-1},\lambda}(X_{j}))$
$\displaystyle(\text{IH})$
$\displaystyle=[\\![\psi_{j}]\\!]_{i_{\lambda_{1},\ldots,\lambda_{j-1}}[X_{j}\mapsto
i_{\lambda_{1},\dots,\lambda_{j-1},\lambda}(X_{j})]}$
$\displaystyle(\text{definition})$
$\displaystyle=[\\![\psi_{j}]\\!]_{i_{\lambda_{1},\ldots,\lambda_{j-1},\lambda}}$
$\displaystyle=i_{\lambda_{1},\ldots,\lambda_{j-1},\lambda+1}(X_{j})$
$\displaystyle(\text{definition}).$

In particular, we thus have

$[\\![\mu
X_{j}.\,\psi_{j}]\\!]_{i_{\lambda_{1},\ldots,\lambda_{j-1}}}=i_{\lambda_{1},\dots,\lambda_{j-1},|C|}(X_{j}).$
(4)

We now have all preparations in hand to prove correctness of the model
checking game:

######  Lemma 21.

Given a coalgebra $(C,\xi)$, a state $x\in C$ and a formula
$\psi\in\mathbf{F}$, we have $x\models\psi$ if and only if the existential
player wins the node $(x,\psi)$ in $\mathsf{G}_{\chi,(C,\xi)}$.

######  Proof 3.3.

We note first that the positions reachable from $(x,\psi)$ in
$\mathsf{G}_{\chi,(C,\xi)}$ are the same as in $\mathsf{G}_{\psi,(C,\xi)}$, so
we can assume w.l.o.g. that $\psi$ is the target formula, that is, that
$\psi=\chi$.

Next, to simplify the proof conceptually, we modify both versions of the model
checking game ($\mathsf{G}_{\chi,(C,\xi)}$ and
$\mathsf{G}^{\mathsf{sub}}_{\chi,(C,\xi)}$, cf. Definition 18) to obtain
symmetry between the players. First, we reassign positions of the form $(x,\nu
X.\,\psi)$ or, in the case of $\mathsf{G}^{\mathsf{sub}}_{\chi,(C,\xi)}$,
$(x,X)$ with $X$ a $\nu$-variable, to the universal player – since these
positions have precisely one outgoing move, this change is clearly immaterial
to how the game is played. Second, out of every pair
$\heartsuit,\overline{\heartsuit}$ of dual modalities, we arbitrarily assign
one to $\exists$ and the other to $\forall$, and from now on we write
$\heartsuit$ for modalities assigned to $\exists$, and $\overline{\heartsuit}$
for modalities assigned to $\forall$. Moreover, we rename the previous
positions of the form $(D,\psi)$ into $(D,\psi,\forall)$, and introduce
additional positions $(D,\psi,\exists)$. Positions of the form
$(x,\heartsuit\psi)$ still belong to $\exists$, with moves like before, into
the renamed positions of the form $(D,\psi,\forall)$, which still belong to
$\forall$. On the other hand, positions of the form
$(x,\overline{\heartsuit}\psi)$ now belong to $\forall$, and $\forall$ can
move to $(D,\psi,\exists)$ if

$\xi(x)\notin{[\\![\overline{\heartsuit}]\\!]}_{C}(\overline{D})$

where $\overline{D}$ denotes complement in $C$. The new positions
$(D,\psi,\exists)$ belong to $\exists$, who can move to $(y,\psi)$ such that
$y\in D$. The new sequences of moves
$(x,\overline{\heartsuit}\psi)\xrightarrow{\forall}(D,\psi,\exists)\xrightarrow{\exists}(y,\psi)$
are, for purposes of $\exists$ winning the game, equivalent to the previous
sequences
$(x,\overline{\heartsuit}\psi)\xrightarrow{\exists}(D,\psi)\xrightarrow{\forall}(y,\psi)$:
In either case, $\exists$ can force the game into a set $U$ of positions of
the form $(y,\psi)$, necessarily of the form $U=D\times\\{\psi\\}$, iff
$\xi(x)\in{[\\![\overline{\heartsuit}]\\!]}_{C}(D)$. To see this for the new
moves
$(x,\overline{\heartsuit}\psi)\xrightarrow{\forall}(D,\psi,\exists)\xrightarrow{\exists}(y,\psi)$,
we reason as follows: $\exists$ can force the game into $D\times\psi$ iff
$\forall$ cannot move to $(D^{\prime},\psi,\exists)$ for any subset
$D^{\prime}\subseteq\overline{D}$ iff
$\xi(x)\in{[\\![\overline{\heartsuit}]\\!]}_{C}(\overline{D}^{\prime})$ for
all $D^{\prime}\subseteq\overline{D}$ iff
$\xi(x)\in{[\\![\overline{\heartsuit}]\\!]}_{C}(D)$, where the last step uses
monotonicity of $\overline{\heartsuit}$.

The claim of the lemma amounts to showing that in $\mathsf{G}_{\chi,(C,\xi)}$,

  1. (1)

if $x\models\chi$, then $\exists$ wins $(x,\chi)$; and

  2. (2)

if $x\not\models\chi$, then $\forall$ wins $(x,\chi)$.

The symmetrization of the game introduced above allows us to conclude (2) from
(1), as follows: If $x\not\models\chi$, then $x\models\neg\chi$ (with
$\neg\chi$ defined by taking negation normal forms as indicated in Section 2).
By (1), $\exists$ wins the node $(x,\neg\chi)$ in the model checking game for
$\neg\chi$. This game is now dual to the model checking game for $\chi$ in the
sense that one is obtained from the other by swapping the positions of the
players and dualizing the priorities (i.e. swapping priorities $2n$ and
$2n-1$); of course, nodes $(x,\neg\psi)$ in the game for $\neg\chi$ correspond
to nodes $(x,\psi)$ in the game for $\chi$. We thus immediately obtain that
$\forall$ wins $(x,\chi)$.

It remains to prove (1). By Lemmas 17 and 19, we can equivalently work with
the subformula model checking game $\mathsf{G}^{\mathsf{sub}}_{\chi,(C,\xi)}$
(Definition 18) in place of $\mathsf{G}_{\chi,(C,\xi)}$. The winning strategy
$s$ for $\exists$ is to maintain the following invariant at positions of the
form $(y,\phi)$:

> $y\in[\\![\phi]\\!]_{i_{\overrightarrow{m}}}$ for some timeout vector
> $\overrightarrow{m}$.

Since we start at $(x,\chi)$, the invariant holds initially: Since $\chi$ is
closed, we have $x\in[\\![\chi]\\!]_{i_{\epsilon}}=[\\![\chi]\\!]$ by
assumption (with $\epsilon$ denoting the empty timeout vector).

We show first that moves of the universal player preserve the invariant,
distinguishing on the form of $\phi$. For $\phi=\top$, there is nothing to
show. The remaining cases are as follows.

  * •

$\phi=\phi_{1}\wedge\phi_{2}$: By the invariant,

$\displaystyle
y\in[\\![\phi]\\!]_{i_{\overrightarrow{m}}}=[\\![\phi_{1}\wedge\phi_{2}]\\!]_{i_{\overrightarrow{m}}}=[\\![\phi_{1}]\\!]_{i_{\overrightarrow{m}}}\cap[\\![\phi_{2}]\\!]_{i_{\overrightarrow{m}}}.$

The universal player can move from $(y,\phi_{1}\wedge\phi_{2})$ to
$(y,\phi_{b})$ where $b\in\\{1,2\\}$; by the above, the invariant holds for
$(y,\phi_{b})$. We note that
${\overrightarrow{m}_{y,\phi_{b}}}\leq{\overrightarrow{m}_{y,\phi}}$.

  * •

$\phi=\overline{\heartsuit}\phi_{1}$: As noted above, from these nodes,
$\exists$ can force the game into the same sets of nodes $(z,\phi_{1})$ after
the next two steps as in the original game, in which all modal nodes are owned
by $\exists$. The analysis is thus the same as for modal nodes
$(y,\heartsuit\phi_{1})$ owned by $\exists$, carried out further below.

  * •

$\phi=\nu X_{j}.\,\psi_{j}$: Then $\overrightarrow{m}$ can be assumed to have
length $j-1$. The universal player moves to $(y,\psi_{j})$, and we have

$\displaystyle y$ $\displaystyle\in{[\\![\nu
X_{j}.\,\psi_{j}]\\!]}_{i_{\overrightarrow{m}}}$
$\displaystyle(\text{invariant})$
$\displaystyle={[\\![\psi_{j}]\\!]}_{i_{\overrightarrow{m}}[X_{j}\mapsto{[\\![\nu
X_{j}.\,\psi_{j}]\\!]}_{i_{\overrightarrow{m}}}]}$
$\displaystyle(\text{fixpoint unfolding})$
$\displaystyle={[\\![\psi_{j}]\\!]}_{i_{\overrightarrow{m},0}}$
$\displaystyle(\text{definition})$

where $\overrightarrow{m},0$ denotes the vector that extends
$\overrightarrow{m}$ with a last entry $0$.

  * •

$\phi=X_{j}$ where $X_{j}$ is a $\nu$-variable. In this case
$\overrightarrow{m}$ can be assumed to have length $j$, and hence is of the
form $\overrightarrow{m}=\overrightarrow{m}^{\prime},\lambda_{j}$. We have

$\displaystyle y$ $\displaystyle\in{[\\![X_{j}]\\!]}_{i_{\overrightarrow{m}}}$
$\displaystyle(\text{invariant})$ $\displaystyle={[\\![\nu
X_{j}.\,\psi_{j}]\\!]}_{i_{\overrightarrow{m}^{\prime}}}$
$\displaystyle(\text{definition})$
$\displaystyle={[\\![\psi_{j}]\\!]}_{i_{\overrightarrow{m}^{\prime}}[X_{j}\mapsto{[\\![\nu
X_{j}.\,\psi_{j}]\\!]}_{i_{\overrightarrow{m}^{\prime}}}]}$
$\displaystyle(\text{fixpoint unfolding})$
$\displaystyle={[\\![\psi_{j}]\\!]}_{i_{\overrightarrow{m}}}$
$\displaystyle(\text{definition})$

Next, we construct $s$ on positions $(y,\phi)\in V_{\exists}$, distinguishing
cases on the shape of $\phi$, and commenting in each case on how the minimal
timeout vector evolves. By the invariant, $\phi\neq\bot$. The remaining cases
are as follows.

  * •

$\phi=\phi_{1}\lor\phi_{2}$: It follows from the invariant that

$y\in[\\![\phi_{1}\lor\phi_{2}]\\!]_{i_{\overrightarrow{m}_{y,\phi}}}=[\\![\phi_{1}]\\!]_{i_{\overrightarrow{m}_{y,\phi}}}\cup[\\![\phi_{2}]\\!]_{i_{\overrightarrow{m}_{y,\phi}}}.$

Thus, $y\in[\\![\gamma_{b}]\\!]_{i_{\overrightarrow{m}_{y,\gamma}}}$ for some
$b\in\\{1,2\\}$, so we can put $s(y,\phi)=(y,\phi_{b})$, preserving the
invariant. We note that the minimal timeout vector does not increase, that is,
${\overrightarrow{m}_{y,\phi_{b}}}\leq{\overrightarrow{m}_{y,\phi}}$.

  * •

$\phi=\mu X_{j}.\,\psi_{j}$. We can assume that $\overrightarrow{m}$ has
length $j-1$. We necessarily put $s(y,\phi)=(y,\psi_{j})$. The invariant is
preserved, as we have

$\displaystyle y$ $\displaystyle\in{[\\![\mu
X_{j}.\,\psi_{j}]\\!]}_{i_{\overrightarrow{m}}}$
$\displaystyle(\text{invariant})$
$\displaystyle={[\\![\psi_{j}]\\!]}_{i_{\overrightarrow{m}}[X_{j}\mapsto{[\\![\mu
X_{j}.\,\psi_{j}]\\!]}_{i_{\overrightarrow{m}}}]}$
$\displaystyle(\text{fixpoint unfolding})$
$\displaystyle={[\\![\psi_{j}]\\!]}_{i_{\overrightarrow{m},|C|}}$
$\displaystyle(\text{\ref{eq:mu-to}}).$

The minimal timeout vector thus remains unchanged in the first $j-1$
components, and receives a new $j$-th component (at most $|C|$).

  * •

$\phi=X_{j}$: Again, we necessarily put $s(x,X_{j})=(x,\psi_{j})$. By the
invariant, $y\in i_{\overrightarrow{m}}(X_{j})$. We can assume that
$\overrightarrow{m}$ has length $j$ and moreover is minimal. By the definition
of $i_{\overrightarrow{m}}$, it is then immediate that the $j$-th component of
$\overrightarrow{m}$ is not a limit ordinal (and non-zero), so
$\overrightarrow{m}$ has the shape
$\overrightarrow{m}=(\lambda_{1},\dots,\lambda_{j-1},\lambda+1)$. By the
definition of $i_{\overrightarrow{m}}$, we thus have
$y\in[\\![\psi_{j}]\\!]_{i_{\lambda_{1},\ldots,\lambda_{j-1},\lambda}}$. This
establishes the invariant; crucially, the minimal timeout vector strictly
decreases.

  * •

$\phi=\heartsuit\phi_{1}$: We put
$s(y,\phi)=([\\![\phi_{1}]\\!]_{i_{\overrightarrow{m}}},\phi_{1})$; to see
that this is a valid move, note that the invariant
$y\in[\\![\heartsuit\phi_{1}]\\!]_{i_{\overrightarrow{m}}}$ is equivalent to
$\xi(y)\in[\\![\heartsuit]\\!]([\\![\phi_{1}]\\!]_{i_{\overrightarrow{m}}})$
by the semantics. After the subsequent move of $\forall$, we reach a position
$(z,\phi_{1})$ where $z\in[\\![\phi_{1}]\\!]_{i_{\overrightarrow{m}}}$; so the
invariant has been preserved, and the minimal timeout vector does not
increase.

It remains to show that $s$ is a winning strategy. So let $\rho$ be a play of
$\mathsf{G}^{\mathsf{sub}}_{\chi,(C,\xi)}$ that starts at $(x,\chi)$ and is
compatible with $s$. By the invariant that $s$ maintains, we have a sequence
of minimal timeout vectors under which the subformulae occurring in $\rho$ are
satisfied at the corresponding states. By the above analysis of the moves,
these timeout vectors

  * •

decrease strictly when $\rho$ passes a $\mu$-variable $X_{j}$;

  * •

receive a new last component $|C|$ when $\rho$ passes a least fixpoint literal
$\mu X_{j}.\,\psi_{j}$;

  * •

receive a new (purely formal) last component $0$ when $\rho$ passes a greatest
fixpoint literal;

  * •

and otherwise do not increase.

Thus, if for some $\mu$-variable $X_{j}$, $\rho$ visits $\mu X_{j}.\,\psi_{j}$
or $X_{j}$ infinitely often, then $\rho$ must visit $\mu X_{j}.\,\psi_{j}$
infinitely often. However, the only way to reach $\mu X_{j}.\,\psi_{j}$ again
after visiting it once is via an unfolding step for some variable $X_{i}$ such
that we have a dependency chain (Definition 6)
$X_{j}\prec_{\mathsf{dep}}\dots\prec_{\mathsf{dep}}X_{i}$ (namely, we must
reach $\mu X_{j}.\,\psi_{j}$ from some formula containing it as a subformula,
which once we have passed $\mu X_{j}.\,\psi_{j}$ can only happen if we unfold
a variable $X_{i}$, with $\theta(X_{i})=\eta X_{i}.\,\psi_{i}$, such that $\mu
X_{j}.\,\psi_{j}$ is a subformula of $\psi_{i}$; the fact that $X_{i}$ occurs
after $\mu X_{j}.\,\psi_{j}$ in $\rho$ implies that we have the required
dependency chain). So some such variable $X_{i}$ is unfolded infinitely often.
Since $\mathsf{ad}(X_{i})>\mathsf{ad}(X_{j})$, this means that the highest
priority that occurs infinitely often on $\rho$ cannot be associated to a
$\mu$-variable, i.e. cannot be odd; in other words, $\exists$ wins $\rho$.

##  4\. Global Caching for the Coalgebraic $\mu$-Calculus

We now introduce a generic global caching algorithm for satisfiability in the
coalgebraic $\mu$-calculus. This algorithm is rooted to some degree in
developments in the theory of coalgebra automata [KV08], that is, automata
that accept coalgebras satisfying given parity conditions, in generalization
of alternating parity tree automata. In particular, it has been shown that
formulae of the coalgebraic $\mu$-calculus can be translated to equivalent so-
called $\Lambda$-automata, a variant of coalgebra automata in which
transitions are based on a variant of one-step satisfiability [FLV10].
Satisfiability checking then reduces to emptiness-checking of such automata.
The global caching algorithm that we present here can be seen as an algorithm
that efficiently decides the emptiness problem of $\Lambda$-automata, and in
particular avoids solving the satisfiability games of doubly exponential size
that were used originally [FLV10], even when no suitable set of modal tableau
rules is provided.

For a given input formula $\chi$, our algorithm constructs the co-determinized
tracking automaton $\mathsf{B}_{\chi}$ (from (1)) step by step and propagates
(un)satisfiability through this graph; the algorithm terminates as soon as the
initial node $q_{\mathsf{init}}$ is marked as (un)satisfiable. The algorithm
bears similarity to standard game-based algorithms for $\mu$-calculi [FL13,
HSD18]; 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 reachable modal transitions, as well as one of the outgoing
transitions from each reachable disjunction, within the automaton
$\mathsf{B}_{\chi}$ in such a way that the resulting sub-automaton is totally
accepting, that is, accepts any word for which there is an infinite run. In
order for this to be possible, it is crucial that the labels of state nodes
$v$ in the reduced automaton are _one-step 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 _one-step satisfiability checking_ , a functor-
specific problem that in many instances can be solved in time singly
exponential in $\mathsf{size}(\chi)$.

######  Definition 22 (One-step satisfiability problem [Sch07, SP08, MPS09]).

Let $V$ be a finite set, and let $\Theta\subseteq\mathcal{P}(V)$. We interpret
$a\in V$ and $\gamma\subseteq\Lambda(V)$ over $\Theta$ by

$\displaystyle[\\![a]\\!]^{\Theta}_{0}$ $\displaystyle=\\{u\in\Theta\mid a\in
u\\}$ $\displaystyle[\\![\gamma]\\!]^{\Theta}_{1}$
$\displaystyle=\textstyle\bigcap_{\heartsuit
a\in\gamma}[\\![\heartsuit]\\!]_{\Theta}[\\![a]\\!]^{\Theta}_{0}.$

We refer to the data $(\gamma,\Theta)$ as a _one-step pair_ (over $V$). We say
that $(\gamma,\Theta)$ is _satisfiable_ (over $F$) if
$[\\![\gamma]\\!]^{\Theta}_{1}\neq\emptyset$. The _strict one-step
satisfiability problem_ is to decide whether a given one-step pair
$(\gamma,\Theta)$ is satisfiable; here, the qualification ‘strict’ refers to
the measure of input size of the problem, which we take to be

$b=\mathsf{size}(\gamma)+|V|$

where $\mathsf{size}(\gamma)=\sum_{\heartsuit
a\in\gamma}(1+\mathsf{size}(\heartsuit))$ (note that $|\Theta|$ may be
exponential in $b$).

######  Remark 23.

We keep the definition of the actual one-step logic as mentioned in the
introduction somewhat implicit in the above definition of the one-step
satisfiability problem. In a more explicitly syntactic view, one will regard
$V$ as a set of propositional variables. One then sees that a one-step pair
contains two layers: a purely propositional layer embodied in $\Theta$, which
postulates which propositional formulae over $V$ are satisfiable (that is, we
see $\Theta\subseteq\mathcal{P}(V)$ as a disjunctive normal form
$\bigvee_{A\in\Theta}\bigwedge_{a\in A}a$); and a modal layer with nesting
depth of modalities uniformly equal to $1$, embodied in the set $\gamma$,
which specifies a constraint $\bigwedge_{\heartsuit a\in\gamma}\heartsuit a$
on an element of $F\Theta$.

######  Remark 24.

Earlier definitions of the one-step satisfiability problem [KPS22] have
included conditions on one-step pairs that in the present notation amount to
restricting attention to one-step pairs $(\gamma,\Theta)$ over $V$ such that
$\gamma$ mentions every element of $V$ exactly once. In this variant, the size
of an input $(\gamma,\Theta)$ to the strict one-step satisfiability problem
can be taken to be just $\mathsf{size}(\gamma)$. The more general version of
the problem defined above reduces to the restricted version by transforming a
one-step pair $(\gamma,\Theta)$ over $V$ into an equisatisfiable one-step pair
$(\gamma^{\prime},\Theta^{\prime})$ over $V^{\prime}$ satisfying the above
requirement, given by

$\displaystyle V^{\prime}$ $\displaystyle=\\{a_{\heartsuit}\mid\heartsuit a\in
v\\}$ $\displaystyle\gamma^{\prime}$ $\displaystyle=\\{\heartsuit
a_{\heartsuit}\mid\heartsuit a\in\gamma\\}$ $\displaystyle\Theta^{\prime}$
$\displaystyle=f[\Theta]\text{ where }f(u)=\\{a_{\heartsuit}\in V^{\prime}\mid
a\in u\\}.$

Equisatisfiability is seen as follows: For one direction, suppose that
$t\in{[\\![\gamma]\\!]}^{\Theta}_{1}$. We note that
$f^{-1}[{[\\![a_{\heartsuit}]\\!]}_{0}^{\Theta^{\prime}}]={[\\![a]\\!]}_{0}^{\Theta}$
for each $a_{\heartsuit}\in V^{\prime}$, since for $u\in\Theta$,
$a_{\heartsuit}\in f(u)$ iff $a\in u$ by definition of $f$. Thus, for
$\heartsuit a\in\gamma$, we obtain $Ff(t)\in{[\\![\heartsuit
a_{\heartsuit}]\\!]}_{1}^{\Theta^{\prime}}$ from $t\in{[\\![\heartsuit
a]\\!]}^{\Theta}_{1}$ by naturality of ${[\\![\heartsuit]\\!]}$, so that
$Ff(t)\in{[\\![\gamma^{\prime}]\\!]}^{\Theta^{\prime}}_{1}$. Conversely,
suppose that $s\in{[\\![\gamma^{\prime}]\\!]}^{\Theta^{\prime}}_{1}$. Pick a
right inverse $e\colon\Theta^{\prime}\to\Theta$ of the surjective map
$f\colon\Theta\to\Theta^{\prime}$. Then, using the previous calculation, we
have
$e^{-1}[{[\\![a]\\!]}^{\Theta}_{0}]=e^{-1}[f^{-1}[{[\\![a_{\heartsuit}]\\!]}_{0}^{\Theta^{\prime}}]]={[\\![a_{\heartsuit}]\\!]}_{0}^{\Theta^{\prime}}$
for $\heartsuit a\in\gamma$, so by same argument as above,
$Fe(s)\in{[\\![\gamma]\\!]}^{\Theta}_{1}$.

######  Example 25.

  1. (1)

For the _relational modal $\mu$-calculus_ (Example 2.1.), where
$\Lambda=\\{\Diamond,\Box\\}$, the one-step satisfiability problem is to
decide, for a given one-step pair $(\gamma,\Theta)$ over $V$, whether there is
$A\in[\\![\gamma]\\!]^{\Theta}_{1}$, that is, a subset $A\in\mathcal{P}\Theta$
such that for each $\Diamond a\in\gamma$, there is $u\in A$ such that $a\in
u$, and for each $\Box b\in\gamma$ and each $u\in A$, $b\in u$. Equivalently,
one needs to check that for each $\Diamond a\in\gamma$ there is $u\in\Theta$
such that $a\in u$ and moreover $b\in u$ for all $\Box b\in\gamma$. This can
be done in time
$\mathcal{O}(\mathsf{size}(\gamma)\cdot|V|\cdot|\Theta|)=\mathcal{O}((\mathsf{size}(\gamma))\cdot|V|\cdot
2^{|V|})$, showing that in this case the strict one-step satisfiability
problem is in ExpTime. We note that this is all the work that will be required
to instantiate our generic complexity bound (Corollary 33 below) to the
relational $\mu$-calculus, obtaining the known upper bound ExpTime for
satisfiability checking [EJ99].

  2. (2)

For the _graded $\mu$-calculus_ (Example 2.3.), the one-step satisfiability
problem is to decide, for a one-step pair $(\gamma,\Theta)$, whether there is
a multiset $\beta\in\mathcal{B}\Theta$ such that $\sum_{u\in\Theta\mid a\in
u}\beta(u)>m$ for each $\langle m\rangle a\in\gamma$ and $\sum_{u\in\Theta\mid
a\notin u}\beta(u)\leq m$ for each $[m]a\in\gamma$. The easiest way to see
that the strict one-step satisfiability problem is in ExpTime is via a
nondeterministic polynomial-space algorithm that goes through all
$u\in\Theta$, guessing multiplicities $\beta(u)\in\\{0,\dots,m+1\\}$ where $m$
is the greatest index of any diamond modality $\langle m\rangle$ that occurs
in $\gamma$. This multiplicity is used to update $|V|$ counters that keep
track of the total measure $\beta({[\\![a]\\!]}^{\Theta}_{0})$ for $a\in V$
and then forgotten, so that only polynomial space is used (for the counters).
Once all multiplicities have been guessed, the algorithm verifies that
$\beta\in{[\\![\gamma]\\!]}^{\Theta}_{1}$, using only the final counter values
[KSV02, Lemma 1]. Essentially the same method works also for the _graded
$\mu$-calculus with polynomial inequalities_ (Example 2.5) (and similar ideas
have been used in work on Presburger modal logic [DL06]): In this setting, it
still suffices to guess multiplicities up to $b+1$ where $b$ is the largest
index of any diamond modality $\langle p\rangle$ occurring in $\gamma$
(indeed, if anything the bounds become smaller; e.g. for $\langle
X_{1}^{2}+X_{2}^{2}-b\rangle$, it suffices to explore multiplicities up to
$\lceil\sqrt{b}\rceil+1$).

  3. (3)

For the _probabilistic $\mu$-calculus with polynomial inequalities_ (Example
2.4), we first observe, following [GJLS17, KPS22], that a small model property
holds for the one-step logic: If a one-step pair $(\gamma,\Theta)$ over $V$ is
satisfiable, then ${[\\![\gamma]\\!]}^{\Theta}_{1}$ contains an element
$(d,Q)\in\mathcal{D}\Theta\times\mathcal{P}(P)$ such that $d(u)>0$ for only
$|V|$-many $u\in\Theta$. This is seen as follows: Suppose that
$(d_{0},Q)\in{[\\![\gamma]\\!]}^{\Theta}_{1}$. Then for any
$d\in\mathcal{D}\Theta$, to have $(d,Q)\in{[\\![\gamma]\\!]}^{\Theta}_{1}$ it
suffices that

$d({[\\![a]\\!]}^{\Theta}_{0})=d_{0}({[\\![a]\\!]}^{\Theta}_{0})$

for each $a\in V$. Since
$d({[\\![a]\\!]}^{\Theta}_{0})=\sum_{u\in{[\\![a]\\!]}^{\Theta}_{0}}d(u)$,
this means that the numbers $y_{u}=d(u)$, for $u\in\Theta$, form a non-
negative solution to the system of linear equations

$\sum_{u\in{[\\![a]\\!]}^{\Theta}_{0}}y_{u}=d_{0}([\\![a]\\!]^{u}_{0})\qquad\text{for
$a\in V$}.$

Since this system has a solution induced by $d_{0}$ itself, we obtain by the
Carathéodory theorem (e.g. [Sch86]) that there is a solution with at most
$|V|$ non-zero components. This allows us to solve the strict one-step
satisfiability problem in non-deterministic polynomial space, and hence in
exponential time, as follows: Guess $|V|$ elements $u\in\Theta$ that receive
positive weight $d(u)$ in a solution $d$, and then check for satisfiability of
the constraint on these $|V|$ real numbers that is embodied in $\gamma$. This
constraint is a polynomially-sized system of polynomial inequalities, whose
satisfiability can, by results of Canny [Can88], be checked in polynomial
space.

######  Remark 26 (One-step polysize model property).

We say that the logic has the _one-step polysize model property (OSPMP)_ if
there is a polynomial $p$ such that whenever a one-step pair $(\gamma,\Theta)$
over $V$ is satisfiable, then $[\\![\gamma]\\!]^{\Theta}_{1}$ has an element
of the form $Fi(t)$ where $i\colon\Theta_{0}\to\Theta$ is the inclusion of a
subset $\Theta_{0}\subseteq\Theta$ such that $|\Theta_{0}|\leq p(|V|)$
[KPS22]. For instance, the arguments in Examples 25.1 and 25.3 show that the
relational $\mu$-calculus and the probabilistic $\mu$-calculus (even with
polynomial inequalities) both have the OSPMP. Similar arguments as for the
probabilistic case show that the graded $\mu$-calculus (even with polynomial
inequalities) also has the OSPMP, using the integer Carathéodory theorem
[ES06]; cf. [KPS22] for details. Our model construction in Section 5 will
establish that the OSPMP implies a polynomially branching model property
(Remark 47).

The following stability property of one-step satisfiability is guaranteed by
naturality and monotonicity of predicate liftings:

######  Lemma 27.

Let $V$, $V^{\prime}$ be finite sets, $\gamma\subseteq\Lambda(V)$,
$\Theta\subseteq\mathcal{P}(V)$,
$\Theta^{\prime}\subseteq\mathcal{P}(V^{\prime})$, and $g\colon V\to
V^{\prime}$; put $\gamma_{g}=\\{\heartsuit g(a)\mid\heartsuit a\in\gamma\\}$.
Suppose that for each $u\in\Theta$, there exists
$u^{\prime}\in\Theta^{\prime}$ such that $g[u]\subseteq u^{\prime}$. If
$(\gamma,\Theta)$ is satisfiable, then so is $(\gamma_{g},\Theta^{\prime})$.

######  Proof 4.1.

Let $t\in{[\\![\gamma]\\!]}^{\Theta}_{1}$, and let
$f\colon\Theta\to\Theta^{\prime}$ witness the existential assumption of the
statement; that is, $g[u]\subseteq f(u)$ for each $u\in\Theta$. We claim that
$Ff(t)\in{[\\![\gamma_{g}]\\!]}^{\Theta^{\prime}}_{1}$. So let $\heartsuit
a\in\gamma$; we have to show
$Ff(t)\in[\\![\heartsuit]\\!]_{\Theta^{\prime}}[\\![g(a)]\\!]^{\Theta^{\prime}}_{0}$.
The defining property of $f$ implies that
$f(u)\in{[\\![g(a)]\\!]}^{\Theta^{\prime}}_{0}$ whenever
$u\in{[\\![a]\\!]}^{\Theta}_{0}$, so ${[\\![a]\\!]}^{\Theta}_{0}\subseteq
f^{-1}[{[\\![g(a)]\\!]}^{\Theta^{\prime}}_{0}]$. Since
$t\in[\\![\heartsuit]\\!]_{\Theta^{\prime}}[\\![a]\\!]^{\Theta}_{0}$, we thus
obtain
$t\in[\\![\heartsuit]\\!]_{\Theta^{\prime}}f^{-1}[[\\![a]\\!]^{\Theta^{\prime}}_{0}]$
by monotonicity of $\heartsuit$, so
$Ff(t)\in[\\![\heartsuit]\\!]_{\Theta^{\prime}}[\\![a]\\!]^{\Theta^{\prime}}_{0}$
by naturality.

We now introduce a characterization of satisfiability by means of standard
parity games. These games are won by the existential player if and only if the
target formula is satisfiable; we defer the proof of this fact to Section 5.

######  Definition 28 (Satisfiability game).

Recall that
$\mathsf{B}_{\chi}=(D_{\chi},\Sigma,\delta,q_{\mathsf{init}},\Omega)$ is the
co-determinized tracking automaton for the target formula $\chi$, and comes
with the labeling function $l^{A}:D_{\chi}\to\mathcal{P}(\mathbf{F})$. The
_satisfiability game_
$\mathsf{G}_{\chi}=(V_{\exists},V_{\forall},E,\Omega^{\prime})$ for $\chi$ is
a parity game with sets

$\displaystyle V_{\exists}$ $\displaystyle=D_{\chi}\times\\{0,1\\}$
$\displaystyle V_{\forall}$
$\displaystyle=D_{\chi}\cup(D_{\chi}\times\mathcal{P}(\mathsf{selections})).$

of nodes. The moves and the priorities in $\mathsf{G}_{\chi}$ are defined by
the following table, where $q\in D_{\chi}$ and
$\Xi\in\mathcal{P}(\mathsf{selections})$.

node | owner | moves to | priority
---|---|---|---
$q$ | $\forall$ | $\\{(q,0),(q,1)\\}$ | $\Omega(q)$
$(q,0)$ | $\exists$ | $\\{\delta(q,\tau)\in D_{\chi}\mid\tau\in\mathsf{choices},\bot\notin l^{A}(q)\\}$ | $0$
$(q,1)$ | $\exists$ | $\\{(q,\Xi)\mid\Xi\in\mathcal{P}(\mathsf{selections}),[\\![l^{A}(q)\cap\Lambda(\mathbf{F})]\\!]^{l^{A}[\\{\delta(q,\kappa)\mid\kappa\in\Xi\\}]}_{1}\neq\emptyset\\}$ | $0$
$(q,\Xi)$ | $\forall$ | $\\{\delta(q,\kappa)\mid\kappa\in\Xi\\}$ | $0$

The game $\mathsf{G}_{\chi}$ is thus played over the co-determinized tracking
automaton $\mathsf{B}_{\chi}$, and its moves largely follow the transition
function $\delta$ of $\mathsf{B}_{\chi}$; in particular, every play in
$\mathsf{G}_{\chi}$ induces a run of $\mathsf{B}_{\chi}$, and, by the
definition of the priority function of $\mathsf{G}_{\chi}$, is won by
$\exists$ if and only if this run is accepting. Note that there are no moves
from $(q,0)$ if $\bot\in l^{A}(q)$, so $\exists$ loses $(q,0)$ in this case.
Otherwise, $\exists$ can select $\tau\in\mathsf{choices}$ and move to
$\delta(q,\tau)$. In this case, all top-level propositional connectives in the
label $l^{A}(q)$ are processed simultaneously, e.g. conjunctions are
decomposed into their conjuncts, and from every disjunction, a disjunct is
picked according to $\tau$.

We will establish soundness and completeness of the game in Section 5, showing
on the one hand that a winning strategy for $\exists$ can be extracted from a
model of $\chi$ (soundness), and on the other hand that the winning region of
$\exists$ carries a coalgebra structure in which every state satisfies its
label (completeness).

Recall that $\mathsf{selections}$ is of exponential size in $n_{0}=|\chi|$.
Since the formation of $V_{\forall}$ according to Definition 28 involves
$\mathcal{P}(\mathsf{selections})$, satisfiability games are thus of doubly
exponential size, and solving them directly, using some algorithm for parity
game solving, does _not_ yield a satisfiability checking algorithm that runs
in singly exponential time. In the remainder of this section, we introduce a
global caching algorithm that essentially computes the solution of the
satisfiability games presented above in singly exponential time and on-the-
fly, under mild assumptions on the complexity of the respective one-step-
satisfiability problem. We recall that $q_{\mathsf{init}}\in D_{\chi}$ is the
initial node of the co-determinized tracking automaton $\mathsf{B}_{\chi}$.
The algorithm expands $\mathsf{B}_{\chi}$ step by step starting from
$q_{\mathsf{init}}$; the expansion step adds nodes according to all possible
choice functions and all selections of modalities in a selected node $q$. The
order of expansion can be chosen freely, e.g. by heuristic methods. Optional
intermediate game solving steps can be used judiciously to realize on-the-fly
solving.

######  Algorithm 1 (Global caching).

To decide satisfiability of the input formula $\chi$, initialize the sets of
_unexpanded_ and _expanded_ nodes, $U=\\{q_{\mathsf{init}}\\}$ and
$Q=\emptyset$, respectively.

  1. (1)

Expansion: Choose some unexpanded node $q\in U$, remove $q$ from $U$, and add
$q$ to $Q$. Add all nodes in the sets $\\{\delta(q,\tau)\in
D_{\chi}\mid\tau\in\mathsf{choices}\\}\setminus Q$ and $\\{\delta(q,\kappa)\in
D_{\chi}\mid\kappa\in\mathsf{selections},\kappa\subseteq l(q)\\}\setminus Q$
to $U$.

  2. (2)

Optional solving: Compute $\mathsf{win}^{\exists}_{Q}$ and/or
$\mathsf{win}^{\forall}_{Q}$. If
$q_{\mathsf{init}}\in\mathsf{win}^{\exists}_{Q}$, then return ‘satisfiable‘,
if $q_{\mathsf{init}}\in\mathsf{win}^{\forall}_{Q}$, then return
‘unsatisfiable‘.

  3. (3)

If $U\neq\emptyset$, then continue with Step 1.

  4. (4)

Final game solving: Compute $\mathsf{win}^{\exists}$. If
$q_{\mathsf{init}}\in\mathsf{win}^{\exists}$, then return ‘satisfiable‘,
otherwise return ‘unsatisfiable‘.

We prove the soundness and completeness of this algorithm in Section 5 below.
Before analyzing the run time behaviour of the algorithm, we first show how to
compute the sets $\mathsf{win}^{\exists}_{Q}$ and $\mathsf{win}^{\forall}_{Q}$
in singly exponential time. To this end, we define $2n_{0}k$-ary set functions
$f_{Q}$ and $g_{Q}$ that compute one-step (un)satisfiability w.r.t. their
argument sets. These functions essentially encode short sequences of moves in
$\mathsf{G}_{\chi}$ leading from one node in $D_{\chi}$ to the next.

######  Definition 29 (One-step propagation).

For sets $Q\subseteq D_{\chi}$ and $X_{1},\ldots,X_{2n_{0}k}\subseteq Q$, we
put

$\displaystyle f_{Q}(X_{1},\ldots,X_{2n_{0}k})=$ $\displaystyle\\{q\in
Q\mid[\\![l^{A}(q)\cap\Lambda(\mathbf{F})]\\!]^{l^{A}[\delta(q,\mathsf{selections})\cap
X_{\Omega(q)}]}_{1}\neq\emptyset,\bot\notin l^{A}(q)\text{ and }$
$\displaystyle\qquad\qquad\exists\tau\in\mathsf{choices}.\,\delta(q,\tau)\in
X_{\Omega(q)}\\}$ $\displaystyle g_{Q}(X_{1},\ldots,X_{2n_{0}k})=$
$\displaystyle\\{q\in
Q\mid[\\![l^{A}(q)\cap\Lambda(\mathbf{F})]\\!]^{l^{A}[\delta(q,\mathsf{selections})\cap\overline{X_{\Omega(q)}}]}_{1}=\emptyset,\bot\in
l^{A}(q)\text{ or}$
$\displaystyle\qquad\qquad\forall\tau\in\mathsf{choices}.\,\delta(q,\tau)\in
X_{\Omega(q)}\\},$

where $\overline{X_{\Omega(q)}}=D_{\chi}\setminus X_{\Omega(q)}$.

To deal with possibly unguarded fixpoint variables, one-step propagation
according to $f_{Q}$ as defined above checks, for each node $q\in Q$, not only
the joint one-step satisfiability of all modal literals from the label of $q$
within the intersection of the successor nodes of $q$ (in the automaton
$\mathsf{B}_{\chi}$) and the set $X_{\Omega(q)}$, but also checks whether
there is a choice function that performs a simultaneous propositional tracking
step and leads to a node in $X_{\Omega(q)}$.

The time required for one-step propagation steps thus depends on the time
complexity of the one-step satisfiability problem. In Lemma 32, we
correspondingly give an estimate of the overall time complexity of the global
caching algorithm under the assumption that the strict one-step satisfiability
problem is in ExpTime.

Next we characterize the winning regions $\mathsf{win}^{\exists}_{Q}$ and
$\mathsf{win}^{\forall}_{Q}$ by fixpoint expressions over
$\mathcal{P}(D_{\chi})$, using the one-step propagation functions $f_{Q}$ and
$g_{Q}$, respectively.

######  Definition 30 (Satisfiability game solving).

Given a set $Q\subseteq D_{\chi}$, we put

$\displaystyle\mathbf{E}_{Q}$
$\displaystyle=\eta_{2n_{0}k}X_{2n_{0}k}.\,\ldots\eta_{1}X_{1}.f_{Q}(\mathbf{X})$
$\displaystyle\mathbf{A}_{Q}$
$\displaystyle=\overline{\eta_{2n_{0}k}}X_{2n_{0}k}\,\ldots\overline{\eta_{1}}X_{1}.g_{Q}(\mathbf{X}),$

where $\mathbf{X}=X_{1},\ldots,X_{2n_{0}k}$ is a vector of variables $X_{i}$
ranging over subsets of $Q$, where $\eta_{i}=\mu$ for odd $i$, $\eta_{i}=\nu$
for even $i$, and where $\overline{\nu}=\mu$ and $\overline{\mu}=\nu$.

Now we will show that this fixpoint characterization is indeed correct, that
is, that $\mathbf{E}_{Q}=\mathsf{win}^{\exists}_{Q}$ and
$\mathbf{A}_{Q}=\mathsf{win}^{\forall}_{Q}$ for $Q\subseteq D_{\chi}$. As the
sets $\mathbf{E}_{Q}$ and $\mathbf{A}_{Q}$ grow monotonically with $Q$, and
since clearly $\mathbf{A}_{D_{\chi}}$ is the complement of
$\mathbf{E}_{D_{\chi}}$, it suffices to prove that the winning region
$\mathsf{win}^{\exists}$ in $\mathsf{G}_{\chi}$ coincides with the set
$\mathbf{E}:=\mathbf{E}_{D_{\chi}}$ (a set defined as a fixpoint as per
Definition 30, using the one-step propagation function $f:=f_{D_{\chi}}$ as
per Definition 29).

######  Lemma 31.

For all $q\in D_{\chi}$, we have $q\in\mathbf{E}$ if and only if the
existential player wins the node $q$ in $\mathsf{G}_{\chi}$.

######  Proof 4.2.

The fixpoint

$\displaystyle\mathbf{E}$
$\displaystyle=\eta_{2n_{0}k}X_{2n_{0}k}.\,\ldots\eta_{1}X_{1}.f_{D_{\chi}}(X_{1},\ldots,X_{2n_{0}k})$

is equivalently presented as a hierarchical equation system consisting of
$2n_{0}k$ equations

$X_{l}=_{\eta_{l}}\begin{cases}X_{l-1}&1<l\leq 2n_{0}k\\\
f_{D_{\chi}}(X_{1},\ldots,X_{2n_{0}k})&l=1\end{cases}$

where $\eta_{l}=\mu$ if $l$ is odd and $\eta_{l}=\nu$ otherwise. Baldan et al.
introduce general _fixpoint games_ [BKMP19], that is, parity games that
characterize the solutions of hierarchical equation system over continuous
lattices. We instantiate these fixpoint games to the equation system for
$\mathbf{E}$ given above and obtain a parity game
$\mathsf{G}_{\mathbf{E}}=(V_{\forall},V_{\exists},E,\Omega:E\to\\{1,\ldots,2n_{0}k\\})$
played on $V_{\exists}=D_{\chi}$ and
$V_{\forall}=\mathcal{P}(D_{\chi})^{2n_{0}k}$. The moves and the priorities in
$\mathsf{G}_{\mathbf{E}}$ are given by the following table, where $q\in
D_{\chi}$ and
$\mathbf{X}=(A_{1},\ldots,A_{2n_{0}k})\in\mathcal{P}(D_{\chi})^{2n_{0}k}$.

node | owner | moves to | priority
---|---|---|---
$q$ | $\exists$ | $\\{\mathbf{X}\in\mathcal{P}(D_{\chi})^{2n_{0}k}\mid q\in f_{D_{\chi}}(\mathbf{X})\\}$ | $0$
$\mathbf{X}$ | $\forall$ | $\\{q\in D_{\chi}\mid q\in A_{l}\\}$ | $l$

The game $\mathsf{G}_{\mathbf{E}}$ is slightly simplified in comparison to the
fixpoint games from [BKMP19] in that edges rather than nodes are annotated
with priorities; this leads to slightly more succinct games since priorities
are not made explicit in nodes, but works only for fixpoint expressions of a
specific canonical format to which $\mathbf{E}$ adheres (that is, all
equations have the form $X_{l}=_{\eta_{l}}X_{l-1}$ except the one for $l=1$).
The existential player thus has to provide
$\mathbf{X}=(A_{1},\ldots,A_{2n_{0}k})$ such that $q\in
f_{D_{\chi}}(\mathbf{X})$ in order to show that $q$ is contained in
$\mathbf{E}$. The universal player in turn can challenge any state
$q^{\prime}\in A_{l}$ where $1\leq l\leq 2n_{0}k$, triggering priority $l$. We
import the correctness theorem for fixpoint games given in [BKMP19]]. In our
setting, this theorem implies that the existential player wins the node $q$ in
the fixpoint game $\mathsf{G}_{\mathbf{E}}$ if and only if $q$ is contained in
the solution of the hierarchical equation system for $\mathbf{E}$ given above.

It hence suffices to give mutual translations of winning strategies for the
satisfiability game $\mathsf{G}_{\chi}$ and the fixpoint game
$\mathsf{G}_{\mathbf{E}}$.

For one direction, suppose that the existential player wins $q$ in
$\mathsf{G}_{\mathbf{E}}$. We have a history-free strategy $s$ using which the
existential player wins every node in her winning region in
$\mathsf{G}_{\mathbf{E}}$. We define a history-free strategy $s^{\prime}$ for
the existential player in $\mathsf{G}_{\chi}$ as follows. Given $q^{\prime}\in
D_{\chi}$ such that the existential player wins the node $q^{\prime}$ in
$\mathsf{G}_{\mathbf{E}}$, we have
$s(q^{\prime})=(Y_{1},\ldots,Y_{2n_{0}k})\in\mathcal{P}(D_{\chi})^{2n_{0}k}$.
By the definition of $\mathsf{G}_{\mathbf{E}}$, $q^{\prime}\in
f_{D_{\chi}}(Y_{1},\ldots,Y_{2n_{0}k})$; that is,
$[\\![l^{A}(q^{\prime})\cap\Lambda(\mathbf{F})]\\!]^{l^{A}[\delta(q^{\prime},\mathsf{selections})\cap
Y_{\Omega(q^{\prime})}]}_{1}\neq\emptyset$, $\bot\notin l^{A}(q^{\prime})$ and
there is some $\tau\in\mathsf{choices}$ such that $\delta(q^{\prime},\tau)\in
Y_{\Omega(q^{\prime})}$. Put

$\displaystyle s^{\prime}(q^{\prime},0)$
$\displaystyle=\delta(q^{\prime},\tau)\qquad\text{and}$ $\displaystyle
s^{\prime}(q^{\prime},1)$ $\displaystyle=(q^{\prime},\Xi)\quad\text{where}$
(5) $\displaystyle\Xi$
$\displaystyle=\\{\kappa\in\mathsf{selections}\mid\delta(q^{\prime},\kappa)\in
Y_{\Omega(q^{\prime})}\\}).$

It is clear that $s^{\prime}(q^{\prime},0)$ is a legal move for the
existential player. To see the same for $s^{\prime}(q^{\prime},1)$, we have to
show by the definition of $\mathsf{G}_{\chi}$ that
$[\\![l^{A}(q^{\prime})\cap\Lambda(\mathbf{F})]\\!]^{l[\\{\delta(q^{\prime},\kappa)\mid\kappa\in\Xi\\}]}_{1}\neq\emptyset$.
But this follows from
$[\\![l^{A}(q^{\prime})\cap\Lambda(\mathbf{F})]\\!]^{l^{A}[\delta(q^{\prime},\mathsf{selections})\cap
Y_{\Omega(q^{\prime})}]}_{1}\neq\emptyset$, since

$\displaystyle l^{A}[\delta(q^{\prime},\mathsf{selections})\cap
Y_{\Omega(q^{\prime})}]$
$\displaystyle=l^{A}[\\{\delta(q^{\prime},\kappa)\mid\kappa\in\mathsf{selections},\delta(q^{\prime},\kappa)\in
Y_{\Omega(q^{\prime})}\\}]$
$\displaystyle=l^{A}[\\{\delta(q^{\prime},\kappa)\mid\kappa\in\Xi\\}]$

Now let $\pi^{\prime}$ be a play of $\mathsf{G}_{\chi}$ that follows
$s^{\prime}$. Then $\pi^{\prime}$ induces a play $\pi$ of
$\mathsf{G}_{{\mathbf{E}}}$ that follows $s$, in the following manner. A
universal node $q^{\prime}$ visited by $\pi^{\prime}$ will correspond to an
existential node $q^{\prime}$ visited by $\pi$. First, suppose that the
universal player moves from $q^{\prime}$ to $(q^{\prime},0)$ in
$\pi^{\prime}$. Then the play proceeds according to $s^{\prime}$, reaching, in
the notation of (5), the universal node $\delta(q^{\prime},\tau)$. From the
existential node $q^{\prime}$ in $\mathsf{G}_{{\mathbf{E}}}$, the play $\pi$
follows $s$, reaching $(Y_{1},\dots,Y_{2n_{0}k})$ in the notation of (5) and
the preceding sentences; since $\delta(q^{\prime},\tau)\in
Y_{\Omega(q^{\prime})}$, we can then let the universal player move to
$\delta(q^{\prime},\tau)$, triggering priority $\Omega(q^{\prime})$ and
continue similarly. Second, suppose that the universal player moves from
$q^{\prime}$ to $(q^{\prime},1)$ in $\pi^{\prime}$. Again, the play further
proceeds according to $s^{\prime}$, reaching $(q^{\prime},\Xi)$ in the
notation of (5). The universal player then moves to
$\delta(q^{\prime},\kappa)$ in $\pi^{\prime}$, for some $\kappa\in\Xi$. Again,
$\pi$ proceeds from $q^{\prime}$ according to $s$, reaching the universal node
$(Y_{1},\dots,Y_{2n_{0}k})$, in notation as above. Since
$\delta(q^{\prime},\kappa)\in Y_{\Omega(q^{\prime})}$ by (5), we can let the
universal player move to $\delta(q^{\prime},\kappa)$ in the next step, thereby
triggering priority $\Omega(q^{\prime})$, and continue similarly.

We have to show that the existential player wins $\pi^{\prime}$. Since $s$ is
a winning strategy (in $\mathsf{G}_{{\mathbf{E}}}$), the existential player
wins $\pi$, so the greatest priority $p$ visited infinitely often in $\pi$ is
even. By the correspondence between $\pi^{\prime}$ and $\pi$ described above,
and by the definition of priorities in $\mathsf{G}_{{\mathbf{E}}}$, the
highest priority visited infinitely often by $\pi^{\prime}$ is $p$, so the
existential player wins $\pi^{\prime}$, as required.

For the converse direction, let the existential player win $q$ in
$\mathsf{G}_{\chi}$ and let $s$ be a history-free strategy using which the
existential player wins every node in her winning region. We define a history-
free strategy $s^{\prime}$ for the existential player in
$\mathsf{G}_{{\mathbf{E}}}$ as follows. Given $q^{\prime}\in D_{\chi}$ such
that the existential player wins the node $q^{\prime}$ in $\mathsf{G}_{\chi}$,
we have $s(q^{\prime},0)=\delta(q^{\prime},\tau)$ where
$\tau\in\mathsf{choices}$ and $\bot\notin l^{A}(q^{\prime})$; furthermore, we
have $s(q^{\prime},1)=(q^{\prime},\Xi)$ where
$\Xi\in\mathcal{P}(\mathsf{selections})$ and
$[\\![l^{A}(q^{\prime})\cap\Lambda(\mathbf{F})]\\!]^{l[\\{\delta(q^{\prime},\kappa)\mid\kappa\in\Xi\\}]}_{1}\neq\emptyset$.
Put
$s^{\prime}(q^{\prime})=(\emptyset,\ldots,\emptyset,Y_{\Omega(w)},\emptyset,\ldots,\emptyset)$
(with $Y_{\Omega(q^{\prime})}$ in position $\Omega(q^{\prime})$) where

$Y_{\Omega(q^{\prime})}=\\{\delta(q^{\prime},\tau)\\}\cup\\{\delta(q^{\prime},\kappa)\mid\kappa\in\Xi\\}.$
(6)

We note that this is a legal move, as $q^{\prime}\in
f_{D_{\chi}}(\emptyset,\ldots,\emptyset,Y_{\Omega(q^{\prime})},\emptyset,\ldots,\emptyset)$
by construction of $Y_{\Omega(q^{\prime})}$.

Now let $\pi^{\prime}$ be a play of $\mathsf{G}_{S_{\mathbf{E}}}$ that follows
$s^{\prime}$. Then $\pi^{\prime}$ induces a play $\pi$ of $\mathsf{G}_{\chi}$
that follows $s$, in the following manner. An existential node $q^{\prime}$
visited in $\pi^{\prime}$ will correspond to a universal node $q^{\prime}$ in
$\pi$. At $s^{\prime}(q^{\prime})$, the universal player picks, in
$\pi^{\prime}$, an element of $Y_{\Omega(q^{\prime})}$. If, in the notation of
(6), this element is $\delta(q^{\prime},\tau)$, then we let the universal
player (in $\mathsf{G}_{\chi}$) move to $(q^{\prime},0)$ in $\pi$, and
otherwise to $(q^{\prime},1)$. From these nodes, $\pi$ proceeds according to
$s$. In the former case, $\pi$ then reaches the node
$\delta(q^{\prime},\tau)$, while $\pi^{\prime}$ reaches the node
$\delta(q^{\prime},\tau)$ and triggers priority $\Omega(q^{\prime})$. In the
latter case, $\pi$ reaches the universal node $(q^{\prime},\Xi)$, from where
we let the universal player move to the node $\delta(q^{\prime},\kappa)$
picked by the universal player in $\pi^{\prime}$. Similarly as in the first
case, the play $\pi^{\prime}$ reaches $\delta(q^{\prime},\kappa)$ and triggers
priority $\Omega(q^{\prime})$.

Let $p$ be the highest priority such that $\pi$ infinitely often visits nodes
$q^{\prime}$ such that $\Omega(q^{\prime})=p$. Since $s$ is a winning
strategy, $p$ is even. By the above description of the correspondence between
$\pi$ and $\pi^{\prime}$, the highest priority triggered infinitely often in
$\pi^{\prime}$ is $p$ as well. Since $p$ is even, the existential player wins
$\pi^{\prime}$.

Having shown how the sets $\mathsf{win}^{\exists}_{Q}$ and
$\mathsf{win}^{\forall}_{Q}$ can be computed by evaluating fixpoint
expressions over $\mathcal{P}(D_{\chi})$, we next analyze the run time
behaviour of the introduced algorithm.

######  Lemma 32.

If the strict one-step satisfiability problem is decidable in time $t(n)$,
then Algorithm 1 runs in time $\mathcal{O}((n_{0}k)!^{2c}\cdot t(n))$ for some
constant $c$ if no optional game solving steps are performed.

(The run time with optional game solving steps is still singly exponential; in
view of the fact that exponential run time of some fixed strategy on
intermediate game solving suffices to obtain the ExpTime bound on