NP Reasoning in the Monotone $\mu$-Calculus

Abstract

Satisfiability checking for monotone modal logic is known to be (only) NP-complete. We show that this remains true when the logic is extended with alternation-free fixpoint operators as well as the universal modality; the resulting logic – the alternation-free monotone $\mu$-calculus with the universal modality – contains both concurrent propositional dynamic logic (CPDL) and the alternation-free fragment of game logic as fragments. We obtain our result from a characterization of satisfiability by means of Büchi games with polynomially many Eloise nodes.

1 Introduction

Monotone modal logic differs from normal modal logics (such as K [4], equivalent to the standard description logic $\mathcal {ALC}$ [1]) by giving up distribution of conjunction over the box modality, but retaining monotonicity of the modalities. Its semantics is based on (monotone) neighbourhood models instead of Kripke models. Monotone modalities have been variously used as epistemic operators that restrict the combination of knowledge by epistemic agents [27]; as next-step modalities in the evolution of concurrent systems, e.g. in concurrent propositional dynamic logic (CPDL) [24]; and as game modalities in systems where one transition step is determined by moves of two players, e.g. in Parikh’s game logic [7, 12, 20, 23]. The monotonicity condition suffices to enable formation of fixpoints; one thus obtains the monotone $\mu$-calculus [8], which contains both CPDL and game logic as fragments (indeed, the recent proof of completeness of game logic [7] is based on embedding game logic into the monotone $\mu$-calculus).

While many modal logics (including K/$\mathcal {ALC}$) have $\textsc {PSpace}$-complete satisfiability problems in the absence of fixpoints, it is known that satisfiability in monotone modal logic is only $\textsc {NP}$-complete [27] (the lowest possible complexity given that the logic has the full set of Boolean connectives). In the present paper, we show that the low complexity is preserved under two extensions that usually cause the complexity to rise from $\textsc {PSpace}$-complete to $\textsc {ExpTime}$-complete: Adding the universal modality (equivalently global axioms or, in description logic parlance, a general TBox) and alternation-free fixpoints; that is, we show that satisfiability checking in the alternation-free fragment of the monotone $\mu$-calculus with the universal modality [8] is only $\textsc {NP}$-complete. This logic subsumes both CPDL and the alternation-free fragment of game logic [23]. Thus, our results imply that satisfiability checking in these logics is only $\textsc {NP}$-complete (the best previously known upper bound being $\textsc {ExpTime}$ in both cases [20, 23, 24]); for comparison, standard propositional dynamic logic (PDL) and in fact already the extension of K with the universal modality are $\textsc {ExpTime}$-hard. (Our results thus seemingly contradict previous results on $\textsc {ExpTime}$-completeness of CPDL. However, these results rely on embedding standard PDL into CPDL, which requires changing the semantics of CPDL to interpret atomic programs as sequential programs, i.e. as relations rather than neighbourhood systems [24].) Our results are based on a variation of the game-theoretic approach to $\mu$-calculi [19]. Specifically, we reduce satisfiability checking to the computation of winning regions in a satisfiability game that has exponentially many $\mathsf {Abelard}$-nodes but only polynomially many $\mathsf {Eloise}$-nodes, so that history-free winning strategies for $\mathsf {Eloise}$ have polynomial size. From this approach we also derive a polynomial model property.

Organization.   We recall basics on fixpoints and games in Sect. 2, and the syntax and semantics of the monotone $\mu$-calculus in Sect. 3. We discuss a key technical tool, formula tracking, in Sect. 4. We adapt the standard tableaux system to the monotone $\mu$-calculus in Sect. 5. In Sect. 6, we establish our main results using a game characterization of satisfiability.

2 Notation and Preliminaries

We fix basic concepts and notation on fixpoints and games.

Fixpoints.   Let U be a set; we write $\mathcal {P}(U)$ for the powerset of U. Let $f:\mathcal {P}(U)\rightarrow \mathcal {P}(U)$ be a monotone function, i.e. $f(A)\subseteq f(B)$ whenever $A\subseteq B\subseteq U$. By the Knaster-Tarski fixpoint theorem, the greatest (${{\,\mathrm{\mathsf {GFP}}\,}}$) and least (${{\,\mathrm{\mathsf {LFP}}\,}}$) fixpoints of f are given by

$$\begin{aligned} {{\,\mathrm{\mathsf {LFP}}\,}}f =&\textstyle \bigcap \{V\subseteq U\mid f(V)\subseteq V\}&{{\,\mathrm{\mathsf {GFP}}\,}}f =&\textstyle \bigcup \{V\subseteq U\mid V\subseteq f(V)\}, \end{aligned}$$

and are thus also the least prefixpoint ($f(V)\subseteq V$) and greatest postfixpoint ($V\subseteq f(V)$) of f, respectively. For $V\subseteq U$ and $n\in \mathbb {N}$, we define $f^n(V)$ as expected by $f^0(V)=V$ and $f^{n+1}(V)=f(f^n(V))$. If U is finite, then ${{\,\mathrm{\mathsf {LFP}}\,}}f = f^{|U|}(\emptyset )$ and ${{\,\mathrm{\mathsf {GFP}}\,}}f = f^{|U|}(U)$ by Kleene’s fixpoint theorem.

Infinite Words and Games.   We denote the sets of finite and infinite sequences of elements of a set U by $U^*$ and $U^\omega$, respectively. We often view sequences $\tau =u_1,u_2,\ldots$ in $U^*$ (or $U^\omega$) as partial (total) functions $\tau :\mathbb {N}\rightharpoonup U$, writing $\tau (i)=u_i$. We write

$$\begin{aligned} \mathsf {Inf}(\tau )=\{u\in U\mid \forall i\in \mathbb {N}.\, \exists j>i.\, \tau (j)=u\} \end{aligned}$$

for the set of elements of U that occur infinitely often in $\tau$.

A Büchi game $G=(V,E,v_0,F)$ consists of a set V of nodes, partitioned into the sets $V_\exists$ of $\mathsf {Eloise}$-nodes and $V_\forall$ of $\mathsf {Abelard}$-nodes, a set $E\subseteq V\times V$ of moves, an initial node $v_0$, and a set $F\subseteq V$ of accepting nodes. We write $E(v)=\{v'\mid (v,v')\in E\}$. For simplicity, assume that $v_0\in V_\exists$ and that the game is alternating, i.e. $E(v)\subseteq V_{\forall }$ for all $v\in V_\exists$, and $E(v)\subseteq V_{\exists }$ for all $v\in V_\forall$ (our games will have this shape). A play of G is a sequence $\tau =v_0,v_1,\ldots$ of nodes such that $(v_i,v_{i+1})\in E$ for all $i\ge 0$ and $\tau$ is either infinite or ends in a node without outgoing moves. $\mathsf {Eloise}$ wins a play $\tau$ if and only if $\tau$ is finite and ends in an $\mathsf {Abelard}$-node or $\tau$ is infinite and $\mathsf {Inf}(\tau )\cap F\ne \emptyset$, that is, $\tau$ infinitely often visits an accepting node. A history-free $\mathsf {Eloise}$-strategy is a partial function $s:V_\exists \rightharpoonup V$ such that $s(v_0)$ is defined, and whenever s(v) is defined, then $(v,s(v))\in E$ and $s(v')$ is defined for all $v'\in E(s(v))$. A play $v_0,v_1,\dots$ is an s-play if $v_{i+1}=s(v_i)$ whenever $v_i\in V_\exists$. We say that s is a winning strategy if $\mathsf {Eloise}$ wins every s-play, and that $\mathsf {Eloise}$ wins G if there is a winning strategy for $\mathsf {Eloise}$. Büchi games are history-free determined, i.e. in every Büchi game, one of the players has a history-free winning strategy [17].

3 The Monotone $\mu$-Calculus

We proceed to recall the syntax and semantics of the monotone $\mu$-calculus.

Syntax. We fix countably infinite sets $\mathsf {P}$, $\mathsf {A}$ and $\mathsf {V}$ of atoms, atomic programs and (fixpoint) variables, respectively; we assume that $\mathsf {P}$ is closed under duals (i.e. atomic negation), i.e. $p\in \mathsf {P}$ implies $\overline{p}\in \mathsf {P}$, where $\overline{\overline{p}}=p$. Formulae of the monotone $\mu$-calculus (in negation normal form) are then defined by the grammar

$$\begin{aligned} \psi ,\phi := \bot \mid \top \mid p \mid \psi \wedge \phi \mid \psi \vee \phi \mid {\langle a\rangle }\psi \mid {[a]}\psi \mid X \mid \eta X.\psi \end{aligned}$$

where $p\in \mathsf {P}$, $a\in \mathsf {A}$, $X\in \mathsf {V}$; throughout, we use $\eta \in \{\mu ,\nu \}$ to denote extremal fixpoints. As usual, $\mu$ and $\nu$ are understood as taking least and greatest fixpoints, respectively, and bind their variables, giving rise to the standard notion of free variable in a formula $\psi$. We write $\mathsf {FV}(\psi )$ for the set of free variables in $\psi$, and say that $\psi$ is closed if $\mathsf {FV}(\psi )=\emptyset$. Negation $\lnot$ is not included but can be defined by taking negation normal forms as usual, with $\lnot p=\overline{p}$. We refer to formulae of the shape ${[a]}\phi$ or ${\langle a\rangle }\phi$ as (a-)modal literals. As indicated in the introduction, the modalities ${[a]}$, ${\langle a\rangle }$ have been equipped with various readings, recalled in more detail in Example 7.

Given a closed formula $\psi$, the closure $\mathsf {cl}(\psi )$ of $\psi$ is defined to be the least set of formulae that contains $\psi$ and satisfies the following closure properties:

$$\begin{aligned} \text {if }&\psi _1\wedge \psi _2\in \mathsf {cl}(\psi ) \text { or } \psi _1\vee \psi _2\in \mathsf {cl}(\psi ),\text { then } \{\psi _1,\psi _2\}\subseteq \mathsf {cl}(\psi ),\\ \text {if }&{\langle a\rangle }\psi _1\in \mathsf {cl}(\psi ) \text { or } {[a]}\psi _1\in \mathsf {cl}(\psi ), \text { then } \psi _1\in \mathsf {cl}(\psi ),\\ \text {if }&\eta X.\psi _1\in \mathsf {cl}(\psi ), \text { then } \psi _1[\eta X.\psi _1/X]\in \mathsf {cl}(\psi ), \end{aligned}$$

where $\psi _1[\eta X.\psi _1/X]$ denotes the formula that is obtained from $\psi _1$ by replacing every free occurrence of X in $\psi _1$ with $\eta X.\psi _1$. Note that all formulae in $\mathsf {cl}(\psi )$ are closed. We define the size $|\psi |$ of $\psi$ as $|\psi |=|\mathsf {cl}(\psi )|$. A formula $\psi$ is guarded if whenever $\eta X.\,\phi \in \mathsf {cl}(\psi )$, then all free occurrences of X in $\phi$ are under the scope of at least one modal operator. We generally restrict to guarded formulae; see however Remark 1. A closed formula $\psi$ is clean if all fixpoint variables in $\psi$ are bound by exactly one fixpoint operator. Then $\theta (X)$ denotes the subformula $\eta X.\phi$ that binds X in $\psi$, and X is a least (greatest) fixpoint variable if $\eta =\mu$ ($\eta =\nu$). We define a partial order $\ge _\mu$ on the least fixpoint variables in $\rho _1$ and $\rho _0$ by $X\ge _\mu Y$ iff $\theta (Y)$ is a subformula of $\theta (X)$ and $\theta (Y)$ is not in the scope of a greatest fixpoint operator within $\theta (X)$ (i.e. there is no greatest fixpoint operator between $\mu X$ and $\mu Y$). The index $\mathsf {idx}(X)$ of such a fixpoint variable X is

$$\begin{aligned} \mathsf {idx}(X)=|\{Y\in \mathsf {V}\mid Y\ge _\mu X\}|, \end{aligned}$$

For a subformula $\phi$ of $\psi$, we write $\mathsf {idx}(\phi )=\max \{\mathsf {idx}(X)\mid X\in \mathsf {FV}(\phi )\}$. We denote by $\theta ^*(\phi _0)$ the closed formula that is obtained from a subformula $\phi _0$ of $\psi$ by repeatedly replacing free variables X with $\theta (X)$. Formally, we define $\theta ^*(\phi _0)$ as $\phi _{|\mathsf {FV}(\phi _0)|}$, where $\phi _{i+1}$ is defined inductively from $\phi _i$. If $\phi _i$ is closed, then put $\phi _{i+1}=\phi _i$. Otherwise, pick the variable $X_i\in \mathsf {FV}(\phi _i)$ with the greatest index and put $\phi _{i+1}=\phi _i[\theta (X_i)/X_i]$. Then $\mathsf {idx}(\phi _{i+1})<\mathsf {idx}(\phi _i)$, so $\theta ^*(\phi _0)$ really is closed; moreover, one can show that $\theta ^*(\phi _0)\in \mathsf {cl}(\psi )$. A clean formula is alternation-free if none of its subformulae contains both a free least and a free greatest fixpoint variable. Finally, $\psi$ is irredundant if $X\in \mathsf {FV}(\phi )$ whenever $\eta X.\phi \in \mathsf {cl}(\psi )$.

Remark 1

We have defined the size of formulae as the cardinality of their closure, implying a very compact representation [3]. Our upper complexity bounds thus become stronger, i.e. they hold even for this small measure of input size. Moreover, the restriction to guarded formulae is then without loss of generality, since one has a guardedness transformation that transforms formulae into equivalent guarded ones, with only polynomial blowup of the closure [3].

Semantics. The monotone $\mu$-calculus is interpreted over neighbourhood models (or epistemic structures [27]) $F=(W,N,I)$ where $N:\mathsf {A}\times W\rightarrow 2^{(2^W)}$ assigns to each atomic program a and each state w a set $N(a,w)\subseteq 2^W$ of a-neighbourhoods of w, and $I: \mathsf {P}\rightarrow 2^W$ interprets propositional atoms such that $I(p)=W\setminus I(\overline{p})$ for $p\in \mathsf {P}$ (by 2, we denote the set $\{\bot ,\top \}$ of Boolean truth values, and $2^W$ is the set of maps $W\rightarrow 2$, which is in bijection with the powerset $\mathcal {P}(W)$). Given such an F, each formula $\psi$ is assigned an extension $\llbracket \psi \rrbracket _\sigma \subseteq W$ that additionally depends on a valuation $\sigma :V\rightarrow 2^W$, and is inductively defined by

$$\begin{aligned} \llbracket p \rrbracket _\sigma&= I(p)&\llbracket X \rrbracket _\sigma&= \sigma (X)\\ \llbracket \psi \wedge \phi \rrbracket _\sigma&= \llbracket \psi \rrbracket _\sigma \cap \llbracket \phi \rrbracket _\sigma&\llbracket \psi \vee \phi \rrbracket _\sigma&= \llbracket \psi \rrbracket _\sigma \cup \llbracket \phi \rrbracket _\sigma \\ \llbracket {\langle a\rangle }\psi \rrbracket _\sigma&= \{w\in W\mid \exists S\in N(a,w).\,S\subseteq \llbracket \psi \rrbracket _\sigma \}&\llbracket \mu X.\psi \rrbracket _\sigma&={{\,\mathrm{\mathsf {LFP}}\,}}\llbracket \psi \rrbracket ^X_{\sigma }\\ \llbracket {[a]}\psi \rrbracket _\sigma&= \{w\in W\mid \forall S\in N(a,w).\,S\cap \llbracket \psi \rrbracket _\sigma \ne \emptyset \}&\llbracket \nu X.\psi \rrbracket _\sigma&={{\,\mathrm{\mathsf {GFP}}\,}}\llbracket \psi \rrbracket ^X_{\sigma } \end{aligned}$$

where, for $U\subseteq W$ and fixpoint variables $X,Y\in \mathsf {V}$, we put $\llbracket \psi \rrbracket ^X_\sigma (U)=\llbracket \psi \rrbracket _{\sigma [X\mapsto U]}$, $(\sigma [X\mapsto U])(X)= U$ and $(\sigma [X\mapsto U])(Y)= \sigma (Y)$ if $X\ne Y$. We omit the dependence on F in the notation ${[\![\phi ]\!]}_\sigma$, and when necessary clarify the underlying neighbourhood model by phrases such as ‘in F’. If $\psi$ is closed, then its extension does not depend on the valuation, so we just write $\llbracket \psi \rrbracket$. A closed formula $\psi$ is satisfiable if there is a neighbourhood model F such that $\llbracket \psi \rrbracket \ne \emptyset$ in F; in this case, we also say that $\psi$ is satisfiable over F. Given a set $\varPsi$ of closed formulae, we write $\llbracket \varPsi \rrbracket =\bigcap _{\psi \in \varPsi }\llbracket \psi \rrbracket$. An (infinite) path through a neighbourhood model (W, N, I) is a sequence $x_0,x_1,\ldots$ of states $x_i\in W$ such that for all $i\ge 0$, there are $a\in \mathsf {A}$ and $S\in N(a,x_i)$ such that $x_{i+1}\in S$.

The soundness direction of our game characterization will rely on the following immediate property of the semantics, which may be seen as soundness of a modal tableau rule [5].

Lemma 2

 [27, Proposition 3.8]. If ${[a]}\phi \wedge {\langle a\rangle }\psi$ is satisfiable over a neighbourhood model F, then $\phi \wedge \psi$ is also satisfiable over F.

Remark 3

The dual box and diamond operators ${[a]}$ and ${\langle a\rangle }$ are completely symmetric, and indeed the notation is not uniform in the literature. Our use of ${[a]}$ and ${\langle a\rangle }$ is generally in agreement with work on game logic [20] and CPDL [24]; in work on monotone modal logics and the monotone $\mu$-calculus, the roles of box and diamond are often interchanged [8, 26, 27].

Remark 4

The semantics may equivalently be presented in terms of monotone neighbourhood models, where the set of a-neighbourhoods of a state is required to be upwards closed under subset inclusion [8, 12, 20, 23]. In this semantics, the interpretation of ${\langle a\rangle }\phi$ simplifies to just requiring that the extension of $\phi$ is an a-neighbourhood of the current state. We opt for the variant where upwards closure is instead incorporated into the interpretation of the modalities, so as to avoid having to distinguish between monotone neighbourhood models and their representation as upwards closures of (plain) neighbourhood models, e.g. in small model theorems.

We further extend the expressiveness of the logic (see also Remark 9) by adding global assumptions or equivalently the universal modality:

Definition 5

(Global assumptions). Given a closed formula $\phi$, a $\phi$-model is a neighbourhood model $F=(W,N,I)$ in which ${[\![\phi ]\!]}=W$. A formula $\psi$ is $\phi$-satisfiable if $\psi$ is satisfiable over some $\phi$-model; in this context, we refer to $\phi$ as the global assumption, and to the problem of deciding whether $\psi$ is $\phi$-satisfiable as satisfiability checking under global assumptions.

We also define an extension of the monotone $\mu$-calculus, the monotone $\mu$-calculus with the universal modality, by adding two alternatives

$$\begin{aligned} \dots \mid [\forall ]\phi \mid [\exists ]\phi \end{aligned}$$

to the grammar, in both alternatives restricting $\phi$ to be closed. The definition of the semantics over a neighbourhood model (W, N, I) and valuation $\sigma$ is correspondingly extended by ${[\![[\forall ]\phi ]\!]}_\sigma = W$ if ${[\![\phi ]\!]}_\sigma =W$, and ${[\![[\forall ]\phi ]\!]}_\sigma = \emptyset$ otherwise; dually, ${[\![[\exists ]\phi ]\!]}_\sigma = W$ if ${[\![\phi ]\!]}_\sigma \ne \emptyset$, and ${[\![[\exists ]\phi ]\!]}_\sigma = \emptyset$ otherwise. That is, $[\forall ]\phi$ says that $\phi$ holds in all states of the model, and $[\exists ]\phi$ that $\phi$ holds in some state.

Remark 6

In description logic, global assumptions are typically called (general) TBoxes or terminologies [1]. For many next-step modal logics (i.e. modal logics without fixpoint operators), satisfiability checking becomes harder under global assumptions. A typical case is the standard modal logic K (corresponding to the description logic $\mathcal {ALC}$), in which (plain) satisfiability checking is $\textsc {PSpace}$-complete [15] while satisfiability checking under global assumptions is $\textsc {ExpTime}$-complete [6, 9]. Our results show that such an increase in complexity does not happen for monotone modalities.

For purposes of satisfiability checking, the universal modality and global assumptions are mutually reducible in a standard manner, where the non-trivial direction (from the universal modality to global assumptions) is by guessing beforehand which subformulae $[\forall ]\phi$, $[\exists ]\phi$ hold (see also [11]).

Example 7

• 1. In epistemic logic, neighbourhood models have been termed epistemic structures [27]. In this context, the $a\in \mathsf {A}$ are thought of as agents, the a-neighbourhoods of a state w are the facts known to agent a in w, and correspondingly the reading of ${[a]}\phi$ is ‘a knows $\phi$’. The use of (monotone) neighbourhood models and the ensuing failure of normality imply that agents can still weaken facts that they know but are not in general able to combine them, i.e. knowing $\phi$ and knowing $\psi$ does not entail knowing $\phi \wedge \psi$ [27].

• 2. In concurrent propositional dynamic logic (CPDL), a-neighbourhoods of a state are understood as sets of states that can be reached concurrently, while the choice between several a-neighbourhoods of a state models sequential non-determinism. CPDL indexes modalities over composite programs $\alpha$, formed using tests $?\phi$ and the standard operations of propositional dynamic logic (PDL) (union $\cup$, sequential composition ‘; ’, and Kleene star $(-)^*$) and additionally intersection $\cap$. It forms a sublogic of Parikh’s game logic, recalled next, and thus in particular translates into the monotone $\mu$-calculus.

  As indicated in the introduction, CPDL satisfiability checking has been shown to be $\textsc {ExpTime}$-complete [24], seemingly contradicting our results (Corollary 25). Note however that the interpretation of atomic programs in CPDL, originally defined in terms of neighbourhood systems [24, p. 453], is, for purposes of the $\textsc {ExpTime}$-hardness proof, explicitly changed to relations [24, pp. 458–459]; $\textsc {ExpTime}$-hardness then immediately follows since PDL becomes a sublogic of CPDL [24, p. 461]. Our $\textsc {NP}$ bound applies to the original semantics.

• 3. Game logic [20, 23] extends CPDL by a further operator on programs, dualization $(-)^d$, and reinterprets programs as games between two players Angel and Demon; in this view, dualization just corresponds to swapping the roles of the players. In comparison to CPDL, the main effect of dualization is that one obtains an additional demonic iteration operator $(-)^\times$, distinguished from standard iteration $(-)^*$ by letting Demon choose whether or not to continue the iteration. A game logic formula is alternation-free if it does not contain nested occurrences (unless separated by a test) of $(-)^\times$ within $(-)^*$ or vice versa [23].

  Enqvist et al. [7] give a translation of game logic into the monotone $\mu$-calculus that is quite similar to Pratt’s [25] translation of PDL into the standard $\mu$-calculus. The translation $(-)^\sharp$ is defined by commutation with all Boolean connectives and by

  $$\begin{aligned} ({\langle \gamma \rangle }\phi )^\sharp = \tau _\gamma (\phi ^\sharp ), \end{aligned}$$

  in mutual recursion with a function $\tau _\gamma$ that translates the effect of applying ${\langle \gamma \rangle }$ into the monotone $\mu$-calculus. (Boxes ${[\gamma ]}$ can be replaced with ${\langle \gamma ^d\rangle }$). We refrain from repeating the full definition of $\tau _\gamma$ by recursion over $\gamma$; some key clauses are

  $$\begin{aligned} \tau _{\gamma \cap \delta }(\psi )\! =\! \tau _\gamma (\psi )\wedge \tau _\delta (\psi )\quad \tau _{\gamma ^*}(\psi )\! =\! \mu X.\,(\psi \vee \tau _\gamma (X))\quad \tau _{\gamma ^\times }(\psi ) = \nu Y.\,(\psi \wedge \tau _\gamma (Y)) \end{aligned}$$

  where in the last two clauses, X and Y are chosen as fresh variables (for readability, we gloss over a more precise treatment of this point given in [7]). The first clause (and a similar one for $\cup$) appear at first sight to cause exponential blowup but recall that we measure the size of formulae by the cardinality of their closure; in this measure, there is in fact no blowup. The translated formula $\psi ^\sharp$ need not be guarded as the clauses for $^*$ and $^\times$ can introduce unguarded fixpoint variables; as mentioned in Remark 1, we can however apply the guardedness transformation, with only quadratic blowup of the closure [3].

  Under this translation, the alternation-free fragment of game logic ends up in the (guarded) alternation-free fragment of the monotone $\mu$-calculus.

For later use, we note

Lemma 8

The monotone $\mu$-calculus with the universal modality has the finite model property.

Proof (sketch)

We reduce to global assumptions as per Remark 6, and proceed by straightforward adaptation of the translations of monotone modal logic [14] and game logic [23] into the relational $\mu$-calculus, thus inheriting the finite model property [2]. This translation is based on turning neighbourhoods into additional states, connected to their elements via a fresh relation e. Then, e.g., the monotone modality ${[a]}$ (in our notation, cf. Remark 3) is translated into ${[a]}{\langle e\rangle }$ (relational modalities). Moreover, we translate a global assumption $\phi$ into a formula saying that all reachable states satisfy $\phi$, expressed in the $\mu$-calculus in a standard fashion.    $\square$

Remark 9

In the relational $\mu$-calculus, we can encode a modality $\boxtimes$ ‘in all reachable states’, generalizating the $\mathsf {AG}$ operator from CTL. As already indicated in the proof of Lemma 8, this modality allows for a straightforward reduction of satisfiability under global assumptions to plain satisfiablity in the relational $\mu$-calculus: A formula $\psi$ is satisfiable under the global assumption $\phi$ iff $\psi \wedge \boxtimes \phi$ is satisfiable, where ‘if’ is shown by restricting the model to reachable states. To motivate separate consideration of the universal modality, we briefly argue why an analogous reduction does not work in the monotone $\mu$-calculus.

It is not immediately clear what reachability would mean on neighbourhood models. We can however equivalently rephrase the definition of $\boxtimes$ in the relational case to let $\boxtimes \phi$ mean ‘the present state is contained in a submodel in which every state satisfies $\phi$’, where as usual a submodel of a relational model C with state set W is a model $C'$ with state set $W'\subseteq W$ such that the graph of the inclusion $W'\hookrightarrow W$ is a bisimulation from $C'$ to C. We thus refer to $\boxtimes$ as the submodel modality. This notion transfers to neighbourhood models using a standard notion of bisimulation: A monotone bisimulation [21, 22] between neighbourhood models $(W_1,N_1,I_1)$, $(W_2,N_2,I_2)$ is a relation $S\subseteq W_1\times W_2$ such that whenever $(x,y)\in S$, then

• for all $a\in \mathsf {A}$ and $A\in N_1(a,x)$, there is $B\in N_2(a,y)$ such that for all $v\in B$, there is $u\in A$ such that $(u,v)\in S$,

• for all $a\in \mathsf {A}$ and $B\in N_2(a,y)$, there is $A\in N_1(a,x)$ such that for all $u\in A$, there is a $v\in B$ such that $(u,v)\in S$,

• for all $p\in \mathsf {P}$, $x\in I_1(p)$ if and only if $y\in I_2(p)$.

We then define a submodel of a neighbourhood model $F=(W,N,I)$ to be a neigbourhood model $F'=(W',N',I')$ such that $W'\subseteq W$ and the graph of the inclusion $W'\hookrightarrow W$ is a monotone bisimulation between $F'$ and F. If $(x,y)\in S$ for some monotone bisimulation S, then x and y satisfy the same formulae in the monotone $\mu$-calculus [8]. It follows that the submodel modality $\boxtimes$ on neighbourhood models, defined verbatim as in the relational case, allows for the same reduction of satisfiability under global assumptions as the relational submodel modality.

However, the submodel modality fails to be expressible in the monotone $\mu$-calculus, as seen by the following example. Let $F_1=(W_1,N_1,I_1)$, $F_2=(W_2,N_2,I_2)$ be the neighbourhood models given by $W_1=\{x_1,u_1,v_{11},v_{12}\}$, $W_2=\{x_2,u_2,v_2\}$, $N_1(a,x_1)=\{\{u_1,v_{11}\},\{v_{11},v_{12}\}\}$, $N_2(a,x_2)=\{\{v_{2}\}\}$, $N_1(b,y)=N_2(b,z)=\emptyset$ for $(b,y)\ne (a,x_1)$, $(b,z)\ne (a,x_2)$, $I_1(p)=\{x_1,v_{11},v_{12}\}$, $I_2(p)=\{x_2,v_2\}$, and $I_1(q)=I_2(q)=\emptyset$ for $q\ne p$. Then $S=\{(x_1,x_2),(u_1,u_2),(v_{11},v_2),(v_{12},v_2)\}$ is a monotone bisimulation, so $x_1$ and $x_2$ satisfy the same formulae in the monotone $\mu$-calculus. However, $x_2$ satisfies $\boxtimes p$ because $x_2$ is contained in a submodel with set $\{x_2,v_2\}$ of states, while $x_1$ does not satisfy $\boxtimes p$.

4 Formula Tracking

A basic problem in the construction of models in fixpoint logics is to avoid infinite unfolding of least fixpoints, also known as infinite deferral. To this end, we use a tracking function to follow formulae along paths in prospective models. For unrestricted $\mu$-calculi, infinite unfolding of least fixpoints is typically detected by means of a parity condition on tracked formulae. However, since we restrict to alternation-free formulae, we can instead use a Büchi condition to detect (and then reject) such infinite unfoldings by sequential focussing on sets of formulae in the spirit of focus games [16].

We fix closed, clean, irredundant formulae $\rho _1$ and $\rho _0$, aiming to check $\rho _0$-satisfiability of $\rho _1$; we also require both $\rho _1$ and $\rho _0$ to be alternation-free. We put $\mathsf {cl}=\mathsf {cl}(\rho _1)\cup \mathsf {cl}(\rho _0)$ and $n=|\mathsf {cl}|$.

Next we formalize our notion of deferred formulae that originate from least fixpoints; these are the formulae for which infinite unfolding has to be avoided.

Definition 10

(Deferrals). A formula $\phi \in \mathsf {cl}(\psi )$ is a deferral if there is a subformula $\chi$ of $\psi$ such that $\mathsf {FV}(\chi )$ contains a least fixpoint variable and $\phi =\theta ^*(\chi )$. We put $\mathsf {dfr}= \{\phi \in \mathsf {cl}\mid \phi \text { is a deferral}\}$.

Since we assume formulas to be alternation-free, no formula $\nu X.\,\phi$ is a deferral.

Example 11

For $\psi =\mu X.\, {[b]}\top \vee {\langle a\rangle }X$, the formula ${[b]}\top \vee {\langle a\rangle }\psi =({[b]}\top \vee {\langle a\rangle }X)[\psi /X]\in \mathsf {cl}(\psi )$ is a deferral since X is a least fixpoint variable and occurs free in ${[b]}\top \vee {\langle a\rangle }X$; the formula ${[b]}\top$ on the other hand is not a deferral since it cannot be obtained from a subformula of $\psi$ by replacing least fixpoint variables with their binding fixpoint formulae.

We proceed to define a tracking function that nondeterministically tracks deferrals along paths in neighbourhood models.

Definition 12

(Tracking function). We define an alphabet $\varSigma =\varSigma _p\cup \varSigma _m$ for traversing the closure, separating propositional and modal traversal, by

$$\begin{aligned} \varSigma _p&=\{(\phi _0\wedge \phi _1,0),(\phi _0\vee \phi _1,b),(\eta X.\phi _0,0)\mid \\&\qquad \qquad \qquad \qquad \qquad \qquad \qquad \phi _0,\phi _1\in \mathsf {cl},\eta \in \{\mu ,\nu \},X\in \mathsf {V},b\in \{0,1\}\}\\ \varSigma _m&=\{({\langle a\rangle }\phi _0,{[a]}\phi _1)\mid \phi _0,\phi _1\in \mathsf {cl},a\in \mathsf {A}\}. \end{aligned}$$

The tracking function $\delta :\mathsf {dfr}\times \varSigma \rightarrow \mathcal {P}(\mathsf {dfr})$ is defined by $\delta (\mathsf {foc},(\chi ,b))=\{\mathsf {foc}\}$ for $\mathsf {foc}\in \mathsf {dfr}$ and $(\chi ,b)\in \varSigma _p$ with $\chi \ne \mathsf {foc}$, and by

$$\begin{aligned} \delta (\mathsf {foc},(\mathsf {foc},b))&= {\left\{ \begin{array}{ll} \{\phi _0,\phi _1\}\cap \mathsf {dfr}&{} \mathsf {foc}=\phi _0\wedge \phi _1\\ \{\phi _b\}\cap \mathsf {dfr}&{} \mathsf {foc}=\phi _0\vee \phi _1 \\ \{\phi _0[\theta (X)/X]\} &{} \mathsf {foc}=\mu X.\,\phi _0 \end{array}\right. }\\ \delta (\mathsf {foc},({\langle a\rangle }\phi _0,{[a]}\phi _1))&= {\left\{ \begin{array}{ll} \{\phi _0\} &{}\qquad \qquad \, \mathsf {foc}={\langle a\rangle }\phi _0\\ \{\phi _1\} &{}\qquad \qquad \, \mathsf {foc}={[a]}\phi _1, \end{array}\right. } \end{aligned}$$

noting that $\mu X.\,\phi _0\in \mathsf {dfr}$ implies $\phi _0[\theta (X)/X]\in \mathsf {dfr}$. We extend $\delta$ to sets $\mathsf {Foc}\subseteq \mathsf {dfr}$ by putting $\delta (\mathsf {Foc},l)=\bigcup _{\mathsf {foc}\in \mathsf {Foc}} \delta (\mathsf {foc},l)$ for $l\in \varSigma$. We also extend $\delta$ to words in the obvious way; e.g. we have $\delta (\mathsf {foc},w)=[a]\mathsf {foc}$ for

$$\begin{aligned} \mathsf {foc}=\mu X.\,(p\vee (\langle b\rangle p\wedge [a]X)) \quad w=(\mathsf {foc},0),(p\vee (\langle b\rangle p\wedge [a]\mathsf {foc}),1), (\langle b\rangle p\wedge [a]\mathsf {foc},0). \end{aligned}$$

Remark 13

Formula tracking can be modularized in an elegant way by using tracking automata to accept exactly the paths that contain infinite deferral of some least fixpoint formula. While tracking automata for the full $\mu$-calculus are in general nondeterministic parity automata [10], the automata for alternation-free formulae are nondeterministic co-Büchi automata. Indeed, our tracking function $\delta$ can be seen as the transition function of a nondeterministic co-Büchi automaton with set $\mathsf {dfr}$ of states and alphabet $\varSigma$ in which all states are accepting. Since models have to be constructed from paths that do not contain infinite deferral of some least fixpoint formula, the tracking automata have to be complemented in an intermediate step (which is complicated by nondeterminism) when checking satisfiability. In our setting, the complemented automata are deterministic Büchi automata obtained using a variant of the Miyano-Hayashi construction [18] similarly as in our previous work on $\textsc {ExpTime}$ satisfiability checking in alternation-free coalgebraic $\mu$-calculi [13]; for brevity, this determinization procedure remains implicit in our satisfiability games (see Definition 20 below).

To establish our game characterization of satisfiability, we combine the tracking function $\delta$ with a function for propositional transformation of formula sets guided by letters from $\varSigma _p$, embodied in the function $\gamma$ defined next.

Definition 14

(Propositional transformation). We define $\gamma :\mathcal {P}(\mathsf {cl})\times \varSigma _p\rightarrow \mathcal {P}(\mathsf {cl})$ on $\varGamma \subseteq \mathsf {cl}$, $(\chi ,b)\in \varSigma _p$ by $\gamma (\varGamma ,(\chi ,b))=\varGamma$ if $\chi \notin \varGamma$, and

$$\begin{aligned} \gamma (\varGamma ,(\chi ,b))= (\varGamma \setminus {\chi })\cup {\left\{ \begin{array}{ll} \{\phi _b\} &{} \chi =\phi _0\vee \phi _1\\ \{\phi _0,\phi _1\} &{} \chi =\phi _0\wedge \phi _1\\ \{\phi _0[\eta X.\,\phi _0/X]\} &{} \chi =\eta X.\,\phi _0 \end{array}\right. } \end{aligned}$$

if $\chi \in \varGamma$. We extend $\gamma$ to words over $\varSigma _p$ in the obvious way.

Example 15

Take $\phi =\chi \vee \nu X.\,(\psi _1\wedge \psi _2)$ and $w=(\chi \vee \nu X.\,(\psi _1\wedge \psi _2),1),(\nu X.(\psi _1\wedge \psi _2),0),((\psi _1\wedge \psi _2)[\theta (X)/X],1)$. The letter $(\chi \vee \nu X.\,(\psi _1\wedge \psi _2),1)$ picks the right disjunct and $(\nu X.\,(\psi _1\wedge \psi _2),0)$ passes through the fixpoint operator $\nu X$ to reach $\psi _1\wedge \psi _2$; the letter $(\psi _1\wedge \psi _2,1)$ picks both conjuncts. Thus,

$$\begin{aligned} \gamma (\{\phi \},w)=\{\psi _1[\theta (X)/X],\psi _2[\theta (X)/X]\}. \end{aligned}$$

5 Tableaux

As a stepping stone between neighbourhood models and satisfiability games, we now introduce tableaux which are built using a variant of the standard tableau rules [10] (each consisting of one premise and a possibly empty set of conclusions), where the modal rule $({\langle a\rangle })$ reflects Lemma 2, taking into account the global assumption $\rho _0$:

(for $a\in \mathsf {A}$, $p\in \mathsf {P}$); we usually write rule instances with premise $\varGamma$ and conclusion $\varTheta =\varGamma _1,\ldots ,\varGamma _n$ ($n\le 2$) inline as $(\varGamma /\varTheta )$. Looking back at Sect. 4, we see that letters in $\varSigma$ designate rule applications, e.g. the letter $({\langle a\rangle }\phi _1,{[a]}\phi _2)\in \varSigma _m$ indicates application of $({\langle a\rangle })$ to formulae ${\langle a\rangle }\phi _1$, ${[a]}\phi _2$.

Definition 16

(Tableaux). Let $\mathsf {states}$ denote the set of (formal) states, i.e. sets $\varGamma \subseteq \mathsf {cl}$ such that $\bot \notin \varGamma$, $\{p,\overline{p}\}\not \subseteq \varGamma$ for all $p\in \mathsf {P}$, and such $\varGamma$ does not contain formulae that contain top-level occurrences of the operators $\wedge$, $\vee$, or $\eta X$.

A pre-tableau is a directed graph (W, L), consisting of a finite set W of nodes labelled with subsets of $\mathsf {cl}$ by a labeling function $l:W\rightarrow \mathcal {P}(\mathsf {cl})$, and of a relation $L\subseteq W\times W$ such that for all nodes $v\in W$ with label $l(v)=\varGamma \in \mathsf {states}$ and all applications $(\varGamma /\varGamma _1,\ldots ,\varGamma _n)$ of a tableau rule to $\varGamma$, there is an edge $(v,w)\in L$ such that $l(w)=\varGamma _i$ for some $1\le i\le n$. For nodes with label $l(v)=\varGamma \notin \mathsf {states}$, we require that there is exactly one node $w\in W$ such that $(v,w)\in L$; then we demand that there is an application $(\varGamma /\varGamma _1,\ldots ,\varGamma _n)$ of a non-modal rule to $\varGamma$ such that $l(w)=\varGamma _i$ for some $1\le i\le n$. Finite or infinite words over $\varSigma$ then encode sequences of rule applications (and choices of conclusions for disjunctions). That is, given a starting node v, they encode branches with root v, i.e. (finite or infinite) paths through (W, L) that start at v.

Deferrals are tracked along rule applications by means of the function $\delta$. E.g. for a deferral $\phi _0\vee \phi _1$, the letter $l=(\phi _0\vee \phi _1,0)$ identifies application of $(\vee )$ to $\{\phi _0\vee \phi _1\}$, and the choice of the left disjunct; then $\phi _0\vee \phi _1$ is tracked from a node with label $\varGamma \cup \{\phi _0\vee \phi _1\}$ to a successor node with label $\varGamma \cup \{\phi _0\}$ if $\phi _0\in \delta (\phi _0\vee \phi _1,l)$, that is, if $\phi _0$ is a deferral. A trace (of $\phi _0$) along a branch with root v (whose label contains $\phi _0$) encoded by a word w is a (finite or infinite) sequence $t=\phi _0,\phi _1\ldots$ of formulae such that $\phi _{i+1}\in \delta (\phi _i,w(i))$. A tableau is a finite pre-tableau in which all traces are finite, and a tableau is a tableau for $\rho _1$ if some node label contains $\rho _1$.

Given a tableau (W, L) and a node $v\in W$, let $\mathsf {tab}(v)$ (for tableau timeout) denote the least number m such that for all formulae $\phi$ in l(v) and all branches of (W, L) that are rooted at v, all traces of $\phi$ along the branch have length at most m; such an m always exists by the definition of tableaux.

To link models and tableaux, we next define an inductive measure on unfolding of least fixpoint formulae in models.

Definition 17

(Extension under timeouts). Let k be the greatest index of any least fixpoint variable in $\psi$, and let (W, N, I) be a finite neighbourhood model. Then a timeout is a vector $\overline{m}=(m_1,\ldots ,m_k)$ of natural numbers $m_i\le |W|$. For $1\le i\le k$ such that $m_i>0$, we put $\overline{m}@i=(m_1,\ldots ,m_{i-1},m_i-1,|W|,\ldots ,|W|)$. Then $\overline{m}>_l\overline{m}@i$, where $>_l$ denotes lexicographic ordering. For $\phi \in \mathsf {cl}$, we inductively define the extension $\llbracket \phi \rrbracket _{\overline{m}}$ under timeout $\overline{m}$ by $\llbracket \phi \rrbracket _{\overline{m}}=\llbracket \phi \rrbracket$ for $\phi \notin \mathsf {dfr}$ and, for $\phi \in \mathsf {dfr}$, by

$$\begin{aligned} \llbracket \psi _0\wedge \psi _1 \rrbracket _{\overline{m}}&= \llbracket \psi _0 \rrbracket _{\overline{m}}\cap \llbracket \psi _1 \rrbracket _{\overline{m}} \\ \llbracket \psi _0\vee \psi _1 \rrbracket _{\overline{m}}&= \llbracket \psi _0 \rrbracket _{\overline{m}}\cup \llbracket \psi _1 \rrbracket _{\overline{m}}\\ \llbracket {\langle a\rangle }\psi \rrbracket _{\overline{m}}&= \{w\in W\mid \exists S\in N(a,w).\,S\subseteq \llbracket \psi \rrbracket _{\overline{m}}\}\\ \llbracket {[a]}\psi \rrbracket _{\overline{m}}&= \{w\in W\mid \forall S\in N(a,w).\,S\cap \llbracket \psi \rrbracket _{\overline{m}}\ne \emptyset \}\\ \llbracket \mu X.\psi \rrbracket _{\overline{m}}&={\left\{ \begin{array}{ll} \emptyset &{} m_{\mathsf {idx}(X)}=0\\ \llbracket \psi [\mu X.\psi /X] \rrbracket _{\overline{m}@\mathsf {idx}(X)} &{} m_{\mathsf {idx}(X)}>0 \end{array}\right. } \end{aligned}$$

using the lexicographic ordering on $(\overline{m},\phi )$ as the termination measure; crucially, unfolding least fixpoints reduces the timeout. We extend this definition to sets of formulae by $\llbracket \varPsi \rrbracket _{\overline{m}}= \bigcap _{\phi \in \varPsi } \llbracket \phi \rrbracket _{\overline{m}}$ for $\varPsi \subseteq {{\,\mathrm{cl}\,}}$.

Lemma 18

In finite neighbourhood models, we have that for all $\psi \in \mathsf {cl}$ there is some timeout $\overline{m}$ such that

$$\begin{aligned} \llbracket \psi \rrbracket \subseteq \llbracket \psi \rrbracket _{\overline{m}}. \end{aligned}$$

Proof

Let W be the set of states. Since $\llbracket \psi \rrbracket _{\overline{m}}$ is defined like $\llbracket \psi \rrbracket$ in all cases but one, we only need to consider the inductive case where $\psi =\mu X.\psi _0\in \mathsf {cl}$. We show that for all subformulae $\phi$ of $\psi _0$, for all timeout vectors $\overline{m}=(m_1,\ldots ,m_k)$ such that $m_i=|W|$ for all i such that $\phi$ does not contain a free variable with index at least i, we have

$$\begin{aligned} \llbracket \phi \rrbracket _{\sigma (\overline{m})}\subseteq \llbracket \theta ^*(\phi ) \rrbracket _{\overline{m}}, \end{aligned}$$

(1)

where $\sigma (\overline{m})$ maps each $Y\in \mathsf {FV}(\phi )$ to $(\llbracket \phi _1 \rrbracket ^Y_{\sigma (\overline{m})})^{m_{\mathsf {idx}(Y)}}(\emptyset )$ where $\theta (Y)=\mu Y.\,\phi _1$ (this is a recursive definition of $\sigma (\overline{m})$ since the value of $\sigma (\overline{m})$ for Y is overwritten in $(\llbracket \phi _1 \rrbracket ^Y_{\sigma (\overline{m})})^{m_{\mathsf {idx}(Y)}}(\emptyset )$ so that this set depends only on values $m_i$ such that $i<\mathsf {idx}(Y)$). This shows that the claimed property $\llbracket \mu X.\,\psi _0 \rrbracket \subseteq \llbracket \mu X.\,\psi _0 \rrbracket _{\overline{m}}$ holds for $\overline{m}=(|W|,\ldots ,|W|)$: By Kleene’s fixpoint theorem,

$$\begin{aligned} \llbracket \mu X.\psi _0 \rrbracket&=(\llbracket \psi _0 \rrbracket ^X)^{|W|}(\emptyset )=\llbracket \psi _0 \rrbracket _{[X\mapsto (\llbracket \psi _0 \rrbracket ^X)^{|W|-1}(\emptyset )]} = \llbracket \psi _0 \rrbracket _{\sigma (\overline{m}@\mathsf {idx}(X))}\\&\subseteq \llbracket \theta ^*(\psi _0) \rrbracket _{\overline{m}@\mathsf {idx(X)}}= \llbracket \mu X.\psi _0 \rrbracket _{\overline{m}}, \end{aligned}$$

using (1) in the second-to-last step.

The proof of (1) is by induction on $\phi$; we do only the non-trivial cases. If $\theta ^*(\phi )\notin \mathsf {dfr}$, then $\phi$ is closed (since $\psi _0$ does not contain a free greatest fixpoint variable and since $\phi$ is not in the scope of a greatest fixpoint operator within $\psi _0$, that is, no free greatest fixpoint variable is introduced during the induction). Hence we have $\llbracket \phi \rrbracket _{\sigma (\overline{m})}=\llbracket \phi \rrbracket$ and $\llbracket \theta ^*(\phi ) \rrbracket _{\overline{m}}=\llbracket \theta ^*(\phi ) \rrbracket =\llbracket \phi \rrbracket$ so that we are done. If $\phi = Y$, then $\llbracket Y \rrbracket _{\sigma (\overline{m})}=(\llbracket \phi _1 \rrbracket ^Y_{\sigma (\overline{m})})^{m_{\mathsf {idx}(Y)}}(\emptyset )$ where $\theta (Y)=\mu Y.\,\phi _1$. If $m_{\mathsf {idx}(Y)}=0$, then $(\llbracket \phi _1 \rrbracket ^Y_{\sigma (\overline{m})})^{m_{\mathsf {idx}(Y)}}(\emptyset )=\emptyset$ so there is nothing to show. If $m_{\mathsf {idx}(Y)}>0$, then

$$\begin{aligned} (\llbracket \phi _1 \rrbracket ^Y_{\sigma (\overline{m})})^{m_{\mathsf {idx}(Y)}}(\emptyset )&= \llbracket \phi _1 \rrbracket ^Y_{\sigma (\overline{m})}((\llbracket \phi _1 \rrbracket ^Y_{\sigma (\overline{m})})^{m_{\mathsf {idx}(Y)-1}}(\emptyset ))\\&=\llbracket \phi _1 \rrbracket _{({\sigma (\overline{m})})[Y\mapsto (\llbracket \phi _1 \rrbracket ^Y_\sigma )^{m_{\mathsf {idx}(Y)}-1}(\emptyset )]}\\&\subseteq \llbracket \theta ^*(\phi _1) \rrbracket _{\overline{m}@\mathsf {idx}(Y)}\\&= \llbracket \theta ^*(\phi _1[\mu Y.\,\phi _1/Y]) \rrbracket _{\overline{m}@\mathsf {idx}(Y)}\\&= \llbracket \theta ^*(\mu Y.\,\phi _1) \rrbracket _{\overline{m}} =\llbracket \theta ^*(Y) \rrbracket _{\overline{m}}, \end{aligned}$$

where the inclusion is by the inductive hypothesis. If $\phi =\mu Y.\,\phi _1$, then

$$\begin{aligned} \llbracket \mu Y.\,\phi _1 \rrbracket _{\sigma (\overline{m})}=(\llbracket \phi _1 \rrbracket _{\sigma (\overline{m})}^Y)^{|W|}(\emptyset )&=\llbracket \phi _1 \rrbracket ^Y_{\sigma (\overline{m})}((\llbracket \phi _1 \rrbracket ^Y_{\sigma (\overline{m})})^{|W|-1}(\emptyset ))\\&=\llbracket \phi _1 \rrbracket _{({\sigma (\overline{m})})[Y\mapsto (\llbracket \phi _1 \rrbracket ^Y)^{|W|-1}(\emptyset )]}\\&\subseteq \llbracket \theta ^*(\phi _1) \rrbracket _{\overline{m}@\mathsf {idx}(Y)}\\&=\llbracket \theta ^*(\phi _1[\theta (Y)/Y]) \rrbracket _{\overline{m}@\mathsf {idx}(Y)}\\&=\llbracket \theta ^*(\mu Y.\,\phi _1) \rrbracket _{\overline{m}}, \end{aligned}$$

where the first equality is by Kleene’s fixpoint theorem and the inclusion is by the inductive hypothesis since $m_{\mathsf {idx}(Y)}=|W|$ (hence $m@\mathsf {idx}(Y)_{\mathsf {idx}(Y)}=|W|-1$) by assumption as $\mu Y.\,\phi _1$ does not contain a free variable with index at least $\mathsf {idx}(Y)$.   $\square$

To check satisfiability it suffices to decide whether a tableau exists:

Theorem 19

There is a tableau for $\rho _1$ if and only if $\rho _1$ is $\rho _0$-satisfiable.

Proof

Let $\rho _1$ be $\rho _0$-satisfiable. Then there is a finite neighbourhood model (W, N, I) such that $W\subseteq \llbracket \rho _0 \rrbracket$ and $W\cap \llbracket \rho _1 \rrbracket \ne \emptyset$ by Lemma 8. We define a tableau over the set $V=\{(x,\varPsi ,w)\in W\times \mathcal {P}(\mathsf {cl})\times \varSigma _p^*\mid x\in \llbracket \varPsi \rrbracket ,\mathsf {u}(\varPsi )\le 3n-|w|\}$, where $\mathsf {u}(\varPsi )$ denotes the sum of the numbers of unguarded operators in formulae from $\varPsi$. Let $(x,\varPsi ,w)\in V$. For $\varPsi \notin \mathsf {states}$, $\mathsf {u}(\varPsi )\le 3n-|w|$, we pick some $\phi \in \varPsi$, distinguishing cases. If $\phi =\phi _0\wedge \phi _1$ or $\phi =\eta X.\,\phi _0$, then we put $b=0$. If $\phi =\phi _0\vee \phi _1$, then let $\overline{m}$ be the least timeout such that $x\in \llbracket \phi \rrbracket _{\overline{m}}$ (such $\overline{m}$ exists by Lemma 18). Then there is some $b'\in \{0,1\}$ such that $x\in \llbracket \phi _{b'} \rrbracket _{\overline{m}}$ and we put $b=b'$. In any case, we put $l=(\phi ,b)$ and add an edge from $(x,\varPsi ,w)$ to $(x,\gamma (\varPsi ,l),(w,l))$ to L, having $\mathsf {u}(\gamma (\varPsi ,l))=\mathsf {u}(\varPsi )-1$ and hence $\mathsf {u}(\gamma (\varPsi ,l))\le 3n-|w,l|$. Since we are interested in the nodes that can be reached from nodes $(x,\varPsi ,\epsilon )$ with $|\varPsi |\le 3$ and since each formula in $\varPsi$ contains at most n unguarded operators, we indeed only have to construct nodes $(x,\varPsi ',w)$ with $\mathsf {u}(\varPsi )\le 3n-|w|$ before reaching state labeled nodes. For $\varPsi \in \mathsf {states}$ and $\{{\langle a\rangle }\phi _0,{[a]}\phi _1\}\subseteq \varPsi$, let $\overline{m}$ be the least timeout such that $x\in \llbracket \{{\langle a\rangle }\phi _0,{[a]}\phi _1\} \rrbracket _{\overline{m}}$ (again, such $\overline{m}$ exists by Lemma 18). Then there is $S\in N(a,x)$ such that $S\subseteq \llbracket \phi _0 \rrbracket _{\overline{m}}\cap \llbracket \rho _0 \rrbracket$ and $S\cap \llbracket \phi _1 \rrbracket _{\overline{m}}\ne \emptyset$. Pick $y\in \llbracket \phi _0 \rrbracket _{\overline{m}}\cap \llbracket \phi _1 \rrbracket _{\overline{m}}\cap \llbracket \rho _0 \rrbracket$ and add an edge from $(x,\varPsi ,w)$ to $(y,\{\phi _0,\phi _1,\rho _0\},\epsilon )$ to L, having $\mathsf {u}(\{\phi _0,\phi _1,\rho _0\})\le 3n - |\epsilon |$. Define the label $l(x,\varPsi ,w)$ of nodes $(x,\varPsi ,w)$ to be just $\varPsi$. Then the structure (V, L) indeed is a tableau for $\rho _1$: Since there is $z\in W\cap \llbracket \rho _1 \rrbracket$, we have $(z,\{\rho _1\},\epsilon )\in V$, that is, $\rho _1$ is contained in the label of some node in (V, L). The requirements of tableaux for matching rule applications are satisfied by construction of L. It remains to show that each trace in (V, L) is finite. So let $\tau =\phi _0,\phi _1,\ldots$ be a trace of some formula $\phi _0$ along some branch (encoded by a word w) that is rooted at some node $v=(x,\varPsi ,w')\in V$ such that $\phi _0\in \varPsi$. Let $\overline{m}$ be the least timeout such that $x\in \llbracket \phi _0 \rrbracket _{\overline{m}}$ (again, such $\overline{m}$ exists by Lemma 18). For each i, we have $\phi _{i+1}\in \delta (\phi _i,w(i))$ and there are $(x_i,\varPsi _i,w_i)\in V$ and $\overline{m}_i$ such that $\phi _i\in \varPsi _i$ and $x_i\in \llbracket \phi _i \rrbracket _{\overline{m}_i}$. We have chosen disjuncts and modal successors in a minimal fashion, that is, in such a way that we always have $\overline{m}_{i+1}\le _l \overline{m}_{i}$. Since traces can be infinite only if they contain infinitely many unfolding steps for some least fixpoint, $\tau$ is finite or some least fixpoint is unfolded in it infinitely often. In the former case, we are done. In the latter case, each unfolding of a least fixpoint by Definition 17 reduces some digit of the timeout so that we have an infinite decreasing chain $\overline{m}_{i_1}>_l\overline{m}_{i_2}>_l\ldots$ with $i_{j+1}>i_j$ for all j, which is a contradiction to $<_l$ being a well-order.

For the converse direction, let (V, L) be a tableau for $\rho _1$ labeled by some function $l:V\rightarrow \mathcal {P}(\mathsf {cl})$. We construct a model (W, N, I) over the set

$$\begin{aligned} W=\{x\in V \mid l(x)\in \mathsf {states}\}. \end{aligned}$$

For $p\in \mathsf {P}$, put $I(p)=\{x\in W\mid p\in l(x)\}$; since (V, L) is a tableau, the rules $(\bot )$ and do not match the label of any node, so we have $I(p)=W\setminus I(\overline{p})$, as required. Let $x\in W$ and $a\in \mathsf {A}$. If l(x) contains no a-box literal, then we put $N(a,x)=\{\emptyset \}$. If l(x) contains some a-box literal but no a-diamond literal, then we put $N(a,x)=\emptyset$. Otherwise, let the a-modalities in l(x) be exactly ${\langle a\rangle }\chi _1,\ldots ,{\langle a\rangle }\chi _o, {[a]}\psi _1,\ldots ,{[a]}\psi _m$. We put $N(a,x)=\{\{y_{1,1},\ldots ,y_{1,m}\},\ldots ,\{y_{o,1},\ldots ,y_{o,m}\}\}$, where, for $1\le i\le o$, $1\le j\le m$, the state $y_{i,j}$ is picked minimally with respect to $\mathsf {tab}$ among all nodes z such that $(x,z)\in L$ and $\{\chi _i,\psi _j,\rho _0\}= l(z)$; such $y_{i,j}$ with minimal tableau timeout always exists since (V, L) is a tableau. It remains to show that (W, N, I) is a $\rho _0$-model for $\rho _1$. We put

$$\begin{aligned} \widehat{[\![\phi ]\!]}=\{x\in W\mid l(x)\vdash _\mathsf {PL}\phi \} \end{aligned}$$

for $\phi \in \mathsf {cl}$, where $\vdash _{\mathsf {PL}}$ denotes propositional entailment (modal literals ${[a]}\phi$, ${\langle a\rangle }\phi$ are regarded as propositional atoms and $\eta X.\,\phi$ and $\phi [\eta X.\,\phi /X]$ entail each other). Since we have $W\subseteq \widehat{[\![\rho _0]\!]}$ and $W\cap \widehat{[\![\rho _1]\!]}\ne \emptyset$ by definition of (W, N, I) and tableaux, it suffices to show that we have $\widehat{[\![\phi ]\!]}\subseteq \llbracket \phi \rrbracket$ for all $\phi \in \mathsf {cl}$. The proof of this is by induction on $\phi$, using coinduction in the case for greatest fixpoint formulae and a further induction on tableau timeouts in the case for least fixpoint formulae.

   $\square$

6 Satisfiability Games

We now define a game characterizing $\rho _0$-satisfiability of $\rho _1$. Player $\mathsf {Eloise}$ tries to establish the existence of a tableau for $\rho _1$ using only polynomially many supporting points for her reasoning. To this end, sequences of propositional reasoning steps are contracted into single $\mathsf {Eloise}$-moves. Crucially, the limited branching of monotone modalities (and the ensuing limited need for tracking of deferrals) has a restricting effect on the nondeterminism that the game needs to take care of.

Definition 20

(Satisfiability games). We put $U=\{\varPsi \subseteq \mathsf {cl}\mid 1\le |\varPsi |\le 2\}$ (note $|U|\le n^2$) and $Q=\{\mathsf {Foc}\subseteq \mathsf {dfr}\mid |\mathsf {Foc}|\le 2\}$. The $\rho _0$-satisfiability game for $\rho _1$ is the Büchi game $G=(V,E,v_0,F)$ with set $V=V_\exists \cup V_\forall$ of nodes (with the union made disjoint by markers omitted in the notation) where $V_\exists =\{(\varPsi ,\mathsf {Foc})\in U\times Q\mid \mathsf {Foc}\subseteq \varPsi$} and $V_\forall =\mathsf {states}\times Q$, with initial node $v_0=(\{\rho _1\},\emptyset )\in V_\exists$, and with set $F=\{(\varPsi ,\mathsf {Foc})\in V_\exists \mid \mathsf {Foc}=\emptyset \}$ of accepting nodes. The set E of moves is defined by

$$\begin{aligned} E(\varPsi ,\mathsf {Foc})&= \{(\gamma (\varPsi \cup \{\rho _0\},w),\delta (\mathsf {Foc},w))\in \mathsf {states}\times Q\mid w\in (\varSigma _p)^*, |w|\le 3n\}\\ E(\varGamma ,\mathsf {Foc})&= \{\,(\{\phi _0,\phi _1\},\mathsf {Foc}')\in \, U\times Q \mid \, \{{\langle a\rangle }\phi _0,{[a]}\phi _1\}\subseteq \varGamma ,\\&\text {if }\mathsf {Foc}\ne \emptyset \text {, then }\mathsf {Foc}'=\delta (\mathsf {Foc},({\langle a\rangle }\phi _0,{[a]}\phi _1)),\\&\text {if }\mathsf {Foc}=\emptyset \text {, then }\mathsf {Foc}'=\{\phi _0,\phi _1\}\cap \mathsf {dfr}\, \} \end{aligned}$$

for $(\varPsi ,\mathsf {Foc})\in V_\exists$, $(\varGamma ,\mathsf {Foc})\in V_\forall$.

Thus, Eloise steers the propositional evolution of formula sets into formal states, keeping track of the focussed formulae, while Abelard picks an application of Lemma 2, and resets the focus set after it is finished, i.e. becomes $\emptyset$; Eloise wins plays in which the focus set is finished infinitely often.

Remark 21

It is crucial that while the game has exponentially many $\mathsf {Abelard}$-nodes, there are only polynomially many $\mathsf {Eloise}$-nodes. In fact, all $\mathsf {Eloise}$-nodes $(\varPsi ,\mathsf {Foc})$ have $\mathsf {Foc}\subseteq \varPsi$, so the game has at most $4|U|\le 4n^2$ $\mathsf {Eloise}$-nodes.

Next we prove the correctness of our satisfiability games.

Theorem 22

There is a tableau for $\rho _1$ if and only if $\mathsf {Eloise}$ wins G.

Proof

Let s be a winning strategy for $\mathsf {Eloise}$ in G with which she wins every node in her winning region $\mathsf {win}_\exists$. For $v=(\varPsi ,\mathsf {Foc})\in \mathsf {win}_\exists$, we let $w_{s(v)}$ denote a fixed propositional word such that $s(\varPsi ,\mathsf {Foc})=(\gamma (\varPsi ,w_{s(v)}),\delta (\mathsf {Foc},w_{s(v)}))$, that is, a witness word for the move of $\mathsf {Eloise}$ that s prescribes at v. We construct a tableau (W, L) over the set

$$\begin{aligned} W=\{(\gamma (\varPsi \cup \{\rho _0\},w'),\delta (\mathsf {Foc},w'))\in&\,\mathcal {P}(\mathsf {cl})\times \mathcal {P}(\mathsf {dfr})\mid \\&(\varPsi ,\mathsf {Foc})\in \mathsf {win}_\exists , w'\text { is a prefix of } w_{s(\varPsi ,\mathsf {Foc})}\}. \end{aligned}$$

We define the label $l(\varPhi ,\mathsf {Foc}')$ of nodes from $(\varPhi ,\mathsf {Foc}')\in W$ to be just $\varPhi$. Let $(\varPhi ,\mathsf {Foc}')=(\gamma (\varPsi \cup \{\rho _0\},w'),\delta (\mathsf {Foc},w'))\in W$. If $w'$ is a proper prefix of $w_{s(\varPsi ,\mathsf {Foc})}$, then we have $\varPhi \notin \mathsf {states}$; let $l\in \varSigma _p$ be the letter such that $(w',l)$ is a prefix of $w_{s(\varPsi ,\mathsf {Foc})}$ and add the pair $((\varPhi ,\mathsf {Foc}'),(\gamma (\varPhi ,l),\delta (\mathsf {Foc}',l)))$ to L. If $w'=w_{s(\varPsi ,\mathsf {Foc})}$, then we have $\varPhi \in \mathsf {states}$. For $\{{\langle a\rangle }\phi ,{[a]}\chi \}\subseteq \varPhi$, we distinguish cases. If $\mathsf {Foc}'=\emptyset$, then put $\mathsf {Foc}''=\{\phi ,\chi \}\cap \mathsf {dfr}$; otherwise, put $\mathsf {Foc}''=\delta (\mathsf {Foc}',({\langle a\rangle }\phi ,{[a]}\chi ))$. Then add the pair $((\varPhi ,\mathsf {Foc}'),(\{\phi ,\chi ,\rho _0\},\mathsf {Foc}''))$ to L, having $(\{\phi ,\chi \},\mathsf {Foc}'')\in \mathsf {win}_\exists$. It remains to show that all traces in (W, L) are finite. So let $\tau =\phi _0,\phi _1,\ldots$ be a trace along some branch (encoded by a word w) that is rooted at some node $(\varPhi ,\mathsf {Foc}')\in W$ such that $\phi _0\in \varPhi$. By construction, this branch gives rise to an s-play $(\varPsi _0,\mathsf {Foc}_0),(\varGamma _0,\mathsf {Foc}'_0), (\varPsi _1,\mathsf {Foc}_1),(\varGamma _1,\mathsf {Foc}'_1),\ldots$ that starts at $(\varPsi _0,\mathsf {Foc}_0)=(\varPsi ,\mathsf {Foc})$. Let i be the least position such that $\mathsf {Foc}'_i=\emptyset$ (i exists because s is a winning strategy). Since the $\phi _j$ are tracked along rule applications, we have $\phi _i\in \varGamma _i$; hence $\phi _{i+1}\in \mathsf {Foc}_{i+1}$. Let $i'$ be the least position greater than i such that $\mathsf {Foc}'_{i'}=\emptyset$ (again, $i'$ exists because s is a winning strategy). Between $(\varPsi _{i+1},\mathsf {Foc}_{i+1})$ and $(\varGamma _{i'},\mathsf {Foc}'_{i'})$, all formulae from $\mathsf {Foc}_{i+1}$ (including $\phi _{i+1}$) are transformed to a non-deferral by the formula manipulations encoded in w. In particular, the trace $\tau$ ends between $\mathsf {node}(\varPsi _{i},\mathsf {Foc}_{i})$ and $\mathsf {node}(\varPsi _{i'},\mathsf {Foc}_{i'})$, and hence is finite.

For the converse direction, let (W, L) be tableau for $\rho _1$, labeled with $l:W\rightarrow \mathcal {P}(\mathsf {cl})$. We extract a strategy s for $\mathsf {Eloise}$ in G. A game node $(\varPsi ,\mathsf {Foc})$ is realized if there is $v\in W$ such that $\varPsi \subseteq l(v)$; then we say that v realizes the game node. For all realized game nodes $(\varPsi ,\mathsf {Foc})$, we pick a realizing tableau node $v(\varPsi ,\mathsf {Foc})$ that is minimal with respect to $\mathsf {tab}$ among the tableau nodes that realize $(\varPsi ,\mathsf {Foc})$. Then we construct a propositional word $w=l_0,l_1,\ldots$ as follows, starting with $\varPsi _0=\varPsi \cup \{\rho _0\}$ and $v_0=v(\varPsi ,\mathsf {Foc})$. For $i\ge 0$, pick some non-modal letter $l_i=(\phi ,b)$ such that $\phi \in \varPsi _i$, $b\in \{0,1\}$ and such that $l(v_{i+1})=\gamma (\varPsi _i,l_i)$ where $v_{i+1}\in W$ is the node such that $(v_i,v_{i+1})\in L$. Such a letter $l_i$ exists since (W, L) is a tableau. By guardedness of fixpoint variables, this process will eventually terminate with a word $w=l_0,l_1,\ldots ,l_m$ such that $m\le 3n$, since $\varPsi _0$ contains at most three formulae and each formula contains at most n unguarded operators. Put $s(\varPsi ,\mathsf {Foc})=(\gamma (\varPsi \cup \{\rho _0\},w),\delta (\mathsf {Foc},w))$, having $\gamma (\varPsi \cup \{\rho _0\},w)= l(v_m)$. It remains to show that s is a winning strategy. So let $\tau =(\varPsi _0,\mathsf {Foc}_0),(\varGamma _0,\mathsf {Foc}'_0),(\varPsi _1,\mathsf {Foc}_1),(\varGamma _1,\mathsf {Foc}'_1),\ldots$ be an s-play, where $\varPsi _0=\{\rho _1\}$ and $\mathsf {Foc}_0=\emptyset$. It suffices to show that for all i such that $\mathsf {Foc}_i\ne \emptyset$, there is $j\ge i$ such that $\mathsf {Foc}_j=\emptyset$. So let $\mathsf {Foc}_i\ne \emptyset$ and let $w_i$ be the word that is constructed in the play from $(\varPsi _i,\mathsf {Foc}_i)$ on. Since (W, L) is a tableau and since s has been constructed using realizing nodes with minimal tableau timeouts, all traces of formulae from $\mathsf {Foc}_i$ along the branch that is encoded by $w_i$ are finite. Let j be the least number such that all such traces have ended after 2j further moves from $(\varPsi _i,\mathsf {Foc}_i)$. Then we have $\mathsf {Foc}'_{i+j}=\emptyset$, as required.    $\square$

Corollary 23

Every satisfiable formula of size n in the alternation-free monotone $\mu$-calculus with the universal modality has a model of size at most $4n^2$.

Corollary 24

The satisfiability checking problem for the alternation-free monotone $\mu$-calculus with the universal modality is in $\textsc {NP}$ (hence $\textsc {NP}$-complete).

Proof

Guess a winning strategy s for $\mathsf {Eloise}$ in G and verify that s is a winning strategy. Verification can be done in polynomial time since the structure obtained from G by imposing s is of polynomial size and since the admissibility of single moves can be checked in polynomial time.   $\square$

By the translations recalled in Example 7, we obtain moreover

Corollary 25

Satisfiability-checking in concurrent propositional dynamic logic CPDL and in the alternation-free fragment of game logic is in $\textsc {NP}$ (hence $\textsc {NP}$-complete).

7 Conclusion

We have shown that satisfiability checking in the alternation-free fragment of the monotone $\mu$-calculus with the universal modality is only $\textsc {NP}$-complete, even when formula size is measured as the cardinality of the closure. Via straightforward translations (which have only quadratic blow-up under the mentioned measure of formula size), it follows that both concurrent propositional dynamic logic (CPDL) and the alternation-free fragment of game logic are also only $\textsc {NP}$-complete under their original semantics, i.e. with atomic programs interpreted as neighbourhood structures (they become $\textsc {ExpTime}$-complete when atomic programs are interpreted as relations). We leave as an open problem whether the upper bound $\textsc {NP}$ extends to the full monotone $\mu$-calculus, for which the best known upper bound thus remains $\textsc {ExpTime}$ , by results on the coalgebraic $\mu$-calculus [5], or alternatively by the translation into the relational $\mu$-calculus that we give in the proof of the finite model property (Lemma 8).