Quasipolynomial Computation of Nested Fixpoints

TL;DR

This paper generalizes quasipolynomial algorithms for parity games to solve systems of fixpoint equations over finite lattices, enabling efficient model checking for various modal fixpoint logics and improving bounds on satisfiability checking.

Contribution

It introduces a quasipolynomial method for computing solutions of arbitrary fixpoint systems using universal graphs, extending beyond parity games.

Findings

Quasipolynomial algorithms apply to fixpoint systems over finite lattices.

Model checking for multiple modal fixpoint logics is in quasipolynomial time.

Improved bounds on satisfiability checking complexity.

Abstract

It is well-known that the winning region of a parity game with $n$ nodes and $k$ priorities can be computed as a $k$-nested fixpoint of a suitable function; straightforward computation of this nested fixpoint requires $\mathcal{O}(n^{\frac{k}{2}})$ iterations of the function. Calude et al.'s recent quasipolynomial-time parity game solving algorithm essentially shows how to compute the same fixpoint in only quasipolynomially many iterations by reducing parity games to quasipolynomially sized safety games. Universal graphs have been used to modularize this transformation of parity games to equivalent safety games that are obtained by combining the original game with a universal graph. We show that this approach naturally generalizes to the computation of solutions of systems of \emph{any} fixpoint equations over finite lattices; hence, the solution of fixpoint equation systems can be computed by quasipolynomially many iterations of the equations. We present applications to modal fixpoint logics and games beyond relational semantics. For instance, the model checking problems for the energy $\mu$-calculus, finite latticed $\mu$-calculi, and the graded and the (two-valued) probabilistic $\mu$-calculus -- with numbers coded in binary -- can be solved via nested fixpoints of functions that differ substantially from the function for parity games but still can be computed in quasipolynomial time; our result hence implies that model checking for these $\mu$-calculi is in QP. Moreover, we improve the exponent in known exponential bounds on satisfiability checking.

Equations

$$X_i{=}_{{\eta }_i}{f}_i(X_0,\dots ,X_k)0\le i\le k$$

$$\mathrm{GFP}f=$$

$$X_i{=}_{{\eta }_i}{f}_i(X_0,\dots ,X_k)$$

$$[[X_i]{]}^{\sigma }={\eta }_i{X}_i.f_i^{\sigma },$$

$$f_i^{\sigma }(A)=f_i($$

$$X_i$$

$$f_{\exists }(V_0,\dots ,V_k)=$$

$$X_i$$

$$f_{◊}(X)$$

$$(f_{\exists }^{\mathsf{e}}(V_0,\dots ,V_k))(v)=\{\begin{array}{ll}\min (\mathsf{en}(v,V_{\Omega (v)}))& \text{ if }v\in V_{\exists }\\ \max (\mathsf{en}(v,V_{\Omega (v)}))& \text{ if }v\in V_{\forall },\end{array}$$

$$\mathsf{en}(v,\sigma )=$$

$$\{b+1\mid \exists u\in E(v).\sigma (u)-w(v,u)>b\text{ or }\sigma (u)>b\},$$

$$E(u,i)$$

$$E(U_0,\dots ,U_k)=\{(u,i)\in B_L\times [k]\mid u⊑U_i\}.$$

$${\mathsf{ad}}_i^{\mu }$$

$${\Omega }^{\prime }(u,i)=\{\begin{array}{ll}2i& \text{ if }{\eta }_i=\mathrm{GFP}\\ 2i+1& \text{ if }{\eta }_i=\mathrm{LFP}\end{array}$$

$$u⊑[[X_i]{]}_f\text{ if and only if there is a history-free witness for }u⊑[[X_i]{]}_f.$$

$$g:\mathcal{P}(B_L\times [k]\times Z)$$

$$U$$

$$P_i^{U,q}=⨆\{u\in B_L\mid \exists s\in K_{\mathsf{ad}(i)}(q).(u,i,s)\in U\}.$$

$$u⊑[[X_i]{]}_f\text{ if and only if there is }q\in Z\text{ such that }(u,i,q)\in [[Y_0]{]}_g.$$

$$R_0^{\prime }(v_1,p_1,\Phi (v_1,p_1),0)=$$

$$(v_2,p_2)\in R_{\mathsf{ad}(p_2)}(v_1,p_1),\Phi (v_2,p_2)\in K_{\mathsf{ad}(p_2)}(\Phi (v_1,p_1))\}$$

$${\pi }_1[R_{\mathsf{ad}(j)}(v_1,p_1)]\subseteq$$

$$\tau =$$

$$q\le q^{\prime }\text{ implies that}$$

$$\text{ i′⪰i and s′∈Ki′(q′) such that s≤s′}.$$

$$U_i^{\mu ,q}=⨆\{u\in B_L\mid \exists s\in K_{\mathsf{ad}(i)}(q).\mu (u,i)\le s\}.$$

$$(\mathsf{Lift}(\mu ))(v,p)=\min \{q\in Z\mid v⊑f_p(U_0^{\mu ,q},\dots ,U_k^{\mu ,q})\}$$

$$(v,p)\in \mathbb{E}\text{ if and only if v∈[[Xp]]f}.$$

$$K_i(m_k,m_{k-2},\dots ,m_1)=\{\begin{array}{ll}\{(m_k,m_{k-2},\dots ,m_i-1)\mid m_i>0\}& \text{if }i\text{ is odd}\\ \{(m_k,m_{k-2},\dots ,m_{i-1})\}& \text{if }i\text{ is even}\end{array}$$

$$R_{i^{\prime }}(u,i)=\{(w,i^{\prime })\in W\mid \exists s\in K_{\mathsf{ad}(i^{\prime })}(\mu (u,i)).\mu (w,i^{\prime })\le s)\}$$

Full text

1 Introduction

Fixpoints are pervasive in computer science, governing large portions of recursion theory, concurrency theory, logic, and game theory. One famous example are parity games, which are central, e.g., to networks and infinite processes [5], tree automata [54], and $\mu$-calculus model checking [21]. Winning regions in parity games can be expressed as nested fixpoints of particular set functions (e.g. [20, 8]). In recent breakthrough work on the solution of parity games in quasipolynomial time, Calude et al. [9] essentially show how to compute this particular fixpoint in quasipolynomial time, that is, in time $2^{\mathcal{O}({(\log n)^{c}})}$ for some constant $c$. Subsequently, it has been shown [34, 17, 16] that universal graphs (that is, even graphs into which every even graph of a certain size embeds by a graph morphism) can be used to transform parity games to equivalent safety games obtained by pairing the original game with a universal graph; the size of these safety games is determined by the size of the employed universal graphs and it has been shown [17, 16] that there are universal graphs of quasipolynomial size. This yields a uniform algorithm for solving parity games to which all currently known quasipolynomial algorithms for parity games have been shown to instantiate using appropriately defined universal graphs [17, 16].

Briefly, our contribution in the present work is to show that the method of using universal graphs to solve parity games generalizes to the computation of nested fixpoints of arbitrary functions over finite lattices. That is, given functions $f_{i}:L^{k+1}\to L$, $0\leq i\leq k$ on a finite lattice $L$, we give an algorithm that uses universal graphs to compute the solutions of systems of equations

[TABLE]

where $\eta_{i}=\operatorname{\mathsf{GFP}}$ (greatest fixpoint) or $\eta_{i}=\operatorname{\mathsf{LFP}}$ (least fixpoint). Since there are universal graphs of quasipolynomial size, the algorithm requires only quasipolynomially many iterations of the functions $f_{i}$ and hence runs in quasipolynomial time, provided that all $f_{i}$ are computable in quasipolynomial time. While it seems plausible that this time bound may also be obtained by translating equation systems to equivalent standard parity games by emulating Turing machines to encode the functions $f_{i}$ as Boolean circuits (leading to many additional states but avoiding exponential blowup during the process), we emphasize that the main point of our result is not so much the ensuing time bound but rather the insight that universal graphs and hence many algorithms for parity games can be used on a much more general level which yields a precise (and relatively low) quasipolynomial bound on the number of function calls that are required to obtain solutions of fixpoint equation systems.

In more detail, the method of Calude et al. can be described as annotating nodes of a parity game with histories of quasipolynomial size and then solving this annotated game, but with a safety winning condition instead of the much more involved parity winning condition. It has been shown that these histories can be seen as nodes in universal graphs, in a more general reduction of parity games to safety games in which nodes from the parity game are annotated with nodes from a universal graph. This method has also been described as pairing separating automata with safety games [17]. It has been shown [17, 16] that there are exponentially sized universal graphs (essentially yielding the basis for e.g. the fixpoint iteration algorithm [8] or the small progress measures algorithm [33]) and quasipolynomially sized universal graphs (corresponding, e.g., to the succinct progress measure algorithm [34], or to the recent quasipolynomial variant of Zielonka’s algorithm [46]).

Hasuo et al. [28], and more generally, Baldan et al. [4] show that nested fixpoints in highly general settings can be computed by a technique based on progress measures, implicitly using exponentially sized universal graphs, obtaining an exponential bound on the number of iterations. Our technique is based on showing that one can make explicit use of universal graphs, correspondingly obtaining a quasipolynomial upper bound on the number of iterations. In both cases, computation of the nested fixpoint is reduced to a single (least or greatest depending on exact formulation) fixpoint of a function that extends the given set function to keep track of the exponential and quasipolynomial histories, respectively, in analogy to the previous reduction of parity games to safety games. Our central result can then be phrased as saying that the method of transforming parity conditions to safety conditions using universal graphs generalizes from solving parity games to solving systems of equations that use arbitrary functions over finite lattices. We use fixpoint games [53, 4] to obtain the crucial result that the solutions of equation systems have history-free witnesses, in analogy to history-freeness of winning strategies in parity games. These fixpoint games have exponential size but we show how to extract polynomial-size witnesses for winning strategies of $\mathsf{Eloise}$, and use these witnesses to show that any node won by $\mathsf{Eloise}$ is also won in the safety game obtained by a universal graph. For the backwards direction, we show that a witness for satisfaction of the safety condition regarding the universal graph induces a winning strategy in the fixpoint game. This proves that universal graphs can be used to compute nested fixpoints of arbitrary functions over finite lattices and hence yields the quasipolynomial upper bound for computation of nested fixpoints. Moreover, we present a progress measure algorithm that uses the nodes of a quasipolynomial universal graph to measure progress and that can be used to efficiently compute nested fixpoints of arbitrary functions over finite lattices.

As an immediate application of these results, we improve known deterministic algorithms for solving energy parity games [10], that is, parity games in which edges have additional integer weights and for which the winning condition is a combined parity condition and a (quantitative) positivity condition on the sum of the accumulated weights. Our results also show that the model checking problem for the associated energy $\mu$-calculus[2] is in QP. In a similar fashion, we obtain quasipolynomial algorithms for model checking in latticed $\mu$-calculi[7] in which the truth values of formulae are computed over arbitrary finite lattices, and for solving associated latticed parity games [36].

Furthermore, our results improve generic upper complexity bounds on model checking and satisfiability checking in the coalgebraic $\mu$-calculus [14], which serves as a generic framework for fixpoint logics beyond relational semantics. Well-known instances of the coalgebraic $\mu$-calculus include the alternating-time $\mu$-calculus [1], the graded $\mu$-calculus [38], the (two-valued) probabilistic $\mu$-calculus [14, 41], and the monotone $\mu$-calculus [22] (the ambient fixpoint logic of concurrent dynamic logic CPDL [48] and Parikh’s game logic [45]). This level of generality is achieved by abstracting system types as set functors and systems as coalgebras for the given functor following the paradigm of universal coalgebra [49]. It was previously shown [30] that the model checking problem for coalgebraic $\mu$-calculi reduces to the computation of a nested fixpoint. This fixpoint may be seen as a coalgebraic generalization of a parity game winning region but can be literally phrased in terms of small standard parity games (implying quasipolynomial run time) only in restricted cases. Our results show that the relevant nested fixpoint can be computed in quasipolynomial time in all cases of interest. Notably, we thus obtain as new specific upper bounds that even under binary coding of numbers, the model checking problems of both the graded $\mu$-calculus and the probabilistic $\mu$-calculus are in QP, even when the syntax is extended to allow for (monotone) polynomial inequalities.

Similarly, the satisfiability problem of the coalgebraic $\mu$-calculus has been reduced to a computation of a nested fixpoint [31], and our present results imply a marked improvement in the exponent of the associated exponential time bound. Specifically, the nesting depth of the relevant fixpoint is exponentially smaller than the basis of the lattice. Our results imply that this fixpoint is computable in polynomial time so that the complexity of satisfiability checking in coalgebraic $\mu$-calculi drops from $2^{\mathcal{O}({n^{2}k^{2}\log n})}$ to $2^{\mathcal{O}({nk\log n})}$ for formulae of size $n$ and with alternation depth $k$.

Related Work

The quasipolynomial bound on parity game solving has in the meantime been realized by a number of alternative algorithms. For instance, Jurdzinski and Lazic [34] use succinct progress measures to improve to quasilinear (instead of quasipolynomial) space; Fearnley et al. [24] similarly achieve quasilinear space. Lehtinen [40] and Boker and Lehtinen [6] present a quasipolynomial algorithm using register games. Parys [46] improves Zielonka’s algorithm [54] to run in quasipolynomial time. In particular the last algorithm is of interest as an additional candidate for generalization to nested fixpoints, due to the known good performance of Zielonka’s algorithm in practice. Daviaud et al. [19] generalize quasipolynomial-time parity game solving by providing a pseudo-quasipolynomial algorithm for mean-payoff parity games. On the other hand, Czerwinski et al. [17] give a quasipolynomial lower bound on universal trees, implying a barrier for prospective polynomial-time parity game solving algorithms. Chatterjee et al. [11] describe a quasipolynomial time set-based symbolic algorithm for parity game solving that is parametric in a lift function that determines how ranks of nodes depend on the ranks of their successors, and thereby unifies the complexity and correctness analysis of various parity game algorithms. Although part of the parity game structure is encapsulated in a set operator $\mathit{CPre}$, the development is tied to standard parity games, e.g. in the definition of the $\mathit{best}$ function, which picks minimal or maximal ranks of successors depending on whether a node belongs to $\mathsf{Abelard}$ or $\mathsf{Eloise}$.

Early work on the computation of unrestricted nested fixpoints has shown that greatest fixpoints require less effort in the fixpoint iteration algorithm, which can hence be optimized to compute nested fixpoints with just $\mathcal{O}(n^{\frac{k}{2}})$ calls of the functions at hand [42, 52], improving the previously known (straightforward) bound $\mathcal{O}(n^{k})$; here, $n$ denotes the size of the basis of the lattice and $k$ the number of fixpoint operators. Recent progress in the field has established the above-mentioned approaches using progress measures [28] and fixpoint games [4] in general settings, both with a view to applications in coalgebraic model checking like in the present paper. In comparison to the present work, the respective bounds on the required number of function iterations in the above unrestricted approaches all are exponential.

A preprint of our present results, specifically the quasipolynomial upper bound on function iteration in fixpoint computation, has been available as an arXiv preprint for some time [29]. Subsequent to this preprint, Arnold, Niwinski and Parys [3] have improved the actual run time by reducing the overhead incurred per iteration (and they give a form of quasipolynomial lower bound for universal-tree-based algorithms), working (like [29]) in the less general setting of directly nested fixpoints over powerset lattices; we show in Section 6 how such an improvement can be incorporated also in our lattice-based algorithm.

2 Notation and Preliminaries

Let $U$ and $V$ be sets, and let $R\subseteq U\times U$ be a binary relation on $U$. For $u\in U$, we then put $R(u):=\{v\in U\mid(u,v)\in R\}$. We put $[k]=\{0,\ldots,k\}$ for $k\in\mathbb{N}$. Labelled graphs $G=(W,R)$ consist of a set $W$ together with a relation $R\subseteq W\times A\times W$ where $A$ is some set of labels; typically, we use $A=[k]$ for some $k\in\mathbb{N}$. An $R$-path in a labelled graph is a finite or infinite sequence $v_{0},a_{0},v_{1},a_{1},v_{2}\dots$ (ending in a node from $W$ if finite) such that $(v_{i},a_{i},v_{i+1})\in R$ for all $i$. For $v\in W$ and $a\in A$, we put $R_{a}(v)=\{w\in W\mid(v,a,w)\in R\}$ and sometimes write $|G|$ to refer to $|W|$. As usual, we write $U^{*}$ and $U^{\omega}$ for the sets of finite sequences or infinite sequences, respectively, of elements of $U$. The domain $\mathsf{dom}(f)$ of a partial function $f:U\rightharpoonup V$ is the set of elements on which $f$ is defined. As usual, the (forward) image of $A^{\prime}\subseteq A$ under a function $f:A\to B$ is $f[A^{\prime}]=\{b\in B\mid\exists a\in A^{\prime}.\,f(a)=b\}$ and the preimage $f^{-1}[B^{\prime}]$ of $B^{\prime}\subseteq B$ under $f$ is defined by $f^{-1}[B^{\prime}]=\{a\in A\mid\exists b\in B^{\prime}.\,f(a)=b\}$. Projections $\pi_{j}:A_{1}\times\ldots\times A_{m}\to A_{j}$ for $1\leq j\leq m$ are given by $\pi_{i}(a_{1},\ldots,a_{m})=a_{j}$. We often regard (finite) sequences $\tau=u_{0},u_{1},\ldots\in U^{*}\cup U^{\omega}$ of elements of $U$ as partial functions of type $\mathbb{N}\rightharpoonup U$ and then write $\tau(i)$ to denote the element $u_{i}$, for $i\in\mathsf{dom}(\tau)$. For $\tau\in U^{*}\cup U^{\omega}$, we define the set $\mathsf{Inf}(\tau)=\{u\in U\mid\forall i\geq 0.\,\exists j>i.\,\tau(j)=u\}$ of elements that occur infinitely often in $\tau$ (so $\mathsf{Inf}(\tau)=\emptyset$ for $\tau\in U^{*}$). An infinite $R$-path $v_{0},p_{0},v_{1},p_{1},\dots$ in a labelled graph $G=(W,R)$ with labels from $[k]$ is even if $\max(\mathsf{Inf}(p_{0},p_{1},\dots))$ is even, and $G$ is even if every infinite $R$-path in $G$ is even. We write $\mathcal{P}(U)$ for the powerset of $U$, and $U^{m}$ for the $m$-fold Cartesian product $U\times\dots\times U$.

Finite Lattices and Fixpoints

A finite lattice $(L,\sqsubseteq)$ (often written just as $L$) consists of a non-empty finite set $L$ together with a partial order $\sqsubseteq$ on $L$, such that there is, for all subsets $X\subseteq L$, a join $\bigsqcup X$ and a meet $\bigsqcap X$. The least and greatest elements of $L$ are defined as $\top=\bigsqcup\emptyset$ and $\bot=\bigsqcap\emptyset$, respectively. A set $B_{L}\subseteq L$ such that $l=\bigsqcup\{b\in B_{L}\mid b\sqsubseteq l\}$ for all $l\in L$ is a basis of $L$. Given a finite lattice $L$, a function $g:L^{k}\to L$ is monotone if $g(V_{1},\ldots,V_{k})\sqsubseteq g(W_{1},\ldots,W_{k})$ whenever $V_{i}\sqsubseteq W_{i}$ for all $1\leq i\leq k$. For monotone $f:L\to L$, we put

[TABLE]

which, by the Knaster-Tarski fixpoint theorem, are the greatest and the least fixpoint of $f$, respectively. Furthermore, we define $f^{0}(V)=V$ and $f^{m+1}(V)=f(f^{m}(V))$ for $m\geq 0$, $V\sqsubseteq L$; since $L$ is finite, we have $\operatorname{\mathsf{GFP}}f=f^{n}(\top)$ and $\operatorname{\mathsf{LFP}}f=f^{n}(\bot)$ by Kleene’s fixpoint theorem. Given a finite set $U$ and a natural number $n$, $(n^{U},\sqsubseteq)$ is a finite lattice, where $n^{U}=\{f:U\to[n-1]\}$ denotes the function space from $U$ to $[n-1]$ and $f\sqsubseteq g$ if and only if for all $u\in U$, $f(u)\leq g(u)$. For $n=2$, we obtain the powerset lattice $(2^{U},\subseteq)$, also denoted by $\mathcal{P}(U)$, with least and greatest elements $\emptyset$ and $U$, respectively, and basis $\{\{u\}\mid u\in U\}$.

Parity games

A parity game $(V,E,\Omega)$ consists of a set of nodes $V$, a left-total relation $E\subseteq V\times V$ of moves encoding the rules of the game, and a priority function $\Omega:V\to\mathbb{N}$, which assigns priorities $\Omega(v)\in\mathbb{N}$ to nodes $v\in V$. Moreover, each node belongs to exactly one of the two players $\mathsf{Eloise}$ or $\mathsf{Abelard}$, where we denote the set of $\mathsf{Eloise}$’s nodes by $V_{\exists}$ and that of $\mathsf{Abelard}$’s nodes by $V_{\forall}$. A play $\rho\in V^{\omega}$ is an infinite sequence of nodes that follows the rules of the game, that is, such that for all $i\geq 0$, we have $(\rho(i),\rho(i+1))\in E$. We say that an infinite play $\rho=v_{0},v_{1},\ldots$ is even if the largest priority that occurs infinitely often in it (i.e. $\max(\mathsf{Inf}(\Omega\circ\rho))$) is even, and odd otherwise, and call this property the parity of $\rho$. Player $\mathsf{Eloise}$ wins exactly the even plays and player $\mathsf{Abelard}$ wins all other plays. A (history-free) $\mathsf{Eloise}$-strategy $s:V_{\exists}\rightharpoonup V$ is a partial function that assigns single moves $s(x)$ to $\mathsf{Eloise}$-nodes $x\in\mathsf{dom}(s)$. Given an $\mathsf{Eloise}$-strategy $s$, a play $\rho$ is an $s$-play if for all $i\in\mathsf{dom}(\rho)$ such that $\rho(i)\in V_{\exists}$, we have $\rho(i+1)=s(\rho(i))$. An $\mathsf{Eloise}$-strategy wins a node $v\in V$ if $\mathsf{Eloise}$ wins all $s$-plays that start at $v$. We have a dual notion of $\mathsf{Abelard}$-strategies; solving a parity game consists in computing the winning regions $\mathsf{win}_{\exists}$ and $\mathsf{win}_{\forall}$ of the two players, that is, the sets of states that they respectively win by some strategy.

It is known that solving parity games is in NP$\,\cap\,$coNP (and, more specifically, in UP$\,\cap\,$co-UP). Recently it has also been shown [9] that for parity games with $n$ nodes and $k$ priorities, $\mathsf{win}_{\exists}$ and $\mathsf{win}_{\forall}$ can be computed in quasipolynomial time $\mathcal{O}(n^{\log k+6})$. Another crucial property of parity games is that they are history-free determined [26], that is, that every node in a parity game is won by exactly one of the two players and then there is a history-free strategy for the respective player that wins the node.

3 Systems of Fixpoint Equations

We now introduce our central notion, that is, systems of fixpoint equations over a finite lattice. Throughout, we fix a finite lattice $(L,\sqsubseteq)$ and a basis $B_{L}$ of $L$ such that $\bot\notin B_{L}$, and $k+1$ monotone functions $f_{i}:L^{k+1}\to L$, $0\leq i\leq k$.

Definition 3.1

A system of equations consists of $k+1$ equations of the form

[TABLE]

where $\eta_{i}\in\{\operatorname{\mathsf{LFP}},\operatorname{\mathsf{GFP}}\}$, briefly referred to as $f$. For a partial valuation $\sigma:[k]\rightharpoonup L$, we inductively define

[TABLE]

where the function $f_{i}^{\sigma}$ is given by

[TABLE]

for $A\in L$, where $(\sigma[i\mapsto A])(j)=\sigma(j)$ for $j\neq i$ and $(\sigma[i\mapsto A])(i)=A$, $\sigma^{\prime}=\sigma[i\mapsto A]$ and where $\mathsf{ev}(\sigma,j)=\sigma(j)$ if $j\in\mathsf{dom}(\sigma)$ and $\mathsf{ev}(\sigma,j)=[\![X_{j}]\!]^{\sigma}$ otherwise (the latter clause handles free variables). Then, the solution of the system of equations is  $[\![X_{k}]\!]^{\epsilon}$ where $\epsilon:[k]\rightharpoonup L$ denotes the empty valuation (i.e. $\mathsf{dom}(\epsilon)=\emptyset$). Similarly, we can obtain solutions for the other components as $[\![X_{i}]\!]^{\epsilon}$ for $0\leq i<k$; we drop the valuation index if no confusion arises, and sometimes write $[\![X_{i}]\!]_{f}$ to make the equation system $f$ explicit. We denote by $\mathsf{E}^{f_{0}}$ the solution $[\![X_{k}]\!]$ for the canonical system of equations of the particular shape

[TABLE]

where $0<i\leq k$, $\eta_{i}=\operatorname{\mathsf{LFP}}$ for odd $i$ and $\eta_{i}=\operatorname{\mathsf{GFP}}$ for even $i$.

Example 3.2

1. (1)

Parity games and the modal $\mu$-calculus: Let $(V,E,\Omega)$ be a parity game with priorities [math] to $k$, take $L=\mathcal{P}(V)$, and consider the canonical system of fixpoint equations $\mathsf{E}^{f_{\exists}}$ for the function $f_{\exists}\colon\mathcal{P}(V)^{k+1}\to\mathcal{P}(V)$ given by

[TABLE]

for $(V_{0},\ldots,V_{k})\in\mathcal{P}(V)^{k+1}$. It is well known that $\mathsf{win}_{\exists}=\mathsf{E}^{f_{\exists}}$, i.e. parity games can be solved by solving fixpoint equation systems. Intuitively, $v\in f_{\exists}(V_{0},\ldots,V_{k})$ iff $\mathsf{Eloise}$ can enforce that some node in $V_{\Omega(v)}$ is reached in the next step. The nested fixpoint expressed by $\mathsf{E}^{f_{\exists}}$ (in which least (greatest) fixpoints correspond to odd (even) priorities) is constructed in such a way that $\mathsf{Eloise}$ only has to rely infinitely often on an argument $V_{i}$ for odd $i$ if she can also ensure that some argument $V_{j}$ for $j>i$ is used infinitely often.

Model checking for the modal $\mu$-calculus [35] and solving parity games are linear-time equivalent problems. Formulae of the $\mu$-calculus are evaluated over Kripke frames $(U,R)$ with set of states $U$ and transition relation $R$. Formulae $\phi$ of the $\mu$-calculus can be directly represented as equation systems over the lattice $\mathcal{P}(U)$ by recursively translating $\phi$ to equations, mapping subformulae $\mu X_{i}.\,\psi(X_{0},\ldots,X_{k})$ and $\nu X_{j}.\,\chi(X_{0},\ldots,X_{k})$ to equations

[TABLE]

and interpreting the modalities $\lozenge$ and $\square$ by functions

[TABLE]

The solution of the resulting system of equations then is the truth set of the formula $\phi$, that is, model checking for the model $\mu$-calculus reduces to solving fixpoint equation systems. Furthermore, satisfiability checking for the modal $\mu$-calculus can be reduced to solving so-called satisfiability games [25], that is, parity games that are played over the set of states of a determinized parity automaton. These satisfiability games can be expressed as systems of fixpoint equations, where the functions track transitions in the determinized automaton. 2. (2)

Energy parity games and the energy $\mu$-calculus: Energy parity games [10] are two-player games played over weighted game arenas $(V,E,w,\Omega)$, where $w:E\to\mathbb{Z}$ assigns integer weights to edges. The winning condition is the combination of a parity condition with a (quantitative) positivity condition on the sum of the accumulated weights. It has been shown [10, 2], that $b=n\cdot d\cdot W$ is a sufficient upper bound on energy level accumulations in energy parity games with $n$ nodes, $k$ priorities and maximum absolute weight $W$. We define a function $f^{\mathsf{e}}_{\exists}:((b+1)^{V})^{k+1}\to(b+1)^{V}$ over the finite lattice $(b+1)^{V}$ (whose elements are functions from $V$ to the set $\{0,\ldots,b+1\}$) by putting

[TABLE]

for $(V_{0},\ldots,V_{k})\in((b+1)^{V})^{k+1}$ and $v\in V$, using $\mathsf{en}(v,\sigma)$ as abbreviation for

[TABLE]

where $\sigma:V\to\{0,\ldots,b+1\}$. Then it follows from the results of [2] that player $\mathsf{Eloise}$ wins a node $v$ in the energy parity game with minimal initial credit $c<b+1$ if $(\mathsf{E}^{f^{\mathsf{e}}_{\exists}})(v)=c$, that is, if the solution of the canonical equation system over $f^{\mathsf{e}}_{\exists}$ maps $v$ to a value $c$ that is at most $b$.

The energy $\mu$-calculus [2] is the fixpoint logic that corresponds to energy parity games. Its formulae are evaluated over weighted game structures and involve operators $\lozenge_{E}\phi$ and $\square_{E}\phi$ that are evaluated depending on the energy function $[\![\phi]\!]:V\to\{0,\ldots,b+1\}$ that is obtained by first evaluating the argument formula $\phi$. The semantics of the diamond operator then is an energy function that assigns, to each state $v$, the least energy value $c\in\{0,\ldots,b+1\}$ such that there is a move from $v$ to some node $u$ such that the credit $c$ suffices to take the move from $v$ to $u$ and retain an energy level of at least $[\![\phi]\!](u)$. Formulae can be translated to equation systems over the finite lattice $(b+1)^{V}$, where the functions for modal operators are defined according to their semantics as presented in [2]. Solving these equation systems then amounts to model checking energy $\mu$-calculus formulae over weighted game structures. 3. (3)

Latticed $\mu$-calculi: In latticed $\mu$-calculi [7], formulae are evaluated over complete lattices $L$ rather than the powerset lattice; for finite lattices $L$, formulae of latticed $\mu$-calculi hence can be translated to fixpoint equation systems over $L$, so that model checking reduces to solving equation systems. An associated latticed variant of games has been introduced in [36] and for finite lattices $L$, solving latticed parity games over $L$ reduces to solving equation systems over $L$. 4. (4)

The coalgebraic $\mu$-calculus and coalgebraic parity games: The coalgebraic $\mu$-calculus [14] supports generalized modal branching types by using predicate liftings to interpret formulae over $T$-coalgebras, that is, over structures whose transition type is specified by an endofunctor $T$ on the category of sets. For instance the functors $T=\mathcal{P}$, $T=\mathcal{D}$ and $T=\mathcal{G}$ map sets $X$ to their powerset $\mathcal{P}(X)$, the set of probability distributions $\mathcal{D}(X)=\{f:X\to[0,\ldots,1]\}$ over $X$, and to the set of multisets $\mathcal{G}(X)=\{f:X\to\mathbb{N}\}$ over $X$, respectively. The corresponding $T$-coalgebras then are Kripke frames (for $T=\mathcal{P}$), Markov chains (for $T=\mathcal{D}$) and graded transition systems (for $T=\mathcal{G}$), respectively. Instances of the coalgebraic $\mu$-calculus comprise, e.g. the two-valued probabilistic $\mu$-calculus [14, 41] with modalities $\lozenge_{p}\phi$ for $p\in[0,\ldots,1]$, expressing ‘the next state satisfies $\phi$ with probability more than $p$’; the graded $\mu$-calculus [38] with modalities $\lozenge_{g}\phi$ for $g\in\mathbb{N}$, expressing ‘there are more than $\phi$ successor states that satisfy $\phi$’; or the alternating-time $\mu$-calculus [1] that is interpreted over concurrent game frames and uses modalities $\langle D\rangle\phi$ for finite $D\subseteq\mathbb{N}$ (encoding a coalition) that express that ‘coalition $D$ has a joint strategy to enforce $\phi$’.

It has been shown in previous work [30] that model checking for coalgebraic $\mu$-calculi against coalgebras with state space $U$ reduces to solving a canonical fixpoint equation system over the powerset lattice $\mathcal{P}(U)$, where the involved function interprets modal operators using predicate liftings, as described in [14, 30]. This canonical equation system can alternatively be seen as the winning region of $\mathsf{Eloise}$ in coalgebraic parity games, a highly general variant of parity games where the game structure is a coalgebra and nodes are annotated with modalities. Examples include two-valued probabilistic parity games and graded parity games in which nodes and edges are annotated with probabilities or grades, respectively. In order to win a node $v$, player $\mathsf{Eloise}$ then has to have a strategy that picks a set of moves to nodes that in turn are all won by $\mathsf{Eloise}$, and such that the joint probability (joint grade) of the picked moves is greater than the probability (grade) that is assigned to $v$. It is known that solving coalgebraic parity games reduces to solving fixpoint equation systems [30].

Furthermore, the satisfiability problem of the coalgebraic $\mu$-calculus has been reduced to solving canonical fixpoint equations systems over lattices $\mathcal{P}(U)$, where $U$ is the state set of a determinized parity automaton and where the innermost equation checks for joint one-step satisfiability of sets of coalgebraic modalities [31]. By interpreting coalgebraic formulae over finite lattices $d^{U}$ rather than over powerset lattices, one obtains the finite-valued coalgebraic $\mu$-calculus (with values $\{0,\ldots,d\}$), which has the finite-valued probabilistic $\mu$-calculus (e.g. [43]) as an instance. Model checking for the finite-valued probabilistic $\mu$-calculus hence reduces to solving equation systems over the finite lattice $d^{|U|}$, where $\{0,\ldots,d\}$ encodes a finite set of probabilities.

4 Fixpoint Games and History-free Witnesses

We instantiate the existing notion of fixpoint games [53, 4], which characterize solutions of equation systems, to our setting (that is, to finite lattices), and then use these games as a technical tool to establish our crucial notion of history-freeness for systems of fixpoint equations.

Definition 4.1 (Fixpoint games)

Let $X_{i}=_{\eta_{i}}f_{i}(X_{0},\ldots,X_{k})$, $0\leq i\leq k$, be a system of fixpoint equations. The associated fixpoint game is a parity game $(V,E,\Omega)$ with set of nodes $V=(B_{L}\times[k])\cup L^{k+1}$, where nodes from $B_{L}\times[k]$ belong to player $\mathsf{Eloise}$ and nodes from $L^{k+1}$ belong to player $\mathsf{Abelard}$. For nodes $(u,i)\in B_{L}\times[k]$, we put

[TABLE]

and for nodes $(U_{0},\ldots,U_{k})\in L^{k+1}$, we put

[TABLE]

The alternation depth $\mathsf{ad}(i)$ of an equation $X_{i}=_{\eta_{i}}f_{i}(X_{0},\ldots,X_{1})$ is defined as $\mathsf{ad}^{\mu}_{i}$ if $\eta_{i}=\mu$ and as $\mathsf{ad}^{\nu}_{i}$ if $\eta_{i}=\nu$, where $\mathsf{ad}^{\mu}_{i}$, $\mathsf{ad}^{\nu}_{i}$ are recursively defined by

[TABLE]

for $0\leq i\leq k$. The priority function $\Omega:V\to[\mathsf{ad}(k)]$ then is defined by $\Omega(u,i)=\mathsf{ad}(i)$ and $\Omega(U_{0},\ldots,U_{k})=0$.

Remark 4.2

In [4], an alternative priority function $\Omega^{\prime}:V\to[2k+1]$ with

[TABLE]

and $\Omega^{\prime}(U_{0},\ldots,U_{k})=0$ is used. Since $\mathsf{ad}(i)$ is even if and only if $\eta_{i}$ is even, and moreover $\mathsf{ad(i)}\leq\mathsf{ad}(j)$ for $i\leq j$, and $i<j$ whenever $\mathsf{ad(i)}<\mathsf{ad}(j)$, it is easy to see that $\Omega$ and $\Omega^{\prime}$ in fact assign identical parities to all plays. In the following, we will use the more economic parity function $\Omega$ so that fixpoint games have only $d:=\mathsf{ad}(k)\leq k$ priorities.

We import the associated characterization theorem [4, Theorem 4.8]:

Theorem 4.3 ([4])

We have $u\sqsubseteq[\![X_{i}]\!]_{f}$ if and only if $\mathsf{Eloise}$ wins the node $(u,i)$ in the fixpoint game for the given system $f$ of equations.

Remark 4.4

While this shows that parity game solving can be used to solve equation systems, the size of fixpoint games is exponential in $|B_{L}|$, so they do not directly yield a quasipolynomial algorithm for solving equation systems.

Next we define our notion of history-freeness for systems of fixpoint equations.

Definition 4.5 (History-free witness)

A history-free witness for $u\sqsubseteq[\![X_{i}]\!]_{f}$ is an even labelled graph $(W,R)$ with labels from $[d]$ such that $W\subseteq B_{L}\times[d]$, $(u,i)\in W$, and for all $(v,p)\in W$, we have $v\sqsubseteq f_{p}(U_{0},\ldots,U_{k})$ where $U_{j}=\bigsqcup\pi_{1}[R_{\mathsf{ad}(j)}(v,p)]$ for $0\leq j\leq k$, noting that $R_{\mathsf{ad}(j)}(v,p)\subseteq W$ so that $\pi_{1}[R_{\mathsf{ad}(j)}(v,p)]\subseteq B_{L}$ and $U_{j}\in L$.

In analogy to history-free strategies for parity games, history-free witnesses assign tuples $(R_{1}(v,p),\ldots,R_{d}(v,p))$ of sets $R_{j}(v,p)\subseteq W$ to pairs $(v,p)\in W$ without relying on a history of previously visited pairs. We have $|W|\leq(d+1)|B_{L}|$ and $|R|\leq(d+1)|W|^{2}$, that is, the size of history-free witnesses is polynomial in $|B_{L}|$. Crucially, history-free witnesses always exist:

Lemma 1

For all $u\in B_{L}$ and $i\in[k]$, we have

[TABLE]

Proof

In one direction, we have $u\sqsubseteq[\![X_{i}]\!]_{f}$ so that $\mathsf{Eloise}$ wins the node $(u,i)$ in the according fixpoint game by Lemma 4.3. Let $s$ be a corresponding history-free winning strategy (such strategies always exists, see e.g. [26]). We inductively construct a witness for $u\sqsubseteq[\![X_{i}]\!]_{f}$, starting at $(u,i)$. When at $(v,p)\in B_{L}\times[k]$ with $s(v,p)=(U_{0},\ldots,U_{k})$, we put $R_{i}(v,p)=\bigcup_{j\mid\mathsf{ad}(j)=i}(U_{j}\times\{j\})$ for $0\leq i\leq d$ and hence have $\mathsf{ad}(j)=i$ for all $((v,p),i,(u,j))\in R$. Since $s$ is a winning strategy, the resulting graph $(W,R)$ is a history-free witness for $u\sqsubseteq[\![X_{i}]\!]_{f}$ by construction; in particular, $(W,R)$ is even. For the converse direction, the witness for $u\sqsubseteq[\![X_{i}]\!]_{f}$ directly yields a winning $\mathsf{Eloise}$-strategy for the node $(u,i)$ in the associated fixpoint game. This implies $u\sqsubseteq[\![X_{i}]\!]_{f}$ by Lemma 4.3.∎

5 Solving Equation Systems using Universal Graphs

We go on to prove our main result. To this end, we fix a system $f$ of fixpoint equations $f_{i}:L^{k+1}\to L$, $0\leq i\leq k$, and put $n:=|B_{L}|$ and $d:=\mathsf{ad}(k)$ for the remainder of the paper.

Definition 5.1 (Universal graphs [17, 16])

Let $G=(W,R)$ and $G^{\prime}=(W^{\prime},R^{\prime})$ be labelled graphs with labels from $[d]$. A homomorphism of labelled graphs from $G$ to $G^{\prime}$ is a function $\Phi:W\to W^{\prime}$ such that for all $(v,p,w)\in R$, we have $(\Phi(v),p,\Phi(w))\in R^{\prime}$. An $(n,d+1)$-universal graph $S$ is an even graph with labels from $[d]$ such that for all even graphs $G$ with labels from $[d]$ and with $|G|\leq n$, there is a homomorphism from $G$ to $S$.

We fix an $(n(d+1),(d+1))$-universal graph $S=(Z,K)$, noting that there are $(n(d+1),(d+1))$-universal graphs (obtained from universal trees) of size quasipolynomial in $n$ and $d$ [17]. We now combine the system $f$ with the universal graph $S$ to turn the parity conditions associated to general systems of fixpoint equations into a safety condition, associated to a single greatest fixpoint equation.

Definition 5.2 (Chained-product fixpoint)

We define a function

[TABLE]

where

[TABLE]

We refer to $Y_{0}=_{\operatorname{\mathsf{GFP}}}g(Y_{0})$ as the chained-product fixpoint (equation) of $f$ and $S$.

We now show our central result: apart from the annotation with states from the universal graph, the chained-product fixpoint $g$ is the solution of the system $f$.

Theorem 5.3

For all $u\in B_{L}$ and $0\leq i\leq k$, we have

[TABLE]

Proof

For the forward direction, let $u\sqsubseteq[\![X_{i}]\!]_{f}$. By Lemma 1, there is a history-free witness $G=(W,R)$ for $u\sqsubseteq[\![X_{i}]\!]_{f}$. Since $S$ is a $(n(d+1),d+1)$-universal graph and since $G$ is a witness and hence an even labelled graph of suitable size $|G|\leq n(d+1)$, there is a graph homomorphism $\Phi$ from $G$ to $S$. Starting at $(u,i,\Phi(u,i),0)$, we inductively construct a witness for containment of $(u,i,\Phi(u,i))$ in $[\![Y_{0}]\!]_{g}$. When at $(v_{1},p_{1},\Phi(v_{1},p_{1}),0)$ with $(v_{1},p_{1})\in W$, we put

[TABLE]

and continue the inductive construction with all these $(v_{2},p_{2},\Phi(v_{2},p_{2}),0)$, having $(v_{2},p_{2})\in W$. The resulting structure $G^{\prime}=(W^{\prime},R^{\prime})$ indeed is a witness for containment of $(u,i,q)$ in $[\![Y_{0}]\!]_{g}$: $G^{\prime}$ is even by construction. Moreover, we need to show that for $(v_{1},p_{1},\Phi(v_{1},p_{1}),0)\in W^{\prime}$, we have $(v_{1},p_{1},\Phi(v_{1},p_{1}),0)\in g(\pi_{1}[R^{\prime}_{0}(v_{1},p_{1},\Phi(v_{1},p_{1}),0)])$, i.e. $v_{1}\sqsubseteq f_{p_{1}}(P^{U,\Phi(v_{1},p_{1})}_{0},\ldots,P^{U,\Phi(v_{1},p_{1})}_{k})$ where $U=\pi_{1}[R^{\prime}_{0}(v_{1},p_{1},\Phi(v_{1},p_{1}),0)]$. Since $G$ is a witness and $(v_{1},p_{1})\in W$ by construction of $W^{\prime}$, we have $v_{1}\sqsubseteq f_{p_{1}}(U_{0},\ldots,U_{k})$ where $U_{j}=\bigsqcup(\pi_{j}[R_{\mathsf{ad}(i)}(v_{1},p_{1})])$. By monotonicity of $f_{p_{1}}$, it thus suffices to show that $U_{j}\sqsubseteq P^{U,\Phi(v_{1},p_{1})}_{j}$ for $0\leq j\leq k$; by definition of $P^{U,\Phi(v_{1},p_{1})}_{j}$ this follows if

[TABLE]

where $W=\pi_{1}[R^{\prime}_{0}(v_{1},p_{1},q_{1},0)]$. So let $w\in B_{L}$ such that $w\in\pi_{1}[R_{\mathsf{ad}(j)}(v_{1},p_{1})]$. Since $R$ is a witness that is constructed as in the proof of Lemma 1, we have $i=\mathsf{ad}(i^{\prime})$ for all $((v^{\prime},p^{\prime}),i,(w^{\prime},i^{\prime}))\in R$. Thus $(w,j)\in R_{\mathsf{ad}(j)}(v_{1},p_{1})$ for some $j$ such that $\mathsf{ad}(j)=i$, that is, $((v_{1},p_{1}),\mathsf{ad}(j),(w,j))\in R$, hence $(\Phi(v_{1},p_{1}),\mathsf{ad}(j),\Phi(w,j))\in K$ because $\Phi$ is a graph homomorphism. By definition of $R^{\prime}_{0}$ we have $(w,j,\Phi(w,j),0)\in R^{\prime}_{0}(v_{1},p_{1},\Phi(v_{1},p_{1}),0)$ so that $(w,j,\Phi(w,j))\in\pi_{1}[R^{\prime}_{0}(v_{1},p_{1},\Phi(v_{1},p_{1}),0)]$. We are done since $\Phi(w,j)\in K_{\mathsf{ad}(j)}(\Phi(v_{1},p_{1}))$.

For the converse implication, let $(u_{0},p_{0},q_{0})\in[\![Y_{0}]\!]_{g}$ for some $q_{0}\in Z$. Let $G=(W,R)$ be a history-free witness for this fact. By Lemma 4.3, it suffices to provide a strategy in the fixpoint game for the system $f$ with which $\mathsf{Eloise}$ wins the node $(u_{0},p_{0})$. We inductively construct a history-dependent strategy $s$ as follows: For $i\geq 0$, we abbreviate $U_{i}=R_{0}(u_{i},p_{i},q_{i},0)$. We put $s(u_{0},p_{0})=(P^{U_{0},q_{0}}_{0},\ldots,P^{U_{0},q_{0}}_{k})$. For the inductive step, let

[TABLE]

be a partial play of the fixpoint game that follows the strategy that has been constructed so far. Then we have an $R$-path $(u_{0},p_{0},q_{0},0),(u_{1},p_{1},q_{1},0),\ldots,(u_{n},p_{n},q_{n},0)$, where, for $0\leq i<n$, we have $(q_{i},p_{i+1},q_{i+1})\in K$ since $u_{i+1}\sqsubseteq P^{U_{i},q_{i}}_{p_{i+1}}$ by the inductive construction. Put $s(\tau)=(P^{U_{n},q_{n}}_{0},\ldots,P^{U_{n},q_{n}}_{k})$. Since $G$ is a witness, the strategy uses only moves that are available to $\mathsf{Eloise}$ (i.e. ones with $u_{n}\sqsubseteq f_{p_{n}}(s(\tau))$). Also, $s$ is a winning strategy as can be seen by looking at the $K$-paths that are induced by complete plays $\tau$ that follow $s$, as described (for partial plays) above. Since $S$ is a universal graph and hence even, every such $K$-path is even and the sequence of priorities in $\tau$ is just the sequence of priorities of one of these $K$-paths. ∎

Remark 5.4

Since the set $[\![Y_{0}]\!]_{g}$ is the greatest fixpoint of $g$, it can be computed by simple approximation from above, that is, as $g^{m}(B_{L}\times[k]\times Z)$ where $m=|B_{L}\times[k]\times Z|$. However, each iteration of the function $g$ may require up to $|Z|$ evaluations of an equation. In the next section, we will show how this additional iteration factor in the computation of $[\![Y_{0}]\!]_{g}$ can be avoided.

6 A Progress Measure Algorithm

We next introduce a lifting algorithm that computes the set $[\![Y_{0}]\!]_{g}$ efficiently, following the paradigm of the progress measure approach for parity games (e.g. [33, 34]). Our progress measures will map pairs $(u,i)\in B_{L}\times[k]$ to nodes in a universal graph that is equipped with a simulation order, that is, a total order that is suitable for measuring progress.

Definition 6.1 (Simulation order)

For natural numbers $i$, $i^{\prime}$, we put $i\succeq i^{\prime}$ if and only if either $i$ is even and $i=i^{\prime}$, or both $i$ and $i^{\prime}$ are odd and $i\geq i^{\prime}$. A total order $\leq$ on $Z$ is a simulation order if for all $q,q^{\prime}\in Z$,

[TABLE]

Lemma 2

There is an $(n(d+1),d+1)$-universal graph $(Z,K)$ of size quasipolynomial in $n$ and $d$, and over which a simulation order $\leq$ exists.

Proof (Sketch)

It has been shown [17, Theorem 2.2] (originally, in different terminology, [34]) that there are $(l,h)$-universal trees (a concept similar to, but slightly more concrete than universal graphs) with set of leaves $T$ such that $|T|\leq{2l}{{\log l+h+1}\choose{h}}$. Leaves in universal trees are identified by navigation paths, that is, sequences of branching directions, so that the leaves are linearly ordered by the lexicographic order $\leq$ on navigation paths (which orders leaves from the left to the right). As described in [16], one can obtain a universal graph $(T,K)$ over $T$ in which transitions $(q,i,q^{\prime})\in K$ for odd $i$ (the crucial case) move to the left, that is, $q^{\prime}$ is a leaf that is to the left of $q$ in the universal tree (so that $q^{\prime}<q$), ensuring universality. As it turns out, the lexicographic ordering on $T$ is a simulation order. Adapting this construction to our setting, we put $l=n(d+1)$ and $h=d+1$ and obtain a $(n(d+1),d+1)$-universal graph (along with a simulation order $\leq$) of size at most ${2n(d+1)}{{\log(n(d+1))+d+2}\choose{d+1}}$ which is quasipolynomial in $n$ and $d$. ∎

We fix an $(n(d+1),d+1)$-universal graph $(Z,K)$ and a simulation order $\leq$ on $Z$ for the remainder of the paper (these exist by the above lemma).

Definition 6.2 (Progress measure, lifting function)

We let $q_{\mathsf{min}}\in Z$ denote the least node w.r.t. $\leq$ and fix a distinguished top element $\star\notin Z$, and extend $\geq$ to $Z\cup\{\star\}$ by putting $\star\geq q$ for all $q\in Z$. A measure is a map $\mu\colon B_{L}\times[k]\to Z\cup\{\star\}$, i.e. assigns nodes in the universal graph or $\star$ to pairs $(v,p)\in B_{L}\times[k]$. A measure $\mu$ is a progress measure if whenever $\mu(v,p)\neq\star$, then $v\sqsubseteq f_{p}(U_{0}^{\mu,q},\ldots,U_{k}^{\mu,q})$ where $q=\mu(v,p)$ and

[TABLE]

We define a function $\mathsf{Lift}:(B_{L}\times[k]\to Z\cup\{\star\})\to(B_{L}\times[k]\to Z\cup\{\star\})$ on measures by

[TABLE]

where $\min(Z^{\prime})$ denotes the least element of $Z^{\prime}$ w.r.t. $\leq$, for $\emptyset\neq Z^{\prime}\subseteq Z$; also we put $\min(\emptyset)=\star$.

The lifting algorithm then starts with the least measure $\mathsf{m}_{\min}$ that maps all pairs $(v,p)\in B_{L}\times[k]$ to the minimal node (i.e. $\mathsf{m}_{\min}(v,p)=q_{\min}$) and repeatedly updates the current measure using $\mathsf{Lift}$ until the measure stabilizes.

Lifting algorithm

1. (1)

Initialize: Put $\mu:=\mathsf{m}_{\min}$. 2. (2)

If $\mathsf{Lift}(\mu)\neq\mu$, then put $\mu:=\mathsf{Lift}(\mu)$ and go to 2. Otherwise go to 3. 3. (3)

Return the set $\mathbb{E}=\{(v,p)\in B_{L}\times[k]\mid\mu(v,p)\neq\star\}$.

Lemma 3 (Correctness)

For all $v\in B_{L}$ and $0\leq p\leq k$, we have

[TABLE]

Proof (Sketch)

Let $\mu$ denote the progress measure that the algorithm computes. For one direction of the proof, let $(v,p)\in\mathbb{E}$. By Lemma 1 it suffices to construct a witness for $v\in[\![X_{p}]\!]_{f}$. We extract such a witness $(\mathbb{E},R)$ from the progress measure $\mu$, relying on the properties of the simulation order $\leq$ that is used to measure the progress of $\mu$ to ensure that any infinite sequence of measures that $\mu$ assigns to some $R$-path induces an infinite (and hence even) path in the employed universal graph. This shows that $(\mathbb{E},R)$ indeed is an even graph and hence a witness. For the converse direction, let $v\in[\![X_{p}]\!]_{f}$ so that there is, by Theorem 5.3, some $q\in Z$ such that $(v,p,q)\in[\![Y_{0}]\!]_{g}$. For $(u,i)$ such that there is $q^{\prime}\in Z$ such that $(u,i,q^{\prime})\in[\![Y_{0}]\!]_{g}$, let $q_{(u,i)}\in Z$ denote the minimal such node w.r.t. $\leq$. It now suffices that $\mu(u,i)\leq q_{(u,i)}$ for all such $(u,i)$, which is shown by induction on the number of iterations of the lifting algorithm.∎

Corollary 1

Solutions of systems of fixpoint equations can be computed with quasipolynomially many evaluations of equations.

Proof

Given an $(n(d+1),d+1)$-universal graph $(Z,K)$ and a simulation order on $Z$, the lifting algorithm terminates and returns the solution of $f$ after at most $n(d+1)\cdot|Z|$ many iterations. This is the case since each iteration (except the final iteration) increases the measure for at least one of the $n(d+1)$ nodes and the measure of each node can be increased at most $|Z|$ times. Using the universal graph and the simulation order from the proof of Lemma 2, we have $|Z|\leq{2n(d+1)}{{\log(n(d+1))+d+2}\choose{d+1}}$ so that the algorithm terminates after at most $2(n(d+1))^{2}{{\log(n(d+1))+d+2}\choose{d+1}}\in\mathcal{O}((n(d+1))^{\log(d+1)})$ iterations of the function $\mathsf{Lift}$. Each iteration can be implemented to run with at most $n(d+1)$ evaluations of an equation. ∎

Corollary 2

The number of function calls required for the solution of systems of fixpoint equations with $d\leq\log n$ is bounded by a polynomial in $n$ and $d$.

Proof

Following the insight of Theorem 2.8 in [9], Theorem 2.2. in [17] implies that if $d<\log n$, then there is an $(n(d+1),d+1)$-universal tree of size polynomial in $n$ and $d$. In the same way as in the proof of Lemma 2, one obtains a universal graph of polynomial size and a simulation order on it. ∎

Example 6.3

Applying Corollary 1 and Corollary 2 to Example 3.2, we obtain the following results:

1. (1)

The model checking problems for the energy $\mu$-calculus and finite latticed $\mu$-calculi are in $\mathsf{QP}$. For energy parity games with sufficient upper bound $b$ on energy level accumulations, we obtain a progress measure algorithm that terminates after a number of iterations that is quasipolynomial in $b$. 2. (2)

Under mild assumptions on the modalities (see [30]), the model checking problem for the coalgebraic $\mu$-calculus is in $\mathsf{QP}$; in particular, this yields $\mathsf{QP}$ model checking algorithms for the graded $\mu$-calculus and the two-valued probabilistic $\mu$-calculus (equivalently: $\mathsf{QP}$ progress measure algorithms for solving graded and two-valued probabilistic parity games). 3. (3)

Under mild assumptions on the modalities (see [31]), we obtain a novel upper bound $2^{\mathcal{O}({nd\log n})}$ for the satisfiability problems of coalgebraic $\mu$-calculi, in particular including the monotone $\mu$-calculus, the alternating-time $\mu$-calculus, the graded $\mu$-calculus and the (two-valued) probabilistic $\mu$-calculus, even when the latter two are extended with (monotone) polynomial inequalities. This improves on the best previous bounds in all cases.

7 Conclusion

We have shown how to use universal graphs to compute solutions of systems of fixpoint equations $X_{i}=\eta_{i}.\,f_{i}(X_{0},\ldots,X_{k})$ (with the $\eta_{i}$ marking least or greatest fixpoints) that use functions $f_{i}:L^{k+1}\to L$ (over a finite lattice $L$ with basis $B_{L}$) and involve up to $k+1$-fold nesting of fixpoints. Our progress measure algorithm needs quasipolynomially many evaluations of equations, and runs in time $\mathcal{O}(q\cdot t(f))$, where $q$ is a quasipolynomial in $|B_{L}|$ and the alternation depth of the equation system, and where $t(f)$ is an upper bound on the time it takes to compute $f_{i}$ for all $i$.

As a consequence of our results, the upper time bounds for the evaluation of various general parity conditions improve. Example domains beyond solving parity games to which our algorithm can be instantiated comprise model checking for latticed $\mu$-calculi and solving latticed parity games[7, 36], solving energy parity games and model checking for the energy $\mu$-calculus [10, 2], and model checking and satisfiability checking for the coalgebraic $\mu$-calculus [14]. The resulting model checking algorithms for latticed $\mu$-calculi and the energy $\mu$-calculus run in time quasipolynomial in the provided basis of the respective lattice. In terms of concrete instances of the coalgebraic $\mu$-calculus, we obtain, e.g., quasipolynomial-time model checking for the graded [38] and the probabilistic $\mu$-calculus [14, 41] as new results (corresponding results for, e.g., the alternating-time $\mu$-calculus [1] and the monotone $\mu$-calculus [22] follow as well but have already been obtained in our previous work [30]), as well as improved upper bounds for satisfiability checking in the graded $\mu$-calculus, the probabilistic $\mu$-calculus, the monotone $\mu$-calculus, and the alternating-time $\mu$-calculus. We foresee further applications, e.g. in the computation of fair bisimulations and fair equivalence [32, 37] beyond relational systems, e.g. for probabilistic systems.

As in the case of parity games, a natural open question that remains is whether solutions of fixpoint equations can be computed in polynomial time (which would of course imply that parity games can be solved in polynomial time). A more immediate perspective for further investigation is to generalize the recent quasipolynomial variant [46] of Zielonka’s algorithm [54] for solving parity games to solving systems of fixpoint equations, with a view to improving efficiency in practice.

Appendix 0.A Appendix

0.A.1 Omitted Proofs

Full proof of Lemma 2.

Proof

It has been shown in [17], Theorem 2.2. that there are $(l,h)$-universal trees with set of leaves $T$ such that $|T|\leq{2l}{{\log l+h+1}\choose{h}}$; following [16], we show how to obtain a universal graph $(Z,K)$ of the same size. The leaves in universal trees can be identified by navigation paths, that is, tuples $(m_{k},m_{k-2},\ldots,m_{1})$ of natural numbers that describe the position of the leaf within the tree. We put $Z=T$ and define the relation $K$ by putting

[TABLE]

for $0\leq i\leq k$, $(m_{k},m_{k-2},\ldots,m_{i})\in Z$. Here we use $(m_{k},m_{k-2},\ldots,m_{p})$ (for odd $p\geq 1$) to denote the rightmost leaf that is reachable from position $(m_{k},m_{k-2},\ldots,m_{p})$ in the universal tree. By $(l,h)$-universality of the used universal tree, $(K,Z)$ is a $(l,h)$-universal graph. Let $\leq$ be the lexicographic order on the leaves of the universal tree; then $\leq$ orders the leaves linearly from left to right. We show that $\leq$ is a simulation order on $(Z,K)$. Let $q=(m_{k},m_{k-2},\ldots,m_{1})\in Z$ and $q^{\prime}=(m^{\prime}_{k},m^{\prime}_{k-2},\ldots,m^{\prime}_{1})\in Z$ such that $q\leq q^{\prime}$. Furthermore let $0\leq i\leq k$ and $s\in K_{i}(q)$. We have to show that there are $i^{\prime}\succeq i$ and $s^{\prime}\in K_{i^{\prime}}(q^{\prime})$ such that $s\leq s^{\prime}$. If $q=q^{\prime}$, then we are done. If $q\neq q^{\prime}$ and there is $s^{\prime}\in K_{i}(q^{\prime})$, then $s^{\prime}=(m^{\prime}_{k},m^{\prime}_{k-2},\ldots,m^{\prime}_{i}-1)$ (if $i$ is odd) or $s^{\prime}=(m^{\prime}_{k},m^{\prime}_{k-2},\ldots,m^{\prime}_{i-1})$ (if $i$ is even). In the first case, we have $s=(m_{k},m_{k-2},\ldots,m_{i}-1)$ and in the second case, we have $s=(m_{k},m_{k-2},\ldots,m_{i-1})$. In both cases we have $i\succeq i$ and $s\leq s^{\prime}$ follows from $q\leq q^{\prime}$. If $q\neq q^{\prime}$ and $K_{i}(q^{\prime})=\emptyset$, then $i$ is odd (and $m^{\prime}_{i}=0$) and there is an odd number $i^{\prime}>i$ such that $m_{i^{\prime}}<m^{\prime}_{i^{\prime}}$, since $q<q^{\prime}$. Since $m^{\prime}_{i^{\prime}}>m_{i^{\prime}}\geq 0$, there is $s^{\prime}=(m_{k},m_{k-2},\ldots,m_{i^{\prime}}-1)\in K_{i^{\prime}}(q^{\prime})\neq\emptyset$. It remains to show $i^{\prime}\succeq i$ and $s=(m_{k},m_{k-2},\ldots,m_{i-1})\leq(m_{k},m_{k-2},\ldots,m_{i^{\prime}}-1)=s^{\prime}$. The former follows from $i^{\prime}>i$ and the fact that both $i$ and $i^{\prime}$ are odd, and the latter follows from $i^{\prime}>i$ together with $m_{i^{\prime}}<m^{\prime}_{i^{\prime}}$ by the definition of lexicographic ordering.

Putting $l=n(k+1)$ and $h=k+1$, we hence obtain an $(n(k+1),k+1)$-universal graph of (quasipolynomial) size at most ${2n(k+1)}{{\log(n(k+1))+k+2}\choose{k+1}}$ and a simulation order $\geq$ on this graph.∎

Full proof of Lemma 3.

Proof

For one direction of the proof, we let $\mu$ be the measure that is obtained at the end of the execution of the lifting algorithm. Then we have $\mathsf{Lift}(\mu)=\mu$ so that $\mu$ is a progress measure. Let $(v,p)\in\mathbb{E}$. By Lemma 1 it suffices to exhibit a history-free witness $(W,R)$ for $v\in[\![X_{p}]\!]_{f}$. We put $W=\mathbb{E}$, having $(v,p)\in W$, and define the relation $R\subseteq W\times[d]\times W$ by

[TABLE]

for $(u,i)\in W$ and $0\leq i^{\prime}\leq d$, having $\star\neq\mu(u,i)\in Z$ by definition of $W$. To show that $(W,R)$ is a history-free witness, we first show that for all $(v,p)\in W$, we have $v\sqsubseteq f_{p}(U_{0},\ldots,U_{k})$ where

[TABLE]

for $1\leq i\leq k$. Since $\mu$ is a progress measure, we have

[TABLE]

Our claim $v\sqsubseteq f_{p}(U_{0},\ldots,U_{k})$ follows since we have, for all $1\leq i\leq k$, that by the definition of $R_{\mathsf{ad}(i)}$,

[TABLE]

It remains to show that $(W,R)$ is an even graph. To see this, let

[TABLE]

be an infinite path in $(W,R)$, that is, let $((u_{i},p_{i}),p_{i+1},(u_{i+1},p_{i+1}))\in R$ for all $i\geq 0$. We have to show that $\pi$ is even. We construct an infinite path

[TABLE]

in the universal graph $(Z,K)$ as follows: We put $s_{0}=\mu(u_{0},p_{0})$, and define $q_{i+1}$ and $s_{i+1}$ inductively from $s_{i}$ for all $i\geq 0$, ensuring the invariant

[TABLE]

First we note that (0.A.1) holds trivially at $i=0$. Next we define $q_{i+1}$ and $s_{i+1}$ for $i\geq 0$, assuming that (0.A.1) holds at $i$. By definition of $R$, it follows from $((u_{i},p_{i}),p_{i+1},(u_{i+1},p_{i+1}))\in R$ that there is $s\in K_{\mathsf{ad}({p_{i+1}})}(\mu(u_{i},p_{i}))$ such that $\mu(u_{i+1},p_{i+1})\leq s$. By the assumption on $\geq$, $s\in K_{\mathsf{ad}(p_{i+1})}(\mu(u_{i},p_{i}))$ and the invariant $s_{i}\geq\mu(u_{i},p_{i})$ imply that there is some $p$ and some $s^{\prime}\in K_{p}(s_{i})$ such that $p\succeq\mathsf{ad}(p_{i+1})$ and $s^{\prime}\geq s$. Put $q_{i+1}:=p$ and $s_{i+1}:=s^{\prime}$; then $s_{i+1}\in K_{q_{i+1}}(s_{i})$ and $\mu(u_{i+1},p_{i+1})\leq s\leq s_{i+1}$, so the invariant (0.A.1) holds at $i+1$. For later use, we point out that we have $q_{i}\succeq\mathsf{ad}(p_{i})$ for all $i>0$ by construction of $\tau$.

The path $\tau$, being an infinite path in the universal graph $(Z,K)$, is even. Since we have $q_{i}\succeq\mathsf{ad}(p_{i})$ for all $i>0$, $p_{i}$ is even if and only if $q_{i}$ is even (and then $q_{i}=\mathsf{ad}(p_{i})$), and $p_{i}$ is odd if and only if $q_{i}$ is odd (and then $q_{i}\geq\mathsf{ad}(p_{i})$). Let $q$ be the highest priority that occurs infinitely often in $\tau$. Then $q$ is even and there are infinitely many positions $i$ such that $q_{i}=q=\mathsf{ad}(p_{i})$ and there is some position $i^{\prime}$ such that for all positions $i^{\prime\prime}>i^{\prime}$, $\mathsf{ad}(p_{i^{\prime\prime}})\leq q_{i^{\prime\prime}}\leq q$. Hence $\pi$ is an even path, as required.

For the converse direction, let $u\in[\![X_{i}]\!]_{f}$. We note that the lifting algorithm computes a progress measure as the least fixpoint of the function $\mathsf{Lift}$ in the lattice of measures, pointwise ordered by the order $\leq$ on nodes of the universal graph. Let $\mu$ be the measure that is obtained at the end of the execution of the lifting algorithm. Then we have $\mathsf{Lift}(\mu)=\mu$ and $\mu=\mathsf{Lift}^{n}(\mathsf{m}_{\min})$ for some natural number $n$ (recall that $\mathsf{m}_{\min}$ denotes the minimal measure). We have to show that $(u,i)\in\mathbb{E}$, i.e. $\mu(u,i)\neq\star$. By Theorem 5.3, there is $q\in Z$ such that $(u,i,q)\in[\![Y_{0}]\!]_{g}$. For all $(v,p)$ such that there is $q^{\prime}\in Z$ such that $(v,p,q^{\prime})\in[\![Y_{0}]\!]_{g}$, we let $q_{(v,p)}\in Z$ denote the least (w.r.t. $\leq$) node of the universal graph with this property. It suffices to show that in this case,

[TABLE]

We proceed by induction over $n$. If $n=0$, then $\mathsf{Lift}^{n}(\mathsf{m}_{\min})=\mathsf{m}_{\min}$ and $\mathsf{m}_{\min}(v,p)=q_{\mathsf{\min}}\leq q_{(v,p)}$. If $n>0$, then we have to show the inequality in

[TABLE]

where $\mu_{n-1}=\mathsf{Lift}^{n-1}(\mathsf{m}_{\min})$. This follows once we show that

[TABLE]

i.e.

[TABLE]

Now since $[\![Y_{0}]\!]_{g}$ is a fixpoint of $g$, we have

[TABLE]

So given that $(v,p,q_{(v,p)})\in[\![Y_{0}]\!]_{g}$, we have

[TABLE]

which implies our goal (0.A.2) by monotonicity of $f_{p}$ once we show that $P_{i}^{[\![Y_{0}]\!]_{g},q_{(v,p)}}\sqsubseteq U_{i}^{\mu_{n-1},q_{(v,p)}}$ for $0\leq i\leq k$. Both sides of this inequality are defined as joins of sets; it suffices to show the set inclusion between these sets. So let $u^{\prime}\in B_{L}$ such that there is $q^{\prime}\in K_{\mathsf{ad}(i)}(q_{(v,p)})$ such that $(u^{\prime},i,q^{\prime})\in[\![Y_{0}]\!]_{g}$ ($P_{i}^{[\![Y_{0}]\!]_{g},q_{(v,p)}}$ is the join of all such $u^{\prime}$). We claim that $u^{\prime}$ is in the set

[TABLE]

(whose join is $U_{i}^{\mu_{n-1},q_{(v,p)}}$ since $\mu_{n-1}=\mathsf{Lift}^{n-1}(\mathsf{m}_{\min})$). Indeed, pick $s=q^{\prime}$ so that $s\in K_{\mathsf{ad}(i)}(q_{(v,p)})$. It remains to show that $(\mathsf{Lift}^{n-1}(\mathsf{m}_{\min}))(u^{\prime},i)\leq s$. By the inductive hypothesis, $(\mathsf{Lift}^{n-1}(\mathsf{m}_{\min}))(u^{\prime},i)\leq q_{(u^{\prime},i)}$, so it suffices to show $q_{(u^{\prime},i)}\leq s$. This follows from the fact that $s=q^{\prime}$ and $(u^{\prime},i,q^{\prime})\in[\![Y_{0}]\!]_{g}$, since $q_{(u^{\prime},i)}$ is by definition the least node (w.r.t. $\leq$) such that $(u^{\prime},i,q_{(u^{\prime},i)})\in[\![Y_{0}]\!]_{g}$. ∎

0.A.2 Details on Applications to Coalgebraic $\mu$-Calculi

Example 0.A.1

We consider probabilistic parity games, which make use of systems of fixpoint equations that deviate considerably from (and apparently do not reduce easily to) the ones for standard parity games. Probabilistic parity games are parity games in which both moves and nodes are annotated with probabilities (these games are not to be confused with the $2\frac{1}{2}$-player stochastic parity games that are considered in [12, 27]). They arise naturally as model checking games for the (two-valued) probabilistic $\mu$-calculus (see Example 0.A.2.(2)); we postpone a more formal and detailled treatment to Section 0.A.2 below, where we discuss the more general coalgebraic $\mu$-calculus (covering e.g. probabilistic, graded and the alternating-time $\mu$-calculi as instances) and its model checking problem (corresponding to solving e.g. probabilistic, graded and alternating-time parity games).

A probabilistic parity game $(V,D,\Omega,\sigma)$ consists of a set $V$ of nodes, a set of probabilistic moves, given by a function $D$ which assigns probability distributions $D(v)$ over $V$ (with $\Sigma_{w\in V}(D(v))(w)=1$) to nodes $v\in V$, a priority function $\Omega:V\to\mathbb{N}$ and a probability assignment $\sigma:V\to[0,1]$. The intuition of $(D(v))(w)=p$ is that the move from $v$ node to node $w$ has probability $p$. A play $\rho=v_{0},v_{1},\ldots$ in a probabilistic parity game is a sequence of nodes such that for all $i\geq 0$, we have $(D(v_{i}))(v_{i+1})>0$ and the winning conditions on plays are the same as in standard parity games. A (history-free) strategy is a partial function $s:V\rightharpoonup\mathcal{P}(V)$ such that for all $v\in\mathsf{dom}(s)$, $\Sigma_{w\in s(v)}(D(v))(w)>\sigma(v)$, that is, strategies pick sets of moves whose joint probability is larger than the probability assignment of the respective node. Crucially, strategies in probabilistic parity games involve branching, unlike strategies in standard parity games which pick single moves for each node on which they are defined. An $s$-play is a play $\rho=v_{0},v_{1},\ldots$ such that for all $i\geq 0$, $v_{i}\in\mathsf{dom}(s)$ and $v_{i+1}\in s(v_{i})$. Player $\mathsf{Eloise}$ wins a node $v$ if there is a strategy $s$ such that $\mathsf{Eloise}$ wins all $s$-plays that start at $v$. We point out that the (somewhat concealed) two-player nature of probabilistic parity games manifests in the fact that $\mathsf{Eloise}$ has to pick, in each turn, some suitable set of moves, whereupon $\mathsf{Abelard}$ can challenge any of these moves (that is, all $s$-plays need to be even in order for $s$ to be a winning strategy for $\mathsf{Eloise}$). Player $\mathsf{Eloise}$ hence wins a node $v$ if and only if there is a set $W\subseteq V$ containing $v$ and a graph $G=(W,R\subseteq W\times W)$ such that

• –

each $R$-edge has $D$-probability greater than 0,

• –

for each $w\in W$, the $R$-successors of $w$ have a joint $D$-probability of more than $\sigma(w)$ and

• –

for each infinite $R$-path that starts at $v$, the highest priority that is visited infinitely often by the path is even.

Consider, for instance, the probabilistic parity game depicted below with $V=\{0,1,2,3\}$, $\Omega(i)=i$ for $i\in V$ and, e.g. $(D(0))(1)=0.2$, $(D(3))(1)=1$ and $(D(3))(3)=0$; let us fix the probability assigment $\sigma$ by putting $\sigma(0)=0.7$, $\sigma(1)=0.3$ $\sigma(2)=0.1$ and $\sigma(3)=0$.

[math]1$$2$$3$$0.5$$0.2\,\,$$\,0.3$$0.8$$\,\,0.2     0.4$$\,0.6$$\,1

To win e.g. the node [math], $\mathsf{Eloise}$ has to have a strategy that selects a set of nodes that have a joint probability (of being reached from [math] in one step) greater than $\sigma(0)=0.7$ and that are in turn all won by the strategy. In this example, player $\mathsf{Eloise}$ wins the nodes [math] and $2$ with the strategy $s$ defined by $s(0)=\{0,2\}$ and $s(2)=\{2\}$: this function indeed is a valid strategy since it uses only moves with nonzero probabilities and also respects the probability assignment $\sigma$ as we have $\Sigma_{j\in s(0)}(D(0))(j)=0.5+0.3>\sigma(0)=0.7$ and $\Sigma_{j\in s(2)}(D(2))(j)=0.4>\sigma(2)=0.1$. Also, every $s$-play that starts at node [math] is of the form $0^{\omega}$ or $0^{*}2^{\omega}$ and hence even and every $s$-play that starts at node $2$ is of the form $2^{\omega}$ and hence even. On the other hand, there is no strategy with which $\mathsf{Eloise}$ can win the nodes $1$ or $3$ since for any strategy $t$ with $1\in\mathsf{dom}(t)$, we have $\Sigma_{w\in t(1)}(D(1))(w)>\sigma(1)=0.3$ and hence $1\in t(1)$; but then there is an odd $t$-play of the form $1^{\omega}$ so that $t$ is not a winning strategy for $\mathsf{Eloise}$. Also, for any candidate winning strategy $u$ with $3\in\mathsf{dom}(u)$, we have $u(3)=\{1\}$ and hence $1\in\mathsf{dom}(u)$ which shows that $u$ is not a winning strategy for $\mathsf{Eloise}$. Hence we have $\mathsf{win}_{\exists}=\{0,2\}$ and $\mathsf{win}_{\forall}=\{1,3\}$.

The winning regions in probabilistic parity games are again just nested fixpoints, where the functions however deviate significantly from the functions for standard parity games. Player $\mathsf{Eloise}$ has to pick sets of moves now, so it does not suffice to consider existential or universal branching, like in the function $f_{\exists}$ for standard parity games. We define $f_{\exists p}:\mathcal{P}(V)^{k+1}\to\mathcal{P}(V)$, for $(V_{0},\ldots,V_{k})\in\mathcal{P}(V)^{k+1}$, by putting

[TABLE]

Then we have $\mathsf{win}_{\exists}=\mathsf{E}^{f_{\exists p}}$ (formally, this is a consequence of Lemma 4, below). The winning region of $\mathsf{Abelard}$ is characterized in a dual manner. Note that nodes $v$ with $\sigma(v)=p$ correspond to model checking modal operators $\langle p\rangle$ which require that their argument is satisfied with probability more than $p$ in the next step (see Example 0.A.2.(2)). The full probabilistic $\mu$-calculus also has dual operators $[p]$ which state that their argument holds with probability at least $1-p$ in the next step; for brevity, we refrain from modelling these operators in this example.

While the above example apparently already goes beyond the setting of [11] in which standard parity games with existential and universal branching are hardwired throughout (e.g. in the set operator $\mathit{CPre}$ and the function $\mathit{best}$), we note that our results cover systems of fixpoint equations for arbitrary functions over finite lattices, which need not be ‘game-like’ at all, that is, they need not be parametrized by any graph structure or priority and player assignment.

We next show how to apply our results to model checking and satisfiability checking for generalized $\mu$-calculi in the setting of coalgebraic logic, covering, for instance, graded [38], probabilistic [15, 41], and alternating-time [1] $\mu$-calculi. It has been shown in previous work [30] that model checking for coalgebraic $\mu$-calculi reduces to computing winning regions in a generalized variant of parity games where the game arenas are coalgebras instead of Kripke frames. We proceed to recall basic definitions and examples in universal coalgebra [49] and the coalgebraic $\mu$-calculus [14] and then continue to show that our main result yields new quasipolynomial-time upper bounds for the model checking problem and improves the known exponential-time upper bound for the satisfiability problem [31] of the coalgebraic $\mu$-calculus. These generic results instantiate to new upper bounds in all concrete cases except the standard relational $\mu$-calculus.

The abstraction principle underlying universal coalgebra is to encapsulate system types as functors, for our present purposes on the category of sets. Such a functor $T:\mathsf{Set}\to\mathsf{Set}$, which we fix in the following, maps every set $X$ to a set $TX$, and every map $f:X\to Y$ to a map $Tf:TX\to TY$, preserving identities and composition. We think of $TX$ as a type of structured collections over $X$; a basic example is the covariant powerset functor $\mathcal{P}$, which assigns to each set its powerset and acts on maps by taking forward image. Systems of the intended type are then cast as $T$-coalgebras $(C,\xi)$ (or just $\xi$) consisting of a set $C$ of states and a transition map $\xi:C\to TC$, thought of as assigning to each state $x\in C$ a structured collection $\xi(x)\in TC$ of successors. E.g. a $\mathcal{P}$-coalgebra $\xi:C\to\mathcal{P}C$ assigns to each state a set of successors, i.e. is a transition system.

Following the paradigm of coalgebraic logic [15], we fix a set $\Lambda$ of modal operators; we interpret each $\heartsuit\in\Lambda$ as predicate lifting ${[\![\heartsuit]\!]}$ for $T$, i.e. a natural transformation

[TABLE]

Here, the index $X$ ranges over all sets; $2^{X}$ denotes the set of maps $X\to 2$ into the two-element set $2=\{\bot,\top\}$, isomorphic to the powerset of $X$ (i.e. $2^{-}$ is the contravariant powerset functor; we generally keep the conversion between $2^{X}$ and $\mathcal{P}(X)$ implicit); and naturality means that ${[\![\heartsuit]\!]}_{X}(f^{-1}[A])=(Tf)^{-1}[{[\![\heartsuit]\!]}_{Y}(A)]$ for $f:X\to Y$ and $A\in 2^{Y}$. Thus, the predicate lifing ${[\![\heartsuit]\!]}$ indeed lifts predicates on a base set $X$ to predicates on the set $TX$. Standard examples for $T=\mathcal{P}$ are the predicate liftings for the $\square$ and $\lozenge$ modalities, given by

[TABLE]

for $A\in PX$. Since we mean to form fixpoint logics, we need to require that every ${[\![\heartsuit]\!]}$ is monotone, that is, $A\subseteq B\subseteq X$ implies $[\![\heartsuit]\!]_{X}(A)\subseteq[\![\heartsuit]\!]_{X}(B)$. To support negation, we assume moreover that $\Lambda$ is closed under duals, i.e. for each $\heartsuit\in\Lambda$ we have $\overline{\heartsuit}\in\Lambda$ such that ${[\![\overline{\heartsuit}]\!]}_{X}(A)=TX\setminus{[\![\heartsuit]\!]}_{X}(X\setminus A)$, chosen so that $\overline{\overline{\heartsuit}}=\heartsuit$ (e.g. $\overline{\square}=\lozenge$, $\overline{\lozenge}=\square)$.

Given a set $\mathsf{Var}$ of fixpoint variables, the set of formulae $\phi,\psi,\dots$ of the coalgebraic $\mu$-calculus is then defined by the grammar

[TABLE]

Given a $T$-coalgebra $\xi:C\to TC$ and a valuation $\sigma:\mathsf{Var}\to\mathcal{P}C$, the extension

[TABLE]

of a formula $\phi$ is defined recursively by $[\![X]\!]_{\sigma}=\sigma(X)$; the expected clauses for the propositional operators (${[\![\top]\!]}_{\sigma}=C$; ${[\![\bot]\!]}_{\sigma}=\emptyset$; ${[\![\phi\land\psi]\!]}_{\sigma}={[\![\phi]\!]}_{\sigma}\cap{[\![\psi]\!]}_{\sigma}$; ${[\![\phi\lor\psi]\!]}_{\sigma}={[\![\phi]\!]}_{\sigma}\cup{[\![\psi]\!]}_{\sigma}$); and

[TABLE]

where the (monotone) map $[\![\psi]\!]^{X}_{\sigma}:\mathcal{P}C\to\mathcal{P}C$ is defined by $[\![\psi]\!]^{X}_{\sigma}(A)=[\![\psi]\!]_{\sigma[X\mapsto A]}$ for $A\subseteq C$, with $(\sigma[X\mapsto A])(X)=A$ and $(\sigma[X\mapsto A])(Y)=\sigma(Y)$ for $X\neq Y$.

The alternation depth $\mathsf{ad}(\eta X.\psi)$ of a fixpoint $\eta X.\psi$ is the depth of alternating nesting of such fixpoints in $\psi$ that depend on $X$; we assign odd numbers to least fixpoints and even numbers to greatest fixpoints. E.g. for $\psi=\nu X.\phi$ and $\phi=\mu Y.(p\wedge\heartsuit X)\vee\heartsuit Y$, we have $\mathsf{ad}(\psi)=2$, $\mathsf{ad}(\phi)=1$. For a detailed definition of alternation depth, see e.g. [44].

Example 0.A.2

As indicated above, the standard relational $\mu$-calculus [35] is one example of a coalgebraic $\mu$-calculus, with propositional atoms treated as nullary modalities. Further important examples are as follows [50, 14, 51].

1. (1)

The graded $\mu$-calculus [38] has modalities $\langle b\rangle$, $[b]$, indexed over $b\in{\mathbb{N}}$, read ‘in more than $b$ successors’ and ‘in all but at most $b$ successors’, respectively. These can be interpreted over relational structures but it is more natural and technically more convenient to use multigraphs [18], i.e. transition systems with edge weights (multiplicities) in ${\mathbb{N}}\cup\{\infty\}$, which are coalgebras for the multiset functor $\mathcal{B}$ given by $\mathcal{B}X=(X\to({\mathbb{N}}\cup\{\infty\}))$. Over $\mathcal{B}$, we interpret $\langle b\rangle$ and $[b]$ by the mutually dual predicate liftings

[TABLE]

E.g. the formula $\nu X.\,(\phi\land\lozenge_{1}X)$ says that the current state is the root of an infinite tree with branching degree at least $2$ (counting multiplicities) on which $\phi$ holds everywhere. 2. (2)

The (two-valued) probabilistic $\mu$-calculus [14, 41] is interpreted over Markov chains, which are coalgebras for the discrete distribution functor $\mathcal{D}$ where $\mathcal{D}X=\{\beta:X\to[0,1]\mid\sum_{x\in X}\beta(x)=1\}$ is the set of discrete probability distributions on $X$, represented, e.g., as probability mass functions $\beta:X\to[0,1]$. We abuse $\beta$ to denote also the induced probability distribution, writing $\beta(A)=\sum_{x\in A}\beta(x)$ for $A\subseteq X$. The logic has modalities $[p]$, $\langle p\rangle$ indexed over $p\in[0,1]\cap{\mathbb{Q}}$, interpreted over $\mathcal{D}$ by

[TABLE]

This example (as well as the previous one) can be extended to admit (monotone) polynomial inequalities among probabilities (or multiplicities, respectively) instead of only comparison with constants, allowing, e.g., for expressing probabilistic independence [23, 39, 31]. In more detail, we can introduce $n$-ary modalities $L_{p,b}$, $M_{p,b}$ indexed over polynomials $p\in{\mathbb{Q}}_{\geq 0}[x_{1},\dots,x_{n}]$ and rational numbers $b\geq 0$, with $L_{p,b}$ interpreted by the predicate lifting

[TABLE]

and $M_{p,b}$ by the corresponding dual predicate lifting. E.g. the formula

[TABLE]

says roughly that if we independently sample two successors of the current state, then with probability at least $0.8$, the first successor state will satisfy $p$, and then $X$ again (continuing indefinitely), and the second successor state will remain on a path where it satisfies $Y$ again until it eventually reaches $q$. 3. (3)

Monotone $\mu$-calculus: The monotone neighbourhood functor ${\mathcal{M}}$ maps a set $X$ to the set

[TABLE]

of set systems over $X$ that are upwards closed under subset inclusion (i.e. $A\in{\mathfrak{A}}$ and $A\subseteq B$ imply $B\in{\mathfrak{A}}$). Coalgebras for ${\mathcal{M}}$ are monotone neighbourhood frames in the sense of Scott-Montague semantics [13]. We take $\Lambda=\{\square,\lozenge\}$ and interpret $\square$ over ${\mathcal{M}}$ by the predicate lifting

[TABLE]

and $\lozenge$ by the corresponding dual lifting, ${[\![\lozenge]\!]}_{X}(A)=\{{\mathfrak{A}}\in{\mathcal{M}}X\mid(X\setminus A)\notin{\mathfrak{A}}\}=\{{\mathfrak{A}}\in{\mathcal{M}}X\mid\forall B\in{\mathfrak{A}}.\,B\cap A\neq\emptyset\}$. The arising coalgebraic $\mu$-calculus is known as the monotone $\mu$-calculus [22]. When we add propositional atoms and actions, and replace ${\mathcal{M}}$ with its subfunctor ${\mathcal{M}}_{s}$ defined by ${\mathcal{M}}_{s}X=\{{\mathfrak{A}}\in{\mathcal{M}}X\mid\emptyset\notin{\mathfrak{A}}\owns X\}$, whose coalgebras are serial monotone neighbourhood frames, we arrive at the ambient fixpoint logic of concurrent dynamic logic [48] and Parikh’s game logic [45]. In game logic, actions are understood as atomic games of Angel vs. Demon, and we read $\square_{a}\phi$ as ‘Angel has strategy to enforce $\phi$ in game $a$’. Game logic is then mainly concerned with composite games, formed by the control operators of dynamic logic and additional ones; the semantics can be encoded into fixpoint definitions. For instance, the formula $\nu X.\,p\land\square_{a}X$ says that Angel can enforce $p$ in the composite game where $a$ is played repeatedly, with Demon deciding when to stop. 4. (4)

Alternating-time $\mu$-calculus: Fix a set $N=\{1,\dots,n\}$ of agents. Using alternative notation from coalition logic [47], we present the alternating-time $\mu$-calculus (AMC) [1] by modalities $[D]$, $\langle D\rangle$ indexed over coalitions $D\subseteq N$, read ‘$D$ can enforce’ and ‘$D$ cannot prevent’, respectively. We define a functor $\mathcal{G}$ by

[TABLE]

where we write $[k]=\{1,\dots,k\}$ in this example. We understand $(k_{1},\dots,k_{n},f)\in\mathcal{G}X$ as a one-step concurrent game with $k_{i}$ available moves for agent $i\in N$, and outcomes in $X$ determined by the outcome function $f$ from a joint choice of moves by all the agents. For $D\subseteq N$, we write $S_{D}=\prod_{i\in D}[k_{i}]$. Given joint choices $s_{D}\in S_{D}$, $s_{\overline{D}}\in S_{\overline{D}}$ of moves for $D$ and $\overline{D}=N\setminus D$ respectively, we write $(s_{D},s_{\overline{D}})\in s_{N}$ for the joint move of all agents induced in the evident way. In this notation, we interpret the modalities $[D]$ over $\mathcal{G}$ by the predicate lifting

[TABLE]

and the modalities $\langle D\rangle$ by dualization. This captures exactly the semantics of the AMC: $\mathcal{G}$-coalgebras are precisely concurrent game structures [1], i.e. assign a one-step concurrent game to each state, and $[D]\phi$ says that the agents in $D$ have a joint move such that however the agents in $\overline{D}$ move, the next state will satisfy $\phi$. E.g. $\nu Y.\,\mu X.\,(p\land[D]Y)\lor[D]X$ says that coalition $D$ can enforce that $p$ is satisfied infinitely often.

We now fix a target formula $\chi$ that does not contain free fixpoint variables, assuming w.l.o.g. that $\chi$ is clean, i.e. that every fixpoint variable is bound by at most one fixpoint operator in $\chi$. For a variable $x\in\mathsf{Var}$ that is bound in $\chi$, we then write $\theta(x)$ to denote the formula $\eta X.\psi$ that is a subformula of $\chi$. Let $\mathsf{Cl}(\chi)$ be the closure (that is, the set of subformulae) of $\chi$. We have $|\mathsf{Cl}(\chi)|\leq|\chi|$, where $|\chi|$ denotes the number of operators or variables in $\chi$.

We proceed to recall how model checking in the coalgebraic $\mu$-calculus is reduced to computing a nested fixpoint of a particular function [30]:

Definition 1 (Coalgebraic model checking function)

Let $\xi:C\to TC$ be a coalgebra, and $U=\mathsf{Cl}(\chi)\times C$. The (coalgebraic) model checking function $\alpha_{\mathsf{mc}}:\mathcal{P}(U)^{k+1}\to\mathcal{P}(U)$ is given by putting, for $\mathbf{U}=(U_{1},\ldots,U_{k+1})\in\mathcal{P}(U)^{k+1}$,

[TABLE]

Lemma 4 (Coalgebraic model checking [30])

Let $\chi$ be a formula of alternation depth $k$, $\xi:C\to TC$ a coalgebra, and $x\in C$ a state. Then we have

[TABLE]

The one-step satisfaction problem consists in deciding whether $t\in[\![\heartsuit]\!](W),$ for given $t\in TC$, $\heartsuit\in\Lambda$ and $W\subseteq C$. The time $t(\alpha_{\mathsf{mc}})$ it takes to compute the model checking function $\alpha_{\mathsf{mc}}$ hence depends on the time it takes to solve the one-step satisfaction problem for the modal operators at hand. By Corollary 1, we obtain

Corollary 3

Model checking for coalgebraic $\mu$-calculus formulae of alternation depth $k$ against coalgebras $\xi:C\to TC$ can be done in time $t_{2}\cdot t_{1}$ where $t_{2}=\max(t(\alpha_{\mathsf{mc}}),t_{1})$, $t_{1}={2n^{3}(k+1)^{2}}{{\log(n(k+1))+k+2}\choose{k+1}}$, and $n=|\mathsf{Cl}(\chi)|\cdot|C|$.

Example 0.A.3 (Quasipolynomial-time model checking for graded and probabilistic

$\mu$-calculi)

In [30, Examples 3.2 and 3.3], it was shown that in the graded and probabilistic cases, the one-step satisfaction problem can be solved in time $\mathcal{O}(\mathsf{size}(\chi)\cdot|C|)$ and $\mathcal{O}(\mathsf{size}(C)^{2}\cdot|C|^{3})$, respectively; here, $\mathsf{size}(\chi)$ denotes the representation size of the formula $\chi$ and $\mathsf{size}(C)$ denotes the representation size of the coalgebra $C$. We hence obtain the following quasipolynomial upper time bounds for the model checking problems of the respective $\mu$-calculi, both with numbers coded in binary (where $t_{1}={2n^{3}(k+1)^{2}}{{\log(n(k+1))+k+2}\choose{k+1}}$ and $n=|\mathsf{Cl}(\chi)|\cdot|C|$):

• •

for the graded $\mu$-calculus: $\mathcal{O}(t_{1}\cdot t_{2})$, where $t_{2}=\max(\mathsf{size(\chi)}\cdot|C|,t_{1})$;

• •

for the probabilistic $\mu$-calculus: $\mathcal{O}(t_{1}\cdot t_{2})$, where $t_{2}=\max(\mathsf{size}(C)^{2}\cdot|C|^{3},t_{1})$.

Similar bounds, with slightly larger $t_{2}$, are obtained for the respective extensions with polynomial inequalities. To the best of our knowledge, these bounds are new. We similarly obtain quasipolynomial bounds for model checking the monotone $\mu$-calculus and the alternating-time $\mu$-calculus. In these cases, the time bounds are already in [30], via an encoding into standard parity games; but we emphasize again that the point of our main result (Corollary 1) is not so much the time bound but rather the quasipolynomial bound on the number of iterations – in this case, we obtain that the fixpoint can be computed with quasipolynomially many calls to the one-step satisfaction problem (which at least for the alternating-time case seems also algorithmically preferable to an encoding in parity games with many additional states).

We now consider satisfiability checking for the coalgebraic $\mu$-calculus, which also reduces to the computation of a nested fixpoints of a certain function [31]. We recall the essential notions that are required to define this function; see [31] for details of the construction. We fix a target formula $\chi$ of size $n$ and alternation depth $k$, to be checked for satisfiability. One then has a deterministic parity automaton that accepts precisely the good branches in tableaux representing prospective models of $\chi$, i.e. the ones not containing infinite deferrals of least fixpoints (which represent eventualities). We work with parity automata in which priorities are assigned to the transitions (rather than the states); our automaton thus has the form $(D_{\chi},\Sigma,\delta,\beta)$ where $D_{\chi}$ is the set of states; $\Sigma$ is the alphabet (designed to allow identifying manipulations of formulae happening in the transitions); $\delta$ is the transition function; and $\beta$ assigns priorities to transitions. Since the automaton is deterministic, we can take $\beta$ to be a function $D_{\chi}\times\Sigma\to{\mathbb{N}}$. Recall that such a parity automaton accepts an infinite word $w$ if and only if it has a run for $w$ in which the highest priority that occurs infinitely often is even. We have $|D_{\chi}|\in\mathcal{O}(2^{\mathcal{O}(nk\log n)})$, and nodes $v\in D_{\chi}$ are labelled with sets $l(v)$ of formulae. We denote the set of nodes whose labels contain some propositional formula by $\mathsf{prestates}$ and the set of nodes whose labels contain only modal formulae by $\mathsf{states}$; for $v\in\mathsf{prestates}$, $\psi_{v}$ is a fixed propositional formula from the label of $v$. The transition function $\delta$ tracks sets of formulae according to the logical manipulations described by a given letter from $\Sigma$. Besides letters identifying propositional transformations, $\Sigma$ contains sets of modal formulae describing modal steps; we write $\mathsf{selections}\subseteq\Sigma$ for the set of these letters.

Definition 2 (Coalgebraic satisfiability checking function [31])

For sets $U\subseteq D_{\chi}$ and $\mathbf{U}=(U_{1},\ldots,U_{2nk})\in\mathcal{P}(U)^{2nk}$, we put

[TABLE]

where $\beta(v,(\psi_{v},b))$ abbreviates $\beta(v,(\psi_{v},b),\delta(v,(\psi_{v},b)))$ and where

[TABLE]

The one-step satisfiability problem is to decide whether

[TABLE]

for given $U$, $v$. Hence checking whether some $v\in\mathsf{prestates}$ is contained in $\alpha_{\mathsf{sat}}(\mathbf{U})$ for given $\mathbf{U}$ is an instance of the one-step satisfiability problem.

Lemma 5 (Fixpoint characterization of satisfiability [31])

In the above notation,

[TABLE]

Corollary 4

If the one-step satisfiability problem of a coalgebraic logic can be solved in time $2^{\mathcal{O}({nk\log n})}$, then the satisfiability problem of the $\mu$-calculus over this logic can be solved in time $2^{\mathcal{O}({nk\log n})}$ as well.

Proof

By the previous Lemma, it suffices to show that $\mathsf{A}^{\alpha_{\mathsf{sat}}}$ can be computed in time $2^{\mathcal{O}({nk\log n})}$. Since we have $2nk<\log{|D_{\chi}|}$, $\mathsf{A}^{\alpha_{\mathsf{sat}}}$ can – by Corollary 2 – be computed in time $\mathcal{O}(t(\alpha_{\mathsf{sat}})\cdot(|D_{\chi}|(2nk+1))^{8})$, where $t(\alpha_{\mathsf{sat}})$ denotes the maximum of $(|D_{\chi}|(2nk+1))^{8}$ and the time it takes to compute $\alpha_{\mathsf{sat}}$; by assumption, $\alpha_{\mathsf{sat}}$ can be computed in time $2^{\mathcal{O}({nk\log n})}$ so that we have $t(\alpha_{\mathsf{sat}})\in 2^{\mathcal{O}({nk\log n})}$. ∎

Example 0.A.4

It has been shown (e.g. in [31]) that the one-step satisfiability problems of all logics from Example 0.A.2 can be solved in time $2^{\mathcal{O}({nk\log n})}$. Hence we obtain an upper bound $2^{\mathcal{O}({nk\log n})}$ for the satisfiability problems of all these logics, in particular including the monotone $\mu$-calculus, the alternating-time $\mu$-calculus, the graded $\mu$-calculus and the (two-valued) probabilistic $\mu$-calculus, even when the latter two are extended with (monotone) polynomial inequalities. This improves on the best previous bounds in all cases.