# Depth-Bounded Epistemic Planning (Preprint)

Thomas Bolander1 Alessandro Burigana2 Marco Montali2
1Technical University of Denmark, Denmark
2Free University of Bozen-Bolzano, Italy
<EMAIL_ADDRESS>{burigana<EMAIL_ADDRESS>
###### Abstract

In this paper, we propose a novel algorithm for epistemic planning based on
dynamic epistemic logic (DEL). The novelty is that we limit the depth of
reasoning of the planning agent to an upper bound $b$, meaning that the
planning agent can only reason about higher-order knowledge to at most (modal)
depth $b$. The algorithm makes use of a novel type of canonical
$b$-bisimulation contraction guaranteeing unique minimal models with respect
to $b$-bisimulation. We show our depth-bounded planning algorithm to be sound.
Additionally, we show it to be complete with respect to planning tasks having
a solution within bound $b$ of reasoning depth (and hence the iterative bound-
deepening variant is complete in the standard sense). For bound $b$ of
reasoning depth, the algorithm is shown to be $(b+1)$-ExpTime complete, and
furthermore fixed-parameter tractable in the number of agents and atoms. We
present both a tree search and a graph search variant of the algorithm, and we
benchmark an implementation of the tree search version against a baseline
epistemic planner.

##  1 Introduction

_Automated planning_ is of central concern in symbolic AI research, with
applications in logistics and robotics. In the simple case of an agent
operating in a known world using deterministic actions, the output of a
planner is just a sequence of actions to be performed to the effect that it
achieves a desired goal state. _Epistemic planning_ is the enrichment of
planning with epistemic notions, in particular knowledge and belief, including
higher-order knowledge, knowledge about what other agents know, knowledge
about what someone knows about someone else, etc. In general, epistemic
planning considers the following problem: given a current state of knowledge
of the agents, and a desirable state of knowledge, how do one get from one to
the other?

One possible framework for epistemic planning is dynamic epistemic logic (DEL)
(?). Using DEL for epistemic planning was first pursued by ? (?), but
independently conceived by several other researchers (?; ?; ?). Recently, a
special issue of the journal Artificial Intelligence (AIJ) was devoted to
epistemic planning (?).

Unrestricted epistemic planning based on DEL is undecidable, meaning that its
plan existence problem is undecidable (?). Several more well-behaved fragments
of epistemic planning exist, where one of the possible approaches is to
restrict the modal depth of the pre- and postconditions of epistemic actions
(?). However, a maybe even more natural approach to taming the complexity of
epistemic planning is to limit the reasoning depth of the planning agent,
limit the depth of higher-order reasoning that the agent can perform. This is
however not completely trivial to define in DEL-based epistemic planning as
states are represented semantically as Kripke models. In this paper, we show
how to use a novel type of bounded bisimulation contractions to define a
notion of depth-bounded epistemic planning. We provide an algorithm for
computing depth-bounded epistemic plans, show soundness, completeness and
complexity results for it, and provide an empirical evaluation of the
algorithm.

##  2 Preliminaries

We now recall the main notions in Dynamic Epistemic Logic. For a more complete
overview, consult ? (?). Following the DEL methodology, we split our
exposition in three parts covering _epistemic models_ , _event models_ and
_product update_. Finally, we recall the definition of the plan existence
problem.

### Epistemic Models

Let $\mathcal{P}$ be a countable set of atomic propositions and $\mathcal{AG}$
a countable set of agents. The language $\mathcal{L}$ of _multi-agent
epistemic logic_ is defined by the BNF:

$\varphi::=p\mid\neg\varphi\mid\varphi\wedge\varphi\mid\Box_{i}\varphi$

where $p\in\mathcal{P}$ and $i\in\mathcal{AG}$. Formulae of the form
$\Box_{i}\varphi$ are read as “agent $i$ knows/believes that $\varphi$”. We
define the symbols $\top$, $\bot$, $\vee$, $\rightarrow$ and $\Diamond_{i}$ as
usual. _Modal depth_ is defined inductively on the structure of formulae of
$\mathcal{L}$: $md(p)=0$ (for $p\in\mathcal{P}$),
$md(\neg\varphi)=md(\varphi)$,
$md(\varphi_{1}\land\varphi_{2})=\max\\{md(\varphi_{1}),md(\varphi_{2})\\}$
and $md(\Box_{i}\varphi)=1+md(\varphi)$.

######  Definition 1 (Epistemic Model and State).

An _(epistemic) model_ of $\mathcal{L}$ is a triple $M=(W,R,L)$ where:

  * •

$W\neq\varnothing$ is a finite set of _(possible) worlds_ ;

  * •

$R:\mathcal{AG}^{\prime}\to 2^{W\times W}$ assigns an _accessibility relation_
$R_{i}$ to each agent $i$ in a finite subset
$\mathcal{AG}^{\prime}\subseteq\mathcal{AG}$;

  * •

$L:W\rightarrow 2^{\mathcal{P}}$ assigns to each world $w$ a _label_ $L(w)$,
being a finite set of atoms.

An _(epistemic) state_ of $\mathcal{L}$ is a pair $(M,w_{d})$, where $w_{d}\in
W$ is the _designated world_.

Intuitively, the designated world $w_{d}$ is considered to be the actual world
from the perspective of an omniscient observer. We also use the infix notation
$wR_{i}v$ to denote $(w,v)\in R_{i}$. For any $X,Y\subseteq W$, $XR_{i}Y$
denotes the fact that $\exists x\in X\exists y\in Y(xR_{i}y)$. Moreover,
$R_{i}(x)=\\{y\in W\mid xR_{i}y\\}$ and $R_{i}(X)=\\{y\in W\mid\exists x\in
X(xR_{i}y)\\}$.

######  Definition 2.

Let $M=(W,R,L)$ be a model and $w\in W$.

$\begin{array}[]{@{}lll}(M,w)\models p&\text{ iff }&p\in L(w)\\\
(M,w)\models\neg\varphi&\text{ iff }&(M,w)\not\models\varphi\\\
(M,w)\models\varphi\wedge\psi&\text{ iff }&(M,w)\models\varphi\text{ and
}(M,w)\models\psi\\\ (M,w)\models\Box_{i}\varphi&\text{ iff }&\text{for all
}v,\text{ if }wR_{i}v\text{ then }(M,v)\models\varphi\end{array}$

For instance, $(M,w)\models p$ means that $p$ is true in $w$;
$(M,w)\models\Diamond_{i}p$ means that agent $i$ considers $\varphi$ to be
possible in $w$; $(M,w)\models\Box_{i}\varphi$ means that $i$ knows/believes
$\varphi$ in $w$, as $\varphi$ holds in all worlds that $i$ considers
possible.

ptpt$w_{0}{:}$ $\mathit{has}(a,5)$ $\mathit{has}(b,4)$ pt$w_{1}{:}$
$\mathit{has}(a,3)$ $\mathit{has}(b,4)$ pt$w_{2}{:}$ $\mathit{has}(a,3)$
$\mathit{has}(b,2)$ pt$w_{3}{:}$ $\mathit{has}(a,1)$
$\mathit{has}(b,2)$pt$w_{4}{:}$ $\mathit{has}(a,1)$ $\mathit{has}(b,0)$
ptpt$b$ptpt$a$ptpt$b$ptpt$a$ptpt$a,b$ptpt$a,b$ptpt$a,b$ptpt$a,b$ptpt$a,b$

Figure 1: Epistemic state of Example 1. Bullets represent worlds, labelled by
their name and the atoms they satisfy. The circled bullet is the designated
world. Edges denote the accessibility relations.

######  Example 1 (Epistemic State).

In the Consecutive Number Puzzle (?), two agents, Anne ($a$) and Bob ($b$),
are given two consecutive numbers $n_{a},n_{b}$ between $0$ and $N$. Both
agents know that this happens, but they only get to see their own number. We
denote with $\mathit{has}(i,n)$ the fact that agent $i$ has number $n$. Figure
1 shows an epistemic state representing the case for $N=5$ where agents $a$
and $b$ are given numbers $3$ and $4$, respectively. Note that both agents
know their number, agent $b$ doesn’t know whether agent $a$ has number $3$ or
$5$ and, similarly, $a$ doesn’t know whether $b$ has $2$ or $4$. Moreover, in
world $w_{2}$, $b$ doesn’t know whether $a$ has $1$ or $3$, and so on until
world $w_{4}$.

We say that two epistemic states $s$ and $s^{\prime}$ _agree on_ (the formulas
of) a set $\Phi\subseteq\mathcal{L}$ if, for all $\phi\in\Phi$, $s\models\phi$
iff $s^{\prime}\models\phi$. We recall below the notions of bisimulation and
bounded bisimulation ($b$-bisimulations) (?; ?).

######  Definition 3 (Bisimulation).

Let $s=(M,w_{d})$ and $s^{\prime}=(M^{\prime},w^{\prime}_{d})$ be two
epistemic states, with $M=(W,R,L)$ and
$M^{\prime}=(W^{\prime},R^{\prime},L^{\prime})$. A _bisimulation_ between $s$
and $s^{\prime}$ is a non-empty binary relation $Z\subseteq W\times
W^{\prime}$ with $(w_{d},w^{\prime}_{d})\in Z$ and satisfying:

  * •

[atom] If $(w,w^{\prime})\in Z$, then $L(w)=L(w^{\prime})$.

  * •

[forth] If $(w,w^{\prime})\in Z$ and $wR_{i}v$, then there exists
$v^{\prime}\in W^{\prime}$ such that $w^{\prime}R^{\prime}_{i}v^{\prime}$ and
$(v,v^{\prime})\in Z$.

  * •

[back] If $(w,w^{\prime})\in Z$ and $w^{\prime}R^{\prime}_{i}v^{\prime}$, then
there exists $v\in W$ such that $wR_{i}v$ and $(v,v^{\prime})\in Z$.

If a bisimulation between $s$ and $s^{\prime}$ exists, we say that $s$ and
$s^{\prime}$ are _bisimilar_ , denoted $s\leftrightarroweq s^{\prime}$. When
$(M,w)\leftrightarroweq(M,w^{\prime})$ for some worlds $w,w^{\prime}$ of the
same model $M$, we simply write $w\leftrightarroweq w^{\prime}$, and say that
$w$ and $w^{\prime}$ are _bisimilar_. We denote the _bisimulation
(equivalence) class_ of a world $w\in W$ as $[w]_{\leftrightarroweq}=\\{v\in
W\mid w\leftrightarroweq v\\}$.

######  Proposition 1 (? ?).

Two pointed models are bisimilar iff they agree on $\mathcal{L}$.

######  Definition 4.

Let $b\geq 0$ and let $s=(M,w_{d})$ and
$s^{\prime}=(M^{\prime},w^{\prime}_{d})$ be two epistemic states, with
$M=(W,R,L)$ and $M^{\prime}=(W^{\prime},R^{\prime},L^{\prime})$. A _$b$
-bisimulation_ between $s$ and $s^{\prime}$ is a sequence of non-empty binary
relations $Z_{k}\subseteq\cdots\subseteq Z_{0}\subseteq W\times W^{\prime}$
with $(w_{d},w^{\prime}_{d})\in Z_{k}$ and satisfying, for all $h<b$:

  * •

[atom] If $(w,w^{\prime})\in Z_{0}$, then $L(w)=L(w^{\prime})$.

  * •

[forthh] If $(w,w^{\prime})\in Z_{h+1}$ and $wR_{i}v$, then there exists
$v^{\prime}\in W^{\prime}$ such that $w^{\prime}R^{\prime}_{i}v^{\prime}$ and
$(v,v^{\prime})\in Z_{h}$.

  * •

[backh] If $(w,w^{\prime})\in Z_{h+1}$ and
$w^{\prime}R^{\prime}_{i}v^{\prime}$, then there exists $v\in W$ such that
$wR_{i}v$ and $(v,v^{\prime})\in Z_{h}$.

If a $b$-bisimulation between $s$ and $s^{\prime}$ exists, we say that $s$ and
$s^{\prime}$ are _$b$ -bisimilar_, denoted $s\leftrightarroweq_{b}s^{\prime}$.
When $(M,w)\leftrightarroweq_{b}(M,w^{\prime})$ for some worlds $w,w^{\prime}$
of the same model $M$, we simply write $w\leftrightarroweq_{b}w^{\prime}$, and
say that $w$ and $w^{\prime}$ are _$b$ -bisimilar_. We denote the _$b$
-bisimulation (equivalence) class_ of a world $w\in W$ as $[w]_{b}=\\{v\in
W\mid w\leftrightarroweq_{b}v\\}$.

Note that a $b$-bisimulation between epistemic states is also an
$h$-bisimulation for all $h\leq b$, and hence that $b$-bisimilar worlds are
also $h$-bisimilar for all $h\leq b$.

######  Proposition 2 (? ?).

Two epistemic states are $b$-bisimilar iff they agree on
$\\{\phi\in\mathcal{L}\mid\mathit{md}(\phi)\leq b\\}$, on all of formulas up
to modal depth $b$.

######  Definition 5.

Let $(M,w_{d})$ be an epistemic state. The _depth_ $0pt{w}$ of a world $w$ is
the length of the shortest path from $w_{d}$ to $w$ ($\infty$ if no such path
exists). Given $d\geq 0$, the _restriction_ $M\upharpoonright d$ of $M$ to $d$
is the sub-model containing all worlds with depth at most $d$ (and preserving
all edges between them).

### Event Models

_Event models_ represent information and ontic change in DEL. We use them to
represent actions that agents can perform, where the individual events
represent different perspectives on the action. To each event is associated a
_precondition_ , which specifies when such event may occur, and
_postconditions_ , which determine how the event changes the information of an
epistemic state.

######  Definition 6 (Event Model and Action).

An _event model_ of $\mathcal{L}$ is a tuple
$A=(E,Q,\mathit{pre},\mathit{post})$ where:

  * •

$E\neq\varnothing$ is a finite set of _events_ ;

  * •

$Q:\mathcal{AG}^{\prime}\rightarrow 2^{E\times E}$ assigns an _accessibility
relation_ $Q_{i}$ to each agent $i$ in a finite subset
$\mathcal{AG}^{\prime}\subseteq\mathcal{AG}$;

  * •

$\mathit{pre}:E\rightarrow\mathcal{L}$ assigns to each event a _precondition_
;

  * •

$\mathit{post}:E\rightarrow(\mathcal{P}\rightarrow\mathcal{L})$ assigns to
each event $e$ a _postcondition map_ $post(e):\mathcal{P}\to\mathcal{L}$ with
$post(e)(p)=p$ on a cofinite subset of $P$.111We can identify postcondition
maps $post(e)$ with their induced finite sets $\\{(p,\phi)\mid
post(e)(p)=\phi\text{ and }\phi\neq p\\}$.

An _action_ of $\mathcal{L}$ is a pair $(A,e_{d})$ where $e_{d}\in E$ is the
_designated event_.

Similarly to epistemic states, the designated event $e_{d}$ represents the
actual event taking place. We also use infix notation $eQ_{i}f$ for $(e,f)\in
Q_{i}$. The maximal modal depth among the pre- and postconditions in an action
$\alpha$ is denoted $\mathit{md}(\alpha)$.

$e:\langle\varphi,\varnothing\rangle$$\mathit{ann}(\varphi)=$$a,b$

Figure 2: Action $\mathit{ann}(\varphi)$ of Example 2 with
$\mathcal{AG}^{\prime}=\\{a,b\\}$. An event $e$ is denoted by a square labeled
by $\langle\mathit{pre}(e),\mathit{post}(e)\rangle$. The designated event is
denoted by a boxed square.

######  Example 2 (Action).

The _public announcement_ $\mathit{ann}(\varphi)$ of a formula $\varphi$ is
the action shown in Figure 2. Consider again Example 1. Letting
$\psi_{i,j}=\bigvee_{0\leq k\leq N}\Box_{i}\mathit{has}(j,k)$, the action
$\mathit{ann}(\mathit{\neg\psi_{b,a}})$ is the public announcement of the fact
that “Bob doesn’t know the number of Anne”.

### Product Update

The _product update_ formalizes the execution of an action $(A,e_{d})$ on a
given state $(M,w_{d})$. Intuitively, the resulting epistemic state
$(M^{\prime},w_{d}^{\prime})$ is computed by a cross product between the
worlds in $M$ and the events in $A$. A pair $(w,e)$ represents the world of
$M^{\prime}$ that results from applying the event $e$ on the world $w$. We say
that $(A,e_{d})$ is _applicable_ in $(M,w_{d})$ iff
$(M,w_{d})\models\mathit{pre}(e_{d})$.

######  Definition 7 (Product Update).

Let $(A,e_{d})$ be an action applicable in an epistemic state $(M,w_{d})$,
where $M=(W,R,L)$ and $A=(E,Q,\mathit{pre},\mathit{post})$. The _product
update_ of $(M,w_{d})$ with $(A,e_{d})$ is the epistemic state
$(M,W_{d})\otimes(A,e_{d})=((W^{\prime},R^{\prime},L^{\prime}),(w_{d},e_{d}))$,
where:

$\displaystyle W^{\prime}$ $\displaystyle=\\{(w,e)\in
W{\times}E\mid(M,w)\models\mathit{pre}(e)\\}$ $\displaystyle R^{\prime}_{i}$
$\displaystyle=\\{((w,e),(v,f))\in W^{\prime}{\times}W^{\prime}\mid
wR_{i}v\text{ and }eQ_{i}f\\}$ $\displaystyle L^{\prime}((w,e))$
$\displaystyle=\\{p\in\mathcal{P}\mid(M,w)\models\mathit{post}(e)(p)\\}$

ptpt$v_{0}{:}$ $\mathit{has}(a,5)$ $\mathit{has}(b,4)$ pt$v_{1}{:}$
$\mathit{has}(a,3)$ $\mathit{has}(b,4)$ pt$v_{2}{:}$ $\mathit{has}(a,3)$
$\mathit{has}(b,2)$ pt$v_{3}{:}$ $\mathit{has}(a,1)$
$\mathit{has}(b,2)$ptpt$b$ptpt$a$ptpt$b$ptpt$a,b$ptpt$a,b$ptpt$a,b$ptpt$a,b$

Figure 3: State $s\otimes\mathit{ann}(\neg\psi_{b})$, where $s$ is the state
in Figure 1.

######  Example 3 (Update).

Let $s$ be the state shown in Figure 1 and consider the action
$\mathit{ann}(\neg\psi_{b,a})$ of Example 2. The epistemic state
$s\otimes\mathit{ann}(\neg\psi_{b,a})$ is shown in Figure 3. Note that the
only world of $s$ where $\neg\psi_{b,a}$ does not hold is $w_{4}$, since in
this world Bob knows that Anne has number $1$. Thus, after the update, all
worlds are preserved but $w_{4}$.

######  Proposition 3 (? ?).

Let $s\leftrightarroweq s^{\prime}$ and let $\alpha$ be an action applicable
in both $s$ and $s^{\prime}$. Then, $s\otimes\alpha\leftrightarroweq
s^{\prime}\otimes\alpha$.

This result was later generalized by ? and it will play a central role in the
rest of the paper.

######  Proposition 4 (? ?).

Let $s\leftrightarroweq_{b}s^{\prime}$ and let $\alpha$ be an action
applicable in both $s$ and $s^{\prime}$ with $\mathit{md}(\alpha)\leq b$.
Then,
$s\otimes\alpha\leftrightarroweq_{b-\mathit{md}(\alpha)}s^{\prime}\otimes\alpha$.

### Epistemic Planning

We recall the notions of epistemic planning task and solution (?).

######  Definition 8.

An _(epistemic) planning task_ is a triple $T=(s_{0},\mathcal{A},$
$\varphi_{g})$, where $s_{0}$ is an epistemic state (the _initial state_);
$\mathcal{A}$ is a finite set of actions; $\varphi_{g}\in\mathcal{L}$ is the
_goal formula_.

######  Definition 9.

A _solution_ (or _plan_) to a planning task $(s_{0},$
$\mathcal{A},\varphi_{g})$ is a finite sequence
$\alpha_{1},\dots,\alpha_{\ell}$ of actions of $\mathcal{A}$ where:

  1. 1.

For all $1{\leq}k{\leq}\ell$, $\alpha_{k}$ is applicable in
$s_{0}{\otimes}\alpha_{1}{\otimes}{\dots}{\otimes}\alpha_{k{-}1}$;

  2. 2.

$s_{0}\otimes\alpha_{1}\otimes\dots\otimes\alpha_{\ell}\models\varphi_{g}$.

##  3 Rooted $b$-Contractions

A significant challenge for epistemic planners is to handle the rapid growth
of the size of states following updates. Typically, planners make use of
bisimulation contractions to obtain smaller (modally equivalent) states after
each update (?; ?; ?). In this paper, we seek to model agents with a bound on
their reasoning depth (a bound on the model depth of formulas they can reason
about). Instead of considering standard bisimulation contractions, we hence
make use of $b$-bisimulation contractions (defined formally below). That is,
after an update, we take the $b$-contraction of the resulting state, thereby
obtaining a minimal state satisfying the same formulas up to modal depth $b$.
A notion of $b$-contraction has already been used in epistemic planning (?;
?). There the $b$-contraction of an epistemic state $s=((W,R,L),w_{d})$,
denoted ${\lfloor s\rfloor}_{b}$, is defined as the quotient structure of $s$
wrt. $\leftrightarroweq_{b}$, namely ${\lfloor
s\rfloor}_{b}=((W^{\prime},R^{\prime},L^{\prime}),[w_{d}]_{b})$, where
$W^{\prime}=\\{[w]_{b}\mid w\in W\\}$,
$R^{\prime}_{i}=\\{([w]_{b},[v]_{b})\mid wR_{i}v\\}$, and
$L^{\prime}([w]_{b})=L(w)$. We call this the _standard $b$-contraction_ of
$s$. However, unfortunately ${\lfloor s\rfloor}_{b}$ is not always minimal
among the states $b$-bisimilar to $s$, as the following example shows.

$w_{b-1}{:}p$$s={\lfloor
s\rfloor}_{b}=$$w_{b-2}{:}p$$w_{1}{:}p$$w_{0}{:}p$$w^{\prime}_{b-1}{:}p$${\llfloor
s\rrfloor}_{b}^{<}=$

Figure 4: Standard (${\lfloor s\rfloor}_{b}$) and rooted (${\llfloor
s\rrfloor}_{b}^{<}$) $b$-contractions of chain $s$ (symbol ${\llfloor
s\rrfloor}_{b}^{<}$ is borrowed from Definition 14). As we consider only one
agent, we omit arrows labels.

######  Example 4 (? ?).

Consider the chain model $s$ in Figure 4 (left). Since $p$ is true in all
worlds, and the length of the chain is $b$, a minimal model $b$-bisimilar to
$s$ is a singleton epistemic state with a loop (Figure 4, right). This is
because the loop model preserves all formulas up to depth $b$, cf. Proposition
2. However, the standard $b$-contraction of $s$ is simply $s$ itself, as no
two worlds of $s$ satisfy the same formulas up to depth $b$.

Recently, ? (?) developed a novel type of $b$-contraction, called _rooted
$b$-contraction_ that actually guarantees contracted states to be minimal. We
here repeat the definition and minimality result, but refer the reader to the
aforementioned paper for further details. _In the rest of this section, we
will suppose given a constant $b\geq 0$ and an epistemic state $s=(M,w_{d})$,
with $M=(W,R,L)$_.

######  Definition 10.

The _bound_ of a world $w\in W$ is $b(w)=b-0pt{w}$, where $0pt{w}$ is the
depth of $w$ (Definition 5).

######  Lemma 1 (? ?).

For every world $w$ of $M\upharpoonright b$, we have $(M\upharpoonright
b,w)\leftrightarroweq_{b(w)}(M,w)$.

Intuitively, Lemma 1 states that, given a formula $\varphi$ of modal depth up
to $b$, the restriction of $M$ to $b$ contains all the worlds that are
necessary to determine whether $\varphi$ is true in $(M,w_{d})$ (since
$b(w_{d})=b$, and therefore $(M\upharpoonright
b,w_{d})\leftrightarroweq_{b}(M,w_{d})$, which means that $(M\upharpoonright
b,w_{d})$ and $(M,w_{d})$ satisfy the same formulas up to modal depth $b$).
Note that if there are two worlds $x,y$ such that $b(x)\geq b(y)$ and
$x\leftrightarroweq_{b(y)}y$, then by Lemma 1 we get $(M\upharpoonright
b,x)\leftrightarroweq_{b(y)}(M\upharpoonright b,y)$, namely, the restriction
of $M$ to $b$ is sufficient to determine the truth of formulas up to modal
depth $b(y)$ in both $x$ and $y$. Moreover, since $b(x)\geq b(y)$, in general
$x$ and $y$ might not be $b(x)$-bisimilar, which implies $(M\upharpoonright
b,x)\not\leftrightarroweq_{b(x)}(M\upharpoonright b,y)$. Thus, the truth of
formulas at $y$ up to modal depth $b(y)$ can always be determined in the sub-
model of depth $b(x)$ rooted in $x$, however, the truth of formulas at $x$ up
to modal depth $b(x)$ can not always be checked in the sub-model of depth
$b(y)$ rooted in $y$. This leads to the next definition.

######  Definition 11 (? ?).

Let $x,y$ be worlds of $M$ with $b(x)\geq 0$ and $b(y)\geq 0$. We say that $x$
_represents_ $y$, denoted $x\succeq y$, if $b(x)\geq b(y)$ and
$x\leftrightarroweq_{b(y)}y$. If furthermore $b(x)>b(y)$, we say that $x$
_strictly represents_ $y$, denoted by $x\succ y$. The set of _maximal
representatives_ of $W$ is the set of worlds $W^{\max}=\\{x\in W\mid b(x)\geq
0\textnormal{ and }\neg\exists y\in W(y\succ x)\\}$. We say that a world $x$
is a _maximal representative_ of $y$ if $x\in W^{\max}$ and $x\succeq y$.

Note that every world $w$ with $b(w)\geq 0$ has at least one maximal
representative: Any chain $w\prec w^{\prime}\prec w^{\prime\prime}\prec\cdots$
is finite (since $W$ is finite) and must hence end in a maximal representative
of $w$. Rooted $b$-contractions are built on the maximal representatives, the
intuition being that all other worlds can be represented by one of these and
hence deleted.

######  Definition 12.

The _representative class_ of $w\in W$ is the class $[w]_{b(w)}$, which we
compactly denote as $\llbracket w\rrbracket$.

######  Definition 13.

Let $<$ be a total order on $W$ and let $0\leq h\leq b$. The _least
$h$-representative_ of $w\in W$ is the world $\min_{h}(w)=\min_{<}\\{v\in
W^{\max}\mid v\leftrightarroweq_{h}w\\}$.

######  Definition 14 (? ?).

Let $<$ be a total order on $W$. The _rooted $b$-contraction_ of $s$ wrt. $<$
is the state ${\llfloor
s\rrfloor}_{b}^{<}=((W^{\prime},R^{\prime},L^{\prime}),\llbracket
w_{d}\rrbracket)$, where:

  * •

$W^{\prime}=\\{\llbracket x\rrbracket\mid x\in W^{\max}\\}$;

  * •

$R^{\prime}_{i}=\\{(\llbracket
x\rrbracket,\llbracket\min_{b(x){-}1}(y)\rrbracket)\mid x\in W^{\max},xR_{i}y$
and $b(x)>0\\}$;

  * •

$L^{\prime}(\llbracket x\rrbracket)=L(x)$, for all $\llbracket x\rrbracket\in
W^{\prime}$.

######  Theorem 1 (? ?).

Let $s$ be an epistemic state and let $b\geq 0$. Then, ${\llfloor
s\rrfloor}_{b}^{<}$ is a minimal epistemic state $b$-bisimilar to $s$.

##  4 Canonical $b$-Contractions

We now present an extension and improvement of the results of ? (?) that will
be useful for our bounded-depth planning algorithm. To preserve small
epistemic states, planners typically take the bisimulation contraction of each
computed state (?; ?), where the _bisimulation contraction_ of
$s=((W,R,L),w_{d})$, denoted ${\lfloor s\rfloor}$, is defined as the quotient
structure of $s$ wrt. $\leftrightarroweq$, namely ${\lfloor
s\rfloor}=((W^{\prime},R^{\prime},L^{\prime}),[w_{d}]_{\leftrightarroweq})$,
where $W^{\prime}=\\{[w]_{\leftrightarroweq}\mid w\in W \\}$,
$R_{i}^{\prime}=\\{([w]_{\leftrightarroweq},[v]_{\leftrightarroweq})\mid
wR_{i}v\\}$, and $L^{\prime}([w]_{\leftrightarroweq})=L(w)$. A very common and
important operation during planning is checking whether a state has already
previously been reached. When working with bisimulation contracted states,
this amounts to checking whether the new state is bisimilar to a previously
computed state. However, checking for bisimilarity after first having computed
the bisimulation contraction of course incurs an extra cost, and ? (?) show
how this can be avoided by devising a so-called _ordered partition refinement_
technique for computing bisimulation contractions guaranteeing two bisimilar
states to have _identical_ bisimulation contractions. Using this technique,
checking whether a computed (contracted) state already exists in the search
tree amounts to check for identity of (contracted) states.222In ? (?), doing
bisimulation contractions is not only for practical efficiency of the planner
but also to guarantee uniformity of the generated policies. In the present
work, we are only interested in preserving the truth of formulas up to modal
depth $b$, and hence we want to compute the rooted $b$-contraction of each
state instead of its standard bisimulation contraction. We then run into the
same issue regarding the need to check whether two $b$-contracted states are
$b$-bisimilar. In this section we will show how to define a notion of
_canonical $b$-contractions_ that guarantees two $b$-bisimilar states to have
identical contractions.

$w_{d}{:}p$$w_{1}{:}q$$~{}w_{2}{:}q$$w_{3}{:}r$$w_{4}{:}r$ (a)

$~{}[w_{d}]_{3}{:}p$$[w_{1}]_{2}{:}q$$~{}~{}[w_{2}]_{2}{:}q$$[w_{3}]_{1}{:}r$$[w_{4}]_{1}{:}r$
(b)

$~{}[w_{d}]_{3}{:}p$$[w_{2}]_{2}{:}q$$~{}~{}[w_{1}]_{2}{:}q$$[w_{3}]_{1}{:}r$$[w_{4}]_{1}{:}r$
(c)

Figure 5: Epistemic states $s$ (left), ${\llfloor s\rrfloor}_{3}^{<}$ (center)
and ${\llfloor t\rrfloor}_{3}^{<}$ (right).

######  Example 5.

Let $s$ be the pointed model in Figure 5 (left) with
$W=\\{w_{d},w_{1},\dots,w_{4}\\}$, and let $<$ be the following total order on
$W$: $w_{d}<w_{1}<w_{2}<w_{3}<w_{4}$. Let $b=3$. Then $b(w_{d})=3$,
$b(w_{1})=b(w_{2})=2$, and $b(w_{3})=b(w_{4})=1$. Since no two worlds of $W$
are $1$-bisimilar, it follows that all worlds of $W$ are maximal
representatives, $W^{\max}=W$. The rooted $b$-contraction of $s$ is shown in
Figure 5 (center). Since $W^{\max}=W$, for each world $w\in W$, ${\llfloor
s\rrfloor}_{3}^{<}$ contains the world $\llbracket w\rrbracket=[w]_{b(w)}$.
The contraction only differs from the original model by the deletion of a
single “unnecessary” edge. Now let $t$ be an epistemic state equal to $s$,
except that we rename $w_{1}$ as $w_{2}$ and, vice versa, $w_{2}$ as $w_{1}$.
Clearly $s$ and $t$ are isomorphic, but ${\llfloor s\rrfloor}_{3}^{<}$ and
${\llfloor t\rrfloor}_{3}^{<}$ are not! The rooted $b$-contraction of $t$ is
shown in Figure 5 (right). We still delete an unnecessary edge, but this time
a different one (since it depends on the order $<$). This shows that rooted
$b$-contractions don’t ensure unique representatives of classes of
$b$-bisimilar states.

We now provide a novel and revised definition of $b$-contractions, called
_canonical $b$-contractions_, guaranteeing a unique representative of each
class of $b$-bisimilar states. We first need unique identifiers for
$h$-bisimilar worlds. We do this by introducing a notion of _$h$ -signature_,
inspired by ? (?).

######  Definition 15.

Let $h\geq 0$. By mutual recursion we define the _$h$ -signature_
$\sigma_{h}(w)$ of $w$ and the relation $\Sigma_{h}(w)$ between agents $i$ and
sets of $(h{-}1)$-signatures $i$-accessible from $[w]_{h}$:

$\displaystyle\sigma_{h}(w)$ $\displaystyle=(L(w),\Sigma_{h}(w))$
$\displaystyle\Sigma_{h}(w)$ $\displaystyle=\begin{cases}\varnothing,&\text{if
}h=0\\\\[0.0pt] \\{(i,\sigma_{h}(w,i))\mid
R_{i}([w]_{h})\neq\varnothing\\},&\text{otherwise}\end{cases}$
$\displaystyle\sigma_{h}(w,i)$ $\displaystyle=\\{\sigma_{h-1}(v)\ |\
[w]_{h}R_{i}[v]_{h-1}\\}$

The _representative signature_ of $w$ is the signature $\sigma_{b(w)}(w)$,
which we compactly denote with $\sigma(w)$.

The $h$-signature of $w$ describes both what atoms hold in $w$ and which
$(h{-}1)$-bisimulation classes are accessible from $[w]_{h}$ by each agent
$i$. More precisely, $\sigma_{h-1}(v)\in\sigma_{h}(w,i)$ denotes that there
exist $w^{\prime}\in[w]_{h},v^{\prime}\in[v]_{h-1}$ such that
$w^{\prime}R_{i}v^{\prime}$. This allows to identify $h$-bisimilar worlds by
the same $h$-signature, as we will formally show (Theorem 2).

######  Lemma 2.

Let $M=(W,R,L)$ and $M^{\prime}=(W^{\prime},R^{\prime},L^{\prime})$ be two
epistemic models, let $h\geq 0$ and let $x\in W$, $x^{\prime}\in W^{\prime}$
be s.t. $\sigma_{h+1}(x)=\sigma_{h+1}(x^{\prime})$. Then
$\sigma_{h}(x)=\sigma_{h}(x^{\prime})$.

###### Proof.

We show this by induction on $h$. If $h=0$ (base case), then
$\sigma_{1}(x)=\sigma_{1}(x^{\prime})$ implies $L(x)=L(x^{\prime})$ and, thus,
$\sigma_{0}(x)=(L(x),\varnothing)=(L(x^{\prime}),\varnothing)=\sigma_{0}(x^{\prime})$.
If $h>0$, assume by induction hypothesis (I.H.) that
$\sigma_{h}(y)=\sigma_{h}(y^{\prime})$ implies
$\sigma_{h-1}(y)=\sigma_{h-1}(y^{\prime})$, for all $y\in W,y^{\prime}\in
W^{\prime}$. If $\sigma_{h+1}(x)=\sigma_{h+1}(x^{\prime})$, then
$L(x)=L(x^{\prime})$ and for all $y\in W$ s.t. $[x]_{h+1}R_{i}[y]_{h}$ there
exists $y^{\prime}\in W^{\prime}$ s.t.
$[x^{\prime}]_{h+1}R^{\prime}_{i}[y^{\prime}]_{h}$ and
$\sigma_{h}(y)=\sigma_{h}(y^{\prime})$ (and vice versa). By I.H., we have
$\sigma_{h-1}(y)=\sigma_{h-1}(y^{\prime})$. Moreover, from
$[x]_{h+1}R_{i}[y]_{h}$ and $[x^{\prime}]_{h+1}R_{i}[y^{\prime}]_{h}$, we get
$[x]_{h}R_{i}[y]_{h-1}$ and
$[x^{\prime}]_{h}R^{\prime}_{i}[y^{\prime}]_{h-1}$. We then have
$L(x)=L(x^{\prime})$ and for all $y\in W$ s.t. $[x]_{h}R_{i}[y]_{h-1}$ there
exists $y^{\prime}\in W^{\prime}$ s.t.
$[x^{\prime}]_{h}R^{\prime}_{i}[y^{\prime}]_{h-1}$ and
$\sigma_{h-1}(y)=\sigma_{h-1}(y^{\prime})$ (and vice versa). Thus,
$\sigma_{h}(x)=\sigma_{h}(x^{\prime})$, as required. ∎

######  Theorem 2.

Let $M=(W,R,L)$ and $M^{\prime}=(W^{\prime},R^{\prime},L^{\prime})$ be two
epistemic models, let $x\in W$, $x^{\prime}\in W^{\prime}$ and let $0\leq
h\leq b$. Then, $(M,x)\leftrightarroweq_{h}(M^{\prime},x^{\prime})$ iff
$\sigma_{h}(x)=\sigma_{h}(x^{\prime})$.

###### Proof.

($\rightarrow$) The proof is by induction on $h$. If $h=0$ (base case), then
$(M,x)\leftrightarroweq_{0}(M^{\prime},x^{\prime})$ iff
$L(x)=L^{\prime}(x^{\prime})$ iff $L(x)=L(x^{\prime})$ iff
$\sigma_{0}(x)=(L(x),\varnothing)=(L(x^{\prime}),\varnothing)=\sigma_{0}(x^{\prime})$.
If $h>0$, assume by induction hypothesis (I.H.) that
$(M,y)\leftrightarroweq_{h-1}(M^{\prime},y^{\prime})$ implies
$\sigma_{h-1}(y)=\sigma_{h-1}(y^{\prime})$, for all $y\in W$, $y^{\prime}\in
W^{\prime}$. Let $(M,x)\leftrightarroweq_{h}(M^{\prime},x^{\prime})$. We need
to prove that $\sigma_{h}(x)=\sigma_{h}(x^{\prime})$. Since $x$ and
$x^{\prime}$ are $h$-bisimilar, they are also $0$-bisimilar. By [atom] of
Definition 4 we then have $L(x)=L^{\prime}(x^{\prime})$, and thus
$L(x)=L(x^{\prime})$. Only left to show is that
$\Sigma_{h}(x)=\Sigma_{h}(x^{\prime})$,
$\sigma_{h}(x,i)=\sigma_{h}(x^{\prime},i)$ for all $i\in\mathcal{AG}$. We only
show $\sigma_{h}(x,i)\subseteq\sigma_{h}(x^{\prime},i)$, the other direction
being symmetrical. So let $\sigma_{h-1}(y)\in\sigma_{h}(x,i)$. We then need to
show $\sigma_{h-1}(y)\in\sigma_{h}(x^{\prime},i)$. From
$\sigma_{h-1}(y)\in\sigma_{h}(x,i)$ we get $[x]_{h}R_{i}[y]_{h-1}$,
$\bar{x}R_{i}\bar{y}$ for some $\bar{x}\in[x]_{h}$ and $\bar{y}\in[y]_{h-1}$.
From $(M,x)\leftrightarroweq_{h}(M^{\prime},x^{\prime})$ and
$x\leftrightarroweq_{h}\bar{x}$, we get
$(M,\bar{x})\leftrightarroweq_{h}(M^{\prime},x^{\prime})$. Since also
$\bar{x}R_{i}\bar{y}$, there exists $y^{\prime}\in W^{\prime}$ such that
$x^{\prime}R^{\prime}_{i}y^{\prime}$ and
$(M,\bar{y})\leftrightarroweq_{h-1}(M^{\prime},y^{\prime})$. By I.H. and from
$y\leftrightarroweq_{h-1}\bar{y}$, we get
$\sigma_{h-1}(y)=\sigma_{h-1}(\bar{y})=\sigma_{h-1}(y^{\prime})$. Since
$x^{\prime}R_{i}^{\prime}y^{\prime}$, we have
$[x^{\prime}]_{h}R^{\prime}_{i}[y^{\prime}]_{h-1}$, and hence
$\sigma_{h-1}(y^{\prime})\in\sigma_{h}(x^{\prime},i)$. As
$\sigma_{h-1}(y^{\prime})=\sigma_{h-1}(y)$, we then get
$\sigma_{h-1}(y)\in\sigma_{h}(x^{\prime},i)$, as required.

($\leftarrow$) Let $\sigma_{h}(x)=\sigma_{h}(x^{\prime})$. For all $g\leq h$,
let $Z_{g}\subseteq W\times W^{\prime}$ be defined by
$Z_{g}=\\{(w,w^{\prime})\in W\times
W^{\prime}\mid\sigma_{g}(w)=\sigma_{g}(w^{\prime})\\}$. We need to show that
$Z_{h},\dots,Z_{0}$ is an $h$-bisimulation between $(M,x)$ and
$(M,x^{\prime})$. Clearly, $(x,x^{\prime})\in Z_{h}$.
$Z_{h}\subseteq\dots\subseteq Z_{0}$ follows from Lemma 2 and [atom] follows
from the definition of $0$-signatures. We only show [forthh] ([backh] being
symmetric). Let $g<h$, $(w,w^{\prime})\in Z_{g+1}$ and $wR_{i}v$. We need to
find $v^{\prime}\in W^{\prime}$ s.t. $w^{\prime}R^{\prime}_{i}v^{\prime}$ and
$(v,v^{\prime})\in Z_{g}$. From $wR_{i}v$ we have $[w]_{g+1}R_{i}[v]_{g}$ and
hence $\sigma_{g}(v)\in\sigma_{g+1}(w,i)$. Since
$\sigma_{g+1}(w)=\sigma_{g+1}(w^{\prime})$, we also have
$\sigma_{g}(v)\in\sigma_{g+1}(w^{\prime},i)$. Thus, there is $u^{\prime}\in
W^{\prime}$ s.t. $\sigma_{g}(u^{\prime})=\sigma_{g}(v)$, implying
$[w^{\prime}]_{g+1}R^{\prime}_{i}[u^{\prime}]_{g}$ and hence there is
$w^{\prime\prime}\in[w^{\prime}]_{g+1}$ and
$u^{\prime\prime}\in[u^{\prime}]_{g}$ s.t.
$w^{\prime\prime}R^{\prime}_{i}u^{\prime\prime}$. From
$w^{\prime}\leftrightarroweq_{g+1}w^{\prime\prime}$ and
$w^{\prime\prime}R^{\prime}_{i}u^{\prime\prime}$ we get a $v^{\prime}\in
W^{\prime}$ s.t. $w^{\prime}R^{\prime}_{i}v^{\prime}$ and
$v^{\prime}\leftrightarroweq_{g}u^{\prime\prime}$. Since
$v^{\prime}\leftrightarroweq_{g}u^{\prime\prime}\leftrightarroweq_{g}u^{\prime}$,
by ($\rightarrow$) we get $\sigma_{g}(v^{\prime})=\sigma_{g}(v)$ and hence
$(v,v^{\prime})\in Z_{g}$. ∎

Note that since the sets $\mathcal{P}$ and $\mathcal{AG}$ are countable, we
can assume a fixed total order on them. This induces a fixed total order on
signatures that we will denote $\lessdot$. From this, we define the notion
_canonical $h$-signatures_.

######  Definition 16.

Let $s$ be an epistemic state and let $0\leq h\leq b$. The _canonical
$h$-signature_ of a world $w$ of $s$ is the signature
$\sigma^{\star}_{h}({w})=\min_{\lessdot}\\{\sigma(v)\mid v\in W^{\max}\text{
and }\sigma_{h}(v)=\sigma_{h}(w)\\}$.

######  Definition 17.

Let $s=((W,R,L),w_{d})$ be an epistemic state and let $b\geq 0$. The
_canonical $b$-contraction_ of $s$ is the epistemic state ${\llfloor
s\rrfloor}_{b}^{\star}=((W^{\prime},R^{\prime},L^{\prime}),\sigma(w_{d}))$,
where:

  * •

$W^{\prime}=\\{\sigma(x)\mid x\in W^{\max}\\}$;

  * •

$R^{\prime}_{i}=\\{(\sigma(x),\sigma^{\star}_{b(x){-}1}({y}))\mid x\in
W^{\max},xR_{i}y$ and $b(x)>0\\}$;

  * •

$L^{\prime}(\sigma(x))=L(x)$, for all $\sigma(x)\in W^{\prime}$.

Note that the canonical $b$-contraction only differs from the rooted
$b$-contraction by the naming of worlds ($\sigma(x)$ instead of $\llbracket
x\rrbracket$) and by the choice of representative of the class of worlds
$(b(x)-1)$-bisimilar to $y$ in the definition of $R^{\prime}_{i}$
($\sigma^{\star}_{b(x){-}1}({y})$ instead of
$\llbracket\min_{b(x){-}1}(y)\rrbracket$). This means that the proof of
Theorem 1 carries directly over to this setting:

######  Theorem 3.

Let $s$ be a state and $b\geq 0$. Then, ${\llfloor s\rrfloor}_{b}^{\star}$ is
a minimal state $b$-bisimilar to $s$.

######  Example 6.

Consider again the states $s$ and $t$ from Example 5. Before the issue was
that whether the contraction of $s$ would delete the edge $(w_{3},w_{1})$ or
the edge $(w_{3},w_{2})$ depended on the naming of the worlds. Let us confirm
that with signatures this is no longer the case. For the canonical
$3-$contraction, the edges $(w_{3},w_{1})$ and $(w_{3},w_{2})$ become the edge
$(\sigma(w_{3}),\sigma^{\star}_{0}({w_{1}}))=(\sigma(w_{3}),\min_{\lessdot}\\{\sigma(v)\mid
v\in W\text{ and
}\sigma_{0}(v)=\sigma_{0}(w_{1})\\})=(\sigma(w_{3}),\min_{\lessdot}\\{\sigma(v)\mid
v\in W\text{ and }L(v)=L(w_{1})\\})$. This shows that the end node of the edge
only depends on the world labelling and the total order on worlds, not on the
naming. So $s$ and $t$ will have the same canonical $3$-contraction, and as
shown by the next theorem, this uniqueness of representatives hold in general.

The next theorem captures the core property of canonical $b$-contractions
(full proof in Supplementary Material).

######  Theorem 4.

If $s\leftrightarroweq_{b}t$, then ${\llfloor s\rrfloor}_{b}^{\star}={\llfloor
t\rrfloor}_{b}^{\star}$.

###### Proof.

(Sketch) We use Theorem 2 to show that the worlds of ${\llfloor
s\rrfloor}_{b}^{\star}$ and ${\llfloor t\rrfloor}_{b}^{\star}$ are equal;
Theorem 2 and Definition 16 to show that such worlds are linked by the same
edges; and Lemma 2 to show that they have the same labels. ∎

##  5 Algorithms

### Bounded Partition Refinement

A well-known technique for computing the standard bisimulation contraction of
an epistemic state $s$ is the _partition refinement_ algorithm (?). As the
original algorithm is described for unlabeled accessibility relations, we
adapt its presentation to accommodate for labeled relations. Let $s=(M,w_{d})$
with $M=(W,R,L)$ and agent set $\mathcal{AG}^{\prime}$. A _partition_ $P$ of
$W$ is a set of non-empty and pairwise disjoints subsets of $W$. Elements of
$P$ are also called _blocks_. A block $B$ is _$i$ -stable_ wrt. a second block
$S$ if either $B\subseteq R_{i}(S)$ or $B\cap R_{i}(S)=\varnothing$. That is,
$B$ is _$i$ -stable_ wrt. $S$ if either $B$ contains all worlds accessible
from $S$ by agent $i$, or if no such world is in $B$. $B$ is _stable_ wrt. $S$
if it is $i$-stable for all $i\in\mathcal{AG}^{\prime}$. A partition $P$ is
_stable_ wrt. $S$ if all blocks of $P$ are stable wrt. $S$. $P$ is _stable_ if
it is stable wrt. to all of its blocks. Given $i\in\mathcal{AG}^{\prime}$, a
partition $P$ and a set $S\subseteq W$, we let $\textsc{Split}(i,S,P)$ be the
partition obtained by replacing each block $B\in P$ such that $B\cap
R_{i}(S)\neq\varnothing$ by the two blocks $B\cap R_{i}(S)$ and $B\setminus
R_{i}(S)$. $\textsc{Split}(i,S,P)$ is also called the _$i$ -refinement_ of $P$
(wrt. $S$). Furthermore, we let $\textsc{Refine}(S,P)$ be the partition
resulting from iteratively taking the $i$-refinement of $P$ wrt. $S$ for all
agents $i\in\mathcal{AG}^{\prime}$. If $P\neq$ $\textsc{Refine}(S,P)$, we call
$S$ a _splitter_ of $P$. Note that $P$ is not stable wrt. $S$ iff $S$ is a
splitter of $P$ and that, furthermore, $\textsc{Refine}(S,P)$ is stable wrt.
$S$. The partition refinement algorithm, PartitionRef, takes as input
parameter an epistemic state $s=(W,R,L)$. First, the algorithm builds an
initial partition $P$ of $W$ that groups worlds with the same label. Then,
until there exists a splitter $S$ of $P$, it replaces $P$ with
$\textsc{Refine}(S,P)$. In other words, at each step the algorithm refines $P$
wrt. one of its splitters, until a stable partition is obtained. At the end of
the partition refinement algorithm, the following holds.

######  Proposition 5 (? ?).

Let $P$ be the partition returned by $\textsc{PartitionRef}(s)$, $B\in P$ and
$x\in B$. Then $[x]_{\leftrightarroweq}=B$.

As a result, from the output of the partition refinement algorithm, we can
build the bisimulation contraction of $s$.

Algorithm 1 Bounded Partition Refinement

1:function BoundedPartitionRef($s=(W,R,L)$, $b$)

2: Let $h=0$ and $P_{0}$ be a partition of $W$ wrt. labels

3: while $h<b$ and $P_{h}$ is not stable do

4: for all $S$ in $P_{h}$ do $P_{h+1}\leftarrow\textsc{Refine}(S,P_{h})$

5: $h\leftarrow h+1$

6: return $[P_{0},\dots,P_{b}]$

To compute rooted and canonical $b$-contractions, we instead do _bounded
partition refinement_ , shown in Algorithm 1. The inputs of the algorithm are
an epistemic state $s=(W,R,L)$ and an integer $b\geq 0$ and the output is a
vector $[P_{0},\dots,P_{b}]$ of partitions of $W$. As in the standard
partition refinement, the algorithm starts from the partition $P_{0}$ of $W$
calculated wrt. labels (line 2). At each step $0\leq h<b$, if $P_{h}$ is not
stable, for all blocks $S\in P_{h}$, the algorithm refines $P_{h}$ wrt. $S$
(line 4) using the Refine operator described above. At each step $h$ of the
algorithm, the following invariant hold.

######  Proposition 6.

Let $P_{h}$ ($0\leq h\leq b$) be a partition computed by
$\textsc{BoundedPartitionRef}(s,b)$, $B\in P_{h}$ and $x\in B$. Then
$[x]_{h}=B$.

This result is Proposition 7 in ? (?), except here adopted to the exact
formulation of Algorithm 1. As a result, the output of
$\textsc{BoundedPartitionRef}(s,b)$ is a vector $[P_{0},\dots,P_{b}]$ of
partitions of $W$ such that each $P_{h}$ contains all the $h$-bisimulation
classes of $s$. From this, we can compute the rooted and canonical
$b$-contraction of $s$ by following Definitions 14 and 17, respectively.

### Iterative Bound-Deepening Search

We now describe two variants of our iterative bound-deepening planning
algorithm. We begin with the tree search variant, IterBoundTreeSearch, shown
in Algorithm 2. A _node_ $n$ of the search tree is a triple
$(s,b,\mathit{is\\_bisim})$, where $s$ is the state of $n$, $b$ is the _depth
bound_ (or simply _bound_) of $n$, intended to denote the maximum modal depth
of formulas we can safely evaluate in $s$, and $\mathit{is\\_bisim}$ is a
boolean representing whether ${\llfloor
s\rrfloor}_{b}^{\star}\leftrightarroweq s$ holds. We denote the elements $s$,
$b$ and $\mathit{is\\_bisim}$ of a node $n$ as $n.$state, $n.$bound and
$n.$is_bisim, respectively. In general, a node $n$ contains an
($n$.bound)-contracted state $n$.state. We can think of $n$.state as an
approximation of a “real” state, where we are guaranteed that $n$.state is at
least ($n$.bound)-bisimilar to the real state.

Algorithm 2 Iterative Bound-Deepening Tree Search

1:function IterBoundTreeSearch($(s_{0},\mathcal{A},\varphi_{g})$)

2: for $b\leftarrow\mathit{md}(\varphi_{g})$ to $\infty$ do

3: $\pi\leftarrow$ BoundedTreeSearch($(s_{0},\mathcal{A},\varphi_{g}),b)$

4: if $\pi\neq$ _fail_ then return $\pi$

5:

6:function BoundedTreeSearch($(s_{0},\mathcal{A},\varphi_{g})$, $b$)

7: $\mathit{frontier}\leftarrow$ $\langle$InitNode($s_{0}$, $b$,
$true$)$\rangle$

8: while $\mathit{frontier}\neq\langle\rangle$ do

9: $n\leftarrow\mathit{frontier}$.pop( )

10: if $n$.state $\models\varphi_{g}$ then return plan to $n$.state

11: for all $\alpha\in\mathcal{A}$ applicable in $n$.state do

12: if $\mathit{md}(\alpha)\leq n$.bound then

13: $n^{\prime}\leftarrow$ ChildNode($n$, $\alpha$,
$\mathit{md}(\varphi_{g})$)

14: if $n^{\prime}\neq$ _fail_ then $\mathit{frontier}$.push($n^{\prime}$)

15: return _fail_

16:

17:function InitNode($s$, $b$, $was\\_bisim$)

18: $n$.state $\leftarrow{\llfloor s\rrfloor}_{b}^{\star}$

19: $n$.bound $\leftarrow b$

20: $n$.is_bisim $\leftarrow(n$.state $\leftrightarroweq s)\land was\\_bisim$

21: return $n$

22:

23:function ChildNode($n$, $\alpha$, $d_{g}$)

24: $(s,b,\mathit{is\\_bisim})\leftarrow(n.$state$,n.$bound$,n.$is_bisim$)$

25: if $\mathit{is\\_bisim}$ then

26: return InitNode($s\otimes\alpha$, $b$, $\mathit{true}$)

27: if $b-md(\alpha)\geq d_{g}$ then

28: return InitNode($s\otimes\alpha$, $b{-}md(\alpha)$, $\mathit{false}$)

29: return _fail_

In the IterBoundTreeSearch algorithm, the integer $b\geq 0$ denotes the global
maximum modal depth of the formulas that we evaluate in each state of the
search tree. In other words, we can see $b$ as a bound on the reasoning-depth
of the planning agent. In the first iteration of the algorithm, we let
$b=\mathit{md}(\varphi_{g})$ (line 2), ensuring that agents can effectively
verify whether the goal formula is satisfied in any state. We then iteratively
call the BoundedTreeSearch algorithm over increasing values of $b$, until a
plan $\pi$ is found (lines 2-4). This algorithm implements a Breadth-First
Search (BFS) that starts from the initial node $n_{0}=(s_{0},b,\mathit{true})$
(line 7). We keep track of the nodes to be expanded in the $\mathit{frontier}$
queue, initially only containing $n_{0}$. While $\mathit{frontier}$ contains a
node $n$, we extract it from the queue and check whether its state satisfies
the goal formula. If it does, then we return the plan that lead to $n.$state
(line 10). Otherwise, we process $n$ by (attempting to) generate child nodes
for all actions $\alpha$ applicable in $n.$state satisfying
$\mathit{md}(\alpha)\leq n$.bound (lines 11-13). The latter condition is
necessary to ensure that we do not evaluate in $n$.state formulas with modal
depth exceeding the bound of node $n$. The update operation is carried out by
the ChildNode function described later. We push onto $\mathit{frontier}$ all
the updated nodes $n^{\prime}\neq$ _fail_ and continue the search. If the
frontier is empty and no plan has been found, we return _fail_ and we proceed
to the next iteration of IterBoundTreeSearch.

We now describe the ChildNode function (line 23). Let
$n=(s,b,\mathit{is\\_bisim})$ be a node, let $\alpha$ be an action and let
$d_{g}$ be the modal depth of the goal formula. The ChildNode function returns
either an updated node $n^{\prime}$, generated by the InitNode function, or
_fail_. We will analyze ChildNode in detail in our later soundness proof, so
here we only provide the intuition. The intuition is that if $n$.is_bisim is
true, then $s=n$.state is a state that is bisimilar to the “real” state
$s^{\prime}$ that it is approximating. In this case, Proposition 3 gives us
that also $s\otimes\alpha$ and $s^{\prime}\otimes\alpha$ are bisimilar, so the
state $n^{\prime}$.state of the generated child $n^{\prime}$ is also
approximating the real child state, $s^{\prime}\otimes\alpha$, up to
bisimilarity (see lines (25-26)). If $n$.is_bisim is false, we only know that
$s$ is $b$-bisimilar to the real state $s^{\prime}$, where $b=n$.bound. Hence,
from Proposition 4 we are only guaranteed that the state $n^{\prime}$.state of
the generated child is $(b-\mathit{md}(\alpha))$-bisimilar to the real child
state $s^{\prime}\otimes\alpha$ (see lines (27-28)). If neither of these
conditions hold, it means that $s\otimes\alpha$ is not a sufficiently good
approximation of the real child state $s^{\prime}\otimes\alpha$ to guarantee
that we can correctly evaluate $\varphi_{g}$ in it, and we return _fail_. This
essentially amounts to a “pruning” or “blocking” technique, where we stop
expanding the tree from nodes when the approximation becomes too bad to safely
evaluate the goal formula.

All nodes $n$ calculated at iteration $b$ such that $n$.is_bisim is true will
be computed again in iteration $b+1$. For this reason, in the implementation,
we make sure to avoid this redundancy and only recompute nodes in iteration
$b+1$ if their is_bisim value was false during iteration $b$.

Finally, we describe the graph search variant of our iterative bound-deepening
search algorithm. As this variant is very similar to the tree search one, we
do not report its pseudocode. The main difference is that in line 14 we also
check that $n^{\prime}$.state has not already been visited. We do so by
keeping a set of $\mathit{visited}$ states containing the canonical
contractions of the states computed so far. By Theorem 4, to check whether
$n^{\prime}$.state has already been visited, it suffices to check whether
${\llfloor
n^{\prime}.\text{state}\rrfloor}_{n^{\prime}.\text{bound}}^{\star}\in\mathit{visited}$.
The graph search variant of BoundedTreeSearch is called BoundedGraphSearch.

##  6 Soundness, Completeness and Complexity

######  Theorem 5 (Soundness).

Let $T=(s_{0},\mathcal{A},\varphi_{g})$ be a planning task and
$b\geq\mathit{md}(\varphi_{g})$. If the algorithm
$\textsc{BoundedTreeSearch}(T,b)$ returns a plan $\pi$, then $\pi$ is a
solution to $T$.

###### Proof.

Let $T=(s_{0},\mathcal{A},\varphi_{g})$ and $b_{0}\geq 0$ be the inputs of the
algorithm. We first prove that for any path

$n_{0}\xrightarrow{\alpha_{0}}n_{1}\xrightarrow{\alpha_{1}}\ldots\xrightarrow{\alpha_{k-1}}n_{k}$
(1)

of the search tree, we have

  1. 1.

If $n_{k}.\text{is\\_bisim}=\mathit{true}$, then

$n_{k}.\text{state}\leftrightarroweq
s_{0}\otimes\alpha_{0}\otimes\cdots\otimes\alpha_{k-1}$ (2)

else

$n_{k}.\text{state}\leftrightarroweq_{n_{k}.\text{bound}}s_{0}\otimes\alpha_{0}\otimes\cdots\otimes\alpha_{k-1}$
(3)

  2. 2.

$n_{k}.\text{bound}\geq b_{0}-\Sigma_{i<k}\mathit{md}(\alpha_{i})$ and
$n_{k}.\text{bound}\geq\mathit{md}(\varphi_{g})$.

This is by induction on $k$. In the base case $k=0$ we have
$n_{0}=\textsc{InitNode}(s_{0},b_{0},true)=({\llfloor
s_{0}\rrfloor}_{b_{0}}^{\star},b_{0},\sigma)$ where $\sigma=\mathit{true}$ iff
${\llfloor s_{0}\rrfloor}_{b_{0}}^{\star}\leftrightarroweq s_{0}$. Thus,
$n_{0}.\text{bound}=b_{0}$ and $n_{0}.\text{state}={\llfloor
s_{0}\rrfloor}_{b_{0}}^{\star}\leftrightarroweq_{b_{0}}s_{0}$. This
immediately proves (3), and if $n.\text{is\\_bisim}=\sigma=\mathit{true}$, we
furthermore get $n_{0}.\text{state}={\llfloor
s_{0}\rrfloor}_{b_{0}}^{\star}\leftrightarroweq s_{0}$, proving (2). Since
$b_{0}\geq\mathit{md}(\varphi_{g})$ by assumption, we get
$n_{0}.\text{bound}=b_{0}\geq\mathit{md}(\varphi_{g})$, proving 2. For the
induction step, suppose the claim holds for $k-1$. Extending the path to
$n_{k}$ we get $n_{k}=\textsc{ChildNode}(n_{k-1},\alpha_{k-1},d_{g})$. Let
$(s,b,\mathit{is\\_bisim})=n_{k-1}$. There are two cases to consider,
depending on whether it was the condition in line 25 or line 27 that was
satisfied in the (successful) call of
$\textsc{ChildNode}(n_{k-1},\alpha_{k-1},d_{g})$.

_Case 1_ : Line 25 was satisfied. Then $\mathit{is\\_bisim}$ is true and
$n_{k}=\textsc{InitNode}(s\otimes\alpha_{k-1},b,\mathit{true})=({\llfloor
s\otimes\alpha_{k-1}\rrfloor}_{b}^{\star},b,\sigma)$ where $\sigma$ is
$\mathit{true}$ iff ${\llfloor
s\otimes\alpha_{k-1}\rrfloor}_{b}^{\star}\leftrightarroweq
s\otimes\alpha_{k-1}$. Since $n_{k-1}.\text{is\\_bisim}=\mathit{true}$, I.H.
gives us $s\leftrightarroweq
s_{0}\otimes\alpha_{0}\otimes\cdots\otimes\alpha_{k-2}$. Proposition 3 then
gives $s\otimes\alpha_{k-1}\leftrightarroweq
s_{0}\otimes\alpha_{0}\otimes\cdots\otimes\alpha_{k-1}$. If
$n_{k}.\text{is\\_bisim}=\sigma=\mathit{true}$, then ${\llfloor
s\otimes\alpha_{k-1}\rrfloor}_{b}^{\star}\leftrightarroweq
s\otimes\alpha_{k-1}$ and hence we get $n_{k}.\text{state}={\llfloor
s\otimes\alpha_{k-1}\rrfloor}_{b}^{\star}\leftrightarroweq
s\otimes\alpha_{k-1}\leftrightarroweq
s_{0}\otimes\alpha_{0}\otimes\cdots\otimes\alpha_{k-1}$, proving (2). If
$n_{k}.\text{is\\_bisim}=\mathit{false}$, we get $n_{k}.\text{state}={\llfloor
s\otimes\alpha_{k-1}\rrfloor}_{b}^{\star}\leftrightarroweq_{b}s\otimes\alpha_{k-1}\leftrightarroweq
s_{0}\otimes\alpha_{0}\otimes\cdots\otimes\alpha_{k-1}$, proving (3), since
$n_{k}.\text{bound}=b$. Thus, we have proved 1. Since
$n_{k}.\text{bound}=b=n_{k-1}.\text{bound}$, I.H. immediately gives us 2.

_Case 2_ : Line 27 was satisfied. Then $\mathit{is\\_bisim}=\mathit{false}$ is
false, $b{-}\mathit{md}(\alpha_{k-1})\geq\mathit{md}(\varphi_{g})$, and
$n_{k}=\textsc{InitNode}(s\otimes\alpha_{k-1},b{-}\mathit{md}(\alpha_{k-1}),\mathit{false})=({\llfloor
s\otimes\alpha_{k-1}\rrfloor}_{b-\mathit{md}(\alpha_{k-1})}^{\star},b{-}\mathit{md}(\alpha_{k-1}),\mathit{false}).$
Now by I.H. we get
$s\leftrightarroweq_{b}s_{0}\otimes\alpha_{0}\otimes\cdots\otimes\alpha_{k-2}$.
Proposition 4 then gives
$s\otimes\alpha_{k-1}\leftrightarroweq_{b-\mathit{md}(\alpha_{k-1})}s_{0}\otimes\alpha_{0}\otimes\cdots\otimes\alpha_{k-1}$,
and hence $n_{k}.\text{state}={\llfloor
s\otimes\alpha_{k-1}\rrfloor}_{b-\mathit{md}(\alpha_{k-1})}^{\star}\leftrightarroweq_{b-\mathit{md}(\alpha_{k-1})}s\otimes\alpha_{k-1}\leftrightarroweq_{b-\mathit{md}(\alpha_{k-1})}s_{0}\otimes\alpha_{0}\otimes\cdots\otimes\alpha_{k-1}$,
proving (3), since $n_{k}.\text{bound}=b-\mathit{md}(\alpha_{k-1})$. As
$n_{k}.\text{is\\_bisim}=\mathit{false}$, we don’t need to prove (2). Since
the condition of line 27 was satisfied, we get
$n_{k}.\text{bound}=b-\mathit{md}(\alpha_{k-1})\geq\mathit{md}(\varphi_{g})$,
proving the second inequality of 2. I.H. then gives us
$n_{k-1}.\text{bound}\geq b_{0}-\Sigma_{i<k-1}\mathit{md}(\alpha_{i})$, and
hence
$n_{k}.\text{bound}=b-\mathit{md}(\alpha_{k-1})=n_{k-1}.\text{bound}-\mathit{md}(\alpha_{k-1})\geq
b_{0}-\Sigma_{i<k}\mathit{md}(\alpha_{i})$, proving the first inequality of 2.

This completes the proof of 1 and 2. If the algorithm returns a plan in line
10, we must have $n_{k}.\text{state}\models\phi_{g}$ where $n_{k}$ is the last
node of a path of the form (1). By 1, we then have
$n_{k}.\text{state}\leftrightarroweq_{n_{k}.\text{bound}}s_{0}\otimes\alpha_{0}\otimes\cdots\otimes\alpha_{k-1}$.
By 2, we have $n_{k}.\text{bound}\geq\mathit{md}(\varphi_{g})$, so Proposition
2 gives us that $n_{k}.\text{state}$ and
$s_{0}\otimes\alpha_{0}\otimes\cdots\otimes\alpha_{k-1}$ agree on formulas up
to modal depth $\mathit{md}(\varphi_{g})$, and hence also
$s_{0}\otimes\alpha_{0}\otimes\cdots\otimes\alpha_{k-1}\models\varphi_{g}$.
Thus, $\alpha_{0},\dots,\alpha_{k-1}$ is a solution to the planning task. ∎

We now introduce the parameters that will be used for our completeness and
complexity results. The same parameters have previously been introduced to do
parameterized complexity analysis of epistemic plan verification (?; ?). For
any planning task $T=(s_{0},\mathcal{A},\varphi_{g})$, we use $\mathsf{a}$ to
denote the number of agents used in $T$, $\mathsf{a}=|\mathcal{AG}^{\prime}|$,
where $\mathcal{AG}^{\prime}$ is the agent set of $s_{0}$ (and of the actions
in $\mathcal{A}$). Similarly, we use $\mathsf{p}$ to denote the number of
propositional atoms used in $s_{0}$ and the actions of $\mathcal{A}$. We
furthermore use $\mathsf{c}$ to denote the maximal modal depth of the pre- and
post-conditions in $\mathcal{A}$,
$\mathsf{c}=\max\\{\mathit{md}(\alpha)\mid\alpha\in\mathcal{A}\\}$. We use
$\mathsf{o}$ to denote the modal depth of the goal formula,
$\mathsf{o}=\mathit{md}(\varphi_{g})$. Finally, we use $\mathsf{u}$ to denote
the maximal allowed solution length.

######  Theorem 6 (Completeness).

If a planning task $T$ has a solution of length at most $\mathsf{u}$, then the
algorithm $\textsc{BoundedTreeSearch}(T,\mathsf{c}\mathsf{u}+\mathsf{o})$ will
find it.

###### Proof.

Suppose $T$ has a solution $\alpha_{0},\dots,\alpha_{l-1}$ with
$l\leq\mathsf{u}$. First we want to prove that the search tree computed by the
algorithm includes a path of the form (1) for all $k\leq l$. The proof is by
induction on $k$. The base case is trivial. For the induction step, suppose
the algorithm has found the path (1) for some $k<l$. We want to show that the
algorithm will at some point extend the path (1) with the node resulting from
applying $\alpha_{k}$. From the soundness proof we have properties 1 and 2
(using I.H.). In particular, we have
$n_{k}.\text{state}\leftrightarroweq_{n_{k}.\text{bound}}s_{0}\otimes\alpha_{0}\otimes\cdots\otimes\alpha_{k-1}$
where $n_{k}.\text{bound}\geq b_{0}-\Sigma_{i<k}\mathit{md}(\alpha)$ and
$n_{k}.\text{bound}\geq\mathit{md}(\varphi_{g})$ with $b_{0}$ being the input
bound, in our case $b_{0}=\mathsf{c}\mathsf{u}+\mathsf{o}$. Since
$\mathit{md}(\alpha)\leq\mathsf{c}$ for all $\alpha\in\mathcal{A}$, and since
$k\leq l-1\leq\mathsf{u}-1$, we get $n_{k}.\text{bound}\geq
b_{0}-\Sigma_{i<k}\mathit{md}(\alpha)\geq\mathsf{c}\mathsf{u}+\mathsf{o}-k\mathsf{c}\geq\mathsf{c}\mathsf{u}+\mathsf{o}-(\mathsf{u}-1)\mathsf{c}\geq\mathsf{c}+\mathsf{o}$.

Since $\alpha_{k}$ is applicable in
$s_{0}\otimes\alpha_{0}\otimes\cdots\otimes\alpha_{k-1}$ (otherwise
$\alpha_{0},\dots,\alpha_{k}$ would not be a solution), and since
$n_{k}.\text{state}\leftrightarroweq_{n_{k}.\text{bound}}s_{0}\otimes\alpha_{0}\otimes\cdots\otimes\alpha_{k-1}$
with $n_{k}.\text{bound}\geq\mathsf{c}+\mathsf{o}\geq\mathit{md}(\alpha_{k})$,
we get that $\alpha_{k}$ is also applicable in $n_{k}.\text{state}$. Hence
when $n_{k}$ is popped from the frontier, $\alpha_{k}$ will eventually be
chosen in line 11, and since $n_{k}.\text{bound}\geq\mathit{md}(\alpha_{k})$,
the test in line 12 will be satisfied, and hence
$\textsc{ChildNode}(n_{k},\alpha_{k},\mathit{md}(\varphi_{g}))$ will be
called. If $\mathit{is\\_bisim}$ tests true in line 25, then we immediately
get that a child node $n^{\prime}$ with state
$n_{k}.\text{state}\otimes\alpha_{k}$ is added, as required. Otherwise, we get
in line 27 that
$b-\mathit{md}(\alpha_{k})=n_{k}.\text{bound}-\mathit{md}(\alpha_{k})\geq\mathsf{c}+\mathsf{o}-\mathit{md}(\alpha)\geq\mathsf{c}+\mathsf{o}-\mathsf{c}=\mathsf{o}\geq\mathit{md}(\varphi_{g})$,
so the test returns true and then the child node $n^{\prime}$ with the
relevant state will be added by line 28.

Thus the algorithm will eventually compute the path (1) for $k=l$. It only
remains to show that when the last node of the path, $n_{l-1}$, is popped, a
solution will be returned. So we need to show that
$n_{l-1}.\text{state}\models\varphi_{g}$. From property 1 of the soundness
proof, we have
$n_{l-1}.\text{state}\leftrightarroweq_{n_{l-1}.\text{bound}}s_{0}\otimes\alpha_{0}\otimes\cdots\otimes\alpha_{l-1}$,
and property 2 gives $n_{l-1}.\text{bound}\geq\mathit{md}(\varphi_{g})$.
Proposition 2 then gives us that $n_{l-1}.\text{state}$ and
$s_{0}\otimes\alpha_{0}\otimes\cdots\otimes\alpha_{l-1}$ agree on all formulas
up to modal depth $\mathit{md}(\varphi_{g})$, and since
$\alpha_{0},\dots,\alpha_{l-1}$ is a solution to $T$, we get
$s_{0}\otimes\alpha_{0}\otimes\cdots\otimes\alpha_{l-1}\models\varphi_{g}$ and
hence $n_{l-1}.\text{state}\models\varphi_{g}$, as required. ∎

Theorem 6 shows that BoundedTreeSearch will always solve a planning task $T$
if the bound is high enough. Since IterBoundTreeSearch calls BoundedTreeSearch
iteratively with increasing bounds, it will eventually find a solution if one
exists.

######  Theorem 7.

$\textsc{BoundedGraphSearch}(T,b)$ runs in time
$|T|^{O(1)}\exp_{2}^{b+1}O(\mathsf{a}+\mathsf{p})$.333Where $\exp^{n}_{a}x$ is
the iterated exponential $a^{a^{\iddots^{a^{x}}}}$ with $n$ $a$s.

###### Proof.

First let us determine the size of the search tree computed by the algorithm,
more precisely, an upper bound on the number of nodes it contains. As we are
doing graph search, it will contain at most one node per canonically
$b$-contracted state, at most one node per $b$-bisimulation class (Theorem 4).
Since each $b$-bisimulation class is uniquely determined by the signature of
the designated worlds of its elements (Theorem 4), it suffices to compute how
many such signatures exist. We can do that using Definition 15. Let
$|\sigma_{h}|$ denote the number of unique $h$-signatures (given a fixed set
of agents and atomic propositions). Recall that $\mathsf{a}$ is the number of
agents, and $\mathsf{p}$ the number of atoms. As $\sigma_{0}(w)$ is just
$(L(w),\varnothing)$, we have $|\sigma_{0}|=2^{\mathsf{p}}$. For $h>0$,
$\sigma_{h}(w)=(L(w),\Sigma_{h}(w))$, where $\Sigma_{h}(w)$ is a mapping from
agents into sets of $(h-1)$-signatures. There are $\mathsf{a}$ agents and
$|\sigma_{h-1}|$ possible $(h-1)$-signatures, so there are
$(2^{|\sigma_{h-1}|})^{\mathsf{a}}=2^{|\sigma_{h-1}|\mathsf{a}}$ such
mappings. Thus in total we get
$|\sigma_{h}|=2^{\mathsf{p}}2^{|\sigma_{h-1}|\mathsf{a}}=2^{\mathsf{p}+|\sigma_{h-1}|\mathsf{a}}$.
We now prove that $|\sigma_{h}|=\exp_{2}^{h+1}O(\mathsf{a}+\mathsf{p})$ by
induction on $h$. For $h=0$ we have
$|\sigma_{h}|=2^{\mathsf{p}}=2^{O(\mathsf{a}+\mathsf{p})}=\exp_{2}^{1}O(\mathsf{a}+\mathsf{p})$.
For $h>0$ we get, using I.H.,
$|\sigma_{h}|=2^{\mathsf{p}+|\sigma_{h-1}|\mathsf{a}}=2^{\mathsf{p}+(\exp_{2}^{h}O(\mathsf{a}+\mathsf{p}))\mathsf{a}}=2^{\exp_{2}^{h}O(\mathsf{a}+\mathsf{p})}=\exp_{2}^{h+1}O(\mathsf{a}+\mathsf{p})$.
We have now proved that the number of nodes of the search tree is bounded by
$|\sigma_{b}|=\exp_{2}^{b+1}O(\mathsf{a}+\mathsf{p})$. This also gives an
upper bound on their size, and hence we also get upper bounds on computing
each contracted update and model checking the goal formula given by
$|T|^{O(1)}\exp_{2}^{b+1}O(\mathsf{a}+\mathsf{p})$ (see the proof of Theorem 4
by ? (?) for details). ∎

######  Corollary 1.

BoundedGraphSearch runs in $(b+1)-\textsc{ExpTime}$.

Theorem 7 generalises a number of existing results. First of all, if
$\mathsf{c}=0$, then by Theorem 6, BoundedTreeSearch, and hence also
BoundedGraphSearch, will solve the problem with bound
$b=\mathsf{c}\mathsf{u}+\mathsf{o}=\mathsf{o}$, and hence in time
$|T|^{O(1)}\exp_{2}^{\mathsf{o}+1}O(\mathsf{a}+\mathsf{p})$. This shows that
we can solve propositional planning tasks (planning tasks where all pre- and
postconditions are propositional) in
$(\mathit{md}(\varphi_{g})+1)-\textsc{ExpTime}$, hence providing a new proof
of an existing result (?; ?). Also note that if
$b\geq\mathsf{c}\mathsf{u}+\mathsf{o}$, then Theorem 6 gives that
BoundedGraphSearch is complete, and Theorem 7 that it runs in time
$|T|^{O(1)}\exp_{2}^{\mathsf{c}\mathsf{u}+\mathsf{o}}O(\mathsf{a}+\mathsf{p})$.
This proves that epistemic planning is fixed-parameter tractable (FPT) with
parameters $\mathsf{a}\mathsf{c}\mathsf{o}\mathsf{p}\mathsf{u}$, generalizing
the corresponding FPT result for plan verification by ? (?). As the
aforementioned paper shows that plan verification is _not_ FPT for any subset
of these parameters, this is the best result we can get. It means that
epistemic planning is tractable as long as we can put a bound on the number of
agents ($\mathsf{a}$), number of atoms ($\mathsf{p}$), modal depth of the
formula ($\mathsf{o}$), maximal modal depth of pre- and postconditions
($\mathsf{c}$) and maximal length of a plan ($\mathsf{u}$), but that if we
only put a bound on some of them, the problem becomes intractable. Also note
that epistemic planning is tractable for a fixed bound on the depth of
reasoning, and fixed agent and atom sets, which might be a quite realistic
assumption for many practical applications. Of course putting a bound on the
reasoning depth means that certain problems become unsolvable, but in other
cases we just get longer solutions (the agent finds a solution that doesn’t
require complex higher-order reasoning). Next, we do a brief experimental
evaluation, and leave a deeper evaluation of the trade-off between reasoning
depth and solution quality for future work.

##  7 Experimental Evaluation

In this section, we report the results of our experiments. We tested our
IterBoundTreeSearch algorithm on a sample of well-known benchmarks from the
literature, such as _Coin in the Box_ (?; ?), _Selective Communication_ and
_Collaboration through Communication_ (?). We refer to the original papers for
a presentation of the benchmarks. We compared our algorithm to a baseline BFS
search using standard bisimulation contractions. The results are shown in
Figure 6 (timetables in Supplementary Material). As seen, our algorithm
consistently outperforms the baseline. The tests show that in most cases, the
two algorithms compute a similar number of nodes (see Supplementary Material).
This suggests that $b$-contractions play a key role in improving the overall
performance. They result in smaller states than standard bisimulation
contractions. As these preliminary experiments show promising results, we plan
to implement also the graph search variant and compare it to tree search.

Figure 6: Time results for IterBoundTreeSearch (blue line) and BFS (red line).

To highlight the strength of our algorithm, we also devised a simple, yet
illustrative domain, called _Switches_. In a control room, agent $a_{0}$ needs
to turn on $n$ switches (all initially off). To turn on switch $1\leq k\leq
n$, agent $a_{0}$ must be supervised by a specific agent $a_{k}$. The result
of turning on a switch is only witnessed by agents $a_{0}$ and $a_{k}$ (the
other agents believe that no switch was toggled). Agents may also communicate
their knowledge on which switches are on. The goal is to turn all switches on.
Since the goal has modal depth $0$ and turning on a switch can be done with a
propositional action, IterBoundTreeSearch does not consider the communication
actions (that have modal preconditions). Hence, our algorithm takes the
$0$-contraction of each visited state, which consists of a singleton state. On
the other hand, the baseline algorithm keeps the states in their full size.
Since each switch action is witnessed only by a particular agent (plus
$a_{0}$), the depth of the state grows after each action. With 8 switches, our
algorithm solves the problem in 16 seconds, while the baseline takes 5
minutes. With 9 switches, our algorithm uses 3 minutes, and the baseline times
out after 30 minutes. If the problem could only be solved at a higher bound
than $0$, of course our algorithm would eventually reach that bound and still
find a solution.

## References

  * Aceto, Ingólfsdóttir, and Srba 2012 Aceto, L.; Ingólfsdóttir, A.; and Srba, J.  2012\.  The algorithmics of bisimilarity.  In Sangiorgi, D., and Rutten, J. J. M. M., eds., Advanced Topics in Bisimulation and Coinduction, volume 52 of Cambridge tracts in theoretical computer science. Cambridge University Press.  100–172.
  * Aucher and Bolander 2013 Aucher, G., and Bolander, T.  2013\.  Undecidability in epistemic planning.  In Rossi, F., ed., IJCAI 2013, Proceedings of the 23rd International Joint Conference on Artificial Intelligence, Beijing, China, August 3-9, 2013, 27–33.  IJCAI/AAAI.
  * Aucher 2012 Aucher, G.  2012\.  DEL-sequents for regression and epistemic planning.  Journal of Applied Non-Classical Logics 22(4):337–367.
  * Baltag, Moss, and Solecki 1998 Baltag, A.; Moss, L. S.; and Solecki, S.  1998\.  The logic of public announcements and common knowledge and private suspicions.  In Gilboa, I., ed., Proceedings of the 7th Conference on Theoretical Aspects of Rationality and Knowledge (TARK-98), Evanston, IL, USA, July 22-24, 1998, 43–56.  Morgan Kaufmann.
  * Baral et al. 2015 Baral, C.; Gelfond, G.; Pontelli, E.; and Son, T. C.  2015\.  An action language for multi-agent domains: Foundations.  CoRR abs/1511.01960.
  * Belle et al. 2022 Belle, V.; Bolander, T.; Herzig, A.; and Nebel, B.  2022\.  Epistemic planning: Perspectives on the special issue.  Artificial Intelligence 103842\.
  * Blackburn, Rijke, and Venema 2001 Blackburn, P.; Rijke, M. d.; and Venema, Y.  2001\.  Modal Logic.  Cambridge Tracts in Theoretical Computer Science. Cambridge University Press.
  * Bolander and Andersen 2011 Bolander, T., and Andersen, M. B.  2011\.  Epistemic planning for single and multi-agent systems.  J. Appl. Non Class. Logics 21(1):9–34.
  * Bolander and Burigana 2024 Bolander, T., and Burigana, A.  2024\.  Better bounded bisimulation contractions.  Under review.
  * Bolander and Lequen 2022 Bolander, T., and Lequen, A.  2022\.  Parameterized Complexity of Dynamic Belief Updates: A Complete Map.  Journal of Logic and Computation.
  * Bolander and Lequen 2023 Bolander, T., and Lequen, A.  2023\.  Parameterized complexity of dynamic belief updates: A complete map.  J. Log. Comput. 33(6):1270–1300.
  * Bolander et al. 2020 Bolander, T.; Charrier, T.; Pinchinat, S.; and Schwarzentruber, F.  2020\.  DEL-based epistemic planning: Decidability and complexity.  Artificial Intelligence 287:1–34.
  * Bolander, Dissing, and Herrmann 2021a Bolander, T.; Dissing, L.; and Herrmann, N.  2021a.  DEL-based Epistemic Planning for Human-Robot Collaboration: Theory and Implementation.  In Proceedings of the 18th International Conference on Principles of Knowledge Representation and Reasoning, 120–129.
  * Bolander, Dissing, and Herrmann 2021b Bolander, T.; Dissing, L.; and Herrmann, N.  2021b.  DEL-based epistemic planning for human-robot collaboration: Theory and implementation.  In Bienvenu, M.; Lakemeyer, G.; and Erdem, E., eds., Proceedings of the 18th International Conference on Principles of Knowledge Representation and Reasoning, KR 2021, Online event, November 3-12, 2021, 120–129.
  * Fabiano et al. 2020 Fabiano, F.; Burigana, A.; Dovier, A.; and Pontelli, E.  2020\.  EFP 2.0: A multi-agent epistemic solver with multiple e-state representations.  In Beck, J. C.; Buffet, O.; Hoffmann, J.; Karpas, E.; and Sohrabi, S., eds., Proceedings of the Thirtieth International Conference on Automated Planning and Scheduling, Nancy, France, October 26-30, 2020, 101–109.  AAAI Press.
  * Goranko and Otto 2007 Goranko, V., and Otto, M.  2007\.  Model theory of modal logic.  In Blackburn, P.; Van Benthem, J.; and Wolter, F., eds., Handbook of Modal Logic, volume 3 of Studies in Logic and Practical Reasoning. Elsevier.  chapter 5, 249–329.
  * Kominis and Geffner 2015 Kominis, F., and Geffner, H.  2015\.  Beliefs In Multiagent Planning: From One Agent to Many.  In Brafman, R. I.; Domshlak, C.; Haslum, P.; and Zilberstein, S., eds., Proceedings of the Twenty-Fifth International Conference on Automated Planning and Scheduling, ICAPS 2015, Jerusalem, Israel, June 7-11, 2015, 147–155.  AAAI Press.
  * Löwe, Pacuit, and Witzel 2011 Löwe, B.; Pacuit, E.; and Witzel, A.  2011\.  DEL planning and some tractable cases.  In van Ditmarsch, H.; Lang, J.; and Ju, S., eds., Logic, Rationality, and Interaction - Third International Workshop, LORI 2011, Guangzhou, China, October 10-13, 2011. Proceedings, volume 6953 of Lecture Notes in Computer Science, 179–192.  Springer.
  * Maubert 2014 Maubert, B.  2014\.  Logical foundations of games with imperfect information : uniform strategies. (Fondations logiques des jeux à information imparfaite : stratégies uniformes).  Ph.D. Dissertation, University of Rennes 1, France.
  * Paige and Tarjan 1987 Paige, R., and Tarjan, R. E.  1987\.  Three partition refinement algorithms.  SIAM J. Comput. 16(6):973–989.
  * Pardo and Sadrzadeh 2012 Pardo, P., and Sadrzadeh, M.  2012\.  Planning in the logics of communication and change.  In Proceedings of the 11th International Conference on Autonomous Agents and Multiagent Systems - Volume 3, AAMAS ’12, 1231–1232.  International Foundation for Autonomous Agents and Multiagent Systems.
  * van de Pol, van Rooij, and Szymanik 2018 van de Pol, I.; van Rooij, I.; and Szymanik, J.  2018\.  Parameterized complexity of Theory of Mind reasoning in dynamic epistemic logic.  Journal of Logic, Language, and Information 27:255––294.
  * van Ditmarsch and Kooi 2015 van Ditmarsch, H., and Kooi, B.  2015\.  One Hundred Prisoners and a Light Bulb.  Cham: Springer International Publishing.  83–94.
  * van Ditmarsch, van der Hoek, and Kooi 2007 van Ditmarsch, H. P.; van der Hoek, W.; and Kooi, B. P.  2007\.  Dynamic Epistemic Logic, volume 337.  Springer Netherlands.
  * Yu, Wen, and Liu 2013 Yu, Q.; Wen, X.; and Liu, Y.  2013\.  Multi-agent epistemic explanatory diagnosis via reasoning about actions.  In Rossi, F., ed., IJCAI 2013, Proceedings of the 23rd International Joint Conference on Artificial Intelligence, Beijing, China, August 3-9, 2013, 1183–1190.  IJCAI/AAAI.


# Braids, links, cobordisms and formal groups

N.M. Glazunov

###### Abstract

V.V. Sharko in his papers and books has investigated functions on manifolds
and cobordism. Braids intimately connect with functions on manifolds. These
connections are represented by mapping class groups of corresponding discs, by
fundamental groups of corresponding punctured discs, and by some other
topological or algebraic structures. This paper presents selected algebraic
methods and results of braids, links, cobordism connect with investigations by
V.V. Sharko. These includes group theoretic results on braids and links,
infinitesimal braid group relations and connections as well as connections on
coherent sheaves on smooth schemes, a sketch of our algorithm for constructing
of Lazard‘s one dimensional universal commutative formal group and selected
results on applications of commutative formal groups to cobordism theory.

Email<EMAIL_ADDRESS>
## Introduction and Acknowledgments

V.V. Sharko in his book [29] and in papers has investigated functions on
manifolds and cobordisms [28, 27]. Braids intimately connect with functions on
manifolds. These connections are represented by mapping class groups of
corresponding discs, by fundamental groups of corresponding punctured discs,
and by some other topological or algebraic structures. Cobordisms and
h-cobordisms were studied by V.V. Sharko in connection with the development of
Morse theory. This paper is organized as follows. Section 1 and 2 contain
preliminaries on braids, lincs and their relations with functions on
manifolds. Section 3 in the framework present very shortly results by
Reidemeister, Alexander and Markov. Sections 4 and 5 discuss infinitesimal
braid group relations and connections as well as connections on coherent
sheaves on smooth schemes. Sections 6 and 7 describe selected results on
cobordism theory. The author’s acquaintance with braids and links, as well as
with the theory of cobordism, took place in 1970-1971. during his internship
with academician A.A. Markov. (A.A. Markov was the head of the laboratory at
the Computing Center of the USSR Academy of Sciences, and, at the same time,
the head of the department of mathematical logic at Moscow State University).
A.A. Markov gave the description of the set of isotopy classes of oriented
links in ${\mathbb{R}}^{3}$ in terms of braids. For manifolds of the dimension
grater than 3 A.A. Markov has proved the undecidability of the problem of
homeomorphy. The author first got acquainted with the elements of the theory
of cobordism at the organized by S.P. Novikov School ”Topology and Algebraic
K-Theory”, which took place in Pushchino on the Oka in 1971. Academician A.
Markov recommended the author to participate in the School. V.V. Sharko
supported the author’s research on the use of formal groups in topology and
algebra. I am deeply grateful to them, as well as to the organizations in
which I was, for the hospitality and support. More recently author got
acquainted with approaches to the algebraic theory of cobordism at the school
”Axiomatic, enriched and motivic homotopy theory”, Isaac Newton Institute for
Mathematical Sciences, Cambridge, 9 Sept. - 20 Sept. 2002. The author is
grateful to the lecturers of the school for exciting lectures and talks, as
well as Isaac Newton Math. Institute for hospitality and financial support. I
am also grateful to the NATO ASI Conference on Bifurcations of Periodic Orbits
in Montreal, Mathematical Institute of Stockholm University, Mittag-Lefler
Institute (Druchholm), Uppsala University, CIRM (Lumini), KITPC/ITP-CAS,
Beijing, Conference “Topological recursion and quantum algebraic geometry”,
Aarhus Universitet for their support. The author deeply grateful to
corresponding member of NASU S. Maksymenko for invitations to present talk on
the Conference of the memory of V. Sharko and to present the corresponding
text. This paper has finished in Bulgaria. The author is deeply grateful to
the Bulgarian Academy of Sciences, the Institute of Mathematics and
Informatics of the Bulgarian Academy of Sciences, Professor P. Boyvalenkov for
their support. The author was supported by Simons grant 992227.

##  1 Braids, links and functions on manifolds

Below in Sections 2, 3, 4 we follow to [14, 13, 3, 24, 23, 31] and references
therein.

###### Definition 1

(Configuration spaces of the ordered sets of points). Let $M$ be a closed
smooth manifold and let $M^{n}$ be the product of $n$ spaces $M$ with the
topology of the product. Put

${\mathcal{F}}_{n}(M)=\\{(u_{1},\ldots,u_{n})\in M^{n};u_{i}\neq u_{j},i\neq
j\\}.$ (1)

###### Remark 1

If $M$ is a topological space of the dimension $dim\;M$ (possibly with the
boundary $\partial M$) then the dimension of ${\mathcal{F}}_{n}(M)$ is equal
$n\cdot dim\;M$. The topological space ${\mathcal{F}}_{n}(M)$ is connected.

###### Definition 2

The fundamental group $\pi({\mathcal{F}}_{n}(M))$ of the manifold
${\mathcal{F}}_{n}(M)$ is called the group of pure braids with $n$ strands.

Let now $M$ be a connected topological manifolds of the dimension $\geq 2$,
$M^{in}=M\setminus\partial M$, $Q_{m}\subset M^{in}$, $Q_{m}$ contains $m\geq
0$ points. Put

${\mathcal{F}}_{m,n}(M)={\mathcal{F}}_{n}(M\setminus Q_{m}).$

and for symmetric group $S_{n}$ put

${\mathcal{G}}_{m,n}={\mathcal{F}}_{m,n}(M)/S_{n}.$

###### Definition 3

The fundamental group $\pi({\mathcal{G}}_{m,n})$ is called the braids group of
the manifold $M\setminus Q_{m}$ with $n$ strands.

###### Remark 2

In the case of $M={\mathbb{R}}^{2}$ we obtain groups of pure braids and braids
in the sense of E. Artin and A. Markov.

Let $M$ be a three dimensional topological manifold possible with the boundary
$\partial M$. Recall that a geometric link in $M$ is a locally flat closed one
dimensional submanifold in $M$.

The connections between algebraic functions and braids were also studied in
the works of V. Arnol’d [2] and others.

##  2 Artin braids ([3, 23, 14])

###### Definition 4

The group of braids of Artin $B_{n}$ is a group given by $n-1$ generators of
$\sigma_{1},\ldots\sigma_{n-1}$ satisfying the relations

$\sigma_{i}\sigma_{j}=\sigma_{j}\sigma_{i}$

for integer $i,j=1,\ldots,n-1,\;|i-j|>1$ and

$\sigma_{i}\sigma_{i+1}\sigma_{i}=\sigma_{i+1}\sigma_{i}\sigma_{i+1}$

for $i=1,\ldots,n-2$.

###  2.1 Generators and relations of groups

Here and below we follow to [23, 5, 21, 4, 17]. Let
$O=\\{g_{1},\ldots,g_{m}\\}$ be a set of generators of a discrete group $G$.
Words are defined by concatenating symbols $g_{i}$ or
$g_{i}^{-1},\;i=1,\ldots,m$. Let $r(g_{1},\ldots,g_{m})$ be a word and $e$ be
the unit of the group.
Let relations

$R=\\{r_{1}(g_{1},\ldots,g_{m})=e,\ldots,r_{s}(g_{1},\ldots,g_{m})=e\\}$

and generators $O$ generate the group $G$.

###### Definition 5

A pair $(O,R)$ of such $O$, $R$ is called the code of the group $G$.

Recall well known

###### Proposition 1

Let $r_{1}(g_{1},\ldots,g_{m}),\ldots,r_{s}(g_{1},\ldots,g_{m})$ be words
which represent relations and $F(O)$ be the free group which is generated by
elements of $O$. Let $N$ be the smallest normal subgroup of $F(O)$ which
contains words $r_{1}(g_{1},\ldots,g_{m}),\ldots,r_{s}(g_{1},\ldots,g_{m})$.
Than the group $G$ is isomorphic to the factor group $F(O)/N$.

###  2.2 The word problem for finitely presented groups

Put

$<O,R>=F(O)/N.$

###### Problem 1

Given the code of the group $G$ and words $u,\;v\in F(O)$. Decide whether u, v
are equal in ¡O,R¿.

###  2.3 Problems of reduction and simplification

The problem of reduction and its solutions is based on the theory of reduction
relations. In most cases a reduction relation on a set is the binary relation
on the set.

###  2.4 The word problem for braid groups

There are a number of solutions for the word problem in the braid groups by
Garside, Thurston, and others [8, 7].

###  2.5 Braids as cobordisms

Geometric interpretation of Artin braids give examples of cobordisms. Let
$I=[0,1]$ be the unit interval. By the definition of cobordism , for a given
element $b=\\{b_{i}\\}_{i=1}^{n}$ (a braid on $n$ strands) of the braid group
$B_{n},n\geq 1$ we have the one dimensional compact manifold $W$ as the
disjoint union of $n$ intervals $I$ and have two zero dimensional closed
manifolds $M$ and $N$ consisting, respectively, of $n$ points
$b_{i}(0)=(i,0,1)$, $b_{i}(1)=(r(i),0,0)$, where $r(i)$ is some permutation.
The tautological cobordism corresponding to a braid is constructed according
to the structure of the braid and the definition of a cobordism,

##  3 Reidemeister, Alexander and Markov’s results

###  3.1 Isotopy and isotopy classes

###### Definition 6

(Milnor) Let $f,\;g$ be two diffeomorphisms of manifolds:

$f,g;X\to Y.$

A diffeomorphism $f$ is smoothly isotopic to diffeomorphism $g$ if there
exists a smooth homotopy

$F:X\times[0,1]\to Y$

between $f$ and $g$ such that for every $t\in[0,1]$ there exists a map

$x\to F(t,x)$

that maps $X$ homeomorphically onto $Y$.

Let $Ist(X,Y)$ be the set of smoothly isotopic diffeomorphisms from $X$ to
$Y$.

###### Remark 3

An isotopy is an equivalence relation, and thus the set $Ist(X,Y)$ is split
into equivalence classes.

###  3.2 Braid diagrams

Let $I$ be the closed interval $[0,1]$.

###### Definition 7

A braid diagram of $n$ strands is a set $\mathcal{D}\subset{\mathbb{R}}\times
I$ split in the form of a union of $n$ topological segments, called the
threads of the diagram $\mathcal{D}$, for which the following conditions are
satisfied:
1) the projection ${\mathbb{R}}\times I\to I$ maps each strand
homeomorphically onto $I$;
2) each point of the product $\\{1,\ldots n\\}\times\\{0,1\\}$ is the end
point of some unique thread;
3) each point of the product ${\mathbb{R}}\times I$ belongs to at most two
strands. At every point of intersection, these threads intersect
transversally.

For braid diagrams Reidemeister moves are defined, which were defined by
Reidemeister [26] for knots and knot diagrams.

###### Theorem 1

(Reidemeister [26]) Two regular representations correspond to isotopic links
if and only if the diagrams are related by isotopy (fixing the crossing
points) and by a finite sequence of the three Reidemeister moves.

Alexander have presented the relation between links and closed braids.

###### Theorem 2

( Alexander [1]) Any link is isotopic to a closed braid on some number of
strands.

A.A. Markov [23] gave the description of the set of isotopy classes of
oriented links in ${\mathbb{R}}^{3}$ in terms of braids. For manifolds of the
dimension grater than 3 A.A. Markov [24] has proved the undecidability of the
problem of homeomorphy (see also [22, 25, 30, 32]).

##  4 On monodromy representation of braid groups and on some connections

Here we present connections which correspond to monodromy representation of
braid groups as at the beginning of the Section (1). For motivations and
general ideas on Yang-Baxter and Knizhnik-Zamolodchikov connections and
equations see [18], [6, 13] and references therein.

###  4.1 On monodromy representation of braid groups

Let $E\to X$ be the fibre bundle of a topological space $X$ with the
fundamental group $\pi(X,x_{0})$ at the point $x_{0}\in X$ and with the fibre
$F_{x_{0}}$ at the same point.

###### Proposition 2

If the connection $\nabla$ is flat (i.e. $K=0$) then there exists the
monodromy representation $\pi(X,x_{0})\to Aut(F_{x_{0}})$ which induced by the
acting of the fundamental group $\pi(X,x_{0})$ on the fibre $F_{x}$ at the
point $x_{0}$.

###  4.2 On infinitesimal braid group relations, and connections

For motivations and general ideas on Yang-Baxter and Knizhnik-Zamolodchikov
equations see [18] and [6]. Below we are using the model of the configuration
space (1) of the form

${\mathcal{F}}_{n}={\mathcal{F}}_{n}(M)=\\{(z_{1},\ldots
z_{n})\in{\mathbb{C}}^{n}|z_{i}\neq z_{j},i\neq j\\}$

which regarded as a smooth manifold. At first recall some known facts about
connections on smooth algebraic varieties.We consider connections with de Rham
differentials.

###### Remark 4

In Section (5) we consider, follow to methods and results by B. Dwork, P.
Griffths, A. Grothendieck, P. Deligne, Yu. Manin, N. Katz a more general
context.

###### Definition 8

For a one-dimensional sheaf of germs of differentials $\Omega^{1}_{S/k}$ and a
coherent sheaf ${\mathcal{F}}$ on $S$, a connection on the sheaf
${\mathcal{F}}$ is a homomorphism of sheaves

$\Delta:{\mathcal{F}}\to\Omega^{1}_{S/k}\otimes{\mathcal{F}}$

such that if $f\in\Gamma(U,{\mathcal{O}}_{S}),g\in\Gamma(U,{\mathcal{F}})$,
then $\Delta(fg)=f\Delta(g)+df\otimes g$.

Let $\Omega^{i}_{S/k}$ be the sheaf of germs of $i-$differentials,

$\nabla^{i}(\alpha\otimes f)=d\alpha\otimes f+(-1)^{i}\alpha\wedge\nabla(f).$

Then $\nabla,\;\nabla^{i}$ define the sequence of homomorphisms:

${\mathcal{F}}\rightarrow\Omega^{1}_{S/k}\otimes{\mathcal{F}}\rightarrow\Omega^{2}_{S/k}\otimes{\mathcal{F}}\rightarrow\cdots,.$
(2)

The map
$K=\nabla\circ\nabla^{1}:{\mathcal{F}}\rightarrow\Omega^{2}_{S/k}\otimes{\mathcal{F}}$
is called the curvature of the connection $\nabla.$

###### Definition 9

A connection $\nabla$ is called the flat if the curvature of the connection is
equal $0$.

Below we consider the $n$-dimensional case. For the complex vector space $W$
let $\\{A_{i,j}\\},1\leq i<j\leq n$ be automorphisms of $W$ which satisfy
conditions

$[A_{i,j},A_{k,l}]=0,\;[A_{i,j},A_{i,k}+A_{j,k}]=[A_{j,k},A_{i,j}+A_{i,k}].$
(3)

###### Remark 5

Below we assume that these conditions are satisfied.

Consider the connection

$\nabla=d-\Gamma,$

on the trivial bundle

${\mathcal{F}}_{n}\times W,$

where

$d\omega=\sum_{1\leq i<j\leq
n}\frac{A_{i,j}}{z_{1}-z_{j}}(dz_{i}-dz_{j})\omega,$ $\Gamma=\sum_{1\leq
i<j\leq n}\frac{A_{i,j}}{z_{1}-z_{j}}(dz_{i}-dz_{j}),$

###### Proposition 3

The connection $\nabla=d-\Gamma$ is flat.

###### Problem 2

Matrices with conditions 3 define for a given $n$ the Lie algebra
$\mathfrak{p}$. By the Lie algebra it is possible to construct the local Lie
group $\mathfrak{P}$. The expansion in group identity of the group law of the
local Lie group $\mathfrak{P}$ gives the formal group law. The algebras,
groups, and formal Lie groups mentioned above correspond to pure braid groups.
What formal group laws correspond to pure braid groups?

In the case of the braid group, we must consider the factormanifold

${\mathcal{G}}_{n}={\mathcal{F}}_{n}/S_{n}$

where $S_{n}$ is the permutation group. Let the group $S_{n}$ acts from the
left on the vector space $W$. Then there is the right action of $S_{n}$ on the
trivial bundle ${\mathcal{F}}_{n}\times W$ by the formula

$(z_{1},\ldots z_{n}),w)\sigma=(z_{\sigma(1)},\ldots
z_{\sigma(n)}),\sigma^{-1}(w)),\sigma\in S_{n}.$

If $d\omega$ is invariant under the action of $S_{n}$ then by the
(Grothendieck) descend theory the connection $\nabla=d-\Gamma$ descends on the
non-trivial vector bundle $({\mathcal{F}}_{n}\times W)/S_{n}$.

###### Problem 3

This problem is similar to the Problem (2). Now algebras, groups, and formal
Lie groups correspond to braid groups. What formal group laws correspond to
braid groups in the monodromy representations?

##  5 Connections on coherent sheaves of smooth schemes

Here we follow to methods and results of B. Dwork, A. Grothendieck, P.
Deligne, Yu. Manin, N. Katz [15], as well as the works [16, 10]. In [10] we
considered applications of the methods of algebraic geometry to string theory.
An open string can be interpreted as a unit (or trivial) braid group $B_{1}$.
A closed string is the closure of the element of the unit braid group.
Introduction to the consideration of non-trivial braid groups extends and
deepens emerging algebraic picture. Below we use notations and results from
subsection (4.2).

Let $\Theta^{1}_{S/k}$ be the tangent sheaf on the scheme $S$,
$\partial\in\Gamma(U,\Theta^{1}_{S/k})$. In this case, we can give a dual
definition of a connection on a sheaf.

###### Definition 10

In the above notation, a connection is a homomorphism

$\rho:\Theta^{1}_{S/k}\to
End_{{\mathcal{O}}_{S}}({\mathcal{F}},{\mathcal{F}})$

such that $\rho(\partial)(fg)=\partial(f)g+f\rho(\partial)$.

Recall that the cochain complex

$(K^{\bullet},d)=\\{K^{0}\xrightarrow{d}K^{1}d=0\xrightarrow{d}K^{2}\xrightarrow{d}\cdots\\}$

in the category of Abelian groups is called the sequence of Abelian groups and
morphisms $d:K^{p}\xrightarrow{d}K^{p+1}$ such that $d\circ d=0$.

###### Remark 6

Let ${\mathcal{A}}$ be an abelian category, ${\mathcal{K}}({\mathcal{A}})$ the
category of complexes over ${\mathcal{A}}$. Furthermore, there are various
full subcategories of ${\mathcal{K}}({\mathcal{A}})$ whose respective objects
are the complexes which are bounded below, bounded above, bounded in both
sides. The notions of homotopy morphism, homotopical category, triangulated
category are described in [9]. The bounded derived category
${\mathcal{D}}^{b}(X)$ of coherent sheaves on $X$ has the structure of a
triangulated category [9].

###  5.1 Integration of Connections

###### Definition 11

A connection is integrable if (2) is a complex.

###### Proposition 4

The statements a),b), c) are equivalent:
a) the connection $\nabla$ is integrable;
b) $K=\nabla\circ\nabla^{1}=0;$
c) $\rho$ is the Lie-algebra homomorphism of sheaves of Lie algebras.

More generally, let $X,S$ be smooth schemas over $k,f:X\rightarrow S$ a smooth
morphism,

$\Omega_{X/S}^{\bullet}:{\mathcal{O}}_{X}\rightarrow\Omega^{1}_{X/S}\rightarrow\Omega^{2}_{X/S}\rightarrow\cdots,$
(4)

the de Rham complex of relative differentials. There is the exact sequence

$0\rightarrow
f^{*}(\Omega_{S}^{\bullet})\rightarrow\Omega_{X}^{\bullet}\rightarrow\Omega_{X/S}^{\bullet}\rightarrow
0.$ (5)

In the case there is an integrable connection, the Gauss-Manin connection.

By an abelian sheaf we mean a sheaf of abelian groups. Let $R^{0}f_{*}$ be the
functor from the category of complexes of abelian sheaves on $X$ to the
category of abelian sheaves on $S.$ Denote by ${\mathcal{H}}^{i}_{DR}(X/S)$
the sheaf of de Rham cohomologies such that

${\mathcal{H}}^{i}_{DR}(X/S)=R^{i}f_{*}\Omega_{X/S}^{\bullet}.$

Recall that

${\mathcal{H}}^{i}={\mathcal{H}}^{i}_{DR}=R^{i}f_{*}\Omega_{X/S}^{\bullet}$

is called the Gauss-Manin bundle.

Here $R^{i}f_{*}$ are the hyperderved functor of $R^{0}f_{*}.$

For each $i\geq 0,{\mathcal{H}}^{i}_{DR}(X/S)$ is a locally free coherent
algebraic sheaf on $S,$ whose fiber at each point $s\in S$ is the ${\bf
C}-$vector space $H^{i}(X_{s},{\bf C})$ and has the Gauss-Manin connection.
${\mathcal{H}}^{i}_{DR}(X/S)$ has the main interpretation as the Picard-Fuchs
equations and $H^{i}(X_{s},{\bf C})$ in the interpretation is the local system
of germs of solutions of the equations.

There is the canonical filtration of $\Omega_{X/S}^{\bullet}$ by locally free
subsheaves

$\Omega_{X/S}^{\bullet}=F^{0}(\Omega_{X/S}^{\bullet})\supset
F^{1}(\Omega_{X/S}^{\bullet})\supset\cdots$

given by

$F^{i}(\Omega_{X}^{n}):=Im(f^{*}(\Omega_{S}^{i})\otimes\Omega_{X}^{n-i}\rightarrow\Omega_{X}^{n}).$

##  6 Formal groups in complex cobordism

###  6.1 Algorithm for constructing of Lazard‘s one dimensional universal
formal group

Here we follow to [19, 12, 11]. We extract from Lazard [19] an algorithm of
constructing of Lazard‘s one dimensional universal formal group law. But we
give here the structute of the Lazard algorithm only. The constructions of
$n(n\geq 1)$-buds, formal groupoids and moduli spaces of one dimensional
formal groups are investigated and are used. Let $A_{q}$ and $A^{`}_{q}$ be
the rings of polynomials $A_{q}={\mathbb{Z}}[\alpha_{1},\ldots,\alpha_{q}]$
and $A^{`}_{q}={\mathbb{Q}}[\alpha_{1},\ldots,\alpha_{q}]$.

###### Proposition 5

The structure of the algorithm has the next form. For the (one-dimensional)
$1$-bud $x+y+\alpha_{1}xy$ we put:

$f_{1}(x,y)=x+y+\alpha_{1}xy;\;\varphi_{1}=x-\frac{1}{2}\alpha_{1}x^{2};$
$f_{q+1}(x,y)=f_{q}(x,y)+h^{`}(x,y)+\alpha_{q+1}C_{q+2}(x,y),\;f_{q}(x,y)\in
A_{q};$

compute $\varphi_{q+1},\;\varphi_{q+1}\in A^{`}_{q}$.

###### Definition 12

The ring ${\mathbb{L}}={\mathbb{Z}}[\alpha_{1},\alpha_{2},\cdots]$ is called
the Lazard ring.

###  6.2 On formal groups in complex cobordism

Let $M$ be a smooth manifoldd, $TM$ be the tangent bundle on $M$ and
${\mathbb{R}}^{m}$ the trivial real $m$-dimensional bundle of $M$.

###### Definition 13

A manifold $M$ is _stably complex_ if for some natural $m$ the real vector
bundle $TM\bigoplus{\mathbb{R}}^{m}$ admits a complex structure.

Let $M_{1}$ and $M_{2}$ be two smooth manifolds of dimension $n$, and $W$ be
the smooth manifold of dimension $n+1$ with a boundary that is the union of
$M_{1}$ and $M_{2}$, i.e. $\partial W=M_{1}+M_{2}$.

###### Definition 14

Let $M_{1},M_{2},W$ be stably complex manifolds. In above notations the
_complex (unitary) cobordism_ between $M_{1}$ and $M_{2}$ is a manifold $W$
whose boundary is the disjoint union of $M_{1}$, $M_{2}$, $\partial
W=M_{1}+{\overline{M}_{2}}$ where the corresponding structure on $\partial W$
is induced from $W$ and ${\overline{M}_{2}}$ denotes the manifold with
opposite structure.

###### Remark 7

Suppose we have the relation of complex cobordism. Then the relation divides
stably complex manifolds on equivalence classes called classes of complex
cobordisms.

###### Lemma 1

The set of classes of complex cobordisms with operations of disjoint union and
product of stable manifolds form commutative graded ring
${\mathbb{L}}={\mathbb{Z}}[v_{1},v_{2},\cdots]$ .

###### Theorem 3

(A.S. Mishchenko) Let $g(t)$ be the logarithm of Lazard universal formal
group, and $[{\mathbb{C}}P^{n}]$ are classes of unitary cobordisms of complex
projective spaces. Then

$g(t)=\sum_{n\geq
0}\frac{[{\mathbb{C}}P^{n}]}{n+1}t^{n+1},\;[{\mathbb{C}}P^{0}]=1.$

## Formal groups in algebraic cobordism

Here we follow to [20]. Let $k$ be a field of characteristic zero and
${\mathbf{Sm}}(k)$ be the full subcategory of smooth quasi-projective
$k$-schemes of the category of separable finite-type $k$-schemes. Let $A^{*}$
be an oriented cohomology theory on ${\mathbf{Sm}}(k)$ and let $c_{1}(L)$ be
the first Chern class of line bundle $L$ on $X\in{\mathbf{Sm}}(k)$.

###### Proposition 6

( Quillen, [20]). Let $L,\;M$ be line bundles on $X\in{\mathbf{Sm}}(k)$..
There exists formal group law $F_{A}$ with coefficients in $A^{*}$ such that

$c_{1}(L\otimes M)=F_{A}(c_{1}(L),c_{1}(M)).$

###### Theorem 4

(Levine-Morel).There is a universal oriented cohomology theory $\Omega$ over
$k$ called algebraic cobordism. The classifying map
$\phi_{\Omega}:{\mathbb{L}}\to\Omega^{*}(k)$ is an isomorphism , so
$F_{\Omega}$ is the universal formal group law.

###### Problem 4

It seems that very little is known about applying $n(n\geq 2)$-dimensional
commutative formal groups to cobordism theory. For instance what is the
application of a two-dimensional 1-bud ?

## References

  * [1] J.W. Alexander.  A lemma on systems of knotted curves.  Proc. Nat. Acad. Sci., 9:93–95, 1923.
  * [2] V. I. Arnol’d.  On some topological invariants of algebraic functions.  Trans. Moscow Math. Soc., 21:30–52, 1970.
  * [3] E Artin.  Theory of braids.  Ann. Math., 48:101–126, 1947.
  * [4] B. Buchberger, G. Collins, R. Loos, and R. Albrecht.  Computer Algebra.  Wien : Springer, 1982.
  * [5] H. Coxeter and W. Moser.  Generators and relations for discret groups.  Berlin & New York : Springer, 1972.
  * [6] V.G. Drinfeld.  Quasi-hopf algebras.  Algebra i Analiz, 1(6):114–148, 1989.
  * [7] Epstein, Cannon, Holt, and Thurston.  Word Processing in Groups.  Boston, MA : Jones and Baitlett, 1974.
  * [8] F.A. Garside.  The braid group and other groups.  Quart. J. Math. Oxford, 20(78):235–254, 1969.
  * [9] S.I. Gelfand and Yu. I. Manin.  Methods of homological algebra.  Nauka, 1988.
  * [10] N.M. Glazunov.  On algebraic geometric and computer algebra aspects of mirror symmetry.  Proc. of the Int. Conf. Computer Algebra and its Applications to Physics, JINR, Dubna, (78):104–113, 2002.
  * [11] N.M. Glazunov.  Duality in abelian varieties and formal groups over local fields.  Chebyshevskii Sbornik, 19(1):44–56, 2018.
  * [12] M. Hazewinkel.  Formal groups and applications.  New York : Academic Press, 1978.
  * [13] C. Kassel and C. Reutenauer.  Sturmian morphisms, the braid group b4, christoffel words and bases of f2.  Ann. Math. Pure Appl., 166(2):317–339, 2007.
  * [14] C. Kassel and V. Turaev.  Braid groups.  Berlin & New York : Springer, 2008.
  * [15] N. Katz.  G2 and hypergeometric sheaves.  Finite Fields Appl., 13(2):175–223, 2007.
  * [16] K. Kedlaya and J. Tuitman.  Effective convergence bounds for frobenius structures on connections.  Rend. Semin. Mat. Univ. Padova., 128:7–16, 2012.
  * [17] W. Koepf.  Computer Algebra: An Algorithm-Oriented introduction.  Berlin & New York : Springer, 2021.
  * [18] T. Kohno.  Monodromy representations of braid groups and yang-baxter equations.  Ann. Inst. P’ourier, Grenoble, 37(4):139–160, 1987.
  * [19] M. Lazard.  Sur les groupes de lie formels a un parametre.  Bull. Sos. Math. France, (83):251–274, 1955.
  * [20] Mark Levine and Fabien Morel.  Algebraic cobordism.  Monographs in Mathematics. Berlin & New York : Springer, 2007.
  * [21] W. Magnus, A. Karrass, and D. Solitar.  Combinatorial group theory.  Berlin & New York : Springer, 1974.
  * [22] A. Markoff.  Uber die freie aquivalenz geschlossener zopfe.  Math. Sbornik, 1(43):73–78, 1936.
  * [23] A. Markov.  Foundations of algebraic theory of braids.  Trudy Steklov Math. Ins., XVI(16):3–53, 1945.
  * [24] A. Markov.  Unsolvability of homeomorphy problem, proc. icm1958.  Cambridge Univer. Press, 1:300–306, 1960.
  * [25] H. R. Morton.  Threading knot diagrams.  Mathematical Proceedings of the Cambridge, 99:247–260, 1986.
  * [26] K. Reidemeiste.  Knotentheorie.  Berlin: Springer-Verlag, 1932.
  * [27] V. Sharko.  K-theory and morse theory. 1.  Amer. Math. Soc. Transl. (2), 149:115–156, 1991.
  * [28] V. Sharko.  Stable algebra in morse theory.  Math. USSR Izvestiya, 36(199):629–653, 1991.
  * [29] V. Sharko.  Functions on manifolds. Algebraic and topological aspects.  Translation of Mathematical Monographs, 1993.
  * [30] P. Traczyk.  A new proof of  Banach Center Publ., 42:095–119, 1995.
  * [31] V. Turaev.  Faithful linear representations of the braid groups.  Astèrisque, 276:389–409, 2002.
  * [32] P. Vogel.  Representation of links by braids: A new algorithm.  Comment. Math.i Helv., 1(65):104–113, 1990.

Glushkov Institute of Cybernetics National Academy of Sciences of Ukraine,
Institute of Mathematics and Informatics Bulgarian Academy of Sciences