$\mathrm{LTS}^{U}$ (i.e., is in $\bm{\mathrm{M}_{\mathrm{AC}}}$);

  2. (2)

for every $\varphi\in\mathsf{L}_{\mathsf{Kh}}$,
$\llbracket\varphi\rrbracket^{\mathcal{S}}=\llbracket\varphi\rrbracket^{\mathcal{M}_{\\_}{\mathcal{S}}}$.

######  Proof..

First, Item (1). For showing that $\mathcal{M}_{\\_}{\mathcal{S}}$ is an
$\mathrm{LTS}^{U}$, note how
$\mathrm{P}^{\prime}=\bigcup_{\\_}{\uppi\in\mathrm{S}^{\prime}}\uppi$ is non-
empty ($\epsilon\in{\rm\sf Act}^{*}$ and $\mathrm{SE}(\epsilon)=\mathrm{W}$,
so $\epsilon\in{\rm\sf Act}^{\prime}$ and hence
$\\{a_{\\_}{\epsilon}\\}\in\mathrm{S}^{\prime}$) and, moreover,
$\mathrm{S}^{\prime}$ does not contain the empty set and its elements are
pairwise disjoint (the latter two by definition). Moreover, we can map
elements from ${\rm\sf Act}^{\prime}$ into ${\rm\sf Act}$ to preserve the same
signature (as their cardinalities match). Activeness is straightforward, as
$\\{a_{\\_}\epsilon\\}$ is in $\mathrm{S}^{\prime}$ and behaves exactly as
$\epsilon$.

For $\mathrm{SE}$-compositionality, take
$\\{a_{\\_}{\sigma_{\\_}1}\\},\\{a_{\\_}{\sigma_{\\_}2}\\}\in\mathrm{S}^{\prime}$
s.t.
$\\{a_{\\_}{\sigma_{\\_}1}\\}\mathbin{\bm{;}}\\{a_{\\_}{\sigma_{\\_}2}\\}\neq\varnothing$.
Then,
$\\{a_{\\_}{\sigma_{\\_}1}\\}\mathbin{\bm{;}}\\{a_{\\_}{\sigma_{\\_}2}\\}=\\{a_{\\_}{\sigma_{\\_}1}a_{\\_}{\sigma_{\\_}2}\\}$
and, moreover, $\mathrm{SE}(\\{a_{\\_}{\sigma_{\\_}1}\\})\neq\varnothing$ and
$\mathrm{R}^{\prime}_{\\_}{\\{a_{\\_}{\sigma_{\\_}1}\\}}(\mathrm{SE}(\\{a_{\\_}{\sigma_{\\_}1}\\}))\subseteq\mathrm{SE}(\\{a_{\\_}{\sigma_{\\_}2}\\})$
($\bm{\otimes_{\\_}1}$). We need to provide a $\uppi\in\mathrm{S}^{\prime}$
satisfying the $\mathrm{SE}$-compositionality conditions; it will be shown
that $\uppi=\\{a_{\\_}{\sigma_{\\_}1\sigma_{\\_}2}\\}$ does the work. In doing
so, it is useful to notice that
$\mathrm{R}^{\prime}_{\\_}{a_{\\_}{\sigma_{\\_}1}a_{\\_}{\sigma_{\\_}2}}=\mathrm{R}^{\prime}_{\\_}{a_{\\_}{\sigma_{\\_}1\sigma_{\\_}2}}$
(the proof is straightforward).

First, we need to show that $\uppi=\\{a_{\\_}{\sigma_{\\_}1\sigma_{\\_}2}\\}$
is in $\mathrm{S}$, which boils down to showing that
$a_{\\_}{\sigma_{\\_}1\sigma_{\\_}2}\in{\rm\sf Act}^{\prime}$, that is,
$\mathrm{SE}(\sigma_{\\_}1\sigma_{\\_}2)\neq\varnothing$. For this, recall
that $\mathrm{SE}(\\{a_{\\_}{\sigma_{\\_}1}\\})\neq\varnothing$, so we know
that $\\{a_{\\_}{\sigma_{\\_}1}\\}$ is strongly executable at some
$u\in\mathrm{W}$. Moreover, from
$\mathrm{R}^{\prime}_{\\_}{\\{a_{\\_}{\sigma_{\\_}1}\\}}(\mathrm{SE}(\\{a_{\\_}{\sigma_{\\_}1}\\}))\subseteq\mathrm{SE}(\\{a_{\\_}{\sigma_{\\_}2}\\})$
it follows that any such execution ends in states where
$a_{\\_}{\sigma_{\\_}2}$ is strongly executable. Then,
$a_{\\_}{\sigma_{\\_}1}a_{\\_}{\sigma_{\\_}2}$ is strongly executable at $u$,
which implies
$\mathrm{R}^{\prime}_{\\_}{a_{\\_}{\sigma_{\\_}1}a_{\\_}{\sigma_{\\_}2}}(u)\neq\varnothing$.
But
$\mathrm{R}^{\prime}_{\\_}{a_{\\_}{\sigma_{\\_}1}a_{\\_}{\sigma_{\\_}2}}=\mathrm{R}^{\prime}_{\\_}{a_{\\_}{\sigma_{\\_}1\sigma_{\\_}2}}$,
so
$\mathrm{R}^{\prime}_{\\_}{a_{\\_}{\sigma_{\\_}1\sigma_{\\_}2}}(u)\neq\varnothing$,
which by definition of $\mathrm{R}^{\prime}$ implies
$u\in\mathrm{SE}(\sigma_{\\_}1\sigma_{\\_}2)$, that is,
$\mathrm{SE}(\sigma_{\\_}1\sigma_{\\_}2)\neq\varnothing$, as required.

Then, the $\mathrm{SE}$-compositionality conditions. The first and the third,
$\mathrm{R}^{\prime}_{\\_}{a_{\\_}{\sigma_{\\_}1}a_{\\_}{\sigma_{\\_}2}}\subseteq\mathrm{R}^{\prime}_{\\_}{a_{\\_}{\sigma_{\\_}1\sigma_{\\_}2}}$
and the bisimilarity one, follow from
$\mathrm{R}^{\prime}_{\\_}{a_{\\_}{\sigma_{\\_}1}a_{\\_}{\sigma_{\\_}2}}=\mathrm{R}^{\prime}_{\\_}{a_{\\_}{\sigma_{\\_}1\sigma_{\\_}2}}$.
For the second,
$\mathrm{SE}(a_{\\_}{\sigma_{\\_}1}a_{\\_}{\sigma_{\\_}2})\subseteq\mathrm{SE}(a_{\\_}{\sigma_{\\_}1\sigma_{\\_}2})$,
take $u\in\mathrm{SE}(a_{\\_}{\sigma_{\\_}1}a_{\\_}{\sigma_{\\_}2})$; we need
to show that $u\in\mathrm{SE}(a_{\\_}{\sigma_{\\_}1\sigma_{\\_}2})$. For this,
it is enough to show that
$\mathrm{R}^{\prime}_{\\_}{a_{\\_}{\sigma_{\\_}1\sigma_{\\_}2}}(u)\neq\varnothing$
(as $a_{\\_}{\sigma_{\\_}1\sigma_{\\_}2}$ is a basic action), i.e., that
$\mathrm{R}_{\\_}{\sigma_{\\_}1\sigma_{\\_}2}(u)\neq\varnothing$ (which
implies $a_{\\_}{\sigma_{\\_}1\sigma_{\\_}2}$ exists) and
$u\in\mathrm{SE}(\sigma_{\\_}1\sigma_{\\_}2)$. Now, the assumption
$u\in\mathrm{SE}(a_{\\_}{\sigma_{\\_}1}a_{\\_}{\sigma_{\\_}2})$ implies
$u\in\mathrm{SE}(a_{\\_}{\sigma_{\\_}1})$ and
$\mathrm{R}^{\prime}_{\\_}{a_{\\_}{\sigma_{\\_}1}}(u)\subseteq\mathrm{SE}(a_{\\_}{\sigma_{\\_}2})$.
The first implies not only
$\mathrm{R}^{\prime}_{\\_}{a_{\\_}{\sigma_{\\_}1}}(u)\neq\varnothing$ (so
$u\in\mathrm{SE}(\sigma_{\\_}1)$) but also
$\mathrm{R}^{\prime}_{\\_}{a_{\\_}{\sigma_{\\_}1}}(u)=\mathrm{R}_{\\_}{\sigma_{\\_}1}(u)$.
From the second and the latter,
$\mathrm{R}_{\\_}{\sigma_{\\_}1}(u)\subseteq\mathrm{SE}(a_{\\_}{\sigma_{\\_}2})$.
But note: $v\in\mathrm{SE}(a_{\\_}{\sigma_{\\_}2})$ implies there is
$v^{\prime}\in\mathrm{R}^{\prime}_{\\_}{a_{\\_}{\sigma_{\\_}2}}(v)$, so
$v\in\mathrm{SE}(\sigma_{\\_}2)$. Thus,
$\mathrm{SE}(a_{\\_}{\sigma_{\\_}2})\subseteq\mathrm{SE}(\sigma_{\\_}2)$ and
hence $\mathrm{R}_{\\_}{\sigma_{\\_}1}(u)\subseteq\mathrm{SE}(\sigma_{\\_}2)$.
Then, the now latter and $u\in\mathrm{SE}(\sigma_{\\_}1)$ imply
$u\in\mathrm{SE}(\sigma_{\\_}1\sigma_{\\_}2)$ (the second goal) and thus, by
definition of $\mathrm{SE}$, it follows that
$\mathrm{R}_{\\_}{\sigma_{\\_}1\sigma_{\\_}2}(u)\neq\varnothing$ (the first
goal).

For Item (2), the proof is by structural induction; again, only the case of
$\mathsf{Kh}(\psi,\varphi)$ is discussed.

$\bm{(\subseteq)}$ Suppose
$w\in\llbracket\mathsf{Kh}(\psi,\varphi)\rrbracket^{\mathcal{S}}$; then there
is $\sigma\in{\rm\sf Act}^{*}$ satisfying both

  1. ($\bm{\mathsf{Kh}}$-1)

$\llbracket\psi\rrbracket^{\mathcal{S}}\subseteq\mathrm{SE}(\sigma)$ and

  2. ($\bm{\mathsf{Kh}}$-2)

$\mathrm{R}_{\\_}\sigma(\llbracket\psi\rrbracket^{\mathcal{S}})\subseteq\llbracket\varphi\rrbracket^{\mathcal{S}}$.

There are two cases. First, assume $\mathrm{SE}(\sigma)=\varnothing$. From
this, ($\bm{\mathsf{Kh}}$-1) implies
$\llbracket\psi\rrbracket^{\mathcal{S}}=\varnothing$, so
$\llbracket\psi\rrbracket^{\mathcal{M}_{\\_}\mathcal{S}}=\varnothing$ (by IH)
and
$\mathrm{R}^{\prime}_{\\_}{\uppi}(\llbracket\psi\rrbracket^{\mathcal{M}_{\\_}\mathcal{S}})=\varnothing$
for any $\uppi\in 2^{({\rm\sf Act}^{\prime})^{*}}$. Hence, to obtain
$w\in\llbracket\mathsf{Kh}(\psi,\varphi)\rrbracket^{\mathcal{M}_{\\_}{\mathcal{S}}}$
it is enough to have $\mathrm{S}^{\prime}\neq\varnothing$, which we do as
$\\{a_{\\_}{\epsilon}\\}\in\mathrm{S}^{\prime}$.

Second, assume $\mathrm{SE}(\sigma)\neq\varnothing$. Then,
$a_{\\_}\sigma\in{\rm\sf Act}^{\prime}$ and
$\\{a_{\\_}\sigma\\}\in\mathrm{S}^{\prime}$; this will be shown to be our
witness. For the first $\mathsf{Kh}$-clause, if
$u\in\llbracket\psi\rrbracket^{\mathcal{M}_{\\_}{\mathcal{S}}}$ then
$u\in\llbracket\psi\rrbracket^{\mathcal{S}}$ (IH), so
$u\in\mathrm{SE}(\sigma)$ (($\bm{\mathsf{Kh}}$-1)), which implies
$\mathrm{R}_{\\_}{\sigma}(u)\neq\varnothing$. The last two together imply
$\mathrm{R}^{\prime}_{\\_}{a_{\\_}{\sigma}}(u)\neq\varnothing$ (definition of
$\mathrm{R}^{\prime}$), so
$u\in\mathrm{SE}(a_{\\_}{\sigma})=\mathrm{SE}(\\{a_{\\_}{\sigma}\\})$. Hence,
$\llbracket\psi\rrbracket^{\mathcal{M}_{\\_}{\mathcal{S}}}\subseteq\mathrm{SE}(\\{a_{\\_}{\sigma}\\})$.
For the second $\mathsf{Kh}$-clause, suppose
$u\in\mathrm{R}^{\prime}_{\\_}{\\{a_{\\_}{\sigma}\\}}(\llbracket\psi\rrbracket^{\mathcal{M}_{\\_}{\mathcal{S}}})$.
Then,
$u\in\mathrm{R}^{\prime}_{\\_}{a_{\\_}\sigma}(\llbracket\psi\rrbracket^{\mathcal{M}_{\\_}\mathcal{S}})$
so
$u\in\mathrm{R}^{\prime}_{\\_}{a_{\\_}\sigma}(\llbracket\psi\rrbracket^{\mathcal{S}})$
(IH) and then
$u\in\mathrm{R}_{\\_}{\sigma}(\llbracket\psi\rrbracket^{\mathcal{S}})$
(definition of $\mathrm{R}^{\prime}$) so, by ($\bm{\mathsf{Kh}}$-2),
$u\in\llbracket\varphi\rrbracket^{\mathcal{S}}$ and thus
$u\in\llbracket\varphi\rrbracket^{\mathcal{M}_{\\_}{\mathcal{S}}}$ (IH).
Consequently,
$\mathrm{R}^{\prime}_{\\_}{\uppi}(\llbracket\psi\rrbracket^{\mathcal{M}_{\\_}{\mathcal{S}}})\subseteq\llbracket\varphi\rrbracket^{\mathcal{M}_{\\_}{\mathcal{S}}}$.
From the two clauses,
$w\in\llbracket\mathsf{Kh}(\psi,\varphi)\rrbracket^{\mathcal{M}_{\\_}{\mathcal{S}}}$.

$\bm{(\supseteq)}$ Suppose
$w\in\llbracket\mathsf{Kh}(\psi,\varphi)\rrbracket^{\mathcal{M}_{\\_}{\mathcal{S}}}$.
Then there is an element of $\mathrm{S}^{\prime}$ fulfilling the
$\mathsf{Kh}$-clauses, which by definition of $\mathrm{S}^{\prime}$ implies
there is $\\{a_{\\_}{\sigma}\\}\in\mathrm{S}^{\prime}$ (with $\sigma\in{\rm\sf
Act}^{*}$) satisfying both

  1. ($\bm{\mathsf{Kh}}$-1)

$\llbracket\psi\rrbracket^{\mathcal{M}_{\\_}{\mathcal{S}}}\subseteq\mathrm{SE}(\\{a_{\\_}{\sigma}\\})$
and

  2. ($\bm{\mathsf{Kh}}$-2)

$\mathrm{R}^{\prime}_{\\_}{\\{a_{\\_}{\sigma}\\}}(\llbracket\psi\rrbracket^{\mathcal{M}_{\\_}{\mathcal{S}}})\subseteq\llbracket\varphi\rrbracket^{\mathcal{M}_{\\_}{\mathcal{S}}}$.

It will be shown that $\sigma$ is our witness. For the first
$\mathsf{Kh}$-clause, $u\in\llbracket\psi\rrbracket^{\mathcal{S}}$ implies
$u\in\llbracket\psi\rrbracket^{\mathcal{M}_{\\_}{\mathcal{S}}}$ (IH), hence
$u\in\mathrm{SE}(\\{a_{\\_}\sigma\\})$ (($\bm{\mathsf{Kh}}$-1)) and then
$\mathrm{R}^{\prime}_{\\_}{a_{\\_}{\sigma}}(u)\neq\varnothing$, which implies
$u\in\mathrm{SE}(\sigma)$ (definition of $\mathrm{R}^{\prime}$). Thus,
$\llbracket\psi\rrbracket^{\mathcal{S}}\subseteq\mathrm{SE}(\sigma)$. For the
second $\mathsf{Kh}$-clause, take
$u\in\mathrm{R}_{\\_}{\sigma}(\llbracket\psi\rrbracket^{\mathcal{S}})$, so
$u\in\mathrm{R}_{\\_}{\sigma}(\llbracket\psi\rrbracket^{\mathcal{M}_{\\_}\mathcal{S}})$
(IH). Then $u\in\mathrm{R}_{\\_}{\sigma}(v)$ for some
$v\in\llbracket\psi\rrbracket^{\mathcal{M}_{\\_}\mathcal{S}}$ By
($\bm{\mathsf{Kh}}$-1), $v\in\mathrm{SE}(\\{a_{\\_}{\sigma}\\})$, i.e.,
$v\in\mathrm{SE}(a_{\\_}{\sigma})$ so
$\mathrm{R}^{\prime}_{\\_}{a_{\\_}\sigma}(v)\neq\varnothing$ and then
$v\in\mathrm{SE}(\sigma)$ (definition of $\mathrm{R}^{\prime}$). This,
together with $u\in\mathrm{R}_{\\_}{\sigma}(v)$ imply
$u\in\mathrm{R}^{\prime}_{\\_}{a_{\\_}\sigma}(v)$, i.e.,
$u\in\mathrm{R}^{\prime}_{\\_}{\\{a_{\\_}\sigma\\}}(v)$. Hence,
$u\in\mathrm{R}^{\prime}_{\\_}{a_{\\_}\sigma}(\llbracket\psi\rrbracket^{\mathcal{M}_{\\_}\mathcal{S}})$,
so $u\in\llbracket\varphi\rrbracket^{\mathcal{M}_{\\_}{\mathcal{S}}}$
(($\bm{\mathsf{Kh}}$-2)) and then
$u\in\llbracket\varphi\rrbracket^{\mathcal{S}}$ (IH). Thus,
$\mathrm{R}_{\\_}{\sigma}(\llbracket\psi\rrbracket^{\mathcal{S}})\subseteq\llbracket\varphi\rrbracket^{\mathcal{S}}$.
From the two clauses,
$w\in\llbracket\mathsf{Kh}(\psi,\varphi)\rrbracket^{\mathcal{S}}$.
$\blacksquare$

$\triangleleft$

From these results, the axiom system for $\mathsf{L}_{\mathsf{Kh}}$ over
$\mathrm{LTS}$ (Table 1) is also sound and complete for
$\mathsf{L}_{\mathsf{Kh}}$ over _active_ and _$\mathrm{SE}$ -compositional_
$\mathrm{LTS}^{U}$s.

######  Theorem 6.

The axiom system $\mathcal{L}^{\mathrm{LTS}}_{\mathsf{Kh}}$ (Table 1) is sound
and strongly complete w.r.t. the class $\bm{\mathrm{M}_{\mathrm{AC}}}$.

######  Proof..

The arguments are exactly as in Theorem 5, by using this time Proposition 13
and Proposition 14.

$\blacksquare$

$\triangleleft$

##  8 Finite model property and complexity

This section is devoted to the study of the computational complexity of the
logic $\mathsf{L}_{\mathsf{Kh}_{i}}$ over $\mathrm{LTS}^{U}$s. To do so, we
will use two standard tools from modal logic: filtration and selection (see,
e.g., [9] for details). First, we define a notion of filtration that, given an
arbitrary model and a formula, allows us to obtain a finite model that
satisfies the formula if and only if the original model satisfies it. This
proves that the satisfiability problem for $\mathsf{L}_{\mathsf{Kh}_{i}}$ is
decidable. Then, we define a (more specialized) selection function which, from
a canonical model, enables us to extract a polynomial-size model. Thus, we
show that the satisfiability problem for $\mathsf{L}_{\mathsf{Kh}_{i}}$ is NP-
complete (given that we provide a model checking algorithm running in P).

###  8.1 Finite model property via filtrations

We start by introducing two relations that will be crucial to define a proper
notion of filtration, given a set of formulas $\Sigma$ and a model
$\mathcal{M}$.

######  Definition 8.1 ($\Sigma$-equivalence).

Let
$\mathcal{M}=\langle\mathrm{W},\mathrm{R},\\{\mathrm{S}_{\\_}i\\}_{\\_}{i\in{\rm\sf
Agt}},\mathrm{V}\rangle$ be an $\mathrm{LTS}^{U}$ and let $\Sigma$ be a set of
$\mathsf{L}_{\mathsf{Kh}_{i}}$-formulas closed under subformulas. Define the
relations
${\mathrel{\leftrightsquigarrow}_{\\_}\Sigma}\subseteq\mathrm{W}\times\mathrm{W}$
and
${\mathrel{\small{\leftrightarrows}}_{\\_}\Sigma}\subseteq\mathrm{S}_{\\_}{\rm\sf
Agt}\times\mathrm{S}_{\\_}{\rm\sf Agt}$ (with $\mathrm{S}_{\\_}{\rm\sf
Agt}:=\bigcup_{\\_}{i\in{\rm\sf Agt}}\mathrm{S}_{\\_}i$) as:

$w\mathrel{\leftrightsquigarrow}_{\\_}\Sigma v$ | $\mbox{\it iff}_{\mbox{\tiny\it def}}$ | for all $\psi\in\Sigma$, $\mathcal{M},w\models\psi$ iff $\mathcal{M},v\models\psi$,
---|---|---
$\uppi\mathrel{\small{\leftrightarrows}}_{\\_}\Sigma\uppi^{\prime}$ | $\mbox{\it iff}_{\mbox{\tiny\it def}}$ | for all $i\in{\rm\sf Agt}$ and $\mathsf{Kh}_{i}(\psi,\varphi)\in\Sigma$, $\uppi$ is a witness
|  | for $\mathsf{Kh}_{i}(\psi,\varphi)$ in $\mathcal{M}$ iff $\uppi^{\prime}$ is a witness for $\mathsf{Kh}_{i}(\psi,\varphi)$ in $\mathcal{M}$.

Notice that $\mathrel{\leftrightsquigarrow}_{\\_}\Sigma$ (a generalisation of
$\mathrel{\leftrightsquigarrow}$ in Definition 5.3 to a given set of formulas)
and $\mathrel{\small{\leftrightarrows}}_{\\_}\Sigma$ are equivalence relations
over $\mathrm{W}$ and $\mathrm{S}_{\\_}{\rm\sf Agt}$, respectively. For
$w\in\mathrm{W}$ (resp., $\uppi\in 2^{({\rm\sf Act}^{*})}$), we use
$[w]_{\\_}\Sigma$ (resp., $[\uppi]_{\\_}\Sigma$) to denote $w$’s (resp.,
$\uppi$’s) $\Sigma$-equivalence class; i.e.,

$[w]_{\\_}\Sigma:=\\{v\in\mathrm{W}\mid
w\mathrel{\leftrightsquigarrow}_{\\_}\Sigma v\\}$;
$[\uppi]_{\\_}\Sigma:=\\{\uppi^{\prime}\in 2^{({\rm\sf
Act}^{*})}\mid\uppi\mathrel{\small{\leftrightarrows}}_{\\_}\Sigma\uppi^{\prime}\\}$.

$\dashv$

Although the notation $[\\_]_{\\_}\Sigma$ is overloaded, its argument will
always disambiguate its use.

######  Definition 8.2.

Let
$\mathcal{M}=\langle\mathrm{W},\mathrm{R},\\{\mathrm{S}_{\\_}i\\}_{\\_}{i\in{\rm\sf
Agt}},\mathrm{V}\rangle$ be an $\mathrm{LTS}^{U}$ and let $\Sigma$ be a set of
$\mathsf{L}_{\mathsf{Kh}_{i}}$-formulas that is closed under subformulas. For
$i\in{\rm\sf Agt}$ define ${\rm\sf
Act}^{\Sigma}_{\\_}i:=\\{a_{\\_}{[\uppi]_{\\_}\Sigma}\mid\uppi\in\mathrm{S}_{\\_}i\text{
is a witness of some }\mathsf{Kh}_{i}(\psi,\varphi)\in\Sigma\text{ in
}\mathcal{M}\\}$; and ${\rm\sf Act}^{\Sigma}:=\bigcup_{\\_}{i\in{\rm\sf
Agt}}{\rm\sf Act}^{\Sigma}_{\\_}i$.

$\dashv$

The idea behind the definition of ${\rm\sf Act}^{\Sigma}$ is that, for each
$\mathsf{Kh}_{i}(\psi,\varphi)\in\Sigma$ that is true at $\mathcal{M}$, we
consider an action mimicking the behaviour of those sets of plans $\uppi$ that
witness the satisfiability of $\mathsf{Kh}_{i}(\psi,\varphi)$ in
$\mathcal{M}$.

Now, we are in position of defining the notion of filtration.

######  Definition 8.3 (Filtration of $\mathcal{M}$ through $\Sigma$).

Let
$\mathcal{M}=\langle\mathrm{W},\mathrm{R},\\{\mathrm{S}_{\\_}i\\}_{\\_}{i\in{\rm\sf
Agt}},\mathrm{V}\rangle$ be an $\mathrm{LTS}^{U}$; let $\Sigma$ be a set of
$\mathsf{L}_{\mathsf{Kh}_{i}}$-formulas that is closed under subformulas. An
$\mathrm{LTS}^{U}$
$\mathcal{M}^{f}=\langle\mathrm{W}^{f},\mathrm{R}^{f},\\{\mathrm{S}^{f}_{\\_}i\\}_{\\_}{i\in{\rm\sf
Agt}},\mathrm{V}^{f}\rangle$ is _a filtration of $\mathcal{M}$ through
$\Sigma$_ if and only if it satisfies the following conditions:

  1. (1)

$\mathrm{W}^{f}:=\\{[w]_{\\_}\Sigma\mid w\in\mathrm{W}\\}$;

  2. (2)

$\mathrm{V}^{f}([w]_{\\_}\Sigma):=\\{p\in\Sigma\mid\mathcal{M},w\models p\\}$;

  3. (3)

for all $i\in{\rm\sf Agt}$, $a_{\\_}{[\uppi]_{\\_}{\Sigma}}\in{\rm\sf
Act}^{\Sigma}_{\\_}i$ implies
$\\{a_{\\_}{[\uppi]_{\\_}{\Sigma}}\\}\in\mathrm{S}^{f}_{\\_}i$;

  4. (4)

$\mathrm{S}_{\\_}i^{f}$ is finite and well-defined (as per Remark 1), and each
$\uppi\in\mathrm{S}^{f}_{\\_}i$ is finite;

  5. (5)

for all $\uppi\in\mathrm{S}^{f}_{\\_}i$, if $\uppi$ is a witness of some
$\mathsf{Kh}_{i}(\psi,\varphi)\in\Sigma$ in $\mathcal{M}^{f}$, then there is
$\uppi^{\prime}\in\mathrm{S}_{\\_}i$ such that $\uppi^{\prime}$ is a witness
of $\mathsf{Kh}_{i}(\psi,\varphi)$ in $\mathcal{M}$;

  6. (6)

if $(w,v)\in\mathrm{R}_{\\_}\uppi$ and $a_{\\_}{[\uppi]_{\\_}\Sigma}\in{\rm\sf
Act}^{\Sigma}_{\\_}i$, then
$([w]_{\\_}\Sigma,[v]_{\\_}\Sigma)\in\mathrm{R}^{f}_{\\_}{a_{\\_}{[\uppi]_{\\_}\Sigma}}$;

  7. (7)

if
$([w]_{\\_}\Sigma,[v]_{\\_}\Sigma)\in\mathrm{R}^{f}_{\\_}{a_{\\_}{[\uppi]_{\\_}\Sigma}}$,
and $\uppi$ is a witness of some $\mathsf{Kh}_{i}(\psi,\varphi)\in\Sigma$ in
$\mathcal{M}$, then $w\in\llbracket\psi\rrbracket^{\mathcal{M}}$ implies
$v\in\llbracket\varphi\rrbracket^{\mathcal{M}}$.

$\dashv$

Note that $\mathrm{V}^{f}$ is well-defined: given $p\in\Sigma$, if
$[w]_{\\_}\Sigma=[v]_{\\_}\Sigma$ and $\mathcal{M},w\models p$, then
$\mathcal{M},v\models p$. Also, as $\mathrm{S}^{f}_{\\_}i$ is well-defined (by
definition), we have that $\mathcal{M}^{f}$ is an $\mathrm{LTS}^{U}$ over
${\rm\sf Act}^{\Sigma}$, ${\rm\sf Prop}$ and ${\rm\sf Agt}$. Also, note that
if (5), (6) and (7) above are turned into if and only if conditions, they
always define an $\mathrm{LTS}^{U}$ which is a filtration.

Definition 8.3 deserves further comments. Notice that, for the $\mathrm{LTS}$
part, the filtration is defined similarly as for the basic modal logic (see,
e.g., [9]). The most significant difference is the change in the labelling of
the relations, since we now use ${\rm\sf Act}^{\Sigma}$ as the set of action
names, instead of ${\rm\sf Act}$. But this has a consequence on the definition
of $\mathrm{S}^{f}_{\\_}i$. The relation
$\mathrel{\small{\leftrightarrows}}_{\\_}\Sigma$ enables us to obtain a finite
set of witnesses for the formulas $\mathsf{Kh}_{i}(\psi,\varphi)\in\Sigma$,
from which we also get that ${\rm\sf Act}^{\Sigma}$ and (together with
$\mathrel{\leftrightsquigarrow}_{\\_}\Sigma$) $\mathrm{W}^{f}$ are finite.
However, the new set $\mathrm{S}^{f}_{\\_}i$ is defined in terms of a new set
of action names, so there are potentially infinite new available plans to
consider. Thus, we need to state that $\mathrm{S}^{f}_{\\_}i$ is any finite
set, satisfying the minimum and maximum conditions, whose members are also
finite, and that is well-defined. Finally, ${\rm\sf Act}^{\Sigma}$ may be
finite, unlike the original set of actions ${\rm\sf Act}$ which is infinite by
definition. However, this poses no problem in the construction, as ${\rm\sf
Act}^{\Sigma}$ can be extended to an infinite set, without breaking the
finiteness of the filtration (recall that the accessibility relation is
defined over a, potentially finite, subset of the set of actions).

######  Theorem 7.

Let
$\mathcal{M}=\langle\mathrm{W},\mathrm{R},\\{\mathrm{S}_{\\_}i\\}_{\\_}{i\in{\rm\sf
Agt}},\mathrm{V}\rangle$ be an $\mathrm{LTS}^{U}$ and let $\Sigma$ be a set of
$\mathsf{L}_{\mathsf{Kh}_{i}}$-formulas that is closed under subformulas.
Then, for all $\psi\in\Sigma$ and $w\in\mathrm{W}$, $\mathcal{M},w\models\psi$
iff $\mathcal{M}^{f},[w]_{\\_}\Sigma\models\psi$. Moreover, if $\Sigma$ is
finite then $\mathcal{M}^{f}$ is a finite model.

######  Proof..

Boolean cases work as expected. So, we will only show that
$\mathcal{M},w\models\mathsf{Kh}_{i}(\psi,\varphi)$ iff
$\mathcal{M}^{f},[w]_{\\_}\Sigma\models\mathsf{Kh}_{i}(\psi,\varphi)$.

$\bm{(\Rightarrow)}$ Suppose that
$\mathcal{M}\models\mathsf{Kh}_{i}(\psi,\varphi)$: let
$\uppi\in\mathrm{S}_{\\_}i$ be such that
$\llbracket\psi\rrbracket^{\mathcal{M}}\subseteq\mathrm{SE}(\uppi)$ and
$\mathrm{R}_{\\_}{\uppi}(\llbracket\psi\rrbracket^{\mathcal{M}})\subseteq\llbracket\varphi\rrbracket^{\mathcal{M}}$.
By definition, $a_{\\_}{[\uppi]_{\\_}\Sigma}\in{\rm\sf Act}^{\Sigma}_{\\_}i$
and therefore, $\\{a_{\\_}{[\uppi]_{\\_}\Sigma}\\}\in\mathrm{S}^{f}_{\\_}i$.
If $\llbracket\psi\rrbracket^{\mathcal{M}^{f}}=\varnothing$, the result
trivially follows. Otherwise, let
$[w]_{\\_}\Sigma\in\llbracket\psi\rrbracket^{\mathcal{M}^{f}}$. By IH,
$w\in\llbracket\psi\rrbracket^{\mathcal{M}}$, and since $\uppi$ is SE at $w$,
$\mathrm{R}_{\\_}{\uppi}(w)\neq\varnothing$. Since $\mathcal{M}^{f}$ is a
filtration, we have that
$\mathrm{R}_{\\_}{a_{\\_}{[\uppi]_{\\_}\Sigma}}(w)\neq\varnothing$ and
$\\{a_{\\_}{[\uppi]_{\\_}\Sigma}\\}$ is SE at $[w]_{\\_}\Sigma$. Thus,
$\llbracket\psi\rrbracket^{\mathcal{M}^{f}}\subseteq\mathrm{SE}(\\{a_{\\_}{[\uppi]_{\\_}\Sigma}\\})$.

Let
$([w]_{\\_}\Sigma,[v]_{\\_}\Sigma)\in\mathrm{R}^{f}_{\\_}{a_{\\_}{[\uppi]_{\\_}\Sigma}}$
be such that $[w]_{\\_}\Sigma\in\llbracket\psi\rrbracket^{\mathcal{M}^{f}}$.
By IH, $w\in\llbracket\psi\rrbracket^{\mathcal{M}}$. Since $\uppi$ is a
witness of $\mathsf{Kh}_{i}(\psi,\varphi)\in\Sigma$ in $\mathcal{M}$ (by
assumption), by the definition of $\mathcal{M}^{f}$ we get
$v\in\llbracket\varphi\rrbracket^{\mathcal{M}}$. Again, by IH,
$[v]_{\\_}\Sigma\in\llbracket\varphi\rrbracket^{\mathcal{M}}$. Thus,
$\mathrm{R}^{f}_{\\_}{\\{a_{\\_}{[\uppi]_{\\_}\Sigma}\\}}(\llbracket\psi\rrbracket^{\mathcal{M}})\subseteq\llbracket\varphi\rrbracket^{\mathcal{M}}$.
Therefore, $\mathcal{M}^{f}\models\mathsf{Kh}_{i}(\psi,\varphi)$.

$\bm{(\Leftarrow)}$ Suppose that
$\mathcal{M}^{f}\models\mathsf{Kh}_{i}(\psi,\varphi)$: let
$\uppi\in\mathrm{S}^{f}_{\\_}i$ be such that
$\llbracket\psi\rrbracket^{\mathcal{M}^{f}}\subseteq\mathrm{SE}(\uppi)$ and
$\mathrm{R}_{\\_}{\uppi}(\llbracket\psi\rrbracket^{\mathcal{M}^{f}})\subseteq\llbracket\varphi\rrbracket^{\mathcal{M}^{f}}$.
By definition of $\mathcal{M}^{f}$, since $\uppi$ is a witness of
$\mathsf{Kh}_{i}(\psi,\varphi)\in\Sigma$ in $\mathcal{M}^{f}$, we have that
there is $\uppi^{\prime}\in\mathrm{S}_{\\_}i$ such that $\uppi^{\prime}$ is a
witness of $\mathsf{Kh}_{i}(\psi,\varphi)$ in $\mathcal{M}$. Thus,
$\mathcal{M}\models\mathsf{Kh}_{i}(\psi,\varphi)$.

It remains to show that $\mathcal{M}^{f}$ is finite. First, note that the
number of elements in $\mathrm{W}^{f}$ is $2^{m}$, with $m$ being the number
of formulas in $\Sigma$. By definition, for all $i\in{\rm\sf Agt}$, ${\rm\sf
Act}^{\Sigma}_{\\_}i$ is at most the number of
$\mathsf{Kh}_{i}(\psi,\varphi)\in\Sigma$, since if there are two groups of
witnesses $[\uppi]_{\\_}\Sigma$ and $[\uppi^{\prime}]_{\\_}\Sigma$ for some
$\mathsf{Kh}_{i}(\psi,\varphi)$,
$[\uppi]_{\\_}\Sigma=[\uppi^{\prime}]_{\\_}\Sigma$. Hence, ${\rm\sf
Act}^{\Sigma}$ is polynomial in the number of $\mathsf{Kh}_{i}(\psi,\varphi)$
in $\Sigma$. Finally, by definition, $\mathrm{S}^{f}_{\\_}i$ is finite. Thus,
$\mathcal{M}^{f}$ is finite. $\blacksquare$

$\triangleleft$

The last theorem states that every satisfiable formula of
$\mathsf{L}_{\mathsf{Kh}_{i}}$, is satisfiable in a finite model. As a
consequence, the satisfiability problem for $\mathsf{L}_{\mathsf{Kh}_{i}}$ is
decidable. In the next section we will refine this result and provide exact
complexity bounds.

###  8.2 Complexity via selection

Here we investigate the computational complexity of the satisfiability problem
of $\mathsf{L}_{\mathsf{Kh}_{i}}$ under the $\mathrm{LTS}^{U}$-based
semantics. We will establish membership in NP by showing a polynomial-size
model property.

Given a formula, we will show that it is possible to select just a piece of
the canonical model which is relevant for its evaluation. The selected model
will preserve satisfiability, and moreover, its size will be polynomial w.r.t.
the size of the input formula.

######  Definition 8.4 (Selection function).

Let
$\mathcal{M}^{\Gamma}=\langle\mathrm{W}^{\Gamma},\mathrm{R}^{\Gamma},\\{\mathrm{S}_{\\_}i^{\Gamma}\\}_{\\_}{i\in{\rm\sf
Agt}},\mathrm{V}^{\Gamma}\rangle$ be a canonical model for an MCS $\Gamma$
(see Definition 6.1); take $w\in\mathrm{W}^{\Gamma}$ and a formula
$\varphi\in\mathsf{L}_{\mathsf{Kh}_{i}}$. Define ${\rm\sf
Act}_{\\_}\varphi:=\\{\langle\theta_{\\_}1,\theta_{\\_}2\rangle\in{\rm\sf
Act}^{\Gamma}\mid\mathsf{Kh}_{\\_}i(\theta_{\\_}1,\theta_{\\_}2)\text{ is a
subformula of }\varphi\\}$. A _canonical selection function_
$\mathsf{sel}^{\varphi}_{\\_}{w}$ is a function that takes
$\mathcal{M}^{\Gamma}$, $w$ and $\varphi$ as input, returns a set
$\mathrm{W}^{\prime}\subseteq\mathrm{W}^{\Gamma}$, and is such that:

  1. (1)

$\mathsf{sel}^{\varphi}_{\\_}{w}(p)=\\{w\\}$;

  2. (2)

$\mathsf{sel}^{\varphi}_{\\_}{w}(\neg\varphi_{\\_}1)=\mathsf{sel}^{\varphi}_{\\_}w(\varphi_{\\_}1)$

  3. (3)

$\mathsf{sel}^{\varphi}_{\\_}{w}(\varphi_{\\_}1\vee\varphi_{\\_}2)=\mathsf{sel}^{\varphi}_{\\_}{w}(\varphi_{\\_}1)\cup\mathsf{sel}^{\varphi}_{\\_}{w}(\varphi_{\\_}2)$;

  4. (4)

If
$\llbracket\mathsf{Kh}_{\\_}i(\varphi_{\\_}1,\varphi_{\\_}2)\rrbracket^{\mathcal{M}^{\Gamma}}\neq\varnothing\text{
and }\llbracket\varphi_{\\_}1\rrbracket^{\mathcal{M}^{\Gamma}}=\varnothing$:
$\mathsf{sel}^{\varphi}_{\\_}{w}(\mathsf{Kh}_{\\_}i(\varphi_{\\_}1,\varphi_{\\_}2))=\\{w\\}$;

  5. (5)

If
$\llbracket\mathsf{Kh}_{\\_}i(\varphi_{\\_}1,\varphi_{\\_}2)\rrbracket^{\mathcal{M}^{\Gamma}}\neq\varnothing\text{
and
}\llbracket\varphi_{\\_}1\rrbracket^{\mathcal{M}^{\Gamma}}\neq\varnothing$:

$\mathsf{sel}^{\varphi}_{\\_}{w}(\mathsf{Kh}_{\\_}i(\varphi_{\\_}1,\varphi_{\\_}2))=\\{w_{\\_}1,w_{\\_}2\\}\cup\mathsf{sel}^{\varphi}_{\\_}{w_{\\_}1}(\varphi_{\\_}1)\cup\mathsf{sel}^{\varphi}_{\\_}{w_{\\_}2}(\varphi_{\\_}2)$,
where $w_{\\_}1$, $w_{\\_}2$ are s.t.
$(w_{\\_}1,w_{\\_}2)\in\mathrm{R}^{\Gamma}_{\\_}{\langle\varphi_{\\_}1,\varphi_{\\_}2\rangle}$;

  6. (6)

If
$\llbracket\mathsf{Kh}_{\\_}i(\varphi_{\\_}1,\varphi_{\\_}2)\rrbracket^{\mathcal{M}^{\Gamma}}=\varnothing$
(note that
$\llbracket\varphi_{\\_}1\rrbracket^{\mathcal{M}^{\Gamma}}\neq\varnothing$):

For all set of plans $\uppi$, either
$\llbracket\varphi_{\\_}1\rrbracket^{\mathcal{M}^{\Gamma}}\not\subseteq\mathrm{SE}(\uppi)$
or
$\mathrm{R}_{\\_}\uppi^{\Gamma}(\llbracket\varphi_{\\_}1\rrbracket^{\mathcal{M}^{\Gamma}})\not\subseteq\llbracket\varphi_{\\_}2\rrbracket^{\mathcal{M}^{\Gamma}}$.
For each $a\in{\rm\sf Act}_{\\_}\varphi$:

    1. (a)

if
$\llbracket\varphi_{\\_}1\rrbracket^{\mathcal{M}^{\Gamma}}\not\subseteq\mathrm{SE}(\\{a\\})$:
we add
$\\{w_{\\_}1\\}\cup\mathsf{sel}^{\varphi}_{\\_}{w_{\\_}1}(\varphi_{\\_}1)$ to
$\mathsf{sel}^{\varphi}_{\\_}{w}(\mathsf{Kh}_{\\_}i(\varphi_{\\_}1,\varphi_{\\_}2))$,
where $w_{\\_}1\in\llbracket\varphi_{\\_}1\rrbracket^{\mathcal{M}^{\Gamma}}$
and $w_{\\_}1\notin\mathrm{SE}(\\{a\\})$;

    2. (b)

if
$\mathrm{R}_{\\_}\uppi^{\Gamma}(\llbracket\varphi_{\\_}1\rrbracket^{\mathcal{M}^{\Gamma}})\not\subseteq\llbracket\varphi_{\\_}2\rrbracket^{\mathcal{M}^{\Gamma}}$
we add
$\\{w_{\\_}1,w_{\\_}2\\}\cup\mathsf{sel}^{\varphi}_{\\_}{w_{\\_}1}(\varphi_{\\_}1)\cup\mathsf{sel}^{\varphi}_{\\_}{w_{\\_}2}(\varphi_{\\_}2)$
to
$\mathsf{sel}^{\varphi}_{\\_}{w}(\mathsf{Kh}_{\\_}i(\varphi_{\\_}1,\varphi_{\\_}2))$,
where $w_{\\_}1\in\llbracket\varphi_{\\_}1\rrbracket^{\mathcal{M}^{\Gamma}}$,
$w_{\\_}2\in\mathrm{R}^{\Gamma}_{\\_}a(w_{\\_}1)$ and
$w_{\\_}2\notin\llbracket\varphi_{\\_}2\rrbracket^{\mathcal{M}^{\Gamma}}$.

$\dashv$

We can now select a small model which preserves the satisfiability of a given
formula.

######  Definition 8.5 (Selected model).

Let $\mathcal{M}^{\Gamma}$ be the canonical model for an MCS $\Gamma$, $w$ a
state in $\mathcal{M}^{\Gamma}$, and $\varphi$ an
$\mathsf{L}_{\mathsf{Kh}_{i}}$-formula. Let $\mathsf{sel}^{\varphi}_{\\_}w$ be
a selection function, we define the _model selected by_
$\mathsf{sel}^{\varphi}_{\\_}w$ as
$\mathcal{M}^{\varphi}_{\\_}w=\langle\mathrm{W}^{\varphi}_{\\_}w,\mathrm{R}^{\varphi}_{\\_}w,\\{(\mathrm{S}^{\varphi}_{\\_}w)_{\\_}i\\}_{\\_}{i\in{\rm\sf
Agt}},\mathrm{V}^{\varphi}_{\\_}w\rangle$, where

  * •

$\mathrm{W}^{\varphi}_{\\_}w:=\mathsf{sel}^{\varphi}_{\\_}w(\varphi)$;

  * •

$(\mathrm{R}^{\varphi}_{\\_}w)_{\\_}{\langle\theta_{\\_}1,\theta_{\\_}2\rangle}:=\mathrm{R}^{\Gamma}_{\\_}{\langle\theta_{\\_}1,\theta_{\\_}2\rangle}\cap(\mathrm{W}^{\varphi}_{\\_}w)^{2}$
for each $\langle\theta_{\\_}1,\theta_{\\_}2\rangle\in{\rm\sf
Act}_{\\_}\varphi$;

  * •

$(\mathrm{S}^{\varphi}_{\\_}w)_{\\_}i:=\\{\\{a\\}\ |\ a\in{\rm\sf
Act}_{\\_}\varphi\\}\cup\\{\\{\langle\bot,\top\rangle\\}\\}$, for $i\in{\rm\sf
Agt}$ (and
$(\mathrm{R}^{\varphi}_{\\_}w)_{\\_}{\langle\bot,\top\rangle}:=\varnothing$);

  * •

$\mathrm{V}^{\varphi}_{\\_}w$ is the restriction of $\mathrm{V}^{\Gamma}$ to
$\mathrm{W}^{\varphi}_{\\_}w$.

$\dashv$

Note that, although ${\rm\sf Act}_{\\_}\varphi$ can be an empty set, each
collection of sets of plans $(\mathrm{S}^{\varphi}_{\\_}w)_{\\_}i$ is not.
Moreover, ${\rm\sf Act}_{\\_}\varphi$ can be extended to an infinite set of
actions, to be defined over a proper signature. Therefore,
$\mathcal{M}^{\varphi}_{\\_}w$ is an $\mathrm{LTS}^{U}$.

######  Proposition 15.

Let $\mathcal{M}^{\Gamma}$ be a canonical model, $w$ a state in
$\mathcal{M}^{\Gamma}$ and $\varphi$ an
$\mathsf{L}_{\mathsf{Kh}_{i}}$-formula. Let $\mathcal{M}^{\varphi}_{\\_}w$ be
the selected model by a selection function $\mathsf{sel}^{\varphi}_{\\_}w$.
Then, $\mathcal{M}^{\Gamma},w\models\varphi$ implies that for all $\psi$
subformula of $\varphi$, and for all $v\in\mathrm{W}^{\varphi}_{\\_}w$ we have
that $\mathcal{M}^{\Gamma},v\models\psi$ iff
$\mathcal{M}^{\varphi}_{\\_}w,v\models\psi$. Moreover,
$\mathcal{M}^{\varphi}_{\\_}w$ is polynomial on the size of $\varphi$.

######  Proof..

The proof proceeds by induction in the size of the formula:

Case $\psi=p$: if $\mathcal{M}^{\Gamma},v\models p$, then
$p\in\mathrm{V}^{\Gamma}(v)$. Given that $v\in\mathrm{W}^{\varphi}_{\\_}w$, we
have $p\in\mathrm{V}^{\varphi}_{\\_}w(v)$ and therefore
$\mathcal{M}^{\varphi}_{\\_}w,v\models p$. The other direction is similar.

Case $\psi=\neg\psi_{\\_}1$: if
$\mathcal{M}^{\Gamma},w\models\neg\psi_{\\_}1$, then
$\mathcal{M}^{\Gamma},w\not\models\psi_{\\_}1$. By IH,
$\mathcal{M}^{\varphi}_{\\_}w,w\not\models\psi_{\\_}1$ and therefore
$\mathcal{M}^{\varphi}_{\\_}w,w\models\neg\psi_{\\_}1$. The other direction is
similar.

Case $\psi=\psi_{\\_}1\vee\psi_{\\_}2$: if
$\mathcal{M}^{\Gamma},v\models\psi_{\\_}1\vee\psi_{\\_}2$, then
$\mathcal{M}^{\Gamma},v\models\psi_{\\_}1$ or
$\mathcal{M}^{\Gamma},v\models\psi_{\\_}2$. By IH,
$\mathcal{M}^{\varphi}_{\\_}w,v\models\psi_{\\_}1$ or
$\mathcal{M}^{\varphi}_{\\_}w,v\models\psi_{\\_}2$ and therefore
$\mathcal{M}^{\varphi}_{\\_}w,v\models\psi_{\\_}1\vee\psi_{\\_}2$. The other
direction is similar.

Case $\psi=\mathsf{Kh}_{\\_}i(\psi_{\\_}1,\psi_{\\_}2)$: Suppose that
$\mathcal{M}^{\Gamma},v\models\mathsf{Kh}_{\\_}i(\psi_{\\_}1,\psi_{\\_}2)$. We
consider two possibilities:

  * •

$\bm{\llbracket\psi_{\\_}1\rrbracket^{\mathcal{M}^{\Gamma}}=\varnothing}$.
Since
$\mathcal{M}^{\Gamma},v\models\mathsf{Kh}_{\\_}i(\psi_{\\_}1,\psi_{\\_}2)$
there is a $\uppi\in\mathrm{S}^{\Gamma}_{\\_}i$ s.t.
$\varnothing=\llbracket\psi_{\\_}1\rrbracket^{\mathcal{M}^{\Gamma}}\subseteq\mathrm{SE}^{\mathcal{M}^{\Gamma}}(\uppi)$
and
$\varnothing=\mathrm{R}^{\Gamma}_{\\_}\uppi(\llbracket\psi_{\\_}1\rrbracket^{\mathcal{M}^{\Gamma}})\subseteq\llbracket\psi_{\\_}2\rrbracket^{\mathcal{M}^{\Gamma}}$.
By IH
$\llbracket\psi_{\\_}1\rrbracket^{\mathcal{M}^{\varphi}_{\\_}w}\subseteq\llbracket\psi_{\\_}1\rrbracket^{\mathcal{M}^{\Gamma}}$.
Notice that, since
$\llbracket\psi_{\\_}1\rrbracket^{\mathcal{M}^{\Gamma}}=\varnothing$, we also
have
$\llbracket\psi_{\\_}1\rrbracket^{\mathcal{M}^{\varphi}_{\\_}w}=\varnothing$.
Let $\uppi^{\prime}=\\{\langle\bot,\top\rangle\\}$, we know that
$\uppi^{\prime}\in(\mathrm{S}^{\varphi}_{\\_}w)_{\\_}i$, and
$(\mathrm{R}^{\varphi}_{\\_}w)_{\\_}{\uppi^{\prime}}(\llbracket\psi_{\\_}1\rrbracket^{\mathcal{M}^{\varphi}_{\\_}w})=\varnothing$.
So, there is a $\uppi^{\prime}\in(\mathrm{S}^{\varphi}_{\\_}w)_{\\_}i$ s.t.
$\llbracket\psi_{\\_}1\rrbracket^{\mathcal{M}^{\varphi}_{\\_}w}\subseteq\mathrm{SE}^{\mathcal{M}^{\varphi}_{\\_}w}(\uppi^{\prime})$
and
$(\mathrm{R}^{\varphi}_{\\_}w)_{\\_}{\uppi^{\prime}}(\llbracket\psi_{\\_}1\rrbracket^{\mathcal{M}^{\varphi}_{\\_}w})\subseteq\llbracket\psi_{\\_}2\rrbracket^{\mathcal{M}}$.
Therefore,
$\mathcal{M}^{\varphi}_{\\_}w,v\models\mathsf{Kh}_{\\_}i(\psi_{\\_}1,\psi_{\\_}2)$.

  * •

$\bm{\llbracket\psi_{\\_}1\rrbracket^{\mathcal{M}^{\Gamma}}\neq\varnothing}$:
since
$\mathcal{M}^{\Gamma},v\models\mathsf{Kh}_{\\_}i(\psi_{\\_}1,\psi_{\\_}2)$
there exists a $\uppi\in\mathrm{S}^{\Gamma}_{\\_}i$ s.t.
$\llbracket\psi_{\\_}1\rrbracket^{\mathcal{M}^{\Gamma}}\subseteq\mathrm{SE}^{\mathcal{M}^{\Gamma}}(\uppi)$
and
$\mathrm{R}^{\Gamma}_{\\_}\uppi(\llbracket\psi_{\\_}1\rrbracket^{\mathcal{M}^{\Gamma}})\subseteq\llbracket\psi_{\\_}2\rrbracket^{\mathcal{M}^{\Gamma}}$.
By Truth Lemma, $\mathsf{Kh}_{\\_}i(\psi_{\\_}1,\psi_{\\_}2)\in v$, then
$\mathsf{Kh}_{\\_}i(\psi_{\\_}1,\psi_{\\_}2)\in\Gamma$ and
$\langle\psi_{\\_}1,\psi_{\\_}2\rangle\in{\rm\sf Act}_{\\_}\Gamma$. By the
definition of
$\mathrm{R}^{\Gamma}_{\\_}{\langle\psi_{\\_}1,\psi_{\\_}2\rangle}$, we have
that for all $w\in\llbracket\psi_{\\_}1\rrbracket^{\mathcal{M}^{\Gamma}}$, it
holds that
$\mathrm{R}^{\Gamma}_{\\_}{\langle\psi_{\\_}1,\psi_{\\_}2\rangle}(w)\neq\varnothing$
and
$\mathrm{R}^{\Gamma}_{\\_}{\langle\psi_{\\_}1,\psi_{\\_}2\rangle}(w)\subseteq\llbracket\psi_{\\_}2\rrbracket^{\mathcal{M}^{\Gamma}}$.
Thus,
$\llbracket\psi_{\\_}1\rrbracket^{\mathcal{M}^{\Gamma}}\subseteq\mathrm{SE}^{\mathcal{M}^{\Gamma}}(\\{\langle\psi_{\\_}1,\psi_{\\_}2\rangle\\})$
and
$\mathrm{R}^{\Gamma}_{\\_}{\langle\psi_{\\_}1,\psi_{\\_}2\rangle}(\llbracket\psi_{\\_}1\rrbracket^{\mathcal{M}^{\Gamma}})\subseteq\llbracket\psi_{\\_}2\rrbracket^{\mathcal{M}^{\Gamma}}$.
Since $\llbracket\psi_{\\_}1\rrbracket^{\mathcal{M}^{\Gamma}}\neq\varnothing$,
there exist $w_{\\_}1,w_{\\_}2\in\mathrm{W}^{\Gamma}$ s.t.
$(w_{\\_}1,w_{\\_}2)\in\mathrm{R}^{\Gamma}_{\\_}{\langle\psi_{\\_}1,\psi_{\\_}2\rangle}$.

Notice that by definition of $\mathcal{M}^{\varphi}_{\\_}w$, we have that
$\\{\langle\psi_{\\_}1,\psi_{\\_}2\rangle\\}\in(\mathrm{S}^{\varphi}_{\\_}w)_{\\_}i$
and that
$(\mathrm{R}^{\varphi}_{\\_}w)_{\\_}{\langle\psi_{\\_}1,\psi_{\\_}2\rangle}$
is defined. Also, by the definition of $\mathsf{sel}^{\varphi}_{\\_}{w}$, Item
(5), there exist
$w^{\prime}_{\\_}1,w^{\prime}_{\\_}2\in\mathrm{W}^{\varphi}_{\\_}w$ s.t.
$(w^{\prime}_{\\_}1,w^{\prime}_{\\_}2)\in(\mathrm{R}^{\varphi}_{\\_}w)_{\\_}{\langle\psi_{\\_}1,\psi_{\\_}2\rangle}$.
Let
$v_{\\_}1\in\llbracket\psi_{\\_}1\rrbracket^{\mathcal{M}^{\varphi}_{\\_}w}$
$\subseteq\llbracket\psi_{\\_}1\rrbracket^{\mathcal{M}^{\Gamma}}$ (the
inclusion holds by IH). Then, we have
$v_{\\_}1\in\mathrm{SE}^{\mathcal{M}^{\Gamma}}(\\{\langle\psi_{\\_}1,\psi_{\\_}2\rangle\\})$
and
$\mathrm{R}^{\Gamma}_{\\_}{\langle\psi_{\\_}1,\psi_{\\_}2\rangle}(v_{\\_}1)\subseteq\llbracket\psi_{\\_}2\rrbracket^{\mathcal{M}^{\Gamma}}$.
Since for all
$v_{\\_}2\in\mathrm{R}^{\Gamma}_{\\_}{\langle\psi_{\\_}1,\psi_{\\_}2\rangle}(v_{\\_}1)$,
we have $v_{\\_}2\in\llbracket\psi_{\\_}2\rrbracket^{\mathcal{M}^{\Gamma}}$,
(in particular $v_{\\_}2=w^{\prime}_{\\_}2$), then
$w^{\prime}_{\\_}2\in(\mathrm{R}^{\varphi}_{\\_}w)_{\\_}{\langle\psi_{\\_}1,\psi_{\\_}2\rangle}(v_{\\_}1)$.
Thus,
$v_{\\_}1\in\mathrm{SE}^{\mathcal{M}^{\varphi}_{\\_}w}(\\{\langle\psi_{\\_}1,\psi_{\\_}2\rangle\\})$.

Aiming for a contradiction, suppose now that
$(\mathrm{R}^{\varphi}_{\\_}w)_{\\_}{\langle\psi_{\\_}1,\psi_{\\_}2\rangle}(v_{\\_}1)=\mathrm{R}^{\Gamma}_{\\_}{\langle\psi_{\\_}1,\psi_{\\_}2\rangle}(v_{\\_}1)\cap\mathrm{W}^{\varphi}_{\\_}w\not\subseteq\llbracket\psi_{\\_}2\rrbracket^{\mathcal{M}^{\varphi}_{\\_}w}$;
and let
$v_{\\_}2\in(\mathrm{R}^{\varphi}_{\\_}w)_{\\_}{\langle\psi_{\\_}1,\psi_{\\_}2\rangle}(v_{\\_}1)$
s.t.
$v_{\\_}2\not\in\llbracket\psi_{\\_}2\rrbracket^{\mathcal{M}^{\varphi}_{\\_}w}$.
Then we have that
$(\mathrm{R}^{\varphi}_{\\_}w)_{\\_}{\langle\psi_{\\_}1,\psi_{\\_}2\rangle}(v_{\\_}1)\subseteq\mathrm{R}^{\Gamma}_{\\_}{\langle\psi_{\\_}1,\psi_{\\_}2\rangle}(v_{\\_}1)$,
but also by IH
$v_{\\_}2\not\in\llbracket\psi_{\\_}2\rrbracket^{\mathcal{M}^{\Gamma}}$. Thus,
$\mathcal{M}^{\Gamma},v\not\models\mathsf{Kh}_{\\_}i(\psi_{\\_}1,\psi_{\\_}2)$,
which is a contradiction. Then, it must be the case that
$(\mathrm{R}^{\varphi}_{\\_}w)_{\\_}{\\{\langle\psi_{\\_}1,\psi_{\\_}2\rangle\\}}(v_{\\_}1)\subseteq\llbracket\psi_{\\_}2\rrbracket^{\mathcal{M}^{\varphi}_{\\_}w}$.
Since we showed that
$\llbracket\psi_{\\_}1\rrbracket^{\mathcal{M}^{\varphi}_{\\_}w}\subseteq\mathrm{SE}^{\mathcal{M}^{\varphi}_{\\_}w}(\\{\langle\psi_{\\_}1,\psi_{\\_}2\rangle\\})$
and
$(\mathrm{R}^{\varphi}_{\\_}w)_{\\_}{\\{\langle\psi_{\\_}1,\psi_{\\_}2\rangle\\}}(\llbracket\psi_{\\_}1\rrbracket^{\mathcal{M}^{\varphi}_{\\_}w})\subseteq\llbracket\psi_{\\_}2\rrbracket^{\mathcal{M}^{\varphi}_{\\_}w}$,
we conclude
$\mathcal{M}^{\varphi}_{\\_}w,v\models\mathsf{Kh}_{\\_}i(\psi_{\\_}1,\psi_{\\_}2)$.

Assume now
$\mathcal{M}^{\varphi}_{\\_}w,v\models\mathsf{Kh}_{\\_}i(\psi_{\\_}1,\psi_{\\_}2)$.
Again, we consider two possibilities:

  * •

$\bm{\llbracket\psi_{\\_}1\rrbracket^{\mathcal{M}^{\varphi}_{\\_}w}=\varnothing}$:
since
$\mathcal{M}^{\varphi}_{\\_}w,v\models\mathsf{Kh}_{\\_}i(\psi_{\\_}1,\psi_{\\_}2)$,
then
$\varnothing=\llbracket\psi_{\\_}1\rrbracket^{\mathcal{M}^{\varphi}_{\\_}w}\subseteq\mathrm{SE}^{\mathcal{M}^{\varphi}_{\\_}w}(\uppi^{\prime})$
and
$\varnothing=(\mathrm{R}^{\varphi}_{\\_}w)_{\\_}{\uppi^{\prime}}(\llbracket\psi_{\\_}1\rrbracket^{\mathcal{M}^{\varphi}_{\\_}w})\subseteq\llbracket\psi_{\\_}2\rrbracket^{\mathcal{M}^{\varphi}_{\\_}w}$
for some $\uppi^{\prime}\in(\mathrm{S}^{\varphi}_{\\_}w)_{\\_}i$. We claim
that $\llbracket\psi_{\\_}1\rrbracket^{\mathcal{M}^{\Gamma}}=\varnothing$.
Because otherwise if
$\mathcal{M}^{\Gamma},v\models\mathsf{Kh}_{\\_}i(\psi_{\\_}1,\psi_{\\_}2)$, by
$\mathsf{sel}^{\varphi}_{\\_}{w}$, Item (5),
$\varnothing\neq(\mathrm{R}^{\varphi}_{\\_}w)_{\\_}{\langle\psi_{\\_}1,\psi_{\\_}2\rangle}$
is defined and
$\llbracket\psi_{\\_}1\rrbracket^{\mathcal{M}^{\varphi}_{\\_}w}\neq\varnothing$,
contradicting hypothesis. And if
$\mathcal{M}^{\Gamma},v\not\models\mathsf{Kh}_{\\_}i(\psi_{\\_}1,\psi_{\\_}2)$,
by $\mathsf{sel}^{\varphi}_{\\_}{w}$, item Item (6), and IH,
$\llbracket\psi_{\\_}1\rrbracket^{\mathcal{M}^{\varphi}_{\\_}w}\neq\varnothing$,
again a contradiction.

Let $\uppi$ be any set of plans in $\mathrm{S}^{\Gamma}_{\\_}i$; since
$\mathrm{R}^{\Gamma}_{\\_}\uppi(\llbracket\psi_{\\_}1\rrbracket^{\mathcal{M}^{\Gamma}})=\varnothing$,
$\llbracket\psi_{\\_}1\rrbracket^{\mathcal{M}^{\Gamma}}\subseteq\mathrm{SE}(\uppi)$
and
$\mathrm{R}^{\Gamma}_{\\_}\uppi(\llbracket\psi_{\\_}1\rrbracket^{\mathcal{M}^{\Gamma}})\subseteq\llbracket\psi_{\\_}2\rrbracket^{\mathcal{M}^{\Gamma}}$.
Then,
$\mathcal{M}^{\Gamma},v\models\mathsf{Kh}_{\\_}i(\psi_{\\_}1,\psi_{\\_}2)$.

  * •

$\bm{\llbracket\psi_{\\_}1\rrbracket^{\mathcal{M}^{\varphi}_{\\_}w}\neq\varnothing}$:
first, notice that by IH,
$\llbracket\psi_{\\_}1\rrbracket^{\mathcal{M}^{\Gamma}}\neq\varnothing$. Also,
by
$\mathcal{M}^{\varphi}_{\\_}w,v\models\mathsf{Kh}_{\\_}i(\psi_{\\_}1,\psi_{\\_}2)$,
we get
$\llbracket\psi_{\\_}1\rrbracket^{\mathcal{M}^{\varphi}_{\\_}w}\subseteq\mathrm{SE}^{\mathcal{M}^{\varphi}_{\\_}w}(\uppi^{\prime})$
and
$(\mathrm{R}^{\varphi}_{\\_}w)_{\\_}{\uppi^{\prime}}(\llbracket\psi_{\\_}1\rrbracket^{\mathcal{M}^{\varphi}_{\\_}w})\subseteq\llbracket\psi_{\\_}2\rrbracket^{\mathcal{M}^{\varphi}_{\\_}w}$,
for some $\uppi^{\prime}\in(\mathrm{S}^{\varphi}_{\\_}w)_{\\_}i$. Aiming for a
contradiction, suppose
$\mathcal{M}^{\Gamma},v\not\models\mathsf{Kh}_{\\_}i(\psi_{\\_}1,\psi_{\\_}2)$.
This implies that for all $\uppi\in\mathrm{S}^{\Gamma}_{\\_}i$,
$\llbracket\psi_{\\_}1\rrbracket^{\mathcal{M}^{\Gamma}}\not\subseteq\mathrm{SE}^{\mathcal{M}^{\Gamma}}(\uppi)$
or
$\mathrm{R}^{\Gamma}_{\\_}\uppi(\llbracket\psi_{\\_}1\rrbracket^{\mathcal{M}^{\Gamma}})\not\subseteq\llbracket\psi_{\\_}2\rrbracket^{\mathcal{M}^{\Gamma}}$.
Also, by definition of ${\rm\sf Act}_{\\_}\varphi$ we have that for all
$\uppi=\\{a\\}\in(\mathrm{S}^{\varphi}_{\\_}w)_{\\_}i$, with $a\in{\rm\sf
Act}_{\\_}\varphi$,
$\llbracket\psi_{\\_}1\rrbracket^{\mathcal{M}^{\Gamma}}\not\subseteq\mathrm{SE}^{\mathcal{M}^{\Gamma}}(\uppi)$
or
$\mathrm{R}^{\Gamma}_{\\_}\uppi(\llbracket\psi_{\\_}1\rrbracket^{\mathcal{M}^{\Gamma}})\not\subseteq\llbracket\psi_{\\_}2\rrbracket^{\mathcal{M}^{\Gamma}}$;
i.e., for all $a\in{\rm\sf Act}_{\\_}\varphi$
$\llbracket\psi_{\\_}1\rrbracket^{\mathcal{M}^{\Gamma}}\not\subseteq\mathrm{SE}^{\mathcal{M}^{\Gamma}}(\\{a\\})$
or
$\mathrm{R}^{\Gamma}_{\\_}{\\{a\\}}(\llbracket\psi_{\\_}1\rrbracket^{\mathcal{M}^{\Gamma}})\not\subseteq\llbracket\psi_{\\_}2\rrbracket^{\mathcal{M}^{\Gamma}}$.
Thus, there exists
$w_{\\_}1\in\llbracket\psi_{\\_}1\rrbracket^{\mathcal{M}^{\Gamma}}$ s.t.
$w_{\\_}1\not\in\mathrm{SE}^{\mathcal{M}^{\Gamma}}(a)$ or there exists
$w_{\\_}2\in\mathrm{R}^{\Gamma}_{\\_}a(w_{\\_}1)$ s.t.
$w_{\\_}2\not\in\llbracket\psi_{\\_}2\rrbracket^{\mathcal{M}^{\Gamma}}$. By
definition of $\mathsf{sel}^{\varphi}_{\\_}{w}$, Item (6), we add witnesses
for each $a\in{\rm\sf Act}_{\\_}\varphi$. So, let
$\uppi^{\prime}\in(\mathrm{S}^{\varphi}_{\\_}w)_{\\_}i$. If
$\uppi^{\prime}=\\{\langle\bot,\top\rangle\\}$, trivially we obtain
$\varnothing\neq\llbracket\psi_{\\_}1\rrbracket^{\mathcal{M}^{\varphi}_{\\_}w}\not\subseteq\mathrm{SE}^{\mathcal{M}^{\varphi}_{\\_}w}(\uppi^{\prime})=\varnothing$.
Then, take another $\uppi^{\prime}=\\{a\\}$ s.t. $a\in{\rm\sf
Act}_{\\_}\varphi$, and
$w^{\prime}_{\\_}1\in\llbracket\psi_{\\_}1\rrbracket^{\mathcal{M}^{\varphi}_{\\_}w}\subseteq\llbracket\psi_{\\_}1\rrbracket^{\mathcal{M}^{\Gamma}}$.
If $w^{\prime}_{\\_}1\not\in\mathrm{SE}^{\mathcal{M}^{\Gamma}}(\\{a\\})$,
$\mathrm{R}^{\Gamma}_{\\_}a(w^{\prime}_{\\_}1)=\varnothing$ and thus
$(\mathrm{R}^{\varphi}_{\\_}w)_{\\_}a(w^{\prime}_{\\_}1)=\varnothing$ and
therefore
$w^{\prime}_{\\_}1\not\in\mathrm{SE}^{\mathcal{M}^{\varphi}_{\\_}w}(\\{a\\})$.
On the other hand, if there exists
$w_{\\_}2\in\mathrm{R}^{\Gamma}_{\\_}a(w^{\prime}_{\\_}1)$ s.t.
$w_{\\_}2\not\in\llbracket\psi_{\\_}2\rrbracket^{\mathcal{M}^{\Gamma}}$, then
by $\mathsf{sel}^{\varphi}_{\\_}{w}$ and IH, there exists
$w^{\prime}_{\\_}2\in\mathrm{W}^{\varphi}_{\\_}w$ s.t.
$w^{\prime}_{\\_}2\in\mathrm{R}^{\Gamma}_{\\_}a(w^{\prime}_{\\_}1)$ and
$w^{\prime}_{\\_}2\not\in\llbracket\psi_{\\_}2\rrbracket^{\mathcal{M}^{\varphi}_{\\_}w}$,
and consequently, there exists
$w^{\prime}_{\\_}2\in(\mathrm{R}^{\varphi}_{\\_}{w})_{\\_}a(w^{\prime}_{\\_}1)$
s.t.
$w^{\prime}_{\\_}2\not\in\llbracket\psi_{\\_}2\rrbracket^{\mathcal{M}^{\varphi}_{\\_}{w}}$.
In any case, it leads to
$\mathcal{M}^{\varphi}_{\\_}{w},v\not\models\mathsf{Kh}_{\\_}i(\psi_{\\_}1,\psi_{\\_}2)$,
a contradiction. Therefore,
$\mathcal{M}^{\Gamma},v\models\mathsf{Kh}_{\\_}i(\psi_{\\_}1,\psi_{\\_}2)$.

Notice now that the selection function adds states from
$\mathcal{M}^{\Gamma}$, only for each $\mathsf{Kh}_{i}$-formula that appears
as a subformula of $\varphi$; and the number of states added at each time is
polynomial in $|\varphi|$. Hence, the size of $\mathrm{W}^{\varphi}_{\\_}w$ is
polynomial. Since $(\mathrm{S}^{\varphi}_{\\_}w)_{\\_}i$ is also polynomial,
the size of $\mathcal{M}^{\varphi}_{\\_}w$ is polynomial in $|\varphi|$.
Finally, the definition of an $\mathrm{LTS}^{U}$ requires the set of actions
to be infinite. It is easy to see that we can extend ${\rm\sf
Act}_{\\_}\varphi$ to an infinite set. Since Definition 3.3 defines relations
over some subset of the actions, this extension does not alter the size of
$\mathcal{M}^{\varphi}_{\\_}w$. $\blacksquare$

$\triangleleft$

In order to prove that the satisfiability problem of
$\mathsf{L}_{\mathsf{Kh}_{i}}$ is in NP, it remains to show that the model
checking problem is in P.

######  Proposition 16.

The model checking problem for $\mathsf{L}_{\mathsf{Kh}_{i}}$ is in P.

######  Proof..

Given a pointed $\mathrm{LTS}^{U}$ $\mathcal{M},w$ and a formula $\varphi$, we
define a bottom-up labeling algorithm running in polynomial time which checks
whether $\mathcal{M},w\models\varphi$. We follow the same ideas as for the
basic modal logic K (see e.g., [10]). Below we introduce the case for formulas
of the shape $\mathsf{Kh}_{\\_}i(\psi,\varphi)$, over an $\mathrm{LTS}^{U}$
$\mathcal{M}=\langle\mathrm{W},\mathrm{R},\mathrm{S},\mathrm{V}\rangle$:

Procedure ModelChecking($(\mathcal{M},w)$, $\mathsf{Kh}_{\\_}i(\psi,\varphi))$

$lab(\mathsf{Kh}_{\\_}i(\psi,\varphi))\leftarrow\varnothing$;

for all $\uppi\in\mathrm{S}_{\\_}i$ do

$kh\leftarrow True$;

for all $\sigma\in\uppi$ do

for all $v\in lab(\psi)$ do

$kh\leftarrow(kh\ \&\ v\in\mathrm{SE}(\sigma)\ \&\
\mathrm{R}_{\\_}\sigma(v)\subseteq lab(\varphi))$;

end for

end for

if $kh$ then

$lab(\mathsf{Kh}_{\\_}i(\psi,\varphi))\leftarrow\mathrm{W}$;

end if

end for

As $\mathrm{S}_{\\_}i$ and each $\uppi\in\mathrm{S}_{\\_}i$ are not empty, the
first two for loops are necessarily executed. If $lab(\psi)=\varnothing$, then
the formula $\mathsf{Kh}_{\\_}i(\psi,\varphi)$ is trivially true. Otherwise,
$kh$ will remain true only if the appropriate conditions for the
satisfiability of $\mathsf{Kh}_{\\_}i(\psi,\varphi))$ hold. If no $\uppi$
succeeds, then the initialization of $lab(\mathsf{Kh}_{\\_}i(\psi,\varphi))$
as $\varnothing$ will not be overwritten, as it should be. Both
$v\in\mathrm{SE}(\sigma)$ and $\mathrm{R}_{\\_}\sigma$ can be verified in
polynomial time. Hence, the model checking problem is in P. $\blacksquare$

$\triangleleft$

The intended result for satisfiability now follows.

######  Theorem 8.

The satisfiability problem for $\mathsf{L}_{\mathsf{Kh}_{i}}$ over
${\mathrm{LTS}^{U}}s$ is NP-complete.

######  Proof..

Hardness follows from NP-completeness of propositional logic (a fragment of
$\mathsf{L}_{\mathsf{Kh}_{i}}$). By Proposition 15, each satisfiable formula
$\varphi$ has a model of polynomial-size on $\varphi$. Thus, we can guess a
polynomial model $\mathcal{M},w$, and verify $\mathcal{M},w\models\varphi$
(which can be done in polyonomial time, due to Proposition 16). Thus, the
satisfiability problem is in the class NP. $\blacksquare$

$\triangleleft$

##  9 Final remarks

In this article, we introduce a new semantics for the _knowing how_ modality
from [57, 58, 59], for multiple agents. It is defined in terms of
_uncertainty-based labeled transition systems ( $\mathrm{LTS}^{U}$)_. The
novelty in our proposal is that ${\mathrm{LTS}^{U}}s$ are equipped with an
indistinguishability relation among plans. In this way, the epistemic notion
of uncertainty of an agent –which in turn defines her epistemic state– is
reintroduced, bringing the notion of _knowing how_ closer to the notion of
_knowing that_ from classical epistemic logics. We believe that the semantics
based on $\mathrm{LTS}^{U}$ can represent properly the situation of a shared,
objective description of the affordances of a given situation, together with
the different, subjective and personal abilities of a group of agents; this
seems difficult to achieve using a semantics based on LTSs alone.

We show that the logic of [57, 58, 59] can be obtained by imposing particular
conditions over $\mathrm{LTS}^{U}$; thus, the new semantics is more general.
In particular, it provides counter-examples to $\mathpzc{EMP}$ and
$\mathpzc{COMP}$, which directly link the knowing how modality $\mathsf{Kh}$
to properties of the universal modality. Indeed, consider $\mathpzc{EMP}$:
even though $\mathsf{A}(\psi\rightarrow\varphi)$ objectively holds in the
underlying LTS of an $\mathrm{LTS}^{U}$, it could be argued that an agent
might not be aware of actions or plans to turn those facts into knowledge,
resulting in $\mathsf{Kh}(\psi,\varphi)$ failing in the model.

To characterize validities in this language over $\mathrm{LTS}^{U}$s, we
introduce a sound and strongly complete axiom system.

We also define a suitable notion of bisimulation over ${\mathrm{LTS}^{U}}s$,
following ideas introduced in [17, 18]. We show that bisimilarity implies
formula equivalence, and that finite models form a Hennessy-Milner class
(i.e., that formula equivalence implies bisimilarity over finite models).

Finally, we prove that the satisfiability problem for our multi-agent knowing
how logic over the $\mathrm{LTS}^{U}$-based semantics is NP-complete. The
proof relies on a selection argument on the canonical model, and on the fact
that the model checking problem is polynomial. We also provide a filtration
technique that, given an arbitrary model satisfying $\varphi$, returns a
finite model that satisfies $\varphi$.

Future work. There are several interesting lines of research to explore in the
future. First, our framework easily accommodates other notions of
executability. For instance, one could require only some of the plans in a set
$\uppi$ to be strongly executable, or weaken the condition of _strong_
executability, etc. We can also explore the effects of imposing different
restrictions on the construction of the indistinguishability relation between
plans. It would be interesting to investigate which logics we obtain in these
cases, and their relations with the $\mathrm{LTS}$ semantics.

Second, to our knowledge, the exact complexity of the satisfiability problem
for knowing how over $\mathrm{LTS}$s is open. It would be interesting to solve
this problem, for instance, by following and adapting ideas from [40].

Third, the $\mathrm{LTS}^{U}$ semantics, in the multi-agent setting, leads to
natural definitions of concepts of _collective_ knowing how, in the spirit of
[13]. For instance, one can easily define a notion of _general knowing how_ as
$\mathsf{EKh}_{\\_}G(\psi,\varphi):=\bigwedge_{\\_}{i\in
G}\mathsf{Kh}_{i}(\psi,\varphi)$, whose reading is _“everyone in the group $G$
knows how to achieve $\varphi$ given $\psi$”_; and _“somebody in the group $G$
knows how to achieve $\varphi$ given $\psi$”_, as
$\mathsf{SKh}_{\\_}G(\psi,\varphi):=\bigvee_{\\_}{i\in
G}\mathsf{Kh}_{i}(\psi,\varphi)$ (see, e.g., [1] for a similar approach in
standard epistemic logic). Other, more complex notions such as _distributed_
and _common knowing how_ , deserve further exploration.

Finally, dynamic modalities capturing epistemic updates can be defined via
operations that modify the indistinguishability relation among plans (as is
done with other dynamic epistemic operators, see, e.g., [53]). This would
allow to express different forms of communication, such as _public_ ,
_private_ and _semi-private_ announcements concerning (sets of) plans. Some
preliminary results have been presented in [4].

## References

  * [1] Thomas Ågotnes and Yì N. Wáng.  Somebody knows.  In Meghyn Bienvenu, Gerhard Lakemeyer, and Esra Erdem, editors, Proceedings of the 18th International Conference on Principles of Knowledge Representation and Reasoning, KR 2021, Online event, November 3-12, 2021, pages 2–11, 2021.
  * [2] Carlos Areces, Valentin Cassano, Pablo F. Castro, Raul Fervari, and Andrés R. Saravia.  A deontic logic of knowingly complying.  In A. Ricci, W. Yeoh, N. Agmon, and B. An, editors, Proceedings of the 22nd International Conference on Autonomous Agents and MultiAgent Systems, AAMAS ’23, London, United Kingdom, May 29 - June 2, 2023. International Foundation for Autonomous Agents and Multiagent Systems, 2023, to appear.
  * [3] Carlos Areces, Raul Fervari, Andrés R. Saravia, and Fernando R. Velázquez-Quesada.  Uncertainty-based semantics for multi-agent knowing how logics.  In Joseph Y. Halpern and Andrés Perea, editors, Proceedings Eighteenth Conference on Theoretical Aspects of Rationality and Knowledge, TARK 2021, Beijing, China, June 25-27, 2021, volume 335 of EPTCS, pages 23–37, 2021.
  * [4] Carlos Areces, Raul Fervari, Andrés R. Saravia, and Fernando R. Velázquez-Quesada.  First steps in updating knowing how.  In Carlos Areces and Diana Costa, editors, Dynamic Logic. New Trends and Applications, pages 1–16. Springer International Publishing, 2023\.
  * [5] Sergei Artemov.  The logic of justification.  The Review of Symbolic Logic, 1(04):477–513, 2008.
  * [6] Alexandru Baltag.  To know is to know the value of a variable.  In Advances in Modal Logic 11, pages 135–155, 2016.
  * [7] Alexandru Baltag, Lawrence S. Moss, and Slawomir Solecki.  The logic of public announcements, common knowledge, and private suspicions.  In Proceedings of TARK ’98, pages 43–56. Morgan Kaufmann Publishers Inc., 1998.
  * [8] Francesco Belardinelli.  Reasoning about knowledge and strategies: Epistemic strategy logic.  In Fabio Mogavero, Aniello Murano, and Moshe Y. Vardi, editors, Proceedings 2nd International Workshop on Strategic Reasoning, SR 2014, Grenoble, France, April 5-6, 2014, volume 146 of EPTCS, pages 27–33, 2014.
  * [9] Patrick Blackburn, Marteen de Rijke, and Yde Venema.  Modal Logic.  Cambridge University Press, November 2002.
  * [10] Patrick Blackburn and Johan van Benthem.  Modal Logic: A Semantic Perspective.  In Handbook of Modal Logic, pages 1–84. Elsevier, 2006.
  * [11] Stéphane Demri and Raul Fervari.  Model-checking for ability-based logics with constrained plans.  In The Thirty-Seventh AAAI Conference on Artificial Intelligence, AAAI 2023, Washington DC, USA, February 7-14, 2023. AAAI Press, 2023, to appear.
  * [12] Ronald Fagin and Joseph Y. Halpern.  Belief, awareness, and limited reasoning.  Artificial Intelligence, 34(1):39–76, 1988.
  * [13] Ronald Fagin, Joseph Y. Halpern, Yoram Moses, and Moshe Y. Vardi.  Reasoning about knowledge.  The MIT Press, Cambridge, Mass., 1995.
  * [14] Jie Fan, Yanjing Wang, and Hans van Ditmarsch.  Contingency and knowing whether.  The Review of Symbolic Logic, 8(1):75–107, 2015.
  * [15] Jeremy Fantl.  Knowledge how.  In E. Zalta, editor, The Stanford Encyclopedia of Philosophy. Metaphysics Research Lab, Stanford University, spring 2021 edition, 2021.
  * [16] Raul Fervari, Andreas Herzig, Yanjun Li, and Yanjing Wang.  Strategically knowing how.  In Carles Sierra, editor, Proceedings of the Twenty-Sixth International Joint Conference on Artificial Intelligence, IJCAI 2017, Melbourne, Australia, August 19-25, 2017, pages 1031–1038. ijcai.org, 2017.
  * [17] Raul Fervari, Fernando R. Velázquez-Quesada, and Yanjing Wang.  Bisimulations for _Knowing How_ logics.  In 5th International Workshop on Strategic Reasoning, SR 2017, 2017.
  * [18] Raul Fervari, Fernando R. Velázquez-Quesada, and Yanjing Wang.  Bisimulations for knowing how logics.  The Review of Symbolic Logic, pages 1–37, 2021.
  * [19] Valentin Goranko and Solomon Passy.  Using the universal modality: Gains and questions.  Journal of Logic and Computation, 2(1):5–30, 1992.
  * [20] Tao Gu and Yanjing Wang.  "Knowing value” logic as a normal modal logic.  In Lev D. Beklemishev, Stéphane Demri, and András Maté, editors, Advances in Modal Logic 11, proceedings of the 11th conference on "Advances in Modal Logic," held in Budapest, Hungary, August 30 \- September 2, 2016, pages 362–381. College Publications, 2016.
  * [21] J. Y. Halpern and R. Pucella.  Dealing with logical omniscience: Expressiveness and pragmatics.  Artificial Intelligence, 175(1):220–235, 2011.
  * [22] David Harel, Dexter Kozen, and Jerzy Tiuryn.  Dynamic Logic.  The MIT Press, 2000.
  * [23] Sergiu Hart, Aviad Heifetz, and Dov Samet.  Knowing whether, knowing that, and the cardinality of state spaces.  Journal of Economic Theory, 70(1):249–256, 1996.
  * [24] Katherine Hawley.  Success and knowledge-how.  American Philosophical Quarterly, 40(1):19–31, 2003.
  * [25] Vincent F. Hendricks.  Introduction: 8 bridges between mainstream and formal epistemology.  Philosophical Studies, 128(1):1–5, March 2006.
  * [26] Andreas Herzig.  Logics of knowledge and action: critical analysis and challenges.  Autonomous Agents and Multi Agent Systems, 29(5):719–753, 2015\.
  * [27] Andreas Herzig and Nicolas Troquard.  Knowing how to play: uniform choices in logics of agency.  In Hideyuki Nakashima, Michael P. Wellman, Gerhard Weiss, and Peter Stone, editors, 5th International Joint Conference on Autonomous Agents and Multiagent Systems (AAMAS 2006), Hakodate, Japan, May 8-12, 2006, pages 209–216. ACM, 2006.
  * [28] Jaakko Hintikka.  Knowledge and Belief.  Cornell University Press, Ithaca N.Y., 1962.
  * [29] Wojciech Jamroga and Thomas Ågotnes.  Constructive knowledge: what agents can achieve under imperfect information.  Journal of Applied Non Classical Logics, 17(4):423–475, 2007.
  * [30] Wojciech Jamroga and Wiebe van der Hoek.  Agents that know how to play.  Fundamenta Informaticae, 63(2-3):185–219, 2004.
  * [31] Yves Lespérance, Hector J. Levesque, Fangzhen Lin, and Richard B. Scherl.  Ability and knowing how in the situation calculus.  Studia Logica, 66(1):165–186, 2000.
  * [32] Yanjun Li.  Stopping means achieving: A weaker logic of knowing how.  Studies in Logic, 9(4):34–54, 2017.
  * [33] Yanjun Li.  Tableau-based decision procedure for logic of knowing-how via simple plans.  In Pietro Baroni, Christoph Benzmüller, and Yì N. Wáng, editors, Logic and Argumentation - 4th International Conference, CLAR 2021, Hangzhou, China, October 20-22, 2021, Proceedings, volume 13040 of Lecture Notes in Computer Science, pages 266–283. Springer, 2021.
  * [34] Yanjun Li and Yanjing Wang.  Achieving while maintaining: - A logic of knowing how with intermediate constraints.  In Sujata Ghosh and Sanjiva Prasad, editors, Logic and Its Applications - 7th Indian Conference, ICLA 2017, Kanpur, India, January 5-7, 2017, Proceedings, volume 10119 of Lecture Notes in Computer Science, pages 154–167. Springer, 2017.
  * [35] Yanjun Li and Yanjing Wang.  Multi-agent knowing how via multi-step plans: A dynamic epistemic planning based approach.  In Patrick Blackburn, Emiliano Lorini, and Meiyun Guo, editors, Logic, Rationality, and Interaction - 7th International Workshop, LORI 2019, Chongqing, China, October 18-21, 2019, Proceedings, volume 11813 of Lecture Notes in Computer Science, pages 126–139. Springer, 2019.
  * [36] Yanjun Li and Yanjing Wang.  Knowing how to plan.  In Joseph Y. Halpern and Andrés Perea, editors, Proceedings Eighteenth Conference on Theoretical Aspects of Rationality and Knowledge, TARK 2021, Beijing, China, June 25-27, 2021, volume 335 of EPTCS, pages 233–247, 2021.
  * [37] Yanjun Li and Yanjing Wang.  Neighborhood semantics for logic of knowing how.  Synthese, 199(3-4):8611–8639, May 2021.
  * [38] Yanjun Li and Yanjing Wang.  Planning-based knowing how: A unified approach.  Artificial Intelligence, 296, 2021.
  * [39] John McCarthy and Patrick J. Hayes.  Some philosophical problems from the standpoint of artificial intelligence.  In Machine Intelligence, pages 463–502. Edinburgh University Press, 1969.
  * [40] Arne Meier, Michael Thomas, Heribert Vollmer, and Martin Mundhenk.  The complexity of satisfiability for fragments of CTL and CTL*.  International Journal of Foundations of Computer Science, 20(5):901–918, 2009.
  * [41] John-Jules Ch. Meyer and Wiebe van der Hoek.  Epistemic Logic for AI and Computer Science.  Cambridge University Press, New York, N.Y., U.S.A., 1995.
  * [42] Robert Moore.  A formal theory of knowledge and action.  In Formal Theories of the Commonsense World. Ablex Publishing Corporation, 1985.
  * [43] Pavel Naumov and Jia Tao.  Together we know how to achieve: An epistemic logic of know-how (extended abstract).  In Jérôme Lang, editor, Proceedings Sixteenth Conference on Theoretical Aspects of Rationality and Knowledge, TARK 2017, Liverpool, UK, 24-26 July 2017, volume 251 of EPTCS, pages 441–453, 2017\.
  * [44] Pavel Naumov and Jia Tao.  Second-order know-how strategies.  In Elisabeth André, Sven Koenig, Mehdi Dastani, and Gita Sukthankar, editors, Proceedings of the 17th International Conference on Autonomous Agents and MultiAgent Systems, AAMAS 2018, Stockholm, Sweden, July 10-15, 2018, pages 390–398. International Foundation for Autonomous Agents and Multiagent Systems Richland, SC, USA / ACM, 2018.
  * [45] Pavel Naumov and Jia Tao.  Together we know how to achieve: An epistemic logic of know-how.  Artificial Intelligence, 262:279–300, 2018.
  * [46] Pavel Naumov and Jia Tao.  Knowing-how under uncertainty.  Artificial Intelligence, 276:41–56, 2019.
  * [47] Andrés Perea.  Epistemic Game Theory: Reasoning and Choice.  Cambridge University Press, Cambridge, 2012.
  * [48] Gilbert Ryle.  The Concept of Mind: 60th Anniversary Edition.  Hutchinson & Co, 1949.
  * [49] Robert Stalnaker.  The problem of logical omniscience, I.  Synthese, 89(3):425–440, 1991.
  * [50] Johan van Benthem.  Logical Dynamics of Information and Interaction.  Cambridge University Press, 2011.
  * [51] Wiebe van der Hoek and Alessio Lomuscio.  Ignore at your peril - towards a logic for ignorance.  In The Second International Joint Conference on Autonomous Agents & Multiagent Systems, AAMAS 2003, July 14-18, 2003, Melbourne, Victoria, Australia, Proceedings, pages 1148–1149. ACM, 2003.
  * [52] Wiebe van der Hoek, Bernd van Linder, and John-Jules Ch. Meyer.  On agents that have the ability to choose.  Stud Logica, 66(1):79–119, 2000.
  * [53] Hans van Ditmarsch, Wiebe van der Hoek, and Barteld Kooi.  Dynamic Epistemic Logic.  Springer, 2007.
  * [54] Jan van Eijck, Malvin Gattinger, and Yanjing Wang.  Knowing values and public inspection.  In Sujata Ghosh and Sanjiva Prasad, editors, Logic and Its Applications - 7th Indian Conference, ICLA 2017, Kanpur, India, January 5-7, 2017, Proceedings, volume 10119 of Lecture Notes in Computer Science, pages 77–90. Springer, 2017.
  * [55] Moshe Y. Vardi.  On epistemic logic and logical omniscience.  In Joseph Y. Halpern, editor, TARK, pages 293–305. Morgan Kaufmann, 1986.
  * [56] Xun Wang.  A logic of knowing how with skippable plans.  In Patrick Blackburn, Emiliano Lorini, and Meiyun Guo, editors, Logic, Rationality, and Interaction - 7th International Workshop, LORI 2019, Chongqing, China, October 18-21, 2019, Proceedings, volume 11813 of Lecture Notes in Computer Science, pages 413–424. Springer, 2019.
  * [57] Yanjing Wang.  A logic of knowing how.  In Wiebe van der Hoek, Wesley H. Holliday, and Wen-Fang Wang, editors, Logic, Rationality, and Interaction - 5th International Workshop, LORI 2015 Taipei, Taiwan, October 28-31, 2015, Proceedings, volume 9394 of Lecture Notes in Computer Science, pages 392–405. Springer, 2015.
  * [58] Yanjing Wang.  Beyond knowing that: a new generation of epistemic logics.  In H. van Ditmarsch and G. Sandu, editors, Jaakko Hintikka on knowledge and game theoretical semantics, pages 499–533. Springer, 2018.
  * [59] Yanjing Wang.  A logic of goal-directed knowing how.  Synthese, 195(10):4419–4439, 2018.
  * [60] Chao Xu, Yanjing Wang, and Thomas Studer.  A logic of knowing why.  Synthese, 198(2):1259–1285, 2021.


Fix some $\varepsilon>0$ and some admissible configuration $P$ on $S^{d}$, and
let $c(\varepsilon)>0$ be the constant promised by the Supersaturation Theorem
(Theorem 9). By our ‘equicontinuity’ Lemma 16, there exists $\delta>0$ such
that, whenever $\|Q-P\|_{\infty}\leq\delta$, we have $|I_{Q}(A)-I_{P}(A)|\leq
c(\varepsilon)$ for all $A\subseteq S^{d}$.

Suppose $Q\in\mathcal{B}(P,\delta)$ and $A\subset S^{d}$ is a measurable set
avoiding $Q$; we must then have $I_{P}(A)\leq c(\varepsilon)$, and so (by the
Supersaturation Theorem) $\sigma(A)\leq\mathbf{m}_{S^{d}}(P)+\varepsilon$. We
conclude that $\mathbf{m}_{S^{d}}(Q)\leq\mathbf{m}_{S^{d}}(P)+\varepsilon$
whenever $Q\in\mathcal{B}(P,\delta)$.

Now write $P=\\{v_{1},\dots,v_{k}\\}$, and consider the function
$g_{P}:(S^{d})^{k}\times\textrm{{O}}(d+1)\rightarrow\mathbb{R}$ given by

$g_{P}(x_{1},\dots,x_{k},T):=\sum_{i=1}^{k}\|x_{i}-Tv_{i}\|.$

Note that this function is continuous, nonnegative and that

$\min_{T\in\textrm{{O}}(d+1)}g_{P}(x_{1},\dots,x_{k},T)=0\hskip
8.53581pt\text{if and only if}\hskip 8.53581pt\\{x_{1},\dots,x_{k}\\}\simeq
P.$

By elementary measure theory, we can find a compact set $A\subset S^{d}$ which
avoids $P$ and has measure $\sigma(A)\geq\mathbf{m}_{S^{d}}(P)-\varepsilon$.
The continuous function $g_{P}$ attains a minimum on the compact set
$A^{k}\times\textrm{{O}}(d+1)$; denote this minimum by $\gamma$, and note that
$\gamma>0$ since $A$ avoids $P$.

Let us show that $A$ also avoids $Q$, for all $Q\in\mathcal{B}(P,\gamma/2k)$.
Indeed, writing $Q=\\{u_{1},\dots,u_{k}\\}$, for any points
$x_{1},\dots,x_{k}\in A$ and any $T\in\textrm{{O}}(d+1)$ we have that

$\displaystyle\sum_{i=1}^{k}\|x_{i}-Tu_{i}\|$
$\displaystyle\geq\sum_{i=1}^{k}\big{|}\|x_{i}-Tv_{i}\|-\|Tu_{i}-Tv_{i}\|\big{|}$
$\displaystyle\geq g_{P}(x_{1},\dots,x_{k},T)-k\|Q-P\|_{\infty},$

which is at least $\gamma/2>0$ if $\|Q-P\|_{\infty}\leq\gamma/2k$. For such
configurations we obtain

$\mathbf{m}_{S^{d}}(Q)\geq\sigma(A)\geq\mathbf{m}_{S^{d}}(P)-\varepsilon.$

We conclude that
$|\mathbf{m}_{S^{d}}(Q)-\mathbf{m}_{S^{d}}(P)|\leq\varepsilon$ whenever
$\|Q-P\|_{\infty}\leq\min\\{\delta,\gamma/2k\\}$, finishing the proof. ∎

As our definition of the independence density $\mathbf{m}_{S^{d}}(P)$ involved
a supremum over all $P$-avoiding measurable sets $A\subseteq S^{d}$, it is not
immediately clear whether there actually exists a measurable $P$-avoiding set
attaining this extremal value of density. In fact, such a result is _false_ in
the case where $d=1$ and we are considering two-point configurations
$\\{u,v\\}\subset S^{1}$: if the length of the arc between $u$ and $v$ is
_not_ a rational multiple of $\pi$, it was shown by Székely [16] that
$\mathbf{m}_{S^{1}}(\\{u,v\\})=1/2$ but there is no $\\{u,v\\}$-avoiding
measurable set of density $1/2$.

We will now show that extremizer sets exist whenever the configuration we are
forbidding is admissible. Note that the result also holds (with the same
proof) when forbidding several admissible configurations; this generalizes to
higher-order configurations a theorem of DeCorte and Pikhurko [7] for
forbidden distances on the sphere.

######  Theorem 12 (Existence of extremizers).

If $P\subset S^{d}$ is an admissible configuration, then there is a
$P$-avoiding measurable set $A\subseteq S^{d}$ attaining
$\sigma(A)=\mathbf{m}_{S^{d}}(P)$.

###### Proof.

Let $A_{1},A_{2},\dots\subseteq S^{d}$ be a sequence of $P$-avoiding
measurable sets satisfying
$\lim_{i\rightarrow\infty}\sigma(A_{i})=\mathbf{m}_{S^{d}}(P)$. By passing to
a subsequence if necessary, we may assume that $(A_{i})_{i\geq 1}$ converges
to some function $A\in\mathcal{B}_{\infty}$ in the weak∗ topology of
$L^{\infty}(S^{d})$. We shall prove two things:

  * $(i)$

the limit function $A$ is $\\{0,\,1\\}$-valued almost everywhere, so we can
identify it with its support $\text{supp}\,A$;

  * $(ii)$

after possibly modifying it on a zero measure set, this set $A$ will avoid
$P$.

With these two results we will be done, since
$\sigma(A)=\lim_{i\rightarrow\infty}\sigma(A_{i})=\mathbf{m}_{S^{d}}(P)$.

By weak∗ convergence we know that $0\leq A\leq 1$ almost everywhere, and by
weak∗ continuity we also have
$I_{P}(A)=\lim_{i\rightarrow\infty}I_{P}(A_{i})=0$. From this we easily
conclude that $I_{P}(\text{supp}\,A)=0$, and also

$\sigma(\text{supp}\,A)=\int_{S^{d}}\text{supp}\,A(x)\,d\sigma(x)\geq\int_{S^{d}}A(x)\,d\sigma(x)=\mathbf{m}_{S^{d}}(P).$
(11)

But Lemma 11 implies that $\sigma(\text{supp}\,A)\leq\mathbf{m}_{S^{d}}(P)$,
which by (11) and the fact that $0\leq A\leq 1$ can only happen if
$A=\text{supp}\,A$ almost everywhere. This proves $(i)$.

Identifying $A$ with its support and using that $I_{P}(A)=0$, Lemma 11 implies
we can remove a zero measure subset of $A$ in order to remove all copies of
$P$. This proves $(ii)$ and finishes the proof of the theorem. ∎

To conclude, let us make explicit what we can say about the possible
independence densities when forbidding $n$ distinct contractions of an
admissible configuration $P$; due to lack of dilation invariance in the
spherical setting, characterizing these values in terms of simpler quantities
is much harder than it is in the Euclidean setting.

Denote
$\mathcal{M}_{n}^{S^{d}}(P):=\big{\\{}\mathbf{m}_{S^{d}}(t_{1}P,\,t_{2}P,\,\dots,\,t_{n}P):\,0<t_{1}<t_{2}<\dots<t_{n}\leq
1\big{\\}}$. Due to continuity of $\mathbf{m}_{S^{d}}$ (Theorem 11) this set
is an interval, and its upper extremity is $\sup_{0<t\leq
1}\mathbf{m}_{S^{d}}(tP)$. By supermultiplicativity (Lemma 19) the lower
extremity of $\mathcal{M}_{n}^{S^{d}}(P)$ is at least $\inf_{0<t\leq
1}\mathbf{m}_{S^{d}}(tP)^{n}$, and by asymptotic independence (Theorem 10) it
can be at most $\inf_{0<t\leq
1}\mathbf{m}_{S^{d}}(tP)\cdot\liminf_{t\rightarrow
0}\mathbf{m}_{S^{d}}(tP)^{n-1}$.

##  4 Concluding remarks and open questions

Our results leave open the question of what happens when the configurations we
forbid are _not_ admissible. There are two different reasons for a given
configuration (either on the space or on the sphere) to not be admissible, so
let us examine them separately.

The fist reason is that $P$ is degenerate, meaning that its points are
affinely dependent if we are on $\mathbb{R}^{d}$ or linearly dependent if we
are on $S^{d}$. In the Euclidean setting, Bourgain [2] showed an example of
sets $A_{d}\subset\mathbb{R}^{d}$ (for each $d\geq 2$) which have positive
density but which avoid arbitrarily large dilates of the degenerate three-
point configuration $\\{-1,0,1\\}$. These sets then show that the conclusion
of Bourgain’s Theorem (and thus also the conclusion of our Theorem 4) is false
for this degenerate configuration.

This counterexample was later generalized by Graham [13], who showed that a
result like Bourgain’s Theorem _can only hold_ if $P$ is contained on the
surface of some sphere of finite radius (as is always the case when $P$ is
non-degenerate). In fact, Graham’s result implies (for instance) that

$\mathbf{m}_{\mathbb{R}^{d}}\big{(}P,\,\sqrt{3}P,\,\sqrt{5}P,\,\sqrt{7}P,\,\dots\big{)}>0$

whenever $P\subset\mathbb{R}^{d}$ is nonspherical, that is, not contained on
the surface of any sphere. Some kind of non-degeneracy hypothesis is thus
necessary both for Bourgain’s result and for our Theorem 4.111111We believe
the same is true for their spherical analogues, namely Theorem 10 and
Corollary 3, though we do not know of a counterexample.

It is interesting to note, however, that a more recent result of Ziegler [17,
18] (generalizing a theorem of Furstenberg, Katznelson and Weiss [12] for
three-point configurations) shows that every set $A\subseteq\mathbb{R}^{d}$ of
positive upper density is _arbitrarily close_ to containing all large enough
dilates of _any_ finite configuration $P\subset\mathbb{R}^{d}$. More
precisely, denoting by $A_{\delta}$ the set of all points at distance at most
$\delta$ from the set $A$, Ziegler proved the following:

######  Theorem 13.

Let $A\subseteq\mathbb{R}^{d}$ be a set of positive upper density and
$P\subset\mathbb{R}^{d}$ be a finite set. Then there exists $l_{0}>0$ such
that, for any $l\geq l_{0}$ and any $\delta>0$, the set $A_{\delta}$ contains
a configuration congruent to $lP$.

Let us now turn to the second reason for a configuration $P$ on
$\mathbb{R}^{d}$ or $S^{d}$ to be non-admissible, namely that it contains
$d+1$ points (if it has more than $d+1$ points then it is obviously
degenerate). In this case we cannot apply the same strategy we used to prove
the Counting Lemmas, and it is not clear whether they or the analogues of
Bourgain’s Theorem are true. We conjecture that they are whenever $d\geq 2$,
so that we can remove the cardinality condition from the statement of
Bourgain’s result and of our ‘asymptotic independence’ Theorems 4 and 10.

In particular, let us make more explicit the simplest case of this conjecture,
which is an obvious question left open since the results of Bourgain and of
Furstenberg, Katznelson and Weiss:

######  Conjecture 1.

Let $A\subset\mathbb{R}^{2}$ be a set of positive upper density and let
$u,v,w\in\mathbb{R}^{2}$ be non-collinear points. Then there exists $l_{0}>0$
such that for any $l\geq l_{0}$ the set $A$ contains a configuration congruent
to $\\{lu,lv,lw\\}$.

Another question we ask is related to a suspected ‘compatibility condition’
between the Euclidean and spherical settings. Since $S^{d}$ resembles
$\mathbb{R}^{d}$ at small scales, it seem geometrically intuitive that
$\mathbf{m}_{S^{d}}(tP)$ should get increasingly close to
$\mathbf{m}_{\mathbb{R}^{d}}(P)$ as $t\rightarrow 0$ whenever $P$ is a
contractible configuration on $S^{d}$. (It is easy to show that a
configuration $P\subset S^{d}$ is contractible if and only if it is contained
in a $d$-dimensional affine subspace, so we can embed it in $\mathbb{R}^{d}$.)
We ask whether this intuition is indeed correct, i.e. is it true that
$\lim_{t\rightarrow 0}\mathbf{m}_{S^{d}}(tP)=\mathbf{m}_{\mathbb{R}^{d}}(P)$
for all contractible configurations $P$?

In a more combinatorial perspective, we wish to know whether an analogue of
the Hypergraph Removal Lemma holds for forbidden geometrical configurations.
In intuitive terms, the question we ask is whether a measurable set $A$
(either on $\mathbb{R}^{d}$ or on $S^{d}$) which contains ‘few’ copies of some
given configuration $P$ can be made $P$-avoiding by removing only ‘a few’ of
its points.121212On the unit sphere, this property would more formally read:
whenever $A\subseteq S^{d}$ satisfies $I_{P}(A)\leq\varepsilon$, there is a
subset $E\subset A$ of measure $\sigma(E)\leq o_{\varepsilon\rightarrow 0}(1)$
such that $A\setminus E$ avoids $P$ (where $o_{\varepsilon\rightarrow 0}(1)$
denotes a quantity that goes to zero as $\varepsilon\rightarrow 0$). Similarly
in the Euclidean setting. Such a result would then ‘explain’ geometrical sets
having few copies of $P$ as those which are close to a set avoiding this
configuration, and it trivially implies the corresponding Supersaturation
Theorem; note that this is a quantitative and stronger version of our ‘zero-
measure removal’ Lemmas 2 and 11.

Finally, it would be very interesting to have a way of obtaining good upper
and lower bounds for the independence densities of a given configuration.
There are several papers (see [1, 6] and the references therein) which
consider this question in the case of two-point configurations, drawing on
powerful methods from the theory of conic optimization and representation
theory, and it is already quite challenging in this simplest case. We believe
that the study of the independence density for higher-order configurations in
the optimization setting is also worthwhile, since they serve as model
problems for symmetric optimization problems depending on higher-order
relations and might prove very fruitful in new methods developed.

## Acknowledgements

The author would like to thank Fernando de Oliveira Filho, Lucas Slot and
Frank Vallentin for many helpful discussions. We also thank F. de Oliveira
Filho and F. Vallentin for several suggestions which improved the presentation
of this paper.

This work is supported by the European Union’s EU Framework Programme for
Research and Innovation Horizon 2020 under the Marie Skłodowska-Curie Actions
Grant Agreement No 764759 (MINOA).

## References

  * [1] C. Bachoc, A. Passuello, and A. Thiery, The density of sets avoiding distance 1 in Euclidean space, Discrete Comput. Geom., 53 (2015), pp. 783–808.
  * [2] J. Bourgain, A Szemerédi type theorem for sets of positive density in ${\bf R}^{k}$, Israel J. Math., 54 (1986), pp. 307–316.
  * [3] B. Bukh, Measurable sets with excluded distances, Geom. Funct. Anal., 18 (2008), pp. 668–697.
  * [4] D. Castro-Silva, Quasirandomness in additive groups and hypergraphs, arXiv preprint arXiv:2107.01463, (2021).
  * [5] F. Dai and Y. Xu, Approximation theory and harmonic analysis on spheres and balls, Springer Monographs in Mathematics, Springer, New York, 2013\.
  * [6] E. DeCorte, F. M. de Oliveira Filho, and F. Vallentin, Complete positivity and distance-avoiding sets, Mathematical Programming, (2020).
  * [7] E. DeCorte and O. Pikhurko, Spherical sets avoiding a prescribed set of angles, Int. Math. Res. Not. IMRN, (2016), pp. 6095–6117.
  * [8] C. F. Dunkl, Operators and harmonic analysis on the sphere, Trans. Amer. Math. Soc., 125 (1966), pp. 250–263.
  * [9] P. Erdős, Problems and results in combinatorial geometry, in Discrete geometry and convexity (New York, 1982), vol. 440 of Ann. New York Acad. Sci., New York Acad. Sci., New York, 1985, pp. 1–11.
  * [10] P. Erdős and M. Simonovits, Supersaturated graphs and hypergraphs, Combinatorica, 3 (1983), pp. 181–192.
  * [11] P. Frankl and R. M. Wilson, Intersection theorems with geometric consequences, Combinatorica, 1 (1981), pp. 357–368.
  * [12] H. Furstenberg, Y. Katznelson, and B. Weiss, Ergodic theory and configurations in sets of positive density, in Mathematics of Ramsey theory, vol. 5 of Algorithms Combin., Springer, Berlin, 1990, pp. 184–198.
  * [13] R. L. Graham, Recent trends in Euclidean Ramsey theory, Discrete Math., 136 (1994), pp. 119–127.
  * [14] V. Rödl and M. Schacht, Regularity lemmas for graphs, in Fete of combinatorics and computer science, vol. 20 of Bolyai Soc. Math. Stud., János Bolyai Math. Soc., Budapest, 2010, pp. 287–325.
  * [15] L. A. Székely, Remarks on the chromatic number of geometric graphs, in Graphs and other combinatorial topics (Prague, 1982), vol. 59 of Teubner-Texte Math., Teubner, Leipzig, 1983, pp. 312–315.
  * [16] , Measurable chromatic number of geometric graphs and sets without some distances in Euclidean space, Combinatorica, 4 (1984), pp. 213–218.
  * [17] T. Ziegler, An application of ergodic theory to a problem in geometric Ramsey theory, Israel J. Math., 114 (1999), pp. 271–288.
  * [18] , Nilfactors of $\mathbb{R}^{m}$-actions and configurations in sets of positive upper density in $\mathbb{R}^{m}$, J. Anal. Math., 99 (2006), pp. 249–266.

D. de Castro Silva, Department Mathematik/Informatik, Abteilung Mathematik,
Universität zu Köln, Weyertal 86–90, 50931 Köln, Germany.

E-mail address<EMAIL_ADDRESS>