printacmref=false none 254 This is a slightly extended version of the same
title paper that will appear in AAMAS 2024\. This version contains a small
appendix with proofs that, for space reasons, do not appear in the AAMAS 2024
version. HSE University Moscow Russian Federation University of Bergen Bergen
Norway Utrecht University Utrecht Netherlands

# Dynamic Epistemic Logic of Resource Bounded Information Mining Agents

Vitaliy Dolgorukov<EMAIL_ADDRESS>,  Rustam Galimullin
<EMAIL_ADDRESS>and  Maksim Gladyshev<EMAIL_ADDRESS>
###### Abstract.

Logics for resource-bounded agents have been getting more and more attention
in recent years since they provide us with more realistic tools for modelling
and reasoning about multi-agent systems. While many existing approaches are
based on the idea of agents as imperfect reasoners, who must spend their
resources to perform logical inference, this is not the only way to introduce
resource constraints into logical settings. In this paper we study agents as
perfect reasoners, who may purchase a new piece of information from a
trustworthy source. For this purpose we propose dynamic epistemic logic for
semi-public queries for resource-bounded agents. In this logic (groups of)
agents can perform a query (ask a question) about whether some formula is true
and receive a correct answer. These queries are called semi-public, because
the very fact of the query is public, while the answer is private. We also
assume that every query has a cost and every agent has a budget constraint.
Finally, our framework allows us to reason about group queries, in which
agents may share resources to obtain a new piece of information together. We
demonstrate that our logic is complete, decidable and has an efficient model
checking procedure.

###### Key words and phrases:

Resource Bounded Agents; Dynamic Epistemic Logic; Epistemic Logic; Group
Queries; Common Knowledge

##  1\. Introduction

In our paper we present a logic for reasoning about resource bounded agents
who might purchase new information from a reliable source but do not
necessarily have enough budget resources.

From a technical perspective, we propose a multi-agent Kripke-style semantics,
in which propositional formulas have (non-negative) costs and agents have
(non-negative) budgets, i.e. amounts of available resources. In order to deal
with costs and budgets in our language, we use linear inequalities initially
introduced in Fagin et al. (1990) for reasoning about probabilities. These
inequalities allow us to formulate statements about formulas’ costs, agents’
budgets, and their comparisons explicitly as formulas of our language. We also
use standard epistemic primitives for individual and common knowledge Fagin et
al. (2003). Combined with linear inequalities, these primitives allow us to
express statements of the form “agent $i$ knows that her budget is at least
$k$”, “agent $j$ knows that the cost of $A$ is lower than the cost of $B$, but
$j$ does not know the cost of $A$”, “it is common knowledge among group $G$
that the joint budget of another group $D$ is lower than the cost of $A$”,
etc. Finally, we introduce a dynamic operator in the vein of dynamic epistemic
logic (DEL) van Ditmarsch et al. (2008) for (group) semi-public queries. This
operator assumes that a group of agents $G$ may perform the following action.
Let $A$ be some propositional formula and $\varphi$ be a formula of our logic
introduced below. We assume that there is a reliable source of information,
such that $G$ may perform a query to this source, ask “Is $A$ true?” and
receive a correct answer: either ’Yes’ or ’No’. Once this answer is received,
$\varphi$ holds. Such queries are semi-public in the sense that the answer is
private, i.e. available to members of $G$ only, but the very fact of the query
is public, i.e. other agents from $\mathbb{AG}-G$ (where $\mathbb{AG}$ is the
set of all agents) observe the fact that $G$ has performed a query, but do not
observe the answer.

There is also an additional constraint in our framework: formula $A$ has a
cost, and this cost can be different for different agents in $G$. The first
assumption captures a natural intuition that access to the information is not
always free, while the latter shows that this access can be non-symmetric (or
non-egalitarian) among agents. For example, there can be premium access to a
database, so the same query may have a lower cost for agents with this access;
one lab may have access to cheaper reagents than another, so it may perform
the same test spending less resources and so on. So, in this settings it may
be rational for agents to cooperate and optimize the amount of resources they
need to obtain a certain piece of knowledge. The last assumption we introduce
in this paper is that agents may share resources in groups. Thus, if $G$
decides to perform a query $A$, they identify the agent $i\in G$ for whom the
cost of this query is the lowest and then share an equal amount of resources
to perform the query. Such group queries are expressed as an operator
$[?_{G}^{A}]\varphi$ of our logic. This operator is inspired by the (dynamic)
epistemic logics of contingency Fan et al. (2015); van Ditmarsch and Fan
(2016). These logics focus on the notion of ‘knowing whether’, which clearly
describes an epistemic attitude of agents after the query $[?_{G}^{A}]$: all
agents $j\in\mathbb{AG}\setminus G$ know that all $i\in G$ know whether $A$ is
true. An earlier version of our logic restricted to individual agents was
proposed in Dolgorukov and Gladyshev (2023). The idea of group updates in
dynamic epistemic logic was proposed and studied in, for example, Ågotnes and
van Ditmarsch (2008); Ågotnes et al. (2010); Galimullin (2021); Galimullin and
Velázquez-Quesada (2023).

This paper is organized as follows. In Section 2 we introduce the language and
models of our logic $\mathsf{SPQ}$. In Section 3 we propose a sound and
complete axiomatisation for $\mathsf{SPQ}$. In Section 4 we provide a
polynomial time algorithm for solving the global model checking problem for
$\mathsf{SPQ}$ and demonstrate that the satisfiability problem for
$\mathsf{SPQ}$ is decidable. Finally, in Section 5 we overview existing works
in this field, and in Section 6 we discuss open problems and possible
directions for future work.

##  2\. Logic of Semi-public Queries

###  2.1. Language

At first, we need to fix a propositional language $\mathcal{L}_{PL}$. Let
$\mathsf{Prop}$ denote a countable set of propositional letters
$\\{p,q,\dots\\}$. Language $\mathcal{L}_{PL}$ is defined by the following
grammar:

$A\ \ ::=\ p\ \mid\ \neg A\ \mid\ (A\land A).$

Here $p\in\mathsf{Prop}$, and all the usual abbreviations of propositional
logic (such as $\top,\bot,\to$, and $\vee$) hold. Let
$\mathbb{AG}=\\{a_{1},\dots,a_{k}\\}$ be a finite set of agents. We fix a set
of terms

$\mathsf{Terms}=\\{c_{(A,i)}\mid
A\in\mathcal{L}_{PL},i\in\mathbb{AG}\\}\cup\\{b_{i}\mid i\in\mathbb{AG}\\}$

It contains a special term $c_{(A,i)}$ for the _cost_ of each propositional
formula $A$ for agent $i$, and a term $b_{i}$ for the _budget_ of each agent
$i$. So, we assume that the same formula $A$ can have a different cost for
different agents. Now, we can define our language
$\mathcal{L}_{\mathsf{SPQ}}$.

######  Definition  (Language).

The _language $\mathcal{L}_{\mathsf{SPQ}}$ of Epistemic Logic for Semi-Public
Queries_ is defined recursively as follows

$\varphi::=p\mid(z_{1}t_{1}+\dots+z_{n}t_{n})\geq
z)\mid\neg\varphi\mid(\varphi\wedge\varphi)\mid K_{i}\varphi\mid
C_{G}\varphi\mid[?_{G}^{A}]\varphi,$

where $p\in\mathsf{Prop}$, $t_{1},\dots,t_{n}\in\mathsf{Terms}$,
${z_{1},\dots,z_{n},z\in\mathbb{Z}}$, $i\in\mathbb{AG}$,
$G\subseteq\mathbb{AG}$, and $A\in\mathcal{L}_{PL}$.

Here $K_{i}\varphi$ means  “agent $i$ knows that $\varphi$ is true”, and
$C_{G}\varphi$ means “it is common knowledge among agents in $G$ that
$\varphi$ is true”. These are two standard operators for epistemic logic Fagin
et al. (2003). Linear inequalities of the form
$(z_{1}t_{1}+\dots+z_{n}t_{n})\geq z$ Fagin et al. (1990), in which only the
terms $c_{(A,i)}$ and $b_{i}$ from $\mathsf{Terms}$ can occur, allow us to
reason about formulas’ costs and agents’ budgets explicitly. Finally, we
interpret the dynamic operator $[?_{G}^{A}]\varphi$ as ”after a group query by
$G$ whether formula $A$ is true, $\varphi$ is true”. This operator can
alternatively be understood as “if $G$ performs query $A$, they can achieve
$\varphi$”.

The dual of $K_{i}$ is $\hat{K}_{i}\varphi:=\neg K_{i}\neg\varphi$.
Abbreviation $E_{G}\varphi:=\bigwedge_{i\in G}K_{i}\varphi$ means “everybody
in $G$ knows $\varphi$”. The dual for dynamic operator is
$\langle?_{G}^{A}\rangle\varphi:=\neg[?_{G}^{A}]\neg\varphi$. For linear
inequalities we use the same abbreviations as in Fagin et al. (1990). Thus, we
write $t_{1}-t_{2}\geq z$ for $t_{1}+(-1)t_{2}\geq z$, $t_{1}\geq t_{2}$ for
$t_{1}-t_{2}\geq 0$, $t_{1}\leq z$ for $-t_{1}\geq-z$, $t_{1}<z$ for
$\neg(t_{1}\geq z)$, and $t_{1}=z$ for $(t_{1}\geq z)\land(t_{1}\leq z)$. A
formula of the form $t\geq\frac{1}{2}$ can be viewed as an abbreviation for
$2t\geq 1$, so we allow rational numbers to appear in our formulas. Other
Boolean connectives $\to,\lor,\leftrightarrow,\bot$ and $\top$ are defined in
the standard way. In the rest of the paper we slightly abuse the notation and
write $c_{i}(A)$ instead of $c_{(A,i)}$. We denote the set of _subformulas_ of
a formula $\varphi$ as $\mathsf{Sub}(\varphi)$ .

Thus, the static fragment of our language $\mathcal{L}_{\mathsf{SPQ}}$ (i.e.
the fragment without $[?_{G}^{A}]\varphi$) allows us to express statements of
the form $c_{i}(p\vee q)\geq 10$ for “the cost of the query whether $p$ or $q$
is true for agent $i$ is at least 10”, $b_{j}\geq 3$ for “the budget of agent
$j$ is at least 3”, $2b_{j}=b_{i}$ for ”$i$’s budget is twice as big as that
of $j$”, $K_{a}(b_{i}+b_{j})\geq c_{i}(p\vee q)$ for “agent $a$ knows that the
joint budget of $i$ and $j$ is higher than the cost of $p\vee q$ for agent
$i$”, etc. The dynamic operator can express statements like
$[?_{\\{i,j\\}}^{(p\vee q)}]C_{\\{i,j\\}}\neg p$ meaning that “after a joint
query about $p\vee q$ by $\\{i,j\\}$ it is common knowledge among $\\{i,j\\}$
that $p$ is false”.

###  2.2. Semantics

Now we are ready to discuss the semantics for $\mathcal{L}_{\mathsf{SPQ}}$
formulas. Models of our logic are basically Kripke-style models endowed with
Cost and Budget functions.

######  Definition  (Model).

A _model_ is a tuple ${\mathcal{M}}=(W,(\sim_{i})_{i\in\mathbb{AG}},$
$\mathsf{Cost},$ $\mathsf{Bdg},$ $V)$, where

  * •

$W$ is a non-empty set of _states_ ,

  * •

${\sim_{i}}\subseteq(W\times W)$ is an equivalence relation for each
${i\in\mathbb{AG}}$,

  * •

$\mathsf{Cost}\colon\mathbb{AG}\times
W\times\mathcal{L}_{PL}\longrightarrow\mathbb{Q}^{+}\cup\\{0\\}$ assigns the
(non-negative) _cost_ to propositional formulas for each agent in each state,

  * •

$\mathsf{Bdg}\colon\mathbb{AG}\times
W\longrightarrow\mathbb{Q}^{+}\cup\\{0\\}$ is the (non-negative) _bugdet_ of
each agent at each state,

  * •

$V\colon\mathsf{Prop}\longrightarrow 2^{W}$ is a _valuation_ of propositional
variables.

Let $P(w):=\\{p\in\mathsf{Prop}\mid w\in V(p)\\}$ be the set of all
propositional variables that are true in state $w$. Moreover, let
$c_{>0}(i,w):=\\{A\in\mathcal{L}_{PL}\mid\mathsf{Cost}_{i}(w,A)>0\\}$ be the
set of all propositional formulas with positive cost for agent $i$ and state
$w$. We call a model _finite_ , if all of $W$, $\bigcup_{w\in W}P(w)$, and
$\bigcup_{(i,w)\in\mathbb{AG}\times W}c_{>0}(i,w)$ are finite. Given a finite
model ${\mathcal{M}}$ we define the _size_ of ${\mathcal{M}}$, denoted
$|{\mathcal{M}}|$, as

$|{\mathcal{M}}|:=\mathrm{card}(W)+\sum_{i\in\mathbb{AG}}\mathrm{card}(\sim_{i})+\\\
+\sum_{(i,w)\in\mathbb{AG}\times W}\mathrm{card}(c_{>0}(i,w))+\sum_{w\in
W}\mathrm{card}(P(w))$

We intentionally put as few restrictions on the $\mathsf{Cost}$ function as
possible to consider the most general case. Thus, our framework allows us to
model situations in which the cost of the same formula is different for
different agents and it can also be different across different states in $W$
for the same agent. Thus, the agent may be unaware of the cost of some formula
for herself as well as for other agents. Another important point is how the
costs of different formulas must be related to each other Feldman (2000). The
only two restrictions we find important to enforce are that the cost of
propositional tautologies must be zero for all agents, and that the costs of
_similar_ formulas must be the same. By _similar_ formulas $A$ and $B$
(denoted $A\approx B$) we mean that $A\approx B$ iff $A\equiv B$ or
$A\equiv\neg B$, where $A\equiv B$ denotes _equivalent_ formulas: $A\equiv B$
iff $\vdash_{PL}A\leftrightarrow B$. Formally, for all $i\in\mathbb{AG},w\in
W$ we require that
(C1) $\mathsf{Cost}_{i}(w,\top)=0$,
(C2) $A\approx B$ implies $\mathsf{Cost}_{i}(w,A)=\mathsf{Cost}_{i}(w,B)$.

For the $\mathsf{Bdg}$ function we only assume that it is non-negative for
every agent. But the budget of each agent may be different in different states
of $W$, so in our framework agents may be unaware of their and others’
budgets. To better illustrate the proposed semantics consider a simple
example.

######  Example  (Telescope example)

Three countries $n,m$ and $l$ are seeking to know a certain fact $p$ about the
universe. If any of them build a very expensive telescope, it will give them a
correct answer. Country $n$ is the richest among others having 15 abstract
resources ($b_{n}=15$). But due to some reasons, e.g. higher labour costs, it
requires the highest amount of resources $c_{n}(p)=30$ to build a telescope
there. Country $m$ has only 10 resources ($b_{m}=10$), but it can build a
telescope for $c_{m}(p)=20$, for example due to better logistics. Country $l$
is the poorest country with only $b_{l}=5$ resources, while the cost of a
telescope is the same as for $n$, so $c_{l}(p)=30$. Finally, we assume that
the costs of the telescope are known to all agents, $n$ and $m$ know the
budgets of each other as well as $l$’s budget. But $l$ is unaware of the exact
budget of $m$: it considers both options $b_{m}=10$ and $b_{m}=9$ as possible
ones.

$w_{1}$$p,b_{m}=10$$w_{3}$$p,b_{m}=9$$w_{2}$$\neg p,b_{m}=10$$w_{4}$$\neg
p,b_{m}=9$$l,m,n$$l,m,n$$l$$l$$\xRightarrow{?_{\\{m,n\\}}^{p}}$$\underline{w_{1}}$$p,b_{m}=0$$w_{2}$$\neg
p,b_{m}=0$$l$$\mathcal{M}$$\mathcal{M}^{?_{\\{m,n\\}}^{p}}$

Figure 1. (Left) Model ${\mathcal{M}}$ for Section 2.2. The model contains
four states $w_{1},w_{2},w_{3}$ and $w_{4}$, and we assume that $w_{1}$ is the
actual one. Arrows represent epistemic equivalence classes for agents $l,m$
and $n$. Reflexive and transitive arrows are omitted for readability. Formulas
$b_{n}=15,b_{l}=5,c_{n}(p)=30,c_{m}(p)=20$ and $c_{l}(p)=30$ hold in all four
states, and we omit them from the figure. (Right) Updated model
${\mathcal{M}}^{?_{\\{n,m\\}}p}$ for Section 2.2. Formulas
$b_{l}=5,c_{n}(p)=30,c_{m}(p)=20$ and $c_{l}(p)=30$ hold in both $w_{1}$ and
$w_{2}$ as before. But $b_{n}=15$ no longer holds, since $n$’s budget is
decreased after update: $b_{n}-\frac{c_{m}(p)}{|\\{n,m\\}|}=5$.

The model of this example is depicted in Figure 1. In this example, no single
country has a sufficient budget to build the telescope, i.e. to perform an
individual query about $p$. But there is still a way for them to cooperate and
build a telescope. If $n$ and $m$ share their resources, and $m$ builds the
telescope, then each of the countries $m$ and $n$ can spend 10 resources to
get the information about $p$. This procedure can be expressed by our dynamic
operator $[?_{\\{n,m\\}}^{p}]$.

Now we are ready to discuss the semantics of semi-public group queries
$[?_{G}^{A}]$. Recall that $[?_{G}^{A}]\varphi$ means “after a group query by
$G$ whether a formula $A$ is true, $\varphi$ is true”. We assume that each
group member receives the correct information about the truth of $A$ after
$[?_{G}^{A}]$. And we also assume that each group member spends equal amount
of resources on this query. But as we already mentioned, the cost of $A$ can
be different for different members of $G$. So, it is natural to assume that
the lowest of these costs must be spent. In other words, $[?_{G}^{A}]$ query
in a state $w$ can be described by the following procedure: identify $i\in G$
with the lowest cost of $A$, let each member of $G$ transfer
$\frac{Cost_{i}(w,A)}{|G|}$ resources to $i$, then let $i$ ask whether $A$ is
true and tell the answer to all agents in $G$.

More formally, let us abbreviate “the Budget Constraint of agent $i\in G$ for
the $G$’s query $A$” as

$\mathbf{BC}_{i}(G,A)\equiv\frac{\min_{j\in G}(c_{j}(A))}{|G|}$

So, $\mathbf{BC}_{i}(G,A)$ denotes the budget that would be sufficient for $i$
to participate in a $G$’s group query whether $A$ is true.

We also denote the fact that “the Budget Constraint for the query $A$ for $G$
is Satisfied” as

$\text{BCS}(G,A)\equiv\bigwedge\limits_{i\in
G}(b_{i}\geq\mathbf{BC}_{i}(G,A))$

If $\text{BCS}(G,A)$ holds, we say that the query $[?_{G}^{A}]$ is realisable
meaning that each group member has enough resources to cooperate according to
our resource distribution rule111Note that linear inequalities in our language
are capable enough to express alternative resource distribution rules. For
example, we can assume that according to another rule
$\text{BCS}^{\prime}(G,A)$ we pick the highest, but not the lowest cost among
members of $G$. This rule looks more arguable, but it is clearly expressible
in $\mathsf{SPQ}$. So, any expressible $\text{BCS}^{\prime}(G,A)$ can be
integrated in our framework with minimal changes.. Note that $\text{BCS}(G,A)$
is in fact a formula of $\mathsf{SPQ}$:

$\text{BCS}(G,A)\equiv\bigvee\limits_{j\in G}\biggl{(}\bigwedge\limits_{i\in
G}\Bigl{(}c_{j}(A)\leq c_{i}(A)\wedge
b_{i}\geq\frac{c_{j}(A)}{|G|}\Bigl{)}\biggl{)}$

######  Definition  (Updated Model).

Given a model ${\mathcal{M}}$, a group $G\subseteq\mathbb{AG}$ and a formula
$A\in\mathcal{L}_{PL}$, an _updated model_ ${\mathcal{M}}^{\prime}$ is a tuple
${\mathcal{M}}^{\prime}=(W^{\prime},$ $(\sim^{\prime}_{j})_{j\in\mathbb{AG}},$
$\mathsf{Cost}^{\prime},$ $\mathsf{Bdg}^{\prime},$ $V^{\prime})$, where

  * •

$W^{\prime}=\\{w\in W\mid{\mathcal{M}},w\vDash\text{BCS}(G,A)\\}$;

  * •

${\sim_{j}^{\prime}}=(W^{\prime}\times W^{\prime})\cap{\sim^{*}_{j}}$ with

$\sim^{*}_{j}=\begin{cases}\sim_{j}&\mbox{if }j\notin G,\\\
{\sim_{j}}\bigcap\Bigl{(}([A]_{\mathcal{M}}\times[A]_{\mathcal{M}})\bigcup([\neg
A]_{\mathcal{M}}\times[\neg A]_{\mathcal{M}})\Bigr{)}&\mbox{if }j\in
G;\end{cases}$

  * •

$\mathsf{Cost}_{j}^{\prime}(w,B)=\mathsf{Cost}_{j}(w,B)$, for all
$B\in\mathcal{L}_{PL},j\in\mathbb{AG}$;

  * •

$\mathsf{Bdg}_{j}^{\prime}(w)=\begin{cases}\mathsf{Bdg}_{j}(w)-\frac{\min\limits_{i\in
G}\mathsf{Cost}_{i}(w,A)}{|G|},&\mbox{if }j\in G,\\\
\mathsf{Bdg}_{j}(w),&\mbox{if }j\notin G,\end{cases}$

  * •

$V^{\prime}(p)=V(p)\cap W^{\prime}$ for all $p\in\mathsf{Prop}$.

By $[A]_{{\mathcal{M}}}$ we denote the set of states in $W$, such that each
$w\in[A]_{{\mathcal{M}}}$ satisfies the formula $A$ in a sense of Section 2.2.

Intuitively, an update $[?_{G}^{A}]$ of a model ${\mathcal{M}}$ firstly
removes all states of ${\mathcal{M}}$ in which at least one agent in $G$ does
not have a sufficient amount of resources for a $G$’s query about $A$. This
can be justified by the fact that agents do not necessarily know others
budgets, but when they observe the fact that $G$ actually performs a query
$A$, it no longer makes sense to consider the states in which
$\text{BCS}(G,A)$ does not hold as possible ones. Note also that when $G$
performs the semi-public query “is $A$ true?”, it gets either ’Yes’ or ’No’ as
an answer and we consider this fact to be known by all agents. Then, after the
update, all agents in $G$ necessarily distinguish any two states of
${\mathcal{M}}$ that do not agree on the valuation of $A$. But since the
actual answer is available only to the agents from $G$, epistemic relations of
other agents remain the same, only taking into account that some states have
been removed. This update does not affect the costs of formulas and budgets of
all agents outside of $G$. The budget of each $i\in G$ decreases by the
minimal cost of $A$ in the group divided by the size of this group.

Returning to Section 2.2, consider the result of updating ${\mathcal{M}}$ with
$[?_{\\{n,m\\}}p]$ in Figure 1. After this update, both $n$ and $m$ will know
that $p$ is true, moreover it will be common knowledge among them. Note that
since $l$ is not a member of this group, she will remain unaware of whether
$p$ is true or not. But since the fact that the telescope is built is public,
$l$ will know that $n$ and $m$ know whether $p$ is true, denoted
$K_{l}(E_{\\{n,m\\}}p\vee E_{\\{n,m\\}}\neg p)$. Moreover, $l$ will know that
$\\{n,m\\}$ has common knowledge whether $p$ is true, denoted
$K_{l}(C_{\\{n,m\\}}p\vee C_{\\{n,m\\}}\neg p)$. This is why we call these
queries semi-public. Note also that budgets of $n$ and $m$ are also decreased
by 10 according to the resource distribution rule.

We call two states $x,y\in W$ $G$-_reachable_ iff there is a sequence of
states $w_{0},\dots,w_{k}$ (where $k\geq 1$), such that $w_{0}=x$ and
$w_{k}=y$ and for all $0\leq j\leq k-1$ there exists $i\in G$ such that
$w_{j}\sim_{i}w_{j+1}$. We denote the $G$-reachability relation as $\sim_{G}$.

######  Definition  (Semantics).

The _truth_ $\vDash$ of a formula $\psi\in\mathcal{L}(\mathsf{SPQ})$ at a
state $w\in W$ of a model ${\mathcal{M}}$ is defined by induction:
${\mathcal{M}},w\vDash p$ iff $w\in V(p)$,
${\mathcal{M}},w\vDash\neg\varphi$ iff ${\mathcal{M}},w\nvDash\varphi$,
${\mathcal{M}},w\vDash\varphi\land\psi$ iff ${\mathcal{M}},w\vDash\varphi$ and
${\mathcal{M}},w\vDash\psi$,
${\mathcal{M}},w\vDash K_{i}\varphi$ iff $\forall w^{\prime}\in W$:
$w\sim_{i}w^{\prime}\Rightarrow{\mathcal{M}},w^{\prime}\vDash\varphi$,
${\mathcal{M}},w\vDash C_{G}\varphi$ iff $\forall w^{\prime}\in W$:
$w\sim_{G}w^{\prime}\Rightarrow{\mathcal{M}},w^{\prime}\vDash\varphi$,
${\mathcal{M}},w\vDash(z_{1}t_{1}+\dots+z_{n}t_{n})\geq z$ iff
$(z_{1}t^{\prime}_{1}+\dots+z_{n}t^{\prime}_{n})\geq z$, where for $1\leq
k\leq n$,

$t^{\prime}_{k}=\begin{cases}\mathsf{Cost}_{i}(w,A),&\text{for
}t_{k}=c_{i}{(A)}\\\ \mathsf{Bdg}_{i}(w),&\text{for }t_{k}=b_{i}.\end{cases}$

${\mathcal{M}},w\vDash[?_{G}^{A}]\varphi$ iff
${\mathcal{M}},w\vDash\text{BCS}(G,A)$ implies
${\mathcal{M}}^{?_{G}^{A}},w\vDash\varphi$, where ${\mathcal{M}}^{?_{G}^{A}}$
is an updated model in the sense of Section 2.2.

$\mathsf{SPQ}$ provides us with tools for reasoning about coalition formation
strategies to obtain the desirable knowledge by group queries. As Section 2.2
demonstrates, sometimes no single agent has enough resources to achieve
certain knowledge, but this knowledge is still achievable via cooperation.
Moreover, in many situations not only the choice of coalition for group query
matters, but also the choice of the right sequence of these queries. Thus,
$\mathsf{SPQ}$ allows us to reason about planning the order of queries as
well.

##  3\. A Sound and Complete Axiomatisation of $\mathsf{SPQ}$

The axiomatisation of $\mathsf{SPQ}$ is presented in Table 1. Axioms (I1)-(I6)
for linear inequalities were proposed in Fagin et al. (1990). Axioms (K)-(C),
(Neci), (RC1) are standard axioms and inference rules for epistemic logic with
common knowledge $S5^{C}$ Fagin et al. (2003). (B+)-(c≈) are axioms ensuring
all necessary properties of $\mathsf{Bdg}$ and $\mathsf{Cost}$ functions.
Axioms (rp)–(rK2), (Rep), (RC2) are reduction-style axioms and rules for
dynamic operator $[?_{G}^{A}]$. In $r_{\geq}$ axiom,
$\bigl{(}\sum\limits_{i=1}^{k}a_{i}t_{i}\geq z\bigr{)}^{(G,A)}$ denotes
$\bigl{(}\sum\limits_{i=1}^{k}a_{i}t_{i}\geq z\bigr{)}$, in which all
occurrences of $b_{i}$ for $i\in G$ among $t_{1},\dots,t_{k}$ are replaced
with $(b_{i}-\frac{c_{j}(A)}{|G|})$, where $j$ is the agent that occurs in
$\text{BCS}(G,A)$, i.e. for whom the cost of $A$ is minimal:
$\bigwedge\limits_{k\in G}c_{j}(A)\leq c_{k}(a)$. Soundness of (rp)–(rK2) can
be shown by a direct application of the definition of semantics. For details
see Technical Appendix. The axiomatisation of $\mathsf{SPQ}$ is sound.

If there is a derivation of $\varphi$ from the axioms and rules of inference
of $\mathsf{SPQ}$, we say that $\varphi$ is a _theorem_ of $\mathsf{SPQ}$ and
write $\vdash_{\mathsf{SPQ}}\varphi$. We write $\vdash$, when the logic we
refer to is clear from the context.

Observe that the presence of reduction axioms for the dynamic operator allows
us to ‘translate away’ the dynamic operator thus showing that $\mathsf{SPQ}$
without common knowledge is equally expressive as $\mathsf{SPQ}$ without
common knowledge and dynamic operators. The completeness of $\mathsf{SPQ}$
without common knowledge follows trivially from the completeness of
$\mathsf{SPQ}$ without common knowledge and dynamic operators Fagin et al.
(1990).

Note that we do not have a complete reduction of $\mathsf{SPQ}$ to its static
fragment due to the presence of common knowledge van Ditmarsch et al. (2008);
Wang and Cao (2013). Indeed, we can show that $\mathsf{SPQ}$ is strictly more
expressive than $\mathsf{SPQ}$ without common knowledge by reusing the
argument from, e.g., (van Ditmarsch et al., 2008, Theorem 8.34) and setting
all agents’ budgets to 0, and cost of all propositional formulas to 1. So, the
reduction argument does not work for our completeness proof.

Axioms: |
---|---
(Taut) | All propositional tautologies
(I1) | $(\sum\limits_{i=1}^{k}a_{i}t_{i}\geq c)\leftrightarrow(\sum\limits_{i=1}^{k}a_{i}t_{i}+0t_{k+1}\geq c)$
(I2) |  $(\sum\limits_{i=1}^{k}a_{i}t_{i}\geq c)\rightarrow(\sum\limits_{i=1}^{k}a_{j_{i}}t_{j_{i}}\geq c)$,
| where $j_{1},\dots,j_{k}$ is a permutation of $1,\dots,k$
(I3) | $(\sum\limits_{i=1}^{k}a_{i}t_{i}\geq c)\wedge(\sum\limits_{i=1}^{k}a^{\prime}_{i}t_{i}\geq c^{\prime})\to$
| $\to\sum\limits_{i=1}^{k}(a_{i}+a^{\prime}_{i})t_{i}\geq(c+c^{\prime})$
(I4) |  $(\sum\limits_{i=1}^{k}a_{i}t_{i}\geq c)\leftrightarrow(\sum\limits_{i=1}^{k}da_{i}t_{i}\geq dc)$ for $d>0$
(I5) | $(t\geq c)\vee(t\leq c)$
(I6) |  $(t\geq c)\to(t>d)$, where $c>d$
(K) | $K_{i}(\varphi\to\psi)\to(K_{i}\varphi\to K_{i}\psi)$
(T) | $K_{i}\varphi\to\varphi$
(4) | $K_{i}\varphi\to K_{i}K_{i}\varphi$
(5) | $\neg K_{i}\varphi\to K_{i}\neg K_{i}\varphi$
(C) | $C_{G}\varphi\to E_{G}(\varphi\wedge C_{G}\varphi)$
(B+) | $b_{i}\geq 0$
(c+) | $c_{i}(A)\geq 0$
(c⊤) | $c_{i}(\top)=0$
(c≈) |  $c_{i}(A)=c_{i}(B)$ if $A\approx B$
(rp) | $[?_{G}^{A}]p\leftrightarrow(\text{BCS}(G,A)\to p)$
(r≥) | $[?_{G}^{A}]\bigl{(}\sum\limits_{i=1}^{k}a_{i}t_{i}\geq z\bigr{)}\leftrightarrow$
|
$\leftrightarrow\Big{(}\text{BCS}(G,A)\to\bigl{(}\sum\limits_{i=1}^{k}a_{i}t_{i}\geq
z\bigr{)}^{(G,A)}\Big{)}$
(r¬) | $[?_{G}^{A}]\neg\varphi\leftrightarrow\text{BCS}(G,A)\to\neg[?_{G}^{A}]\varphi$
(r∧) | $[?_{G}^{A}](\varphi\wedge\psi)\leftrightarrow[?_{G}^{A}]\varphi\wedge[?_{G}^{A}]\psi$
(rK1) |  $[?_{G}^{A}]K_{j}\varphi\leftrightarrow\text{BCS}(G,A)\to K_{j}[?_{G}^{A}]\varphi$, for $j\notin G$
(rK2) | $[?_{G}^{A}]K_{i}\varphi\leftrightarrow\text{BCS}(G,A)\to$
|  $\to\bigwedge\limits_{A^{\prime}\in\\{A,\neg
A\\}}\Big{(}\bigl{(}A^{\prime}\to
K_{i}(A^{\prime}\to[?_{G}^{A}]\varphi)\bigr{)}\Big{)}$, for $i\in G$
Rules: |
(MP) | from $\varphi$ and $\varphi\rightarrow\psi$, infer $\psi$
(Neci) | from $\varphi$ infer $K_{i}\varphi$
(RC1) | from $\varphi\to E_{G}(\varphi\wedge\psi)$, infer $\varphi\to C_{G}\psi$
(Rep) | from $\varphi\leftrightarrow\psi$, infer
|  $[?_{G}^{A}]\varphi\leftrightarrow[?_{G}^{A}]\psi$ for any
$A\in\mathcal{L}_{PL}$
(RC2) | from $\chi\to[?_{G}^{A}]\psi$ and $(\chi\wedge\text{BCS}(G,A))\to$
|  $\to\bigwedge\limits_{A^{\prime}\in\\{A,\neg A\\}}(A^{\prime}\to E_{H\cap
G}(A^{\prime}\to\chi))\wedge E_{H\setminus G}\chi$,
| infer $\chi\to[?_{G}^{A}]C_{H}\psi$
Table 1. Proof system for $\mathsf{SPQ}$.

Moreover, $\mathsf{SPQ}$ is not compact due to the presence of common
knowledge. But even the $C_{G}$-free fragment is not compact due to the linear
inequalities. Consider a set of $\mathsf{SPQ}$-formulas: $\\{c_{i}(A)>n\mid
n\in\mathbb{N}\\}$. It is easy to see that any finite subset of this set is
satisfiable while the set itself is not.

$\mathsf{SPQ}$ is not compact.

For this reason, in the rest of this section we prove the weak completeness of
$\mathsf{SPQ}$. The proof is organised as follows. First, we define a Fisher-
Ladner Fischer and Ladner (1977) style closure $cl(\varphi)$ for any
$\mathsf{SPQ}$-consistent formula $\varphi$. Then we construct a finite
canonical pre-model, in which $\mathsf{Cost}$ and $\mathsf{Bdg}$ functions are
undefined and prove that such functions satisfying (C1) and (C2) exist. It
gives us a finite canonical model, for which we prove the truth lemma and
establish completeness. Later, we use the bounded size of canonical model to
prove that $\mathsf{SPQ}$ is decidable.

######  Definition  (Closure).

Let $cl(\varphi)$ be the smallest set of formulas such that

  1. (1)

$cl(\varphi)$ contains $\mathsf{Sub}(\varphi)$, i.e. all subformulas of
$\varphi$;

  2. (2)

$cl(\varphi)$ is closed under single negation: if $\psi\in cl(\varphi)$ and
$\psi$ does not start with $\neg$, then ${\neg\psi\in cl(\varphi)}$;

  3. (3)

$(b_{i}\geq 0)\in cl(\varphi)$, for each agent $i\in\mathbb{AG}$;

  4. (4)

$(c_{i}(A)\geq 0)\in cl(\varphi)$, for each $i\in\mathbb{AG}$ and each $A\in
cl(\varphi)$;

  5. (5)

$c_{i}(\top)=0\in cl(\varphi)$,

  6. (6)

$c_{i}(A)=c_{i}(B)\in cl(\varphi)$ for all $A,B\in cl(\varphi)$ s.t. $A\approx
B$;

  7. (7)

if $C_{G}\psi\in cl(\varphi)$, then $E_{G}(\psi\wedge C_{G}\psi)\in
cl(\varphi)$;

  8. (8)

if $[?_{G}^{A}]p\in cl(\varphi)$, then $\text{BCS}(G,A)\to p\in cl(\varphi)$;

  9. (9)

if $[?_{G}^{A}]\bigl{(}\sum\limits_{i=1}^{k}a_{i}t_{i}\geq z\bigr{)}\in
cl(\varphi)$, then
$\Big{(}\text{BCS}(G,A)\to\bigl{(}\sum\limits_{i=1}^{k}a_{i}t_{i}\geq
z\bigr{)}^{(G,A)}\Big{)}\in cl(\varphi)$;

  10. (10)

if $[?_{G}^{A}]\neg\psi\in cl(\varphi)$, then
$(\text{BCS}(G,A)\to\neg[?_{G}^{A}]\psi)\in cl(\varphi)$;

  11. (11)

if $[?_{G}^{A}](\chi\wedge\psi)\in cl(\varphi)$, then
$[?_{G}^{A}]\chi\wedge[?_{G}^{A}]\psi\in cl(\varphi)$;

  12. (12)

if $[?_{G}^{A}]K_{j}\psi\in cl(\varphi)$, where $j\notin G$, then
$\text{BCS}(G,A)\to K_{j}[?_{G}^{A}]\psi\in cl(\varphi)$;

  13. (13)

if $[?_{G}^{A}]K_{i}\psi\in cl(\varphi)$, where $i\in G$, then
$\text{BCS}(G,A)\to$
$\to\bigwedge\limits_{A^{\prime}\in\\{A,\neg
A\\}}\Bigl{(}\bigl{(}A^{\prime}\to
K_{i}(A^{\prime}\to[?_{G}^{A}]\psi)\bigl{)}\Bigl{)}\in cl(\varphi)$;

  14. (14)

if $[?_{G}^{A}]C_{G}\psi\in cl(\varphi)$, then
$\\{[?_{G}^{A}]K_{i}C_{G}\psi\mid i\in G\\}\subseteq cl(\varphi)$.

This construction guarantees that $cl(\varphi)$ is non-empty and finite as
well as the set of all maximal consistent subsets of $cl(\varphi)$. Note also
that $|cl(\varphi)|$ is polynomial in $|\varphi|$, where
$|\varphi|=|\mathsf{Sub}(\varphi)|$.

Now we construct a finite _canonical pre-model_ which does not (yet) contain
$\mathsf{Cost}$ and $\mathsf{Bdg}$ functions.

######  Definition  (Canonical pre-model).

Given a $\mathsf{SPQ}$-consistent formula $\varphi$, let a _canonical pre-
model_ for $\varphi$ be a tuple

${\mathcal{M}}^{cp}=(W^{c},\\{\sim^{c}_{i}\\}_{i\in\mathbb{AG}},V^{c}),\text{where}$

  * •

$W^{c}$ is the set of all maximal $\mathsf{SPQ}$-consistent subsets of
$cl(\varphi)$;

  * •

$x\sim^{c}_{i}y$ iff for all formulas $\psi\in cl(\varphi)$, it holds that
${K_{i}\psi\in x}$ iff ${K_{i}\psi\in y}$;

  * •

$w\in V^{c}(p)$ iff $p\in w$, for each $p\in cl(\varphi)$.

Next we need to prove the existence of appropriate $\mathsf{Cost}$ and
$\mathsf{Bdg}$ functions.

###### Lemma

There exist $\mathsf{Cost}^{c}$ and $\mathsf{Bdg}^{c}$ functions, such that
for all $(\sum\limits_{i=1}^{k}a_{i}t_{i}\geq z)$ and all $w\in W^{c}$ it
holds that $(\sum\limits_{i=1}^{k}a_{i}t_{i}\geq z)\in w$ iff
$\sum\limits_{i=1}^{k}a_{i}t^{\prime}_{i}\geq z$, where

$t^{\prime}_{k}=\begin{cases}\mathsf{Cost}_{i}^{c}(w,A),&\text{for
}t_{k}=c_{i}{(A)}\\\ \mathsf{Bdg}_{i}^{c}(w),&\text{for
}t_{k}=b_{i}\end{cases}$

###### Proof.

Since every state $w\in W^{c}$ is $\mathsf{SPQ}$-consistent, the set of all
linear inequalities contained in $w$ is satisfiable, i.e. has at least one
solution, due to (I1)-(I6) Fagin et al. (1990). Then we can construct
functions $\mathsf{Cost}^{c}_{i}(w,A)$ and $\mathsf{Bdg}^{c}_{i}(w)$ that
agree with this solution: for formulas $A\in\mathcal{L}_{PL}$ such that
$c_{i}(A)$ occurs in $cl(\varphi)$, we put $\mathsf{Cost}^{c}_{i}(w,A)$ to be
the rational that corresponds to $c_{i}(A)$ in that solution; for other
formulas $B\in\mathcal{L}_{PL}$, if $B\approx A$ for some formula $A\in
cl(\varphi)$, then we put
$\mathsf{Cost}^{c}_{i}(w,B):=\mathsf{Cost}_{i}^{c}(w,A)$. Thus we can enforce
that for all $w\in W^{c}$ and all $A\in\mathcal{L}_{PL}$ such that
$c_{i}(A)\in cl(\varphi)$ it holds that
(1) $\mathsf{Cost}^{c}_{i}(w,A)\geq 0$ for all $i\in\mathbb{AG}$ and all
formulas $A\in\mathcal{L}_{PL}$ such that $A$ occurs in $cl(\varphi)$ by the
construction of $cl(\varphi)$ and $(c^{+})$ axiom,
(2) $\mathsf{Cost}_{i}^{c}(w,\top)=0$, by the construction of $cl(\varphi)$
and $(c^{\top})$ axiom,
(3) $\mathsf{Cost}_{i}^{c}(w,A)=\mathsf{Cost}_{i}^{c}(w,B)$ for all
$A,B\in\mathcal{L}_{PL}$ such that $A\approx B$, by $(c^{\approx})$ axiom.

Similarly, we construct $\mathsf{Bdg}^{c}_{i}(w)$ functions in accordance with
the existing solution of linear inequalities contained in $w$. This
construction is well-defined, and for any $w\in W^{c}$ and any
$i\in\mathbb{AG}$, it holds that $\mathsf{Bdg}_{i}^{c}(w)\geq 0$ by $(B^{+})$
axiom and the construction of $cl(\varphi)$. ∎

This finishes the construction of a finite canonical model
${\mathcal{M}}^{c}=(W^{c}\\!,(\sim^{c}_{i})_{i\in\mathbb{AG}}$,
$\mathsf{Cost}^{c}\\!,\mathsf{Bdg}^{c}\\!,V^{c})$. As we have already
demonstrated, this model satisfies (C1) and (C2). It is also clear that for
all $i\in\mathbb{AG}$, ${\sim_{i}^{c}}$ is an equivalence relation on $W^{c}$
(for details see Halpern and Moses (1992)). Moreover, all $w\in W^{c}$ are
deductively closed in $cl(\varphi)$ (van Ditmarsch et al., 2008, Lemma 7.31).

######  Lemma  (Truth Lemma)

Let ${\mathcal{M}}^{c}$ be the canonical model for $\varphi$. For all $\psi\in
cl(\varphi),w\in W^{c}:{\mathcal{M}}^{c},w\vDash\psi$ iff $\psi\in w$.

###### Proof.

It is relatively straightforward to define a _complexity_ measure $c$ for
formulas $\varphi,\psi\in\mathsf{SPQ}$ such that if $\varphi$ is one of the
antecedents of (rp)–(rK2) and $\psi$ is a corresponding consequent, then
$c(\varphi)>c(\psi)$. For details see van Ditmarsch et al. (2008) and
Technical Appendix.

Induction Hypothesis (IH). For all $c(\psi)<c(\varphi)$ and all maximal
consistent subsets $w$ of $cl(\varphi)$, ${\mathcal{M}}^{c},w\models\psi$ if
and only if $\psi\in w$.

Cases for $\psi=p,\neg,\wedge$ and $K_{i}\varphi^{\prime}$ are trivial.

Case for $\psi=(z_{1}t_{1}+\dots+z_{n}t_{n})\geq z$ follows straightforwardly
from the choice of $\mathsf{Cost}^{c}$ and $\mathsf{Bdg}^{c}$ in Section 3.

Case $\psi=C_{G}\varphi^{\prime}$. We follow the proof from Halpern and Moses
(1992).

Right-to-left. Assume $C_{G}\varphi^{\prime}\in w$. We will show by induction
on $k$ that if $w^{\prime}$ is $\sim_{G}$-reachable from $w$ in $k$ steps then
$\varphi^{\prime}\in w^{\prime}$ and $C_{G}\varphi^{\prime}\in w^{\prime}$.
For the case of $k=1$ it is clear that if $C_{G}\varphi^{\prime}\in
w^{\prime}$ then $E_{G}(\varphi^{\prime}\wedge C_{G}\varphi^{\prime})\in w$ by
the construction of $cl(\varphi)$ and the fact that $w$ is its maximally
consistent subset. Then for all $y\in W^{c}$ if $y$ is $\sim_{G}$-reachable
from $w$ in one step, then both $\varphi^{\prime}\in y$ and
$C_{G}\varphi^{\prime}\in y$ since for some $i\in\mathbb{AG}$ it holds that
$\forall y:w\sim_{i}y$ and $E_{G}(\varphi^{\prime}\wedge
C_{G}\varphi^{\prime})\in w\Rightarrow(\varphi^{\prime}\wedge
C_{G}\varphi^{\prime})\in y$. Now we can prove the induction step: assume our
statement holds for $k$ and prove that it also holds for $k+1$. Assume that
$w^{\prime}\in W^{c}$ is $\sim_{G}$-reachable from $w$ in $k+1$ steps. Then
exists $t\in W^{c}$ which is $\sim_{G}$-reachable from $w$ in $k$ steps and
$w^{\prime}$ is $G$-reachable from $t$ in one step. By our induction
hypothesis, $C_{G}\varphi^{\prime}\in t$ and $\varphi^{\prime}\in t$. By our
first argument it is clear that $\varphi^{\prime}\in w^{\prime}$. Then by our
main induction hypothesis $M,w^{\prime}\vDash\varphi$ for all $w^{\prime}$
which are $\sim_{G}$-reachable from $w$. Then $M,w\vDash
C_{G}\varphi^{\prime}$.

Left-to-right. Assume $M,w\vDash C_{G}\varphi^{\prime}$. Note that every $y\in
W^{c}$ contains a finite set of formulas. Then we can write their conjunction
in our language: $\varphi_{y}$. Let $\chi=\bigvee\limits_{y\in\\{w\mid
M,w\vDash C_{G}\varphi^{\prime}\\}}\varphi_{y}$. Now it is easy to see that
the following statements hold: $\vdash_{\mathsf{SPQ}}\varphi_{w}\to\chi$,
$\vdash_{\mathsf{SPQ}}\chi\to\varphi^{\prime}$, $\vdash_{\mathsf{SPQ}}\chi\to
E_{G}\chi$. It follows straightforwardly that $\vdash\varphi_{w}\to
C_{G}\varphi^{\prime}$, and hence $C_{G}\varphi^{\prime}\in w$. Otherwise it
would hold that $\neg C_{G}\varphi^{\prime}\in w$ which would imply
inconsistency of $w$.

Case $\psi=[?_{G}^{A}]\varphi^{\prime}$. Subcases for $\psi=[?_{G}^{A}]p$,
$\psi=[?_{G}^{A}]\neg\varphi^{\prime}$,
$\psi=[?_{G}^{A}]\varphi^{\prime}\wedge\psi$ and
$[?_{G}^{A}]K_{i}\varphi^{\prime}$ follow from the construction of
$cl(\varphi)$, and the IH that $c([?_{G}^{A}]\varphi^{\prime})>c(\chi)$, where
$\chi$ is a consequent of one of the axioms (rp)-(rK2).

Subcase $\psi=[?_{G}^{A}]C_{H}\varphi^{\prime}$.
Right-to-left. Suppose that $[?_{G}^{A}]C_{H}\varphi^{\prime}\in w$ and
$w\sim^{?_{G}^{A}}_{H}w^{\prime}$. By definition,
$w\sim^{?_{G}^{A}}_{H}w^{\prime}$ means that there is a finite path
$w\sim_{i_{1}}^{?_{G}^{A}}w_{1}\sim_{i_{2}}^{?_{G}^{A}}w_{2}\sim_{i_{3}}^{?_{G}^{A}}\dots\sim_{i_{n}}^{?_{G}^{A}}w_{n}=w^{\prime}$
such that $i_{1},\dots,i_{n}\in H$. We first prove that for
$k\in\\{1,...,n\\}$ it holds that $[?_{G}^{A}]C_{H}\varphi^{\prime}\in w_{k}$
and $[?_{G}^{A}]\varphi^{\prime}\in w_{k}$, where $w_{k}=w$. For this, for
each $\sim_{i_{k}}$ we need to distinguish cases, where $i_{k}\in H-G$ and
$i_{k}\in H\cap G$.

First, let us consider the case $i\in H-G$ for any
$i\in\\{i_{1},...,i_{n}\\}$. Assume that $\text{BCS}(G,A)\in w_{k}$. Then,
from items (14) and (12) of Definition 3 by MP we have that
$K_{i}[?_{G}^{A}]C_{H}\varphi^{\prime}\in w$. By the construction of the
canonical model and the assumption that $w_{k}\sim_{i}^{?_{G}^{A}}w_{k+1}$,
the latter implies that $K_{i}[?_{G}^{A}]C_{H}\varphi^{\prime}\in w_{k+1}$.
Since all states of the canonical model are deductively closed, we get
$[?_{G}^{A}]C_{H}\varphi^{\prime}\in w_{k+1}$. Finally, from that the fact
that $w_{k+1}$ is deductively closed, we also have
$[?_{G}^{A}]\varphi^{\prime}\in w_{k+1}$ due to
$C_{H}\varphi^{\prime}\to\varphi^{\prime}$ and the distributivity of
$[?_{G}^{A}]$222Can be shown by a straightforward application of the
definition of semantics..

Second, we consider the case $i\in H\cap G$. By items (14) and (13) of
Definition 3, we have that $[?^{G}_{A}]K_{i}C_{H}\varphi^{\prime}\in w_{k}$
and $\bigwedge\limits_{A^{\prime}\in\\{A,\neg
A\\}}\Big{(}\bigl{(}A^{\prime}\to
K_{i}(A^{\prime}\to[?_{G}^{A}]C_{H}\varphi^{\prime})\bigr{)}\Big{)}\in w_{k}$.
Without loss of generality, assume that $A\in w_{k}$. Then by the deductive
closure of $w_{k}$ we obtain
$K_{i}(A^{\prime}\to[?_{G}^{A}]C_{H}\varphi^{\prime})\bigr{)}\in w_{k}$. By
the construction of the canonical model and the assumption that
$w_{k}\sim_{i}^{?_{G}^{A}}w_{k+1}$, the latter implies that
$A^{\prime}\to[?_{G}^{A}]C_{H}\varphi^{\prime}\in w_{k+1}$. Moreover,
assumption $w_{k}\sim_{i}^{?_{G}^{A}}w_{k+1}$ implies that $A\in w_{k+1}$.
Hence, we have $[?_{G}^{A}]C_{H}\varphi^{\prime}\in w_{k+1}$, and similarly to
the previous case, $[?_{G}^{A}]\varphi^{\prime}\in w_{k+1}$.

Finally, we are ready to prove our main claim here. Recall that we assume that
$[?_{G}^{A}]C_{H}\varphi^{\prime}\in w$ and $w\sim^{?_{G}^{A}}_{H}w^{\prime}$.
We have shown that $[?_{G}^{A}]\varphi^{\prime}\in w_{k}$ for all $w_{k}$ on
the path $w\sim^{?_{G}^{A}}_{H}w^{\prime}$. By IH, this is equivalent to the
fact that ${\mathcal{M}}^{c},w_{k}\models[?_{G}^{A}]\varphi^{\prime}$ for all
states $w_{k}$ on the path $w\sim^{?_{G}^{A}}_{H}w^{\prime}$. The latter is
equivalent to ${\mathcal{M}}^{c},w\models[?_{G}^{A}]C_{H}\varphi^{\prime}$ by
the semantics.

Left-to-right. Assume that
${\mathcal{M}}^{c},w\models[?_{G}^{A}]C_{H}\varphi^{\prime}$, and let us
define $S:=\\{w\in
W^{c}\mid{\mathcal{M}}^{c},w\models[?_{G}^{A}]C_{H}\varphi^{\prime}\\}$ and
$\chi:=\bigvee\\{\underline{X}\mid X\in S\\}$, where
$\underline{X}:=\varphi_{1}\wedge\dots\wedge\varphi_{m}$, such that
$\\{\varphi_{1},\dots,\varphi_{m}\\}=X$. Clearly, $w\in S$, and hence, due to
$w$ being deductively closed, $\chi\in w$. Moreover, it is straightforward to
prove that $\chi\to[?_{G}^{A}]C_{H}\varphi^{\prime}\in w$, and hence
$[?_{G}^{A}]C_{H}\varphi^{\prime}\in w$ (see (van Ditmarsch et al., 2008,
Chapter 7.5) for details). ∎

[Completeness] For any $\varphi\in\mathcal{L}_{\mathsf{SPQ}}$, if $\varphi$ is
valid, then $\vdash\varphi$.

###### Proof.

Assume towards a contradiction that $\not\vdash\varphi$. This means that
$\lnot\varphi$ is consistent, and thus it is in one of the maximal consistent
sets $w$ built from $cl(\lnot\varphi)$. For such a closure we can construct
the canonical model, such that ${\mathcal{M}}^{c},w\models\lnot\varphi$ by
Lemma 3, or, equivalently, ${\mathcal{M}}^{c},w\not\models\varphi$. ∎

As a corollary of the canonical model construction, we immediately get the
small model theorem.

[Small Model Theorem] If $\varphi\in\mathcal{L}_{\mathsf{SPQ}}$ is
satisfiable, then it is satisfied in a model with at most $2^{|cl(\varphi)|}$
states.

##  4\. Complexity profile of $\mathsf{SPQ}$

In this section we explore the complexity of the model checking and
satisfiability problems of $\mathsf{SPQ}$. In particular, we first establish
that model checking $\mathsf{SPQ}$ can be done in polynomial time. After that,
we show that $\mathsf{SPQ}$ is decidable with NEXPTIME upper bound.

###  4.1. Model checking

######  Definition .

Given a finite
${\mathcal{M}}=(W,(\sim_{i})_{i\in\mathbb{AG}},\mathsf{Cost},\mathsf{Bdg},V)$
and a formula $\varphi\in\mathcal{L}_{\mathsf{SPQ}}$, the _global model
checking problem_ for $\mathsf{SPQ}$ consists in finding all $w\in W$ such
that ${\mathcal{M}},w\vDash\varphi$.

In this section, we provide a polynomial time algorithm for solving the global
model checking problem for $\mathsf{SPQ}$. The algorithm requires for a given
$\varphi$ a list of subformulas of $\varphi$ ordered so that group queries are
evaluated before the formulas within the scope of the dynamic modalities, i.e.
in $[?_{G}^{A}]\psi$ we would like to find the extension of $A$ first, and
only then the extension of $\psi$. In such a way we can simulate the effects
of queries before checking the formulas that may be impacted by them.

Let some $\varphi\in\mathcal{L}_{\mathsf{SPQ}}$ be given. First, we create a
list $sub(\varphi)$ of subformulas of $\varphi$ that also includes modalities
$[?^{A}_{G}]$ occurring in $\varphi$. After that we label each $\psi\in
sub(\varphi)$ by a sequence of dynamic modalities inside the scope of which it
appears. Finally, we order the list in the following way. For $\psi^{\sigma}$
and $\chi^{\tau}$ with (possibly empty) labellings $\sigma$ and $\tau$,
$\psi^{\sigma}$ precedes $\chi^{\tau}$ if and only if

  * •

$\psi^{\sigma}$ and $\chi^{\tau}$ occur in modalities $[?^{A}_{G}]$, and
$\sigma<\tau$ (i.e. $\sigma$ is a proper prefix of $\tau$), or else

  * •

$\psi^{\sigma}$ appears in some $[?^{A}_{G}]$, and $\chi^{\tau}$ does not, or
else

  * •

$\psi^{\sigma}$ is of the form $[?^{A}_{G}]$, and $\chi^{\tau}$ is not, or
else

  * •

neither $\psi^{\sigma}$ nor $\chi^{\tau}$ appear in any $[?^{A}_{G}]$, and
$\tau<\sigma$, or else

  * •

both $\psi^{\sigma}$ and $\chi^{\tau}$ are of the form $[?^{A}_{G}]$, and
$\sigma<\tau$, or else

  * •

$\sigma=\tau$, and $\psi^{\sigma}$ is a part of $\chi^{\tau}$, or else

  * •

$\psi$ appears to left of $\chi$ in $\varphi$.

As an example, let $\varphi:=[?^{p}_{G}][?^{p\lor q}_{H}]C_{G}p$. The ordered
list $sub(\varphi)$ would look as follows:

$\\{p,[?^{p}_{G}],p^{[?^{p}_{G}]},q^{[?^{p}_{G}]},(p\lor
q)^{[?^{p}_{G}]},p^{[?^{p}_{G}],[?^{p\lor q}_{H}]},\\\
(C_{G}p)^{[?^{p}_{G}],[?^{p\lor q}_{H}]},([?^{p}_{G}]C_{G}p)^{[?^{p\lor
q}_{H}]},\varphi\\}.$

Note that the size of $sub(\varphi)$ is bounded by $\mathcal{O}(|\varphi|)$.

Our global model checking Algorithm 4.1 for $\mathsf{SPQ}$ is based on the
labelling algorithm for epistemic logic (see, e.g., Halpern and Moses (1992)).
Thus we omit all Boolean and some epistemic cases for brevity, and provide
only the case of common knowledge as an example. The technical complexity in
our algorithm is that for the case of the dynamic modalities, we should keep
track of which states and relations are preserved after a sequence of updates.
Moreover, we also create a polynomial number of additional budget variables to
store the remaining budget of agents after each query.

1 An algorithm for global model checking for $\mathsf{SPQ}$

1:procedure Global$\mathsf{SPQ}$($M,\varphi$)

2: for all $\psi^{\sigma}\in sub(\varphi)$ do

3: for all $w\in W$ do

4: case $\psi^{\sigma}=C_{G}{\chi}^{\sigma}$

5: $\mathit{check}\leftarrow\mathit{true}$

6: for all $(w,v)\in R_{G}$ do

7: if $(w,v)$ is labelled with $\sigma$ then

8: if $v$ is not labelled with $\chi^{\sigma}$ then

9: $\mathit{check}\leftarrow\mathit{false}$

10: break

11: if $\mathit{check}$ then

12: label $w$ with $C_{G}{\chi}^{\sigma}$

13: case $\psi^{\sigma}=[?^{A}_{G}]^{\sigma}$

14: for all $i\in\mathbb{AG}$ do

15: for all $(v,u)^{\sigma}\in\sim_{i}$ do

16: if ${\mathcal{M}},v\models BCS^{\sigma}(G,A)$ and ${\mathcal{M}},u\models
BCS^{\sigma}(G,A)$ then

17: for all $j\in G$ do

18: $Bdg_{j}(v)^{\sigma}\leftarrow Bdg_{j}^{?_{G}A}(v)$

19: $Bdg_{j}(u)^{\sigma}\leftarrow Bdg_{j}^{?_{G}A}(u)$

20: if $i\not\in G$ then

21: label $(v,u)$ with $\sigma,[?^{A}_{G}]$

22: else

23: if $v$ is labelled with $A$ iff $u$ is labelled with $A$ then

24: label $(v,u)$ with $\sigma,[?^{A}_{G}]$

25: case $\psi^{\sigma}=([?^{A}_{G}]\chi)^{\sigma}$

26: if $w$ is labelled with $\chi^{\sigma,[?^{A}_{G}]}$ then

27: label $w$ with $([?^{A}_{G}]\chi)^{\sigma}$

28:end procedure

The algorithm mimics the definition of semantics, and its correctness can be
shown by induction on $\varphi$. The preparation of ordered list
$sub(\varphi)$ takes $\mathcal{O}(|\varphi|^{2})$ number of steps. On line 16,
$BCS^{\sigma}(G,A)$ is the budget constraint for query $A$ for agents from $G$
after the sequence of updates $\sigma$. Respective budgets of agents after
updates are calculated on lines 18 and 19. Observe, that computing
$Bdg_{j}(v)^{\sigma}$ and $BCS^{\sigma}(G,A)$ requires only arithmetical
computation with values of all variables known. This can be done in polynomial
time. Each computation of $BCS^{\sigma}$ is called for
$\mathcal{O}(|\varphi|\cdot|W|\cdot|\mathbb{AG}|\cdot|\\!\sim\\!|)$ times.
Finally, each computation of some $Bdg_{j}(v)^{\sigma}$ is called for
$\mathcal{O}(|\varphi|\cdot|W|\cdot|\mathbb{AG}|^{2}\cdot|\\!\sim\\!|)$ times.
Since in the worst case, $BCS^{\sigma}$ and $Bdg_{j}(v)^{\sigma}$ require a
polynomial number of steps, model checking $\mathsf{SPQ}$ is in polynomial
time.

Model checking $\mathsf{SPQ}$ is in P.

###  4.2. Decidability

######  Definition .

Given a formula of $\varphi\in\mathcal{L}_{\mathsf{SPQ}}$, the _satisfiability
problem_ for $\mathsf{SPQ}$ consists in determining whether there is a pointed
model ${\mathcal{M}},w$ such that ${\mathcal{M}},w\models\varphi$.

[Decidability] The satisfiability problem for $\mathsf{SPQ}$ is decidable.

###### Proof.

The decidability of $\mathsf{SPQ}$ follows from the small model theorem
(Theorem 1). This theorem states that a formula
$\varphi\in\mathcal{L}_{\mathsf{SPQ}}$ is satisfiable iff it is satisfiable in
a model $M$ with at most $2^{|cl(\varphi)|}$ states. Usually, like in the
cases of PDL Fischer and Ladner (1977) or $S5_{n}^{C}$ Halpern and Moses
(1992), there are finitely many such models, so it is sufficient to enumerate
them and check whether $\varphi$ holds in any. But in our case there are
infinitely many choices of $\mathsf{Bdg}$ and $\mathsf{Cost}$ functions, so
there are infinitely many models with at most $2^{|cl(\varphi)|}$ states. In
order to overcome this difficulty, we apply the technique used in Dautović et
al. (2021). The idea is to consider pre-structures
$M^{\prime}=(W,(\sim_{i})_{i\in\mathbb{AG}},P^{*},V^{c})$, in which $P^{*}$ is
a ‘pseudo’ function that emulates actual $\mathsf{Cost}$ and $\mathsf{Bdg}$
for all subformulas of $\varphi$ of the form
$\sum\limits_{i=1}^{k}a_{i}t_{i}\geq z$:

$P^{*}\colon W\times(\sum\limits_{i=1}^{k}a_{i}t_{i}\geq
z)\longrightarrow\\{true,false\\}.$

Then we can define a satisfiability relation $\vDash^{\prime}$, similarly to
Section 2.2 in all cases except $(\sum\limits_{i=1}^{k}a_{i}t_{i}\geq z)$. We
say that

$M^{\prime},w\vDash^{\prime}(\sum\limits_{i=1}^{k}a_{i}t_{i}\geq z)\text{ iff
}P^{*}(w,\sum\limits_{i=1}^{k}a_{i}t_{i}\geq z)=true.$

Since there are only finitely many such pre-structures with $\leq
2^{|cl(\varphi)|}$ states, we can enumerate them all and check if $\varphi$
holds in any of $M^{\prime}$’s according to $\vDash^{\prime}$. If it does,
then we need to check if $P^{*}$ can be replaced with
($\mathsf{Cost},\mathsf{Bdg}$). For this purpose we define a set of linear
inequalities $I(w)$ for each state $w\in M^{\prime}$, such that

  * •

$(\sum\limits_{i=1}^{k}a_{i}t_{i}\geq z)\in I(w)$ iff
$P^{*}(w,\sum\limits_{i=1}^{k}a_{i}t_{i}\geq z)=true$;

  * •

$(\sum\limits_{i=1}^{k}a_{i}t_{i}<z)\in I(w)$ iff
$P^{*}(w,\sum\limits_{i=1}^{k}a_{i}t_{i}\geq z)=false$;

  * •

$c_{i}(A)\geq 0,b_{i}\geq 0$, $c_{i}(\top)=0\in I(w)$ for all $A\in
cl(\varphi)\cap\mathcal{L}_{PL}$, $i\in\mathbb{AG}$;

  * •

$c_{i}(A)=c_{i}(B)\in I(w)$ for all $A\in cl(\varphi)\cap\mathcal{L}_{PL}$,
s.t. $A\approx B$.

It remains to find at least one solution of such system of linear inequalities
to define $(\mathsf{Cost},\mathsf{Bdg})$. But since a problem of solving a
system of linear inequalities is well-known to be decidable in polynomial time
Khachiyan (1980), then given a pre-model $M^{\prime}$ we can extend it to a
normal model ${\mathcal{M}}$ according to Section 3 in finitely many steps.

Finally, given a $\varphi$, we can enumerate finite pre-models of size at most
$2^{|cl(\varphi)|}$, solve the corresponding systems of linear inequalities to
extend these pre-models to normal models, and check whether $\varphi$ is true
in any of them. If yes, the formula is satisfiable, if not, then $\varphi$ is
unsatisfiable, since each satisfiable formula has a model of size at most
$2^{|cl(\varphi)|}$.

This algorithm gives us a NEXPTIME upper-bound, because each satisfiable
formula $\varphi$ has a model of exponential size in $|\varphi|$. So, we can
guess an exponential model ${\mathcal{M}}^{\prime}$ and a state $w$ of the
model, such that ${\mathcal{M}}^{\prime},w\vDash\varphi$, which can be checked
in polynomial time by Section 4.1. ∎

We leave finding the precise complexity bounds for future work, noting that
the satisfiability problem for $\mathsf{SPQ}$ is EXPTIME-hard from the
EXPTIME-completeness of $S5_{n}^{C}$Halpern and Moses (1992).

##  5\. Related Work

In the literature, there are several reasons to put resource constraints on
agents. One may want to deal with non-omniscient agents, and thus treat
resources as limitations on their reasoning abilities Fagin and Halpern
(1987). Similarly, Duc (1997) explores rational but non-omniscient agents. The
logics for agents as perfect reasoners who take time to derive consequences of
their knowledge were studied in Alechina and Logan (2002); Alechina et al.
(2004); Alechina and Logan (2009). In a similar vein, Balbiani et al. (2019)
proposed a logic for reasoning about the formation of beliefs through
perception or inference in non-omniscient resource-bounded agents.

One may also want to constrain agents’ strategic abilities by introducting
costs of actions. Extensions of various strategic logics, like alternating-
time temporal logic Alur et al. (2002) and coalition logic Pauly (2002), for
resource bounded agents were proposed and studied in Alechina et al. (2010);
Bulling and Farwer (2010); Alechina et al. (2011); Della Monica et al. (2011);
Alechina et al. (2014); Nguyen et al. (2015); Alechina et al. (2015); Cao and
Naumov (2017).

Our work deals with knowledge and communication in the settings, where
information available to agents might be constrained by their resources. In
such settings, resources would be treated as a cost of some ‘information
mining’ process for agents. A similar proposal introduced a logical system for
reasoning about budget-constrained knowledge Naumov and Tao (2015). This
approach, however, deals with resource bounded knowledge statically, while we
introduce a DEL-style framework. DEL-style logics with inferential actions
that require spending resources were studied in Solaki (2020, 2022);
Costantini et al. (2021). Alternatively, one can also explore agents that can
reason about epistemic formulas only up to a specific modal depth as well as
about public announcements of bounded depth Arthaud and Rinard (2023).
Finally, logics for resource-bounded agents have also been of interest in the
epistemic planning community Engesser et al. (2017); Belardinelli and Rendsvig
(2021); Bolander et al. (2021).

Finally, our work is also inspired by Fagin et al. (1990); Fagin and Halpern
(1994), where linear inequalities were introduced to reason about
probabilities. Linear inequalities were also used in a probabilistic DEL
setting Achimescu et al. (2016). An alternative way to encode linear
inequalities was proposed in Delgrande et al. (2019).

##  6\. Discussion and Future Work

In this paper we presented a dynamic epistemic logic for Semi-Public Queries
with Budgets and Costs ($\mathsf{SPQ}$) and demonstrated that this logic is
complete, decidable and has an efficient model checking procedure. We believe
that these results can find their applications in various fields of multi-
agent systems like formal verification, automated reasoning and epistemic
planning.

In order to keep the generality of our framework we have tried to impose as
few semantic restrictions as possible. Thus, we allow agents to be unaware of
the costs of some formulas for themselves as well as for other agents, and of
their and others’ budgets. The proposed framework, however, can be
straightforwardly extended to capture alternative modelling settings. Thus,
one can add axioms like (A1) $(b_{i}=k)\to K_{i}(b_{i}=k)$ and (A2)
$(c_{i}(A)=k)\to K_{i}(c_{i}(A)=k)$ to impose that all agents know their
budget and how much it would cost them to mine formulas. Some existing papers
on modelling resource bounded agents, e.g. Alechina et al. (2011), assume that
resource bounds should be represented as vectors $(r_{1},\dots,r_{k})$ of
costs of actions, where each $r_{l}\in(r_{1},\dots,r_{k})$ represents a
specific resource. In this paper, we deal with a single resource to keep the
presentation simple. However, one can also implement multiple resources in our
framework. Let $c^{l}_{i}(A)$ denote the amount of $l$’s resource required
from agent $i$ to make a query about $A$ and $b^{l}_{i}(A)$ denote the amount
of $l$’s resource that agent $i$ has. Then, the cost of $A$ and the budget of
$i$ may be represented as two vectors $(c^{1}_{i}(A),\dots,c^{k}_{i}(A))$ and
$(b^{1}_{i},\dots,b^{k}_{i})$ respectively. Now, it is relatively
straightforward to modify the proposed framework to deal with multiple
resources.

Currently, $\mathsf{SPQ}$ allows only propositional formulas $A$ to occur
under $[?_{G}^{A}]$. The extension of $\mathsf{SPQ}$, where any formula
$\varphi$ can occur in $[?_{G}^{\varphi}]$ is a matter of future work. Apart
from that, we also plan to extend our framework and allow quantification over
queries in the spirit of logics of quantified announcements, e.g. APAL
Balbiani et al. (2008), GAL Ågotnes et al. (2010), CAL Ågotnes and van
Ditmarsch (2008); Galimullin (2021), and their versions with group knowledge
Ågotnes et al. (2022); Ågotnes and Galimullin (2023). Another important
direction for future work is to consider more complicated communicative
actions (e.g. van Benthem (2007); Ciardelli and Roelofsen (2015); Baltag and
Smets (2020)) in our settings. Finally, we would also like to find tight
complexity bounds for the $\mathsf{SPQ}$ satisfiability problem.

We thank the anonymous AAMAS 2024 reviewers for their incisive and
constructive comments. This work (Vitaliy Dolgorukov) is an output of a
research project implemented as part of the Basic Research Program at the
National Research University Higher School of Economics (HSE University).

## References

  * (1)
  * Achimescu et al. (2016) Andreea Achimescu, Alexandru Baltag, and Joshua Sack. 2016\.  The probabilistic logic of communication and change.  _Journal of Logic and Computation_ 29, 7 (2016), 1015–1040.  https://doi.org/10.1093/logcom/exv084
  * Ågotnes et al. (2022) Thomas Ågotnes, Natasha Alechina, and Rustam Galimullin. 2022.  Logics with Group Announcements and Distributed Knowledge: Completeness and Expressive Power.  _Journal of Logic, Language and Information_ 31, 2 (2022), 141–166.  https://doi.org/10.1007/S10849-022-09355-0
  * Ågotnes et al. (2010) Thomas Ågotnes, Philippe Balbiani, Hans van Ditmarsch, and Pablo Seban. 2010.  Group announcement logic.  _Journal of Applied Logic_ 8, 1 (2010), 62–81.  https://doi.org/10.1016/j.jal.2008.12.002
  * Ågotnes and Galimullin (2023) Thomas Ågotnes and Rustam Galimullin. 2023.  Quantifying over information change with common knowledge.  _Autonomous Agents and Multi-Agent Systems_ 37, 1 (2023), 19\.  https://doi.org/10.1007/s10458-023-09601-0
  * Ågotnes and van Ditmarsch (2008) Thomas Ågotnes and Hans van Ditmarsch. 2008.  Coalitions and Announcements. In _Proceedings of the 7th AAMAS_ , Lin Padgham, David C. Parkes, Jörg P. Müller, and Simon Parsons (Eds.). IFAAMAS, 673–680.
  * Alechina and Logan (2002) Natasha Alechina and Brian Logan. 2002.  Ascribing Beliefs to Resource Bounded Agents. In _Proceedings of the 1st AAMAS_ , Cristiano Castelfranchi, Maria Gini, Toru Ishida, and W. Lewis Johnson (Eds.). ACM, 881–888.  https://doi.org/10.1145/544862.544948
  * Alechina and Logan (2009) Natasha Alechina and Brian Logan. 2009.  A Logic of Situated Resource-Bounded Agents.  _Journal of Logic, Language and Information_ 18, 1 (2009), 79–95.  https://doi.org/10.1007/s10849-008-9073-6
  * Alechina et al. (2010) Natasha Alechina, Brian Logan, Nguyen Hoang Nga, and Abdur Rakib. 2010.  Resource-Bounded Alternating-Time Temporal Logic. In _Proceedings of the 9th AAMAS_ , Wiebe van der Hoek, Gal A. Kaminka, Yves Lespérance, Michael Luck, and Sandip Sen (Eds.). IFAAMAS, 481–488.
  * Alechina et al. (2011) Natasha Alechina, Brian Logan, Hoang Nga Nguyen, and Abdur Rakib. 2011.  Logic for coalitions with bounded resources.  _Journal of Logic and Computation_ 21, 6 (2011), 907–937.  https://doi.org/10.1093/logcom/exq032
  * Alechina et al. (2014) Natasha Alechina, Brian Logan, Hoang Nga Nguyen, and Franco Raimondi. 2014.  Decidable Model-Checking for a Resource Logic with Production of Resources. In _Proceedings of the 21st ECAI_ , Torsten Schaub, Gerhard Friedrich, and Barry O’Sullivan (Eds.). IOS Press, 9–14.  https://doi.org/10.3233/978-1-61499-419-0-9
  * Alechina et al. (2015) Natasha Alechina, Brian Logan, Hoang Nga Nguyen, Franco Raimondi, and Leonardo Mostarda. 2015\.  Symbolic Model-Checking for Resource-Bounded ATL. In _Proceedings of the 14th AAMAS_ , Gerhard Weiss, Pinar Yolum, Rafael H. Bordini, and Edith Elkind (Eds.). IFAAMAS, 1809–1810.
  * Alechina et al. (2004) Natasha Alechina, Brian Logan, and Mark Whitsey. 2004\.  A Complete and Decidable Logic for Resource-Bounded Agents. In _Proceedings of the 3rd AAMAS_. IEEE Computer Society, 606–613.  https://doi.org/10.1109/AAMAS.2004.10090
  * Alur et al. (2002) Rajeev Alur, Thomas A. Henzinger, and Orna Kupferman. 2002\.  Alternating-time temporal logic.  _Journal of the ACM_ 49, 5 (2002), 672–713.  https://doi.org/10.1145/585265.585270
  * Arthaud and Rinard (2023) Farid Arthaud and Martin C. Rinard. 2023.  Depth-bounded Epistemic Logic. In _Proceedings of the 19th TARK_ _(EPTCS, Vol. 379)_ , Rineke Verbrugge (Ed.). 46–65.  https://doi.org/10.4204/EPTCS.379.7
  * Balbiani et al. (2008) Philippe Balbiani, Alexandru Baltag, Hans van Ditmarsch, Andreas Herzig, Tomohiro Hoshi, and Tiago de Lima. 2008.  ‘Knowable’ as ‘Known After an Announcement’.  _The Review of Symbolic Logic_ 1, 3 (2008), 305–334.  https://doi.org/10.1017/S1755020308080210
  * Balbiani et al. (2019) Philippe Balbiani, David Fernández-Duque, and Emiliano Lorini. 2019\.  The Dynamics of Epistemic Attitudes in Resource-Bounded Agents.  _Studia Logica_ 107, 3 (2019), 457–488.  https://doi.org/10.1007/s11225-018-9798-4
  * Baltag and Smets (2020) Alexandru Baltag and Sonja Smets. 2020.  Learning What Others Know. In _Proceedings of the 23rd LPAR_ _(EPiC Series in Computing, Vol. 73)_ , Elvira Albert and Laura Kovacs (Eds.). EasyChair, 90–119.  https://doi.org/10.29007/plm4
  * Belardinelli and Rendsvig (2021) Gaia Belardinelli and Rasmus K. Rendsvig. 2021.  Epistemic Planning with Attention as a Bounded Resource. In _Proceedings of the 8th LORI_ _(LNCS, Vol. 13039)_ , Sujata Ghosh and Thomas Icard (Eds.). Springer, 14–30.
  * Bolander et al. (2021) Thomas Bolander, Lasse Dissing, and Nicolai Herrmann. 2021\.  DEL-based Epistemic Planning for Human-Robot Collaboration: Theory and Implementation. In _Proceedings of the 18th KR_ , Meghyn Bienvenu, Gerhard Lakemeyer, and Esra Erdem (Eds.). 120–129.  https://doi.org/10.24963/kr.2021/12
  * Bulling and Farwer (2010) Nils Bulling and Berndt Farwer. 2010.  On the (Un-)Decidability of Model Checking Resource-Bounded Agents. In _Proceedings of the 19th ECAI_ _(Frontiers in Artificial Intelligence and Applications, Vol. 215)_ , Helder Coelho, Rudi Studer, and Michael J. Wooldridge (Eds.). IOS Press, 567–572.  https://doi.org/10.3233/978-1-60750-606-5-567
  * Cao and Naumov (2017) Rui Cao and Pavel Naumov. 2017.  Budget-Constrained Dynamics in Multiagent Systems. In _Proceedings of the 26th IJCAI_ , Carles Sierra (Ed.). 915–921.  https://doi.org/10.24963/ijcai.2017/127
  * Ciardelli and Roelofsen (2015) Ivano A. Ciardelli and Floris Roelofsen. 2015.  Inquisitive dynamic epistemic logic.  _Synthese_ 192, 6 (2015), 1643–1687.  https://doi.org/10.1007/s11229-014-0404-7
  * Costantini et al. (2021) Stefania Costantini, Andrea Formisano, and Valentina Pitoni. 2021.  An Epistemic Logic for Multi-agent Systems with Budget and Costs. In _Proceedings of the 17th JELIA_ _(LNCS, Vol. 12678)_ , Wolfgang Faber, Gerhard Friedrich, Martin Gebser, and Michael Morak (Eds.). Springer, 101–115.  https://doi.org/10.1007/978-3-030-75775-5_8
  * Dautović et al. (2021) Šejla Dautović, Dragan Doder, and Zoran Ognjanović. 2021.  An Epistemic Probabilistic Logic with Conditional Probabilities. In _Proceedings of the 17th JELIA_ _(LNCS, Vol. 12678)_ , Wolfgang Faber, Gerhard Friedrich, Martin Gebser, and Michael Morak (Eds.). Springer, 279–293.  https://doi.org/10.1007/978-3-030-75775-5_19
  * Delgrande et al. (2019) James P. Delgrande, Bryan Renne, and Joshua Sack. 2019\.  The logic of qualitative probability.  _Artificial Intelligence_ 275 (2019), 457–486.  https://doi.org/10.1016/j.artint.2019.07.002
  * Della Monica et al. (2011) Dario Della Monica, Margherita Napoli, and Mimmo Parente. 2011\.  On a Logic for Coalitional Games with Priced-Resource Agents. In _Proceedings of the 7th M4M and the 4th LAMAS_ _(ENTCS, Vol. 278)_ , Hans van Ditmarsch, David Fernández-Duque, Valentin Goranko, Wojciech Jamroga, and Manuel Ojeda-Aciego (Eds.). Elsevier, 215–228.  https://doi.org/10.1016/j.entcs.2011.10.017
  * Dolgorukov and Gladyshev (2023) Vitaliy Dolgorukov and Maksim Gladyshev. 2023.  Dynamic Epistemic Logic for Budget-Constrained Agents. In _Proceedings of the 4th DaLí_ _(LNCS, Vol. 13780)_ , Carlos Areces and Diana Costa (Eds.). Springer, 56–72.
  * Duc (1997) Ho Ngoc Duc. 1997\.  Reasoning about Rational, but not Logically Omniscient, Agents.  _Journal of Logic and Computation_ 7, 5 (1997), 633–648.  https://doi.org/10.1093/logcom/7.5.633
  * Engesser et al. (2017) Thorsten Engesser, Thomas Bolander, Robert Mattmüller, and Bernhard Nebel. 2017.  Cooperative Epistemic Multi-Agent Planning for Implicit Coordination. In _Proceedings of the 9th M4M@ICLA_ _(EPTCS, Vol. 243)_ , Sujata Ghosh and R. Ramanujam (Eds.). 75–90.  https://doi.org/10.4204/EPTCS.243.6
  * Fagin and Halpern (1987) Ronald Fagin and Joseph Y. Halpern. 1987.  Belief, awareness, and limited reasoning.  _Artificial Intelligence_ 34, 1 (1987), 39–76.  https://doi.org/10.1016/0004-3702(87)90003-8
  * Fagin and Halpern (1994) Ronald Fagin and Joseph Y. Halpern. 1994.  Reasoning about Knowledge and Probability.  _J. ACM_ 41, 2 (1994), 340–367.  https://doi.org/10.1145/174652.174658
  * Fagin et al. (1990) Ronald Fagin, Joseph Y. Halpern, and Nimrod Megiddo. 1990\.  A logic for reasoning about probabilities.  _Information and Computation_ 87, 1 (1990), 78–128.  https://doi.org/10.1016/0890-5401(90)90060-U
  * Fagin et al. (2003) Ronald Fagin, Joseph Y. Halpern, Yoram Moses, and Moshe Vardi. 2003.  _Reasoning About Knowledge_.  MIT Press.
  * Fan et al. (2015) Jie Fan, Yanjing Wang, and Hans van Ditmarsch. 2015.  Contingency and knowing whether.  _The Review of Symbolic Logic_ 8, 1 (2015), 75–107.  https://doi.org/10.1017/S1755020314000343
  * Feldman (2000) Jacob Feldman. 2000\.  Minimization of Boolean complexity in human concept learning.  _Nature_ 407, 6804 (2000), 630–633.  https://doi.org/10.1038/35036586
  * Fischer and Ladner (1977) Michael J. Fischer and Richard E. Ladner. 1977.  Propositional Modal Logic of Programs. In _Proceedings of the 9th STOC_. ACM, 286–294.  https://doi.org/10.1145/800105.803418
  * Galimullin (2021) Rustam Galimullin. 2021\.  Coalition and Relativised Group Announcement Logic.  _Journal of Logic, Language and Information_ 30, 3 (2021), 451–489.  https://doi.org/10.1007/s10849-020-09327-2
  * Galimullin and Velázquez-Quesada (2023) Rustam Galimullin and Fernando R. Velázquez-Quesada. 2023\.  (Arbitrary) Partial Communication. In _Proceedings of the 22nd AAMAS_ , Noa Agmon, Bo An, Alessandro Ricci, and William Yeoh (Eds.). ACM, 400–408.  https://doi.org/10.5555/3545946.3598663
  * Halpern and Moses (1992) Joseph Y. Halpern and Yoram Moses. 1992.  A guide to completeness and complexity for modal logics of knowledge and belief.  _Artificial Intelligence_ 54, 3 (1992), 319–379.  https://doi.org/10.1016/0004-3702(92)90049-4
  * Khachiyan (1980) L.G. Khachiyan. 1980\.  Polynomial algorithms in linear programming.  _U. S. S. R. Comput. Math. and Math. Phys._ 20, 1 (1980), 53–72.  https://doi.org/10.1016/0041-5553(80)90061-0
  * Naumov and Tao (2015) Pavel Naumov and Jia Tao. 2015.  Budget-Constrained Knowledge in Multiagent Systems. In _Proceedings of the 14th AAMAS_ , Gerhard Weiss, Pinar Yolum, Rafael H. Bordini, and Edith Elkind (Eds.). IFAAMAS, 219–226.
  * Nguyen et al. (2015) Hoang Nga Nguyen, Natasha Alechina, Brian Logan, and Abdur Rakib. 2015.  Alternating-time temporal logic with resource bounds.  _Journal of Logic and Computation_ 28, 4 (2015), 631–663.  https://doi.org/10.1093/logcom/exv034
  * Pauly (2002) Marc Pauly. 2002\.  A Modal Logic for Coalitional Power in Games.  _Journal of Logic and Computation_ 12, 1 (2002), 149–166.  https://doi.org/10.1093/logcom/12.1.149
  * Solaki (2020) Anthia Solaki. 2020\.  Bounded Multi-agent Reasoning: Actualizing Distributed Knowledge. In _Proceedings of the 3rd DaLí_ , Manuel A. Martins and Igor Sedlár (Eds.). Springer, 239–258.
  * Solaki (2022) Anthia Solaki. 2022\.  Actualizing distributed knowledge in bounded groups.  _Journal of Logic and Computation_ 33, 6 (2022), 1497–1525.  https://doi.org/10.1093/logcom/exac007
  * van Benthem (2007) Johan van Benthem. 2007\.  Dynamic Logic for Belief Revision.  _Journal of Applied Non-Classical Logics_ 17, 2 (2007), 129–155.  https://doi.org/10.3166/jancl.17.129-155
  * van Ditmarsch and Fan (2016) Hans van Ditmarsch and Jie Fan. 2016.  Propositional quantification in logics of contingency.  _Journal of Applied Non-Classical Logics_ 26, 1 (2016), 81–102.  https://doi.org/10.1080/11663081.2016.1184931
  * van Ditmarsch et al. (2008) Hans van Ditmarsch, Wiebe Hoek, and Barteld Kooi. 2008\.  _Dynamic Epistemic Logic_.  Springer.  https://doi.org/10.1007/978-1-4020-5839-4
  * Wang and Cao (2013) Yanjing Wang and Qinxiang Cao. 2013.  On Axiomatizations of Public Announcement Logic.  _Synthese_ 190, Supplement-1 (2013).  https://doi.org/10.1007/s11229-012-0233-5

## A.1 Technical Appendix

Theorem 3.1 (Soundness). The axiomatisation of $\mathsf{SPQ}$ is sound.

###### Proof.

To prove Soundness of $\mathsf{SPQ}$, we need to demonstrate that all axioms
presented in Table 1 are valid and all inference rules preserve validity. The
cases for (I1)–(I6) Fagin et al. (1990), (K)–(C) and (Neci)–(RC1) Fagin et al.
(2003); Halpern and Moses (1992) are standard and we refer to original papers.
The cases for (B+)–(c≈), (rp) and (r¬)–(rK2) are fairly simple and we omit
them. Consider the remaining cases.

Case (r≥).

${\mathcal{M}},w\vDash[?_{G}^{A}]\bigl{(}\sum\limits_{i=1}^{k}a_{i}t_{i}\geq
z\bigr{)}\text{ iff
}{\mathcal{M}},w\vDash\text{BCS}(G,A)\to\bigl{(}\sum\limits_{i=1}^{k}a_{i}t_{i}\geq
z\bigr{)}^{(G,A)}$

Note that ${\mathcal{M}},w\vDash[?_{G}^{A}](z_{1}t_{1}+\dots+z_{n}t_{n})\geq
z$ iff ${\mathcal{M}},w\vDash\text{BCS}(G,A)$ implies
${\mathcal{M}}^{?_{G}^{A}},w\vDash(z_{1}t_{1}+\dots+z_{n}t_{n})\geq z$ by
Section 2.2. Note also that
${\mathcal{M}}^{?_{G}^{A}},w\vDash(z_{1}t_{1}+\dots+z_{n}t_{n})\geq z$ is
equivalent to ${\mathcal{M}},w\vDash(z_{1}t^{*}_{1}+\dots+z_{n}t^{*}_{n})\geq
z$, where $t^{*}_{k}=t_{k}$ for $t_{k}=c_{A}$ (for all $A\in\mathcal{L}_{PL}$)
and $t_{k}=b_{j}$ (for all $j\notin G$) and if $t_{k}=b_{i}$ (for $i\in G$),
then $t^{*}_{k}=t_{k}-\frac{\min_{j\in G}(c_{j}(A))}{|G|}$. The previous claim
holds since $\mathsf{Cost}_{i}^{?_{G}^{A}}(B)=\mathsf{Cost}_{i}(B)$,
$\mathsf{Bdg}^{?_{G}^{A}}_{j}(w)=\mathsf{Bdg}_{j}(w)$ for $i\neq j$ and
$\mathsf{Bdg}^{?_{G}^{A}}_{i}(w)=\mathsf{Bdg}_{i}(w)-\frac{\min_{j\in
G}(\mathsf{Cost}_{j}(A))}{|G|}$. Then
${\mathcal{M}},w\vDash[?_{G}^{A}](z_{1}t_{1}+\dots+z_{n}t_{n})\geq z$ iff
${\mathcal{M}},w\vDash\text{BCS}(G,A)$ implies
${\mathcal{M}},w\vDash[(z_{1}t_{1}+\dots+z_{n}t_{n})\geq z)]^{(G,A)}$.

Case (rK1).

${\mathcal{M}},w\vDash[?_{G}^{A}]K_{j}\varphi\text{ iff
}{\mathcal{M}},w\vDash\text{BCS}(G,A)\to K_{j}[?_{G}^{A}]\varphi,\text{for
}j\notin G$

($\Rightarrow$) Let ${\mathcal{M}},w\vDash[?_{G}^{A}]K_{j}\varphi$ (1) and
${\mathcal{M}},w\vDash\text{BCS}(G,A)$ (2). From (1),
${\mathcal{M}},w\vDash\text{BCS}(G,A)$ implies
${\mathcal{M}}^{?_{G}^{A}},w\vDash K_{j}\varphi$ by Section 2.2. Then
${\mathcal{M}}^{?_{G}^{A}},w\vDash K_{j}\varphi$ from (2). Then $\forall
w^{\prime}:w\sim^{?_{G}^{A}}_{j}w^{\prime}\Rightarrow{\mathcal{M}}^{?_{G}^{A}},w^{\prime}\vDash\varphi$
by Section 2.2. This, together with the fact that
$w\sim^{?_{G}^{A}}_{j}w^{\prime}$ iff $w\sim_{j}w^{\prime}$,
${\mathcal{M}},w\vDash\text{BCS}(G,A)$ and
${\mathcal{M}},w^{\prime}\vDash\text{BCS}(G,A)$, implies that $\forall
w^{\prime},$ s.t. $w\sim_{j}w^{\prime}$:
${\mathcal{M}},w^{\prime}\vDash\text{BCS}(G,A)\Rightarrow{\mathcal{M}}^{?_{G}^{A}},w^{\prime}\vDash\varphi$.
This is equivalent to ${\mathcal{M}},w\vDash K_{j}[?_{i}A]\varphi$, by Section
2.2.

($\Leftarrow$) The case for ${\mathcal{M}},w\nvDash\text{BCS}(G,A)$ is
trivial. Consider only the case for
${\mathcal{M}},w\vDash\text{BCS}(G,A)\wedge K_{j}[?_{i}A]\varphi$. Then
$\forall w^{\prime}$ s.t.
$w\sim_{j}w^{\prime},{\mathcal{M}},w^{\prime}\vDash\text{BCS}(G,A)\Rightarrow{\mathcal{M}}^{?_{G}^{A}},w^{\prime}\vDash\varphi$.
Then $\forall
w^{\prime},w\sim^{?_{G}^{A}}_{j}w^{\prime}\Rightarrow{\mathcal{M}}^{?_{G}^{A}},w^{\prime}\vDash\varphi$.
By Section 2.2, ${\mathcal{M}}^{?_{G}^{A}},w\vDash K_{j}\varphi$ and hence
${\mathcal{M}},w\vDash[?_{G}^{A}]K_{j}\varphi$.

Case (rK2).

${\mathcal{M}},w\vDash[?_{G}^{A}]K_{i}\varphi\text{ iff
}{\mathcal{M}},w\vDash\text{BCS}(G,A)\to$
$\to\bigwedge\limits_{A^{\prime}\in\\{A,\neg A\\}}\Big{(}\bigl{(}A^{\prime}\to
K_{i}(A^{\prime}\to[?_{G}^{A}]\varphi)\bigr{)}\Big{)},\text{where }i\in G$

($\Rightarrow$) Let ${\mathcal{M}},w\vDash[?_{G}^{A}]K_{i}\varphi$ (1) and
${\mathcal{M}},w\vDash\text{BCS}(G,A)$ (2). From (1), (2) and Section 2.2 we
get ${\mathcal{M}}^{?_{G}^{A}},w\vDash K_{i}\varphi$. Then $\forall
w^{\prime},w\sim^{?_{G}^{A}}_{i}w^{\prime}\Rightarrow{\mathcal{M}}^{?_{G}^{A}},{w^{\prime}\vDash\varphi}$.
Assume that ${\mathcal{M}},w\vDash A$. Then $\forall w^{\prime}$, s.t.
$w\sim_{i}w^{\prime}\text{ and }{\mathcal{M}},w^{\prime}\vDash A\text{ and
}{\mathcal{M}},w^{\prime}\vDash\text{BCS}(G,A)$ implies
${\mathcal{M}}^{?_{G}^{A}},w^{\prime}\vDash\varphi$. This is equivalent to
${\mathcal{M}},w\vDash K_{i}(A\to[?_{G}^{A}]\varphi)$ by Section 2.2. Then,
from our assumption we have proved that ${\mathcal{M}},w\vDash A\to
K_{i}(A\to[?_{G}^{A}]\varphi)$. By a symmetric argument, we can show that
${\mathcal{M}},w\vDash\neg A\to K_{i}(\neg A\to[?_{G}^{A}\varphi)$.

($\Leftarrow$) The case for ${\mathcal{M}},w\nvDash\text{BCS}(G,A)$ is
trivial. Consider only the case for
${\mathcal{M}},w\vDash\text{BCS}(G,A)\wedge\bigwedge\limits_{A^{\prime}\in\\{A,\neg
A\\}}\bigl{(}A^{\prime}\to K_{i}(A^{\prime}\to[?_{G}^{A}]\varphi)\bigr{)}$.
Assume that ${\mathcal{M}},w\vDash A$. Then ${\mathcal{M}},w\vDash
K_{i}(A\to[?_{G}^{A}]\varphi)$. Similarly, assuming ${\mathcal{M}},w\vDash\neg
A$ entails ${\mathcal{M}},w\vDash K_{i}(\neg A\to[?_{G}^{A}]\varphi)$. Then
for all $w^{\prime}$, s.t. $w\sim_{i}w^{\prime}$ and $w^{\prime}$ agrees with
$w$ on the valuation of $A$ it holds that
${\mathcal{M}},w^{\prime}\vDash[?_{G}^{A}]\varphi$ and hence
${\mathcal{M}},w^{\prime}\vDash\text{BCS}(G,A)$ implies
${\mathcal{M}}^{?_{G}^{A}},w^{\prime}\vDash\varphi$. Then it holds that
$\forall
w^{\prime}:w\sim^{?_{G}^{A}}_{i}w^{\prime}\Rightarrow{\mathcal{M}}^{?_{G}^{A}},w^{\prime}\vDash\varphi$.
And hence ${\mathcal{M}}^{?_{G}^{A}},w\vDash K_{i}\varphi$. By Section 2.2,
the last claim implies ${\mathcal{M}},w\vDash[?_{G}^{A}]K_{i}\varphi$.

Case (RC2).

${\mathcal{M}}\vDash\chi\to[?_{G}^{A}]\psi\text{ and }$
${\mathcal{M}}\vDash(\chi\wedge\text{BCS}(G,A))\to\bigwedge\limits_{A^{\prime}\in\\{A,\neg
A\\}}(A^{\prime}\to E_{H\cap G}(A^{\prime}\to\chi))\wedge E_{H\setminus
G}\chi,$ $\text{ implies }{\mathcal{M}}\vDash\chi\to[?_{G}^{A}]C_{H}\psi$

Since cases for $H\cap G=\emptyset$ and $H\setminus G=\emptyset$ are trivial,
consider only the case for $H\cap G\neq\emptyset$ and $H\setminus
G\neq\emptyset$. From the antecedent we know that ${\mathcal{M}},w\vDash\chi$
implies ${\mathcal{M}}^{?_{G}^{A}},w\vDash\psi$ and
${\mathcal{M}}^{?_{G}^{A}},w\vDash E_{H}\chi$ for all $w\in W^{?_{G}^{A}}$.
The latter implies ${\mathcal{M}}^{?_{G}^{A}},w\vDash\chi$ by the reflexivity
of $\sim$. Since ${\mathcal{M}}^{?_{G}^{A}},w\vDash\psi$ for all $w\in
W^{?_{G}^{A}}$, it also holds that
${\mathcal{M}}^{?_{G}^{A}},w^{\prime}\vDash\psi$ for all
$w^{\prime}\sim^{?_{G}^{A}}_{H}w$ and then
${\mathcal{M}}^{?_{G}^{A}},w^{\prime}\vDash E_{H}\psi$. That gives us
${\mathcal{M}}^{?_{G}^{A}},w\vDash\chi\to E_{H}(\chi\wedge\psi)$. By RC1 we
get ${\mathcal{M}}^{?_{G}^{A}},w\vDash\chi\to C_{H}\psi$ and then
${\mathcal{M}},w\vDash\chi$ implies ${\mathcal{M}}^{?_{G}^{A}},w\vDash\chi\to
C_{H}\psi$ for all $w\in W^{?_{G}^{A}}$. Together with the fact that
${\mathcal{M}}^{?_{G}^{A}},w\vDash\chi$ it gives us
${\mathcal{M}},w\vDash\chi\to[?_{A}^{G}]C_{H}\psi$. ∎

Lemma 3.6 (Truth Lemma). Let ${\mathcal{M}}^{c}$ be the canonical model for
$\varphi$. For all $\psi\in cl(\varphi),w\in
W^{c}:{\mathcal{M}}^{c},w\vDash\psi$ iff $\psi\in w$.

###### Proof.

Note that the proof of the Truth Lemma is organized by the induction on a
_complexity_ measure for $\varphi$, denoted $c(\varphi)$. We define this
_complexity_ measures as follows.

Definition ( Formula Complexity). The complexity
$c:\mathcal{L}_{\mathsf{SPQ}}\to\mathbb{N}$ of $\mathsf{SPQ}$ formulas is
defined as follows:
(1) $c(p)=1$;
(2) $c((z_{1}t_{1}+\dots+z_{n}t_{n})\geq z)=1$;
(3) $c(\neg\varphi)=c(\varphi)+1$;
(4) $c(\varphi\wedge\psi)=\max\\{c(\varphi),c(\psi)\\}+1$;
(5) $c(K_{i}\varphi)=c(\varphi)+1$;
(6) $c(C_{G}\varphi)=c(\varphi)+1$;
(7) $c([?_{G}^{A}]\varphi)=(c(A)+5)\cdot c(\varphi)$;

The number 5 in this Definition seems arbitrary, but we may take take any
natural number that gives us the following properties.

Proposition. For all $\psi,\varphi,\chi\in\mathcal{L}(\mathsf{SPQ})$ and all
$A\in\mathcal{L}_{PL}$

  1. (1)

$c(\psi)\geq c(\varphi)$, for all $\varphi\in\mathsf{Sub}(\psi)$

  2. (2)

$c([?_{G}^{A}]p)>c(\text{BCS}(G,A)\to p)$

  3. (3)

$c([_{G}A]\bigl{(}\sum\limits_{i=1}^{k}a_{i}t_{i}\geq
z\bigr{)})>c\Big{(}\Big{(}\text{BCS}(G,A)\to\bigl{(}\sum\limits_{i=1}^{k}a_{i}t_{i}\geq
z\bigr{)}^{(G,A)}\Big{)}\Big{)}$

  4. (4)

$c([?_{G}^{A}]\neg\varphi)>c(\text{BCS}(G,A)\to\neg[?_{G}^{A}]\varphi)$

  5. (5)

$c([?_{G}^{A}](\varphi\wedge\psi))>c([?_{G}^{A}]\varphi\wedge[?_{G}^{A}]\psi)$

  6. (6)

$c([?_{G}^{A}]K_{j}\varphi)>c(\text{BCS}(G,A)\to K_{j}[?_{G}^{A}]\varphi)$,
where $j\notin G$

  7. (7)

$c([?_{G}^{A}]K_{i}\varphi\leftrightarrow\text{BCS}(G,A))>c(\bigwedge\limits_{A^{\prime}\in\\{A,\neg
A\\}}\Big{(}\bigl{(}A^{\prime}\to
K_{i}(A^{\prime}\to[?_{G}^{A}]\varphi)\bigr{)}\Big{)})$, where $i\in G$

  8. (8)

$c([?_{G}^{A}]C_{H}\varphi)>c([?_{G}^{A}]\varphi)$

∎