Friedrich-Alexander-Universität Erlangen-Nürnberg, Erlangen,
Germanymerlin.humml@fau.dehttps://orcid.org/0000-0002-2251-8519Work performed
under the DFG Project _Reconstructing Arguments from Noisy Text (RANT)_ , SCHR
1118/14-1 / SCHR 1118/14-2 Friedrich-Alexander-Universität Erlangen-Nürnberg,
Erlangen, Germanylutz.schroeder@fau.dehttp://orcid.org/0000-0002-3146-5906Work
performed under the DFG Project _RANT_ , SCHR 1118/14-1 / SCHR 1118/14-2 The
Australian National University, Canberra,
Australiadirk.pattinson@anu.edu.auhttps://orcid.org/0000-0002-5832-6666 Merlin
Humml, Lutz Schröder, and Dirk Pattinson [500]Theory of computation Modal and
temporal logics [500]Computing methodologies Multi-agent systems Christel
Baier and Jean Goubault-Larrecq 2 29th EACSL Annual Conference on Computer
Science Logic (CSL 2021) CSL 2021 CSL 2021 January 25–28, 2021 Ljubljana,
Slovenia (Virtual Conference) 183 14

# The Alternating-Time $\mu$-Calculus With Disjunctive Explicit Strategies

Merlin Humml  Lutz Schröder  Dirk Pattinson

###### Abstract

ATL and its extensions, including the AMC, serve the specification of the
strategic abilities of coalitions of agents in concurrent game structures. The
key ingredient of the logic are path quantifiers specifying that some
coalition of agents has a joint strategy to enforce a given goal. This basic
setup has been extended to let some of the agents (revocably) commit to using
certain named strategies, as in _ with explicit strategies (ATLES)_. In the
present work, we extend ATLES with fixpoint operators and strategy
disjunction, arriving at the _ alternating-time $\mu$-calculus with
disjunctive explicit strategies (AMCDES)_, which allows for a more flexible
formulation of temporal properties (e.g. fairness) and, through strategy
disjunction, a form of controlled non-determinism in commitments. Our main
result is an ExpTime upper bound for satisfiability checking (which is thus
ExpTime-complete). We also prove upper bounds QP (quasipolynomial time) and
$\textsc{NP}\cap\textsc{coNP}$ for model checking under fixed interpretations
of explicit strategies, and NP under open interpretation. Our key technical
tool is a treatment of the AMCDES within the generic framework of coalgebraic
logic, which in particular reduces the analysis of most reasoning tasks to the
treatment of a very simple _one-step logic_ featuring only propositional
operators and next-step operators without nesting; we give a new model
construction principle for this one-step logic that relies on a set-valued
variant of first-order resolution.

###### keywords:

Alternating-time logic, multi-agent systems, coalitional strength

###### category:

##  1 Introduction

_ATL_ [1] extends computation tree logic (CTL) with path quantifiers
$\mathop{\langle\\!\langle A\rangle\\!\rangle}$ read ‘coalition $A$ of agents
has a (long-term) joint strategy to enforce’. It is embedded into the _AMC_ ,
which instead of path quantifiers, features nested least and greatest
fixpoints alongside the next-step coalition modalities
$\mathop{\langle\\!\langle A\rangle\\!\rangle}\bigcirc$ (‘$A$ can enforce in
the next step’). The AMC is strictly more expressive than ATL, e.g. supports
fairness constraints.

Coalitional power in ATL and the AMC is measured without any restrictions on
the moves chosen by the opponents. There has been interest in extensions of
ATL where the power of the opponents can be constrained, e.g. by committing
some of them to a particular strategy, allowing for statements such as ‘no
matter what the other network actors do, Alice and Bob can collaborate to
exchange keys via Server $S$ provided that $S$ adheres to the protocol’. One
such extension is provided in _ATLES_ [30], which has path quantifiers
$\mathop{\langle\\!\langle A\rangle\\!\rangle}_{\rho}$ additionally
parametrized over a commitment $\rho$ of some agents to given named
strategies, read ‘provided that the commitments $\rho$ are kept, $A$ can
enforce …’. This extension has substantial impact on expressiveness; e.g.
unlike in basic ATL, the semantics of ATLES over history-free strategies
differs from the one over history-dependent strategies.

Restricting opponents to fixed moves is, of course, quite drastic; as noted
already in the conclusion of Walther [29, Chapter 4], it is desirable to allow
for more permissive restrictions where the opponents can still pick among
several designated moves, as in ‘Alice has a strategy to get her print job
executed if Bob either cancels his large print job or splits it into several
smaller ones’. In the present paper, we introduce such an extension with
disjunctive commitments. Additionally, we include full support for least and
greatest fixpoint operators, with associated gains in expressivity analogous
to the extension from ATL to the AMC. We thus arrive at the _AMCDES_.

Our main result on this logic is that satisfiability checking remains only
ExpTime-complete (i.e. no harder than the AMC, or in fact than basic ATL or
even CTL). We note also that (following a distinction made also in work on
ATLES [30]) model checking is in quasipolynomial time QP and in
$\textsc{NP}\cap\textsc{coNP}$ under fixed interpretation of explicit
strategies (matching the best known bounds for the AMC and in fact even the
plain relational $\mu$-calculus), and in NP under open interpretation; these
results are obtained by fairly straightforward adaptation of results on the
AMC [12], and therefore discussed in full only in the appendix. We obtain our
results by casting the AMCDES as an instance of _coalgebraic logic_ [5], a
unifying framework for modal and temporal logics. The driving principle of
coalgebraic logic is to reduce reasoning tasks to the analysis of a simple
_one-step logic_ , whose formulae employ only Boolean connectives and a single
layer of next-step modalities [23, 4, 12]. In particular, the automata- and
game-theoretic machinery needed for the treatment of fixpoint logics is
entirely encapsulated in results on the coalgebraic $\mu$-calculus [4, 12].
The actual technical work then lies in providing algorithms, axiomatizations,
and model constructions for the one-step logic of AMCDES, still posing
substantial challenges due to nested quantification over strategies. The model
construction principle for the one-step logic that we employ is based on a
set-valued variant of first-order resolution that we introduce here, along
with an associated notion of equationally complete model that we use to move
from (generally infinite) Herbrand universes to finite models; this principle
is the key to supporting strategy disjunction.

The present material revises and extends a previous conference publication
[10].

##### Related Work

Many ATL extensions are concerned with commitments of agents to strategies.
Besides  with explicit strategies (ATLES), this includes, e.g., counterfactual
[27], which differs from ATLES by making commitments irrevocable.  with
actions (ATL-A) [31] has per-agent disjunctive commitments (while the AMCDES
allows disjunctions over joint commitments). ATL-A admits polynomial-time
model checking; satisfiability checking is not considered (it would be
somewhat simpler than in the present setting, as in ATL-A all actions are
named, and hence known in advance).  with explicit actions (ATLEA) [13]
features commitments of agents to a given action at only the current world,
and has a fairly straightforward satisfiability-preserving embedding into the
AMCDES. Various forms of _strategy logic_ [3, 16, 17] possibly contain ATL∗
with disjunctive explicit strategies (but presumably not the AMCDES or even
the AMC, as they lack fixpoint operators); they tend to be computationally
much harder than the AMCDES. Goranko and Ju [7] discuss various forms of
conditional strategic modalities, one of which ($O_{dd}$) is similar in spirit
to our strategy disjunction in that it restricts the moves of the opposition,
however not to given named moves but rather to moves enforcing a given goal;
their main technical result is a Hennessy-Milner style expressiveness theorem.
De Nicola and Vandraager [19] consider disjunction of named actions in
labelled transition systems, which in that setting can be encoded into next-
modalities for single actions using logical disjunction.

##### Organization

We introduce the syntax and the semantics of the alternating-time
$\mu$-calculus with disjunctive explicit strategies (AMCDES) in Section 2.
After recalling the requisite principles of coalgebraic logic in Section 3 we
introduce the method of set-valued first-order resolution in Section 4. We
illustrate these methods on the basic AMC in Section 5, and establish our main
results on satisfiability checking for the AMCDES in Section 6.

##  2 AMC With Disjunctive Explicit Strategies

We proceed to introduce the syntax and semantics of the alternating-time
$\mu$-calculus with disjunctive explicit strategies (AMCDES). As indicated in
Section 1, the logic is inspired by  with explicit strategies (ATLES) [30]. We
deviate from the ATLES syntax in that we express (disjunctive) commitments of
agents by means of names for strategies in the syntax. Also, we shorten the
ATL syntax for next-step operators from $\mathop{\langle\\!\langle
C\rangle\\!\rangle}\bigcirc$ (‘$C$ can enforce in the next step that …’) to
$\mathop{[C]}$ as in coalition logic [21]. We thus arrive at modalities
$\mathop{[C,O]}$ where $O$ is a set of named joint strategies for agents in a
further coalition $D$ of agents restricted in their choice of strategies,
disjoint from $C$, read ‘if the agents in $D$ use one of the joint strategies
in $O$, then $C$ can enforce that …’. The dual modality $\mathop{\langle
C,O\rangle}$ is read ‘even if the agents in $D$ are limited to the joint
strategies in $O$, $C$ cannot prevent that …’. Formally, our syntax is defined
as follows.

######  Definition .

The syntax of the AMCDES is parametrized over a set $\mathsf{At}$ of
(propositional) _atoms_ , $V$ of _variables_ , a finite set $\Sigma$ of agents
(for technical simplicity, assumed to be linearly ordered), and sets $M_{j}$
of _explicit strategies_ (i.e. names for strategies) per agent $j$; _we fix
these data from now on_. A _coalition_ is a subset of $\Sigma$. We also (and
mainly) refer to explicit strategies as _explicit moves_. We write
$M_{D}=\prod_{j\in D}M_{j}$ for the set of _joint explicit moves_ of a
coalition $D$. Formulae $\phi,\psi$ are then given by the grammar

$\phi,\psi::=p\mid\neg p\mid
x\mid\top\mid\bot\mid\phi\land\psi\mid\phi\lor\psi\mid\mathop{[C,O]}\phi\mid\mathop{\langle
C,O\rangle}\phi\mid\mu x.\,\phi\mid\nu x.\,\phi$

where $x\in V$, $p\in\mathsf{At}$, and $C\subseteq\Sigma$, i.e. a _coalition_.
We generally write $\overline{C}=\Sigma\setminus C$. Moreover, $O\subseteq
M_{D}$ is a set of joint explicit moves, called a _disjunctive explicit
strategy_ (or _move_), for some coalition $D$, disjoint from $C$, that we
denote by $\mathit{Ag}(O)$. We call a modality $\mathop{[C,O]}$ or
$\mathop{\langle C,O\rangle}$ a _grand coalition modality_ if
$C\cup\mathit{Ag}(O)=\Sigma$, and _non-disjunctive_ if $|O|=1$, in which case
we often omit set brackets and just write $O$ as its single element. We
restrict grand coalition modalities to be non-disjunctive (cf. Remark 2.6). As
usual, $\mu$ and $\nu$ take least and greatest fixpoints, respectively.
Negation $\neg$ is not included but can be defined in the standard way, taking
negation normal forms. The  with explicit strategies (AMCES) is the fragment
of the AMCDES allowing only non-disjunctive modalities.

The AMCDES thus subsumes both the standard AMC [1] (with $\mathop{[C]}$
corresponding to $\mathop{[C,O]}$ with $\mathit{Ag}(O)=\emptyset$) and the
history-free variant of ATLES [30] (which as we will detail in Remark 2.5 is
the variant to which previous technical results refer).

######  Example 2.1.

The formula indicated in the introduction,

$\mathop{[\mathsf{Alice},(\mathsf{Bob}\colon\\{\mathsf{cancelPrint},\mathsf{splitPrint}\\})]}\mathsf{printed}$

says (using hopefully self-explanatory human-readable syntax for disjunctive
explicit moves) that ‘Alice has a strategy to have her print job executed,
provided that Bob opts to either cancel his print job or to split it into
smaller jobs’. The fixpoint formula

$\nu
x.\,\neg\mathsf{corrupted}\land\mathop{[\mathsf{ECC},(\mathsf{Env}\colon\\{0\mathsf{\text{-}flips},1\mathsf{\text{-}flip}\\})]}x$

expresses that ECC memory can ensure that the stored data is not corrupted
provided that in each cycle the environment flips either one or zero bits. The
formula

$\nu
x.\,\neg\mathsf{intrusion}\land\mathop{\langle\mathsf{Attacker},(\mathsf{IPS}\colon\\{\mathsf{dropPackage},\mathsf{blockIP}\\})\rangle}x$

expresses that ‘No matter what an attacker tries, the intrusion prevention
system can always drop suspicious packets or block his IP address to prevent
illegitimate access to company resources’.

######  Remark 2.2.

One can encode an extension ATLDES of ATL with disjunctive explicit strategies
into the AMCDES, e.g. defining $\mathop{\langle\\!\langle
C,O\rangle\\!\rangle}(G\,\phi)$ ‘$C$ can enforce that $\phi$ always holds,
provided that $\mathit{Ag}(O)$ are committed to play strategies in $O$’ as

$\mathop{\langle\\!\langle C,O\rangle\\!\rangle}(G\,\phi):=\nu
x.\,\phi\land\mathop{[C,O]}x.$

The AMCDES is more expressive than ATLDES in this sense; e.g. for
$C=\\{\mathsf{client}\\}$ and
$O=(\mathsf{server}\colon\\{\mathsf{protocol},\mathsf{recover}\\})$ the
formula $\nu x.\,\mu
y.\,(\mathsf{granted}\,\land\,\mathop{[C,O]}x)\,\lor\mathop{[C,O]}y$ says that
‘$\mathsf{client}$ can enforce that his requests are $\mathsf{granted}$
infinitely often, provided that $\mathsf{server}$ always either keeps to the
$\mathsf{protocol}$ or immediately $\mathsf{recover}$s when failures occur’ (a
specification that may, of course, hold or fail in a given system).

Note that the definition of $\mathop{\langle\\!\langle C,O\rangle\\!\rangle}$
allows $\mathit{Ag}(O)$ to choose their joint move from $O$ anew in each step,
like in the fixpoint formulae of Example 2.1, which in fact belong to the
ATLDES fragment of the AMCDES. To illustrate that this is really the
reasonable choice of a semantics for ATLDES (as opposed to letting $O$ choose
only in the beginning of a play), consider a situation where players $K$
(_Kangaroo_) and $M$ (_Marc-Uwe_) [15] play rock-paper-scissors ($R$, $P$,
$S$) for an indefinite number of rounds, say to determine daily who does the
dishwashing, until someone quits. Let the model include memory for the moves
in the previous round, and atoms $p$ ‘at least two rounds have been played’
and $k$ ‘$K$ won the previous round’. Consider the ATLDES formula

$\mathsf{rigged}=\mathop{\langle\\!\langle
K,(M\colon\\{R,P,S\\})\rangle\\!\rangle}G(p\to k)$

‘$K$ wins all rounds after the first if $M$ keeps playing’. In  with
disjunctive explicit strategies (ATLDES), $\mathsf{rigged}$ does not hold in
the model, as one would expect. If $M$ could make his choice of $R,P,S$ only
once (in reality, sadly, he does just that [14]), then $\mathsf{rigged}$ would
in fact hold.

We proceed to define the semantics, which is based on concurrent game
structures [1] extended with interpretations of explicit moves.

######  Notation 2.3.

For $k\in\mathbb{N}$, we write $[k]=\\{1,\dots,k\\}$. For $C\subseteq\Sigma$
and a tuple ${(k_{j})}_{j\in C}\in\mathbb{N}^{C}$, we put $[k_{C}]=\prod_{j\in
C}[k_{j}]$. Given $m\in[k_{C}]$ and $D\subseteq C$, we write $m|_{D}$ for the
restriction of $m$ to an element of $[k_{D}]$. We write $n\sqsubseteq m$ if
$n=m|_{\mathit{Ag}(n)}$, and $n\mathrel{=_{\sqcap}}m$ if
$n|_{\mathit{Ag}(n)\cap\mathit{Ag}(m)}=m|_{\mathit{Ag}(n)\cap\mathit{Ag}(m)}$.
We write $\mathcal{P}X$ for the powerset of a set $X$.

######  Definition 1.

A _ concurrent game structure with explicit strategies (CGSES)_ is a tuple
$(W,k,v,f,\iota)$ consisting of

  * •

a finite set $W$ of _states_ ,

  * •

for each agent $j$ and each state $w$, a natural number $k_{j}^{w}\geq 1$
determining the set of _moves_ available to agent $j$ at state $w$ to be
$[k_{j}^{w}]$,

  * •

for each state $w\in W$,

    * –

a set $v(w)\subseteq\mathsf{At}$ of propositional atoms true at $w$,

    * –

an _outcome function_ $f^{w}:[k_{\Sigma}^{w}]\to W$, and

    * –

for each agent $j$, a _move interpretation_ $\iota^{w}_{j}\colon
M_{j}\to[k_{j}^{w}]$.

For a joint explicit move $m\in M_{D}$, we just write $\iota^{w}(m)$ for the
joint move with components $\iota^{w}_{j}(m_{j})$ for $j\in D$. We use
function image notation $\iota^{w}[O]$ to denote the result of applying
$\iota^{w}$ to each joint move in the set $O$. The semantics of the AMCDES is
then defined by assigning to each formula $\phi$ an extension
${\llbracket\phi\rrbracket}^{\sigma}_{S}\subseteq Q$, which depends on a CGSES
$S=(W,k,v,f,\iota)$ and a valuation $\sigma:V\to\mathcal{P}W$. The
propositional cases are standard (e.g. ${\llbracket
p\rrbracket}_{S}^{\sigma}=\\{w\in W\mid p\in v(w)\\}$, ${\llbracket
x\rrbracket}_{S}^{\sigma}=\sigma(x)$,
${\llbracket\top\rrbracket}_{S}^{\sigma}=W$, and
${\llbracket\phi\wedge\psi\rrbracket}_{S}^{\sigma}={\llbracket\phi\rrbracket}_{S}^{\sigma}\cap{\llbracket\psi\rrbracket}_{S}^{\sigma}$).
The remaining clauses are

$\displaystyle{\llbracket\mathop{[C,O]}\phi\rrbracket}_{S}^{\sigma}$
$\displaystyle=\\{w\in W\mid\exists m_{C}\in[k_{C}^{w}].\,\forall
m_{\Sigma}\in[k_{\Sigma}^{w}].\,$ $\displaystyle\hskip
70.0001pt(m_{C}\sqsubseteq m_{\Sigma}\land
m_{\Sigma}|_{\mathit{Ag}(O)}\in\iota^{w}[O])\Rightarrow
f^{w}(m_{\Sigma})\in{\llbracket\phi\rrbracket}_{S}^{\sigma}\\}$
$\displaystyle{\llbracket\mathop{\langle
C,O\rangle}\phi\rrbracket}_{S}^{\sigma}$ $\displaystyle=\\{w\in W\mid\forall
m_{C}\in[k_{C}^{w}].\,\exists m_{\Sigma}\in[k_{\Sigma}^{w}].\,$
$\displaystyle\hskip 70.0001ptm_{C}\sqsubseteq m_{\Sigma}\land
m_{\Sigma}|_{\mathit{Ag}(O)}\in\iota^{w}[O]\land
f^{w}(m_{\Sigma})\in{\llbracket\phi\rrbracket}_{S}^{\sigma}\\}$
$\displaystyle{\llbracket\mu x.\,\phi(x)\rrbracket}_{S}^{\sigma}$
$\displaystyle=\textstyle\bigcap\\{B\subseteq
W\mid{\llbracket\phi(x)\rrbracket}_{S}^{\sigma[x\mapsto B]}\subseteq B\\}$
$\displaystyle{\llbracket\nu x.\,\phi(x)\rrbracket}_{S}^{\sigma}$
$\displaystyle=\textstyle\bigcup\\{B\subseteq W\mid
B\subseteq{\llbracket\phi(x)\rrbracket}_{S}^{\sigma[x\mapsto B]}\\}$

where $\sigma[x\mapsto B]$ denotes $\sigma$ updated to return $B$ on input
$x$; and ${\llbracket\mathop{\langle
C,O\rangle}\phi\rrbracket}_{S}^{\sigma}={\llbracket\neg\mathop{[C,O]}\neg\phi\rrbracket}_{S}^{\sigma}$.
That is, $\mu$ and $\nu$ take least and greatest fixpoints according to the
Knaster-Tarski fixpoint theorem. At a state $w$, $\mathop{[C,O]}\phi$ holds if
the agents in $C$ have a joint move such that a state satisfying $\phi$ is
reached no matter what the other agents do, as long as the agents in
$\mathit{Ag}(O)$ play one of the joint moves in $O$. Dually, $\mathop{\langle
C,O\rangle}\phi$ holds at $w$ if whatever the agents in $C$ do, the other
agents have a joint move that leads to an outcome in $\phi$ and in which the
joint move of $\mathit{Ag}(O)$ is in $O$.

######  Remark 2.4.

In the modal operators $\mathop{[C,O]}$, $\mathit{Ag}(O)$ is in opposition to
$C$. One may envision an alternative setup where $\mathit{Ag}(O)$ is instead
made a part of $C$. However, then $\mathop{[C,O]}\phi$ would become equivalent
to $\bigvee_{m\in O}\mathop{[C,\\{m\\}]}\phi$, hence expressible already in
ATLES. We thus opt for our present more expressive version where
$\mathit{Ag}(O)$ and $C$ are disjoint. Note that $\mathop{[C,O]}\phi$ then is
_not_ equivalent to $\bigwedge_{m\in O}\mathop{[C,\\{m\\}]}\phi$: The latter
formula allows $C$ to use different moves against each $m\in O$, while in
$\mathop{[C,O]}\phi$, the _same_ joint move of $C$ must work against every
$m\in O$.

######  Remark 2.5.

The above semantics uses history-free strategies (i.e. ones that look only at
the present state, not the history of previously visited states). While basic
ATL is insensitive to whether it is interpreted over history-free or history-
dependent strategies [1], ATLES does distinguish these semantics [30].
Although this may not be always apparent from the phrasing, all technical
results on ATLES in Walther et al. [30] are meant to apply to the semantics
over history-free strategies only111Personal communication with the authors
(in particular the fixpoint unfolding axioms [30, Figure 1] clearly hold only
over the history-free semantics). Note that the basic AMC, which the AMCDES
extends, similarly is interpreted over history-free strategies (and
nevertheless includes ATL∗, which is history-dependent [1]).

######  Remark 2.6.

The interdiction of proper strategy disjunction in grand coalition modalities
is needed (only) for the upper bound on satisfiability checking (Section 6);
our results on model checking (Section 2) would actually not need this
restriction. The fragment we term AMCES in Section 2 does include grand
coalition modalities with (non-disjunctive) explicit strategies. It is hence
more permissive on these modalities than the original version of ATLES [30],
where the set of agents is made variable, which for purposes of satisfiability
is equivalent to excluding grand coalition modalities.

We note that the axiomatization we present later and its completeness proof
become much simpler if one excludes the grand coalition completely (like,
effectively, in ATLES): E.g. in the rule $(C)$ for basic coalition logic / ATL
(Section 5), the literals $\mathop{\langle\Sigma\rangle}c_{j}$ disappear; and
in the proof of one-step tableau completeness (Theorem 5.1), one can, in this
simplified setting, just use a single move $\bot$ as witness for all
$\mathop{\langle C_{j}\rangle}c_{j}$ in $\Xi$, using non-determinism to ensure
satisfaction of the $\mathop{\langle C_{j}\rangle}c_{j}$. This is discussed in
detail in Appendix B.

#### Model Checking

Walther et al. [30] consider two variants of the model checking problem that
differ on whether the interpretation of explicit strategies is considered part
of the model (_fixed_) or to be found by the model checking algorithm
(_open_). They show for ATLES that if strategies are restricted to be history-
free, then the problem is P-complete under fixed interpretation, and NP-
complete under open interpretation, with the upper bound being by
straightforward guessing of history-free strategies. The complexity for the
history-dependent variant remains open.

We obtain upper bounds for model checking in the AMCDES using generic results
on the coalgebraic $\mu$-calculus [12]:

######  Theorem 2.7.

Model checking for the full AMCDES is in $\textsc{NP}\cap\textsc{coNP}$ as
well as in QP under fixed interpretation of explicit strategies, and in NP
under open interpretation.

We defer a summary of the requisite results in coalgebraic logic and the proof
of Theorem 2.7 to Appendix A, as the details are mostly by simple adaptation
from the AMC [12].

##  3 Preliminaries: Coalgebraic Logic

We will employ the machinery of coalgebraic logic to obtain our main
complexity results; we recall basic definitions and tools, using the standard
AMC as our running example.

Coalgebraic logic [5] is a uniform framework for modal and temporal logics
interpreted over state-based systems. It parametrizes the semantics of logics
over the type of such systems, encapsulated in a _functor_ $F$ on the category
of sets. Such a functor assigns to each set $X$ a set $FX$ and to each map
$f:X\to Y$ a map $Ff:FX\to FY$, preserving identities and composition. We
think of the elements of $FX$ as structured collections over $X$. Systems are
then _$F$ -coalgebras_, i.e. pairs $(W,\gamma)$ consisting of a set $W$ of
_states_ and a _transition map_ $\gamma:W\to FW$, which thus assigns to each
state a structured collection of successors. Our leading example is the
functor $\mathsf{G}$ that maps a set $X$ to the set

$\mathsf{G}X=\\{({(k_{j})}_{j\in\Sigma},f)\mid(k_{j})\in\mathbb{N}_{\geq
1}^{\Sigma},f:\textstyle(\prod_{j\in\Sigma}[k_{j}])\to X\\}$

of _one-step games_ over $X$. $\mathsf{G}$-Coalgebras are essentially
concurrent game structures [1] without the interpretation of propositional
atoms, as they assign to each state numbers $k_{j}$ of available moves for the
agents and an outcome function $f$. Propositional atoms are covered by
extending $\mathsf{G}$ to
$\mathsf{G}_{\mathsf{p}}X=\mathcal{P}\mathsf{At}\times\mathsf{G}X$; although
the logic becomes trivial without propositional atoms, we mostly elide their
explicit treatment, which is straightforward and can be dealt with using
fusion results in coalgebraic logic [24]. To obtain CGSESs, we extend
$\mathsf{G}$ to the functor $\mathsf{G}_{\mathsf{ES}}$ with
$\mathsf{G}_{\mathsf{ES}}X$ consisting of _one-step games with explicit
strategies_ $((k_{j}),f,\iota)$ over $X$, where $((k_{j}),f)$ is a one-step
game over $X$ and $\iota_{j}\colon M_{j}\to[k_{j}]$ (for $j\in\Sigma$)
interprets explicit strategies; we use the same notation for $\iota$ as
introduced for $\iota^{w}$ in Section 2.

The syntax of coalgebraic logics is then parametrized over the choice of a set
$\Lambda$ of (next-step) _modal operators_ with assigned finite arities;
nullary modalities are just propositional atoms. For readability, we assume in
the technical treatment that all modalities are unary. We require that for
every $\mathop{\heartsuit}\in\Lambda$ there is a _dual_ operator
$\overline{\mathop{\heartsuit}}\in\Lambda$. The _coalgebraic $\mu$-calculus_
[4] over $\Lambda$ then has formulae $\phi,\psi$ given by the grammar

$\phi,\psi::=\top\mid\bot\mid
x\mid\phi\land\psi\mid\phi\lor\psi\mid\mathop{\heartsuit}\phi\mid\mu
x.\,\phi\mid\nu x.\,\phi$

where $x$ ranges over a reservoir $V$ of _fixpoint variables_ , and
$\mathop{\heartsuit}$ over $\Lambda$. The operators $\mu$ and $\nu$ take least
and greatest fixpoints, respectively. Again, negation is definable. We assume
a representation of the modalities in $\Lambda$ as strings over some alphabet,
with an ensuing notion of _representation size_ for formulae and modalities.

Over $F$-coalgebras, a modal operator $\mathop{\heartsuit}\in\Lambda$ is
interpreted by assigning to it a _predicate lifting_
${\llbracket\mathop{\heartsuit}\rrbracket}$, which is a family of maps
${\llbracket\mathop{\heartsuit}\rrbracket}_{X}$, indexed over all sets $X$,
that assign to each subset $Y\subseteq X$ a subset
${\llbracket\mathop{\heartsuit}\rrbracket}_{X}(Y)\subseteq FX$, subject to a
naturality condition. To enable fixpoint formation, we require
${\llbracket\mathop{\heartsuit}\rrbracket}_{X}$ to be monotone w.r.t. subset
inclusion. Moreover, we require predicate liftings to respect duals, i.e.
${\llbracket\overline{\mathop{\heartsuit}}\rrbracket}_{X}(Y)=FX\setminus{\llbracket\mathop{\heartsuit}\rrbracket}_{X}(X\setminus
Y)$. Given an $F$-coalgebra $C=(W,\gamma)$ and a valuation
$\sigma:V\to\mathcal{P}W$, the semantic clauses defining the extension
${\llbracket\phi\rrbracket}^{\sigma}_{C}\subseteq W$ of a formula $\phi$ are
then the standard ones for the Boolean connectives; $\mu$ and $\nu$ take least
and greatest fixpoints in the same way as made explicit for the AMCDES in
Section 2; and

${\llbracket\mathop{\heartsuit}\phi\rrbracket}_{C}^{\sigma}=\gamma^{-1}[{\llbracket\mathop{\heartsuit}\rrbracket}_{W}({\llbracket\phi\rrbracket}^{\sigma}_{C})].$

_We fix the data $F$, $\Lambda$, ${\llbracket\mathop{\heartsuit}\rrbracket}$
for the remainder of this section._

######  Example 3.1.

The AMC is cast as a coalgebraic $\mu$-calculus by interpreting the modality
$\mathop{[C]}$ over the functor $\mathsf{G}$ by the predicate lifting

${\llbracket\mathop{[C]}\rrbracket}_{X}(Y)=\\{((k_{j}),f)\in\mathsf{G}X\mid\exists
m_{C}\in[k_{C}].\,\forall m\in[k_{\Sigma}].\,m_{C}\sqsubseteq m\Rightarrow
f(m)\in Y\\}$

(using notation introduced in Section 2). The more general modalities
$\mathop{[C,O]}$ of AMCDES are interpreted by a predicate lifting that
correspondingly lifts a predicate $Y$ on $X$ to the set of all one-step games
with explicit strategies $((k_{j}),f,\iota)\in\mathsf{G}_{\mathsf{ES}}X$ such
that there exists a joint move $m_{C}\in[k_{C}]$ such that $f(m)\in Y$ for all
$m\in[k_{\Sigma}]$ such that $m_{C}\sqsubseteq m$ and $\iota(n)\sqsubseteq m$
for some $n\in O$.

Satisfiability checking in coalgebraic logics can be based on the provision of
a complete set of tableau rules for the next-step modal operators [23, 4]. The
basic example of such a rule is the tableau rule
$\mathop{\Box}a_{1},\dots,\mathop{\Box}a_{n},\mathop{\Diamond}b/a_{1},\dots,a_{n},b$
for standard modal logic, which says essentially that in order to satisfy
$\mathop{\Box}a_{1}\land\dots\land\mathop{\Box}a_{n}\land\mathop{\Diamond}b$,
we need to generate a successor state satisfying $a_{1}\land\dots\land
a_{n}\land b$. Formal definitions are as follows.

######  Definition 2 (One-step tableau rules).

Fix a supply $\mathsf{V}$ of _(propositional) variables_ , serving as
placeholders for formulae in rules. A _(monotone) one-step (tableau) rule_ has
the form

$\frac{\Phi}{\Theta_{1}\mid\dots\mid\Theta_{n}}\qquad(n\geq 0)$

where the _conclusions_ $\Theta_{1},\dots,\Theta_{n}$ are finite subsets of
$\mathsf{V}$, read as finite conjunctions, and the _premiss_ $\Phi$ is a
finite subset of the set
$\Lambda(\mathsf{V})=\\{\mathop{\heartsuit}a\mid\mathop{\heartsuit}\in\Lambda,a\in\mathsf{V}\\}$
of _modal atoms_ , also read conjunctively; additionally, we require that
$\Phi$ mentions each variable at most once, and the $\Theta_{i}$ mention only
variables occurring in $\Phi$. Given a set $X$ and a $\mathcal{P}X$-valuation
$\tau:\mathsf{V}\to\mathcal{P}X$, we interpret such a $\Theta_{i}$ as
${\llbracket\Theta_{i}\rrbracket}\tau=\bigcap_{a\in\Theta_{i}}\tau(a)$, and
$\Phi$ as
${\llbracket\Phi\rrbracket}\tau=\textstyle\bigcap_{\mathop{\heartsuit}a\in\Phi}{\llbracket\mathop{\heartsuit}\rrbracket}_{X}(\tau(a))\subseteq
FX.$

The rule $\Phi/\Theta_{1}\mid\dots\mid\Theta_{n}$ is _one-step tableau sound_
if ${\llbracket\Theta_{i}\rrbracket}\tau\neq\emptyset$ for some $i$ whenever
${\llbracket\Phi\rrbracket}\tau\neq\emptyset$. Let $\mathcal{R}$ be a set of
one-step tableau rules, closed under injective renaming of variables. Then
$\mathcal{R}$ is _one-step tableau complete_ if the following condition holds:
For all $X$, $\tau:\mathsf{V}\to\mathcal{P}X$, and
$\Xi\subseteq\Lambda(\mathsf{V})$, whenever for each rule
$\Phi/\Theta_{1}\mid\dots\mid\Theta_{n}\in\mathcal{R}$ such that
$\Phi\subseteq\Xi$, we have
${\llbracket\Theta_{i}\rrbracket}\tau\neq\emptyset$ for some $i$, then
${\llbracket\Xi\rrbracket}\tau\neq\emptyset$.

We will give one-step tableau sound and complete sets of rules for the AMCDES
in Section 6. To obtain complexity results, rule sets formally need to be
_ExpTime -tractable_, meaning that rule matches are encodable as strings over
some alphabet such that all rule matches to a given set of formulae can be
represented by polynomially sized codes and moreover basic operations on codes
(well-formedness check, check for rule matching, access to conclusions) can be
performed in exponential time [23, 4]; we refrain from elaborating details, as
all rule sets we consider here will be clearly computationally harmless. The
main benefit that we draw from these rule sets is the following generic upper
complexity bound.

######  Theorem 3.2 (Satisfiability checking [4]).

If a coalgebraic $\mu$-calculus admits an ExpTime-tractable one-step tableau
complete set of one-step tableau sound rules, then its satisfiability problem
is in ExpTime.

In the algorithm underlying the above theorem, one-step rules combine with
standard tableau rules for propositional and fixpoint operators. The arising
tableaux need to be checked for bad branches (where least fixpoints are
unfolded indefinitely) using dedicated parity automata, which combine with the
tableau to form the _tableau game_ , a parity game that is won by
$\mathsf{Eloise}$ iff the target formula is satisfiable.

##  4 Set-Valued First-Order Resolution

For use in completeness proofs of modal rules, we next introduce _set-valued
first-order resolution_ , an adaptation of the standard first-order resolution
method [6] to a logic of _outcome models_
$\mathcal{G}=((S_{j})_{j\in\Sigma},f,W,{\llbracket-\rrbracket})$ where the
$S_{j}$ are sets and $W$ is a finite set, ${\llbracket-\rrbracket}$ interprets
sorted algebraic operations over the $S_{j}$, and
$f:\big{(}\prod_{j\in\Sigma}S_{j}\big{)}\to W$ is an outcome function. One-
step games in $\mathsf{G}W$ are (operation-free reducts of) outcome models
where the $S_{j}$ are finite; for the time being, we allow infinite $S_{j}$
for readability, explaining in the proof sketches in Sections 5 and 6 how
finiteness can be regained. Formulae of _set-valued first-order logic_ are
clause sets formed over literals of the form $A(\bar{t})$ where $A\subseteq W$
and $\bar{t}$ is an $\Sigma$-tuple of terms (i.e. a clause is a finite set of
literals, read disjunctively, and a clause set is a finite set of clauses,
read conjunctively). Terms live in a sorted setting with one sort $j$
(interpreted as $S_{j}$) for each agent $j$, and the $j$-th term in $\bar{t}$
has sort $j$. Terms are built from sorted variables and function symbols with
given sort profiles (e.g. $g:1\times 0\to 2$ takes moves of agents $1$ and
$0$, and produces a move of agent $2$) in the standard way, ensuring well-
sortedness. Function symbols are interpreted as sorted functions on the
$S_{j}$, respecting the sort profile; this induces an interpretation of
(tuples of) terms depending on sort-respecting valuations of the variables as
usual. We write ${\llbracket\bar{t}\rrbracket}\eta$ for the interpretation of
a tuple $\bar{t}$ of terms under a valuation $\eta$. An outcome model
$\mathcal{G}$ as above _satisfies_ a literal $A(\bar{t})$ under a valuation
$\eta$ (notation: $\mathcal{G},\eta\models A(\bar{t})$) if
$f({\llbracket\bar{t}\rrbracket}\eta)\in A$, and $\mathcal{G}$ satisfies a
clause $\Gamma$ under $\eta$ (notation: $\mathcal{G},\eta\models\Gamma$) if
$\mathcal{G},\eta\models A(\bar{t})$ for some literal $A(\bar{t})$ in
$\Gamma$. Finally, $\mathcal{G}$ _satisfies_ a clause $\Gamma$ (notation:
$\mathcal{G}\models\Gamma$) if $\mathcal{G},\eta\models\Gamma$ for every
valuation $\eta$. A clause set is satisfiable if there exists an outcome model
that satisfies all its clauses. We will generate clauses from modal atoms in
$\Lambda(\mathsf{V})$ (2); e.g. given a $\mathcal{P}W$-valuation
$\tau:\mathsf{V}\to\mathcal{P}W$, modalized atoms $\mathop{[C]}a$ and
$\mathop{\langle C\rangle}a$ induce singleton clauses of the form

$\displaystyle\\{\tau(a)(e_{C},x_{\,\overline{C}})\\}$ (for $\mathop{[C]}a$)
(1) $\displaystyle\\{\tau(a)(x_{C},g_{\,\overline{C}}(x_{C}))\\}$ (for
$\mathop{\langle C\rangle}a$) (2)

respectively, where $x_{C}$, $x_{\,\overline{C}}$ are tuples of variables
(implicitly universally quantified, and representing moves for the agents in
$C$ and $\overline{C}$, respectively); $e_{C}$ is a family of Skolem constants
witnessing the ability of $C$ to force $a$; and $g_{\,\overline{C}}$ is a
family of Skolem functions producing countermoves $g_{\,\overline{C}}(x_{C})$
for the agents in $\overline{C}$ that keep $C$ from enforcing $\neg a$ using
$x_{C}$. Of course these symbols are fresh so that clauses induced by
different modalized atoms have disjoint sets of function symbols and
variables, which we will later distinguish via superscripts in proofs.

We implicitly normalize clauses to mention each tuple of terms at most once
(rewriting $A(\bar{t}),B(\bar{t})$ into $(A\cup B)(\bar{t})$), and operate on
clauses using the _(set-valued) resolution rule_

$(SR)\;\frac{\Gamma,A_{1}(\bar{t}_{1}),\dots,A_{n}(\bar{t}_{n})\qquad
B(\bar{u}),\Delta}{\Gamma\sigma,((\bigcup_{i=1}^{n}A_{i})\cap
B)(\bar{u}\sigma),\Delta\sigma}\;(n\geq 1)$

where $\sigma$ is the most general unifier (mgu) of
$\bar{t}_{1},\dots,\bar{t}_{n}$, and $\bar{u}$, with variables in the premises
made disjoint by suitable renaming; as usual, we write ‘,’ for union of
clauses and omit set brackets around singleton clauses (so $\Gamma,A(\bar{t})$
is shorthand for $\Gamma\cup\\{A(\bar{t})\\}$). We will also need to consider
a liberalized variant $(\mathit{lSR})$ of $(\mathit{SR})$ where we only
require $\sigma$ to be a unifier (rather than the mgu). Note that the above
formulation of $(SR)$ includes _one-sided implicit factoring_ , i.e. several
literals in the left-hand clause may be resolved against one literal in the
right-hand clause. A clause is _blatantly inconsistent_ if all its literals
are of the form $\emptyset(\bar{t})$. A clause set $\phi$ is _blatantly
inconsistent_ if it contains a blatantly inconsistent clause, and
_inconsistent_ if a blatantly inconsistent clause can be derived from it using
the resolution rule; otherwise, $\phi$ is _consistent_. We note that the
liberalized rule $(\mathit{lSR})$ is admissible; that is, calling a clause set
_$(lSR)$ -consistent_ if no blatantly inconsistent clause can be derived from
it using $(\mathit{lSR})$, we have

######  Lemma 4.1.

Consistent clause sets are also $(\mathit{lSR})$-consistent.

######  Proof 4.2.

By straightforward induction on derivations under $(\mathit{lSR})$, one shows
that every clause derivable from a clause set $\phi$ under $(\mathit{lSR})$ is
a substitution instance of a clause derivable from $\phi$ under
$(\mathit{SR})$. The claim follows immediately by the observation that a
clause that has a blatantly inconsistent substitution instance must itself be
blatantly inconsistent.

Recall that unification can fail either due to a _clash_ , i.e. when terms
with distinct head symbols need to be unified, or at the _occurs check_ ,
which happens when a variable needs to be unified with a term that contains
it. In particular, this happens in clauses (2) associated with diamonds: E.g.
the modal atoms $\mathop{\langle\\{0\\}\rangle}a$ and
$\mathop{\langle\\{1\\}\rangle}b$ generate clauses
$\\{\tau(a)(x_{0},g^{1}_{1}(x_{0}))\\}$ and
$\\{\tau(b)(g^{2}_{0}(x_{1}),x_{1})\\}$, whose (tuples of) argument terms fail
to unify since no substitution solves $x_{0}=g_{0}^{2}(g_{1}^{1}(x_{0}))$.

We note that from one-sided implicit factoring as incorporated in $(SR)$, we
can derive two-sided implicit factoring:

######  Lemma 4.3.

From $(lSR)$, the rule

$(\mathit{SR}^{+})\;\frac{\Gamma,A_{1}(\bar{t}_{1}),\dots,A_{n}(\bar{t}_{n})\qquad
B_{1}(\bar{u}_{1}),\dots,B_{m}(\bar{u}_{m}),\Delta}{\Gamma\sigma,((\bigcup_{i=1}^{n}A_{i})\cap(\bigcup_{i=1}^{m}B_{i}))(\bar{u}_{1}\sigma),\Delta\sigma}\;(n,m\geq
1)$

is derivable where $\sigma$ is the mgu of
$\bar{t}_{1},\dots,\bar{t}_{n},\bar{u}_{1}.\dots,\bar{u}_{m}$, with variables
in the premises made disjoint by suitable renaming.

######  Proof 4.4.

Using $(\mathit{lSR})$, we derive from the premises the clause
$\Gamma\sigma,((\bigcup_{i=1}^{n}A_{i})\cap
B_{1})(\bar{u}_{1}\sigma),B_{2}(\bar{u}_{2}),\dots,B_{m}(\bar{u}_{m}\sigma),\Delta\sigma$.
Further resolving this clause with the left premise according to
$(\mathit{lSR})$, we obtain the clause
$\Gamma\sigma,((\bigcup_{i=1}^{n}A_{i})\cap
B_{1})(\bar{u}_{1}\sigma),((\bigcup_{i=1}^{n}A_{i})\cap
B_{2})(\bar{u}_{2}\sigma),\dots,B_{m}(\bar{u}_{m}\sigma),\Delta\sigma$. Since
$\bar{u}_{1}\sigma=\bar{u}_{2}\sigma$, this clause is identified with
$\Gamma\sigma,((\bigcup_{i=1}^{n}A_{i})\cap(B_{1}\cup
B_{2}))(\bar{u}_{1}\sigma),\dots,B_{m}(\bar{u}_{m}\sigma),\Delta\sigma$ (note
that $((\bigcup_{i=1}^{n}A_{i})\cap B_{1})\cup((\bigcup_{i=1}^{n}A_{i})\cap
B_{2})=(\bigcup_{i=1}^{n}A_{i})\cap(B_{1}\cup B_{2})$). Continuing in this
manner, we obtain the conclusion of $(\mathit{SR}^{+})$.

_Set-valued propositional resolution_ in _set-valued propositional logic_
simplifies the above setup by replacing tuples $\bar{t}$ of terms in literals
$A(\bar{t})$ with elements $y$ of some index set $Y$; models are then just
functions $f\colon Y\to W$, and $f$ _satisfies_ a literal $A(y)$ if $f(y)\in
A$. The resolution rule is just like the above but of course does not involve
unification, substitution, and implicit factoring, i.e. it just derives
$\Gamma,(A\cap B)(y),\Delta$ from $\Gamma,A(y)$ and $B(y),\Delta$.

######  Theorem 4.5 (Soundness and completeness of set-valued resolution).

A clause set in set-valued propositional (first-order) logic is satisfiable
iff it is consistent under set-valued propositional (first-order) resolution.

######  Proof 4.6 (Proof sketch).

Soundness (‘only if’) is clear (see Appendix B). Completeness (‘if’) of the
propositional variant depends on $W$ being finite. It proceeds via maximally
consistent clause sets (MCS) and a Hintikka lemma stating in particular that
an MCS containing $(A\cup B)(y)$ must also contain one of $A(y),B(y)$.
Completeness of the first-order variant is by adaptation of the completeness
proof for standard first-order resolution, going via Herbrand models (i.e.
models having the set of ground terms as the carrier set) and reduction to
completeness of set-valued propositional resolution.

Of course, the Herbrand models constructed in the proof of Theorem 4.5 are in
general infinite. For purposes of constructing finite models, we identify a
property of ‘sufficient completeness’ of a model for a set of terms.

######  Definition 3.

A set $\mathcal{T}$ of (tuples of) terms is _closed under unification_ if
whenever $t,s\in\mathcal{T}$ are unifiable and $\sigma$ is an mgu of $t,s$,
then $u\sigma\in\mathcal{T}$ for every $u\in\mathcal{T}$.

######  Remark 4.7.

If $\mathcal{T}$ is closed under unification, then $\mathcal{T}$ is in
particular closed under injective renaming of variables: For
$u\in\mathcal{T}$, every injective renaming $\sigma$ is an mgu of $u,u$, so
that $u\sigma\in\mathcal{T}$.

We will treat tuples of terms like terms in the following, in particular
mentioning equations between tuples of terms and unifiers of such equations;
this is to be understood as referring to componentwise equality.

######  Definition 4.

A _solution_ of an equation $t=s$ in an outcome model $\mathcal{G}$ is a
valuation $\eta$ such that
${\llbracket\bar{t}\rrbracket}\eta={\llbracket\bar{s}\rrbracket}\eta$ in
$\mathcal{G}$. Let $\mathcal{T}$ be a set of tuples of terms. We say that
$\mathcal{G}$ is _$\mathcal{T}$ -equationally complete_ if whenever an
equation $\bar{t}=\bar{s}$ with $\bar{t},\bar{s}\in\mathcal{T}$ has a solution
in $\mathcal{G}$, then $\bar{t},\bar{s}$ are unifiable, and the mgu $\sigma$
of $\bar{t},\bar{s}$ is a _most general solution_ of $\bar{t}=\bar{s}$ in
$\mathcal{G}$, i.e. every solution $\eta$ of $\bar{t}=\bar{s}$ in
$\mathcal{G}$ has the form
$\eta(x)={\llbracket\sigma(x)\rrbracket}\eta^{\prime}$ for some valuation
$\eta^{\prime}$; we then say briefly that $\eta$ _factorizes through_
$\sigma$.

######  Theorem 4.8.

Let $\mathcal{T}$ be a set of tuples of terms that is closed under
unification, and let $\mathcal{G}$ be $\mathcal{T}$-equationally complete. Let
$\phi$ be a clause set such that $\bar{t}\in\mathcal{T}$ for every literal
$B(\bar{t})$ occurring in $\phi$. If $\phi$ is consistent under set-valued
first-order resolution, then $\phi$ is satisfiable over $\mathcal{G}$.

######  Proof 4.9.

By completeness of set-valued propositional resolution (Theorem 4.5), it
suffices to show that the clause set $\phi^{\mathcal{G}}$ consisting of all
instances over $\mathcal{G}$ of clauses in $\phi$ is consistent under set-
valued propositional resolution. Formally, an instance
${\llbracket\Gamma\rrbracket}\eta$ over $\mathcal{G}$ of a clause $\Gamma$ is
induced by an $A$-valuation $\eta$, and given as

${\llbracket\Gamma\rrbracket}\eta=\\{B({\llbracket\bar{t}\,\rrbracket}\eta)\mid
B(\bar{t}\,)\in\Gamma\\}.$

Since $\mathcal{T}$ is closed under unification, we can assume w.l.o.g. (using
Lemmas 4.1 and 4.3) that $\phi$ is closed under set-valued first-order
resolution with implicit two-sided factoring, i.e. under the rule
$(\mathit{SR}^{+})$ (since all terms that appear when closing $\phi$ under
resolution remain in $\mathcal{T}$); then it suffices to show that
$\phi^{\mathcal{G}}$ is closed under set-valued propositional resolution,
since $\phi$ and, hence, $\phi^{\mathcal{G}}$ do not contain blatantly
inconsistent clauses.

So let $\Gamma,A_{1}(\bar{t}_{1}),\dots,A_{n}(\bar{t}_{n})$ and
$B_{1}(\bar{s}_{1}),\dots,B_{m}(\bar{s}_{m}),\Delta$ be clauses in $\phi$,
with variables made disjoint. By the latter restriction, resolvable instances
of these clauses in $\mathcal{G}$ can be assumed to use the same valuation; so
let $\eta$ be a valuation such that
${\llbracket\bar{t}_{1}\rrbracket}\eta=\dots={\llbracket\bar{t}_{n}\rrbracket}\eta={\llbracket\bar{s}_{1}\rrbracket}\eta=\dots={\llbracket\bar{s}_{m}\rrbracket}\eta$.
Then in particular
$\bar{t}_{1}=\dots=\bar{t}_{n}=\bar{s}_{1}=\dots=\bar{s}_{m}$ is solvable in
$\mathcal{G}$. Since
$\bar{t}_{1},\dots,\bar{t}_{n},\bar{s}_{1},\dots,\bar{s}_{m}\in\mathcal{T}$,
it follows by $\mathcal{T}$-equational completeness of $\mathcal{G}$ that
$\bar{t}_{1},\dots,\bar{t}_{n},\bar{s}_{1},\dots,\bar{s}_{m}$ are unifiable,
hence have an mgu $\sigma$, and that $\sigma$ is a most general solution of
$\bar{t}_{1}=\dots=\bar{t}_{n}=\bar{s}_{1}=\dots=\bar{s}_{m}$ in
$\mathcal{G}$. This implies that $\eta$ has the form
$\eta(x)={\llbracket\sigma(x)\rrbracket}\eta^{\prime}$ for some $A$-valuation
$\eta^{\prime}$. Thus, the resolvent
${\llbracket\Gamma,((\bigcup_{i=1}^{n}A_{i})\cap(\bigcup_{i=1}^{m}B_{i}))(\bar{u}),\Delta\rrbracket}\eta$
of the two instances has the form
${\llbracket\Gamma\sigma,((\bigcup_{i=1}^{n}A_{i})\cap(\bigcup_{i=1}^{m}B_{i}))(\bar{u}\sigma),\Delta\sigma\rrbracket}\eta^{\prime}$,
and hence is in $\phi^{\mathcal{G}}$ as required since
$\Gamma\sigma,((\bigcup_{i=1}^{n}A_{i})\cap(\bigcup_{i=1}^{m}B_{i}))(\bar{u}\sigma),\Delta\sigma$
is in $\phi$ by closure of $\phi$ under $(\mathit{SR}^{+})$.

##  5 The AMC, Coalgebraically

To illustrate the use of one-step tableau rules, we briefly indicate how to
obtain the ExpTime upper bound for the AMC by Theorem 3.2. The requisite
functor $\mathsf{G}$ and the associated predicate liftings have been recalled
in Section 3. We recall the known rule set [23, 4]:

$\displaystyle(CD)\;\frac{\mathop{[D_{1}]}a_{1},\dots,\mathop{[D_{\alpha}]}a_{\alpha}}{a_{1},\dots,a_{\alpha}}$
$\displaystyle(C)\;\frac{\mathop{[D_{1}]}a_{1},\dots,\mathop{[D_{\alpha}]}a_{\alpha},\mathop{\langle
E\rangle}b,\mathop{\langle\Sigma\rangle}c_{1},\dots,\mathop{\langle\Sigma\rangle}c_{\beta}}{a_{1},\dots,a_{\alpha},b,c_{1},\dots,c_{\beta}}$

where for each $j,k$, $D_{j}\cap D_{k}=\emptyset$ and $D_{j}\subseteq E$.
Soundness of these rules is straightforward (they say in particular that
disjoint coalitions can combine their abilities and that coalitions inherit
the abilities of subcoalitions); for illustration, we show one-step tableau
completeness using set-valued resolution (Section 4), alternative to proofs in
the literature [28, 8, 22].

######  Theorem 5.1 (One-step tableau completeness).

The rules $(C)$, $(CD)$ are one-step tableau complete w.r.t. AMC.

By Theorem 3.2, this implies the known (tight) ExpTime upper bound for
satisfiability checking in the AMC [22].

######  Proof 5.2.

As indicated above, we present a proof producing infinite sets of moves in
one-step games, and then discuss how finiteness of move sets is regained using
the notion of $\mathcal{T}$-equationally complete (finite) model (Theorem
4.8).

Let $\tau$ be a $\mathcal{P}W$-valuation, and let
$\Xi=\\{\mathop{[D_{1}]}a_{1},\dots,\allowbreak\mathop{[D_{\alpha}]}a_{\alpha},\allowbreak\mathop{\langle
C_{1}\rangle}c_{1},\dots,\allowbreak\mathop{\langle
C_{\beta}\rangle}c_{\beta}\\}$ such that for every instance of $(C)$ or $(CD)$
that applies to (some subset of) $\Xi$, the conclusion $\Theta$ satisfies
${\llbracket\Theta\rrbracket}\tau\neq\emptyset$. We have to show that
${\llbracket\Xi\rrbracket}\tau\neq\emptyset$. To this end, we translate $\Xi$
into a clause set $\phi$ in set-valued first-order logic (Section 4),
generating one (singleton) clause for each modalized atom
$\mathop{[D_{j}]}a_{j}$ and $\mathop{\langle C_{j}\rangle}c_{j}$ according to
(1) and (2) (Section 4), with distinct Skolem constants $e^{j}_{D_{j}}$ and
Skolem functions $g^{j}_{\overline{C_{j}}}$, respectively. By Theorem 4.5, it
suffices to show that $\phi$ is consistent under set-valued resolution. We
observe the following.

  1. 1.

Two clauses $b_{j}$ and $b_{k}$ of shape (1), for $j\neq k$, resolve only if
$D_{j}\cap D_{k}=\emptyset$ – otherwise, unification fails due to a clash
between $e^{j}_{i}$ and $e^{k}_{i}$ for each agent $i\in D_{j}\cap D_{k}$.

  2. 2.

Similarly, a clause $b_{j}$ of shape (1) resolves with a clause $d_{k}$ of
shape (2) only if $D_{j}\cap\overline{C}_{k}=\emptyset$, i.e. $D_{j}\subseteq
C_{k}$.

  3. 3.

Similarly, two clauses $d_{j}$ and $d_{k}$ of shape (2), for $k\neq j$,
resolve only if $\overline{C_{j}}\cap\overline{C_{k}}=\emptyset$, i.e.
$C_{j}\cup C_{k}=\Sigma$

  4. 4.

Crucially, two clauses $d_{j}$ and $d_{k}$ of shape (2) , for $k\neq j$,
resolve only if at least one of $C_{j}$ and $C_{k}$ is $\Sigma$: Assume that
$p\in\overline{C_{j}}$ and $q\in\overline{C_{k}}$. By the previous item, $p\in
C_{k}$ and $q\in C_{j}$, so $x_{p}$ is an argument in $g^{k}_{q}$ and
$x^{\prime}_{q}$ (renamed for purposes of the resolution step) is an argument
in $g^{j}_{p}$, implying that unification of $d_{j}$ and $d_{k}$ fails at the
occurs check (cf. p. 4.2). This explains why only one $\mathop{\langle
E\rangle}$ with $E\neq N$ is needed in rule $(C)$.

These observations imply that a resolution proof of a blatantly inconsistent
(necessarily singleton) clause from $\phi$ will witness a rule match of either
$(C)$ or $(CD)$ (depending on whether clauses of shape (2) are involved), and
blatant inconsistency means that ${\llbracket\Theta\rrbracket}\tau=\emptyset$
for the corresponding rule conclusion $\Theta$, contradicting the assumption
on $\Xi$.

##### Finitely many moves

As indicated in Section 4, the model of $\Xi$ thus produced will have
infinitely many moves per agent, namely the ground terms generated by the
Skolem constants and functions. We can replace these with finitely many moves
where agents play _Skolem symbols_ paired with _colours_ – simulating the
effect of the occurs check from the unification procedure – taken from a
finite abelian group $U$ (with neutral element $0$ and group operation $+$)
that contains distinct elements $u_{1},\dots,u_{\beta}$ (e.g.
$U=\mathbb{Z}/\beta\mathbb{Z}$). Specifically, all agents receive (for
simplicity) the same moves, namely

  * •

moves $(e^{j},0)$ for $j=1,\dots,\alpha$, intended as witnesses for
$\mathop{[D_{j}]}a_{j}$, and

  * •

moves $(g^{j},u)$ for $j=1,\dots,\beta$ and $u\in U$, intended as witnesses
for $\mathop{\langle C_{j}\rangle}c_{j}$.

We refer to the first component of a move as its _move symbol_ , and to the
second as its _colour_. By $\mathsf{col}(m_{C})$ we denote the sum of all
colours of the moves in a joint move $m_{C}$ for $C$.

Let $\mathcal{T}$ be the unification closure of the set of all tuples of
argument terms occuring in clauses from $\phi$. By the above analysis, all
tuples in $\mathcal{T}$ essentially have the shape
$(x_{A},e_{B},g_{\,\overline{A\cup B}}(x_{A},e_{B}))$ where $x_{A}$ are
variables, $e_{B}$ are Skolem constants possibly from different box
modalities, and $g_{\,\overline{A\cup B}}$ are Skolem functions from a single
diamond (as Skolem functions for different diamonds do not initially occur in
the same tuple of terms and such occurrences are not introduced during
unification due to the occurs check); any one of $x_{A}$, $e_{B}$, $g$ may be
absent. The (finite) model $\mathcal{G}$ is then defined over coloured moves.
Skolem constants $e^{j}$ are interpreted as $(e^{j},0)$, and Skolem functions
$g_{i}^{j}$ for $i\in\overline{C_{j}}$ are interpreted as mapping a joint move
$m_{C_{j}}$ of $C_{j}$ to $(g^{j},u_{j}-\mathsf{col}(m_{C_{j}}))$ if $i$ is
the least element of $\overline{C_{j}}$, and to $(g^{j},0)$ otherwise, thus
ensuring that $\mathsf{col}(m_{C_{j}},g^{j}(m_{C_{j}}))=u_{j}$. We proceed to
show that $\mathcal{G}$ is $\mathcal{T}$-equationally complete, obtaining by
Theorem 4.8 and consistency of $\phi$ under set-valued first-order resolution
that $\phi$ is satisfiable over $\mathcal{G}$.

So let $t,u\in\mathcal{T}$ such that $t=u$ has a solution $\eta$ in
$\mathcal{G}$. We proceed by case distinction on the shape of $t=u$:

$(x_{A},e_{B})=(x^{\prime}_{A^{\prime}},e^{\prime}_{B^{\prime}})$: In the
simplest case the terms just consist of variables ($x_{A}$,
$x^{\prime}_{A^{\prime}}$) and Skolem constants ($e_{B}$,
$e^{\prime}_{B^{\prime}}$). Given the interpretation of the Skolem constants
in $\mathcal{G}$, it is clear that $e_{B}$ and $e_{B}^{\prime}$ must agree on
$B\cap B^{\prime}$ so $t,u$ are unifiable. The solution $\eta$ necessarily
replaces variables in $A\cap B^{\prime}$ and $A^{\prime}\cap B$ with the
respective interpretations of Skolem constants on the other side of the
equality. Hence, the solution $\eta$ factorizes through the mgu of $t$ and
$u$.

$(x_{A},e_{B},g^{j}_{\,\overline{A\cup
B}}(x^{\prime}_{A},e^{\prime}_{B}))=(x_{A^{\prime}},e_{B^{\prime}})$: This
case is similar to the previous one, using the observation that given the
interpretation of $g^{j}$ in $\mathcal{G}$, the equation can only have a
solution if $(\overline{A\cup B})\cap B^{\prime}=\emptyset$, i.e.
$(\overline{A\cup B})\subseteq A^{\prime}$.

$(x_{A},e_{B},g^{j}_{\,\overline{A\cup
B}}(x_{A},e_{B}))=(x^{\prime}_{A^{\prime}},e^{\prime}_{B^{\prime}},g^{k}_{\,\overline{A^{\prime}\cup
B^{\prime}}}(x^{\prime}_{A^{\prime}},e^{\prime}_{B^{\prime}}))$: The
interpretations of the terms $g^{j}_{\,\overline{A\cup B}}(x_{A},e_{B})$ and
$g^{k}_{\,\overline{A^{\prime}\cup
B^{\prime}}}(x_{A^{\prime}},e^{\prime}_{B^{\prime}}))$ in $\mathcal{G}$ (under
$\eta$) have the form $(g^{j},c)$ and $(g^{k},d)$ for some $c$ and $d$,
respectively. The case where $j=k$ is essentially like the previous cases. The
interesting case is where $j\neq k$, in which case necessarily
$\overline{A\cup B}\subseteq A^{\prime}$ and $\overline{A^{\prime}\cup
B^{\prime}}\subseteq A$; this is the case where unification of $t,u$ fails at
the occurs check as explained above. However, the construction of
$\mathcal{G}$ ensures that now $t=u$ also has no solution in $\mathcal{G}$, as
the respective interpretations of $g^{j}$ and $g^{k}$ ensure that the colour
of the whole joint move is $u_{j}$ on the left and $u_{k}$ on the right. The
proof for the AMCDES proceeds in a quite similar fashion, and will be
presented in less detail.

##  6 AMCDES Satisfiability

We now extend this treatment to obtain ExpTime satisfiability checking for
AMCDES, cast coalgebraically using the functor and predicate liftings
presented in Section 3. We have one-step rules $(\mathit{DES}_{0})$,
$(\mathit{DES}_{1})$, where $(\mathit{DES}_{1})$ is

$(\mathit{DES}_{1})\;\frac{\mathop{[D_{1},P_{G_{1}}]}a_{1},\dots,\mathop{[D_{\alpha},P_{G_{\alpha}}]}a_{\alpha},\mathop{\langle
E,Q_{K}\rangle}b,\mathop{\langle
C_{1},r_{H_{1}}\rangle}c_{1},\dots,\mathop{\langle
C_{\beta},r_{H_{\beta}}\rangle}c_{\beta}}{{(a_{j})}_{j\in
I_{q}},b,{(c_{j})}_{j\in J_{q}}\mid\cdots\text{ for }q\in Q_{K}}$

(i.e. the rule has one conclusion for each $q$) where $\mathit{Ag}(Q_{K})=K$;
the $r_{H_{j}}$ are (non-disjunctive) explicit joint moves for coalitions
$H_{j}$; $I_{q}\subseteq\\{1,\dots,\alpha\\}$,
$J_{q}\subseteq\\{1,\dots,\beta\\}$ for each $q\in Q_{K}$; and the following
side conditions hold, with
$L:=\bigcup^{\alpha}_{j=1}G_{j}\cup\bigcup^{\beta}_{j=1}H_{j}$:

  1. 1.

For each $j,k$, $D_{j}\cap D_{k}=\emptyset$.

  2. 2.

For each $j$, $C_{j}\cup H_{j}=\Sigma$.

  3. 3.

$\bigcup^{\alpha}_{j=1}D_{j}\cap L=\emptyset$.

  4. 4.

$\bigcup^{\alpha}_{j=1}D_{j}\subseteq E$.

  5. 5.

$E\cup K\supseteq L$.

  6. 6.

$r_{H_{j}}\mathrel{=_{\sqcap}}q$ for all $q\in Q_{K}$, $j\in J_{q}$.

  7. 7.

There is a joint explicit move $l$ for $E\cap L$ such that
$r_{H_{j}}\mathrel{=_{\sqcap}}l$ for each $q\in Q_{K}$, $j\in J_{q}$, and
moreover for each $j\in I_{q}$ there exists $p\in P_{G_{j}}$ such that
$p\mathrel{=_{\sqcap}}q$ and $p\mathrel{=_{\sqcap}}l$.

Rule $(\mathit{DES}_{0})$ is a variant of $(\mathit{DES}_{1})$ obtained by
instantiating to $\mathop{\langle
E,Q_{K}\rangle}b=\mathop{\langle\Sigma,\\{()\\}\rangle}\top$,
$I_{()}=\\{1,\dots,\alpha\\}$, and $J_{()}=\\{1,\dots,\beta\\}$, and then
omitting the (valid) literal $\mathop{\langle\Sigma,\\{()\\}\rangle}\top$ from
the rule premiss; side conditions 4.–6. then become trivial and can be
omitted.

Rule $(\mathit{DES}_{1})$ extends the rules for the basic AMC as recalled in
Section 5. The new features are intuitively understood as follows. Imagine
that $D_{1},\dots,D_{n}$ play moves witnessing their ability to
(conditionally) enforce $a_{1},\dots,a_{n}$. According to $\mathop{\langle
E,Q_{K}\rangle}$, $K$ can then play some move $q\in Q_{K}$ additionally
ensuring $b$; the $q$-th conclusion of $(\mathit{DES}_{1})$ captures the
constraints on the next state reached in this situation. These additionally
depend on the moves chosen by the remaining agents (those in
$E\setminus\bigcup D_{i}$): If the arising joint move restricts to one of the
moves in $P_{G_{j}}$, then $D_{j}$ successfully enforces $a_{j}$, and if it
restricts to $r_{H_{j}}$, then the next state must satisfy $c_{j}$ (note that
since $C_{j}\cup H_{j}=\Sigma$, $\mathop{\langle C_{i},r_{H_{k}}\rangle}c_{j}$
says that $c_{j}$ is enforced as soon as $H_{j}$ play $r_{H_{j}}$). The index
sets $I_{q}$ and $J_{q}$ indicate for which $j$ this applies, and side
conditions 6 and 7 ensure that a corresponding joint move actually exists. For
definiteness, we note

######  Lemma 6.1 (One-step soundness).

The rules $(\mathit{DES}_{0})$, $(\mathit{DES}_{1})$ are one-step tableau
sound w.r.t. AMCDES.

######  Proof 6.2.

By the above, it suffices to show soundness of $(\mathit{DES}_{1})$,
formalizing the above intuitive explanation. Write $\phi$ for the premiss of
the rule, and $\psi_{q}$ for the conclusion associated to $q\in Q_{K}$. Let
$\tau$ be a $\mathcal{P}W$-valuation such that
${\llbracket\phi\rrbracket}\tau\neq\emptyset$, and fix
$\mathcal{G}=((k_{j}),f,\iota)\in{\llbracket\phi\rrbracket}\tau$; we have to
show that ${\llbracket\psi_{q}\rrbracket}\tau\neq\emptyset$ for some $q\in
Q_{K}$. We refer to side conditions by their numbers:

  * •

For each $j\in\\{1,\dots,\alpha\\}$, we have a joint move $e_{j}$ for $D_{j}$
witnessing $\mathop{[D_{j},P_{G_{j}}]}a_{j}$. By 1., the $e_{j}$ can be
combined into a joint move $e$ for $\bigcup_{j=1}^{\alpha}D_{j}$.

  * •

By 3., $e$ can be combined with (the interpretation of) the explicit move $l$
postulated in 7. into a move $x_{0}$ for $(E\cap
L)\cup\bigcup_{j=1}^{\alpha}D_{j}\subseteq E$, where the inclusion is by 4.
Extend $x_{0}$ arbitrarily to a move $x$ for the whole coalition $E$.

  * •

Since $\mathcal{G}\in{\llbracket\mathop{\langle E,Q_{K}\rangle}b\rrbracket}$
and $\mathit{Ag}(x)=E$, there is some $q\in Q_{K}$ and a joint move $m_{q}$
for $\Sigma$ such that $x,q\sqsubseteq m_{q}$ and $f(m_{q})\in\tau(b)$.

  * •

To obtain that $f(m_{q})\in{\llbracket\psi_{q}\rrbracket}\tau$ for this $q$,
it remains to show that $f(m_{q})$ satisfies the remaining literals
$a_{j},c_{j}$ of $\psi_{q}$:

    * –

For $j\in I_{q}$, we have $e_{j}\sqsubseteq m_{q}$ and, by 5. and 7.,
$\iota[p]\sqsubseteq m_{q}$ for some $p\in P_{G_{j}}$, so that
$\mathcal{G}\in{\llbracket\mathop{[D_{j},P_{G_{j}}]}a_{j}\rrbracket}\tau$
implies $f(m_{q})\in\tau(a_{j})$.

    * –

For $j\in J_{q}$, we have $\iota[r_{H_{j}}]\sqsubseteq m_{q}$ by 5., 6., and
7. Since $C_{j}\cup H_{j}=\Sigma$, we thus have that
$\mathcal{G}\in{\llbracket\mathop{\langle
C_{k},r_{H_{k}}\rangle}c_{k}\rrbracket}\tau$ implies $f(m_{j})\in\tau(c_{k})$.

It remains to prove ompleteness:

######  Lemma 6.3 (One-step tableau completeness).

The rules $(\mathit{DES}_{0})$, $(\mathit{DES}_{1})$ are one-step tableau
complete w.r.t. AMCDES.

######  Proof 6.4.

Let $\tau$ be a $\mathcal{P}W$-valuation, and let
$\Xi=\\{\mathop{[D_{1},P_{G_{1}}]}a_{1},\dots,\allowbreak\mathop{[D_{\alpha},P_{G_{\alpha}}]}a_{\alpha},\allowbreak\mathop{\langle
C_{1},R_{H_{1}}\rangle}c_{1},\dots,\allowbreak\mathop{\langle
C_{\beta},R_{H_{\beta}}\rangle}c_{\beta}\\}$ such that every instance of
$(\mathit{DES}_{0})$ or $(\mathit{DES}_{1})$ whose premise is contained in
$\Xi$ has a conclusion that is non-empty under $\tau$. We have to show that
${\llbracket\Xi\rrbracket}\tau\neq\emptyset$. We translate $\Xi$ into a clause
set $\phi$ in set-valued first-order logic by including for each
$\mathop{[D_{j},P_{G_{j}}]}a_{j}$ and each $p\in P_{G_{j}}$ a singleton clause

$\\{\tau(a_{j})(e^{j}_{D_{j}},x_{\,\overline{D_{j}\cup G_{j}}},p)\\},$ (3)

(so $e^{j}_{D_{j}}$ witnesses $\mathop{[D_{j},P_{G_{j}}]}a_{j}$), and for each
$\mathop{\langle C_{j},R_{H_{j}}\rangle}c_{j}$ a clause

$\\{\tau(c_{j})(x_{C_{j}},g^{j}_{\,\overline{C_{j}\cup
H_{j}}}(x_{C_{j}}),r)\mid r\in R_{H_{j}}\\}$ (4)

(so the $g^{j}_{\,\overline{C_{j}\cup H_{j}}}$ are Skolem functions witnessing
$\mathop{\langle C_{j},R_{H_{j}}\rangle}c_{j}$). We now proceed as in the
proof of Theorem 5.1: We first show that $\phi$ is consistent under set-valued
resolution, obtaining by Theorem 4.5 that $\phi$ is satisfiable in a model
that may have infinitely many moves, and then present a finite
$\mathcal{T}$-equationally complete model for the unification closure
$\mathcal{T}$ of the involved terms. Write $b^{p}_{j}$ for clauses of type (3)
for given $j=1,\dots,\alpha$ and $p\in G_{j}$, and $d_{j}$ for the $j$-th
clause of type (4).

Unlike in the proof of Theorem 5.1, we thus may have non-singleton clauses, of
shape (4). We first note that implicit factoring plays no role in resolution
from this clause set: The non-singleton clause resulting from a diamond
$\mathop{\langle C_{j},R_{H_{j}}\rangle}c_{j}$ has a unique Skolem constant
$r\in R_{H_{j}}$ in each literal, so its literals do not unify among each
other. As unification does not get rid of these constants, this restriction
will be an invariant throughout resolution over this clause set. However, we
shall see that these non-singleton clauses do not resolve among each other. We
note the following observations.

  1. 1.

$b^{p}_{j}$ and $b^{q}_{j}$, for $p\neq q$, do not resolve (and resolving
$b^{p}_{j}$ with itself is pointless).

  2. 2.

$b^{p}_{j}$ and $b^{q}_{k}$, for $k\neq j$, resolve only if $D_{j}\cap
D_{k}=D_{j}\cap G_{k}=D_{k}\cap G_{j}=\emptyset$, and moreover
$p\mathrel{=_{\sqcap}}q$.

  3. 3.

$b^{p}_{j}$ and $d_{k}$ resolve, at the $d_{k}$-literal for $r\in R_{H_{k}}$,
only if $D_{j}\subseteq C_{k}$, and hence in particular also $D_{j}\cap
H_{k}=\emptyset$, $D_{j}\cup G_{j}\subseteq C_{k}\cup H_{k}$ (equivalently
$\overline{C_{k}\cup H_{k}}\subseteq\overline{D_{j}\cup G_{j}}$), and
$r\mathrel{=_{\sqcap}}p$.

  4. 4.

$d_{j}$ and $d_{k}$, for $k\neq j$, resolve, at the $d_{j}$-literal for $r\in
H_{j}$ and the $d_{k}$-literal for $r^{\prime}\in H_{k}$, only if $C_{j}\cup
C_{k}\cup H_{k}=\Sigma$ (equivalently $\overline{C_{k}\cup H_{k}}\subseteq
C_{j}$), $C_{k}\cup C_{j}\cup H_{j}=\Sigma$, and
$r\mathrel{=_{\sqcap}}r^{\prime}$.

  5. 5.

Like in the proof of Theorem 5.1, it follows that $d_{j}$ and $d_{k}$ resolve
only if at least one of $\mathop{\langle C_{j},R_{H_{j}}\rangle}$ and
$\mathop{\langle C_{k},R_{H_{k}}\rangle}$ is a grand coalition modality (since
otherwise unification fails at the occurs check), in which case the
corresponding clause is a singleton.

  6. 6.

Clauses obtained from clauses of shape (4) by resolving with singleton clauses
retain essentially shape (4), only with some of the variables $x_{i}$ replaced
with constants. Resolution of such clauses is thus subject to the same
restrictions; in particular, non-singleton clause of this kind they will not
resolve among each other.

Thus, a proof of a blatantly inconsistent clause from $\phi$ by set-valued
resolution will involve either zero or one clauses $d_{j}$ where $C_{j}\cup
H_{j}\neq\Sigma$. We will refer to resolution proofs of the first kind as
type-0 and to proofs of the second kind as type-1.

##### Type-0 proofs

We show that in this case, the impossibility of deriving a blatantly
inconsistent clause is obtained via rule $(\mathit{DES}_{0})$. To apply
$(\mathit{DES}_{0})$ to the set of modal atoms involved in the proof, we need
to show the side conditions of the rule (1.–3. and 7). Indeed, condition 2.
holds by the definition of type-0 proofs. As no disjunctive diamond is
involved in a type-0 proof, all involved clauses are singletons. Hence, 1.,
3., and 7. directly follow from the observations above. The type-0 proof at
hand thus induces a match of rule $(\mathit{DES}_{0})$ to a subset of $\Xi$;
the conclusion of this rule match having non-empty extension under $\tau$
means precisely that the resolution proof does not produce a blatantly
inconsistent clause.

##### Type-1 proofs

Those consist in successively resolving all literals of a single clause of the
form $d_{j_{0}}$ where $C_{j_{0}}\cup H_{j_{0}}\neq\Sigma$ with suitable
singleton clauses, of the form either $b^{p}_{j}$ or $d_{k}$ where $C_{k}\cup
H_{k}=\Sigma$. We will refer to these resolution steps as ‘resolving into
$d_{j_{0}}$’, although of course $d_{j_{0}}$ will have been modified by
previous resolution steps as described above. To match the notation of rule
$(\mathit{DES}_{1})$, we rename $\mathop{\langle
C_{j_{0}},R_{H_{j_{0}}}\rangle}$ into $\mathop{\langle E,Q_{K}\rangle}b$ (so
that all the $\mathop{\langle C_{j},R_{H_{j}}\rangle}c_{j}$ that remain have
$C_{j}\cup H_{j}=\Sigma$ and hence $|R_{H_{j}}|=1$). The literals in
$d_{j_{0}}$ are then indexed over $q\in Q_{K}$. Let $I_{q}$ be the set of all
$j$ such that for some $p\in P_{j}$, $b^{p}_{j}$ is resolved into $d_{j_{0}}$
at the literal for $q$, and put $G=\bigcup_{q\in Q_{K},j\in I_{q}}G_{j}$;
similarly, let $J_{q}$ be the set of all $j$ such that $d_{j}$ (a singleton
clause) is resolved into $d_{j_{0}}$ at the literal for $q$, and put
$H=\bigcup_{q\in Q_{K},j\in J_{q}}H_{j}$. Notice that two clauses resolve only
if whenever they both assign a constant (either a Skolem constant or an
explicit move) to a certain agent, then the constant is the same in both
clauses; this implies condition 7. Conditions 1. and 3. are established as in
the type-0 case, condition 2. is ensured by the above renaming, and the
remaining conditions follow directly from the above observations. The type-1
proof at hand thus induces a match of rule $(\mathit{DES}_{1})$ to a subset of
$\Xi$; a conclusion of this rule match having non-empty extension under $\tau$
means precisely that the resolution proof does not produce a blatantly
inconsistent clause.

##### Finitely many moves

As indicated above, we obtain a model with finitely many moves by constructing
a finite $\mathcal{T}$-equationally complete model $\mathcal{G}$, where
$\mathcal{T}$ is the unification closure of the tuples of terms occurring in
$\phi$. This construction is essentially the same as for the AMC, up to the
presence of additional constant symbols, viz. the explicit strategies
occurring in $\phi$. These constants can be treated exactly like the Skolem
constants already present in the proof of Theorem 5.1. The full proof is
available in Appendix B. Since the rules $(\mathit{DES}_{1})$,
$(\mathit{DES}_{0})$ are algorithmically sufficiently harmless, our main
result follows from Lemmas 6.1 and 6.3 by Theorem 3.2:

######  Theorem 6.5.

Satisfiability checking for the AMCDES is ExpTime-complete.

##  7 Conclusions

We have introduced the alternating-time $\mu$-calculus with disjunctive
explicit strategies (AMCDES), which extends  with explicit strategies (ATLES)
[30] with fixpoint operators and disjunction over explicit strategies of
opposing agents in non-grand modalities. We have employed methods from
coalgebraic logic to show that model checking with fixed interpretation of
explicit strategies is in QP as well as in $\textsc{NP}\cap\textsc{coNP}$, and
in NP with open interpretation of strategies, and moreover that satisfiability
checking is in ExpTime.

The coalgebraic treatment in fact implies a whole range of additional results,
e.g. reasoning in the next-step fragment of the logic extended with nominals
(ExpTime with global axioms, and PSpace without) [25, 18, 9]; cut-free sequent
systems for the next-step fragment [20]; and completeness of a Kozen-Park
axiomatization for flat (i.e. single-variable) fragments of the AMCDES, e.g.
ATL with disjunctive explicit strategies [26]. A special case of the latter
result is completeness of ATLES as proved already in Walther et al. [30].

In ongoing work we are extending our axiomatization and complexity results to
allow strategy disjunction also in grand coalition modalities. A natural but
more challenging further extension would be to add negative strategies
prohibiting moves for some agents as suggested by Herzig et al. [13].

## References

  * [1] Rajeev Alur, Thomas Henzinger, and Orna Kupferman.  Alternating-time temporal logic.  J. ACM, 49:672–713, 2002.  doi:10.1145/585265.585270.
  * [2] Cristian Calude, Sanjay Jain, Bakhadyr Khoussainov, Wei Li, and Frank Stephan.  Deciding parity games in quasipolynomial time.  In Theory of Computing, STOC 2017, pages 252–263. ACM, 2017\.
  * [3] Krishnendu Chatterjee, Thomas A. Henzinger, and Nir Piterman.  Strategy logic.  Inf. Comput., 208(6):677–693, 2010.  doi:10.1016/j.ic.2009.07.004.
  * [4] Corina Cîrstea, Clemens Kupke, and Dirk Pattinson.  EXPTIME tableaux for the coalgebraic $\mu$-calculus.  Log. Methods Comput. Sci., 7(3), 2011.  doi:10.2168/LMCS-7(3:3)2011.
  * [5] Corina Cîrstea, Alexander Kurz, Dirk Pattinson, Lutz Schröder, and Yde Venema.  Modal logics are coalgebraic.  Comput. J., 54(1):31–41, 2011.  doi:10.1093/comjnl/bxp004.
  * [6] Melvin Fitting.  First-Order Logic and Automated Theorem Proving.  Springer, 2nd edition, 1996.  doi:10.1007/978-1-4612-2360-3.
  * [7] Valentin Goranko and Fengkui Ju.  Towards a logic for conditional local strategic reasoning.  In Patrick Blackburn, Emiliano Lorini, and Meiyun Guo, editors, Logic, Rationality, and Interaction, LORI 2019, volume 11813 of LNCS, pages 112–125. Springer, 10 2019.  doi:10.1007/978-3-662-60292-8_9.
  * [8] Valentin Goranko and Govert van Drimmelen.  Complete axiomatization and decidability of alternating-time temporal logic.  Theor. Comput. Sci., 353(1-3):93––117, 3 2006.  doi:10.1016/j.tcs.2005.07.043.
  * [9] Rajeev Goré, Clemens Kupke, Dirk Pattinson, and Lutz Schröder.  Global caching for coalgebraic description logics.  In Automated Reasoning, IJCAR 2010, volume 6173 of LNCS, pages 46–60. Springer, 2010.  doi:10.1007/978-3-642-14203-1.
  * [10] Merlin Göttlinger, Lutz Schröder, and Dirk Pattinson.  The alternating-time $\mu$-calculus with disjunctive explicit strategies.  In Christel Baier and Jean Goubault-Larrecq, editors, Computer Science Logic, CSL 2021, volume 183 of LIPIcs, pages 26:1–26:22. Schloss Dagstuhl – Leibniz-Zentrum für Informatik, 2021.  doi:10.4230/LIPIcs.CSL.2021.26.
  * [11] Erich Grädel, Wolfgang Thomas, and Thomas Wilke, editors.  Automata, Logics, and Infinite Games: A Guide to Current Research, volume 2500 of LNCS. Springer, 2002.  doi:10.1007/3-540-36387-4.
  * [12] Daniel Hausmann and Lutz Schröder.  Game-based local model checking for the coalgebraic mu-calculus.  In Concurrency Theory, CONCUR 2019, volume 140 of LIPIcs, pages 35:1–35:16. Schloss Dagstuhl – Leibniz-Zentrum für Informatik, 8 2019.  URL: http://www.dagstuhl.de/dagpub/978-3-95977-121-4, doi:10.4230/LIPIcs.CONCUR.2019.35.
  * [13] Andreas Herzig, Emiliano Lorini, and Dirk Walther.  Reasoning about actions meets strategic logics.  In Logic, Rationality, and Interaction, LORI 2013, volume 8196 of LNCS, pages 162–175. Springer, 2013.  doi:10.1007/978-3-642-40948-6\\_13.
  * [14] Marc-Uwe Kling.  Das Känguru-Manifest.  Ullstein, Berlin, 2011.
  * [15] Marc-Uwe Kling.  The Kangaroo Chronicles.  Voland & Quist, 2016.  Translated by Sarah Cossaboon and Paul-Henri Campbell.
  * [16] Fabio Mogavero, Aniello Murano, Giuseppe Perelli, and Moshe Vardi.  Reasoning about strategies: On the model-checking problem.  ACM Trans. Comput. Log., 15(4):34:1–34:47, 2014.  doi:10.1145/2631917.
  * [17] Fabio Mogavero, Aniello Murano, Giuseppe Perelli, and Moshe Vardi.  Reasoning about strategies: on the satisfiability problem.  LMCS, 13(1), 2017.  doi:10.23638/LMCS-13(1:9)2017.
  * [18] Robert Myers, Dirk Pattinson, and Lutz Schröder.  Coalgebraic hybrid logic.  In Foundations of Software Science and Computational Structures, FOSSACS 2009, volume 5504 of LNCS, pages 137–151. Springer, 2009.  doi:10.1007/978-3-642-00596-1.
  * [19] Rocco De Nicola and Frits W. Vaandrager.  Action versus state based logics for transition systems.  In Irène Guessarian, editor, Semantics of Systems of Concurrent Processes, LITP Spring School on Theoretical Computer Science 1990, volume 469 of LNCS, pages 407–419. Springer, 4 1990.  doi:10.1007/3-540-53479-2_17.
  * [20] Dirk Pattinson and Lutz Schröder.  Cut elimination in coalgebraic logics.  Inf. Comput., 208(12):1447–1468, 2010.  doi:10.1016/j.ic.2009.11.008.
  * [21] Marc Pauly.  A modal logic for coalitional power in games.  J. Log. Comput., 12(1):149–166, 2002.  doi:10.1093/logcom/12.1.149.
  * [22] Sven Schewe.  Synthesis of Distributed Systems.  PhD thesis, Universität des Saarlandes, 2008.
  * [23] Lutz Schröder and Dirk Pattinson.  PSPACE bounds for rank-1 modal logics.  ACM Trans. Comput. Log., 10(2):13:1–13:33, 2009.  doi:10.1145/1462179.1462185.
  * [24] Lutz Schröder and Dirk Pattinson.  Modular algorithms for heterogeneous modal logics via multi-sorted coalgebra.  Math. Struct. Comput. Sci., 21(2):235–266, 2011.  doi:10.1017/S0960129510000563.
  * [25] Lutz Schröder, Dirk Pattinson, and Clemens Kupke.  Nominals for everyone.  In International Joint Conference on Artificial Intelligence, IJCAI 2009, pages 917–922, 7 2009.  URL: http://ijcai.org/proceedings/2009.
  * [26] Lutz Schröder and Yde Venema.  Completeness of flat coalgebraic fixpoint logics.  ACM Trans. Comput. Log., 19(1):4:1–4:34, 2018.  doi:10.1145/3157055.
  * [27] Wiebe van der Hoek, Wojciech Jamroga, and Michael Wooldridge.  A logic for strategic reasoning.  In Autonomous Agents and Multiagent Systems, AAMAS 2005, pages 157–164. ACM, 2005.  doi:10.1145/1082473.1082497.
  * [28] Govert van Drimmelen.  Satisfiability in alternating-time temporal logic.  In Logic in Computer Science, LICS 2003, pages 208–217. IEEE Comp. Soc., 6 2003.  URL: http://ieeexplore.ieee.org/xpl/mostRecentIssue.jsp?punumber=8592, doi:10.1109/LICS.2003.1210060.
  * [29] Dirk Walther.  Strategic Logics: Complexity, Completeness and Expressivity.  PhD thesis, University of Liverpool, 2007.
  * [30] Dirk Walther, Wiebe van der Hoek, and Michael Wooldridge.  Alternating-time temporal logic with explicit strategies.  In Theoretical Aspects of Rationality and Knowledge, TARK 2007, pages 269–278. ACM Press, 2007.  doi:10.1145/1324249.1324285.
  * [31] Thomas Ågotnes.  Action and knowledge in alternating-time temporal logic.  Synthese, 149(2):375–407, 3 2006.  doi:10.1007/s11229-005-3875-8.

##  Appendix A Appendix: AMCDES Model Checking Details

### Summary of Results on Coalgebraic Model Checking

Given a functor $F$, we assume a representation of the elements of $FX$, for
finite $X$, as strings over some alphabet. Specifically, we represent elements
of $({(k_{j})}_{j\in\Sigma},f)\in\mathsf{G}X$ as tabulations of $f$.

Model checking results [12] for the full coalgebraic $\mu$-calculus require
only very simple properties of the predicate liftings:

######  Definition 5.

The _one-step satisfaction problem_ is to determine, given a finite set $X$,
$Y\subseteq X$, $\mathop{\heartsuit}\in\Lambda$, and $t\in FX$, whether
$t\in{\llbracket\mathop{\heartsuit}\rrbracket}_{X}(Y)$.

######  Theorem A.1 (Model checking via one-step satisfaction [12, Theorem
11]).

If the one-step satisfaction problem is in P, then the model checking problem
for the coalgebraic $\mu$-calculus over this logic is in
$\textsc{NP}\cap\textsc{coNP}$.

The proof of this upper bound is via parity games, specifically by noting that
Cîrstea et al.’s _evaluation games_ [4] are exponentially large but have only
polynomially many $\mathsf{Eloise}$-nodes, so that winning strategies for
$\mathsf{Eloise}$ can be guessed and verified in (nondeterministic) polynomial
time.

On the other hand, to obtain a model checking algorithm in QP (deterministic
quasipolynomial time $2^{\mathcal{O}((\log n)^{k})}$ for some $k$; a
complexity class not currently known to be comparable with NP) we need to show
that we can design suitable one-step satisfaction arenas for use in model
checking games (we use standard terminology for games, e.g. [11]):

######  Definition 6.

A _one-step satisfaction arena_ $\mathsf{A}$ for a set $X$, a modality
$\mathop{\heartsuit}\in\Lambda$, and $t\in FX$ is an acyclic arena for games
with two players $\mathsf{Eloise}$ and $\mathsf{Abelard}$ (recall that an
arena is like a game in that it specifies nodes, each assigned to one of the
players, and allowed moves between nodes but does not include a winning
condition; acyclicity refers to the move relation), with a single initial
node, with $X$ as the set of terminal nodes, and with additional inner nodes.
A _one-step game_ on $\mathsf{A}$ additionally specifies a winning condition
in the shape of a subset $Y$ of the terminal nodes; then, $\mathsf{Eloise}$
wins plays that either get stuck at an inner $\mathsf{Abelard}$ node without
successors or terminate in a node in $Y$. We say that $\mathsf{A}$ is _sound
and complete_ if for every $Y\subseteq X$, $\mathsf{Eloise}$ wins (the initial
node of) the one-step game on $\mathsf{A}$ with winning condition $Y$ iff
$t\in{\llbracket\mathop{\heartsuit}\rrbracket}_{X}(Y)$.

######  Theorem A.2 (Model checking via one-step games [12, Corollary 18]).

If for every set $X$, $\mathop{\heartsuit}\in\Lambda$, and $t\in FX$, there is
a sound and complete one-step satisfaction arena with polynomially many inner
nodes in the representation size of $\mathop{\heartsuit}$ and $t$, then the
model checking problem for the $\mu$-calculus over this logic is in QP.

The model checking procedure underlying this theorem is to construct a
polynomial-size model checking parity game using one-step games as building
blocks; by well-known recent advances in parity game solving [2], these games
can be solved in quasipolynomial time.

### Proof of Theorem 2.7

######  Proof A.3.

The one-step satisfaction problem for the AMCDES is to check whether
$((k_{j}),f,\iota)\in{\llbracket\mathop{[C,O]}\rrbracket}_{X}(Y)$ can be
decided in P for given $C,O$, $Y\subseteq X$, and a one-step game with
explicit strategies $((k_{j}),f,\iota)\in\mathsf{G}_{\mathsf{ES}}X$. This can
be done by iterating over joint moves of $C$ in an outer loop and over joint
moves of $\overline{C}$ in an inner loop. Since $f$ needs to tabulate the
outcomes of all joint moves of $\Sigma$, both loops have at most linearly many
(in the size of $f$) iterations per invocation, making for a quadratic overall
number of iterations of the inner loop, and hence polynomial run time.

for  _$m_{C}\leftarrow[k_{C}]$_ do

$x:=\top$

for  _$o\leftarrow O,m_{\bar{C}}\leftarrow[k_{\Sigma\setminus
C\setminus\mathit{Ag}(O)}]$_ do

if  _$f(m_{c},m_{\bar{C}},\iota[o])\notin Y$_ then $x:=\bot$

if  _$x$_ then return $\top$

return $\bot$

Algorithm 1 One-step Satisfaction Algorithm

By Theorem A.1, we thus obtain the $\textsc{NP}\cap\textsc{coNP}$ bound for
the fixed case. The NP bound for the open case follows by guessing history-
free strategies.

For the QP bound, we use Theorem A.2 and adapt the one-step satisfaction
arenas for the AMC [12, Example 15.5] to obtain small one-step satisfaction
arenas for the AMCDES:

The one-step satisfaction arena
$A_{\mathop{[C,O]},w}=(V_{\mathop{[C,O]},w},E_{\mathop{[C,O]},w})$ for $X$,
$\mathop{[C,O]}$, and a one-step game
$((k_{j}),f,\iota)\in\mathsf{G}_{\mathsf{ES}}X$ for disjoint
$C,D\subseteq\Sigma$, $O\subseteq\prod_{a\in D}M_{a}$ is constructed as
follows. The node set $V_{\mathop{[C,O]},w}$ consists of an initial node
$(\mathop{[C,O]},w)$ belonging to $\mathsf{Eloise}$, and additionally a set of
inner nodes $I_{\mathop{[C,O]},w}:=[k_{C}]$ belonging to $\mathsf{Abelard}$
i.e. one node for each joint move of $C$. The set $E_{\mathop{[C,O]},w}(x)$ of
moves available at a node $x$ is

$\displaystyle E_{\mathop{[C,O]},w}(x)=\begin{cases}I_{\mathop{[C,O]},w}\text{
if }x=(\mathop{[C,O]},w)\\\ \\{f(x,m_{\bar{C}},o)\mid
m_{\bar{C}}\in[k_{\,\overline{C\cup D}}],o\in\iota[O]\\}\end{cases}$

It is easy to see that the size of the arena is thus linear in the tabulation
size of $f$. The soundness and completeness of the resulting one-step
satisfaction game stems from the fact that the moves of $\mathsf{Eloise}$ and
$\mathsf{Abelard}$ essentially construct the witnessing moves from the
original game.

##  Appendix B Appendix: Omitted Proofs and Further Details

### Proof of Theorem 4.5

##### Soundness

It suffices to show that the rule $(SR)$ is sound. Let
$\Gamma,A_{1}(\bar{t_{1}}),\dots,A_{n}(\bar{t_{n}})$ and $B(\bar{u}),\Delta$
be two clauses such that $\bar{t}_{1},\dots,\bar{t}_{n}$, and $\bar{u}$ are
unifiable, and let $\sigma=mgu(\bar{t_{1}},\dots,\bar{t_{n}},\bar{u})$. Let
$\mathcal{G}=((S_{j})_{j\in N},f,W,{\llbracket-\rrbracket})$ be an outcome
model satisfying both $\Gamma,A_{1}(\bar{t_{1}}),\dots,A_{n}(\bar{t_{n}})$ and
$B(\bar{u}),\Delta$. Let $\eta$ be a valuation such that
$\mathcal{G},\eta\not\models\Gamma\sigma,\Delta\sigma$; we have to show
$\mathcal{G},\eta\models((\bigcup_{i=1}^{n}A_{i})\cap B)(\bar{u}\sigma)$. By
the evident substitution lemma,
$\mathcal{G},\eta_{\sigma}\not\models\Gamma,\Delta$ where
$\eta_{\sigma}(x)={\llbracket\sigma(x)\rrbracket}\eta$ for all $x$; hence
necessarily $\mathcal{G},\eta_{\sigma}\models
A_{1}(\bar{t_{1}}),\dots,A_{n}(\bar{t_{n}})$, and
$\mathcal{G},\eta_{\sigma}\models B(\bar{u})$. Again by the substitution
lemma, $\mathcal{G},\eta\models
A_{1}(\bar{t_{1}}\sigma),\dots,A_{n}(\bar{t_{n}}\sigma)$, and
$\mathcal{G},\eta\models B(\bar{u}\sigma)$. Since
$\bar{t_{1}}\sigma=\dots=\bar{t_{n}}\sigma=\bar{u}\sigma$, our goal
$\mathcal{G},\eta\models((\bigcup_{i=1}^{n}A_{i})\cap B)(\bar{t}\sigma)$
follows by the semantics of literals.

##### Completeness

The completeness proof for the propositional variant proceeds via _maximally
consistent clause sets_ , defined in the expected way. By Zorn’s lemma, we
have

######  Lemma B.1 (Lindenbaum lemma for set-valued propositional resolution).

Every consistent clause set in set-valued propositional logic is contained in
a maximally consistent set.

Moreover, we have the following set of Hintikka properties:

######  Lemma B.2 (Hintikka lemma for set-valued propositional resolution).

Let $\phi$ be a maximally consistent clause set in set-valued propositional
logic. Then

  1. 1.

A clause $\Gamma,\Delta$ is in $\phi$ iff $\Gamma\in\phi$ or $\Delta\in\phi$.

  2. 2.

A clause $\Gamma,(A\cup B)(y)$ is in $\phi$ iff one of $\Gamma,A(y)$ and
$\Gamma,B(y)$ is in $\phi$.

  3. 3.

For every $y\in Y$, $W(y)\in\phi$.

######  Proof B.3.

_1, ‘if’:_ Assume w.l.o.g. that $\Gamma\in\phi$. By maximality, it suffices to
show that $\phi\cup\\{\Gamma,\Delta\\}$ remains consistent. So assume that a
blatantly inconsistent clause can be derived from
$\phi\cup\\{\Gamma,\Delta\\}$. Then by removing literals from the clauses in
this derivation, we obtain a derivation of a blatantly inconsistent clause
from $\phi\cup\\{\Gamma\\}$, contradiction.

_1, ‘only if’:_ By maximality, it suffices to show that one of
$\phi\cup\\{\Gamma\\}$ and $\phi\cup\\{\Delta\\}$ is consistent. Assume the
contrary. Then one can derive a blatantly inconsistent clause
$\Gamma^{\prime}$ from $\phi\cup\\{\Gamma\\}$. Adding $\Delta$ to all clauses
in the derivation (that is, to the original $\Gamma$ and then to all clauses
newly produced by the resolution rule), we obtain a derivation of
$\Gamma^{\prime},\Delta$ from $\phi\cup\\{\Gamma,\Delta\\}$. Similarly, we
have a derivation of a blatantly inconsistent clause $\Delta^{\prime}$ from
$\phi\cup\\{\Delta\\}$, from which we obtain a derivation of
$\Gamma^{\prime},\Delta^{\prime}$ from $\phi\cup\\{\Gamma^{\prime},\Delta\\}$.
Chaining the two derivations, we obtain a derivation of the blatantly
inconsistent clause $\Gamma^{\prime},\Delta^{\prime}$ from
$\phi\cup\\{\Gamma,\Delta\\}$, contradiction.

_2, ‘if’:_ Assume w.l.o.g. that $\Gamma,A(y)$ is in $\phi$. By maximality, it
suffices to show that $\phi\cup\\{\Gamma,(A\cup B)(y)\\}$ is consistent.
Assume the contrary, i.e. we can derive a blatantly inconsistent clause from
$\Gamma,(A\cup B)(y)$. Tracing $(A\cup B)(y)$ through the derivation in the
obvious sense (with $A\cup B$ possibly transformed into strictly smaller
subsets by the resolution rule) and intersecting with $A$ at each occurrence,
we obtain a derivation of a blatantly inconsistent clause from
$\phi\cup\\{\Gamma,A(y)\\}=\phi$, contradiction.

_2, ‘only if’:_ By contraposition, again using maximality: assume that both
$\phi\cup\\{\Gamma,A(y)\\}$ and $\phi\cup\\{\Gamma,B(y)\\}$ are inconsistent;
we have to show that $\phi\cup\\{\Gamma,(A\cup B)(y)\\}$ is inconsistent. By
assumption, we can derive from $\phi\cup\\{\Gamma,A(y)\\}$ a blatantly
inconsistent clause, necessarily of the form $\Gamma^{\prime},\emptyset(y)$
(since no $y\in Y$ can be made to disappear by the resolution rule). Tracing
$A(y)$ through the derivation and taking unions with $B$ at each occurrence,
we obtain a derivation of $\Gamma^{\prime},B(y)$ from
$\phi\cup\\{\Gamma,(A\cup B)(y)\\}$. Similarly, we can derive a blatantly
inconsistent clause from $\phi\cup\\{\Gamma,B(y)\\}$. Replacing literals
$C(z)$ with $\emptyset(z)$ and adding new literals of the form $\emptyset(z)$,
we obtain a derivation of a blatantly inconsistent clause $\Theta$ from
$\phi\cup\\{\Gamma^{\prime},B(y)\\}$. Chaining derivations, we obtain a
derivation of $\Theta$ from $\phi\cup\\{(A\cup B)(y)\\}$, showing the required
inconsistency.

_3:_ Clear.

Now fix a maximally consistent clause set $\phi$, and assume that $W$ is
finite; we construct a model, i.e. a function $f_{\phi}:Y\to W$, from $\phi$
as follows. For $y\in Y$, we have $W(y)\in\phi$ by the Hintikka lemma, and
then, again by the Hintikka lemma and by finiteness of $W$,
$\\{w_{y}\\}(y)\in\phi$ for some $w_{y}\in W$, which by consistency of $\phi$
is moreover unique; we put $f_{\phi}(y)=w_{y}$.

######  Lemma B.4 (Truth lemma for set-valued propositional resolution).

Given a maximally consistent clause set $\phi$ in set-valued propositional
logic over a finite set $W$, the function $f_{\phi}$ constructed above
satisfies $\phi$.

######  Proof B.5.

Induction over the size of clauses $\Gamma$, measured as the sum of the
cardinalities of the subsets of $W$ occurring in $\Gamma$. The inductive step
makes a case distinction over whether there is more than one or exactly one
literal in $\Gamma$ (the case of zero literals does not occur, as a clause
without literals is blatantly inconsistent), and then proceeds according to
the relevant clause of the Hintikka lemma. We are left with the induction
base, where $\Gamma$ has the form $\\{w\\}(y)$; in this case, the claim holds
by construction of $f_{\phi}$.

In combination with Lemma B.1, this proves completeness of the propositional
variant. Completeness for the first-order variant is then shown via a form of
Herbrand theory. We build a _Herbrand universe_ where the moves of each agent
$i$ are ground terms of sort $i$. We denote these sets of moves by $S_{i}$. A
_ground substitution_ replaces variables by ground terms, respecting sorts.
_Ground instances_ of literals $A(\bar{t})$, clauses, and clause sets are
obtained by applying a ground substitution.

Now let $\phi$ be a clause set in set-valued first-order logic that is closed
under set-valued first-order resolution and not blatantly inconsistent; it
suffices to show that such $\phi$ are satisfiable. By admissibility of
$(\mathit{lSR})$ (Lemma 4.1), we can assume that $\phi$ is even closed under
$(\mathit{lSR})$, and hence closed under set-valued first-order resolution
with two-sided factoring, i.e. under the rule $(\mathit{SR}^{+})$, as this
rule is derivable from $(\mathit{lSR})$ (Lemma 4.3). We denote by $I(\phi)$
the set of ground instances of clauses in $\phi$. In the same way as
admissibility of $(\mathit{lSR})$ under $(\mathit{SR})$, one shows easily that
a liberalized variant $(\mathit{lSR}^{+})$ of $(\mathit{SR}^{+})$ where the
substitution applied is only required to be a unifier (rather than an mgu) is
admissible under $(\mathit{SR}^{+})$, so we can assume that $\phi$ is even
closed under $(\mathit{lSR}^{+})$. To show that $\phi$ is satisfiable over the
Herbrand universe, it suffices to establish that $I(\phi)$ is satisfiable.
Clearly, $I(\phi)$ is not blatantly inconsistent. We show that it is moreover
closed under set-valued propositional resolution (implying that $I(\phi)$ is
satisfiable, and hence that $\phi$ is satisfiable). A pair of resolvable
clauses in $I(\phi)$ has the form
$\Gamma\theta,(\bigcup_{i=1}^{n}A_{i})(\bar{t}_{1}\theta)$ and
$(\bigcup_{i=1}^{m}B_{i})(\bar{u}_{1}\theta),\Delta\theta$ where
$\Gamma,A_{1}(\bar{t}_{1}),\dots,A_{n}(\bar{t}_{n})$ and
$B_{1}(\bar{u}_{1}),\dots,B_{m}(\bar{u}_{m}),\Delta$ are in $\phi$, w.l.o.g.
with disjoint sets of variables, and $\theta$ is a ground substitution such
that
$\bar{t}_{1}\theta=\dots=\bar{t}_{n}\theta=\bar{u}_{1}\theta=\dots=\bar{u}_{m}\theta$.
In particular, $\theta$ is a unifier of
$\bar{t}_{1},\dots,\bar{t}_{n},\bar{u}_{1},\dots,\bar{u}_{m}$. It follows that
the resolvent
$\Gamma\theta,((\bigcup_{i=1}^{n}A_{i})\cap(\bigcup_{i=1}^{m}B)(\bar{u}\theta),\Delta\theta$
of $\Gamma,A_{1}(\bar{t}_{1}),\dots,A_{n}(\bar{t}_{n})$ and
$B_{1}(\bar{u}_{1}),\dots,B_{m}(\bar{u}_{m}),\Delta$ under
$(\mathit{lSR}^{+})$ is in $\phi$, and hence (since $\theta$ is already
ground) in $I(\phi)$; but this clause is the propositional resolvent of the
given clauses $\Gamma\theta,(\bigcup_{i=1}^{n}A_{i})(\bar{t}_{1}\theta)$ and
$(\bigcup_{i=1}^{m}B_{i})(\bar{u}_{1}\theta),\Delta\theta$, so we are done. ∎

### Remarks on One-step Tableau Completeness for the AMC (Theorem 5.1)

In the proof of Theorem 5.1, one could equally well have used previous one-
step model constructions implicit in van Drimmelen, Goranko, and Schewe [28,
8, 22]; we provide our construction for illustration, in preparation for the
treatment of disjunctive explicit strategies, to which, as far as we can see,
the previous constructions do not adapt (they do extend to explicit strategies
without strategy disjunction). We note that the model construction becomes
much simpler if one excludes the grand coalition (as, effectively, in ATLES):
In the rule $(C)$, the literals $\mathop{\langle\Sigma\rangle}c_{j}$
disappear; in the proof of one-step tableau completeness of the arising rule,
one can just use a single move $\bot$ as witness for all $\mathop{\langle
C_{j}\rangle}c_{j}$ in $\Xi$ (in the notation of the original proof of Theorem
5.1), using non-determinism to ensure satisfaction of the $\mathop{\langle
C_{j}\rangle}c_{j}$. In detail, this is seen as follows.

As indicated above, in the absence of grand coalition modalities, rule $(C)$
specializes to

$(C^{-})\;\frac{\mathop{[D_{1}]}a_{1},\dots,\mathop{[D_{\alpha}]}a_{\alpha},\mathop{\langle
E\rangle}b}{a_{1},\dots,a_{\alpha},b}$

with the same side conditions as $(C)$. The shorter proof of one-step tableau
completeness then runs as follows. Let $\tau$ be a $\mathcal{P}W$-valuation,
and let
$\Xi=\\{\mathop{[D_{1}]}a_{1},\dots,\mathop{[D_{\alpha}]}a_{\alpha},\mathop{\langle
C_{1}\rangle}c_{1},\dots,\mathop{\langle C_{\beta}\rangle}c_{\beta}\\}$ (where
$D_{j}\neq\Sigma$, $C_{j}\neq\Sigma$ for all $j$) be such that every rule
match of $(C^{-})$ to $\Xi$ has non-empty conclusion under $\tau$. We have to
construct an element of ${\llbracket\Xi\rrbracket}\tau$. Give every agent
moves $e_{j}$ for $j=1,\dots,n$ intended as witnesses for
$\mathop{[D_{j}]}a_{j}$, and a single refusal move $\bot$; write (slightly
abusively) $e_{D_{j}}$ for the joint move of $D_{j}$ that is $e_{j}$ in all
components. Define a non-deterministic outcome function $f$ by
$f(m_{\Sigma})=\textstyle\bigcap_{e_{D_{j}}\sqsubseteq
m_{\Sigma}}\tau(a_{j}),$ noting that this set is non-empty thanks to rule
$(CD)$ since for $j\neq k$, having both $e_{D_{j}}\sqsubseteq m_{\Sigma}$ and
$e_{D_{k}}\sqsubseteq m_{\Sigma}$ implies $D_{j}\cap D_{k}=\emptyset$. Then
$f$ clearly satisfies $\mathop{[D_{j}]}a_{j}$ under $\tau$. To see that $f$
also satisfies $\mathop{\langle C_{j}\rangle}c_{j}$, let $m_{C_{j}}$ be a
joint move of $C_{j}$. Let $m_{\Sigma}$ be the joint move of $\Sigma$
extending $m_{C_{j}}$ by letting all other agents pick $\bot$. We have to show
that $f(m_{\Sigma})\cap\tau(c_{j})\neq\emptyset$. But this is immediate by
rule $(C^{-})$, since $e_{D_{k}}\sqsubseteq m_{\Sigma}$ implies
$D_{k}\subseteq C_{j}$.

We note further that excluding grand coalition modalities is equivalent to
making the outcome function non-deterministic: It is clear that excluding
grand coalition modalities is equivalent to always taking the set of agents to
consist of the agents $\Sigma_{\phi}$ mentioned in the target formula $\phi$
and one extra agent $*$ (convert models with larger set $C$ of additional
agents into one with only $*$ by taking the previous joint moves of $C$ to be
the moves of $*$). Then, note that $\phi$ is satisfiable in a CGS with set
$\Sigma_{\phi}\cup\\{*\\}$ of agents iff $\phi$ is satisfiable in a _non-
deterministic CGS_ with set $\Sigma=\Sigma_{\phi}$ of agents, where a non-
deterministic CGS is defined like a CGS except that the outcome function
$f_{q}$ at a state $q$ returns a non-empty set of possible post-states rather
than just a single post-state. Over such a non-deterministic CGS, a formula
$\mathop{[C]}\psi$ is satisfied at a state $q$ if $C$ has a joint move $m_{C}$
such that for all joint moves $m_{\overline{C}}$ of $\overline{C}$, _all_
possible post-states of $q$ under the induced joint move of $\Sigma$ satisfy
$\psi$. A non-deterministic CGS with set $\Sigma$ of agents is converted into
a CGS with set $\Sigma\cup\\{*\\}$ of agents by giving $*$ all states as
moves, allowing $*$ to pick one of the possible post-states determined by the
other agents (with some possible post-state chosen arbitrarily if $*$ plays a
state that is not a possible post-state). Conversely, a CGS $S$ with set
$\Sigma\cup\\{*\\}$ of agents is converted into a non-deterministic CGS with
set $\Sigma$ of agents by taking the possible post-states under a joint move
$m_{\Sigma}$ of the agents in $\Sigma$ to be the set of all post-states of
joint moves in $S$ extending $m_{\Sigma}$. Both conversions clearly preserve
satisfaction of formulae $\phi$ mentioning only agents in $\Sigma$.

### Proof of One-step Tableau Completeness for the AMCDES (Lemma 6.3) with
Finite Sets of Moves

######  Proof B.6.

Similarly to how the finite moves were achieved in the proof of Theorem 5.1,
we will colour the moves to simulate the effect of the occurs check in
unification. We use the same terminology and notation for colours as in the
proof of Theorem 5.1, and take the colours from the same Abelian group $U$.
Let $\phi$ be the clause set constructed in the ongoing proof as shown in the
main part of the paper. Now, all agents receive (for simplicity) the same
moves, namely

  * •

moves $(e^{j},0)$ for $j=1,\dots,\alpha$, intended as witnesses for the moves
of the agents in $D_{j}$ in $\mathop{[D_{j},P_{G_{j}}]}a_{j}$,

  * •

moves $(p,0)$ for $j=1,\dots,\alpha$, $p\in P_{G_{j}}$ witnessing explicit
moves from $\mathop{[D_{j},P_{G_{j}}]}a_{j}$,

  * •

moves $(r,0)$ for $j=1,\dots,\beta$, $r\in R_{H_{j}}$ witnessing explicit
moves from $\mathop{\langle C_{j},R_{H_{j}}\rangle}c_{j}$, and

  * •

moves $(g^{j},u)$ for $j=1,\dots,\beta$ and $u\in U$, intended as witnesses
for $\mathop{\langle C_{j},R_{H_{j}}\rangle}c_{j}$.

Let $\mathcal{T}$ be the unification closure of all argument terms occuring in
clauses in $\phi$. All tuples in $\mathcal{T}$ have the shape
$(x_{A},e_{B},p_{C},r_{D},g_{\,\overline{A\cup B\cup C\cup
D}}(x_{A},e_{B},p_{C},r_{D}))$ where the $x_{A}$ are variables; the $e_{B}$
are Skolem constants and $p_{C}$, $r_{D}$ are constants for named moves, from
possibly different boxes and diamonds; and the $g_{\,\overline{A\cup B\cup
C\cup D}}$ are Skolem functions from a single diamond, as Skolem functions
from multiple diamonds do not occur together in the starting terms and such
occurrences are not introduced during unification due to the occurs check.

The (finite) model $\mathcal{G}$ is then defined over coloured moves. Skolem
constants $e^{j}$ are interpreted as $(e^{j},0)$, explicit strategies $r$ and
$p$ are interpreted as $(r,0)$ and $(p,0)$, and Skolem functions $g_{i}^{j}$
for $i\in\overline{C_{j}}$ are interpreted as mapping a joint move $m_{C_{j}}$
of $C_{j}$ to $(g^{j},u_{j}-\mathsf{col}(m_{C_{j}}))$ if $i$ is the least
element of $\overline{C_{j}}$, and to $(g^{j},0)$ otherwise, thus ensuring
that $\mathsf{col}(m_{C_{j}},g^{j}(m_{C_{j}}))=u_{j}$. It remains to show that
$\mathcal{G}$ is $\mathcal{T}$-equationally complete, obtaining by Theorem 4.8
and consistency of $\phi$ under set-valued first-order resolution that $\phi$
is satisfiable over $\mathcal{G}$. Indeed, observing that the symbols for
explicit strategies represent constants in the unification process and are
translated exactly like the Skolem constants, we can treat them as part of
$e_{B}$ and proceed in the same way as in Theorem 5.1.

  *[AMC]: alternating-time μ-calculus
  *[]:
  *[ATLES]:  with explicit strategies
  *[AMCDES]: alternating-time μ-calculus with disjunctive explicit strategies
  *[CTL]: computation tree logic
  *[ATL]: alternating-time temporal logic
  *[ATL-A]:  with actions
  *[ATLEA]:  with explicit actions
  *[AMCES]:   () with explicit strategies
  *[ATLDES]:  with disjunctive explicit strategies
  *[CGSES]: concurrent game structure with explicit strategies
  *[CGSESs]: concurrent game structure with explicit strategies
  *[CGS]: concurrent game structure
  *[ CGS]: concurrent game structure