0.60275ptx\colon g}\right\rrbracket(s,h)$ iff
$\displaystyle\alpha\leq\max\big{\\{}\left\llbracket{g}\right\rrbracket(s\left[{x}\texttt{:=}{v}\right],h)~{}\mid~{}v\in\mathsf{Vals}\big{\\}}$
iff $\displaystyle\text{there is a $v\in\mathsf{Vals}$
with}~{}\alpha\leq\left\llbracket{g}\right\rrbracket(s\left[{x}\texttt{:=}{v}\right],h)$
($\textsf{{Eval}}\left(g\right)$ is finite) iff $\displaystyle\text{there is a
$v\in\mathsf{Vals}$
with}~{}(s\left[{x}\texttt{:=}{v}\right],h)\models\lceil\alpha\preceq g\rceil$
(IH) iff $\displaystyle(s,h)\models\exists x\colon\lceil\alpha\preceq g\rceil$

_The case $f=\raisebox{0.6pt}{\rotatebox{-30.0}{{{\reflectbox{J}}}}}x\colon
g$_ is analogous to the previous case.

_The case $f=g\mathbin{{\star}}u$._

$\displaystyle\alpha\leq\left\llbracket{g\mathbin{{\star}}u}\right\rrbracket(s,h)$
iff
$\displaystyle\alpha\leq\max\left\\{\left\llbracket{g}\right\rrbracket(s,h_{1})\cdot\left\llbracket{u}\right\rrbracket(s,h_{2})~{}\mid~{}h=h_{1}\mathbin{{\star}}h_{2}\right\\}$
iff there exists $h_{1},h_{2}\in\textsf{{Heaps}}_{\Bbbk}$ with
$h=h_{1}\mathbin{{\star}}h_{2}$ and
$\displaystyle\qquad\alpha\leq\left\llbracket{g}\right\rrbracket(s,h_{1})\cdot\left\llbracket{u}\right\rrbracket(s,h_{2})$
($\textsf{{Eval}}\left(g\right)$ and $\textsf{{Eval}}\left(u\right)$ are
finite) iff there exists $h_{1},h_{2}\in\textsf{{Heaps}}_{\Bbbk}$ with
$h=h_{1}\mathbin{{\star}}h_{2}$ and there exists
$\beta\in\textsf{{Val}}\left[g\right]$,
$\gamma\in\textsf{{Val}}\left[u\right]$ with $\beta\cdot\gamma\geq\alpha$ and
$\displaystyle\qquad\beta\leq\left\llbracket{g}\right\rrbracket(s,h_{1})~{}\text{and}~{}\gamma\leq\left\llbracket{u}\right\rrbracket(s,h_{2})$
(monotonicity) iff there exists $\beta\in\textsf{{Val}}\left[g\right]$,
$\gamma\in\textsf{{Val}}\left[u\right]$ with $\beta\cdot\gamma\geq\alpha$ and
there exists $h_{1},h_{2}\in\textsf{{Heaps}}_{\Bbbk}$ with
$h=h_{1}\mathbin{{\star}}h_{2}$ and
$\displaystyle\qquad\beta\leq\left\llbracket{g}\right\rrbracket(s,h_{1})~{}\text{and}~{}\gamma\leq\left\llbracket{u}\right\rrbracket(s,h_{2})$
iff there exists $\beta\in\textsf{{Val}}\left[g\right]$,
$\gamma\in\textsf{{Val}}\left[u\right]$ with $\beta\cdot\gamma\geq ra$ and
there exists $h_{1},h_{2}\in\textsf{{Heaps}}_{\Bbbk}$ with
$h=h_{1}\mathbin{{\star}}h_{2}$ and
$\displaystyle\qquad(s,h_{1})\models\lceil\beta\preceq
g\rceil~{}\text{and}~{}(s,h_{2})\models\lceil\gamma\preceq u\rceil$ (IH) iff
there exists $\beta\in\textsf{{Val}}\left[g\right]$,
$\gamma\in\textsf{{Val}}\left[u\right]$ with $\beta\cdot\gamma\geq\alpha$ and
$\displaystyle\qquad(s,h)\models\lceil\beta\preceq
g\rceil\mathbin{{\star}}\lceil\gamma\preceq u\rceil$ iff
$\displaystyle(s,h)\models\bigvee_{\beta\in\textsf{{Val}}\left[g\right],\gamma\in\textsf{{Val}}\left[u\right],\beta\cdot\gamma\geq\alpha}\lceil\beta\preceq
g\rceil\mathbin{{\star}}\lceil\gamma\preceq u\rceil$
($\textsf{{Val}}\left[g\right]$ and $\textsf{{Val}}\left[u\right]$ are finite)

_The case
$f=\left[{\psi}\right]\mathbin{\text{\raisebox{-0.3014pt}{$\boldsymbol{{-}{-}}$}}\text{\raisebox{0.39182pt}{\rotatebox{-17.0}{$\star$}}}}g$._

$\displaystyle\alpha\leq\left\llbracket{\left[{\psi}\right]\mathbin{\text{\raisebox{-0.3014pt}{$\boldsymbol{{-}{-}}$}}\text{\raisebox{0.39182pt}{\rotatebox{-17.0}{$\star$}}}}g}\right\rrbracket(s,h)$
iff
$\displaystyle\alpha\leq\inf\left\\{\left\llbracket{g}\right\rrbracket(s,h\mathbin{{\star}}h^{\prime})~{}\mid~{}h^{\prime}\mathrel{\bot}h~{}\text{and}~{}\left[{\psi}\right](s,h^{\prime})=1\right\\}$
iff $\displaystyle\text{for all $h^{\prime}\in\textsf{{Heaps}}_{\Bbbk}$ with
$h^{\prime}\mathrel{\bot}h$ and $(s,h^{\prime})\models\psi$ we
have}~{}\alpha\leq\left\llbracket{g}\right\rrbracket(s,h\mathbin{{\star}}h^{\prime})$
($\dagger$ see below) iff $\displaystyle\text{for all
$h^{\prime}\in\textsf{{Heaps}}_{\Bbbk}$ with $h^{\prime}\mathrel{\bot}h$ and
$(s,h^{\prime})\models\psi$ we
have}~{}(s,h\mathbin{{\star}}h^{\prime})\models\lceil\alpha\preceq g\rceil$
(IH) iff
$\displaystyle(s,h)\models\psi\mathbin{\text{\raisebox{-0.3014pt}{$\boldsymbol{{-}{-}}$}}\text{\raisebox{0.39182pt}{\rotatebox{-17.0}{$\star$}}}}\lceil\alpha\preceq
g\rceil$

Regarding $\dagger$ we have the following cases: Either there is no
$h^{\prime}$ with $h^{\prime}\mathrel{\bot}h$ and $(s,h^{\prime})\models\psi$,
then both statements hold for all $\alpha\in\mathbb{P}$. If there is at least
one $h^{\prime}$ with $h^{\prime}\mathrel{\bot}h$ and
$(s,h^{\prime})\models\psi$, then since $\textsf{{Eval}}\left(g\right)$ is
finite, there is a $h^{\prime}$ with $h\mathrel{\bot}h^{\prime}$ and
$(s,h^{\prime})\models\psi$ that minimizes
$\left\llbracket{g}\right\rrbracket(s,h\mathbin{{\star}}h^{\prime})$ and we
let
$\beta=\left\llbracket{g}\right\rrbracket(s,h\mathbin{{\star}}h^{\prime})$.
Thus $\alpha\leq\beta$ if and only if for all $h^{\prime}$ with
$h^{\prime}\mathrel{\bot}h$ and $(s,h^{\prime})\models\psi$ we have
$\alpha\leq\left\llbracket{g}\right\rrbracket(s,h\mathbin{{\star}}h^{\prime})$.

This concludes the proof.

##  Appendix 0.D Appendix to Section 5

Table 9: Inductive definitions of the size of
$\textsf{{SL}}\left[\mathfrak{A}\right]$ and
$\textsf{{QSL}}\left[\mathfrak{A}\right]$ formulae.

$\varphi$ | $|\varphi|$
---|---
$\psi\in\mathfrak{A}$ | $|\varphi|$
$\neg\psi$ | $1+|\psi|$
$\psi\wedge\vartheta$ | $1+|\psi|+|\vartheta|$
$\psi\vee\vartheta$ | $1+|\psi|+|\vartheta|$
$\exists x\colon\psi$ | $1+|\psi|$
$\forall x\colon\psi$ | $1+|\psi|$
$\psi\mathbin{{\star}}\vartheta$ | $1+|\psi|+|\vartheta|$
$\psi\mathbin{\text{\raisebox{-0.3014pt}{$\boldsymbol{{-}{-}}$}}\text{\raisebox{0.39182pt}{\rotatebox{-17.0}{$\star$}}}}\vartheta$ | $1+|\psi|+|\vartheta|$

$f$ $|f|$ $|f|_{p}$ $\left[{\psi}\right]$ $|\psi|$ $0$
$\left[{\pi}\right]\cdot g+\left[{\neg\pi}\right]\cdot u$
$1+|\pi|+|g|+|\neg\pi|+|u|$ $|g|_{p}+|u|_{p}$ $q\cdot g+(1-q)\cdot u$
$1+|g|+|u|$ $1+|g|_{p}+|u|_{p}$ $g\cdot u$ $1+|g|+|u|$ $1+|g|_{p}+|u|_{p}$
$1-g$ $1+|g|$ $|g|_{p}$ $g\max u$ $1+|g|+|u|$ $|g|_{p}+|u|_{p}$ $g\min u$
$1+|g|+|u|$ $|g|_{p}+|u|_{p}$ $\reflectbox{{{S}}}\hskip 0.60275ptx\colon g$
$1+|g|$ $|g|_{p}$
$\raisebox{0.6pt}{\rotatebox{-30.0}{{{\reflectbox{J}}}}}x\colon g$ $1+|g|$
$|g|_{p}$ $g\mathbin{{\star}}u$ $1+|g|+|u|$ $1+|g|_{p}+|u|_{p}$
$\left[{\psi}\right]\mathbin{\text{\raisebox{-0.3014pt}{$\boldsymbol{{-}{-}}$}}\text{\raisebox{0.39182pt}{\rotatebox{-17.0}{$\star$}}}}g$
$1+|g|+|\psi|$ $|g|_{p}$

###### Theorem 5.1

We have $|\textsf{{Val}}\left[f\right]|\leq 2^{|f|_{p}+1}$. Hence, checking
$f\models g$ by means of Theorem 4.3 requires checking
$2^{\mathcal{O}(|f|_{p})}$ entailments in
$\textsf{{SL}}\left[\mathfrak{A}\right]$.

###### Proof

We prove this by induction of $f$.

_For the base case for $f=\left[{\psi}\right]$_ we have
$|\textsf{{Val}}\left[\left[{\psi}\right]\right]|=2^{0+1}=2^{|\left[{\psi}\right]|_{p}+1}$.

For the composite cases we assume that for some fixed, but arbitrary formulae
$g,u\in\textsf{{QSL}}\left[\mathfrak{A}\right]$, the inequalities
$|\textsf{{Val}}\left[g\right]|\leq 2^{|g|_{p}+1}$ and
$|\textsf{{Val}}\left[u\right]|\leq 2^{|u|_{p}+1}$ hold.

_For the induction steps $f=\left[{\pi}\right]\cdot
g+\left[{\neg\pi}\right]\cdot u$,_ we distinguish three cases.

  1. 1.

$|g|_{p}=0$. Then by the induction hypothesis, we have
$|\textsf{{Val}}\left[g\right]|\leq 2$. By Lemma 4, we have
$\\{0,1\\}=\textsf{{Val}}\left[g\right]$ and
$0,1\in\textsf{{Val}}\left[u\right]$. However, then the union will not
increase the set, i.e.
$\textsf{{Val}}\left[f\right]=\textsf{{Val}}\left[u\right]$. Finally we have
$|\textsf{{Val}}\left[f\right]|=|\textsf{{Val}}\left[u\right]|\leq
2^{|u|_{p}+1}=2^{|f|_{p}+1}$ by the induction hypothesis.

  2. 2.

$|u|_{p}=0$ is analogous.

  3. 3.

$0<|g|_{p},|u|_{p}$. Then the size of the set is at most the sum of each set
$|\textsf{{Val}}\left[f\right]|\leq|\textsf{{Val}}\left[g\right]|+|\textsf{{Val}}\left[u\right]|$.
By the induction hypothesis we then have

$|\textsf{{Val}}\left[f\right]|\leq\underbrace{2^{|g|_{p}+1}+2^{|u|_{p}+1}\leq
2\cdot 2^{|g|_{p}}\cdot
2^{|u|_{p}}}_{\text{because}~{}0<|g|_{p},|u|_{p}}=2^{|g|_{p}+|u|_{p}+1}=2^{|f|_{p}+1}~{}.$

_For the induction steps $f=q\cdot g+(1-q)\cdot u$,_ we have that
$|\textsf{{Val}}\left[f\right]|~{}{}\leq{}~{}|\textsf{{Val}}\left[g\right]|\cdot|\textsf{{Val}}\left[u\right]|$.
By the induction hypothesis we deduce the upper bound

$\textsf{{Val}}\left[f\right]\leq 2^{|g|_{p}+1}\cdot
2^{|u|_{p}+1}=2^{|g|_{p}+|u|_{p}+1+1}=2^{|f|_{p}+1}~{}.$

_The induction step $f=g\cdot u$_ is analogous to the previous case.

_For the induction step $f=1-g$,_ we have that the set does not change in size
$|\textsf{{Val}}\left[f\right]|=|\textsf{{Val}}\left[g\right]|$ and
$|f|_{p}=|g|_{p}$. Thus this follows directly from the induction hypothesis.

_The induction steps $f=g\min u$ and $f=g\max u$_ are analogous to case
$f=\left[{\pi}\right]\cdot g+\left[{\neg\pi}\right]\cdot u$.

_The induction steps $f=\reflectbox{{{S}}}\hskip 0.60275ptx\colon g$ and
$f=\raisebox{0.6pt}{\rotatebox{-30.0}{{{\reflectbox{J}}}}}x\colon g$_ are
analogous to the case $f=1-g$.

_The induction step $f=g\mathbin{{\star}}u$_ is analogous to the case
$f=g\cdot u$.

_The induction step
$f=\left[{\psi}\right]\mathbin{\text{\raisebox{-0.3014pt}{$\boldsymbol{{-}{-}}$}}\text{\raisebox{0.39182pt}{\rotatebox{-17.0}{$\star$}}}}g$_
is analogous to the case $f=1-g$.

###### Theorem 5.2

For any formulae $f\in\textsf{{QSL}}\left[\mathfrak{A}\right]$ and all
probabilities $\alpha\in\mathbb{P}$, the
$\textsf{{SL}}\left[\mathfrak{A}\right]$ formula $\lceil\alpha\preceq f\rceil$
has at most size $3\cdot|f|\cdot 2^{(|f|_{p}+1)^{2}}$. Hence the size of the
formula $\lceil\alpha\preceq f\rceil$ is in $\mathcal{O}(|f|)\cdot
2^{\mathcal{O}(|f|_{p}^{2})}$.

###### Proof

We show by induction on $f$ that $|\lceil\alpha\preceq f\rceil|\leq
3\cdot|f|\cdot 2^{(|f|_{p}+1)^{2}}$ for all $\alpha\in\mathbb{P}$.

_For the base case $f=\left[{\psi}\right]$_ we have $|\lceil\alpha\preceq
f\rceil|\leq|\psi|=|\psi|\cdot 2^{1}\leq 3\cdot|f|\cdot 2^{(|f|_{p}+1)^{2}}$.

For the composite cases we assume that for some arbitrary, but fixed formulae
$g,u\in\textsf{{QSL}}\left[\mathfrak{A}\right]$ and all probabilities
$\alpha\in\mathbb{P}$ the inequalities for both formulae $|\lceil\alpha\preceq
g\rceil|\leq 3\cdot|g|\cdot 2^{(|g|_{p}+1)^{2}}$ and $|\lceil\alpha\preceq
u\rceil|\leq 3\cdot|u|\cdot 2^{(|u|_{p}+1)^{2}}$ hold.

_For the induction step $f=\left[{\pi}\right]\cdot
g+\left[{\neg\pi}\right]\cdot u$_ we have that

$\displaystyle|\lceil\alpha\preceq f\rceil|$ $\displaystyle=\quad$
$\displaystyle|(\left[{\pi}\right]\land\lceil\alpha\preceq
u\rceil)\lor(\left[{\neg\pi}\right]\land\lceil\alpha\preceq u\rceil)|$
$\displaystyle=\quad$ $\displaystyle|\left[{\pi}\right]+1+|\lceil\alpha\preceq
u\rceil|+1+|\left[{\neg\pi}\right]|+1+|\lceil\alpha\preceq u\rceil||$
$\displaystyle=\quad$ $\displaystyle|\pi|+|\lceil\alpha\preceq
g\rceil|+|\neg\pi|+|\lceil\alpha\preceq u\rceil|+3$ $\displaystyle\leq\quad$
$\displaystyle|\pi|+3\cdot|g|\cdot
2^{(|g|_{p}+1)^{2}}+|\neg\pi|+3\cdot|u|\cdot 2^{(|u|_{p}+1)^{2}}+3$ (IH)
$\displaystyle\leq\quad$ $\displaystyle|\pi|+3\cdot|g|\cdot
2^{(|g|_{p}+|u|_{p}+1)^{2}}+|\neg\pi|+3\cdot|u|\cdot
2^{(|g|_{p}+|u|_{p}+1)^{2}}+3$ $\displaystyle\leq\quad$ $\displaystyle
3\cdot(|\pi|+|g|+|\neg\pi|+|u|+1)\cdot 2^{(|g|_{p}+|u|_{p}+1)^{2}}$
$\displaystyle=\quad$ $\displaystyle 3\cdot(|\pi|+|g|+|\neg\pi|+|u|+1)\cdot
2^{(|f|_{p}+1)^{2}}$ ($|f|_{p}=|g|_{p}+|u|_{p}$) $\displaystyle=\quad$
$\displaystyle 3\cdot|f|\cdot 2^{(|f|_{p}+1)^{2}}$
($|f|=|\pi|+|g|+|\neg\pi|+|u|+1$)

_For the induction step $f=p\cdot g+(1-p)\cdot u$,_ we have for
$\beta,\gamma\in\mathbb{P}$ maximizing $|\lceil\beta\preceq g\rceil|$ and
$|\lceil\gamma\preceq u\rceil|$ that

$|\lceil\alpha\preceq
f\rceil|~{}{}\leq{}~{}\left(|\textsf{{Val}}\left[g\right]|\cdot|\textsf{{Val}}\left[u\right]|\right)\cdot\left(|\lceil\beta\preceq
g\rceil|+|\lceil\gamma\preceq u\rceil|+2\right)~{},$

thus using the induction hypothesis and Theorem 5.1

$|\lceil\alpha\preceq f\rceil|~{}{}\leq{}~{}\left(2^{|g|_{p}+1}\cdot
2^{|u|_{p}+1}\right)\cdot\left(3\cdot|g|\cdot
2^{(|g|_{p}+1)^{2}}+3\cdot|u|\cdot 2^{(|u|_{p}+1)^{2}}+2\right)~{}.$

Remark that $1\leq|f|_{p}$ by assumption. We now prove the upper bound on the
right side by distinguishing two cases on $|f|_{p}$:

  1. 1.

$|f|_{p}=1$. Then $|g|_{p}=|u|_{p}=0$ and we have:

$\displaystyle|\lceil\alpha\preceq f\rceil|$ $\displaystyle\leq\quad$
$\displaystyle 2\cdot 2\cdot(3\cdot|g|\cdot 2+3\cdot|u|\cdot 2+2)$
(($\dagger$) and $|f|_{p}=1$) $\displaystyle=\quad$ $\displaystyle 2^{3}\cdot
3\cdot(|g|+|u|+\nicefrac{{1}}{{5}})$ $\displaystyle\leq\quad$ $\displaystyle
2^{3}\cdot 3\cdot|f|$ ($|f|=|g|+|u|+1$) $\displaystyle\leq\quad$
$\displaystyle 3\cdot|f|\cdot 2^{(|f|_{p}+1)^{2}}$ ($|f|_{p}=1$)

  2. 2.

$|f|_{p}>1$. Here we require a bit more mathematical tools in form of Lemma 5.
Then we have:

$\displaystyle|\lceil\alpha\preceq f\rceil|$ $\displaystyle\leq\quad$
$\displaystyle\left(2^{|g|_{p}+1}\cdot
2^{|u|_{p}+1}\right)\cdot\left(3\cdot|g|\cdot
2^{(|g|_{p}+1)^{2}}+3\cdot|u|\cdot 2^{(|u|_{p}+1)^{2}}+2\right)$ ($\dagger$)
$\displaystyle=\quad$ $\displaystyle 2^{|f|_{p}+1}\cdot\left(3\cdot|g|\cdot
2^{(|g|_{p}+1)^{2}}+3\cdot|u|\cdot 2^{(|u|_{p}+1)^{2}}+2\right)\hskip
35.00008pt$ ($|f|_{p}=|g|_{p}+|u|_{p}+1$) $\displaystyle=\quad$ $\displaystyle
3\cdot|g|\cdot 2^{|f|_{p}+1}\cdot 2^{(|g|_{p}+1)^{2}}+3\cdot|u|\cdot
2^{|f|_{p}+1}\cdot 2^{(|u|_{p}+1)^{2}}+2^{|f|_{p}+1}\cdot 2$
$\displaystyle\leq\quad$ $\displaystyle\quad 3\cdot(|g|+|u|)\cdot
2^{|f|_{p}+1}\cdot 2^{(|g|_{p}+|u|_{p}+1)^{2}}$
$\displaystyle+3\cdot(|g|+|u|)\cdot 2^{|f|_{p}+1}\cdot
2^{(|g|_{p}+|u|_{p}+1)^{2}}$ $\displaystyle+2\cdot 2^{|f|_{p}+1}$
$\displaystyle\leq\quad$ $\displaystyle 2\cdot 3\cdot(|g|+|u|)\cdot
2^{|f|_{p}+1}\cdot 2^{(|g|_{p}+|u|_{p}+1)^{2}}+2^{|f|_{p}+2}$
$\displaystyle\leq\quad$ $\displaystyle 2\cdot 3\cdot|f|\cdot
2^{|f|_{p}+1}\cdot 2^{(|g|_{p}+|u|_{p}+1)^{2}}+2^{|f|_{p}+2}$
($|f|=|g|+|u|+1$) $\displaystyle=\quad$ $\displaystyle 2\cdot 3\cdot|f|\cdot
2^{|f|_{p}+1}\cdot 2^{|f|_{p}^{2}}+2^{|f|_{p}+2}$
($|f|_{p}=|g|_{p}+|u|_{p}+1$) $\displaystyle=\quad$ $\displaystyle
3\cdot|f|\cdot 2^{|f|_{p}^{2}+|f|_{p}+2}+2^{|f|_{p}+2}$
$\displaystyle\leq\quad$ $\displaystyle
3\cdot|f|\cdot\left(2^{|f|_{p}^{2}+|f|_{p}+2}+2^{|f|_{p}+2}\right)$
$\displaystyle\leq\quad$ $\displaystyle 3\cdot|f|\cdot 2^{(|f|_{p}+1)^{2}}$
(by $1<|f|_{p}$ and Lemma 5)

_The induction steps for $f=g\cdot u$_ is analogous to the previous case.

_For the induction step $f=1-g$_ we have that

$\displaystyle|\lceil\alpha\preceq f\rceil|$ $\displaystyle\leq\quad$
$\displaystyle|\lceil\alpha\preceq g\rceil|+1$ $\displaystyle\leq\quad$
$\displaystyle 3\cdot|g|\cdot 2^{(|g|_{p}+1)^{2}}+1$ (IH)
$\displaystyle\leq\quad$ $\displaystyle 3\cdot|g|\cdot
2^{(|f|_{p}+1)^{2}}+2^{(|f|_{p}+1)^{2}}$ ($0\leq|g|_{p}=|f|_{p}$)
$\displaystyle=\quad$ $\displaystyle 3\cdot(|g|+\nicefrac{{1}}{{3}})\cdot
2^{(|f|_{p}+1)^{2}}$ $\displaystyle\leq\quad$ $\displaystyle 3\cdot|f|\cdot
2^{(|f|_{p}+1)^{2}}$ ($|f|=|g|+1$)

_The induction steps for $g\max u$, $g\min u$, $\reflectbox{{{S}}}\hskip
0.60275ptx\colon g$ and
$\raisebox{0.6pt}{\rotatebox{-30.0}{{{\reflectbox{J}}}}}x\colon g$_ are
analogous to the previous case.

_The induction steps for $g\mathbin{{\star}}u$_ is analogous to the case
$f=p\cdot g+(1-p)\cdot u$.

_For the induction step
$\left[{\psi}\right]\mathbin{\text{\raisebox{-0.3014pt}{$\boldsymbol{{-}{-}}$}}\text{\raisebox{0.39182pt}{\rotatebox{-17.0}{$\star$}}}}g$_
we have that

$\displaystyle|\lceil\alpha\preceq f\rceil|$ $\displaystyle=\quad$
$\displaystyle|\lceil\alpha\preceq g\rceil|+|\psi|+1$ $\displaystyle\leq\quad$
$\displaystyle 3\cdot|g|\cdot 2^{(|g|_{p}+1)^{2}}+|\psi|+1$ (IH)
$\displaystyle\leq\quad$ $\displaystyle 3\cdot|g|\cdot
2^{(|f|_{p}+1)^{2}}+(|\psi|+1)\cdot 2^{(|f|_{p}+1)^{2}}$
($0\leq|g|_{p}=|f|_{p}$) $\displaystyle=\quad$ $\displaystyle
3\cdot(|g|+\nicefrac{{|\psi|}}{{3}}+\nicefrac{{1}}{{3}})\cdot
2^{(|f|_{p}+1)^{2}}$ $\displaystyle\leq\quad$ $\displaystyle 3\cdot|f|\cdot
2^{(|f|_{p}+1)^{2}}$ ($|f|=|g|+|\psi|+1$)

This concludes the proof.

###### Lemma 5

For all natural numbers $n>1$, we have $2^{n^{2}+n+2}+2^{n+2}\leq
2^{(n+1)^{2}}$.

###### Proof

By induction over $n$.

_For the base case $n=2$,_ we have
$2^{2^{2}+2+2}+2^{2+2}=2^{8}+2^{4}<2^{8}+2^{8}=2^{(2+1)^{2}}$.

Now we assume that for some fixed, but arbitrary natural number $n>1$ the
inequality $2^{n^{2}+n+2}+2^{n+2}\leq 2^{(n+1)^{2}}$ holds.

_For the induction step $n\rightarrow n+1$,_ we have

$\displaystyle 2^{(n+1)^{2}+n+1+2}+2^{n+1+2}$ $\displaystyle=\quad$
$\displaystyle 2^{n^{2}+2n+1+n+1+2}+2^{n+1+2}$ $\displaystyle=\quad$
$\displaystyle 2^{n^{2}+n+2}\cdot 2^{2n+2}+2^{n+2}\cdot 2$
$\displaystyle\leq\quad$ $\displaystyle
2^{2n+2}\cdot\left(2^{n^{2}+n+2}+2^{n+2}\right)$ $\displaystyle\leq\quad$
$\displaystyle 2^{2n+2}\cdot 2^{(n+1)^{2}}$ (IH) $\displaystyle=\quad$
$\displaystyle 2^{n^{2}+4n+3}$ $\displaystyle\leq\quad$ $\displaystyle
2^{n^{2}+4n+4}$ $\displaystyle=\quad$ $\displaystyle 2^{(n+1+1)^{2}}~{}.$

This concludes the proof.

##  Appendix 0.E Appendix to Section 6

###### Lemma 1

Let Q be a $\textsf{{QSL}}\left[\mathfrak{A}\right]$ fragment. If an
$\textsf{{SL}}\left[\mathfrak{A}\right]$ fragment S satisfies the requirements
provided in Table 7, then S is Q-admissible.

###### Proof

By induction on $f$.

_For the base case $f=\left[{\psi}\right]$,_ we have
$\lceil\alpha\preceq\left[{\psi}\right]\rceil=\mathsf{true}~{}\text{if}~{}\alpha=0~{}\text{otherwise}~{}\left[{\psi}\right]$,
thus $\mathsf{true}$ and $\psi$ are required.

For all other composite cases we assume for some fixed, but arbitrary
$g,u\in\textsf{{QSL}}\left[\mathfrak{A}\right]$ that for all
$\beta,\gamma\in\mathbb{P}$ the formulae $\lceil\beta\preceq g\rceil$ and
$\lceil\gamma\preceq u\rceil$ satisfy the requirements.

_For the case $f=\left[{\pi}\right]\cdot g+\left[{\neg\pi}\right]\cdot u$,_ we
have $\lceil\alpha\preceq f\rceil=(\pi\land\lceil\alpha\preceq
g\rceil)\lor(\neg\pi\land\lceil\alpha\preceq u\rceil)$, since by the induction
hypothesis $\lceil\alpha\preceq g\rceil$ and $\lceil\alpha\preceq u\rceil$
already satisfy all requirements, we only require additionally
$\pi,\neg\pi,\land$ and $\lor$.

_For the case $f=p\cdot g+(1-p)\cdot u$,_ we have

$\lceil\alpha\preceq
f\rceil=\bigvee_{\beta\in\textsf{{Val}}\left[g\right],\gamma\in\textsf{{Val}}\left[u\right],p\cdot\beta+(1-p)\cdot\gamma\geq\alpha}\quad\lceil\beta\preceq
g\rceil\wedge\lceil\gamma\preceq u\rceil~{}.$

Here we have two observations:

  1. 1.

There are only finitely many disjunctions since $\textsf{{Val}}\left[g\right]$
and $\textsf{{Val}}\left[u\right]$ is finite by Theorem 4.1.

  2. 2.

The disjunctions is not empty since $1\in\textsf{{Val}}\left[g\right]$ and
$1\in\textsf{{Val}}\left[u\right]$ by Lemma 4 and $p\cdot 1+(1-p)\cdot
1=1\geq\alpha$ for all $\alpha\in\mathbb{P}$.

Thus, for any $\alpha\in\mathbb{P}$, we can construct the big disjunction by
only using $\land$, $\lor$, $\lceil\beta\preceq g\rceil$ and
$\lceil\gamma\preceq u\rceil$ for all $\beta,\gamma\in\mathbb{P}$. Since
$\lceil\beta\preceq g\rceil$ and $\lceil\gamma\preceq u\rceil$ satisfy all
requirements by the induction hypothesis, we only require additionally $\land$
and $\lor$.

_The case $f=g\cdot u$_ is analogous to the previous case.

_For the case $f=1-g$,_ we have $\lceil\alpha\preceq
f\rceil=\mathsf{true}~{}\text{if}~{}\alpha=0~{}\text{otherwise}~{}\neg\lceil\delta\preceq
g\rceil$ where
$\delta=\min\left\\{\,{\beta\in\textsf{{Val}}\left[g\right]}~{}\middle|~{}{\beta>1-\alpha}\,\right\\}$.
Remark that we compute $\delta$ during the construction of
$\lceil\alpha\preceq f\rceil$ and not during the checking of
$(s,h)\models\lceil\alpha\preceq f\rceil$. Since $\lceil\delta\preceq g\rceil$
already satisfy all requirements by the induction hypothesis, we thus only
additionally require $\neg$ and $\mathsf{true}$.

_The cases $f=g\max u$, $f=g\min u$, $f=\reflectbox{{{S}}}\hskip
0.60275ptx\colon g$ and
$f=\raisebox{0.6pt}{\rotatebox{-30.0}{{{\reflectbox{J}}}}}x\colon g$_ are
analogous to the case $f=\left[{\pi}\right]\cdot g+\left[{\neg\pi}\right]\cdot
u$.

_The case $f=g\mathbin{{\star}}u$_ is analogous to the case $f=p\cdot
g+(1-p)\cdot u$.

_The case
$f=\left[{\psi}\right]\mathbin{\text{\raisebox{-0.3014pt}{$\boldsymbol{{-}{-}}$}}\text{\raisebox{0.39182pt}{\rotatebox{-17.0}{$\star$}}}}g$_
is analogous to the case $f=\left[{\pi}\right]\cdot
g+\left[{\neg\pi}\right]\cdot u$.

This concludes the proof.

##  Appendix 0.F Appendix to Section 6.1

###### Theorem 6.2

For loop- and allocation-free hpGCL programs $C$ (that only perform pointer
operations, no arithmetic and guards of the pure fragment of $\mathfrak{A}$)
and $f_{1},f_{2}\in\textsf{{QSH}}$, it is decidable whether the entailment
$\textsf{{wlp}}\llbracket C\rrbracket\left(f_{1}\right)\models f_{2}$ holds.

####  0.F.0.1 Proof of Theorem 6.2

The proof requires extended quantitative symbolic heaps:

###### Definition 5

The set eQSH of _extended quantitative symbolic heaps_ is given by the grammar

$\displaystyle g\quad\rightarrow\quad$
$\displaystyle\left[{\Phi}\right]~{}\mid~{}\left[{B}\right]\cdot g+\left[{\neg
B}\right]\cdot g~{}\mid~{}q\cdot g+(1-q)\cdot g~{}\mid~{}g\mathbin{{\star}}g$
$\displaystyle~{}\mid~{}\reflectbox{{{S}}}\hskip 0.60275ptx\colon
g~{}\mid~{}\left[{x\mapsto(y_{1},\ldots,y_{k})}\right]\mathbin{\text{\raisebox{-0.3014pt}{$\boldsymbol{{-}{-}}$}}\text{\raisebox{0.39182pt}{\rotatebox{-17.0}{$\star$}}}}g~{}.$
$\triangle$

Notice that indeed $\textsf{{QSH}}\subseteq\textsf{{eQSH}}$.

###### Lemma 2

For every loop- and allocation-free program $C\in\textnormal{{{hpGCL}}}$
without arithmetic and only with guards of the pure fragment of
$\mathfrak{A}$, extended quantitative symbolic heaps are closed under
$\textsf{{wlp}}\llbracket C\rrbracket$, i.e.,

$\text{for all $g\in\textsf{{eQSH}}$}\colon\quad\textsf{{wlp}}\llbracket
C\rrbracket\left(g\right)\in\textsf{{eQSH}}~{}.$

In particular, since $\textsf{{QSH}}\subseteq\textsf{{eQSH}}$, we have

$\text{for all $f\in\textsf{{QSH}}$}\colon\quad\textsf{{wlp}}\llbracket
C\rrbracket\left(f\right)\in\textsf{{eQSH}}~{}.$

###### Proof

Since we not allow arithmetic in expressions, we only have expressions of the
form $E=y$. Moreover, eQSH is trivially closed under the substitution
$g\left[{x}\texttt{:=}{y}\right]$ for any $x,y\in\mathsf{Vars}$. Now we prove
the lemma by induction on the structure of loop- and allocation-free program
$C$ with $\Bbbk=1$, however the proof is easy to adapt for any $\Bbbk$.

_For the base case $C=\texttt{{skip}}$_ we have
$\textsf{{wlp}}\llbracket\texttt{{skip}}\rrbracket\left(g\right)=g\in\textsf{{eQSH}}$.

_For the base case $C=x\mathrel{\textnormal{{:=}}}y$_ we have

$\textsf{{wlp}}\llbracket
x\mathrel{\textnormal{{:=}}}y\rrbracket\left(g\right)~{}{}={}~{}g\left[{x}\texttt{:=}{y}\right]~{}{}\in{}~{}\textsf{{eQSH}}~{}.$

_For the base case $C=\mathtt{free}(y)$_ we have

$\textsf{{wlp}}\llbracket\mathtt{free}(y)\rrbracket\left(g\right)~{}{}={}~{}\reflectbox{{{S}}}\hskip
0.60275ptz\colon\left[{y\mapsto
z}\right]\mathbin{{\star}}g~{}{}\in{}~{}\textsf{{eQSH}}$

where $z$ is fresh.

_For the base case $C=x\mathrel{\textnormal{{:=}}}\texttt{<}\,y\,\texttt{>}$_
we have

$\textsf{{wlp}}\llbracket
x\mathrel{\textnormal{{:=}}}\texttt{<}\,y\,\texttt{>}\rrbracket\left(g\right)~{}{}={}~{}\reflectbox{{{S}}}\hskip
0.60275ptz\colon\left[{x\mapsto z}\right]\mathbin{{\star}}(\left[{x\mapsto
y}\right]\mathbin{\text{\raisebox{-0.3014pt}{$\boldsymbol{{-}{-}}$}}\text{\raisebox{0.39182pt}{\rotatebox{-17.0}{$\star$}}}}f\left[{x}\texttt{:=}{y}\right])~{}{}\in{}~{}\textsf{{eQSH}}$

where $z$ is fresh.

_For the base case $C=\texttt{<}\,x\,\texttt{>}\mathrel{\textnormal{{:=}}}y$_
we have

$\textsf{{wlp}}\llbracket\texttt{<}\,x\,\texttt{>}\mathrel{\textnormal{{:=}}}y\rrbracket\left(g\right)~{}{}={}~{}\reflectbox{{{S}}}\hskip
0.60275ptz\colon\left[{x\mapsto z}\right]\mathbin{{\star}}(\left[{x\mapsto
y}\right]\mathbin{\text{\raisebox{-0.3014pt}{$\boldsymbol{{-}{-}}$}}\text{\raisebox{0.39182pt}{\rotatebox{-17.0}{$\star$}}}}f)~{}{}\in{}~{}\textsf{{eQSH}}$

where $z$ is fresh.

For all other composite cases we assume for some fixed, but arbitrary loop-
and allocation-free programs $C_{1},C_{2}\in\textnormal{{{hpGCL}}}$ without
arithmetic and only with guards of the pure fragment of $\mathfrak{A}$ such
that for all $g\in\textsf{{eQSH}}\colon\quad\textsf{{wlp}}\llbracket
C_{1}\rrbracket\left(g\right)\in\textsf{{eQSH}}$ and for all
$u\in\textsf{{eQSH}}\colon\textsf{{wlp}}\llbracket
C_{2}\rrbracket\left(u\right)\in\textsf{{eQSH}}$.

_For the case
$C=\left\\{\,{C_{1}}\,\right\\}\mathrel{\left[\,p\,\right]}\left\\{\,{C_{2}}\,\right\\}$_
we have

$\textsf{{wlp}}\llbracket\left\\{\,{C_{1}}\,\right\\}\mathrel{\left[\,p\,\right]}\left\\{\,{C_{2}}\,\right\\}\rrbracket\left(g\right)~{}{}={}~{}p\cdot\textsf{{wlp}}\llbracket
C_{1}\rrbracket\left(g\right)+(1-p)\cdot\textsf{{wlp}}\llbracket
C_{2}\rrbracket\left(g\right)~{}{}\in{}~{}\textsf{{eQSH}}$

by the induction hypothesis.

_For the case $C={C_{1}}{\,;}~{}{C_{2}}$_ we have

$\textsf{{wlp}}\llbracket{C_{1}}{\,;}~{}{C_{2}}\rrbracket\left(g\right)~{}{}={}~{}\textsf{{wlp}}\llbracket
C_{1}\rrbracket\left(\textsf{{wlp}}\llbracket
C_{2}\rrbracket\left(g\right)\right)~{}{}\in{}~{}\textsf{{eQSH}}$

by the induction hypothesis.

_For the case
$C=\textnormal{{if}}\,\left(\,{B}\,\right)\,\left\\{\,{C_{1}}\,\right\\}\,\textnormal{{else}}\,\left\\{\,{C_{2}}\,\right\\}$_
we have either $B=(x=y)$, then

$\displaystyle\textsf{{wlp}}\llbracket\textnormal{{if}}\,\left(\,{x=y}\,\right)\,\left\\{\,{C_{1}}\,\right\\}\,\textnormal{{else}}\,\left\\{\,{C_{2}}\,\right\\}\rrbracket\left(g\right)\qquad\qquad\qquad\qquad\qquad$
$\displaystyle\qquad\qquad\qquad~{}{}={}~{}\left[{x=y}\right]\cdot\textsf{{wlp}}\llbracket
C_{1}\rrbracket\left(g\right)+\left[{x\neq
y}\right]\cdot\textsf{{wlp}}\llbracket
C_{2}\rrbracket\left(g\right)~{}{}\in{}~{}\textsf{{eQSH}}$

by the induction hypothesis; or $B=(x\neq y)$ which is analogous.

This concludes the proof.

Hence, if $g\models f$ is decidable for $g\in\textsf{{eQSH}}$ and
$f\in\textsf{{QSH}}$, Theorem 6.2 follows.

###### Lemma 3

For $g\in\textsf{{eQSH}}$ and $f\in\textsf{{QSH}}$, it is decidable whether
$g\models f$ holds.

###### Proof

We employ Lemma 1 to determine two $\textsf{{SL}}\left[\mathfrak{A}\right]$
fragments $\textsf{{S}}_{1},\textsf{{S}}_{2}$ such that $\textsf{{S}}_{1}$ is
eQSH-admissible and $\textsf{{S}}_{2}$ is QSH-admissible. Then, by Theorem
6.1, decidability of $g\models f$ follows from decidability of
$\varphi\models\psi$ for $\varphi\in\textsf{{S}}_{1}$ and
$\psi\in\textsf{{S}}_{2}$. For that, we exploit the equivalence

$\varphi\models\psi\qquad\text{iff}\qquad\varphi\wedge\neg\psi~{}\text{is
unsatisfiable}~{}.$

The latter is decidable by [19, Theorem 3.3] since $\varphi\wedge\neg\psi$ is
equivalent to a formula of the form $\exists^{*}\forall^{*}\colon\vartheta$
with $\vartheta$ quantifier-free and such that no formula
$\vartheta_{1}\mathbin{\text{\raisebox{-0.3014pt}{$\boldsymbol{{-}{-}}$}}\text{\raisebox{0.39182pt}{\rotatebox{-17.0}{$\star$}}}}\vartheta_{2}$
occurring in $\vartheta$ contains a universally quantified variable. The eQSH-
admissible $\textsf{{SL}}\left[\mathfrak{A}\right]$ fragment
$\textsf{{S}}_{1}$ is given by

$\displaystyle\varphi\quad\rightarrow\quad$ $\displaystyle\Phi$
$\displaystyle\mid~{}\varphi\wedge\varphi$
$\displaystyle\mid~{}\varphi\vee\varphi$ $\displaystyle\mid~{}\exists
x\colon\varphi$ $\displaystyle\mid~{}\varphi\mathbin{{\star}}\varphi$
$\displaystyle\mid~{}x\mapsto(y_{1},\ldots,y_{k})\mathbin{\text{\raisebox{-0.3014pt}{$\boldsymbol{{-}{-}}$}}\text{\raisebox{0.39182pt}{\rotatebox{-17.0}{$\star$}}}}\varphi~{}.$

The QSH-admissible $\textsf{{SL}}\left[\mathfrak{A}\right]$ fragment
$\textsf{{S}}_{2}$ is given by

$\displaystyle\psi\quad\rightarrow\quad$ $\displaystyle\Phi$
$\displaystyle\mid~{}\psi\wedge\psi$ $\displaystyle\mid~{}\psi\vee\psi$
$\displaystyle\mid~{}\exists x\colon\psi$
$\displaystyle\mid~{}\psi\mathbin{{\star}}\psi~{}.$

###### Lemma 6

Every $\varphi\in\textsf{{S}}_{1}$ is equivalent to a formula $\psi=\exists
x_{1},\ldots,x_{n}\colon\vartheta$ for some $n\in\mathbb{N}$ with
$\vartheta\in\textsf{{S}}_{1}$ quantifier-free.

###### Proof

By induction on $\varphi$. For the base case $\varphi=\Phi$ we choose $n=0$
and have nothing to show. The cases $\wedge,\vee,\exists$ are standard. For
the remaining cases, we reason as follows: As the induction hypothesis assume
that for some arbitrary, but fixed,
$\varphi_{1},\varphi_{2}\in\textsf{{S}}_{1}$ there are $\psi_{1}=\exists
x_{1},\ldots,x_{n}\colon\vartheta_{1}$ and $\psi_{2}=\exists
y_{1},\ldots,y_{m}\colon\vartheta_{2}$ with
$\vartheta_{1},\vartheta_{2}\in\textsf{{S}}_{1}$ quantifier-free and
$\psi_{1}\equiv\varphi_{1}$ and $\psi_{2}\equiv\varphi_{2}$. Furthermore,
assume without loss of generality that $x_{1},\ldots,x_{n}$ do not occur in
$\vartheta_{2}$ and that $y_{1},\ldots,y_{m}$ do not occur in $\vartheta_{1}$.

_The case $\varphi=\varphi_{1}\mathbin{{\star}}\varphi_{2}$._ For every
$(s,h)\in\textsf{{States}}$, we have

$\displaystyle(s,h)~{}{}\models{}~{}\varphi_{1}\mathbin{{\star}}\varphi_{2}$
iff there are $h_{1},h_{2}$ with $h_{1}\mathbin{{\star}}h_{2}=h$ such that
$\displaystyle(s,h_{1})~{}{}\models{}~{}\varphi_{1}~{}\text{and}~{}(s,h_{2})~{}{}\models{}~{}\varphi_{2}$
iff there are $h_{1},h_{2}$ with $h_{1}\mathbin{{\star}}h_{2}=h$ such that
there are $v_{1},\ldots,v_{n},w_{1},\ldots,w_{m}$ such that
$\displaystyle(s\left[{x_{1}}\texttt{:=}{v_{1}}\right]\ldots\left[{x_{n}}\texttt{:=}{v_{n}}\right],h_{1})~{}{}\models{}~{}\vartheta_{1}~{}\text{and}~{}(s\left[{y_{1}}\texttt{:=}{w_{1}}\right]\ldots\left[{y_{m}}\texttt{:=}{w_{m}}\right],h_{2})~{}{}\models{}~{}\vartheta_{2}$
(by I.H.) iff there are $v_{1},\ldots,v_{n},w_{1},\ldots,w_{m}$ such that
there are $h_{1},h_{2}$ with $h_{1}\mathbin{{\star}}h_{2}=h$ such that
$\displaystyle(s\left[{x_{1}}\texttt{:=}{v_{1}}\right]\ldots\left[{x_{n}}\texttt{:=}{v_{n}}\right],h_{1})~{}{}\models{}~{}\vartheta_{1}~{}\text{and}~{}(s\left[{y_{1}}\texttt{:=}{w_{1}}\right]\ldots\left[{y_{m}}\texttt{:=}{w_{m}}\right],h_{2})~{}{}\models{}~{}\vartheta_{2}$
iff there are $v_{1},\ldots,v_{n},w_{1},\ldots,w_{m}$ such that
$\displaystyle(s\left[{x_{1}}\texttt{:=}{v_{1}}\right]\ldots\left[{x_{n}}\texttt{:=}{v_{n}}\right]\left[{y_{1}}\texttt{:=}{w_{1}}\right]\ldots\left[{y_{m}}\texttt{:=}{w_{m}}\right],h)~{}{}\models{}~{}\vartheta_{1}\mathbin{{\star}}\vartheta_{2}$
(variables do not overlap) iff $\displaystyle(s,h)\models\exists
v_{1},\ldots,w_{n},w_{1},\ldots,w_{m}\colon\vartheta_{1}\mathbin{{\star}}\vartheta_{2}~{}.$

_The case
$\varphi=x\mapsto(z_{1},\ldots,z_{k})\mathbin{\text{\raisebox{-0.3014pt}{$\boldsymbol{{-}{-}}$}}\text{\raisebox{0.39182pt}{\rotatebox{-17.0}{$\star$}}}}\varphi_{1}$._
We assume without loss of generality that $x\not\in\\{x_{1},\ldots,x_{n}\\}$
and $\\{x_{1},\ldots,x_{n}\\}\cap\\{z_{1}\ldots z_{k}\\}=\emptyset$. Let
$(s,h)\in\textsf{{States}}$. We distinguish the cases
$s(x)\in\textsf{{dom}}\left({h}\right)$ and
$s(x)\not\in\textsf{{dom}}\left({h}\right)$. If
$s(x)\in\textsf{{dom}}\left({h}\right)$, we have

$\displaystyle(s,h)~{}{}\models{}~{}x\mapsto(z_{1},\ldots,z_{k})\mathbin{\text{\raisebox{-0.3014pt}{$\boldsymbol{{-}{-}}$}}\text{\raisebox{0.39182pt}{\rotatebox{-17.0}{$\star$}}}}\varphi_{1}$
iff $\displaystyle\mathsf{true}$ iff
$\displaystyle(s,h)~{}{}\models{}~{}\exists x_{1},\ldots,x_{n}\colon
x\mapsto(z_{1},\ldots,z_{k})\mathbin{\text{\raisebox{-0.3014pt}{$\boldsymbol{{-}{-}}$}}\text{\raisebox{0.39182pt}{\rotatebox{-17.0}{$\star$}}}}\vartheta_{1}~{}.$
(variables do not overlap)

If $s(x)\not\in\textsf{{dom}}\left({h}\right)$, we have

$\displaystyle(s,h)~{}{}\models{}~{}x\mapsto(z_{1},\ldots,z_{k})\mathbin{\text{\raisebox{-0.3014pt}{$\boldsymbol{{-}{-}}$}}\text{\raisebox{0.39182pt}{\rotatebox{-17.0}{$\star$}}}}\varphi_{1}$
iff
$\displaystyle(s,h\mathbin{{\star}}s(x)\mapsto(s(z_{1}),\ldots,s(z_{k})))~{}{}\models{}~{}\varphi_{1}$
iff
$\displaystyle(s,h\mathbin{{\star}}s(x)\mapsto(s(z_{1}),\ldots,s(z_{k})))~{}{}\models{}~{}\exists
x_{1},\ldots,x_{n}\colon\vartheta_{1}$ (by I.H.) iff there are
$v_{1},\ldots,v_{n}$ such that
$\displaystyle(s\left[{x_{1}}\texttt{:=}{v_{1}}\right]\ldots\left[{x_{n}}\texttt{:=}{v_{n}}\right],h\mathbin{{\star}}s(x)\mapsto(s(z_{1}),\ldots,s(z_{k})))~{}{}\models{}~{}\vartheta_{1}$
(variables do not overlap) iff there are $v_{1},\ldots,v_{n}$ such that
$\displaystyle(s\left[{x_{1}}\texttt{:=}{v_{1}}\right]\ldots\left[{x_{n}}\texttt{:=}{v_{n}}\right],h)~{}{}\models{}~{}x\mapsto(z_{1},\ldots,z_{k})\mathbin{\text{\raisebox{-0.3014pt}{$\boldsymbol{{-}{-}}$}}\text{\raisebox{0.39182pt}{\rotatebox{-17.0}{$\star$}}}}\vartheta_{1}$
(variables do not overlap) iff $\displaystyle(s,h)~{}{}\models{}~{}\exists
x_{1},\ldots,x_{n}\colon
x\mapsto(z_{1},\ldots,z_{k})\mathbin{\text{\raisebox{-0.3014pt}{$\boldsymbol{{-}{-}}$}}\text{\raisebox{0.39182pt}{\rotatebox{-17.0}{$\star$}}}}\vartheta_{1}~{}.$

This completes the proof.

###### Lemma 7

Every $\varphi\in\textsf{{S}}_{2}$ is equivalent to a formula $\psi=\exists
x_{1},\ldots,x_{n}\colon\vartheta$ for some $n\in\mathbb{N}$ with
$\vartheta\in\textsf{{S}}_{2}$ quantifier-free.

###### Proof

Analogous to the proof of Lemma 6.

Now let $\varphi\in\textsf{{eQSH}}$ and $\psi\in\textsf{{QSH}}$. By Lemma 6
and Lemma 7 there are $\varphi^{\prime}=\exists
x_{1},\ldots,x_{n}\colon\vartheta_{1}$ and $\psi^{\prime}=\exists
y_{1},\ldots,y_{m}\colon\vartheta_{2}$ with
$\vartheta_{1}\in\textsf{{S}}_{1}$,$\vartheta_{2}\in\textsf{{S}}_{2}$
quantifier-free and $\varphi\equiv\varphi^{\prime}$ and
$\psi\equiv\psi^{\prime}$. Notice that $\vartheta_{2}$ does not contain
$\mathbin{\text{\raisebox{-0.3014pt}{$\boldsymbol{{-}{-}}$}}\text{\raisebox{0.39182pt}{\rotatebox{-17.0}{$\star$}}}}$.
We may without loss of generality assume that $x_{1},\ldots,x_{n}$ do not
occur in $\vartheta_{2}$ and that $y_{1},\ldots,y_{m}$ do not occur in
$\vartheta_{1}$. Hence, we get

$\displaystyle\varphi~{}{}\models{}~{}\psi$ iff
$\displaystyle\varphi\wedge\neg\psi~{}\text{is unsatisfiable}$ iff
$\displaystyle\exists x_{1},\ldots,x_{n}\colon\vartheta_{1}\wedge\neg(\exists
y_{1},\ldots,y_{m}\colon\vartheta_{2})~{}\text{is unsatisfiable}$ (by above
reasoning) iff $\displaystyle(\exists
x_{1},\ldots,x_{n}\colon\vartheta_{1})\wedge(\forall
y_{1},\ldots,y_{m}\colon\neg\vartheta_{2})~{}\text{is unsatisfiable}$ iff
$\displaystyle\exists x_{1},\ldots,x_{n}\colon\forall
y_{1},\ldots,y_{m}\colon\vartheta_{1}\wedge\neg\vartheta_{2}~{}\text{is
unsatisfiable}~{},$ (standard prenexing)

since $\vartheta_{1}\wedge\neg\vartheta_{2}$ is quantifier free and since none
of $y_{1},\ldots,y_{m}$ occur in an instance of
$\mathbin{\text{\raisebox{-0.3014pt}{$\boldsymbol{{-}{-}}$}}\text{\raisebox{0.39182pt}{\rotatebox{-17.0}{$\star$}}}}$
occurring in $\vartheta_{1}\wedge\neg\vartheta_{2}$, the claim follows.


the result follows.

##  8\. Acknowledgements

The author was funded through the Engineering and Physical Sciences Research
Council Doctoral Training Partnership at the University of Warwick. The author
would like to thank Simon Rydin Myerson for unwavering support and guidance
while the present work was being carried out, and also Junxian Li for very
helpful conversations on Voronoï-type summation formulae.

## References

  * [1] V. N. Aznar, _On the Chern classes and the Euler characteristic for nonsingular complete intersections_ , Proc. Amer. Math. Soc. 78 143-148 (1980)
  * [2] B.J. Birch, _Forms in many variables_ , Proc. Roy. Soc. Ser. A 265 245–263 (1961)
  * [3] V. Blomer, L. Grimmelt, J. Li, S. L. Rydin Myerson, _Additive problems with almost prime squares_ , arxiv:2111.01601 (2022)
  * [4] T.D. Browning and D.R. Heath-Brown, _Rational points on quartic hypersurfaces_ , J. reine angew. Math. 629 37–88 (2009)
  * [5] T. D. Browning, D. R. Heath-Brown and P. Salberger, _Counting rational points on algebraic varieties_ , Duke Math. J. 132 545-578 (2006)
  * [6] T. D. Browning and R. Munshi, _Rational points on singular intersections of quadrics_ , Compositio Math. 149 1457-1494 (2013)
  * [7] J.-L. Colliot-Thélène, J.-J. Sansuc and P. Swinnerton-Dyer, _Intersections of two quadrics and Châtelet surfaces, I_ , J. reine angew. Math. 373 37-107 (1987)
  * [8] D. Cox, _Primes of the form $x^{2}+ny^{2}$, Second Edition_, Wiley (2013)
  * [9] H. Davenport, _Cubic forms in 16 variables_. Proc. Roy. Soc. A 272, 285–303 (1963)
  * [10] P. Deligne, _La conjecture de Weil. I_ , Publ. Math. Inst. Hautes Études Sci. 43 273-307 (1974)
  * [11] W. Duke, J. B. Friedlander and H. Iwaniec, _Bounds for automorphic $L$-functions_, Invent. Math. 112 1-8 (1993)
  * [12] L. Ein, _Varieties with small dual varieties, I_ , Invent. Math. 86 63-74 (1986)
  * [13] D. R. Heath-Brown, _A new form of the circle method, and its applications to quadratic forms_ , J. Reine. Angew. Math. 481 149-206 (1996)
  * [14] D.R. Heath-Brown, _Cubic forms in 14 variables_ , Invent. Math. 170, 199–230 (2007)
  * [15] D.R. Heath-Brown, _Cubic forms in ten variables_ , Proc. London Math. Soc. 47 225–257 (1983)
  * [16] C. Hooley, _On nonary cubic forms_ , J. reine angew. Math. 386 32–98 (1988)
  * [17] C. Hooley, _On the number of points on a complete intersection over a finite field_ , J. Number Theory 38 338-358 (1991)
  * [18] H. Iwaniec, _Topics in classical automorphic forms_ , Grad. Stud. Math. 17, AMS (1997)
  * [19] H. Iwaniec, E. Kowalski, _Analytic Number Theory_ , Colloquium Publications 53
  * [20] E. Kowalski, P. Michel, J. Vanderkam, _Rankin-Selberg L-functions in the level aspect_ , Duke Math. J. 114 (1) 123 - 191 (2002)
  * [21] D. Marcus, _Number Fields, Second Edition_ , Springer (2018)
  * [22] O. Marmon, P. Vishe, _On the Hasse principle for quartic hypersurfaces_ , Duke Math. J. 168 (14) 2727 - 2799, (2019)
  * [23] R. Munshi, _Pairs of quadrics in $11$ variables_, Compositio Math. 151 1189-1214 (2015)
  * [24] S. L. Rydin Myerson, _Systems of forms in many variables_ , arXiv:1709.08917 (2017)


[LO,RE]2mmEduardo Gallo

[LO,RE]2mmEduardo Gallo

[LO,RE]2mmEduardo Gallo

block        = [draw, fill=blue!30, rectangle, text centered, minimum height=3em, minimum width=6em]
blockred     = [draw, fill=red!30, rectangle, text centered, minimum height=3em, minimum width=6em]
blockyellow  = [draw, fill=yellow!30, rectangle, text centered, minimum height=3em, minimum width=6em]
blockyellow1 = [draw, fill=yellow!15, rectangle, text centered, minimum height=3em, minimum width=6em]
blockyellow2 = [draw, fill=yellow!30, rectangle, text centered, minimum height=3em, minimum width=6em]
blockyellow3 = [draw, fill=yellow!45, rectangle, text centered, minimum height=3em, minimum width=6em]
blockyellow4 = [draw, fill=yellow!60, rectangle, text centered, minimum height=3em, minimum width=6em]
blockgreen   = [draw, fill=green!30, rectangle, text centered, minimum height=3em, minimum width=6em]
blockgreen1  = [draw, fill=green!15, rectangle, text centered, minimum height=3em, minimum width=6em]
blockgreen2  = [draw, fill=green!30, rectangle, text centered, minimum height=3em, minimum width=6em]
blockgreen3  = [draw, fill=green!45, rectangle, text centered, minimum height=3em, minimum width=6em]
blockgreen4  = [draw, fill=green!60, rectangle, text centered, minimum height=3em, minimum width=6em]
blockgrey1   = [draw, fill=black!8,  rectangle, text centered, minimum height=3em, minimum width=6em]
blockgrey2   = [draw, fill=black!16, rectangle, text centered, minimum height=3em, minimum width=6em]
blockgrey3   = [draw, fill=black!24, rectangle, text centered, minimum height=3em, minimum width=6em]
blockgrey4   = [draw, fill=black!32, rectangle, text centered, minimum height=3em, minimum width=6em]
blockgrey5   = [draw, fill=black!40, rectangle, text centered, minimum height=3em, minimum width=6em]
blocknofill  = [draw=black!50, line width=1.5pt, rectangle, rounded corners, text centered, minimum height=3em, minimum width=6em]
blockhigh    = [draw, fill=blue!20, rectangle, text centered, minimum height=6em, minimum width=6em]
noblock      = [draw=black!50, line width=1.5pt, rectangle, rounded corners, text centered, minimum height=3em, minimum width=6em]
sum          = [draw, fill=blue!20, circle, node distance=1cm]
sumrest      = [draw, fill=black, circle, radius=0.5cm]
pinstyle     = [pin edge=to-,thin,black]
title        = [text centered]

Universidad Politécnica de Madrid
Centro de Automática y Robótica

Author:     [-12pt]0pt12ptEduardo Gallo

CHAPTER: ABSTRACT

This document describes the architecture and algorithms of a high fidelity fixed wing flight simulator intended to test and validate novel guidance, navigation, and control (GNC) algorithms for autonomous aircraft. The flight simulator aims to replicate the influence of as many factors as possible on the aircraft performances, the Earth model on which the flight takes place, the physics of flight and the associated equations of motion, and in particular the behavior of the onboard sensors, limiting the assumptions or simplifications to the bare minimum, and including multiple relatively minor effects not usually considered in simulation that may in occasions play a role in the GNC algorithms not performing as intended. The author releases the flight simulator  implementation as open-source software.

The simulator modular design enables the user to replace the standard GNC algorithms with new ones, with the objective of evaluating their performances when subject to specific missions and meteorological conditions (atmospheric properties, wind field, air turbulence). The testing and evaluation is performed by means of Monte Carlo simulations, as most simulation modules (such as the aircraft mission, the meteorological conditions, the errors introduced by the sensors, and the initial conditions) are defined stochastically and hence vary in a pseudo-random way from one execution to the next according to certain user-defined input parameters, ensuring that the results are valid for a wide range of conditions.

In addition to modeling the outputs of all sensors usually present onboard a fixed wing platform, such as accelerometers, gyroscopes, magnetometers, Pitot tube, air vanes, and a Global Navigation Satellite System (GNCC) receiver, the simulator is also capable of generating realistic images of the Earth surface that resemble what an onboard camera would record if following the resulting trajectory, enabling the use and evaluation of  visual and visual inertial navigation systems.

Keywords: flight simulator, GNC, sensors, stochastic, fixed wing

empty tocchapter

CHAPTER: NOTATION

The meaning of a given variable or symbol is always clarified on its first appearance, or otherwise a cross reference is included to the location where it is properly explained. This document is organized into chapters and appendices (e.g., chapter <ref> or appendix <ref>), sections (e.g., section <ref> or <ref>), subsections (e.g., section <ref> or <ref>), and so on. Note that the prefix “sub” is not employed when referring to subsections. Referencing tables (e.g., table <ref>) and figures (e.g., figure <ref>) is also straightforward. When a reference appears in between parenthesis, it refers to an equation or mathematical expression, as in (<ref>); when in between square brackets, to a bibliographic reference, as in <cit.>; and when preceded by an A and in between square brackets, it refers to an assumption listed in appendix <ref>, e.g. [A<ref>]. Acronyms are displayed in uppercase teletype font, and reference to the proper location within the acronym list, as in GNSS.

With respect to the mathematical notation, vectors and matrices appear in bold (e.g., x⃗ or R⃗), and in general the former are lowercase and the latter uppercase, although not always. A variable or vector with a hat over it < ·̂ > refers to its (inertial) estimated value, with a circular accent <·> to its (visual) estimated value, with a tilde < · > to its measured value, and with a dot < ·̇ > to its time derivative. Other commonly employed symbols for vectors are the wide hat < · >, which refers to its skew-symmetric form, the double vertical bars <  · >, which refer to its norm, and the wedge <·^∧>, which implies a tangent space representation. In the case of a scalar, the vertical bars < | ·| > refer to its absolute value.

Appendix <ref> defines the various reference frames employed throughout this document, which are listed in table <ref>. Each is represented by an uppercase F followed by a subindex identifying the frame, such as  for the body frame. The reference frames are employed so often that it is not practical to use cross references to the proper sections within appendix <ref> every time a frame appears in the text; most have thus been omitted.

Superindexes are employed over vectors to specify the reference system in which they are viewed or evaluated (e.g.,  refers to ground velocity viewed in NED or , while  is the same vector but viewed in the body frame ). Subindexes may be employed to clarify the meaning of the variable or vector, such as in  for airspeed vector instead of the ground velocity v⃗, or to refer to a given component of a vector (e.g.  refers to the second component of ). In addition, where two reference systems appear as subindexes to a vector, it means that the vector goes from the first system to the second. For example,  refers to the angular velocity from  to  viewed in [This is analogous to the angular velocity of  with respect to  viewed in .].

This document heavily relies on the linear and Lie algebra notions discussed in <cit.>, which include:

* Random variables, distributions, stochastic processes, white noise, and robust statistics.

* Euclidean spaces and Lie groups, including the various parameterizations of the Special Orthogonal group of ℝ^3 or 𝕊𝕆(3), which represents the rigid body rotations (attitudes), and the Special Euclidean group of ℝ^3 or 𝕊𝔼(3) representing full rigid body motions (poses).

* Notions of Lie algebra, such as manifolds, tangent spaces, perturbations, plus and minus operators, time derivatives and velocities, adjoints, covariances, and Jacobians.

* Common mathematical techniques such as discrete integration, gradient descent optimization, and state estimation for Euclidean spaces and their adaptations to Lie groups.

* Composition of the linear and angular velocities and accelerations of multiple rigid bodies.

As in the case of the reference frames, it is not practical to include an external reference to <cit.> every time a concept discussed in it is employed. References to <cit.> are present in some occasions, but the reader should automatically refer to it every time that additional information about one of the above topics is required.

Many different types of Jacobians or function partial derivative matrices can be found in this document (a formal definition can be found in <cit.>), and a special notation is hence required. Jacobians are represented by a J⃗ combined with a subindex and a superindex:

* The subindex provides information about the function domain, and is composed by a symbol representing how increments are added to the domain, followed by the domain itself. A + is employed when the domain belongs to an Euclidean space[The subindex symbol may sometimes be omitted when it is clear from the context that the domain is Euclidean.] but not when it is a manifold or Lie group; in these cases, ⊕ means that increments are added in the local tangent space and ⊞ that they are added in the global tangent space.

* The superindex is composed by a second symbol representing how differences are computed in the function image or codomain, followed by the codomain itself. A - is employed when the codomain is Euclidean[The superindex symbol may sometimes be omitted when it is clear from the context that the codomain is Euclidean.], ⊖ when the differences are evaluated in the local tangent space to the codomain manifold, and ⊟ when evaluated in the global tangent space.

Several 𝕊𝕆3 and 𝕊𝔼3 representations are possible <cit.>, and while they are fully equivalent, each application has its preferred parameterization. As such, rotation matrices (e.g., ), rotation vectors (e.g., r⃗_NB), unit quaternions (e.g., ), and Euler angles (e.g., ) are all employed as required, without indicating that they refer to the same concept, e.g., the ℛ_NB rotation between the spatial  and local  frames. Similarly, affine representations (e.g., ,   ), homogeneous matrices (e.g., ), transform vectors (e.g., τ⃗_EB), and unit dual quaternions (e.g., ), are also employed as required referring to the ℳ_EB rigid body motion between a spatial frame  and a local one . The most widely used parameterizations are however the unit quaternion q⃗ for rotations and the unit dual quaternion ζ⃗ for rigid body motions.

The most common symbols related with the use of 𝕊𝕆(3) and 𝕊𝔼(3) Lie groups are ∘ for concatenation, ⊗ for both the unit quaternion and the unit dual quaternion products, < ·^-1 > for the inverse, ⊕ and ⊖ for local perturbations, ⊞ and ⊟ for global perturbations, A⃗d⃗ for the adjoint matrix, g⃗() for the transformation of points, and g⃗_*() for that of vectors.

Last, note that there are instances in this document in which it is necessary to integrate, optimize, or estimate states that include 𝕊𝕆(3) and 𝕊𝔼(3) instances. As these are not Euclidean[Although Euclidean spaces are formally defined in <cit.>, they can be informally understood as those that comply with the five axioms of Euclidean geometry ( things that are equal to the same thing are also equal to one another;  if equals be added to equals, the wholes are equal;  if equals be subtracted from equals, the remainders are equal;  things that coincide with one another are equal to one another;  the whole is greater than the part).], the author has relied on Lie theory to adapt common calculus techniques such as Runge-Kutta integration, Gauss-Newton minimization, and Extended Kalman Filtering or EKF state estimation so they operate within the 𝕊𝕆(3) or 𝕊𝔼(3) manifolds, as explained in <cit.>. This approach, which has recently experienced increased usage in the field of robotics and avoids the simplifications usually employed in aircraft navigation and trajectory prediction, is not only more rigorous and elegant, but also avoids the accumulation of errors caused by continuously reprojecting the resulting poses back into the manifold.

empty tocchapter

CHAPTER: ACRONYMS

ACC			    ACCelerometers 								        ISO			    International Organization for

ADS			    Air Data System								       											    Standardization

AOA			    Angle Of Attack								        MAG			    MAGnetometers

AOS			    Angle Of Sideslip								        MEMS		    Micro Machined Electromechanical

AT 			    Actual Trajectory								       											    System

AVL			    Athena Vortex Lattice							        MSL			    Mean Sea Level

CAM			    CAMera										        NED			    North East Down

CEP			    Circular Error Probability					        NSE			    Navigation System Error

D				    Derivative									        OAT			    Outside Air Temperature

ECEF		    Earth Centered Earth Fixed					        OSP			    Outside Static Pressure

EGM96		    Earth Gravitational Model 1996				        OT			    Observed Trajectory

EKF			    Extended Kalman Filter						        P				    Proportional

EUROCONTROL     European Organization for the Safety	        PID			    Proportional Integral Derivative

of Air Navigation								        PSD			    Power Spectral Density

FTE			    Flight Technical Error						        PSFC 		    Power Specific Fuel Consumption

GLONASS	    GLObal NAvigation Satellite System			        ROC			    Rate Of Climb

GNC			    Guidance, Navigation, and Control				        RT			    Reference Trajectory

GNSS		    Global Navigation Satellite System			        ST			    Sensed Trajectory

GPS			    Global Positioning System						        SWaP		    Size, Weight, and Power

GYR			    GYRoscopes									        TAS			    True Air Speed

I				    Integral										        TSE			    Total System Error

ICAO		    International Civil Aviation					        UAS			    Unmanned Aircraft System

Organization									        UAV			    Unmanned Aerial Vehicle

IMU			    Inertial Measurement Unit				                VLM			    Vortex Lattice Method

INS			    Inertial Navigation System					       	VT			    Visual Trajectory

INSA		    ICAO Non Standard Atmosphere		        WGS84		    World Geodetic System 1984

ISA			    ICAO Standard Atmosphere			       	WMM			    World Magnetic Model


# Bio-Inspired Modality Fusion for Active Speaker Detection

Gustavo Assunção1,2,†, Nuno Gonçalves1,2, and Paulo Menezes1,2 This work was
supported by OE - national funds of FCT/MCTES (PIDDAC) under project
UID/EEA/00048/2019.1Institute of Systems and Robotics (ISR), University of
Coimbra, R. Silvio Lima, 3030-194 Coimbra, Portugal2Department of Electrical
and Computer Engineering, University of Coimbra, Portugal†Corresponding author
<EMAIL_ADDRESS>
###### Abstract

Human beings have developed fantastic abilities to integrate information from
various sensory sources exploring their inherent complementarity. Perceptual
capabilities are therefore heightened enabling, for instance, the well-known
”cocktail party” and McGurk effects, i.e. speech disambiguation from a panoply
of sound signals. This fusion ability is also key in refining the perception
of sound source location, as in distinguishing whose voice is being heard in a
group conversation. Furthermore, Neuroscience has successfully identified the
superior colliculus region in the brain as the one responsible for this
modality fusion, with a handful of biological models having been proposed to
approach its underlying neurophysiological process. Deriving inspiration from
one of these models, this paper presents a methodology for effectively fusing
correlated auditory and visual information for active speaker detection. Such
an ability can have a wide range of applications, from teleconferencing
systems to social robotics. The detection approach initially routes auditory
and visual information through two specialized neural network structures. The
resulting embeddings are fused via a novel layer based on the superior
colliculus, whose topological structure emulates spatial neuron cross-mapping
of unimodal perceptual fields. The validation process employed two publicly
available datasets, with achieved results confirming and greatly surpassing
initial expectations.

##  I INTRODUCTION

The ability to discern between activity and passivity in humans may well
benefit social robots and autonomous cognition systems by enabling a more
accurate and natural response in interactive scenarios. Accordingly, machines
capable of this task would be able to measure some user’s engagement level and
infer valuable conclusions. Moreover, successfully solving this task would
expedite a research shift towards other problems whose solutions depend on the
output of a human activity-passivity recognizer. Recent work on data mining
and collection [1] and speaker diarization [2], which heavily rely on the use
of active speaker detection are exemplary of the topic’s importance.

Active speaker detection (ASD), or the ability to recognize who in a group is
speaking at any given time, is a subset of human activity-passivity
recognition. This subset focuses on mapping utterances that make up a speech
signal, such as in a conversation, to either a closed or open set of
intervening speakers. In turn, techniques from the subset may take advantage
of audio-only, visual-only or audiovisual information depending on their
nature. Though studies do exist taking advantage of other types of perceptual
input, such as [3], these are far more uncommon and somewhat less successful.
In the past, extensive research effort has been put towards the audio-only
section of ASD as a side tool for other problems [4], [5]. Techniques
generally relying on sequential speaker clustering [6] or speech source
localization [7], [8] were often enough to achieve real-time diarization, some
occasionally aided by supervised learning. Unfortunately these were
constrained by predetermined assumptions – mic location, static speakers,
controlled environment. Furthermore, audio-only approaches remain unable to
match segmented and clustered speech with visual speakers without additional
data or restrictions, limiting their use on audiovisual data. Hence, visual
approaches to the topic become useful, though not without their own drawbacks.
Unreservedly interpreting lip movement [9], or other facial feature variations
[10], [11] as vocal activity without accounting for similar motions stemming
from normal human interaction – emotional expression, coughing, chewing – will
of course negatively impact the detection process. An exemplary output of an
active speaker detection system is shown in Fig. 1, for easier understanding.

Figure 1: Exemplary output of an multi-speaker ASD system where the
intervening speaker(s) is(are) denoted in green and speaker passiveness is
encircled in red.

In terms of multi-modal approaches, by means of complementing a visual
approach with its audio counterpart or vice-versa, performances are generally
higher thanks to increased robustness. This improvement is obtained by
exploiting correlations between the two types of data (e.g. [12], [13]) which
may decrease ambiguous situations prone to cause model confusion – speaker
overlap, unrelated movement. Self-evidently, techniques requiring both a
visual and audio input are unable to deal with situations where either of the
modalities is missing. These situations however are scarce, an do not
correspond to the immensely vast amount of audiovisual data available
nowadays. Thus multi-modality remains as the preferred manner of addressing
active speaker detection [14], [15], [16].

In spite of the recent technological advancements which have allowed deep
learning research to flourish, such improvements would likely not have been
possible without key biological contributions to the area. The success of
remarkable architectures such as convolutional neural networks, whose earliest
iterations [17] strived to emulate neuron behavior in the visual cortex of
primates [18], would likely have been halted without this biological
inspiration. However, Engineering maintains a collaborative yet stubbornly
segregated relationship with Biology by disregarding several other promising
models which the latter has to offer.

In this study our contribution is two-fold as we propose a new multi-modal
approach to visual ASD as well as a novel bio-inspired modality fusion layer
which strives to emulate the superior colliculus structure of the brain. The
approach is designed to work in real-time and makes no prior assumptions
regarding noise, number of participants or spatial configuration. This is
because it was developed also with the intent of being used in parallel
projects, where it is required to recognize speakers and the moments they
intervene in. The newly designed modality fusion layer performs successful
integration of multi-source uni-sensory information through feedback
stimulation of spatially proximal neural regions. The obtained results were
highly positive, having exceeded expectations in terms of current state-of-
the-art standards.

The presented paper is structured as follows. Initially, examination and
insight into previous research is shown in Section II, inducting the reader
into the topic and contextualizing our approach. The proposed technique is
described in Section III, followed by an overview of the experiments carried
out in Section IV and the obtained results. These are then examined and
critically discussed in Section V. Finally, a conclusion is provided in
Section VI.

##  II RELATED WORK

The overview presented is branched into two sub-sections. To begin with,
recent research on the topic is summarized in order to give further insight
into active speaker detection (ASD), and contextualize our own approach to the
matter. Following that, we analyze a number of the few available datasets and
their suitability as an integrating part of ASD techniques.

###  II-A ASD Recent Research

Given the broad array of early audio-centered approaches, and their lingering
success with nonvisual data, current efforts have turned more towards vision-
oriented issues. This is not to say audio has stopped being a key aspect of
current approaches to ASD. In fact, multi-modal state-of-the-art techniques
have used machine learning to realize audiovisual correlations in data. Such
techniques are successful, for instance, as a means to recognize speech
related facial motion while also discerning it from other unrelated movements.
In [16], [19] Stefanov et al. used the outputs of a face detector, along with
audio-derived voice activity detection (VAD) labels, to train a CNN task
specific feature extractor together with a Perceptron classifier. For transfer
learning comparison, known CNN architectures were used as pre-trained feature
extractors whose outputs were employed in training temporal (LSTM net) and
nontemporal (Perceptron) classifiers. In a related work [20], Ren et al.
tackled clutter and unrelated motion fallible situations by extending
conventional LSTM models to share learned weights across the audio and visual
modalities. Thus learning audiovisual correlations to improve model
robustness. With a real implementation in a NAO robot, Cech et al. [21] used
time difference of arrival (TDOA) over a set of microphone pairs to
simultaneously evince potential sound sources in 2D space. A facial detector
then estimated mouth locations in 3D space, to be statistically mapped to the
former 2D sound sources and TDOAs. In a similar fashion, Gebru et al. [22]
mapped located sound sources to the 2D image plane as well as estimated
potential speaker lip positions. However, this cross-modal weighting approach
employed a GMM variation to assign weights to audio observations based on
their spatial proximity to visual observations, and vice-versa. Audiovisual
clustering then achieved active speaker detection. To give another example,
Hoover et al. [23] attempted correlating the degree of occurrence of
individual faces in a video with single speaker clusters of speech segments,
obtained using vectors of locally aggregated descriptors (VLADs) [24].

In addition to the usual reliance on high-end equipment or ideal settings –
consistent number of speakers, frontal facing and nonoverlapping speech,
mic/camera location – which is common to clustering and other methods, further
issues also occur with current state-of-the-art techniques. Particularly,
unidirectional dependency between modalities is recurrent among machine
learning approaches. The lack of carefully labeled big data on both the audio
and visual modalities for ASD evidently forces resourcing to alternatives
which transfer labels generated from one modality to its sibling (typically
from audio to video). Such processes unavoidably lead to propagation of error,
originating from the single modality prediction techniques, which could be
avoided were large ASD datasets existent and applicable to robust machine
learning architectures.

###  II-B Datasets

In order to validate audiovisual ASD techniques (and train when required),
some data encompassing all considered modalities must be available.
Furthermore, such data is required to include some form of labeling so as to
enable its application in the aforementioned techniques. Unfortunately, the
multi-modal nature and challenges inherent to audiovisual ASD constitute a
major setback in terms of acquiring labeled data. As such, small and
constrained datasets are frequently built by research teams just to evaluate
their own approaches, which of course restricts their comparability and
reduces the credibility of their success. Yet very recently a few datasets
have been created and made available, which address this current necessity in
ASD research.

In [2] the AVSpeech dataset was presented, an automatically collected large-
scale corpus made up of several lecture recordings available on YouTube. These
recordings, amounting to around 4700 hours of audiovisual data, always show a
single clearly visible face to which the ongoing speech corresponds. This
dataset could be labeled for active speaker detection using some voice
activity detection (VAD) or speech-silence discerning technique, and then
applied for training and testing of ASD approaches. However, this may lead to
model confusion later on in multi-speaker scenarios and as such AVSpeech is
perhaps best left for ASD testing. A potentially better example of a suitable
corpus is given in [15], where the Columbia dataset was first introduced.
Here, the recording of a panel discussion between 7 speakers was overlapped
with upper body bounding boxes for all participants, each labeled with
speak/no-speak markers. By always including more than one speaker in each
frame, this dataset has the benefit over AVSpeech to enable dealing with
multi-speaker situations in inference models. As for its downside, the dataset
is of reduced size and its data is considerably homogeneous. This evidently
means it may be harder to extrapolate relevant features only and generalize a
model trained on this data, which constrains the dataset’s usage in machine
learning approaches.

The largest and most heterogeneous active speaker detection dataset available
at the moment is presumably AVA-ActiveSpeaker [25], developed by Google for
the 4th ActivityNet challenge at CVPR 2019. This hand labeled set of segments
obtained from 160 YouTube videos amounts to around 38.5 hours of audiovisual
data, where each of the covered 3.65 million frames is detailed with bounding
box locations for all detected speaker faces as well as with three types of
labels for each present bounding box – speaking and audible, speaking but not
audible, not speaking. Such a corpus should therefore be perfect for learning
ASD as it covers all previously mentioned requirements for a suitable
audiovisual dataset and presents no major drawbacks. To support this, the team
behind AVA-ActiveSpeaker used it to train and test both static and recurrent
prediction models, applying modality fusion and consistently achieving great
performances. Unfortunately however, this dataset encompasses an extremely
high amount of low quality videos in terms of image resolution, audio
intelligibility and noise. The creators of the dataset even went so far as to
include several voice-over videos and dubbed versions of movies not in their
original language. This naturally means a copious amount audio clips are out
of sync with their supposedly respective facial image sequences, besides also
the lengths of these clips frequently not pairing with those of their
sequences – the same phrase usually varies in duration for different
languages. Taking this into account each of the 160 videos was manually
inspected for quality assessment, as though they may be appropriate for a
challenge in the same conditions, it would be senseless to use such great
amounts of noisy incorrect data to train a model and expect it to perform
successfully with correct data and in the real world. A total of only 20
videos, whose list is available on our github
repository111https://github.com/gustavomiguelsa/SCF, were deliberated to meet
today’s audiovisual capture standards. The repository also contains an
exemplary demonstration video of the technique described in this paper, for
easier understanding.

##  III METHODOLOGY

This section describes the path taken to develop the proposed technique aimed
at performing active speaker detection, including detailed descriptions of
each individual component of the overall system.

The developed method is capable of dealing with either audio data, visual data
or audiovisual data thanks to its split structure. To put simply, each
modality is dealt with independently through separate preprocessing and the
use of dedicated architectures for feature extraction. In order to achieve
this, audiovisual raw data is divided into audio segments for which narrowband
spectrograms are generated and propagated through the VGGVox model [1], and
corresponding sequences of facial images, whose features and corresponding
temporal correlations are obtained through the employment of an extended
ResNet50 architecture [26] with incorporated recurrence henceforth designated
as RN-LSTM. The convolutional stage of the former has been pretrained with the
VGGFace2 dataset [27] and is available in [28]. Detail is further provided for
each model component in the following sections.

###  III-A Audio Clips and VGGVox

In [1], the VGGVox model was first introduced as a modified VGG-M CNN
architecture [29] aimed at speaker recognition through examination of spectral
representations of audio clips. Given its extensive training with over 100,000
utterances by 7000+ distinct speakers, the observed excellent performance has
been recognized as a state-of-the-art standard in recent research. Thus, the
model is ideal for extrapolating speaker specific cues and discern multiple
distinct speakers in an active speaker detection scenario.

In terms of actual audio clips to be analyzed, they should be required to
undergo minimal preprocessing only while still being able to progress through
a machine learning model. In the past, many techniques have been proposed to
obtain audio representations which achieve this goal such as the known Mel-
frequency cepstral coefficients [30]. Despite their success, such techniques
are noted to introduce increased overhead and require a manual tuning which
somewhat invalidates the posterior model’s positive performance. Therefore for
each raw audio clip in our approach, a sliding Hamming window of width 25ms
was applied with a step of 10ms in order to generate a respective narrowband
spectrogram, as well as means and variances being normalized at each frequency
bin of the spectrum. These operations were the single ones performed on the
audio data, following VGGVox’s preprocessing stage.

###  III-B Image Sequences and RN-LSTM

The ResNet-50 residual network architecture is one based on the deep residual
learning process proposed in the work [26], which may shortcut the connections
between the inputs and outputs of a network’s intermediate layers – creating
identity mappings. This procedure is performed in order to attempt
approximation of residual functions in lieu of fitting a more complex mapping,
thanks to the ease of learning advantage caused by occasional skipping of
layers considered less relevant. Through skipping, increasingly deeper models
may be created without the inherent accuracy degradation previously observed
in [31] and still benefiting from improved generalization. In addition, the
identity mappings also imply a loss similar to that of their shallow non-
residual equivalent models. For these reasons, residual networks should be
capable of achieving the level of generalization necessary for extracting
activity/inactivity cues from face images.

Whilst residual networks may be suitable for the task, these were not
originally trained for facial analysis. Furthermore, ASD approaches must
unavoidably deal with human faces in real world interactions which are
obviously unconstrained by pose or expression, besides potentially
encompassing several and extremely diversified physical attributes. As a means
of dealing with these face issues and other common image problems (e.g.
varying light/exposure) while still benefiting from the advantages of residual
architectures, the ResNet-50 model trained with VGGFace2 made available by
[27] was chosen for our approach.

Considering how little to no conclusions pertaining to speech activity may be
drawn from solo face images, analyzing the sequential patterns between them
becomes a requirement for success. Undoubtedly, recurrent neural networks and
more specifically LSTMs are highly suitable for approaching that requirement
given their demonstrated past success when dealing with the temporal
correlation of facial embeddings [32], [33]. Thus a wide double-layered LSTM
was appended to the trained ResNet-50 architecture creating the mentioned RN-
LSTM. This new recurrent section was trained freely by freezing the weights of
its preceding ResNet-50 layers.

###  III-C Bio-Inspired Embedding Fusion

Integration of multi-modal information is a considerably complex task
characterized by deeply convoluted data correlations. In the animal kingdom,
such a task is unconsciously performed on certain brain regions, allowing for
beings and equally humans to derive multi-sensory conclusions. Inspired by the
work of Ursino et al. in [34] and their model of the brain’s superior
colliculus (SC) for multi-sensory integration, we present a novel bio-inspired
neural network layer for audio and visual embedding fusion. This section
describes its structure and behavior.

The proposed SC fusion layer, henceforth abbreviated to SCF, is composed by
two upstream uni-modal neural areas corresponding to the audio and visual
modalities, plus the additional downstream multi-modal area in charge of
audiovisual integration. Each upstream area comprises $N\times M$ basic neuron
units interlinked within that same area, but not between upstream areas, and
topologically organized to communicate inputs to corresponding downstream
neurons whose receptive fields (RF) – kernels – are in the same spatial
positions. The downstream area in turn, also made up of $N\times M$ neurons,
feedbacks to each upstream area in the same neuron spatial fashion. This
serves to emulate how proximal biological neurons respond to stimuli in
proximal position of space, and allows for visual area neurons to indirectly
excite audio area neurons or vice-versa through the multi-modal area. Lateral
synapses between intra-area neurons are modelled after a mexican hat (Ricker)
wavelet, so they may be both excitatory (central region) and inhibitory
(surrounding region). The overall described structure is depicted in Fig. 2.

Figure 2: Overall SCF layer structure, where the synapses of the central
darker neuron (representing neuron $ij$ in a $N\times M$ neural area) are
modelled after a Mexican Hat wavelet. Each neuron is laterally linked to its
area $s$ neighbors by excitatory $ex$ and inhibitory $in$ synapses (red
arrows). The described spatially conditional connection between uni-modal
neurons (visual/auditory) and their multi-modal counterparts is shown on the
right.

Considering a neural area $s\in S=\\{a,v,m\\}$, pertaining to the auditory,
visual and multi-modal factors. Asserting $s$ to be composed of $N\times M$
neurons as previously described, each neuron $ij$ or $hk$
($i,h=1,\ldots,N;j,k=1,\ldots,M$) receives a composite input $u^{s}_{ij}[n]$
as in (1).

$u^{s}_{ij}[n]=\left\\{\begin{array}[]{ll}r^{s}_{ij}[n]+l^{s}_{ij}[n]+f^{s}_{ij}[n]\hskip
28.45274pts=\\{a,v\\}\vspace{0.5cm}\\\ k^{a}\cdot z^{a}_{ij}[n]+k^{v}\cdot
z^{v}_{ij}[n]+l^{s}_{ij}[n]\hskip 8.5359pts=m\\\ \end{array}\right.$ (1)

Where $r^{s}_{ij}[n]$ denotes the input at neuron $ij$ triggered by an
external stimulus, $l^{s}_{ij}[n]$ represents the input caused by lateral
synapses between intra-area neurons, $f^{s}_{ij}[n]$ is the feedback input
from the multi-modal SC neurons up to the uni-modal neurons, and
$z^{s}_{ij}[n]$ describes an arbitrary neuron’s activity whose continuous
differential model is discretized in our implementation as the signal in (2)
for any $s\in S$.

$\begin{array}[]{ll}\tau_{s}z^{s}_{ij}[n+1]=(\tau_{s}-1)z^{s}_{ij}[n]+\phi(p^{s}(u^{s}_{ij}[n]-\vartheta^{s}))\end{array}$
(2)

Figure 3: Structure overview of the proposed model. From a video, the image
sequence of a face is extracted as well as the corresponding audio. A
narrowband spectrogram is generated from the audio and progressed through
VGGVox. The image sequence is progressed through the RN-LSTM without any
preprocessing. The obtained audio and visual embeddings are then classified
either separately or merged by concatenation or the SCF layer.

For such a response $\tau_{s}$ refers to the speed with which a neuron
responds to some stimulus, and $\phi$ is the sigmoidal activation of some
input $u^{s}_{ij}[n]$ normalized by $\vartheta^{s}$ and $p^{s}$ – respectively
the input value at the central point of neuron activity and its slope. As a
consequence, the input to a multi-modal neuron can be seen as the weighted sum
of the input activities of each of its spatial uni-sensory counterparts
($k^{a}$ and $k^{v}$ being inter-area synaptic connection intensity) plus the
area’s own lateral synapses.

The laterally synaptic input received by some neuron $ij$ of an area $s$ is
defined simply as the weighted sum of the neighboring neurons activities,
following (3). Here $L^{s}_{ij,hk}$ represents the strength of the synaptic
connection from neuron $hk$ to neuron $ij$, which follows the mexican hat
wavelet in (4) as previously explained.

$\begin{array}[]{ll}l^{s}_{ij}[n]=\sum_{h,k}L^{s}_{ij,hk}\cdot
z^{s}_{hk}[n]&s\in S\end{array}$ (3)

$\begin{array}[]{ll}L^{s}_{ij,hk}=L_{ex}^{s}\cdot
e^{-\frac{[d_{x}^{2}+d_{y}^{2}]}{2\cdot(\sigma_{ex}^{s})^{2}}}-L_{in}^{s}\cdot
e^{-\frac{[d_{x}^{2}+d_{y}^{2}]}{2\cdot(\sigma_{in}^{s})^{2}}}&s\in
S\end{array}$ (4)

Where the $L_{ex},\sigma_{ex}$ and $L_{in},\sigma_{in}$ parameters define the
strength and spatial disposition of excitatory and inhibitory lateral
synapses, respectively. As for $d_{x}$ and $d_{y}$ these refer to the inter-
area distances between vertically and horizontally intervening neurons, being
calculated circularly to prevent border issues.

In terms of the external stimulus input at each neuron $r^{s}_{ij}[n]$, this
was obtained through the inner product of the stimulus $I_{s}$ with the
neuron’s own receptive field $R_{ij}^{s}$, made trainable and adaptive at each
epoch, as in (5). This was also the case for the feedback input
$f^{s}_{ij}[n]$, being calculated as the inner product of a multi-modal
neuron’s activity $z^{m}_{ij}[n]$ and $F_{s}$, the strength of the feedback
synaptic connection, as in (6).

$\begin{array}[]{ll}r^{s}_{ij}[n]=R_{ij}^{s}\cdot
I_{s}&s=\\{a,v\\}\end{array}$ (5)

$\begin{array}[]{ll}f^{s}_{ij}[n]=F_{s}\cdot
z^{m}_{ij}[n]&s=\\{a,v\\}\end{array}$ (6)

The motivation behind the proposed layer structure comes from the need to
effectively fuse single modality embeddings. The ideal result is an enhanced
multi-modal embedding of the most useful audio-video correlations and
features. This is achieved thanks to the SC emulation area which upon
receiving a multi-modal stimulus reinforces each of its uni-sensory fractions
upstream to spatially correlated neuron regions. This concept has greater
reach than the one demonstrated on this paper, as there is absolutely no
restrictions in terms of number of modalities for fusion – a posture analysis
neural area could be added by extending (1), behaving similarly to the
auditory and visual areas. Moreover, prior sub-fusion areas could also be
integrated in the model to combine more closely correlated information – the
vision neural area could be divided in two in the case of using a stereo
rather than mono visual capture technique. Finally, the structure’s described
non-trainable parameters were made fine tunable to application specific goals
but we kept their default values in our implementation, being supported by the
literature pointed in [34].

Evidently the embeddings used for the concatenation approach as well as the
input auditory + visual stimulus for the novel SCF layer method were obtained
using the previously described VGGVox and RN-LSTM networks. A comprehensive
diagram of the overall structure is shown in Fig. 3.

##  IV EXPERIMENTS

The experimental portion of our work consisted of two distinct parts: (1) data
preparation, given how the condition of the available data was not suitable
for proper immediate testing; (2) modality experimentation, where each
modality was tested first individually and then fused together.

###  IV-A Data preparation

The evaluation of the proposed ASD system required a considerably large amount
of data, preferably with a high degree of heterogeneity and with respect to
natural conversations. Yet as previously noted, no single dataset encompasses
all these characteristics and so the testing phase examined data from two
sources: the Columbia dataset [15]; and the 20 videos considered acceptable
from the AVA-ActiveSpeaker dataset [25]. All of the latter’s sequences were
already under the 10 second mark and so were left untouched, as opposed to the
former’s which were originally only 136 and ranged from less than 1 second to
several minutes in terms of duration. Consequently and considering the
standard 30 fps frame rate of the original video, all instances above the 30
frame mark were segmented into 30 frame long sequences. This was performed in
order to obtain a much larger number of instances and take better advantage of
all the available data for training and testing. Sequences from both datasets
below the 30 frame mark were discarded as it was considered samples under 1
second in length would likely suffer from the same problems as static images
with respect to active speaker detection. Given how ultimately the obtained
sequences for training and testing were of varying lengths, masking was
employed in order to enable all available sequences to be accepted by the RN-
LSTM. Considering this, training was independent of frame window size, making
it arbitrary (within 1 and 10 seconds) for model applications. As for the AVA-
ActiveSpeaker sequences pertaining to the third label ’SPEAKING_NOT_AUDIBLE’,
these were considered for the visual only portion of the experiments and
disregarded for the rest. The overall characteristics of the evaluated data
are specified in Table I.

TABLE I: Characteristics of the prepared data

Dataset | Sequences | Frames |  | Unique
---
Facial Trackings
222This factor is provided in place of number of speakers given the fact that AVA-ActiveSpeaker does not inform on speaker amount. However, the same speaker has been manually verified to not exist in two different videos. | Image
---
Conditions
Columbia | 4914 | 30 | 34 (6 speakers) | Identical
AVA-ActiveSpeaker |  | 5510 (3 labels)
---
5470 (2 labels)
[30,300] | 4321 (20 videos) | Varied

###  IV-B Modality Experimentation

Before attempting classification of the fused multi-modal embeddings, an
initial testing of each individual modality was performed to assess the
extrapolation quality and obtain a term of comparison for later on.
Accordingly, multilayer perceptrons (MLP) were attached to the end of the
feature extraction layers of VGGVox and the developed RN-LSTM, for
classification. Additionally, level of model generalization was also assessed
by comparing dependence and independence scenarios in terms of speaker for the
Columbia dataset and in terms of video for AVA-ActiveSpeaker – a solution to
the unknown speaker amount issue22footnotemark: 2. Essentially, for dependent
scenario experiments (closed set) the test data includes instances from
speakers who are also represented in the training data, albeit by completely
distinct instances. On the contrary, for independent scenario experiments
(open set) it is guaranteed that the speakers from the test data are
completely different and never before seen by the model during training. These
two types of testing allow for a better evaluation of the model’s
generalization ability, by examining how much the model’s performance
decreases from dependency to independency. The obtained results are presented
in Tables II and III, respectively.

TABLE II: Audio/video results using the Columbia dataset Mean Accuracy
(Standard Deviation)

| Speaker Dependent | Speaker Independent
---|---|---
| $VGGVox+MLP_{2}$
---
(Audio Only)
47.37 (0.52) [%] | 17.34 (9.14) [%]
|  $RN$-$LSTM+MLP_{1}$
---
(Video Only)
97.68 (0.39) [%] | 64.89 (14.44) [%]

TABLE III: Audio/video results using the AVA-ActiveSpeaker videos Mean
Accuracy (Standard Deviation)

| Video Dependent | Video Independent
---|---|---
| $VGGVox+MLP_{2}$
---
(Audio Only)
87.73 (0.87) [%] | 84.96 (1.78) [%]
|  $RN$-$LSTM+MLP_{1}$
---
(Video Only)
78.68 (1.79) [%] | 72.48 (2.17) [%]

The novel SCF layer, as well as the entirety of the implemented experiments,
were realized using the Keras framework [35]. In order to assess its
superiority against state-of-the-art standards and suitability to the task at
hand, we compared its performance to a naive baseline. This was composed of an
audiovisual concatenated embedding array fed directly to a multi-layer
perceptron, as seen in Fig. 3. The results of this experiment and those
obtained with the SCF layer alternative are shown in Tables IV and V for the
Columbia and AVA datasets, respectively.

TABLE IV: Audiovisual results using the Columbia dataset Mean Accuracy
(Standard Deviation)

| Speaker Dependent | Speaker Independent
---|---|---
| $Concat+MLP_{3}$
---
(Baseline)
97.60 (0.49) [%] | 41.78 (15.46) [%]
| $SCF+MLP_{3}$
---
(New Approach)
98.53 (0.21) [%] | 58.50 (7.71) [%]

TABLE V: Audiovisual results using the AVA-ActiveSpeaker videos Mean Accuracy
(Standard Deviation)

| Video Dependent | Video Independent
---|---|---
| $Concat+MLP_{3}$
---
(Baseline)
89.10 (0.41) [%] | 87.52 (2.49) [%]
| $SCF+MLP_{3}$
---
(New Approach)
91.68 (0.51) [%] | 88.46 (2.06) [%]

The SCF layer’s neural areas were kept at a $17\times 17$ dimension, for the
sake of computational simplicity. Each of the presented values in all tables
was obtained using 5-fold cross validation for increased robustness.
Furthermore, the adaptive moment estimation (Adam) optimizer [36] was employed
during the training phase of the models for weight adjustment. Batch
normalization [37] was also integrated in the training, in addition to minor
dropout [38]. The number of epochs was maintained constant across transversal
testing, having each ideal value been obtained through early stopping
mechanism for the three experimental phases (video-only, audio-only and
audiovisual).

##  V DISCUSSION

As a first observation, it can be noted how the audio-only approach to active
speaker detection (Tables II, III) performed surprisingly well for the AVA-
ActiveSpeaker videos but was rather unsuccessful for the Columbia dataset.
This is attributed to the mentioned data homogeneity of the latter,
considering it encompasses a single speaker panel video. The fact that there
is constant speech in the video (one speaker picks up after the other)
prevents the model from learning even the most basic factor of discerning
silence from speech. Hence results matching random decision for speaker
dependency but failing with the independent case.

Still regarding the Columbia dataset’s homogeneity, it proves to be
advantageous for the dependent section of the video-only testing phase, but
again not so much for the independent one. Thus the model naturally performs
better with previously seen subjects but fails to extrapolate suitable ASD
features by training with such a reduced number of speakers. Not unlike the
audio testing however, the AVA videos led to a considerably high performance
using images only, proving data heterogeneity and speaker abundance to be
ultimately better for training as expected.

Audiovisual results greatly surpassed expectations, with the baseline
concatenation approach already demonstrating state-of-the-art performance for
either dataset considered. Increase in terms of standard deviation from the
dependent to the independent testing was observed as expected, considering how
the model suffers a natural decrease of confidence in its predictions when
analyzing previously unseen speakers. Relatively poor results are of course
still obtained for the independent part of the Columbia dataset testing due to
the constant speech issue, which as expected severely hinders the model’s
performance. Nonetheless, results are remarkably positive for either
concatenation or SCF layer approaches with respect to speaker dependent
testing. Moreover, the SCF layer still showed its superiority by majorly
improving over concatenation and even surpassing a random choice performance
despite having to deal with crippling audio data. As for the AVA video
testing, both the concatenation and SCF results beat those presented in the
dataset paper [25]333Even though testing was carried out with only 20 of the
original videos, the performance gain was still exemplary in terms of result
excellence.. Even more so, the SCF layer successfully improved the already
excellent baseline performance. This serves to validate its bio-inspired
concept – mutual neuron excitation of spatially proximal multi-modal neural
regions for integration of uni-sensory information – here emulated for
modality fusion. Undoubtedly even greater performance gains could be achieved
if all the layer’s hyperparameters were finely tuned to our application,
rather than using default values. Nonetheless, results were highly successful
and warrant further research in this and other areas encompassing several
types of modalities.

##  VI CONCLUSIONS

This work proposed a novel modality fusion layer (SCF), bio-inspired by the
brain’s superior colliculus region and incorporated into a new method for
active speaker detection (ASD) in real-world scenarios. This proposed method
deals with audio and video information jointly and makes no assumptions
regarding input data. The audiovisual technique was extensively tested against
data from two tried and tested ASD databases, specifically the Columbia [15]
and the AVA-ActiveSpeaker [25] datasets. The obtained results were compared to
those of audio-only and video-only approaches, as well as those of a naive
concatenation multi-modal baseline. In any case the SCF technique always
demonstrated state-of-the-art performance, surpassing its baseline and uni-
modal counterparts. It was shown how mutual neuron excitation of a spatially
proximal multi-modal region by uni-modal neurons can be a remarkably
successful modality fusion technique.

This observed SCF layer’s success in terms of uni-sensory data integration,
even despite doing so with default settings, evidently warrants a greater
exploration of its capabilities. As such, in the future we intend to further
examine the layer’s behavior in terms of not only audiovisual fusion but also
combination of data of other natures (e.g. tactile). In addition, the
development of a real-time ASD demo based on the system presented in this work
is underway.

## References

  * [1] A. Nagrani, J. S. Chung, and A. Zisserman. Voxceleb: a large-scale speaker identification dataset. InProc. Inter-speech, 2018.
  * [2] A. Ephrat, I. Mosseri, O. Lang, T. Dekel, K. Wilson, A. Hassidim, W. T. Freeman, and M. Rubinstein. Looking to listen at the cocktail party: A speaker-independent audio-visual model for speech separation. ACT Trans. Graph., 37(112),2018.
  * [3] H. Vajaria, S. Sarkar, and R. Kasturi, “Exploring co-occurrence between speech and body movement for audio-guided video localization,” IEEE Transactions on Circuits and Systems for Video Technology, vol. 18,no. 11, pp. 1608–1617, 2008.
  * [4] S. E. Tranter and D. A. Reynolds, ”An overview of automatic speaker diarization systems,” in IEEE Transactions on Audio, Speech, and Language Processing, vol. 14, no. 5, pp. 1557-1565, Sept. 2006.
  * [5] R. Le Bouquin-Jeannès and G. Faucon, ”Study of a voice activity detector and its influence on a noise reduction system,” Speech Comm., vol. 16, pp. 245-254, 1995.
  * [6] D. Liu and F. Kubala,“Online speaker clustering”, in Proc. IEEE Int. Conf. Acoust., Speech, Signal Processing, vol. I, Hong Kong, China, Apr.2003, pp. 572–575.
  * [7] S. Maraboina, D. Kolossa, P. K. Bora and R. Orglmeister, ”Multi-speaker voice activity detection using ICA and beampattern analysis,” 2006 14th European Signal Processing Conference, Florence, 2006, pp. 1-5.
  * [8] A. Bertrand and M. Moonen, ”Energy-based multi-speaker voice activity detection with an ad hoc microphone array,” 2010 IEEE International Conference on Acoustics, Speech and Signal Processing, Dallas, TX, 2010, pp. 85-88.
  * [9] S. Siatras, N. Nikolaidis, M. Krinidis and I. Pitas, ”Visual Lip Activity Detection and Speaker Detection Using Mouth Region Intensities,” in IEEE Transactions on Circuits and Systems for Video Technology, vol. 19, no. 1, pp. 133-137, Jan. 2009.
  * [10] R. Ahmad, S. P. Raza and H. Malik, ”Visual Speech Detection Using an Unsupervised Learning Framework,” 2013 12th International Conference on Machine Learning and Applications, Miami, FL, 2013, pp. 525-528. doi: 10.1109/ICMLA.2013.171.
  * [11] K. Stefanov, A. Sugimoto, and J. Beskow. Look who’s talking: Visual identification of the active speaker in multi-party human-robot interaction. InProc. Workshop Advance-ments in Social Signal Processing for Multimodal Interac-tion, pages 22–27. ACM, 2016.
  * [12] V. P. Minotto, C. R. Jung and B. Lee, ”Simultaneous-Speaker Voice Activity Detection and Localization Using Mid-Fusion of SVM and HMMs,” in IEEE Transactions on Multimedia, vol. 16, no. 4, pp. 1032-1044, June 2014.
  * [13] R. Cutler and L. Davis, ”Look who’s talking: speaker detection using video and audio correlation,” 2000 IEEE International Conference on Multimedia and Expo. ICME2000. Proceedings. Latest Advances in the Fast Changing World of Multimedia (Cat. No.00TH8532), New York, NY, 2000, pp. 1589-1592 vol.3.
  * [14] P. Chakravarty, S. Mirzaei, T. Tuytelaars, and H. Vanhamme. Who’s speaking? audio-supervised classification of active speakers in video. InProc. ACM Int. Conf. Multimodal In-teraction, pages 1–5, 2015.
  * [15] P. Chakravarty and T. Tuytelaars. Cross-modal supervision for learning active speaker detection in video. InProc. European Conference on Computer Vision, pages 1–5, 2016.
  * [16] K. Stefanov, J. Beskow, and G. Salvi, “Vision-based active speaker detection in multiparty interaction,” in Proceedings of GLU 2017 Inter-national Workshop on Grounding Language Understanding, 2017, pp.47–51.
  * [17] K. Fukushima. ”Neocognitron: A self-organizing neural network model for a mechanism of pattern recognition unaffected by shift in position”, Biological Cybernetics, vol. 36 (4):93-202, 1980.
  * [18] D. H. Hubel, and T. N. Wiesel. ”Receptive fields and functional architecture of monkey striate cortex”, The Journal of physiology, vol. 195 (1):215-243, 1968.
  * [19] K. Stefanov, J. Beskow and G. Salvi, ”Self-Supervised Vision-Based Detection of the Active Speaker as Support for Socially-Aware Language Acquisition”, in IEEE Transactions on Cognitive and Developmental Systems, 2019.
  * [20] J. Ren, Y. Hu, Y.-W. Tai, C. Wang, L. Xu, W. Sun, and Q. Yan, “Look, listen and learn - a multimodal LSTM for speaker identification”, in Proceedings of the Thirtieth AAAI Conference on Artificial Intelligence, 2016, pp. 3581–3587.
  * [21] J. Cech, R. Mittal, A. Deleforge, J. Sanchez-Riera, X. Alameda-Pineda and R. Horaud, ”Active-speaker detection and localization with microphones and cameras embedded into a robotic head”, 2013 13th IEEE-RAS International Conference on Humanoid Robots (Humanoids), Atlanta, GA, 2013, pp. 203-210.
  * [22] I. D. Gebru, X. Alameda-Pineda, R. Horaud and F. Forbes, ”Audio-visual speaker localization via weighted clustering”, 2014 IEEE International Workshop on Machine Learning for Signal Processing (MLSP), Reims, 2014, pp. 1-6.
  * [23] K. Hoover, S. Chaudhuri, C. Pantofaru, I. Sturdy and M. Slaney, ”Using audio-visual information to understand speaker activity: Tracking active speakers on and off screen”, 2018 IEEE International Conference on Acoustics, Speech and Signal Processing (ICASSP), Calgary, AB, 2018, pp. 6558-6562.
  * [24] H. Jegou, F. Perronnin, M. Douze, J. Sanchez, P. Perez, and C. Schmid. ”Aggregating local image descriptors into compact codes”, TPAMI, 2012.
  * [25] J. Roth, S. Chaudhuri, O. Klejch, R. Marvin, A. C. Gallagher, L. Kaver, S. Ramaswamy, A. Stopczynski, C. Schmid, Z. Xi and C. Pantofaru, ”AVA-ActiveSpeaker: An Audio-Visual Dataset for Active Speaker Detection”, 2019. ArXiv, abs/1901.01342.
  * [26] K. He, X. Zhang, S. Ren, and J. Sun, ”Deep residual learning for image recognition”, In Proceedings of the Conference on Computer Vision and Pattern Recognition, pp 770–778, 2016.
  * [27] Q. Cao, L. Shen, W. Xie, O. Parkhi, A. Zisserman, ”VGGFace2: A Dataset for Recognising Faces across Pose and Age”, In Proceedings of the IEEE International Conference on Automatic Face & Gesture Recognition, 2018.
  * [28] The Keras-VGGFace Package. Available at: https://pypi.org/project/keras-vggface/.
  * [29] K. Chatfield, K. Simonyan, A. Vedaldi, and A. Zisserman, ”Return of the devil in the details: Delving deep into convolutional nets”. In Proceedings of the British Machine Vision Conference, 2014.
  * [30] P. Mermelstein, ”Distance measures for speech recognition, psychological and instrumental,” in Pattern Recognition and Artificial Intelligence, 1976, C. H. Chen Ed., pp374–388, Academic, New York.
  * [31] K. He and J. Sun, ”Convolutional neural networks at constrained timecost”, In CVPR, 2015.
  * [32] S. Kankanamge, C. Fookes and S. Sridharan, ”Facial analysis in the wild with LSTM networks”, 2017 IEEE International Conference on Image Processing (ICIP), Beijing, 2017, pp. 1052-1056.
  * [33] Z. Xu, S. Li and W. Deng, ”Learning temporal features using LSTM-CNN architecture for face anti-spoofing”, 2015 3rd IAPR Asian Conference on Pattern Recognition (ACPR), Kuala Lumpur, 2015, pp. 141-145.
  * [34] M. Ursino, C. Cuppini, E. Magosso, A. Serino, and G. di Pellegrino. ”Multisensory integration in the superior colliculus: a neural network model”, Journal of Computational Neuroscience, 26(1):55–73, May 2008.
  * [35] F. Chollet and others. Keras. https://keras.io, 2015.
  * [36] D. P. Kingma and J. Ba, ”Adam: A method for stochastic optimization”, arXivpreprint arXiv:1412.6980, 2014.
  * [37] S. Ioffe and C. Szegedy, ”Batch normalization: Acceleratingdeep network training by reducing internal covariate shift”, arXivpreprint arXiv:1502.03167, 2015.
  * [38] N. Srivastava, G. Hinton, A. Krizhevsky, I. Sutskever, and R. Salakhutdinov. ”Dropout: A simple way to prevent neural networks from overfitting”, Journal of Machine Learning Research, 15:1929–1958, 2014.