$\mathbf{EF}^{J}_{k}(A,B)$ and showing that this captures the equivalence in
$\text{FO}_{k}(S,J)$ by an adaptation of the standard single-sorted proof
found in chapter three of [30]. We then prove that the existence of a
Duplicator winning strategy in $\mathbf{EF}^{J}_{k}(A,B)$ is equivalent to the
existence of open pathwise embeddings
$F^{\mathbb{E}_{k}}\mathfrak{t}^{J}A\leftarrow(W,\upsilon)\rightarrow
F^{\mathbb{E}_{k}}\mathfrak{t}^{J}B$ by adapting the single-sorted proof found
in [4]. Later we explain how to adapt the proof to obtain also the second item
of the statement.

Generalising the single-sorted case, every move of the
$\mathbf{EF}^{J}_{k}(A,B)$ game results in a $S$-sorted relation $\gamma$ of
type $A$ to $B$. A $S$-sorted relation $\gamma$ from $S$-sorted set $A$ to
$S$-sorted set $B$ is an $S$-indexed family of sets $\gamma_{s}\subseteq
A_{s}\times B_{s}$. Since the logic $\text{FO}_{k}(S,J)$ has equality only for
terms of sort $s\in J$, the winning condition of $\mathbf{EF}^{J}_{k}(A,B)$
requires a notion of $S$-sorted relation $\gamma$ which is only required to be
single-valued, i.e. a partial function, on sorts $s\in J$. The following
notion is used to define the winning moves in $\mathbf{EF}^{J}_{k}(A,B)$:

######  Definition A.32.

Given $S$-sorted $\sigma$ structures $A$,$B$ and $J\subseteq S$, a $S$-sorted
relation $\gamma$ of type $A\times B$ is a partial isomorphism on $J$ from $A$
to $B$ if the following conditions hold:

  * •

If $c\in\mathbf{cs}(\sigma,s)$, then $(c^{A},c^{B})\in\gamma_{s}$

  * •

For all $s\in J$, $\gamma_{s}$ is a partial function from $A_{s}$ to $B_{s}$

  * •

For every $R\in\sigma$ of arity $\langle s_{1},\dots,s_{m}\rangle$,

$R^{A}(a_{1},\dots,a_{m})\Leftrightarrow R^{B}(b_{1},\dots,b_{m})$

whenever $(a_{1},b_{1})\in\gamma_{s_{1}},\dots,(a_{m},b_{m})\in\gamma_{s_{m}}$

We are now able to introduce the $k$-round many-sorted Ehrenfeucht–Fraïssé
game:

######  Definition A.33.

Given $S$-sorted $\sigma$ structures $A$ and $B$, the $k$-round $S$-sorted
Ehrenfeucht-Fraïssé game $\mathbf{EF}^{J}_{k}(A,B)$ with equality on $J$ is
played between two players, Spoiler and Duplicator. In each round $i\leq k$,

  * •

Spoiler chooses a sort $s_{i}\in S$ and element $a_{i}\in A_{s_{i}}$ or
$b_{i}\in B_{s_{i}}$.

  * •

Duplicator responds with an element $b_{i}\in B_{s_{i}}$ or $a_{i}\in
A_{s_{i}}$ in the other structure’s $s_{i}$ sort.

Duplicator wins round $i$, if the following $S$-sorted relation $\gamma$,
defined componentwise,

$\gamma_{i,s}=\\{(c^{A},c^{B})\mid
c\in\mathbf{cs}(\sigma,s)\\}\cup\\{(a_{j},b_{j})\mid\text{ for }s_{j}=s\text{
and }j\leq i\\}$

is a partial isomorphism on $J$ from $A$ to $B$.

Duplicator is said to have a winning strategy in $\mathbf{EF}^{J}_{k}(A,B)$ if
for all possible Spoiler moves in the $k$-round game, Duplicator can win round
$i$ for all $i\leq k$.

As expected, the $\mathbf{EF}^{J}_{k}(A,B)$ game captures equivalence in
$\text{FO}_{k}(S,J)$. To prove this, we consider structures $(A,a)$ in the
expanded signature $\sigma(c{:}s)$. The signature $\sigma(c{:}s)$ has an
additional fresh constant symbol $c$ added to $\mathbf{cs}(\sigma,s)$, the
same constants as $\mathbf{cs}(\sigma,s^{\prime})$ for $s^{\prime}\not=s$, and
the same relation symbols as $\sigma$. The notation $(A,a)$ is the
$\sigma(c{:}s)$-structure where $A$ is a $\sigma$-structure and $c^{A}=a\in
A_{s}$.

######  Proposition A.34.

The following are equivalent

  1. 1.

Duplicator has a winning strategy in $\mathbf{EF}^{J}_{k}(A,B)$

  2. 2.

$A\equiv_{\text{FO}_{k}(S,J)}B$

######  Proof A.35.

$(1)\Rightarrow(2)$ We prove the statement by induction on $k$. Suppose $k=0$
and that Duplicator has a winning strategy in $\mathbf{EF}^{J}_{0}(A,B)$. By
the winning condition, the relation $\gamma$, defined componentwise as
${\gamma_{s}=\\{(c^{A},c^{B})\mid c\in\mathbf{cs}(\sigma,s)\\}}$ is a partial
isomorphism. In particular, $\gamma$ is a partial isomorphism on $J$. Hence,
from the definition of partial isomorphism, $A$ and $B$ satisfy the same
atomic sentences.

For the inductive step, suppose Duplicator has a winning strategy in
$\mathbf{EF}^{J}_{k+1}(A,B)$ and consider the sentence $\phi$ of rank $k+1$.
It follows from the definition of quantifier rank, that every sentence $\phi$
of rank $k+1$ is a boolean combination of sentences of the form $\exists
y{:}s\psi(y{:}s)$ for sort $s\in S$ where $\psi$ is a formula of rank $\leq
k$. Hence, by recursion on the construction of formulas $\phi(\vv{x})$, it
suffices to only prove that $A\vDash\phi\Leftrightarrow B\vDash\phi$ for
$\phi=\exists y{:}s\psi(y{:}s)$.

Suppose $A\vDash\exists y{:}s\psi(y{:}s)$, then there exists some $a\in
A_{s}$, such that ${(A,a)\vDash\psi(y{:}s)}$. Consider the
$\mathbf{EF}^{J}_{k+1}(A,B)$ game where Spoiler plays $s\in S$ and $a\in
A_{s}$ in the first round. Let Duplicator’s response be $b\in B_{s}$ according
to the winning strategy. Duplicator then has a winning strategy in the
$\mathbf{EF}^{J}_{k}((A,a),(B,b))$ game by playing according the subsequent
$k$ moves of the $\mathbf{EF}_{k+1}(A,B)$ game. Hence, by the inductive
hypothesis, we have that for all $\sigma(c{:}s)$ sentences $\phi^{\prime}$ of
rank $\leq k$,
$(A,a)\vDash\phi^{\prime}\Leftrightarrow(B,b)\vDash\phi^{\prime}$. In
particular, $(B,b)\vDash\psi(y{:}s)$. Hence, $B\vDash\exists
y{:}s\psi(y{:}s)$. To show the other direction, i.e. $B\vDash\exists
y{:}s\psi(y{:}s)\Rightarrow A\vDash\exists y{:}s\psi(y{:}s)$, is essentially
the same.

$(2)\Rightarrow(1)$ We prove the statement by induction on $k$. For $k=0$, $A$
and $B$ satisfying the same atomic sentences proves that $\gamma$, formed from
just the pairs of constants, is a partial isomorphism on $J$.

For the inductive step, assume $A$ and $B$ satisfy the same sentences of rank
$k+1$. We need to show that Duplicator has a winning strategy in the
$\mathbf{EF}_{k+1}(A,B)$ game. Suppose, in the first round of $k+1$, Spoiler
chooses $s\in S$ and $a\in A_{s}$. There is finite collection of in-equivalent
formulas $\varphi_{1},\dots,\varphi_{M}$ of rank $k$ with variable $x{:}s$
such that $(A,a)\vDash\varphi_{i}(x{:}s)$. Hence, $A\vDash\exists
x{:}s(\bigwedge_{i\leq M}\varphi_{i}(x{:}s))$. The sentence $\exists
x{:}s(\bigwedge_{i\leq M}\varphi_{i}(x{:}s))$ has rank $k+1$, so by the
supposition, $B\vDash\exists x{:}s(\bigwedge_{i\leq M}\varphi_{i}(x{:}s))$.
Therefore, there exists a $b\in B_{s}$ witnessing the existential quantifier
$\exists x{:}s$; and so Duplicator responds with this $b\in B_{s}$. By
construction,
${(A,a)\vDash\varphi(x{:}s)\Leftrightarrow(B,b)\vDash\varphi(x{:}s)}$ for all
$\sigma(c)$-sentences of rank $\leq k$. By the inductive hypothesis,
Duplicator has a winning strategy in the $\mathbf{EF}_{k}((A,a),(B,b))$ game.
Therefore, Duplicator proceeding in the subsequent $k$ moves of
$\mathbf{EF}_{k+1}(A,B)$ according to the moves of
$\mathbf{EF}_{k}((A,a),(B,b))$ yields a winning strategy for
$\mathbf{EF}_{k+1}(A,B)$.

######  Proposition A.36.

The following are equivalent:

  1. 1.

Duplicator has a winning strategy in $\mathbf{EF}^{J}_{k}(A,B)$

  2. 2.

$\mathfrak{t}^{J}A\leftrightarrow_{\mathbb{E}_{k}}\mathfrak{t}^{J}B$

######  Proof A.37.

$(1)\Rightarrow(2)$ Suppose Duplicator has a winning strategy in
$\mathbf{EF}^{J}_{k}(A,B)$, this determines a $S$-sorted set $W$ with
components $W_{s}\subseteq(\mathbb{E}_{k}A)_{s}\times(\mathbb{E}_{k}B)_{s}$
that satisfy the following conditions:

  * •

For all $c\in\mathbf{cs}(\sigma,s)$,
$(c^{\mathbb{E}_{k}A},c^{\mathbb{E}_{k}B})\in W_{s}$

  * •

(forth) For every pair $(w,v)\in W_{s}$ such that $w$ is a word of length $<k$
or a pair of empty words $(w,v)$ and $a\in A_{s^{\prime}}$ (Spoiler’s move),
there exists a $b\in B_{s^{\prime}}$ (Duplicator’s response) such that
$(w[a{:}s^{\prime}],v[b{:}s^{\prime}])\in W_{s^{\prime}}$.

  * •

(back) For every pair $(w,v)\in W_{s}$ such that $v$ is a word of length $<k$
or a pair of empty words $(w,v)$ and $b\in B_{s^{\prime}}$, there exists a
$a\in A_{s^{\prime}}$ such that $(w[a{:}s^{\prime}],v[b{:}s^{\prime}])\in
W_{s^{\prime}}$

  * •

(winning) The relation $\gamma_{w,v}$ where $(\gamma_{w,v})_{s}$ consists of
pairs $(a,b)$ such that $a{:}s$ and $b{:}s$ appear at the same index in $w$
and $v$ (respectively) is partial isomorphism on $J$ for every pair $(w,v)$ in
$S$-sorted set $W$.

Since $W$ is a $S$-sorted subset of
$\mathbb{E}_{k}\mathfrak{t}^{J}A\times\mathbb{E}_{k}\mathfrak{t}^{J}B$, we can
consider the induced substructure $W$ of this product structure. This
structure $W$ has a natural coalgebra $\omega:W\rightarrow\mathbb{E}_{k}W$
where constants are mapped to constants and $\omega_{s}(w_{n},v_{n})$ is
mapped to the sequence $[(w_{1},v_{1}){:}s_{1},\dots,(w_{n},v_{n}){:}s_{n}]$
where $w_{1}\sqsubset_{\delta_{A}}\dots\sqsubset_{\delta_{A}}w_{n}$ and
$v_{1}\sqsubset_{\delta_{B}}\dots\sqsubset_{\delta_{B}}v_{n}$ are the unique
chains below in $w_{n}$ and $v_{n}$ in $F^{\mathbb{E}_{k}}\mathfrak{t}^{J}A$
and $F^{\mathbb{E}_{k}}\mathfrak{t}^{J}B$, respectively. The projection maps
$p_{1}:(W,\omega)\rightarrow F^{\mathbb{E}_{k}}\mathfrak{t}^{J}A$ and
$p_{2}:(W,\omega)\rightarrow F^{\mathbb{E}_{k}}\mathfrak{t}^{J}B$ are
coalgebra morphisms, but we must show that these projection maps are also open
pathwise embeddings.

To verify $p_{1}:(W,\omega)\rightarrow F^{\mathbb{E}_{k}}\mathfrak{t}^{J}A$ is
a pathwise embedding, we note that the image of path embedding
$e:(P,\pi)\rightarrow(W,\omega)$ contains elements
$(w_{1},v_{1}){:}s_{1},\dots,(w_{n},v_{n}){:}s_{n}$ where
$w_{1}\sqsubset_{\delta_{A}}\dots\sqsubset_{\delta_{A}}w_{n}$ and
$v_{1}\sqsubset_{\delta_{B}}\dots\sqsubset_{\delta_{B}}v_{n}$ are chains in
$\mathbb{E}_{k}\mathfrak{t}^{J}A$ and $\mathbb{E}_{k}\mathfrak{t}^{J}B$,
respectively. As $w_{1}\sqsubset\dots\sqsubset w_{n}$ is a path in
$\mathbb{E}_{k}\mathfrak{t}^{J}A$, we have that $p_{1}\circ
e:(P,\pi)\rightarrow\mathbb{E}_{k}\mathfrak{t}^{J}A$ is a path embedding.

To verify $p_{1}:(W,\omega)\rightarrow F^{\mathbb{E}_{k}}\mathfrak{t}^{J}A$ is
open, consider the following commuting diagram in
$\mathsf{EM}(\mathbb{E}_{k})$:

${(P,\pi)}$${(Q,\chi)}$${(W,\omega)}$${F^{\mathbb{E}_{k}}\mathfrak{t}^{J}A}$$\scriptstyle{e_{0}}$$\scriptstyle{e_{1}}$$\scriptstyle{\pi_{1}}$

where $e_{0}:(P,\pi)\rightarrowtail(W,\omega)$ and
$e_{1}:(Q,\chi)\rightarrowtail F^{\mathbb{E}_{k}}\mathfrak{t}^{J}A$ are path
embeddings. Suppose
$w_{1}\sqsubset_{\delta_{A}}\dots\sqsubset_{\delta_{A}}w_{n}$ is the image of
path $Q$ presented as $r_{1}\sqsubset_{\chi}\dots\sqsubset_{\chi}r_{n}$ under
embedding $e_{1}$, then by the above diagram commuting
$(w_{1},v_{1})\sqsubset_{\omega}\dots\sqsubset_{\omega}(w_{i},v_{i})$ for some
$i\leq n$ and $v_{1}\sqsubset_{\delta_{B}}\dots\sqsubset_{\delta_{B}}v_{i}$ in
$\mathbb{E}_{k}\mathfrak{t}^{J}B$. We need to construct an embedding
$d:(Q,\chi)\rightarrowtail(W,\omega)$ that ‘fills the diagonal’.

Suppose $w_{j}=w_{i}[a_{i+1}{:}s_{i+1},\dots,a_{j}{:}s_{j}]$ such that $w_{j}$
are the elements in the image of $e_{1}$, but not in the image of $e_{1}\circ
e$. By repeated applications of the forth property, we obtain pairs
$(w_{j},v_{j})\in W_{s}$ with
$v_{j}=v_{i}[b_{i+1}{:}s_{i+1},\dots,b_{j}{:}s_{j}]$. Let
$d(r_{z})=(w_{z},v_{z}){:}s_{z}$ for all $z\leq n$. By the winning condition
on $W_{s}$, $d$ is indeed an embedding. Hence, the following diagram commutes:

${(P,\pi)}$${(Q,\chi)}$${(W,\omega)}$${F^{\mathbb{E}_{k}}\mathfrak{t}^{J}A}$$\scriptstyle{e_{0}}$$\scriptstyle{e_{1}}$$\scriptstyle{d}$$\scriptstyle{p_{1}}$

A similar proof shows that $p_{2}:(W,\omega)\rightarrow F^{\mathbb{E}_{k}}B$
is a open pathwise embedding.

$(2)\Rightarrow(1)$ Suppose we have span of open pathwise embeddings
$F^{\mathbb{E}_{k}}\mathfrak{t}^{J}A\xleftarrow{h_{1}}(W,\omega)\xrightarrow{h_{2}}F^{\mathbb{E}_{k}}\mathfrak{t}^{J}B$.
We prove the following statement by induction on $n\leq k$:

$(*)$ For every $s\in S$ and $b\in B_{s}$, there exists a path $P$ consisting
of constants $\mathbf{cs}(P)$ and a chain
$r_{1}\sqsubset_{\pi}\dots\sqsubset_{\pi}r_{n}$ with embedding
$d:(P,\pi)\rightarrowtail(W,\omega)$ and $a\in A_{s}$ such that:

  * •

$\varepsilon_{A}(h_{1,s}(d_{s}(r_{n})))=a$ and
$\varepsilon_{B}(h_{2,s}(d_{s}(r_{n})))=b$

  * •

The $S$-sorted relation $\gamma$ defined componetwise:

$\displaystyle\gamma_{n,t}$ $\displaystyle=\\{(c^{A},c^{B})\mid
c\in\mathbf{cs}(\sigma,t)\\}$ $\displaystyle\cup\\{(a_{j},b_{j})\mid\text{ for
$r_{j}\in P_{t}$ and $j\leq n$}\\}$

where $a_{j}=h_{1,t}(d_{t}(r_{j}))$ and $b_{j}=h_{2,t}(d_{t}(r_{j}))$ is a
partial isomorphism on $J$.

For the base case $0$, since $h_{1}:(W,\omega)\rightarrow
F^{\mathbb{E}_{k}}\mathfrak{t}^{J}A$ and $h_{2}:(W,\omega)\rightarrow
F^{\mathbb{E}_{k}}\mathfrak{t}^{J}B$ are $\sigma$-morphism, $h_{1}$ and
$h_{2}$ send constants to constants. Therefore, the $S$-sorted set given by
$\gamma_{s}=\\{(h_{1}(c^{R}),h_{2}(c^{R}))\mid
c\in\mathbf{cs}(\sigma,s)\\}=\\{(c^{A},c^{B})\mid
c\in\mathbf{cs}(\sigma,s)\\}$ is a partial isomorphism (and in particular, a
partial isomorphism on $J$). We set $P$ to be the $0$-length chain containing
only interpretations for the constants in $\mathbf{cs}(\sigma,s)$.

For the inductive step, suppose $s\in S$ and $b\in B_{s}$. By the inductive
hypothesis, there exists a path $(P,\pi)$ containing constants and a chain
$r_{1}\sqsubset_{\pi}\dots\sqsubset_{\pi}r_{n}$ with embedding
$d:(P,\pi)\rightarrowtail(W,\omega)$. Consider the extension of this path to
$(Q,\chi)$ where $Q_{s^{\prime}}=P_{s^{\prime}}$ for $s^{\prime}\not=s$ and
$Q_{s}=P_{s}\cup\\{r_{n+1}\\}$. We define $\chi$ componentwise where
$\chi_{s^{\prime}}=\pi_{s^{\prime}}$ for all $s^{\prime}\not=s$ and
$\chi_{s}(r)=\pi_{s}(r)$ for $r\not=r_{n+1}$,
$\chi_{s}(r_{n+1})=[r_{1}{:}s_{1},\dots,r_{n}{:}s_{n},r_{n+1}{:}s]$. We can
define an embedding $e:(Q,\chi)\rightarrowtail
F^{\mathbb{E}_{k}}\mathfrak{t}^{J}B$ such that $e_{s^{\prime}}=h_{2,s}\circ
d_{s^{\prime}}$ for $s^{\prime}\not=s$, $e_{s}(r)=h_{2,s}(d_{s}(r))$ for all
$r\not=r_{n+1}$ and $e_{s}(r_{n+1})=h_{2,s_{n}}(d_{s_{n}}(r_{n}))[b{:}s]$. By
construction, we have that the following diagram commutes:

${(P,\pi)}$${(Q,\chi)}$${(W,\omega)}$${F^{\mathbb{E}_{k}}\mathfrak{t}^{J}B}$$\scriptstyle{e_{0}}$$\scriptstyle{e_{1}}$$\scriptstyle{h_{2}}$

Hence, by $h_{2}$ being a open map, there exists an embedding
$f:(Q,\chi)\rightarrowtail(W,\omega)$. To verify that $\gamma_{n,t}$ is
partial isomorphism on $J$, we note that by $h_{1},h_{2}$ pathwise embeddings,
we have that $h_{1}\circ f$ and $h_{2}\circ f$ are embeddings. Therefore:

$\displaystyle R^{\mathfrak{t}^{J}A}(a_{i_{1}},\dots,a_{i_{m}})$
$\displaystyle\Leftrightarrow
R^{\mathfrak{t}^{J}A}(\varepsilon_{A}(h_{1,s_{1}}(f(r_{i_{1}}))),\dots,\varepsilon_{A}(h_{1,s_{m}}(f(r_{i_{m}}))))$
$\displaystyle\Leftrightarrow
R^{\mathbb{E}_{k}\mathfrak{t}^{J}A}(h_{1,s_{1}}(f(r_{i_{1}})),\dots,h_{1,s_{m}}(f(r_{i_{m}})))$
$\displaystyle\Leftrightarrow R^{Q}(r_{i_{1}},\dots,r_{i_{m}})$
$\displaystyle\Leftrightarrow
R^{\mathbb{E}_{k}\mathfrak{t}^{J}B}(h_{2,s_{1}}(f(r_{i_{1}})),\dots,h_{2,s_{m}}(f(r_{i_{m}})))$
$\displaystyle\Leftrightarrow
R^{\mathfrak{t}^{J}B}(\varepsilon_{B}(h_{2,s_{1}}(f(r_{i_{1}}))),\dots,\varepsilon_{B}(h_{2,s_{m}}(f(r_{i_{m}}))))$
$\displaystyle\Leftrightarrow
R^{\mathfrak{t}^{J}B}(b_{i_{1}},\dots,b_{i_{m}})$

for all relations of $R\in\sigma^{J}$ of arity $R$. In particular, this
equivalence holds for the relations $I_{s}\in\sigma^{J}$. Since $I$ is
interpreted as equality in $\mathfrak{t}^{J}A$ and $\mathfrak{t}^{J}B$, we
have that $\gamma_{n,t}$ is a partial isomorphism on $J$.

Now to show that Duplicator has winning strategy in $\mathbf{EF}_{k}(A,B)$,
suppose at the $n$-th round Spoiler chooses $s$ and $b\in B_{s}$, then by
$(*)$, Duplicator can respond with $a\in A_{s}$ producing a partial
isomorphism $\gamma_{n}$ on $J$. If Spoiler chooses $s\in S$ and $a\in A_{s}$,
we can prove a statement similar to $(*)$ which implies that Duplicator can
respond with a $b\in B_{s}$ that results in a partial isomorphism on $J$.

Proposition A.34 and A.36 conclude the proof of the first item of proposition
4.2, demonstrating that $\equiv_{\text{FO}_{k}(S,J)}$ is captured by the many-
sorted $\mathbb{E}_{k}$

For the next part, we use the following fact, which allows us to reason about
$\mathbb{E}_{k}^{\text{nc}}$-coalgebras the same way as about
$\mathbb{E}_{k}$-coalgebras.

######  Lemma A.38.

Given a many-sorted signature $\sigma$, and the comonads $\mathbb{E}_{k}$ and
$\mathbb{E}_{k}^{\text{nc}}$ on $\mathcal{R}^{S}(\sigma)$ and
$\mathcal{R}^{S}_{\text{nc}}(\sigma)$, respectively, the categories
$\mathsf{EM}(\mathbb{E}_{k})$ and $\mathsf{EM}(\mathbb{E}_{k}^{\text{nc}})$
are isomorphic.

Moreover, the factorisation systems (surjective, strong mono) on
$\mathcal{R}^{S}(\sigma)$ and $\mathcal{R}^{S}_{\text{nc}}(\sigma)$ lift to
the identical factorisation system on both categories of coalgebras.

######  Proof A.39.

We check that every morphism involved in the definition
$A\leftrightarrow_{\mathbb{E}_{k}}B$ exists in the category
$\mathcal{R}_{\text{nc}}(\sigma)$. First, observe that the embedding of
categories
$I\colon\mathcal{R}_{\text{nc}}(\sigma)\hookrightarrow\mathcal{R}(\sigma)$
lifts to an embedding
$\widehat{I}\colon\mathsf{EM}(\mathbb{E}_{k}^{\text{nc}})\hookrightarrow\mathsf{EM}(\mathbb{E}_{k})$.
Indeed, the obvious comonad morphism
$I\circ\mathbb{E}_{k}^{\text{nc}}\to\mathbb{E}_{k}\circ I$ introduces a
functor $\widehat{I}$, mapping every coalgebra
$A\to\mathbb{E}_{k}^{\text{nc}}A$ to
$A\to\mathbb{E}_{k}^{\text{nc}}A\hookrightarrow\mathbb{E}_{k}A$. Moreover,
$\widehat{I}$ is surjective on objects (i.e.
$\mathsf{EM}(\mathbb{E}_{k}^{\text{nc}})$ is a wide subcategory of
$\mathsf{EM}(\mathbb{E}_{k})$), because every coalgebra $A\to\mathbb{E}_{k}A$
is uniquely determined by its order $\sqsubseteq_{\alpha}$ on non-constants
via the mapping $a\mapsto[x_{1},\dots,x_{n}]$ where $[x_{1},\dots,x_{n}]$ is
the chain of non-constant elements below $a$ (with $x_{n}=a$). This chain only
lists non-constants and therefore factors through
$\mathbb{E}_{k}^{\text{nc}}(A)\subseteq\mathbb{E}_{k}(A)$. Moreover, the
underlying homomorphism of every coalgebra morphism in
$\mathsf{EM}(\mathbb{E}_{k})$ is in $\mathcal{R}_{\text{nc}}(\sigma)$ (i.e.
$\widehat{I}$ is an isomorphism of categories).

Next, observe the following.

  1. 1.

$\mathcal{R}_{\text{nc}}(\sigma)$ contains all embeddings: this is automatic
by the definition of $\mathcal{R}_{\text{nc}}(\sigma)$ and the fact that
embeddings are injective.

  2. 2.

$\mathbb{E}_{k}^{\text{nc}}$ preserves embeddings.

  3. 3.

The factorisation system (surjective, strong injective) in
$\mathcal{R}(\sigma)$ restricts to $\mathcal{R}_{\text{nc}}(\sigma)$.

By (1), (2), (3) and lemma 2.3, $\mathsf{EM}(\mathbb{E}_{k}^{\text{nc}})$
consists of the same quotients and embeddings as in
$\mathsf{EM}(\mathbb{E}_{k})$.

For the second item of proposition 4.2 we remark that the coalgebra $(W,v)$ in
the proof of proposition A.36 can be be restricted to
$\mathbb{E}_{k}^{\text{nc}}$, i.e. plays where constants are never selected by
Spoiler nor Duplicator. Conversely, we know that in the presence of equality,
the action of Spoiler and Duplicator are determined when playing constants. So
a span of open pathwise embeddings
$F^{\mathbb{E}_{k}^{\text{nc}}}(\mathfrak{t}^{J}_{\text{nc}}A)\leftarrow
R\rightarrow F^{\mathbb{E}_{k}^{\text{nc}}}(\mathfrak{t}^{J}_{\text{nc}}B)$
contains a full strategy for the $\mathbf{EF}^{J}_{k}(A,B)$ game. Hence, the
construction proceeds as in the direction (2) $\Rightarrow$ (1) of the proof
of proposition A.36.

###  A.10 Proofs for section 4.2

See 4.3 We prove that bisimulation for the $\mathfrak{t}^{e}$-lifting of
$S$-sorted equivalence captures equivalence in $\text{MSO}_{k}$, by first
noting the functor $\mathfrak{t}^{e}$ decomposes as
$\mathfrak{t}^{J}\circ\mathfrak{u}^{e}$ where $J=\\{\mathbf{f}\\}$ and
$\mathfrak{u}^{e}\colon\mathcal{R}(\sigma)\rightarrow\mathcal{R}(\sigma^{e}\setminus\\{I\\})$
is functor from $\mathcal{R}(\sigma)$ to a category of $S$-sorted
$\sigma^{e}$-structures $\mathcal{R}(\sigma^{e}\setminus\\{I\\})$ without the
$I$-relation. For a $\sigma$-structure $A$, $\mathfrak{u}^{e}(A)$ is the
$\sigma^{e}\setminus\\{I\\}$ reduct of $\mathfrak{t}^{e}(A)$. We then prove
the following lemma by adapting the translation detailed in footnote 12 of
[42] which translates full second-order logic into many-sorted first-order
logic:

######  Lemma A.40.

  * •

For every $\text{MSO}_{k}$ sentence $\phi$ in signature $\sigma$, there exists
a $\text{FO}_{k}(S,J)$ sentence $F(\phi)$ in signature
$\sigma^{e}\setminus\\{I\\}$ such that

$A\vDash\phi\Leftrightarrow\mathfrak{u}^{e}A\vDash F(\phi)$

  * •

For every $\text{FO}_{k}(S,J)$ sentence $\phi$ in signature
$\sigma^{e}\setminus\\{I\\}$, there exists a $\text{MSO}_{k}$ sentence
$M(\phi)$ in signature $\sigma$ such that

$A\vDash M(\phi)\Leftrightarrow\mathfrak{u}^{e}A\vDash\phi$

######  Proof A.41.

We can define $F$ and $M$ by recursion on MSO and FO formulas (respectively):

$\displaystyle F(x_{i}=x_{j})$
$\displaystyle=v_{i}{:}\mathbf{f}=v_{j}{:}\mathbf{f}$ $\displaystyle
F(x_{i}\in X_{j})$ $\displaystyle=e(v_{i}{:}\mathbf{f},w_{j}{:}\mathbf{m})$
$\displaystyle F(R(x_{i_{1}},\dots,x_{i_{r}}))$
$\displaystyle=R(v_{i_{1}}{:}\mathbf{f},\dots,v_{i_{r}}{:}\mathbf{f})$
$\displaystyle F(\varphi\land\psi)$ $\displaystyle=F(\varphi)\land F(\psi)$
$\displaystyle F(\neg\varphi)$ $\displaystyle=\neg F(\varphi)$ $\displaystyle
F(\exists x_{i}\,\varphi)$
$\displaystyle=\exists\,v_{i}{:}\mathbf{f}\,F(\varphi)$ $\displaystyle
F(\exists X_{i}\,\varphi)$
$\displaystyle=\exists\,w_{i}{:}\mathbf{m}\,F(\varphi)$ $\displaystyle
M(v_{i}{:}\mathbf{f}=v_{j}{:}\mathbf{f})$ $\displaystyle=x_{i}=x_{j}$
$\displaystyle M(e(v_{i}{:}\mathbf{f},w_{j}{:}\mathbf{m}))$
$\displaystyle=x_{i}\in X_{j}$ $\displaystyle
M(R(v_{i_{1}}{:}\mathbf{f},\dots,v_{i_{r}}{:}\mathbf{f}))$
$\displaystyle=R(x_{i_{1}},\dots,x_{i_{r}})$ $\displaystyle
M(\varphi\land\psi)$ $\displaystyle=M(\varphi)\land M(\psi)$ $\displaystyle
M(\neg\varphi)$ $\displaystyle=\neg M(\varphi)$ $\displaystyle
M(\exists\,v_{i}{:}\mathbf{f}\,\varphi)$ $\displaystyle=\exists
x_{i}\,M(\varphi)$ $\displaystyle M(\exists\,w_{i}{:}\mathbf{m}\,\varphi)$
$\displaystyle=\exists X_{i}\,M(\varphi)$

The proofs that $A\vDash\phi\Leftrightarrow\mathfrak{u}^{e}A\vDash F(\phi)$
and $A\vDash M(\phi)\Leftrightarrow\mathfrak{u}^{e}A\vDash\phi$ are immediate
from the standard semantics of $\vDash$.

With this lemma and previous results about the many-sorted $\mathbb{E}_{k}$,
we obtain the proof of 4.3

######  Proof A.42 (Proof of theorem 4.3).

$\displaystyle A\equiv_{\text{MSO}_{k}}B$
$\displaystyle\Leftrightarrow\mathfrak{u}^{e}A\equiv_{\text{FO}_{k}(S,J)}\mathfrak{u}^{e}B$
by lemma A.40
$\displaystyle\Leftrightarrow\mathfrak{t}^{J}\mathfrak{u}^{e}A\leftrightarrow_{\mathbb{E}_{k}}\mathfrak{t}^{J}\mathfrak{u}^{e}B$
by prop. 4.2
$\displaystyle\Leftrightarrow\mathfrak{t}^{e}A\leftrightarrow_{\mathbb{E}_{k}}\mathfrak{t}^{e}B$
$\displaystyle\mathfrak{t}^{e}=\mathfrak{t}^{J}\circ\mathfrak{u}^{e}$

Moreover, since the condition in the second item of proposition 4.2 is
satisfied for our choice of $J$ and $\mathbf{cs}(\sigma,\mathbf{f})$, we can
obtain
$A\equiv_{\text{MSO}_{k}}B\Leftrightarrow\mathfrak{t}^{e}_{\text{nc}}A\leftrightarrow_{\mathbb{E}_{k}^{\text{nc}}}\mathfrak{t}^{e}_{\text{nc}}B$
using the same argument.

###  A.11 Proofs for section 4.3

See 4.5

######  Proof A.43.

This proof proceeds similarly to the proof that
${\operatorname{join}_{\bar{i}}^{R}}$ is FO-$\mathbb{E}_{k}$-smooth. Axioms
(F1) and (F2) follow automatically because the underlying function of $\kappa$
is the two-sorted identity function.

To check that $\kappa$ is a smooth Kleisli law, we to check that $\kappa$
satisfies the smoothness axioms from (S1) and (S2’) from lemma A.24.

For (S1), we can repeat the verification of (S1) as in lemma 3.15 nearly
verbatim, but instead of using the relations in $R,P_{i_{z}}\in\sigma$, we use
the corresponding relations $R,P_{i_{z}}\in\sigma^{e}$. By definition, the
interpretations of these relations are the same.

For (S2’), suppose $\pi\colon P\to\mathbb{E}_{k}P$ is a path
$r_{1}\sqsubset_{\pi}r_{2}\sqsubset_{\pi}\dots\sqsubset_{\pi}r_{n}$ and
$f\colon\pi\to[\alpha]$ is a multilinear map. The proof that $\widehat{f}$ has
a minimal decomposition follows nearly verbatim to the FO case in lemma 3.15.
The key difference is that $\kappa$ is the two-sorted identity function.

In addition to demonstrating that $\kappa$ is a Kleisli law. We must also show
there exists a natural transformation
$\theta:{\operatorname{join}_{\bar{i}}^{R,e}}\circ\mathfrak{t}^{e}\rightarrow\mathfrak{t}^{e}\circ{\operatorname{join}_{\bar{i}}^{R}}$
such that $F^{\mathbb{E}_{k}}(\theta_{A})$ is an open pathwise embedding. The
components $\theta_{A}$ are given by $S$-sorted functions where $\theta_{A,t}$
sends an element $x\in
A_{t}\in{\operatorname{join}_{\bar{i}}^{R,e}}(\mathfrak{t}^{e}(A))$ the same
element in $\mathfrak{t}^{e}{\operatorname{join}_{\bar{i}}^{R}}(A)$. The
interpretation of $Q\in\sigma^{e}\setminus\\{e,I\\}$ has the same tuples as
the interpretation of $Q\in\sigma$ (including $R$). Moreover, since
$\mathfrak{t}^{e}{\operatorname{join}_{\bar{i}}^{R}}(A)$ and
${\operatorname{join}_{\bar{i}}^{R,e}}\mathfrak{t}^{e}(A)$ have the same
universe, the membership relation (consequently, interpretations of $e$) and
the identity relation (consequently, interpretations of $I$) are the same, so
we have that $\theta_{A}$ is a $\sigma^{e}$-morphism. Since $\theta_{A}$ is
the $S$-sorted identity function, the underlying set function of
$F^{\mathbb{E}_{k}}(\theta_{A})$ is the identity and it is easy to check that
$F^{\mathbb{E}_{k}}(\theta_{A})$ is an open pathwise embedding.

###  A.12 Proofs for section 4.4

We first verify the following claim.

######  Lemma A.44.

$\theta\colon\mathfrak{t}^{e}(A)\bowtie\mathfrak{t}^{e}(B)\to\mathfrak{t}^{e}(A\mathbin{\parallel}B)$
is a strong onto homomorphism.

######  Proof A.45.

Since $\theta$ is defined as the identity function on the $\mathbf{f}$-sort,
this holds true for the $\sigma_{3}$-reduct and the $\mathbf{f}$-sort part of
$\theta$. On the $\mathbf{m}$-sort, $\theta$ is clearly onto. So we only need
to check that the $e$ relation is reflected. Let $a\in A$, $M\subseteq A$ and
$N\subseteq B$. Assume that
$(\mathfrak{i}(a),\mathfrak{i}(M)\cup\mathfrak{i}(N))\in
e^{\mathfrak{t}^{e}(A\mathbin{\parallel}B)}$, i.e.
$\mathfrak{i}(a)\in\mathfrak{i}(M)\cup\mathfrak{i}(N)$. If $a$ is non-constant
then clearly $a\in M$ and so $(a,(M,N))\in
e^{\mathfrak{t}^{e}(A)\bowtie\mathfrak{t}^{e}(B)}$. Otherwise, $a$ is a
constant, i.e. $a=c^{A}$ for some $c\in\mathbf{cs}(\sigma)$. Then, no matter
if $a\in\mathfrak{i}(M)$ or $a\in\mathfrak{i}(N)$, we have that
$(c^{A\mathbin{\parallel}B},(M,N))\in
e^{\mathfrak{t}^{e}(A)\bowtie\mathfrak{t}^{e}(B)}$, which concludes the proof
because $\iota(a)=\iota(c^{A})=c^{A\mathbin{\parallel}B}$.

The fact that $F^{\mathbb{E}_{k}^{\text{nc}}}(\theta)$ is component-wise an
open pathwise embedding then follows from the following.

######  Lemma A.46.

For a multi-sorted signature $\sigma$, if $q$ is a strong onto homomorphism in
$\mathcal{R}^{S}_{\text{nc}}(\sigma)$ then $F^{\mathbb{E}_{k}^{\text{nc}}}(q)$
is an open pathwise-embedding.

######  Proof A.47.

In the following, we will write $U\dashv F$ for the adjunction
$U^{\mathbb{E}_{k}^{\text{nc}}}\dashv F^{\mathbb{E}_{k}^{\text{nc}}}$. Observe
that the correspondence

$\displaystyle\hom(U(\pi),A)\cong\hom(\pi,F(A)),$ (10)

for $\pi$ an $\mathbb{E}_{k}^{\text{nc}}$-path and $A$ a (multi-sorted)
$\sigma$-structure, restrict to a bijection between strong homomorphisms
$U(\pi)\to A$ and (path) embeddings $\pi\to F(A)$.

To check that $F(q)\colon F(A)\to F(B)$ is a pathwise-embedding, let
$e\colon\pi\rightarrowtail F(A)$ be a path embedding. By the above, this
embedding corresponds to a strong homomorphism $e^{r}\colon
U(\pi)\rightarrowtail A$. Then, $q\circ e^{r}$ is a strong homomorphism
$e^{r}\colon U(\pi)\rightarrowtail B$ because $q$ is also strong. Therefore,
the corresponding coalgebra morphism $(q\circ
e^{r})^{l}\colon\pi\rightarrowtail F(B)$ is an embedding and $F(q)\circ
e=(q\circ e^{r})^{l}$ by naturality of (10).

For openness, let $\pi$ and $\rho$ be paths and the following is a commutative
square of path embeddings shown on left below.

${\pi}$${\rho}$${F(A)}$${F(B)}$$\scriptstyle{e}$$\scriptstyle{h}$$\scriptstyle{g}$$\scriptstyle{F(q)}$
${U(\pi)}$${U(\rho)}$${A}$${B}$$\scriptstyle{e^{l}}$$\scriptstyle{U(h)}$$\scriptstyle{g^{l}}$$\scriptstyle{d}$$\scriptstyle{q}$

In view of (10), we have a commuting diagram on the right above, giving us
that $\pi$ corresponds to a word (of non-constants)
$[x_{1}:s_{1},\dots,x_{n}:s_{n}]$ in $A$ and $\rho$ corresponds to a word (of
non-constants) $[y_{1}:s^{\prime}_{1},\dots,y_{m}:s^{\prime}_{m}]$ where
$n\leq m$, $s_{i}=s^{\prime}_{i}$ and $q(x_{i})=y_{i}$, for $1\leq i\leq n$.
Since $q$ is onto, there exist $x_{j}\in A_{s_{j}}$ such that
$q_{s_{j}}(x_{j})=y_{j}$, for $n+1\leq j\leq m$. We define $d\colon U(\rho)\to
A$ by sending $y_{i}\mapsto x_{i}$ (for $1\leq i\leq m$). It is easy to see
that $d$ is a homomorphism because $q$ is a strong homomorphism. Also, the map
$d$ makes both triangles in the diagram commute, by definition. Consequently,
we have a coalgebra homomorphism $d^{r}\colon\rho\to F(A)$ making the obvious
triangles on the left diagram above commute.

######  Lemma A.48.

$\kappa\colon\mathbb{E}_{k}^{\text{nc}}(A\bowtie
B)\to\mathbb{E}_{k}^{\text{nc}}(A)\bowtie\mathbb{E}_{k}^{\text{nc}}(B)$ is a
smooth Kleisli law.

######  Proof A.49.

The proof of the fact that $\kappa$ is a well-defined natural transformation
that satisfies (F1), (F2), (S1), and (S2’) is identical to the single-sorted
proof of the same, in the proof lemma 3.16 above, with the only addition that
we have to keep track of sorts.

Also, $\mathsf{EM}(\mathbb{E}_{k}^{\text{nc}})$ has equalisers of reflexive
pairs. This follows from lemma 3.8, adapted verbatim to the multi-sorted
setting. Since $\kappa$ is a Kleisli law, the functor $\bowtie$ lifts to a
functor
$\mathbin{\widehat{\bowtie}}\colon\mathsf{EM}(\mathbb{E}_{k}^{\text{nc}})\times\mathsf{EM}(\mathbb{E}_{k}^{\text{nc}})\to\mathsf{EM}(\mathbb{E}_{k}^{\text{nc}})$
and so $\kappa$ is smooth by theorem 3.14 and lemma A.24.

This now follows from the observations above. See 4.6

###  A.13 Proofs for section 5

See 5.1

######  Proof A.50.

For the proof we build a (bottom-up finite) tree automaton. The set of states
of this automaton is the set $S=\\{1,\,\dots,\,(t_{1}+\dots+t_{n})\\}$ where
$t_{i}$ is the total number of
$\leftrightarrow_{\mathbb{C}_{i}}^{\mathfrak{t}_{i}}$-equivalence classes in
$\mathcal{R}_{0}(\sigma_{i})$, for $i=1,\dots,n$. Since every comonad
$\mathbb{C}_{i}$ has finite MSO type and since we only have finitely many
categories, we know that $t_{1}+\dots+t_{n}$ is a finite number. For the
alphabet we take the set $\\{o_{H}\mid H\in\mathcal{H}\\}$ of names for
operations in $\mathcal{H}$, where the arity of $o_{H}$ is precisely the arity
of the functor $H$ (ignoring the types).

Next, let $l_{A}\in S$ be the label corresponding to the
$\leftrightarrow_{\mathbb{C}_{i}}^{\mathfrak{t}_{i}}$-equivalence class of
$A$, for every $A\in\mathcal{R}(\sigma_{i})$ and $1\leq i\leq n$. Then, for
transition rules, given $H\in\mathcal{H}$ of type
$\mathcal{R}(\sigma_{i(1)})\times\dots\times\mathcal{R}(\sigma_{i(u)})\to\mathcal{R}(\sigma_{i(u+1)})$
and structures $A_{l}\in\sigma_{i(l)}$, for $1\leq l\leq u$, we add the
transition

$o_{H}(l_{A_{1}},\dots,l_{A_{n}})\enspace\leadsto\enspace
l_{H(A_{1},\dots,A_{n})}.$

We see that this transition is deterministic because every $H\in\mathcal{H}$
is MSO-$(\mathbb{C}_{1},\dots,\mathbb{C}_{n})$-smooth.

Lastly, we define the accepting states as those $l_{A}\in S$ such that the
$\tau$-reduct of $A$ is in $\Delta$. This, is well-defined by assumption (3).

Now, given any term $t_{A}$, we build a tree $T_{A}$ by translating every
constant $B\in\mathcal{B}$ into the label $l_{B}$ and every operation
application of $H\in\mathcal{H}$ into the letter $o_{H}$. Recall that checking
if an input tree is accepted can be done in linear time, for any tree
automaton. Lastly, observe that, by construction, $T_{A}$ is accepted if and
only if $A\in\Delta$.

###  A.14 Proofs for section 5.1

Recall that
$\operatorname{fg}_{C,D}\colon\mathcal{R}_{0}(\sigma_{C})\to\mathcal{R}_{0}(\sigma_{D})$,
for $D\subseteq C\subseteq\\{c_{1},\dots,c_{m}\\}$, is the operation which
sends a relational structure $A$, in signature $\sigma_{C}$, to its
$\sigma_{D}$-reduct. This operation naturally extends to the two-sorted
functor
$\operatorname{fg}_{C,D}^{e}\colon\mathcal{R}_{\text{nc}}(\sigma^{e}_{C})\to\mathcal{R}_{\text{nc}}(\sigma^{e}_{D})$,
which acts as the identity mapping on morphisms.

We immediately see that
$\mathfrak{t}^{e}\circ\operatorname{fg}_{C,D}\cong\operatorname{fg}_{C,D}^{e}\circ\mathfrak{t}^{e}$.
Therefore, for MSO-$\mathbb{E}_{k}^{\text{nc}}$-smoothness of
$\operatorname{fg}_{C,D}$, we only need to find a smooth Kleisli law

$\kappa\colon\mathbb{E}_{k}^{\text{nc}}\circ\operatorname{fg}_{C,D}^{e}\to\operatorname{fg}_{C,D}^{e}\circ\mathbb{E}_{k}^{\text{nc}}.$

Given $A$ in $\mathcal{R}_{\text{nc}}(\sigma^{e}_{C})$, we divide its universe
as $A_{\mathbf{f}}\uplus A_{\mathbf{m}}=A_{0}\uplus C_{0}\uplus D$ where
$D=\\{c^{A}\mid c\in\mathbf{cs}(\sigma_{D})\\}$, $C_{0}=\\{c^{A}\mid
c\in\mathbf{cs}(\sigma_{C})\setminus\mathbf{cs}(\sigma_{D})\\}$ and
$A_{0}=A_{\mathbf{f}}\uplus A_{\mathbf{m}}\setminus(D\cup C_{0})$. Recall that
the universe of $\mathbb{E}_{k}^{\text{nc}}(\operatorname{fg}_{C,D}^{e}(A))$
consists of $(A_{0}\cup C_{0})^{\leq k}\uplus\mathbf{cs}(\sigma_{D})$ whereas
the universe of $\operatorname{fg}_{C,D}^{e}(\mathbb{E}_{k}^{\text{nc}}(A))$
consists of $A_{0}^{\leq k}\uplus\mathbf{cs}(\sigma_{C})$, with only
$\mathbf{cs}(\sigma_{D})\subseteq\mathbf{cs}(\sigma_{C})$ marked as constants.
Define $\kappa$ componentwise on non-constants by (while preserving the sorts
as usual):

$\displaystyle\kappa\colon\mathbb{E}_{k}^{\text{nc}}(\operatorname{fg}_{C,D}^{e}(A))$
$\displaystyle\enspace\longrightarrow\enspace\operatorname{fg}_{C,D}^{e}(\mathbb{E}_{k}^{\text{nc}}(A)),$
$\displaystyle w\in(A_{0}\cup C_{0})^{\leq k}$
$\displaystyle\enspace\longmapsto\enspace\begin{cases}\mathtt{ex}(w)\in
A_{0}^{\leq k}&\text{ if }\varepsilon(w)\in A_{0}\\\\[5.0pt]
c^{\mathbb{E}_{k}^{\text{nc}}(A)}&\text{ if }\varepsilon(w)=c^{A}\in
C_{0}\end{cases}$

Here $\mathtt{ex}([x_{1}:s_{1},\dots,x_{n}:s_{n}])$ is defined as
$[x_{i}:s_{i}\mid x_{i}\in A_{0}]$. It is clear that $\kappa$ is a
$\sigma_{D}$-structure homomorphism. Furthermore, it sends non-constants to
non-constants since $c^{\mathbb{E}_{k}^{\text{nc}}(A)}$ with $c^{A}\in C_{0}$
is no longer a constant in
$\operatorname{fg}_{C,D}^{e}(\mathbb{E}_{k}^{\text{nc}}(A))$. The reasoning
justifying that axioms (F1) and (F2) hold is exactly the same for lemma 3.16
and (S1) holds for trivial reasons. Lastly, we check (S2’). Assume we are
given a path embedding, in terms of a multilinear map $e$ as shown below.

${P}$${\operatorname{fg}_{C,D}^{e}(A)}$${\mathbb{E}_{k}^{\text{nc}}(P)}$${\mathbb{E}_{k}^{\text{nc}}\operatorname{fg}_{C,D}^{e}(A)}$${\operatorname{fg}_{C,D}^{e}(\mathbb{E}_{k}^{\text{nc}}A)}$$\scriptstyle{e}$$\scriptstyle{\pi}$$\scriptstyle{\operatorname{fg}_{C,D}^{e}(\alpha)}$$\scriptstyle{\mathbb{E}_{k}^{\text{nc}}(e)}$$\scriptstyle{\kappa}$

Let
$x_{1}:s_{1}\sqsubset_{\pi}x_{1}:s_{1}\sqsubset_{\pi}\dots\sqsubset_{\pi}x_{n}:s_{n}$
be the chain of non-constant elements of $P$. The commutativity of the above
square means that, for every $i$,

$\kappa([a_{1}:s_{1},\dots,a_{i}:s_{i}])=\alpha(a_{i})$

where $a_{j}$ is set to be $e(x_{j})$, for $1\leq j\leq n$. In other words, if
$a_{i}\in A_{0}$ it must be that the word
$\kappa([a_{1}:s_{1},\dots,a_{i}:s_{i}])$ is the chain of non-constant
elements $\sqsubset_{\alpha}$-below $a_{i}$ in $A$. If $a_{i}\in C_{0}$ then
we automatically get that $\kappa([a_{1}:s_{1},\dots,a_{i}:s_{i}])=a_{i}$ and
also $\alpha(a_{i})=a_{i}$, making this automatically satisfied. Therefore,
the word $[a_{1}:s_{1},\dots,a_{n}:s_{n}]$ consists of elements from a path
$(P^{\prime},\pi^{\prime})$ in $(A,\alpha)$ interleaved by constant elements
from $C_{0}$. It is immediate that $e$ factors through
$\operatorname{fg}_{C,D}^{e}(e^{\prime})$ of the embedding
$e^{\prime}\colon(P^{\prime},\pi^{\prime})\rightarrowtail(A,\alpha)$ and that
this $(P^{\prime},\pi^{\prime})$ is minimal possible. As a result we obtain
the following by theorem 3.14 and lemma A.24.

######  Lemma A.51.

For every $D\subseteq C\subseteq\\{c_{1},\dots,c_{m}\\}$, the operation
$\operatorname{fg}_{C,D}\colon\mathcal{R}(\sigma_{C})\to\mathcal{R}(\sigma_{D})$
is MSO-$\mathbb{E}_{k}^{\text{nc}}$-smooth.

###  A.15 Proofs for section 5.2

What remains to check to support theorem 5.5 is the following claim.

######  Lemma A.52.

For every $i,j\in\\{1,\dots,m\\}$, the operation
$\operatorname{relab}_{i,j}:\mathcal{R}(\sigma_{m})\to\mathcal{R}(\sigma_{m})$
is MSO-$\mathbb{E}_{k}$-smooth.

######  Proof A.53.

It is clear that
$\operatorname{relab}_{i,j}\colon\mathcal{R}(\sigma_{m})\rightarrow\mathcal{R}(\sigma_{m})$
and the corresponding two-sorted operation
$\operatorname{relab}_{i,j}^{e}\colon\mathcal{R}^{S}(\sigma^{e}_{m})\rightarrow\mathcal{R}^{S}(\sigma^{e}_{m})$
are functorial. We need to define smooth Kleisli law

$\kappa\colon\mathbb{E}_{k}\circ\operatorname{relab}_{i,j}^{e}\rightarrow\operatorname{relab}_{i,j}^{e}\circ\mathbb{E}_{k}$

The components $\kappa_{A}$ are given by $S$-sorted functions where
$\kappa_{A,t}$ sends a word
$w\in(\mathbb{E}_{k}(\operatorname{relab}_{i,j}(A)))_{t}$ to the same word
$w\in(\operatorname{relab}_{i,j}(\mathbb{E}_{k}(A)))_{t}$ for
$t\in\\{\mathbf{f},\mathbf{m}\\}=S$. This is the same definition, on the level
of $S$-sorted sets, as the smooth Kleisli law used to witness that
${\operatorname{join}_{\bar{i}}^{R}}$ is MSO-$\mathbb{E}_{k}$-smooth. We also
need to exhibit a natural transformation
$\theta:\operatorname{relab}_{i,j}^{e}\circ\mathfrak{t}^{e}\rightarrow\mathfrak{t}^{e}\circ\operatorname{relab}_{i,j}$.
As in the case of ${\operatorname{join}_{\bar{i}}^{R}}$, we define the
components $\theta_{A}$ to be the $S$-sorted identify function sending an
element $a\in\operatorname{relab}_{i,j}^{e}(\mathfrak{t}^{e}(A))$ to the same
element $a\in\mathfrak{t}^{e}(\operatorname{relab}_{i,j}A)$. Consequently, the
proof of lemma 4.5 can be adapted to demonstrate that
$\operatorname{relab}_{i,j}$ is MSO-$\mathbb{E}_{k}$-smooth.


# Global Motion Understanding in Large-Scale Video Object Segmentation

Volodymyr Fedynyak
Ukrainian Catholic University
<EMAIL_ADDRESS>Yaroslav Romanus
Ukrainian Catholic University
<EMAIL_ADDRESS>Oles Dobosevych
Ukrainian Catholic University
<EMAIL_ADDRESS>Igor Babin
ADVA Soft
<EMAIL_ADDRESS>Roman Riazantsev
ADVA Soft
<EMAIL_ADDRESS>
###### Abstract

In this paper, we show that transferring knowledge from other domains of video
understanding combined with large-scale learning can improve robustness of
Video Object Segmentation (VOS) under complex circumstances. Namely, we focus
on integrating scene global motion knowledge to improve large-scale semi-
supervised Video Object Segmentation. Prior works on VOS mostly rely on direct
comparison of semantic and contextual features to perform dense matching
between current and past frames, passing over actual motion structure. On the
other hand, Optical Flow Estimation task aims to approximate the scene motion
field, exposing global motion patterns which are typically undiscoverable
during all pairs similarity search. We present WarpFormer, an architecture for
semi-supervised Video Object Segmentation that exploits existing knowledge in
motion understanding to conduct smoother propagation and more accurate
matching. Our framework employs a generic pretrained Optical Flow Estimation
network whose prediction is used to warp both past frames and instance
segmentation masks to the current frame domain. Consequently, warped
segmentation masks are refined and fused together aiming to inpaint occluded
regions and eliminate artifacts caused by flow field imperfects. Additionally,
we employ novel large-scale MOSE 2023 dataset to train model on various
complex scenarios. Our method demonstrates strong performance on DAVIS
2016/2017 validation (93.0% and 85.9%), DAVIS 2017 test-dev (80.6%) and
YouTube-VOS 2019 validation (83.8%) that is competitive with alternative
state-of-the-art methods while using much simpler memory mechanism and
instance understanding logic.

##  1 Introduction

Video Object Segmentation (VOS) is a fundamental task in Video Understanding,
aiming to segment multiple objects through an entire video sequence. In this
work, we address semi-supervised video object segmentation, i.e. the scenario
where only the first frame annotations are given, or the annotations are given
only for the frames where the corresponding object appears in the video for
the first time.

The key feature of Video Object Segmentation is the complete agnosticity of
the actual class information for considered objects. This allows a very broad
range of possible applications, including but not limited to autonomous
driving, sports and video editing.

Prior works achieved significant success in VOS, focusing on making solution
highly generalizable and robust under different complex scenarios while
maintaining real-time efficiency and low GPU memory footprint. AOT [38]
proposed to map objects to a pre-defined set of feature vectors making
possible simultaneous processing of many instances. While most works use
feature memory to correctly treat occlusions and eliminate errors during
propagation, XMem [7] points out the high memory consumption of such an
approach and designs efficient unified multi-type memory inspired by Atkinson-
Shiffrin model. DeAOT [39] notes the poor performance of existing methods when
the objects drastically change in scale and appearance during the video,
presenting a novel feature decoupling block to treat such cases more robustly.
ISVOS [33] argues that instance understanding matters in VOS and employ an
instance segmentation branch based on state-of-the-art instance segmentation
architectures increasing the VOS performance for video clips with a high
number of similar objects.

Existing approaches rely on dense attention-based feature matching [30] to
propagate segmentation masks through the video sequence. Even though this
achieves remarkably high scores on existing benchmarks, a single all-pairs
correlation search is not capable of capturing global motion context and
uncovering relevant motion patterns. In this work, we argue that motion
understanding matters in VOS. Inspired by ISVOS proposing to reuse existing
instance segmentation architectures to improve instance understanding for VOS
domain, we propose to reuse existing optical flow estimation architectures to
propagate instance information between video frames.

We present WarpFormer, an VOS architecture that benefits from global motion
structure knowledge. We adopt a generic VOS architecture for spatial-temporal
matching similar to [38] and replace short-term memory mechanism with optical
flow warp, for which we employ a flow estimation network. The propagation
process is tackled by optical flow warp while the spatial windowed attention
is used to refine warped segmentation mask and inpaint occlusions. Finally,
refined mask is fused with long-term memory matches and passed to decoder.

We conduct additional training of our model on large-scale MOSE 2023 [8]
dataset to achieve robustness under complex VOS scenarios. We evaluate our
method on DAVIS 2016 & 2017 and YouTube-VOS 2019 benchmarks. Conducted
experiments demonstrate that both exploiting global motion structure and
large-scale training improve evaluation scores and qualitative results.

##  2 Related Work

Figure 1: The architecture of a WarpFormer. Best viewed in color.

###  2.1 Optical Flow Estimation

Optical flow is a critical component of our work. Its main idea is to estimate
the shift of all points from one frame to another. Early approaches in that
area were focused on optimization problems, maximizing visual similarity with
regularization terms [11, 2, 3, 27]. However, the advent of deep neural
networks, specifically convolutional networks, propelled the field forward.
Pioneering models like FlowNet [9] and FlowNet2.0 [14] set the stage for more
advanced methods, such as SpyNet [24], PWC-Net [28], and LiteFlowNet [13]
which adopted coarse-to-fine and iterative estimation strategies.

Despite their advancements, these models struggled to capture small, fast-
moving objects during the coarse stage. The RAFT model [29] introduced
significant improvements, a novel architecture employing a coarse-and-fine
(multi-scale search window per iteration), and a recurrent approach to optical
flow estimation. Subsequent works based on RAFT, such as GMA [16] and DEQ-Flow
[1], aimed to improve computational efficiency or enhance flow accuracy.

A recent example of a state-of-the-art recurrent approach is FlowFormer
[12]—an extension of the RAFT architecture. It introduces a transformer-based
method that aggregates cost volume in a latent space. This approach builds on
the work of Perceiver IO [15], which was the first to incorporate transformers
[30] for establishing long-range relationships in optical flow, achieving
state-of-the-art performance. FlowFormer retains the cost volume as a compact
similarity representation and pushes the search space to the extreme by
globally aggregating similarity information using a transformer architecture.
Another state-of-the-art approach is GMFlow [35], which formulates optical
flow as a global matching problem and employs a customized Transformer for
feature enhancement, global feature matching, and flow propagation. This
approach outperforms the RAFT on the Sintel benchmark while offering greater
efficiency [35].

###  2.2 Video Object Segmentation

One popular method that has achieved state-of-the-art performance in VOS is
AOT (Associating Objects with Transformers for VOS) [38]. AOT exploits the
Long Short-Term Transformer (LSTT) block that includes self-attention, short-
term attention, and long-term attention to extract features from input images.
Long-term attention is responsible for aggregating information from long-term
memory frames, while short-term attention propagates information from the
previous frame. The outputs of long-term and short-term attention blocks are
combined in the feed-forward network, which passes information to the decoder
that returns mask estimation for the current frame. AOT also uses a joint
architecture that includes an attention map for the attention blocks and a 4D
correlation volume, as in the RAFT [29] architecture, to calculate the same
spatial correlation between frames. The short-term attention in AOT and 4D
correlation volume in RAFT calculate the same correlation between features
from consecutive frames, which can be combined in the shared part of the joint
architecture as a unified motion representation.

DeAOT [39] (Decoupling Features in Hierarchical Propagation for Video Object
Segmentation) is a recent method for semi-supervised video object segmentation
that builds on the hierarchical propagation introduced in the AOT approach.
DeAOT decouples the hierarchical propagation of object-agnostic and object-
specific embeddings into two independent branches to prevent the loss of
object-agnostic visual information in deep propagation layers. To compensate
for the additional computation from dual-branch propagation, DeAOT introduces
a Gated Propagation Module that is carefully designed with single-head
attention. Experimental results show that DeAOT outperforms AOT in both
accuracy and efficiency, achieving new state-of-the-art performance on several
benchmarks, including YouTube-VOS, DAVIS 2016 and DAVIS 2017.

###  2.3 Optical Flow-based Video Segmentaiton

Optical flow-based Video Object Segmentation has progressed substantially over
time. One of the early works in this domain, MaskTrack [17], combined object
segmentation and tracking by employing optical flow for object mask
propagation and refining the results using a convolutional neural network
(CNN). Building on this foundation, OSVOS [4] further enhanced segmentation
performance.

More advanced methods like PDB [40] and RVOS [31] emerged, employing multi-
stage frameworks and recurrent neural networks, respectively, while still
leveraging optical flow. The Regional Memory Network (RMNet) [34] recently
introduced a local-to-local matching approach that minimizes mismatches with
similar objects using regional memory embedding and optical flow-based
tracking.

We build on these foundational works in our proposed method, utilizing optical
flow for short-term frames and attention mechanism for long-term frames to
enhance the segmentation process.

##  3 Method

###  3.1 Background

Video object segmentation is a challenging task that often involves tracking
multiple objects of interest in a single video. Previous approaches to this
problem have focused on matching and propagating a single object, requiring
independent matching and propagation of each object in multi-object scenarios
[32]. This can result in increased GPU usage and inference time, hindering the
efficiency of the overall pipeline.

To address this challenge, AOT proposed an identification mechanism for
embedding masks of any number into the same high-dimensional space, enabling
multi-object scenario training and inference as efficient as single-object
ones [38]. This mechanism involves creating a predefined set of $M$ trainable
vectors, known as the identity bank, and picking a vector from this bank for
each pixel corresponding to a specific class. During training, the vector
corresponding to each class is randomly selected to ensure uniform training of
the identity bank. To add object-specific information to the feature maps in
our architecture, which are at the $\frac{1}{16}$ spatial size of the input
video, we adopt a patch-wise identity bank strategy similar to AOT [38]. This
involves dividing the input mask into non-overlapping $16\times 16$ patches,
matching each pixel in the patch with the corresponding vector from the
identity bank, and obtaining the final result for the identity bank by summing
the values for the pixels inside the patch. This operation also encodes some
geometry inside the patch and can be implemented as a single $16\times 16$
convolution.

###  3.2 Warp Refinement Transformer

Figure 2: Warpformer Modules. Best viewed in color.

(a) Refinement Transformer Block

(b) Windowed Cross-Attention

(c) Cross-Attention

The straightforward approach for VOS uses optical flow to propagate masks from
the previous frame to the current frame. However, occlusions and optical flow
imperfections can lead to errors in mask propagation, degrading the quality of
the propagated mask with each frame. Additionally, this approach cannot handle
newly appeared parts of an object. Our proposed method, WarpFormer, aims to
refine the estimated mask using semantic information, which is easier to
interpret after motion was decoupled. The overall architecture of WarpFormer
is shown in Figure 1.

To achieve this, some previous frame $I_{k}$ and mask $M_{k}$ is used as a
reference point. Our method calculates optical flow using a given Flow
Estimator:

$f_{k\to t}=\mbox{FE}(I_{k},I_{t})$

To estimate the current frame mask, the following equation is used:

$M_{k}^{warp}=\mbox{Warp}(M_{k},f_{k\to t})$

The method then warps the previous frame $I_{k}$ using the same optical flow
$f_{k\to t}$ to obtain $I_{k}^{warp}$. Next, the features $X_{t}$ and $X_{k}$
are extracted from the current frame $I_{t}$ and $I_{k}^{warp}$ using a
Feature Encoder and embedding $Y_{k}$ of our mask $M_{k}^{warp}$ is formed
from an identity bank. Similarly, we create features $X_{m}$ and
identification embedding $Y_{m}$ from the long-term memory frames $I_{m}$ with
masks $M_{m}$. The resulting information is fed into our Refinement
Transformer Block, which outputs the refined mask $\widehat{M_{t}}$. Finally,
the decoder upsamples the refined mask estimation to the spatial dimensions of
the current frame.

###  3.3 Refinemenet Transformer Block

Table 1: The quantitative evaluation on multi-object benchmarks YouTube-VOS 2019 and DAVIS 2017. * denotes training on MOSE 2023. Bold denotes the best or three best results. FPS in brackets denotes the value measured not including optical flow estimation time.  | YouTube-VOS 2019 Val | DAVIS 2017 Val | DAVIS 2017 Test |
---|---|---|---|---
Methods | $\mathcal{J}_{s}$ | $\mathcal{F}_{s}$ | $\mathcal{J}_{u}$ | $\mathcal{F}_{u}$ | $\mathcal{J}\&\mathcal{F}$ | $\mathcal{J}$ | $\mathcal{F}$ | $\mathcal{J}\&\mathcal{F}$ | $\mathcal{J}$ | $\mathcal{F}$ | $\mathcal{J}\&\mathcal{F}$ | FPS
AOT-T | 79.6 | 83.8 | 73.7 | 81.8 | 79.7 | 77.4 | 82.3 | 79.9 | 68.3 | 75.7 | 72.0 | 51.4
DeAOT-T | 81.2 | 85.6 | 76.4 | 84.7 | 82.0 | 77.7 | 83.3 | 80.5 | 70.0 | 77.3 | 73.7 | 63.5
WarpFormer-S | 79.0 | 85.1 | 73.5 | 82.8 | 80.1 | 77.6 | 84.2 | 80.9 | 66.2 | 76.1 | 71.1 | 27.7 (37.0)
WarpFormer-S* | 79.0 | 85.3 | 73.1 | 82.5 | 80.1 | 77.8 | 84.3 | 81.0 | 65.9 | 76.1 | 71.0 | 27.7 (37.0)
CFBI+ | 81.7 | 86.2 | 77.1 | 85.2 | 82.6 | 80.1 | 85.7 | 82.9 | 74.4 | 81.6 | 78.0 | 3.4
RMNet | 74.0 | 82.2 | 80.2 | 79.9 | 77.4 | 81.0 | 86.0 | 83.5 | 71.9 | 78.1 | 75.0 | -
STCN | 81.1 | 85.4 | 78.2 | 85.9 | 82.7 | 82.2 | 88.6 | 85.4 | 73.1 | 80.0 | 76.1 | 19.5
XMem | 84.3 | 88.6 | 80.3 | 88.6 | 85.5 | 82.9 | 89.5 | 86.2 | 77.4 | 84.5 | 81.0 | 20.2
ISVOS | 85.2 | 89.7 | 80.7 | 88.9 | 86.1 | 83.7 | 90.5 | 87.1 | 79.3 | 86.2 | 82.8 | -
Swin-B AOT-L | 84.0 | 88.8 | 78.4 | 86.7 | 84.5 | 82.4 | 88.4 | 85.4 | 77.3 | 85.1 | 81.2 | 12.1
Swin-B DeAOT-L | 85.3 | 90.2 | 80.4 | 88.6 | 86.1 | 83.1 | 89.2 | 86.2 | 78.9 | 86.7 | 82.8 | 15.4
WarpFormer-L | 83.2 | 88.9 | 78.1 | 84.9 | 83.8 | 81.1 | 88.9 | 85.0 | 76.4 | 84.9 | 80.6 | 10.0 (23.9)
WarpFormer-L* | 83.3 | 89.1 | 78.0 | 85.0 | 83.8 | 82.4 | 89.3 | 85.9 | 76.3 | 84.9 | 80.6 | 10.0 (23.9)

Many recent cutting-edge VOS methods have utilized the attention mechanism and
have demonstrated promising results. To define the attention mechanism
formally, we consider queries ($Q$), keys ($K$), and values ($V$). The
attention operation can then be defined as follows:

$\mbox{Att}(Q,K,V)=\mbox{Corr}(Q,K)V=\operatorname{softmax}\Bigl{(}\frac{QK^{T}}{\sqrt{C}}\Bigr{)}V$

where $C$ is the number of channels.

In our method, we incorporate the identification embedding into the attention
operation for mask refinement as follows:

$\mbox{AttID}(Q,K,V,ID)=\mbox{Att}(Q,K,V+ID)$

Following the common transformer blocks, our Refinement Transformer Block
(RTB) first employs a self-attention layer on the features of the images to
learn the association between the targets within our frames (Figure 2(a)). Our
RTB, similarly to the AOT[38], is then divided into two branches: long-term
and short-term.

The long-term branch (Figure 2(c)) is responsible for aggregating information
from long-term (reference) memory frames. It utilizes simple cross-attention,
defined as:

$\mbox{CAtt}(X_{t},X_{m},Y_{m})=\mbox{AttID}(X_{t}W_{k},X_{m}W_{k},X_{m}W_{v},Y_{m}),$

where $X_{m}$ and $Y_{m}$ are the features and masks embeddings of the long-
term memory frames. Besides, $W_{k}$ and $W_{v}$ are trainable projections for
matching and refinement, respectively.

The short-term (sensory memory) branch (Figure 2(b)) propagates information
from the previous frames by taking a look at only some neighboring patches to
apply matching. Since image changes between consecutive frames are smooth and
continuous, this approach is only more powerful as we convert our previous
frames to the current frame domain after warp. The short-term branch utilizes
windowed cross-attention:

$\mbox{WCAtt}(X_{t},X_{l},Y_{l}|p)=\mbox{Catt}(X_{t}^{p},X_{l}^{N(p)},Y_{l}^{N(p)})$

where $X_{l}$ and $Y_{l}$ are the features and masks embeddings of warped
previous frames, $X_{t}^{p}$ \- feature of $X_{t}$ at location $p$ and $N(p)$
is a $\lambda\times\lambda$ spatial neighborhood centered at location $p$,
where $\lambda$ is window size. We implement windowed cross-attention by
including a relative position bias $B$:

$\mbox{WCAtt}(Q,K,V)=\operatorname{softmax}\Bigl{(}\frac{QK^{T}}{\sqrt{C}}+B\Bigr{)}V$

Finally, the outputs of the long-term and short-term branches are combined
together in one more self-attention layer.

##  4 Implementation Details

###  4.1 Network details

To study performance capabilities and contributions impact we introduce two
variants of network architecture. Namely, WarpFormer-S (Small) is an efficient
implementation of the proposed method, which adopts MobileNet-V2 [25] as
encoder backbone, only a single reference frame is exploited for long-term
memory. Alternatively, WarpFormer-L (Large) is a large-scale implementation,
for which we adopt cutting edge transformer-based encoder Swin-B [19];
following [38], we append every 2 frame to long-term memory bank for training
and every 5 frame for evaluation. For both architecture variants we use FPN
decoder with Group Normalization [18]. We employ Global Motion Aggregation
(GMA) [16] as an optical flow estimating network for both WarpFormer-S and
WarpFormer-L; however, we set the number of flow optimization updates to 4 for
small architecture and to 12 for a large.

Following [38], we set the number of identification vectors $M$ to 10 in order
to align it with the maximum object number in most of benchmarks. For encoders
and patch-wise identity bank, their final resolution is $\frac{1}{16}$ as of
an input image and mask. For self-attention and cross-attention blocks in Warp
Refinement Transformer we use traditional multi-head architecture [30] with
Feed-Forward layer and Layer Normalization. The embedding dimension is set to
256, the number of heads is 8 and the hidden dimension of Feed-Forward layers
is 1024. For windowed cross-attention used to refine warped sensory memory, we
employ original implementation [19] with relative position bias and
additionally equip learned relative positional embedding [26]. The window size
is set to 15. We also apply fixed sine spatial positional embedding to the
self-attention following [5].

###  4.2 Training details

We train both architecture variants in two stages. On the first stage, the
model is trained for 40K optimization steps, while the second stage takes 60K
steps. During the entire training process, we employ a mixture of DAVIS 2017
[23, 4] train and YouTube-VOS 2019 [37, 36] train datasets in $5:1$
proportion. Additionally, we study adopting MOSE 2023 [8] as additional
training data, in which case we apply DAVIS, YouTube-VOS and MOSE mixture with
proportion $5:k:p$ where $k+p=1$. Initial value of $k_{start}=0.5$ linearly
decays during the training to a final value $k_{end}=0.25$. More detailed
description of datasets is presented in Sec. 5.1. For both stages we use
curriculum sampling strategy [21]. Notably, ground truth memory masks are used
for temporal-spatial matching during the first stage, while second stage only
implies an utilization of the first reference mask providing better
supervision for inference setup. Identity banks are frozen after the first
stage following [38].

We adopt AdamW optimizer [20] with a one-cycle learning rate schedule. Initial
learning rate of $lr_{start}=3\times 10^{-4}$ declines to a final value of
$lr_{end}=2\times 10^{-5}$ in polynomial manner with $0.9$ decay factor. We
also use learning rate warm-up [10] for 3000 steps. In order to prevent
overfitting, we set the learning rate for the encoder to $0.1$ of the overall
learning rate. Following [7], we use bootstrapped cross entropy and dice
losses with equal weighting. For both stages, we use a batch size of 8.
WarpFormer-L model training is distributed across four RTX 3090 GPUs, while
for WarpFromer-S we use only two RTX 3090 GPUs. The entire training process
takes around 40 hours for the large model and 35 hours for the small one.

###  4.3 Video augmentations

Figure 3: Qualitative comparison between WarpFormer and several state-of-the-
art VOS methods. Best viewed in zoom. We don’t include ISVOS [33] since there
is no source code available. For all methods we used DAVIS2017 val sequences
in 480p.

We employ a variety of video augmentations to prevent overfitting on the seen
data. Specifically, we apply random scaling followed by object-balanced random
cropping to the sampled sequence. Additionally, color jitter, random Gaussian
blur and random grey-scaling are applied to RGB images.

Dynamic merge augmentation. In order to better adapt our model to a multi-
object scenario, we adopt dynamic merging augmentation. To enrich generated
sequence with more objects, we generate another sequence of the same length
from a different video clip and overlay it on the top of the first one. In
details, the merging process is as follows: for pair of corresponding frames
from the first and second sequence the resulting frame at pixel $(x,y)$,
denoted by $I_{merge}(x,y)$, is set to $I_{1}(x,y)$ if no objects from the
second image are present at that pixel, and $I_{2}(x,y)$ otherwise.

For both training stages we employ the full set of augmentations, for the
DAVIS and YouTube-VOS dynamic merge augmentation is applied with probability
0.4, for MOSE merge augmentation is not used since it already features complex
multi-object scenes.

##  5 Results

Table 2: The quantitative evaluation on DAVIS 2016. Bold denotes the best result. Methods | $\mathcal{J}$ | $\mathcal{F}$ | $\mathcal{J}\&\mathcal{F}$
---|---|---|---
AOT-T | 86.1 | 87.4 | 86.8
DeAOT-T | 87.8 | 89.9 | 88.9
WarpFormer-S | 87.2 | 90.5 | 88.9
RMNet | 88.9 | 88.7 | 88.8
STCN | 90.8 | 92.5 | 91.6
XMem | 90.4 | 92.7 | 91.5
ISVOS | 91.5 | 93.7 | 92.6
Swin-B AOT-L | 90.7 | 93.3 | 92.0
Swin-B DeAOT-L | 91.1 | 94.7 | 92.9
WarpFormer-L | 90.7 | 95.3 | 93.0

###  5.1 Metrics and Dataset

In order to evaluate our models we use traditional VOS metrics as proposed in
[23].

$\boldsymbol{\mathcal{J}}$ score for region similarity evaluation.
$\mathcal{J}$ score (Jaccard index) is defined as the intersection-over-union
(IoU) rate of the predicted and ground-truth segmentation mask. Given a
predicted mask $\widehat{M}$ and ground-truth mask $G$:

$\mathcal{J}=\frac{|\widehat{M}\displaystyle\cap
G|}{|\widehat{M}\displaystyle\cup G|}$

$\boldsymbol{\mathcal{F}}$ score for contour accuracy evaluation. To estimate
contour matching accuracy, one finds the contour-based precision $P_{c}$ and
recall $R_{c}$ between the boundaries of the predicted and ground-truth mask.
Subsequently, one computes a F1-score as a simple harmonic mean:

$\mathcal{F}=\frac{2P_{c}R_{c}}{P_{c}+R_{c}}$

Scores are averaged on whole video clip separately for each object.
$\boldsymbol{\mathcal{J}}\boldsymbol{\&}\boldsymbol{\mathcal{F}}$ score is the
average of $\mathcal{J}$ score and $\mathcal{F}$ score presenting a good
trade-off between boundary quality and region matching.

DAVIS 2016 [22] is a single-object VOS benchmark containing 20 video
sequences. Even though single-object scenario is significantly less complex
then the multi-object setup, the benchmark features various challenging
scenarios including heavy occlusions, objects changing in shape, scale and
appearance, fast movements and unfavorable environment settings.

DAVIS 2017 [23] benchmark complements DAVIS 2016 with multi-object video
clips. It contains 205 different objects and features a 16.1% disappearance
rate [8]. Benchmark presents train, validation and test-dev splits containing
60, 30 and 30 sequences respectively. While validation split doesn’t introduce
a high amount of unseen during training classes, test-dev is much more
challenging featuring complex circumstances in most of videos.

We evaluate our method on DAVIS 2016 & 2017 using the default 480p 24FPS
videos, not benefiting from full-resolution details. Also we do not apply any
test-time augmentations like multi-scale inference [6].

YouTube-VOS [37, 36] benchmark introduces a large-scale VOS dataset covering a
wide variety of in-the-wild videos. YouTube-VOS 2019 training and validation
splits contain 3471, 474 video sequences respectively. Dataset features 91
object categories (7755 objects in total), 26 of which are not present in
training split. The explicit annotation of unseen classes is available and the
official evaluation tool additionally computes separate metrics for seen and
unseen classes to benchmark the generalization power of the approaches. The
disappearance rate is only 13% [8], so, in general, YouTube-VOS implies less
challenging circumstances compared to DAVIS.

While evaluation our method on YouTube-VOS 2019 validation split we exploit
all intermediate frames of the videos to benefit from smooth motion implying
more accurate optical flow. Even though we use 24 FPS sequences during
evaluation, 6FPS version is used during training and for metric computation.

Table 3: The quantitative evaluation on MOSE 2023. * denotes training on MOSE 2023. Bold denotes the best result. Methods | $\mathcal{J}$ | $\mathcal{F}$ | $\mathcal{J}\&\mathcal{F}$
---|---|---|---
STCN | 46.6 | 55.0 | 50.8
RDE | 44.6 | 52.9 | 48.8
SWEM | 46.8 | 54.9 | 50.9
WarpFormer-S* | 47.7 | 55.6 | 51.7
XMem | 53.3 | 62.0 | 57.6
Swin-B AOT-L | 53.1 | 61.3 | 57.2
Swin-B DeAOT-L | 55.1 | 63.8 | 59.4
WarpFormer-L* | 55.1 | 64.9 | 60.0

MOSE 2023 [8] (CoMplex video Object SEgmentation) is a novel VOS benchmark
featuring extreme scenarios of the video sequence which are not handled good
enough by existing VOS methods. The main features of introduced videos
include: large number of crowded and similar objects, heavy occlusions by
similar looking objects, extremely small-scale objects and reference masks
covering only a small region of the whole object. MOSE contains 1507 training
and 311 validation video clips with 36 object categories (5200 objects in
total). MOSE features overall disappearance rate of 28.8% which is
significantly higher compared to classic VOS benchmarks.

###  5.2 Comparison with State-of-the-art Methods

Our method doesn’t adopt complex memory model used in existing methods (XMem
[7]), neither it features special architecture injecting instance segmentation
logic to benefit from better instance-specific understanding (ISVOS [33]).
Also both our small and large models feature only a single transformer block
for spatial-temporal matching while existing methods (AOT [38], DeAOT [39])
use up to three blocks. Instead, we incorporate additional training data from
MOSE 2023, allowing WarpFormer to tackle scenarios with heavy occlusions,
large number of overlapping similar objects or objects dramatically changing
in appearance and scale.

Quantitative comparison. The comparison of WarpFormer with other state-of-the-
art methods on DAVIS 2017 validation, DAVIS 2017 test-dev and Youtube-VOS 2019
validation validation may be found in Table 1. The quantitative comparison
with relevant existing methods on DAVIS 2016 validation are listed in Table 2.

Without training on MOSE 2023, our Swin-B WarpFormer-L achieves state-of-the-
art performance on DAVIS 2016 single-object benchmark scoring 93.0%
$\mathcal{J}\&\mathcal{F}$. Being evaluated on multi-object benchmarks, model
demonstrates highly competitive performance wrapping up with top-ranked scores
_i.e_. 85.0% and 80.6% $\mathcal{J}\&\mathcal{F}$ on DAVIS 2017 validation and
test-dev splits and 83.8% $\mathcal{J}\&\mathcal{F}$ on Youtube-VOS 2019
validation.

Trained only on Youtube-VOS and DAVIS, our MobileNet-V2 WarpFormer-S
outperforms most of its competitors on both single-object and multi-object
benchmarks. Namely, it scores 88.9%, 81.0% and 71.0%
$\mathcal{J}\&\mathcal{F}$ on DAVIS 2016 validation and DAVIS 2017 validation
& test-dev. YouTube-VOS 2019 validation score is 80.1%
$\mathcal{J}\&\mathcal{F}$. We believe that strong and balanced performance
under different complex scenarios, simple architecture and lightweight encoder
along with agnosticity of actual flow estimation method make WarpFormer-S
ideal candidate for usage in various industrial applications.

Qualitative comparison. The qualitative comparison of state-of-the-art
approaches and our method is visualized in Fig. 3. Existing methods fail to
reconstruct fine-grained details under the rapid motion circumstances. In
contrast, our method benefits from global motion field and is much more robust
to motion blur. On the other hand, adopting MOSE as additional training data
gives enough supervision to successfully handle overlapping similar objects
without having special architecture design, as instance segmentation branch
[33] or feature decoupling module [39].

###  5.3 Training with MOSE 2023

Adopting MOSE 2023 as training data gives a significant boost on MOSE 2023
validation split so that both our WarpFormer-S and WarpFormer-L models achieve
state-of-the-art performance among competitors, scoring 51.7% and 60.0%
$\mathcal{J}\&\mathcal{F}$ respectively. One the other hand, performance on
the classic benchmarks experience an insignificant boost, likely because they
doesn’t feature any similar extreme scenarios. However, they focus on
circumstances with a large number of object classes and classes unseen during
training, along with a wide variety of challenging environments, while MOSE
2023 lacks such flexibility. Wrapping up, even minor improvements on classic
benchmarks while training with MOSE 2023 indicate the high robustness and
performance capacity of the proposed method. The quantitative comparison with
other methods on MOSE 2023 validation are listed in Table 3.

###  5.4 Optical Flow benchmark

We benchmark different optical flow estimation methods during evaluation on
DAVIS 2017. As our architecture is completely agnostic to the actual
implementation of the flow estimator, we test various approaches in terms of
performance / resource requirements trade-off. For RAFT-based models [29, 16,
12], we also try various numbers of iterative flow updates. To demonstrate the
impact of flow-warped windowed attention refinement, we also include ”zero-
flow”, which implies identity transformation; in this case, our sensory memory
processing degenerates to simple windowed attention similar to [38]. The
quantitative comparison may be found in Table 4.

The results indicate that our model is indeed optical flow agnostic, and its
performance is directly proportional to the quality of the flow. Additionally,
for iterative-based optical flow approaches, we observed that a smaller number
of iterations was sufficient to achieve fairly good results. This may be
attributed to the model’s ability to already capture the global motion trend.
However, the accuracy of ”zero-flow” deteriorated, as our network was trained
solely for refinement, rather than direct matching.

Table 4: Optical Flow estimator benchmark. Subscript denotes the number of flow optimization iterations. Methods | $\mathcal{J}\&\mathcal{F}$ | $\\#\text{param.}$ | FPS
---|---|---|---
MobileNet-V2
Zero-Flow | 76.1 | 7.7M | 57.8
RAFT-S4 | 80.5 | 8.7M | 34.7
RAFT4 | 80.7 | 13M | 33.6
RAFT12 | 80.7 | 13M | 18.4
GMA1 | 80.2 | 13.6M | 37.0
GMA4 | 80.8 | 13.6M | 27.7
GMA12 | 81.0 | 13.6M | 12.6
GMA32 | 80.8 | 13.6M | 6.1
FlowFormer | 80.7 | 23.9M | 3.9
Swin-B
Zero-Flow | 80.7 | 64.9M | 32.2
GMA1 | 85.0 | 70.8M | 23.9
GMA4 | 85.7 | 70.8M | 15.2
GMA12 | 85.9 | 70.8M | 10.0
FlowFormer | 85.9 | 81.1M | 3.6

##  6 Conclusion

This paper proposes to reuse existing motion understanding knowledge by
adopting optical flow estimation network to support a generic VOS
architecture. To integrate global motion structure we replace propagation with
optical flow warping and introduce Warp Refinement Transformer block, which
aims to inpaint occlusions and fuse warped segmentation mask with long-term
memory information. Experimental results show that our method demonstrates
strong performance and generalization capabilities. We believe that combining
WarpFormer with complex memory mechanisms or specific architecture blocks for
instance understanding may further boost it effectivness.

##  7 Acknowledgements

The work is supported by Ukrainian Catholic University and ADVA Soft.

## References

  * [1] Shaojie Bai, Zhaoyang Geng, Yash Savani, and J Zico Kolter.  Deep equilibrium optical flow estimation.  arXiv preprint arXiv:2204.08442, 2022.
  * [2] Michael J Black and P Anandan.  A framework for the robust estimation of optical flow.  In Proceedings of the 4th International Conference on Computer Vision, pages 231–236. IEEE, 1993.
  * [3] André Bruhn, Joachim Weickert, and Christoph Schnörr.  Lucas/kanade meets horn/schunck: Combining local and global optic flow methods.  International journal of computer vision, 61(3):211–231, 2005.
  * [4] S. Caelles, K. K. Maninis, J. Pont-Tuset, L. Leal-Taixé, D. Cremers, and L. Van Gool.  One-shot video object segmentation.  In Proceedings of the IEEE conference on computer vision and pattern recognition, pages 221–230, 2017.
  * [5] Nicolas Carion, Francisco Massa, Gabriel Synnaeve, Nicolas Usunier, Alexander Kirillov, and Sergey Zagoruyko.  End-to-end object detection with transformers, 2020.
  * [6] Siddhartha Chandra and Iasonas Kokkinos.  Fast, exact and multi-scale inference for semantic image segmentation with deep gaussian crfs, 2016.
  * [7] Ho Kei Cheng and Alexander G. Schwing.  XMem: Long-term video object segmentation with an atkinson-shiffrin memory model.  In ECCV, 2022.
  * [8] Henghui Ding, Chang Liu, Shuting He, Xudong Jiang, Philip HS Torr, and Song Bai.  Mose: A new dataset for video object segmentation in complex scenes.  arXiv preprint arXiv:2302.01872, 2023.
  * [9] Alexey Dosovitskiy, Philipp Fischer, Eddy Ilg, Philip Häusser, Caner Hazirbas, Vladimir Golkov, Patrick Van Der Smagt, Daniel Cremers, and Thomas Brox.  Flownet: Learning optical flow with convolutional networks.  In Proceedings of the IEEE international conference on computer vision, pages 2758–2766, 2015.
  * [10] Akhilesh Gotmare, Nitish Shirish Keskar, Caiming Xiong, and Richard Socher.  A closer look at deep learning heuristics: Learning rate restarts, warmup and distillation, 2018.
  * [11] Berthold K Horn and Brian G Schunck.  Determining optical flow.  Artificial intelligence, 17(1-3):185–203, 1981.
  * [12] Ziqi Huang, Xuesong Shi, Chenxu Zhang, Qiyang Wang, Kin Chung Cheung, Hong Qin, Jifeng Dai, and Hao Li.  Flowformer: A transformer architecture for optical flow.  arXiv preprint arXiv:2203.16194, 2022.
  * [13] Tak-Wai Hui, Xiaoou Tang, and Chen Change Loy.  Liteflownet: A lightweight convolutional neural network for optical flow estimation.  In Proceedings of the IEEE conference on computer vision and pattern recognition, pages 8981–8989, 2018.
  * [14] Eddy Ilg, Nikolaus Mayer, Tonmoy Saikia, Margret Keuper, Alexey Dosovitskiy, and Thomas Brox.  Flownet 2.0: Evolution of optical flow estimation with deep networks.  In Proceedings of the IEEE conference on computer vision and pattern recognition, pages 2462–2470, 2017.
  * [15] Andrew Jaegle, Sébastien Borgeaud, Jean-Baptiste Alayrac, Carl Doersch, Catalin Ionescu, Dov Ding, Skanda Koppula, Dan Zoran, Andrew Brock, Evan Shelhamer, et al.  Perceiver io: A general architecture for structured inputs & outputs.  arXiv preprint arXiv:2107.14795, 2021.
  * [16] Saining Jiang, Dylan Campbell, Yi Lu, Hongdong Li, and Richard Hartley.  Learning to estimate hidden motions with global motion aggregation.  arXiv preprint arXiv:2104.02409, 2021.
  * [17] A. Khoreva, F. Perazzi, R. Benenson, B. Schiele, and A. Sorkine-Hornung.  Learning video object segmentation from static images.  arXiv preprint arXiv:1612.02646, 2016.
  * [18] Tsung-Yi Lin, Piotr Dollár, Ross Girshick, Kaiming He, Bharath Hariharan, and Serge Belongie.  Feature pyramid networks for object detection, 2017.
  * [19] Ze Liu, Yutong Lin, Yue Cao, Han Hu, Yixuan Wei, Zheng Zhang, Stephen Lin, and Baining Guo.  Swin transformer: Hierarchical vision transformer using shifted windows.  In Proceedings of the IEEE/CVF International Conference on Computer Vision (ICCV), 2021.
  * [20] Ilya Loshchilov and Frank Hutter.  Decoupled weight decay regularization, 2019.
  * [21] Seoung Wug Oh, Joon-Young Lee, Ning Xu, and Seon Joo Kim.  Video object segmentation using space-time memory networks, 2019.
  * [22] F. Perazzi, J. Pont-Tuset, B. McWilliams, L. Van Gool, M. Gross, and A. Sorkine-Hornung.  A benchmark dataset and evaluation methodology for video object segmentation.  In Computer Vision and Pattern Recognition, 2016.
  * [23] Jordi Pont-Tuset, Federico Perazzi, Sergi Caelles, Pablo Arbeláez, Alexander Sorkine-Hornung, and Luc Van Gool.  The 2017 davis challenge on video object segmentation.  arXiv:1704.00675, 2017.
  * [24] Anurag Ranjan and Michael J Black.  Optical flow estimation using a spatial pyramid network.  In Proceedings of the IEEE conference on computer vision and pattern recognition, pages 4161–4170, 2017.
  * [25] Mark Sandler, Andrew Howard, Menglong Zhu, Andrey Zhmoginov, and Liang-Chieh Chen.  Mobilenetv2: Inverted residuals and linear bottlenecks, 2019.
  * [26] Peter Shaw, Jakob Uszkoreit, and Ashish Vaswani.  Self-attention with relative position representations, 2018.
  * [27] Deqing Sun, Stefan Roth, and Michael J Black.  A quantitative analysis of current practices in optical flow estimation and the principles behind them.  International Journal of Computer Vision, 106(2):115–137, 2014\.
  * [28] Deqing Sun, Xiaodong Yang, Ming-Yu Liu, and Jan Kautz.  Pwc-net: Cnns for optical flow using pyramid, warping, and cost volume.  In Proceedings of the IEEE conference on computer vision and pattern recognition, pages 8934–8943, 2018.
  * [29] Zachary Teed and Jia Deng.  Raft: Recurrent all-pairs field transforms for optical flow.  In European Conference on Computer Vision, pages 402–419. Springer, 2020.
  * [30] Ashish Vaswani, Noam Shazeer, Niki Parmar, Jakob Uszkoreit, Llion Jones, Aidan N Gomez, Lukasz Kaiser, and Illia Polosukhin.  Attention is all you need.  In Advances in neural information processing systems, pages 5998–6008, 2017.
  * [31] C. Ventura, M. Bellver, A. Girbau, A. Salvador, F. Marqués, and X. Giro-i Nieto.  Rvos: End-to-end recurrent network for video object segmentation.  In Proceedings of the IEEE Conference on Computer Vision and Pattern Recognition (CVPR), pages 5277–5286, 2019.
  * [32] Paul Voigtlaender, Yuning Chai, Florian Schroff, Hartwig Adam, Bastian Leibe, and Liang-Chieh Chen.  Feelvos: Fast end-to-end embedding learning for video object segmentation, 2019.
  * [33] Junke Wang, Dongdong Chen, Zuxuan Wu, Chong Luo, Chuanxin Tang, Xiyang Dai, Yucheng Zhao, Yujia Xie, Lu Yuan, and Yu-Gang Jiang.  Look before you match: Instance understanding matters in video object segmentation, 2022.
  * [34] Haoxiang Xie, Wenhai Wang, Xiang Li, Lingxi Xie, Ya Zhang, and Qi Tian.  Rmnet: Equivalently removing residual connection from networks.  arXiv preprint arXiv:2111.00687, 2021.
  * [35] Hengshuang Xu, Jian Zhang, Jianfeng Cai, Hamid Rezatofighi, and Dacheng Tao.  Gmflow: Learning optical flow via global matching.  arXiv preprint arXiv:2111.13680, 2021.
  * [36] Ning Xu, Linjie Yang, Yuchen Fan, Jianchao Yang, Dingcheng Yue, Yuchen Liang, Brian Price, Scott Cohen, and Thomas Huang.  Youtube-vos: Sequence-to-sequence video object segmentation, 2018.
  * [37] Ning Xu, Linjie Yang, Yuchen Fan, Dingcheng Yue, Yuchen Liang, Jianchao Yang, and Thomas Huang.  Youtube-vos: A large-scale video object segmentation benchmark, 2018.
  * [38] Zongxin Yang, Yunchao Wei, and Yi Yang.  Associating objects with transformers for video object segmentation.  arXiv preprint arXiv:2106.02638, 2021.
  * [39] Zongxin Yang and Yi Yang.  Associating objects with transformers for video object segmentation.  arXiv preprint arXiv:2210.09782, 2022.
  * [40] Xuming Zhang, Wenguan Wang, Yuchen Liu, and Huchuan Lu.  Pdb: A multi-stage approach for video object segmentation.  In Proceedings of the IEEE Conference on Computer Vision and Pattern Recognition (CVPR), pages 3142–3151, 2019.


z((\theta^{\star},\bm{\psi}^{*},\bm{x}^{*},\\{{\bm{y}^{k}}^{\star}\\}_{k\in\mathcal{K}}),\bm{\xi}^{\prime})>0$.
The violation of the sequence
$\\{(\theta^{n+1},\bm{\psi}^{n+1},\bm{x}^{n+1},\\{\bm{y}^{k}\\}^{n+1}_{k\in\mathcal{K}}),\bm{\xi}^{n})\\}$
is always less than zero, and the sequence also converges to the same
accumulation point. Thus, we have
$z((\theta^{\star},\bm{\psi}^{*},\bm{x}^{*},\\{{\bm{y}^{k}}^{\star}\\}_{k\in\mathcal{K}}),\bm{\xi}^{\star})\leq
0$ and raise the desired contradiction.

We now show the optimality of the accumulation point of the solution sequence
corresponding to an infinite branch. If there is a solution of the problem
(8), denoted as
$(\overline{\theta},\overline{\bm{\psi}},\overline{\bm{x}},\\{\overline{\bm{y}}^{k}\\}_{k\in\mathcal{K}})$,
where ${\theta}^{\prime}\leq\theta^{\star}$. Then, using the same logic as the
correctness proof, it is either a node solution of the branch-and-cut tree or
an accumulation point of a sequence. In each case, the current objective value
will be updated to $\theta^{\prime}+\delta$, where $\delta\geq 0$ and is an
arbitrarily small number. Consequently, the branch corresponding to the
sequence
$\\{(\theta^{n},\bm{\psi}^{n},\bm{x}^{n},\\{{\bm{y}^{k}}\\}^{n}_{k\in\mathcal{K}})\\}_{1}^{+\infty}$
must be finite since it will be cut by a better solution. Therefore, we reach
a contradiction with the infinite branch and conclude our proof. ∎