key: cord-0046634-ib4jf7dw
authors: Hausmann, Daniel; Schröder, Lutz
title: NP Reasoning in the Monotone [Formula: see text]-Calculus
date: 2020-05-30
journal: Automated Reasoning
DOI: 10.1007/978-3-030-51074-9_28
sha: a1aad52e5c74f5e03a4fbe81b48732f03a10ed56
doc_id: 46634
cord_uid: ib4jf7dw

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 [Formula: see text]-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.

Monotone modal logic differs from normal modal logics (such as K [4] , equivalent to the standard description logic 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 μ-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 μ-calculus).

While many modal logics (including K/ALC) have PSpace-complete satisfiability problems in the absence of fixpoints, it is known that satisfiability in monotone modal logic is only 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 PSpace-complete to 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 μ-calculus with the universal modality [8] is only 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 NP-complete (the best

For simplicity, assume that v 0 ∈ V ∃ and that the game is alternating, i.e. E(v) ⊆ V ∀ for all v ∈ V ∃ , and E(v) ⊆ V ∃ for all v ∈ V ∀ (our games will have this shape). A play of G is a sequence τ = v 0 , v 1 , . . . of nodes such that (v i , v i+1 ) ∈ E for all i ≥ 0 and τ is either infinite or ends in a node without outgoing moves. Eloise wins a play τ if and only if τ is finite and ends in an Abelard-node or τ is infinite and Inf(τ )∩F = ∅, that is, τ infinitely often visits an accepting node. A history-free Eloise-strategy is a partial function s : V ∃ V such that s(v 0 ) is defined, and whenever s(v) is defined, then (v, s(v) ) ∈ E and s(v ) is defined for all v ∈ E(s(v)). A play v 0 , v 1 , . . . is an s-play if v i+1 = s(v i ) whenever v i ∈ V ∃ . We say that s is a winning strategy if Eloise wins every s-play, and that Eloise wins G if there is a winning strategy for 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] .

We proceed to recall the syntax and semantics of the monotone μ-calculus.

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

where p ∈ P, a ∈ A, X ∈ V; throughout, we use η ∈ {μ, ν} to denote extremal fixpoints. As usual, μ and ν 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 ψ. We write FV(ψ) for the set of free variables in ψ, and say that ψ is closed if FV(ψ) = ∅. Negation ¬ is not included but can be defined by taking negation normal forms as usual, with ¬p = p. We refer to formulae of the shape [a]φ or a φ as ( a-)modal literals. As indicated in the introduction, the modalities [a], a have been equipped with various readings, recalled in more detail in Example 7.

Given a closed formula ψ, the closure cl(ψ) of ψ is defined to be the least set of formulae that contains ψ and satisfies the following closure properties:

where ψ 1 [ηX.ψ 1 /X] denotes the formula that is obtained from ψ 1 by replacing every free occurrence of X in ψ 1 with ηX.ψ 1 . Note that all formulae in cl(ψ) are closed. We define the size |ψ| of ψ as |ψ| = |cl(ψ)|. A formula ψ is guarded if whenever ηX. φ ∈ cl(ψ), then all free occurrences of X in φ are under the scope of at least one modal operator. We generally restrict to guarded formulae; see however Remark 1. A closed formula ψ is clean if all fixpoint variables in ψ are bound by exactly one fixpoint operator. Then θ(X) denotes the subformula ηX.φ that binds X in ψ, and X is a least (greatest) fixpoint variable if η = μ (η = ν). We define a partial order ≥ μ on the least fixpoint variables in ρ 1 and ρ 0 by X ≥ μ Y iff θ(Y ) is a subformula of θ(X) and θ(Y ) is not in the scope of a greatest fixpoint operator within θ(X) (i.e. there is no greatest fixpoint operator between μX and μY ). The index idx(X) of such a fixpoint variable X is

For a subformula φ of ψ, we write idx(φ) = max{idx(X) | X ∈ FV(φ)}. We denote by θ * (φ 0 ) the closed formula that is obtained from a subformula φ 0 of ψ by repeatedly replacing free variables X with θ(X). Formally, we define

A clean formula is alternation-free if none of its subformulae contains both a free least and a free greatest fixpoint variable. Finally, ψ is irredundant if X ∈ FV(φ) whenever ηX.φ ∈ cl(ψ).

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 μ-calculus is interpreted over neighbourhood models (or epistemic structures [27] ) F = (W, N, I) where N : A×W → 2 (2 W ) assigns to each atomic program a and each state w a set N (a, w) ⊆ 2 W of a-neighbourhoods of w, and I : P → 2 W interprets propositional atoms such that I(p) = W \ I(p) for p ∈ P (by 2, we denote the set {⊥, } of Boolean truth values, and 2 W is the set of maps W → 2, which is in bijection with the powerset P(W )). Given such an F , each formula ψ is assigned an extension ψ σ ⊆ W that additionally depends on a valuation σ : V → 2 W , and is inductively defined by

We omit the dependence on F in the notation [[φ]] σ , and when necessary clarify the underlying neighbourhood model by phrases such as 'in F '. If ψ is closed, then its extension does not depend on the valuation, so we just write ψ . A closed formula ψ is satisfiable if there is a neighbourhood model F such that ψ = ∅ in F ; in this case, we also say that ψ is satisfiable over F . Given a set Ψ of closed formulae, we write Ψ = ψ∈Ψ ψ . An (infinite) path through a neighbourhood model (W, N, I) is a sequence x 0 , x 1 , . . . of states x i ∈ W such that for all i ≥ 0, there are a ∈ A and S ∈ N (a, x i ) such that x i+1 ∈ 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]φ ∧ a ψ is satisfiable over a neighbourhood model F , then φ ∧ ψ is also satisfiable over F .

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

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 a φ simplifies to just requiring that the extension of φ 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 φ, a φ-model is a neighbourhood model F = (W, N, I) in which [[φ]] = W . A formula ψ is φsatisfiable if ψ is satisfiable over some φ-model; in this context, we refer to φ as the global assumption, and to the problem of deciding whether ψ is φ-satisfiable as satisfiability checking under global assumptions.

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

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 ALC), in which (plain) satisfiability checking is PSpacecomplete [15] while satisfiability checking under global assumptions is ExpTimecomplete [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 [∀]φ, [∃]φ hold (see also [11] ). Example 7. 1. In epistemic logic, neighbourhood models have been termed epistemic structures [27] . In this context, the a ∈ 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]φ is 'a knows φ'. 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 φ and knowing ψ does not entail knowing φ ∧ ψ [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 nondeterminism. CPDL indexes modalities over composite programs α, formed using tests ?φ and the standard operations of propositional dynamic logic (PDL) (union ∪, sequential composition ';', and Kleene star (−) * ) and additionally intersection ∩. It forms a sublogic of Parikh's game logic, recalled next, and thus in particular translates into the monotone μ-calculus.

As indicated in the introduction, CPDL satisfiability checking has been shown to be 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 ExpTime-hardness proof, explicitly changed to relations [24, pp. 458-459] ; ExpTime-hardness then immediately follows since PDL becomes a sublogic of CPDL [24, p. 461 ]. Our 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 (−) × , 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 (−) × within (−) * or vice versa [23] .

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

in mutual recursion with a function τ γ that translates the effect of applying γ into the monotone μ-calculus. (Boxes [γ] can be replaced with γ d ). We refrain from repeating the full definition of τ γ by recursion over γ; some key clauses are

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 ∪) 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 ψ need not be guarded as the clauses for * and × 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 μ-calculus.

For later use, we note Lemma 8. The monotone μ-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 μ-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] e (relational modalities). Moreover, we translate a global assumption φ into a formula saying that all reachable states satisfy φ, expressed in the μ-calculus in a standard fashion.

In the relational μ-calculus, we can encode a modality 'in all reachable states', generalizating the 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 μ-calculus: A formula ψ is satisfiable under the global assumption φ iff ψ ∧ φ 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 μ-calculus.

It is not immediately clear what reachability would mean on neighbourhood models. We can however equivalently rephrase the definition of in the relational case to let φ mean 'the present state is contained in a submodel in which every state satisfies φ', where as usual a submodel of a relational model C with state set W is a model C with state set W ⊆ W such that the graph of the inclusion W → W is a bisimulation from C to C. We thus refer to 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 ,

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 ⊆ W and the graph of the inclusion W → W is a monotone bisimulation between F and F . If (x, y) ∈ S for some monotone bisimulation S, then x and y satisfy the same formulae in the monotone μ-calculus [8] . It follows that the submodel modality 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 μ-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

} is a monotone bisimulation, so x 1 and x 2 satisfy the same formulae in the monotone μ-calculus. However, x 2 satisfies p because x 2 is contained in a submodel with set {x 2 , v 2 } of states, while x 1 does not satisfy p.

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 μ-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 ρ 1 and ρ 0 , aiming to check ρ 0satisfiability of ρ 1 ; we also require both ρ 1 and ρ 0 to be alternation-free. We put cl = cl(ρ 1 ) ∪ cl(ρ 0 ) and n = |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.

A formula φ ∈ cl(ψ) is a deferral if there is a subformula χ of ψ such that FV(χ) contains a least fixpoint variable and φ = θ * (χ). We put dfr = {φ ∈ cl | φ is a deferral}.

Since we assume formulas to be alternation-free, no formula νX. φ is a deferral.

is a deferral since X is a least fixpoint variable and occurs free in [b] ∨ a X; the formula [b] on the other hand is not a deferral since it cannot be obtained from a subformula of ψ 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.

We define an alphabet Σ = Σ p ∪ Σ m for traversing the closure, separating propositional and modal traversal, by

The tracking function δ : dfr × Σ → P(dfr) is defined by δ(foc, (χ, b)) = {foc} for foc ∈ dfr and (χ, b) ∈ Σ p with χ = foc, and by

noting that μX. φ 0 ∈ dfr implies φ 0 [θ(X)/X] ∈ dfr. We extend δ to sets Foc ⊆ dfr by putting δ(Foc, l) = foc∈Foc δ(foc, l) for l ∈ Σ. We also extend δ to words in the obvious way; e.g 

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 μ-calculus are in general nondeterministic parity automata [10] , the automata for alternation-free formulae are nondeterministic co-Büchi automata. Indeed, our tracking function δ can be seen as the transition function of a nondeterministic co-Büchi automaton with set dfr of states and alphabet Σ 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 ExpTime satisfiability checking in alternation-free coalgebraic μ-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 δ with a function for propositional transformation of formula sets guided by letters from Σ p , embodied in the function γ defined next.

We define γ :

We extend γ to words over Σ p in the obvious way. 

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 ( a ) reflects Lemma 2, taking into account the global assumption ρ 0 :

(for a ∈ A, p ∈ P); we usually write rule instances with premise Γ and conclusion Θ = Γ 1 , . . . , Γ n (n ≤ 2) inline as (Γ/Θ). Looking back at Sect. 4, we see that letters in Σ designate rule applications, e.g. the letter ( a φ 1 , [a]φ 2 ) ∈ Σ m indicates application of ( a ) to formulae a φ 1 , [a]φ 2 .

Let states denote the set of (formal) states, i.e. sets Γ ⊆ cl such that ⊥ / ∈ Γ , {p, p} ⊆ Γ for all p ∈ P, and such Γ does not contain formulae that contain top-level occurrences of the operators ∧, ∨, or ηX.

A pre-tableau is a directed graph (W, L), consisting of a finite set W of nodes labelled with subsets of cl by a labeling function l : W → P(cl), and of a relation L ⊆ W × W such that for all nodes v ∈ W with label l(v) = Γ ∈ states and all applications (Γ/Γ 1 , . . . , Γ n ) of a tableau rule to Γ , there is an edge (v, w) ∈ L such that l(w) = Γ i for some 1 ≤ i ≤ n. For nodes with label l(v) = Γ / ∈ states, we require that there is exactly one node w ∈ W such that (v, w) ∈ L; then we demand that there is an application (Γ/Γ 1 , . . . , Γ n ) of a non-modal rule to Γ such that l(w) = Γ i for some 1 ≤ i ≤ n. Finite or infinite words over Σ 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 δ. E.g. for a deferral φ 0 ∨ φ 1 , the letter l = (φ 0 ∨ φ 1 , 0) identifies application of (∨) to {φ 0 ∨ φ 1 }, and the choice of the left disjunct;

root v (whose label contains φ 0 ) encoded by a word w is a (finite or infinite) sequence t = φ 0 , φ 1 . . . of formulae such that φ i+1 ∈ δ(φ i , w(i)). A tableau is a finite pre-tableau in which all traces are finite, and a tableau is a tableau for ρ 1 if some node label contains ρ 1 .

Given a tableau (W, L) and a node v ∈ W , let tab(v) (for tableau timeout) denote the least number m such that for all formulae φ in l(v) and all branches of (W, L) that are rooted at v, all traces of φ 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. for φ / ∈ dfr and, for φ ∈ dfr, by

using the lexicographic ordering on (m, φ) as the termination measure; crucially, unfolding least fixpoints reduces the timeout. We extend this definition to sets of formulae by Ψ m = φ∈Ψ φ m for Ψ ⊆ cl.

In finite neighbourhood models, we have that for all ψ ∈ cl there is some timeout m such that

Proof. Let W be the set of states. Since ψ m is defined like ψ in all cases but one, we only need to consider the inductive case where ψ = μX.ψ 0 ∈ cl. We show that for all subformulae φ of ψ 0 , for all timeout vectors m = (m 1 , . . . , m k ) such that m i = |W | for all i such that φ does not contain a free variable with index at least i, we have

where 

using (1) in the second-to-last step. The proof of (1) is by induction on φ; we do only the non-trivial cases. If θ * (φ) / ∈ dfr, then φ is closed (since ψ 0 does not contain a free greatest fixpoint variable and since φ is not in the scope of a greatest fixpoint operator within ψ 0 , that is, no free greatest fixpoint variable is introduced during the induction). Hence we have φ σ(m) = φ and θ * (φ) m = θ * (φ) = φ so that we are

where the inclusion is by the inductive hypothesis. If φ = μY. φ 1 , then

where the first equality is by Kleene's fixpoint theorem and the inclusion is by

by assumption as μY. φ 1 does not contain a free variable with index at least idx(Y ).

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

There is a tableau for ρ 1 if and only if ρ 1 is ρ 0 -satisfiable.

Proof. Let ρ 1 be ρ 0 -satisfiable. Then there is a finite neighbourhood model (W, N, I) such that W ⊆ ρ 0 and W ∩ ρ 1 = ∅ by Lemma 8. We define a tableau over the set

where u(Ψ ) denotes the sum of the numbers of unguarded operators in formulae from Ψ . Let (x, Ψ, w) ∈ V . For Ψ / ∈ states, u(Ψ ) ≤ 3n − |w|, we pick some φ ∈ Ψ , distinguishing cases. If φ = φ 0 ∧φ 1 or φ = ηX. φ 0 , then we put b = 0. If φ = φ 0 ∨φ 1 , then let m be the least timeout such that x ∈ φ m (such m exists by Lemma 18) . Then there is some b ∈ {0, 1} such that x ∈ φ b m and we put b = b . In any case, we put l = (φ, b) and add an edge from (x, Ψ, w) to (x, γ(Ψ, l), (w, l)) to L, having u(γ(Ψ, l)) = u(Ψ ) − 1 and hence u(γ(Ψ, l)) ≤ 3n − |w, l|. Since we are interested in the nodes that can be reached from nodes (x, Ψ, ) with |Ψ | ≤ 3 and since each formula in Ψ contains at most n unguarded operators, we indeed only have to construct nodes (x, Ψ , w) with u(Ψ ) ≤ 3n − |w| before reaching state labeled nodes. For Ψ ∈ states and { a φ 0 , [a]φ 1 } ⊆ Ψ , let m be the least timeout such that x ∈ { a φ 0 , [a]φ 1 } m (again, such m exists by Lemma 18) . Then there is S ∈ N (a, x) such that S ⊆ φ 0 m ∩ ρ 0 and S ∩ φ 1 m = ∅. Pick y ∈ φ 0 m ∩ φ 1 m ∩ ρ 0 and add an edge from (x, Ψ, w) to (y, {φ 0 , φ 1 , ρ 0 }, ) to L, having u({φ 0 , φ 1 , ρ 0 }) ≤ 3n − | |. Define the label l(x, Ψ, w) of nodes (x, Ψ, w) to be just Ψ . Then the structure (V, L) indeed is a tableau for ρ 1 : Since there is z ∈ W ∩ ρ 1 , we have (z, {ρ 1 }, ) ∈ V , that is, ρ 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 τ = φ 0 , φ 1 , . . . be a trace of some formula φ 0 along some branch (encoded by a word w) that is rooted at some node v = (x, Ψ, w ) ∈ V such that φ 0 ∈ Ψ . Let m be the least timeout such that x ∈ φ 0 m (again, such m exists by Lemma 18) . For each i, we have φ i+1 ∈ δ(φ i , w(i)) and there are (x i , Ψ i , w i ) ∈ V and m i such that φ i ∈ Ψ i and x i ∈ φ i mi . We have chosen disjuncts and modal successors in a minimal fashion, that is, in such a way that we always have m i+1 ≤ l m i . Since traces can be infinite only if they contain infinitely many unfolding steps for some least fixpoint, τ 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 m i1 > l m i2 > l . . . 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 ρ 1 labeled by some function l : V → P(cl). We construct a model (W, N, I) over the set 

We now define a game characterizing ρ 0 -satisfiability of ρ 1 . Player Eloise tries to establish the existence of a tableau for ρ 1 using only polynomially many supporting points for her reasoning. To this end, sequences of propositional reasoning steps are contracted into single 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.

We put U = {Ψ ⊆ cl | 1 ≤ |Ψ | ≤ 2} (note |U | ≤ n 2 ) and Q = {Foc ⊆ dfr | |Foc| ≤ 2}. The ρ 0 -satisfiability game for ρ 1 is the Büchi game G = (V, E, v 0 , F ) with set V = V ∃ ∪ V ∀ of nodes (with the union made disjoint by markers omitted in the notation) where

The set E of moves is defined by

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 ∅; Eloise wins plays in which the focus set is finished infinitely often.

It is crucial that while the game has exponentially many Abelardnodes, there are only polynomially many Eloise-nodes. In fact, all Eloise-nodes (Ψ, Foc) have Foc ⊆ Ψ , so the game has at most 4|U | ≤ 4n 2 Eloise-nodes.

Next we prove the correctness of our satisfiability games.

There is a tableau for ρ 1 if and only if Eloise wins G.

Proof. Let s be a winning strategy for Eloise in G with which she wins every node in her winning region win ∃ . For v = (Ψ, Foc) ∈ win ∃ , we let w s(v) denote a fixed propositional word such that s(Ψ, Foc) = (γ(Ψ, w s(v) ), δ(Foc, w s(v) )), that is, a witness word for the move of Eloise that s prescribes at v. We construct a tableau (W, L) over the set

We define the label l(Φ, Foc ) of nodes from (Φ, Foc ) ∈ W to be just Φ. Let (Φ, Foc ) = (γ(Ψ ∪ {ρ 0 }, w ), δ(Foc, w )) ∈ W . If w is a proper prefix of w s(Ψ,Foc) , then we have Φ / ∈ states; let l ∈ Σ p be the letter such that (w , l) is a prefix of w s(Ψ,Foc) and add the pair ((Φ, Foc ), (γ(Φ, l), δ(Foc , l))) to L. If w = w s(Ψ,Foc) , then we have Φ ∈ states. For { a φ, [a] χ} ⊆ Φ, we distinguish cases. If Foc = ∅, then put Foc = {φ, χ} ∩ dfr; otherwise, put Foc = δ (Foc , ( a φ, [a] χ)). Then add the pair ((Φ, Foc ), ({φ, χ, ρ 0 }, Foc )) to L, having ({φ, χ}, Foc ) ∈ win ∃ . It remains to show that all traces in (W, L) are finite. So let τ = φ 0 , φ 1 , . . . be a trace along some branch (encoded by a word w) that is rooted at some node (Φ, Foc ) ∈ W such that φ 0 ∈ Φ. By construction, this branch gives rise to an s-play (Ψ 0 , Foc 0 ), (Γ 0 , Foc 0 ), (Ψ 1 , Foc 1 ), (Γ 1 , Foc 1 ), . . . that starts at (Ψ 0 , Foc 0 ) = (Ψ, Foc). Let i be the least position such that Foc i = ∅ (i exists because s is a winning strategy). Since the φ j are tracked along rule applications, we have φ i ∈ Γ i ; hence φ i+1 ∈ Foc i+1 . Let i be the least position greater than i such that Foc i = ∅ (again, i exists because s is a winning strategy). Between (Ψ i+1 , Foc i+1 ) and (Γ i , Foc i ), all formulae from Foc i+1 (including φ i+1 ) are transformed to a non-deferral by the formula manipulations encoded in w. In particular, the trace τ ends between node(Ψ i , Foc i ) and node(Ψ i , Foc i ), and hence is finite.

For the converse direction, let (W, L) be tableau for ρ 1 , labeled with l : W → P(cl). We extract a strategy s for Eloise in G. A game node (Ψ, Foc) is realized if there is v ∈ W such that Ψ ⊆ l(v); then we say that v realizes the game node. For all realized game nodes (Ψ, Foc), we pick a realizing tableau node v(Ψ, Foc) that is minimal with respect to tab among the tableau nodes that realize (Ψ, Foc). Then we construct a propositional word w = l 0 , l 1 , . . . as follows, starting with Ψ 0 = Ψ ∪ {ρ 0 } and v 0 = v(Ψ, Foc). For i ≥ 0, pick some non-modal letter l i = (φ, b) such that φ ∈ Ψ i , b ∈ {0, 1} and such that l(v i+1 ) = γ(Ψ i , l i ) where v i+1 ∈ W is the node such that (v i , v i+1 ) ∈ 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 , . . . , l m such that m ≤ 3n, since Ψ 0 contains at most three formulae and each formula contains at most n unguarded operators. Put s(Ψ, Foc) = (γ(Ψ ∪ {ρ 0 }, w), δ(Foc, w)), having γ(Ψ ∪ {ρ 0 }, w) = l(v m ). It remains to show that s is a winning strategy. So let τ = (Ψ 0 , Foc 0 ), (Γ 0 , Foc 0 ), (Ψ 1 , Foc 1 ), (Γ 1 , Foc 1 ), . . . be an s-play, where Ψ 0 = {ρ 1 } and Foc 0 = ∅. It suffices to show that for all i such that Foc i = ∅, there is j ≥ i such that Foc j = ∅. So let Foc i = ∅ and let w i be the word that is constructed in the play from (Ψ i , 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 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 (Ψ i , Foc i ). Then we have Foc i+j = ∅, as required.

Every satisfiable formula of size n in the alternation-free monotone μ-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 μ-calculus with the universal modality is in NP (hence NP-complete).

Proof. Guess a winning strategy s for 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.

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 NP (hence NPcomplete).

We have shown that satisfiability checking in the alternation-free fragment of the monotone μ-calculus with the universal modality is only 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 NPcomplete under their original semantics, i.e. with atomic programs interpreted as neighbourhood structures (they become ExpTime-complete when atomic programs are interpreted as relations). We leave as an open problem whether the upper bound NP extends to the full monotone μ-calculus, for which the best known upper bound thus remains ExpTime, by results on the coalgebraic μcalculus [5] , or alternatively by the translation into the relational μ-calculus that we give in the proof of the finite model property (Lemma 8).

The Description Logic Handbook

Modal μ-calculi

On guarded transformation in the modal μ-calculus

Modal Logic

EXPTIME tableaux for the coalgebraic μcalculus

Complexity of reasoning

Completeness for game logic

Monadic second-order logic and bisimulation invariance for coalgebras

Propositional dynamic logic of regular programs

Deciding the unguarded modal μ-calculus

Using the universal modality: gains and questions

A coalgebraic perspective on monotone modal logic

Global caching for the alternation-free coalgebraic μ-calculus

Normal monomodal logics can simulate all others

The computational complexity of provability in systems of modal propositional logic

Focus games for satisfiability and completeness of temporal logic

Infinite games

Alternating finite automata on ω-words

Games for the μ-calculus

The logic of games and its applications

Bisimulation for general non-normal modal logic

Logic for social software

Game logic -an overview

Concurrent dynamic logic

A decidable mu-calculus: preliminary report

A propositional dynamic logic for instantial neighborhood semantics

On the complexity of epistemic reasoning