# Mean-square Analysis of the NLMS Algorithm

Tareq Y. Al-Naffouri, Muhammad Moinuddin, and Anum Ali T. Y. Al-Naffouri is
with the Computer, Electrical and Mathematical Sciences and Engineering
Division, King Abdullah University of Science and Technology, Thuwal
23955-6900, Saudi Arabia (e-mail: tareq.alnaffouri@kaust.edu.sa).M. Moinuddin
is with the Department of Electrical and Computer Engineering, King Abdulaziz
University, Jeddah 21589, Saudi Arabia, and also with the Center of Excellence
in Intelligent Engineering Systems (CEIES), King Abdulaziz University, Jeddah
21589, Saudi Arabia (e-mail: mmsansari@ kau.edu.sa).A. Ali is with the
Standards and Mobility Innovation Laboratory, Samsung Research America, Plano,
TX 75023, USA (e-mail: anum.ali@samsung.com).

###### Abstract

This work presents a novel approach to the mean-square analysis of the
normalized least mean squares (NLMS) algorithm for circular complex colored
Gaussian inputs. The analysis is based on the derivation of a closed-form
expression for the Cumulative Distribution Function (CDF) of random variables
of the form $(||{\bf u}||_{{\bf D}_{1}}^{2})(||{\bf u}||_{{\bf
D}_{2}}^{2})^{-1}$ where ${\bf u}$ is an isotropic vector and ${\bf D}_{1}$
and ${\bf D}_{2}$ are diagonal matrices and using that to derive some moments
of these variables. These moments in turn completely characterize the mean-
square behavior of the NLMS algorithm in explicit closed-form expressions.
Specifically, the transient, steady-state, and tracking mean-square behavior
of the NLMS algorithm is studied.

##  I Introduction

The most widely used algorithm for adaptive filters is the Least Mean Squares
(LMS) [1] algorithm which provides a solution to the optimal Weiner Filter
criterion minimizing the mean square value of the error in a stochastic
approximation sense. Since the LMS algorithm belongs to such a class of
gradient-type algorithms whose convergence properties depend on the input
correlation, it inherits slow convergence, especially when operating on highly
correlated signals like speech. This dependency is removed by the input
normalization in the NLMS algorithm [2] which results in a great improvement
in convergence compared to the LMS algorithm [1]. However, the normalization
complicates the performance analysis of the algorithm.

Many researchers have attempted to study the performance of the NLMS [3, 1, 4,
5, 6, 7, 9, 8] and to understand why it has superior performance over that of
the LMS. In [3], closed-form expressions for the transient analysis and the
steady-state mean-square error (MSE) of the NLMS algorithm are developed but
these expressions are in terms of multidimensional moments which [3] falls
short of evaluation. Other prior work has attempted to evaluate these moments
but the corresponding analyses do not result in closed form performance
expressions [1, 3, 4], or rely on strong assumptions. Examples of these
assumptions include the separation principle [5, 6], approximations [7], white
input [4, 7, 8], specific structure of input regressor’s distribution [5, 10],
small step size [5], long filters [7], approximate solutions using Abelian
integrals [5] and partial evaluation of moments [11].

In this work, we obtain the closed form expressions for the required
multidimensional input moments. Our approach is based on evaluating the CDF
and the moments of random variables of the form111For any matrix ${\bf D}$,
the quadratic form $||{\bf a}||_{{\bf D}}^{2}$ is defined as $||{\bf
a}||_{{\bf D}}^{2}\stackrel{{\scriptstyle\triangle}}{{=}}{\bf a}^{*}{\bf
D}{\bf a}$. $\xi\left({\bf u},{\bf D}_{1},{\bf D}_{2}\right)=(||{\bf
u}||_{{\bf D}_{1}}^{2})(||{\bf u}||_{{\bf D}_{2}}^{2})^{-1}$ where ${\bf u}$
is a white Gaussian vector and ${\bf D}_{1}$ and ${\bf D}_{2}$ are diagonal
matrices, by expressing them as ratios of quadratic forms
$(||{\mbox{\boldmath$\phi$}}||_{{\bf
D}_{1}}^{2})(||{\mbox{\boldmath$\phi$}}||_{{\bf D}_{2}}^{2})^{-1}$ in
isotropic random vector $\phi$. We then use complex integration to evaluate
the CDF and the moments of these ratios.

The closed-form expressions obtained in this work permit the transient,
steady-state, and tracking mean-square analyses of the NLMS algorithm in a
(non) stationary environment for colored circular Gaussian inputs. Unlike
existing work, our approach neither uses the separation principle nor the
small step-size assumption. As a by-product of our approach, we demonstrate
how to statistically characterize indefinite quadratic forms in isotropic
random vectors using complex integration. These quantities are of vital
importance in signal processing, communications, and information theory and
researchers have resorted to non-traditional techniques to study these forms
[12, 13, 14]. To the best of our knowledge, this is the first work that
provides the closed-form expressions for the performance of the NLMS.

The paper is organized as follows. Following this introduction, we carry out
the transient, tracking, and steady-state mean-square analyses of the NLMS
algorithm in Section II and point out the moments that need to be evaluated to
express the performance in closed form. In Section III, the approach of our
work is outlined. Derivation for the CDF of the random variable of the form
$(||{\mbox{\boldmath$\phi$}}||_{{\bf
D}_{1}}^{2})(||{\mbox{\boldmath$\phi$}}||_{{\bf D}_{2}}^{2})^{-1}$ as well as
the derivation of its moments are carried out in Section IV. In Section V, we
present the simulation results to verify the analysis, followed by our
conclusion in Section VI.

##  II Performance Analysis of the NLMS Algorithm

###  II-A System Model

Given a sequence of desired response $\\{d_{i}\\}$ and a sequence of regressor
(row) vectors $\\{{\bf u}_{i}\\}$, an adaptive filter generates a weight
vector ${\bf w}_{i}$ at each instant so that ${\bf u}_{i}{\bf w}_{i}$ is a
good estimate of $d_{i}$. In the NLMS algorithm, the weight vector starting
from ${\bf w}_{-1}=0$ is updated according to

${\bf w}_{i}={\bf w}_{i-1}+\mu\frac{{\bf u}_{i}^{*}}{||{\bf
u}_{i}||^{2}}e_{i},\hskip 28.45274pti\geq 0,$ (1)

where $e_{i}=d_{i}-{\bf u}_{i}{\bf w}_{i-1}$ is the estimation error and $\mu$
is the step-size. In performing the analysis of the NLMS algorithm, we
consider the time variant case222Note that time invariant case is a special
scenario of time variant case which is obtained by setting ${\bf q}_{i}=0$ for
all $i$. and hence, $d_{i}$ is generated by the time-variant system
identification model $d_{i}={\bf u}_{i}{\bf w}_{i}^{o}+v_{i}$, where $v_{i}$
is a zero mean i.i.d. noise sequence with variance $\sigma_{v}^{2}$ and ${\bf
w}_{i}^{o}$ varies according to

${\bf w}_{i}^{o}={\bf w}_{i-1}^{o}+{\bf q}_{i},$ (2)

and where ${\bf q}_{i}$ is assumed to be i.i.d. colored circular complex
Gaussian ${\bf q}_{i}\sim{\mathcal{C}}{\mathcal{N}}\leavevmode\nobreak\ ({\bf
0},{\bf R}_{q})$. The ${\bf w}_{i}$ generated by the adaptive filter attempts
to track the time variant system ${\bf w}_{i}^{o}$. Let ${\tilde{\bf
w}}_{i}={\bf w}_{i}^{o}-{\bf w}_{i}$ denote the weight error vector, then

$e_{i}={\bf u}_{i}({\bf w}_{i}^{o}-{\bf w}_{i-1})+v_{i}={\bf u}_{i}{\tilde{\bf
w}}_{i-1}+v_{i}+{\bf u}_{i}{\bf q}_{i},$ (3)

and, by subtracting ${\bf w}_{i}$ from both sides of (2) and substituting the
value of ${\bf w}_{i}$ from (1), the NLMS update can be equivalently written
as

$\tilde{{\bf w}}_{i}=\tilde{{\bf w}}_{i-1}-\mu\frac{{\bf u}_{i}^{*}}{||{\bf
u}_{i}||^{2}}e_{i}+{\bf q}_{i},\hskip 28.45274pti\geq 0.$ (4)

We assume that the sequences $\\{v_{i}\\},\leavevmode\nobreak\ \\{{\bf
u}_{i}\\}$, and $\\{{\bf q}_{i}\\}$ are mutually independent which is well
justified in real practice. In addition, we will restrict our attention in
this work to circularly symmetric Gaussian inputs, i.e. ${\bf
u}_{i}\sim{\mathcal{C}}{\mathcal{N}}\leavevmode\nobreak\ ({\bf 0},{\bf
R}_{u})$. We also assume that the input vectors are independent but their
entries are correlated. For the sake of mean-square analysis, the
autocorrelation matrix ${\bf R}_{u}$ can be assumed to be diagonal, that is,
${\bf
R}_{u}=\mbox{\boldmath$\Lambda$}=\mbox{diag}(\lambda_{1},\lambda_{2},\cdots,\lambda_{M})$,
without loss of generality [3, 4].

###  II-B Mean Square Performance of the NLMS Algorithm

Starting from the recursion (4) and using an approach similar to that of [1,
3], we can show that the weighted variance relation of the NLMS weight error
vector results in333Here, ${\bf u}_{i}$ has diagonal correlation matrix
$\Lambda$ and ${\bf q}_{i}$ has rotated correlation matrix ${\bf
R}_{\bar{q}}$.

$E[||{\tilde{\bf w}}_{i}||^{2}_{\mbox{\boldmath$\sigma$}}]=E[||{\tilde{\bf
w}}_{i-1}||^{2}_{{\bf
F}\mbox{\boldmath$\sigma$}}]+\mu^{2}\sigma_{v}^{2}E\left[\frac{||{\bf
u}_{i}||^{2}_{\mbox{\boldmath$\sigma$}}}{(||{\bf
u}_{i}||^{2})^{2}}\right]+E[||{\bf q}_{i}||^{2}_{{\bf
F}\mbox{\boldmath$\sigma$}}],$ (5)

where $\sigma$ is an $M\times 1$ parameter weight vector that can provide
different performance measures by choosing its value appropriately. The matrix
${\bf F}$ is defined as

${\bf F}\mathop{=}^{\triangle}{\bf I}-\mu{\bf A}+\mu^{2}{\bf B},$ (6)

where ${\bf I}$ is the identity matrix and ${\bf A}$ and ${\bf B}$ are the
multidimensional input moment matrices

${\bf A}\mathop{=}^{\triangle}2E\left[\frac{{\bf u}^{*}_{i}{\bf u}_{i}}{||{\bf
u}_{i}||^{2}}\right],\leavevmode\nobreak\ \leavevmode\nobreak\ {\bf
B}\mathop{=}^{\triangle}E\left[\frac{({\bf u}_{i}^{*}{\bf
u}_{i})^{T}\odot({\bf u}_{i}^{*}{\bf u}_{i})}{(||{\bf
u}_{i}||^{2})^{2}}\right],$ (7)

where the notation $\odot$ denotes an element-by-element (Hadamard) product.
Equation (5) can be used to describe both the transient and steady-state
performance of the NLMS algorithm. In order to derive an expression for the
steady-state EMSE ($\zeta$), we evaluate (5) by taking the limit of both sides
of (5) as $i\rightarrow\infty$ and utilizing the fact that the terms
$E[||{\tilde{\bf w}}_{i}||^{2}_{\mbox{\boldmath$\sigma$}}]$ and
$E[||{\tilde{\bf w}}_{i-1}||^{2}_{{\bf F}\mbox{\boldmath$\sigma$}}]$ can be
combined to $E[||{\tilde{\bf w}}_{\infty}||^{2}_{(\bf{I}-{\bf
F})\mbox{\boldmath$\sigma$}}]$ at $i\rightarrow\infty$. Thus, by setting
$\mbox{\boldmath$\sigma$}=(\bf{I}-{\bf
F})^{-1}\mbox{\small{\boldmath$\lambda$}}$ (where $\lambda$ is a vector
defined as
$\mbox{\small{\boldmath$\lambda$}}=\mbox{diag}(\mbox{\boldmath$\Lambda$})$),
we can show that the steady-state EMSE of the NLMS is given by

$\zeta_{track}=\mu^{2}\sigma_{v}^{2}\mbox{Tr}({\bf C}{\bf G})+\mbox{Tr}({\bf
R}_{\bar{q}}{\bf G}_{\bar{q}}),$ (8)

where ${\bf C}$ is the multidimensional moment

${\bf C}\mathop{=}^{\triangle}E\left[\frac{{\bf u}^{*}_{i}{\bf u}_{i}}{(||{\bf
u}_{i}||^{2})^{2}}\right],$ (9)

and ${\bf G}$ and ${\bf G}_{\bar{q}}$ are diagonal matrices such that
$\mbox{diag}({\bf G})=(\bf{I}-{\bf F})^{-1}\mbox{\small{\boldmath$\lambda$}}$
and $\mbox{diag}({\bf G}_{q})={\bf F}(\bf{I}-{\bf
F})^{-1}\mbox{\small{\boldmath$\lambda$}}$. It can be noted that the steady-
state EMSE of the time invariant case can be directly deduced from (8) by
setting ${\bf q}_{i}$ to zero.

A summary of the various mean-square performance measures of the NLMS
algorithm obtained from (5) is shown in Table I.

Table I: Summary of analytical results for various performance measures of the NLMS algorithm. Performance Measure | Analytical Result | Moments Required
---|---|---
EMSE Learning Curve | $E[||{\tilde{\bf w}}_{i}||^{2}_{\mbox{\small{\boldmath$\lambda$}}}]=E[||{\bf w}^{o}||^{2}_{{\bf F}^{i}\mbox{\small{\boldmath$\lambda$}}}]+\mu^{2}\sigma_{v}^{2}E\left[\frac{||{\bf u}_{i}||^{2}_{({\bf I}+{\bf F}+\cdots+{\bf F}^{i-1})\mbox{\small{\boldmath$\lambda$}}}}{(||{\bf u}_{i}||^{2})^{2}}\right]$ |  ${\bf A},{\bf B},{\bf C}$
MSD Learning Curve | $E[||{\tilde{\bf w}}_{i}||^{2}_{\bf 1}]=E[||{\bf w}^{o}||^{2}_{{\bf F}^{i}{\bf 1}}]+\mu^{2}\sigma_{v}^{2}E\left[\frac{||{\bf u}_{i}||^{2}_{({\bf I}+{\bf F}+\cdots+{\bf F}^{i-1}){\bf 1}}}{(||{\bf u}_{i}||^{2})^{2}}\right]$ |  ${\bf A},{\bf B},{\bf C}$
Mean Stability | $0<\mu<2/\lambda_{max}(\frac{1}{2}{\bf A})$ |  ${\bf A}$
Mean Square Stability | $0<\mu<1/\lambda_{max}({\bf A}^{-1}{\bf B})$ |  ${\bf A},{\bf B}$
Steady-state EMSE | $\mu^{2}\sigma_{v}^{2}E\left[\frac{||{\bf u}_{i}||^{2}_{(\bf{I}-{\bf F})^{-1}\mbox{\small{\boldmath$\lambda$}}}}{(||{\bf u}_{i}||^{2})^{2}}\right]$ |  ${\bf A},{\bf B},{\bf C}$
Steady-state MSD | $\mu^{2}\sigma_{v}^{2}E\left[\frac{||{\bf u}_{i}||^{2}_{(\bf{I}-{\bf F})^{-1}{\bf 1}}}{(||{\bf u}_{i}||^{2})^{2}}\right]$ |  ${\bf A},{\bf B},{\bf C}$
Tracking EMSE | $\mu^{2}\sigma_{v}^{2}E\left[\frac{||{\bf u}_{i}||^{2}_{(\bf{I}-{\bf F})^{-1}\mbox{\small{\boldmath$\lambda$}}}}{(||{\bf u}_{i}||^{2})^{2}}\right]+E\left[||{\bf q}_{i}||^{2}_{{\bf F}(\bf{I}-{\bf F})^{-1}\mbox{\small{\boldmath$\lambda$}}}\right]$ |  ${\bf A},{\bf B},{\bf C}$

##  III Our Methodology

By inspecting Table I, we see that all the MSE performance measures are
completely determined by the moment matrix ${\bf F}$ (and hence the moment
matrices ${\bf A}$ and ${\bf B}$) and by the moment matrix444Table I contains
entries of the form $E\left[\frac{||{\bf u}_{i}||^{2}_{{\bf G}}}{(||{\bf
u}_{i}||^{2})^{2}}\right]$ for some weighting matrix ${\bf G}$. Knowing that
${\bf C}$ is a diagonal matrix (see Table III), it is easy to show that
$E\left[\frac{||{\bf u}_{i}||^{2}_{{\bf G}}}{(||{\bf
u}_{i}||^{2})^{2}}\right]=\mbox{Tr}({\bf C}{\bf G})$ ${\bf C}$. In order to
evaluate these moment matrices, we rewrite them as follows

${\bf A}\mathop{=}\mbox{\boldmath$\Lambda$}\bar{\bf A},\leavevmode\nobreak\
\leavevmode\nobreak\ {\bf B}=\mbox{\boldmath$\Lambda$}\bar{\bf
B}\mbox{\boldmath$\Lambda$},\leavevmode\nobreak\ \leavevmode\nobreak\
\mbox{and}\leavevmode\nobreak\ \leavevmode\nobreak\ {\bf
C}=\mbox{\boldmath$\Lambda$}\bar{\bf C},$ (10)

where $\bar{\bf A}$, $\bar{\bf B}$, and $\bar{\bf C}$ stand for the “whitened”
versions of the matrices ${\bf A}$, ${\bf B}$, and ${\bf C}$, respectively,
i.e.,

$\bar{\bf A}\mathop{=}^{\triangle}2E\left[\frac{\bar{{\bf u}}^{*}_{i}\bar{{\bf
u}}_{i}}{||{\bf u}_{i}||^{2}}\right],\leavevmode\nobreak\ \leavevmode\nobreak\
\bar{\bf B}\mathop{=}^{\triangle}E\left[\frac{(\bar{{\bf u}}_{i}^{*}\bar{{\bf
u}}_{i})^{T}\odot(\bar{{\bf u}}_{i}^{*}\bar{{\bf u}}_{i})}{(||{\bf
u}_{i}||^{2})^{2}}\right],\leavevmode\nobreak\ \leavevmode\nobreak\
\mbox{and}\leavevmode\nobreak\ \leavevmode\nobreak\ \bar{\bf
C}\mathop{=}^{\triangle}E\left[\frac{\bar{{\bf u}}^{*}_{i}\bar{{\bf
u}}_{i}}{(||{\bf u}_{i}||^{2})^{2}}\right].$ (11)

Here $\bar{u}_{i}(k)$ is the whitened version of $u_{i}(k)$, i.e.
$u_{i}(k)=\sqrt{\lambda_{k}}\bar{u}_{i}(k)$, where $\lambda_{k}$ are the
eigenvalues of the autocorrelation of the input sequence making the vector
$\bar{{\bf u}}_{i}$ of identity correlation matrix, i.e., $\bar{\bf
u}_{i}\sim{\mathcal{C}}{\mathcal{N}}\leavevmode\nobreak\ ({\bf 0},{\bf I})$.
Note that $||{\bf u}_{i}||^{2}=||\bar{\bf u}_{i}||_{\Lambda}^{2}$. Thus, from
(11), it can be easily deduced that the entries of the moment matrices
$\bar{\bf A}$, $\bar{\bf B}$, and $\bar{\bf C}$ are completely determined by
the expectation of the following

$\frac{|\bar{u}(k)|^{2}}{||\bar{\bf u}||_{\Lambda}^{2}},\leavevmode\nobreak\
\leavevmode\nobreak\ \frac{|\bar{u}(k)|^{2}|\bar{u}(\bar{k})|^{2}}{(||\bar{\bf
u}||_{\Lambda}^{2})^{2}},\leavevmode\nobreak\ \leavevmode\nobreak\
\frac{|\bar{u}(k)|^{2}}{(||\bar{\bf
u}||_{\Lambda}^{2})^{2}},\leavevmode\nobreak\ \leavevmode\nobreak\
\leavevmode\nobreak\ (\mbox{with}\leavevmode\nobreak\ k\neq\bar{k}),$ (12)

where $k$ and $\bar{k}$ denote the $k^{th}$ and $\bar{k}^{th}$ distinct
positions of the regressor elements in the input vector $\bar{{\bf u}}$. Here
we have dropped the subscript $i$ for convenience of notation. To evaluate
these moments, we will express them in terms of moments of ratios of quadratic
forms as it is relatively easy to characterize these ratios statistically
(i.e. to determine their pdf/CDF). The first random variable

$s_{k}\stackrel{{\scriptstyle\triangle}}{{=}}\frac{|\bar{u}(k)|^{2}}{||\bar{\bf
u}||_{\Lambda}^{2}},$ (13)

is already a ratio of quadratic forms. The second random variable in (12) can
be expressed with the aid of the binomial expansion as

$\frac{|\bar{u}(k)|^{2}|\bar{u}(\bar{k})|^{2}}{(||\bar{\bf
u}||_{\Lambda}^{2})^{2}}=\frac{1}{2}s_{k\bar{k}}^{2}-\frac{1}{2}\frac{\lambda_{k}}{\lambda_{\bar{k}}}s_{k}^{2}-\frac{1}{2}\frac{\lambda_{\bar{k}}}{\lambda_{k}}s_{\bar{k}}^{2},$
(14)

where $s_{k\bar{k}}$ is defined as

$s_{k\bar{k}}\stackrel{{\scriptstyle\triangle}}{{=}}\frac{\sqrt{\frac{\lambda_{k}}{\lambda_{\bar{k}}}}|\bar{u}(k)|^{2}+\sqrt{\frac{\lambda_{\bar{k}}}{\lambda_{k}}}|\bar{u}(\bar{k})|^{2}}{||\bar{\bf
u}||_{\Lambda}^{2}},$ (15)

and so (15) is a sum of two ratios of quadratic forms. Finally, in order to
evaluate the moment of third random variable in (12), we define the following
two new variables

$z_{k}\stackrel{{\scriptstyle\triangle}}{{=}}\frac{|\bar{u}(k)|^{2}+1}{||\bar{\bf
u}||_{\Lambda}^{2}},\leavevmode\nobreak\ \leavevmode\nobreak\
\leavevmode\nobreak\ \mbox{and}\leavevmode\nobreak\ \leavevmode\nobreak\
r\stackrel{{\scriptstyle\triangle}}{{=}}\frac{1}{||\bar{\bf
u}||_{\Lambda}^{2}}.$ (16)

Thus, the required random variable $\frac{|\bar{u}_{k}|^{2}}{(||\bar{\bf
u}||_{\Lambda}^{2})^{2}}$ can be obtained using binomial expansion as follows:

$\frac{|\bar{u}(k)|^{2}}{(||\bar{\bf
u}||_{\Lambda}^{2})^{2}}=\frac{1}{2}\left(\frac{|\bar{u}(k)|^{2}+1}{||\bar{\bf
u}||_{\Lambda}^{2}}\right)^{2}-\frac{1}{2}\left(\frac{|\bar{u}(k)|^{2}}{||\bar{\bf
u}||_{\Lambda}^{2}}\right)^{2}-\frac{1}{2}\left(\frac{1}{||\bar{\bf
u}||_{\Lambda}^{2}}\right)^{2}=\frac{1}{2}z_{k}^{2}-\frac{1}{2}s_{k}^{2}-\frac{1}{2}r^{2}.$
(17)

Thus, all required moments are expressed as function of the moments of
$s_{k}$, $s_{k\bar{k}}$, $r$, and $z_{k}$ as in Table II. With this, the
entries of the matrices $\bar{\bf A}$, $\bar{\bf B}$, and $\bar{\bf C}$ can be
expressed directly in terms of the moments of these random variables as shown
in Table III. In the remaining part of the paper, we derive the CDF’s of
$s_{k}$, $s_{k\bar{k}}$, $r$, and $z_{k}$ and subsequently use them to derive
the moments listed in Table III.

Table II: Required moments and their relations to $s_{k}$, $s_{k\bar{k}}$, $r$, and $z_{k}$. Required Moments |  Required Expressions
---|---
$E\left[\frac{|\bar{u}(k)|^{2}}{||\bar{\bf u}||_{\Lambda}^{2}}\right]$ |  $E\left[s_{k}\right]$
$E\left[\frac{|\bar{u}(k)|^{2}|\bar{u}(\bar{k})|^{2}}{(||\bar{\bf u}||_{\Lambda}^{2})^{2}}\right]$ | $\frac{1}{2}E\left[s_{k\bar{k}}^{2}\right]-\frac{1}{2}\frac{\lambda_{k}}{\lambda_{\bar{k}}}E\left[s_{k}^{2}\right]-\frac{1}{2}\frac{\lambda_{\bar{k}}}{\lambda_{k}}E\left[s_{\bar{k}}^{2}\right]$
$E\left[\left(\frac{1}{||\bar{\bf u}||_{\Lambda}^{2}}\right)^{2}\right]$ |  $E\left[r^{2}\right]$
$E\left[\left(\frac{|\bar{u}(k)|^{2}+1}{||\bar{\bf u}||_{\Lambda}^{2}}\right)^{2}\right]$ |  $E\left[z_{k}^{2}\right]$
$E\left[\frac{|\bar{u}(k)|^{2}}{(||\bar{\bf u}||_{\Lambda}^{2})^{2}}\right]$ | $\frac{1}{2}E\left[z_{k}^{2}\right]-\frac{1}{2}E\left[s_{k}^{2}\right]-\frac{1}{2}E\left[r^{2}\right]$
Table III: Relation of entries of moment matrices $\bar{\bf A}$, $\bar{\bf B}$, and $\bar{\bf C}$ to $s_{k}$, $s_{k\bar{k}}$, $r$, and $z_{k}$. Matrix Entries |  Required Moments
---|---
$\bar{\bf A}(k,k)$ |  $2E\left[s_{k}\right]$
$\bar{\bf A}(k,\overline{k})$ |  $0$
$\bar{\bf B}(k,k)$ |  $E\left[s_{k}^{2}\right]$
$\bar{\bf B}(k,\overline{k})$ | $\frac{1}{2}E\left[s_{k\bar{k}}^{2}\right]-\frac{1}{2}\frac{\lambda_{k}}{\lambda_{\bar{k}}}E\left[s_{k}^{2}\right]-\frac{1}{2}\frac{\lambda_{\bar{k}}}{\lambda_{k}}E\left[s_{\bar{k}}^{2}\right]$
$\bar{\bf C}(k,k)$ | $\frac{1}{2}E\left[z_{k}^{2}\right]-\frac{1}{2}E\left[s_{k}^{2}\right]-\frac{1}{2}E\left[r^{2}\right]$
$\bar{\bf C}(k,\overline{k})$ |  $0$

##  IV Evaluation of the CDF and Moments

In this section, we derive the CDF and moments for all the required variables
defined in previous section.

###  IV-A The CDF of $s_{k}$ and $s_{k\bar{k}}$

The key to evaluating the CDF of $s_{k\bar{k}}$ is to first define
$s_{k\bar{k}}$ in terms of isotropic random variables. By using the definition
${\mbox{\boldmath$\phi$}}=\left[\frac{\bar{u}(1)}{\|\bar{u}\|},\leavevmode\nobreak\
\frac{\bar{u}(2)}{\|\bar{u}\|},\cdots,\frac{\bar{u}(M)}{\|\bar{u}\|}\right]$,
we can rewrite $s_{k\bar{k}}$ as

$s_{k\bar{k}}=\frac{\sqrt{\frac{\lambda_{k}}{\lambda_{\bar{k}}}}|\bar{u}(k)|^{2}+\sqrt{\frac{\lambda_{\bar{k}}}{\lambda_{k}}}|\bar{u}(\bar{k})|^{2}}{\sum_{i=1}^{M}\lambda_{i}|\bar{u}(i)|^{2}}=\frac{\|{\mbox{\boldmath$\phi$}}\|^{2}_{{\bf\Sigma}_{k\bar{k}}}}{\|{\mbox{\boldmath$\phi$}}\|^{2}_{\bf\Lambda}},\leavevmode\nobreak\
\leavevmode\nobreak\ \leavevmode\nobreak\ k\neq\bar{k},$ (18)

where ${\bf\Sigma}_{k\bar{k}}$ is an $M\times M$ matrix with all elements set
to zero except the $k^{th}$ and $\bar{k}^{th}$ elements on the main diagonal
which are set to $\sqrt{\frac{\lambda_{k}}{\lambda_{\bar{k}}}}$ and
$\sqrt{\frac{\lambda_{\bar{k}}}{\lambda_{k}}}$, respectively. The random
vector $\phi$ in (18) is known as an isotropic random vector [14] and has the
pdf

$p(\phi)=\frac{\Gamma(M)}{\pi^{M}}\leavevmode\nobreak\
\delta(\|\phi\|^{2}-1).$ (19)

We can now express the CDF of $s_{k\bar{k}}$ using the isotropic random
variable $\phi$. Specifically,

$F_{s_{k\bar{k}}}(x)=Pr\\{s_{k\bar{k}}\leq
x\\}=Pr\\{\|{\mbox{\boldmath$\phi$}}\|^{2}_{x{\bf\Lambda}-{{\bf\Sigma}_{k\bar{k}}}}\geq
0\\}=\int_{\|{\mbox{\boldmath$\phi$}}\|^{2}_{x{\bf\Lambda}-{{\bf\Sigma}_{k\bar{k}}}}\geq
0}p({\mbox{\boldmath$\phi$}})d\phi.$ (20)

This is an $M$-dimensional integral over the region defined by the inequality
$\|{\mbox{\boldmath$\phi$}}\|^{2}_{x{\bf\Lambda}-{\bf\Sigma_{k\bar{k}}}}\geq
0$ which is difficult to evaluate. To go around this, we rewrite (20) as an
unconstrained integral by using the unit step function as

$F_{s_{k\bar{k}}}(x)=\int_{-\infty}^{\infty}p({\mbox{\boldmath$\phi$}})\tilde{u}(\|{\mbox{\boldmath$\phi$}}\|^{2}_{x{\bf\Lambda}-{{\bf\Sigma}_{k\bar{k}}}})d{\mbox{\boldmath$\phi$}}.$
(21)

This multidimensional integral is evaluated in Appendix A, where we show that

$F_{s_{k\bar{k}}}(x)=\sum_{i=1}^{M}\frac{(\lambda_{i}x-\sigma_{i}^{k\bar{k}})^{M-1}\tilde{u}(\lambda_{i}x-\sigma_{i}^{k\bar{k}})}{\Pi_{j=1,j\neq
i}^{M}[(\sigma_{j}^{k\bar{k}}-\sigma_{i}^{k\bar{k}})-(\lambda_{j}-\lambda_{i})x]}.$
(22)

Here $\sigma_{i}^{k\bar{k}}$ is the $i^{th}$ diagonal element in matrix
${{\bf\Sigma}_{k\bar{k}}}$ and it is given by

$\sigma_{i}^{k\bar{k}}=\left\\{\begin{array}[]{l@{\quad\quad}l}\sqrt{\frac{\lambda_{k}}{\lambda_{\bar{k}}}},&{\rm
for\leavevmode\nobreak\ \leavevmode\nobreak\ }i=k\\\
\sqrt{\frac{\lambda_{\bar{k}}}{\lambda_{k}}},&{\rm for\leavevmode\nobreak\
\leavevmode\nobreak\ }i=\bar{k}\\\ 0,&{\rm otherwise}.\end{array}\right.$ (23)

The CDF of $s_{k}$, denoted by $F_{s_{k}}(x)$, can be derived using the same
approach and is found to be the same expression as given in (22) with
$\sigma_{i}^{k\bar{k}}$ set to 1 for $i=k$ and 0 otherwise. Thus,
$F_{s_{k}}(x)$ can be shown to be

$F_{s_{k}}(x)=\frac{\left(\lambda_{k}x-1\right)^{M-1}\tilde{u}\left(\lambda_{k}x-1\right)}{\Pi_{j=1,j\neq
k}^{M}\left[-1-(\lambda_{j}-\lambda_{k})x\right]}+\sum_{i=1,i\neq
k}^{M}\frac{\lambda_{i}^{M-1}x^{M-1}\tilde{u}(\lambda_{i}x)}{\left[1-(\lambda_{k}-\lambda_{i})x\right]\Pi_{j=1,j\neq
k,i}^{M}[(\lambda_{i}-\lambda_{j})x]}.$ (24)

###  IV-B Moments of $s_{k}$

From (13), it is easy to see that $s_{k}$ is a positive random variable whose
support is the interval $\left[0,\frac{1}{\lambda_{k}}\right]$. Thus, by
employing integration, the first moment of $s_{k}$ can be evaluated as

$E[s_{k}]=\int_{0}^{\infty}\left(1-F_{s_{k}}(x)\right)dx=\int_{0}^{\frac{1}{\lambda_{k}}}\left(1-F_{s_{k}}(x)\right).$
(25)

Using (22) and (25) and applying partial fraction expansion, we can show after
tedious but straight forward algebraic manipulations that

$E[s_{k}]=\frac{1}{\lambda_{k}}-\sum_{i=1,i\neq
k}^{M}p_{i}\left(\frac{1}{\lambda_{k}}-\frac{\mbox{ln}\left(\lambda_{ik}\right)}{(\lambda_{i}-\lambda_{k})}\right),$
(26)

where $\mbox{ln}(.)$ represents the natural logarithm while $\lambda_{ij}$ and
$p_{i}$ are defined as

$\lambda_{ij}\stackrel{{\scriptstyle\triangle}}{{=}}\frac{\lambda_{i}}{\lambda_{j}},\forall\leavevmode\nobreak\
i,j\leavevmode\nobreak\ \leavevmode\nobreak\ \leavevmode\nobreak\
\mbox{and}\leavevmode\nobreak\ \leavevmode\nobreak\ \leavevmode\nobreak\
p_{i}\stackrel{{\scriptstyle\triangle}}{{=}}\frac{\lambda_{i}^{M-1}}{\Pi_{j=1,j\neq
i}^{M}(\lambda_{i}-\lambda_{j})},\forall\leavevmode\nobreak\ i.$ (27)

Now, observe that $\sum_{i=1}^{M}p_{i}=1$. Thus, we can use $1-\sum_{i=1,i\neq
k}^{M}p_{i}=p_{k}$. As a result, the expression for $E[s_{k}]$ in (26) is
simplified to

$E[s_{k}]=\frac{p_{k}}{\lambda_{k}}+\sum_{i=1,i\neq
k}^{M}p_{i}\frac{\mbox{ln}\left(\lambda_{ik}\right)}{(\lambda_{i}-\lambda_{k})}.$
(28)

In a similar manner, we can express the second moment of $s_{k}$ as

$E[s^{2}_{k}]=\int_{0}^{\frac{1}{\lambda_{k}}}2x\left(1-F_{s_{k}}(x)\right)dx.$
(29)

Thus, together with CDF expression in (22), we get the following expression

$E[s_{k}^{2}]=\frac{1}{\lambda_{k}^{2}}-\sum_{i=1,i\neq
k}^{M}p_{i}\left(\frac{1}{\lambda_{k}^{2}}-\frac{2}{\lambda_{k}(\lambda_{i}-\lambda_{k})}+\frac{2\mbox{ln}\left(\lambda_{ik}\right)}{(\lambda_{i}-\lambda_{k})^{2}}\right).$
(30)

Finally, by using $1-\sum_{i=1,i\neq k}^{M}p_{i}=p_{k}$, we find

$E[s_{k}^{2}]=\frac{p_{k}}{\lambda_{k}^{2}}+\sum_{i=1,i\neq
k}^{M}\frac{2p_{i}}{\lambda_{k}(\lambda_{i}-\lambda_{k})}-\sum_{i=1,i\neq
k}^{M}\frac{2p_{i}\mbox{ln}\left(\lambda_{ik}\right)}{(\lambda_{i}-\lambda_{k})^{2}}.$
(31)

###  IV-C Second Moment of $s_{k\bar{k}}$

We only need the second moment of $s_{k\bar{k}}$. We evaluate it using a
similar approach that was used to evaluate the second moment of $s_{k}$.
Specifically, we use the fact that $s_{k\bar{k}}$ has support over
$\left[0,\frac{1}{\sqrt{\lambda_{k}\lambda_{\bar{k}}}}\right]$. Thus, after
some tedious algebraic manipulations the second moment of $s_{k\bar{k}}$ can
be shown to be

$\displaystyle E[s_{k\bar{k}}^{2}]$ $\displaystyle=$
$\displaystyle\int_{0}^{\frac{1}{\sqrt{\lambda_{k}\lambda_{\bar{k}}}}}2x\left(1-F_{s_{k\bar{k}}}(x)\right)dx,$
(32) $\displaystyle=$
$\displaystyle\frac{p_{k}}{\lambda_{k}\lambda_{\bar{k}}}-\sum_{i=1,i\neq
k,\bar{k}}^{M}p_{i}\Bigg{(}\frac{2c_{ki}+2c_{\bar{k}i}}{\sqrt{\lambda_{k}\lambda_{\bar{k}}}}+\mbox{ln}\left(\lambda_{ki}\right)^{2c_{ki}\bar{\sigma}_{ki}}+\mbox{ln}\left(\lambda_{\bar{k}i}\right)^{2c_{\bar{k}i}\bar{\sigma}_{\bar{k}i}}\Bigg{)},$

where $\bar{\sigma}_{ji}$, $c_{k}$ and $c_{\bar{k}i}$ are defined as

$\bar{\sigma}_{ji}=\frac{\sigma_{j}^{k\bar{k}}}{(\lambda_{i}-\lambda_{j})},\leavevmode\nobreak\
\leavevmode\nobreak\
c_{ki}=\frac{(-\bar{\sigma}_{ki})^{M-1}}{(\bar{\sigma}_{\bar{k}i}-\bar{\sigma}_{ki})}\leavevmode\nobreak\
\leavevmode\nobreak\ \mbox{and}\leavevmode\nobreak\ \leavevmode\nobreak\
c_{\bar{k}i}=\frac{(-\bar{\sigma}_{\bar{k}i})^{M-1}}{(\bar{\sigma}_{ki}-\bar{\sigma}_{\bar{k}i})}.$
(33)

Thus, using the expression for $\bar{\sigma}_{ji}$, the expressions for
$c_{k}$ and $c_{\bar{k}i}$ can be reformulated as

$c_{ki}=\frac{(-1)^{M-1}\lambda_{k\bar{k}}^{(M-2)/2}}{(\lambda_{i}-\lambda_{k})^{M-2}\left[1-\frac{\lambda_{\bar{k}k}^{2}(\lambda_{i}-\lambda_{k})}{(\lambda_{i}-\lambda_{\bar{k}})}\right]},\leavevmode\nobreak\
\leavevmode\nobreak\ \leavevmode\nobreak\ \mbox{and}\leavevmode\nobreak\
\leavevmode\nobreak\ \leavevmode\nobreak\
c_{\bar{k}i}=\frac{(-1)^{M-1}\lambda_{\bar{k}k}^{(M-2)/2}}{(\lambda_{i}-\lambda_{\bar{k}})^{M-2}\left[1-\frac{\lambda_{k\bar{k}}^{2}(\lambda_{i}-\lambda_{\bar{k}})}{(\lambda_{i}-\lambda_{k})}\right]}.$
(34)

Finally, by utilizing the above expressions, we can express
$E[s_{k\bar{k}}^{2}]$ as

$\displaystyle E[s_{k\bar{k}}^{2}]$ $\displaystyle=$
$\displaystyle\frac{p_{k}}{\lambda_{k}\lambda_{\bar{k}}}-\frac{2(-1)^{M-1}\lambda_{k\bar{k}}^{(M-2)/2}}{\sqrt{\lambda_{k}\lambda_{\bar{k}}}}\Bigg{\\{}\sum_{i=1,i\neq
k,\bar{k}}^{M}\frac{p_{i}(1+\mbox{ln}\left(\lambda_{ki}\right))}{(\lambda_{i}-\lambda_{k})^{M-2}\left[1-\frac{\lambda_{\bar{k}k}^{2}(\lambda_{i}-\lambda_{k})}{(\lambda_{i}-\lambda_{\bar{k}})}\right]}$
(35) $\displaystyle\hskip 113.81102pt+\sum_{i=1,i\neq
k,\bar{k}}^{M}\frac{p_{i}(1+\mbox{ln}\left(\lambda_{\bar{k}i}\right))}{(\lambda_{i}-\lambda_{\bar{k}})^{M-2}\left[1-\frac{\lambda_{k\bar{k}}^{2}(\lambda_{i}-\lambda_{\bar{k}})}{(\lambda_{i}-\lambda_{k})}\right]}\Bigg{\\}}.$

###  IV-D The pdf and second moment of $r$

Consider the random variable $r$ defined in (16). Its CDF can be evaluated
using the approach outlined above for the CDF of $s_{k}$ and $s_{k\bar{k}}$
and is found to be (derivation is omitted for brevity)

$F_{r}(x)=\sum_{m=1}^{M}\frac{\lambda_{m}^{M}}{|\mbox{\boldmath$\Lambda$}|\Pi_{i=1,i\neq
m}^{M}\left(\lambda_{mi}-1\right)}e^{\frac{-1}{\lambda_{m}x}}\leavevmode\nobreak\
\tilde{u}(x).$ (36)

Consequently, the pdf of $r$ is given by

$p_{r}(x)=\sum_{m=1}^{M}\frac{\lambda_{m}^{M-1}}{x^{2}|\mbox{\boldmath$\Lambda$}|\Pi_{i=1,i\neq
m}^{M}\left(\lambda_{mi}-1\right)}e^{\frac{-1}{\lambda_{m}x}}.$ (37)

We can use the above pdf to show that

$\displaystyle E[r^{2}]$ $\displaystyle=$
$\displaystyle\sum_{m=1}^{M}\frac{\lambda_{m}^{M-1}}{|\mbox{\boldmath$\Lambda$}|\Pi_{i=1,i\neq
m}^{M}\left(\lambda_{mi}-1\right)}\int_{0}^{\infty}\frac{e^{\frac{-1}{\lambda_{m}x}}}{x^{2}}dx=\sum_{m=1}^{M}\frac{\lambda_{m}^{M}}{|\mbox{\boldmath$\Lambda$}|\Pi_{i=1,i\neq
m}^{M}\left(\lambda_{mi}-1\right)}.$ (38)

###  IV-E The pdf and second moment of $z_{k}$

The second moment of $z_{k}$ is evaluated in this section by first deriving
its pdf. However, we cannot derive the pdf of $z_{k}$ directly and so we
derive the conditional pdf of $z_{k}$ conditioned on $a_{k}$ defined as

$a_{k}=\sum_{m=1,m\neq k}^{M}|u(m)|^{2}$ (39)

Thus, we can rewrite $z_{k}$ as

$z_{k}=\frac{(1/\lambda_{k})|u(k)|^{2}+1}{|u(k)|^{2}+a_{k}}=\frac{||{\bf
u}||^{2}_{\bar{\bf H}_{k}}+1}{||{\bf u}||^{2}_{{\bf H}_{k}}+a_{k}},$ (40)

where $\bar{\bf H}_{k}$ and ${\bf H}_{k}$ are the $M\times M$ matrices with
all elements set to 0 except the $k^{th}$ element on the diagonal which is set
to $\frac{1}{\lambda_{k}}$ and 1, respectively. By applying an approach
similar to the one used with $s_{k}$, we can show that

$f_{z_{k}|a_{k}}(x)=\left[\frac{a_{k}}{(\lambda_{k}x-1)}+\frac{\lambda_{k}(1-a_{k}x)}{(\lambda_{k}x-1)^{2}}\right]e^{\frac{-(1-a_{k}x)}{(\lambda_{k}x-1)}}\leavevmode\nobreak\
\left[\tilde{u}\left(x-\frac{1}{\lambda_{k}}\right)-\tilde{u}\left(x-\frac{1}{a_{k}}\right)\right],$
(41)

which allows us to evaluate the conditional moment $E[z_{k}^{2}|a_{k}]$ as

$E[z_{k}^{2}|a_{k}]=\int_{0}^{\infty}x^{2}f_{z_{k}|a_{k}}(x)dx=\int_{\frac{1}{\lambda_{k}}}^{\frac{1}{a_{k}}}x^{2}\frac{(\lambda_{k}-a_{k})}{(\lambda_{k}x-1)^{2}}e^{\frac{-(1-a_{k}x)}{(\lambda_{k}x-1)}}dx.$
(42)

Here, we have utilized the fact that the support of $z_{k}$ is between
$\mbox{min}\left(\frac{1}{\lambda_{k}},\frac{1}{a_{k}}\right)$ and
$\mbox{max}\left(\frac{1}{\lambda_{k}},\frac{1}{a_{k}}\right)$. Now, by
applying change of variable and using partial fraction expansion, the above
integral is found to be

$E[z_{k}^{2}|a_{k}]=\frac{1}{\lambda_{k}^{2}}+\frac{2(\lambda_{k}-a_{k})}{\lambda_{k}^{3}}\leavevmode\nobreak\
e^{\frac{a_{k}}{\lambda_{k}}}\leavevmode\nobreak\
\Gamma\left(0,\frac{a_{k}}{\lambda_{k}}\right)+\frac{(\lambda_{k}-a_{k})^{2}}{\lambda_{k}^{4}}\leavevmode\nobreak\
e^{\frac{a_{k}}{\lambda_{k}}}\leavevmode\nobreak\
\Gamma\left(-1,\frac{a_{k}}{\lambda_{k}}\right),$ (43)

where
$\Gamma(\alpha,x)\stackrel{{\scriptstyle\triangle}}{{=}}\int_{x}^{\infty}t^{\alpha-1}e^{-t}dt$
is the Incomplete Gamma function. The unconditional moment $E[z_{k}^{2}]$ is
obtained by averaging the conditional moment $E[z_{k}^{2}|a_{k}]$ over the pdf
of $a_{k}$. The pdf of $a_{k}$ can be obtained using the approach of random
variable $r$ and is found to be

$f_{a_{k}}(a_{k})=\frac{\lambda_{k}}{|\mbox{\boldmath$\Lambda$}|}\sum_{m=1,m\neq
k}^{M}\frac{e^{-\frac{a_{k}}{\lambda_{m}}}}{\Pi_{l=1,l\neq
k,m}^{M}\left(\frac{1}{\lambda_{l}}-\frac{1}{\lambda_{m}}\right)}.$ (44)

Thus, by using (43) and (44), the moment $E[z_{k}^{2}]$ is found to be

$\displaystyle E[z_{k}^{2}]$ $\displaystyle=\sum_{m=1,m\neq
k}^{M}\frac{\mbox{ln}(\lambda_{m})}{|\mbox{\boldmath$\Lambda$}|\Pi_{l=1,l\neq
k,m}^{M}\left(\frac{1}{\lambda_{l}}-\frac{1}{\lambda_{m}}\right)}$
$\displaystyle+\sum_{m=1,m\neq
k}^{M}\frac{\lambda_{m}\Big{(}1+_{2}F_{1}\left(1,1;2;\eta_{mk}\right)-\leavevmode\nobreak\
_{2}F_{1}\left(1,1;3;\eta_{mk}\right)\Big{)}}{\lambda_{k}|\mbox{\boldmath$\Lambda$}|\Pi_{l=1,l\neq
k,m}^{M}\left(\frac{1}{\lambda_{l}}-\frac{1}{\lambda_{m}}\right)}$
$\displaystyle+\sum_{m=1,m\neq
k}^{M}\frac{\lambda_{m}^{2}}{\lambda_{k}^{2}|\mbox{\boldmath$\Lambda$}|\Pi_{l=1,l\neq
k,m}^{M}\left(\frac{1}{\lambda_{l}}-\frac{1}{\lambda_{m}}\right)}\left(\frac{1}{3}\leavevmode\nobreak\
_{2}F_{1}\left(1,2;4;\eta_{mk}\right)-\leavevmode\nobreak\
_{2}F_{1}\left(1,2;3;\eta_{mk}\right)\right),$ (45)

where $\eta_{mk}=1-\lambda_{mk}$ and $\leavevmode\nobreak\
{}_{2}F_{1}\left(\alpha,\beta;\gamma;x\right)$ is the Hypergeometric Function
defined as

$\leavevmode\nobreak\
_{2}F_{1}\left(\alpha,\beta;\gamma;x\right)\stackrel{{\scriptstyle\triangle}}{{=}}\frac{1}{B(\beta,\gamma-\beta)}\int_{0}^{1}x^{\beta-1}(1-x)^{\gamma-\beta-1}(1-xz)^{-\alpha}dx,\leavevmode\nobreak\
\leavevmode\nobreak\ \mbox{Re}(\gamma)>\mbox{Re}(\beta)>0,$ (46)

and $B(x,y)$ is the Beta Function defined as

$B(x,y)\stackrel{{\scriptstyle\triangle}}{{=}}\int_{0}^{1}t^{x-1}(1-t)^{y-1}dt,\leavevmode\nobreak\
\leavevmode\nobreak\ \leavevmode\nobreak\ \leavevmode\nobreak\
\leavevmode\nobreak\ \leavevmode\nobreak\ \leavevmode\nobreak\
\leavevmode\nobreak\ \mbox{Re}(x)>0,\leavevmode\nobreak\ \leavevmode\nobreak\
\mbox{Re}(y)>0.$ (47)

##  V Simulation Results

In this section, the performance analysis of the NLMS algorithm is
investigated for an unknown system identification problem. The system noise is
a zero mean i.i.d. sequence with variance 0.01 which sets the SNR to 20 dB.
Throughout the simulation, the adaptive filter used has the same length as
that of the unknown system. The optimal weight vector is
${\bf{w}^{o}}=[0.227,\leavevmode\nobreak\ 0.460,\leavevmode\nobreak\
0.688,\leavevmode\nobreak\ 0.460,\leavevmode\nobreak\ 0.227]^{T}$ as we assume
${\mathbf{q}}_{i}={\mathbf{0}},\leavevmode\nobreak\
\forall\leavevmode\nobreak\ i$. The input to the adaptive filter and unknown
system is correlated complex Gaussian input which is generated with
correlation matrix with entries ${\bf R}(i,j)=\alpha_{c}^{|i-j|}$ with
correlation factor555The case $\alpha_{c}=0$ corresponds to the white case
while $\alpha_{c}=1$ corresponds to the fully correlated case $\alpha_{c}$
($0<\alpha_{c}<1$). The numerical results are averaged over $100$ independent
runs. The objective of our simulations is to validate the derived analytical
results for both steady-state and transient analysis. In order to validate the
derived analytical result for the transient behavior, the MSE of the NLMS
algorithm is analyzed in Fig. 1 for two different values of step-size which
are 0.1 and 0.01. The value of correlation factor $\alpha_{c}$ is set to 0.5.
It can be easily seen that the results validate our theoretical findings for
both step-sizes.

Figure 1: Analytical and simulation results for the MSE learning curves of the
NLMS algorithm for $\alpha_{c}=0.5$.

##  VI Conclusion

We analyzed the NLMS adaptive filter driven by correlated circularly symmetric
Gaussian input. The paper demonstrates that the MSE performance can be
articulated in terms of the moments of ratios of quadratic forms in isotropic
random variables. The CDFs of these ratios then obtained using novel complex
integration techniques, which are then used to evaluate the corresponding
moments in closed form expressions. Our MSE results apply to the transient,
stead-state, and tracking results. Our proposed approach for the analysis of
the NLMS could be extended other normalized adaptive filters (e.g. Recursive
Least Square (RLS) and affine projection algorithms).

## Appendix A: Evaluating the CDF of $s_{k\bar{k}}$

In order to evaluate the integral in (21), we utilize the following integral
representations of the step and the delta functions [14]

$\tilde{u}(x)=\frac{1}{2\pi}\int_{-\infty}^{\infty}\frac{e^{x(j\omega+\beta)}}{(j\omega+\beta)}d\omega\leavevmode\nobreak\
\leavevmode\nobreak\ \mbox{and}\leavevmode\nobreak\ \leavevmode\nobreak\
\delta(x)=\frac{1}{2\pi}\int_{-\infty}^{\infty}e^{x(\alpha+j\omega)}d\omega,$
(48)

These are valid for any $\alpha,\leavevmode\nobreak\ \beta>0$ which are free
parameters that we can conveniently choose [15]. After replacing the delta and
the step functions with their equivalent integral representations, the pdf
$p({\mbox{\boldmath$\phi$}})$ and
$\tilde{u}(\|{\mbox{\boldmath$\phi$}}\|^{2}_{x{\bf\Lambda}-{{\bf\Sigma}_{k\bar{k}}}})$
in (21) can be rewritten as

$\displaystyle p({\mbox{\boldmath$\phi$}})$
$\displaystyle=\frac{\Gamma(M)}{2\pi^{M+1}}\int_{-\infty}^{\infty}e^{(\|{\mbox{\boldmath$\phi$}}\|^{2}-1)(\alpha+j\omega)}d\omega,$
(49)

and

$\displaystyle\tilde{u}(\|{\mbox{\boldmath$\phi$}}\|^{2}_{x{\bf\Lambda}-{{\bf\Sigma}_{k\bar{k}}}})$
$\displaystyle=\frac{1}{2\pi}\int_{-\infty}^{\infty}\frac{e^{(\|{\mbox{\boldmath$\phi$}}\|^{2}_{x{\bf\Lambda}-{{\bf\Sigma}_{k\bar{k}}}})(j\omega+\beta)}}{(j\omega+\beta)}d\omega,$
(50)

which allows us to set up the CDF of $s_{k\bar{k}}$ in (21) as

$F_{s_{k\bar{k}}}(x)=\frac{\Gamma(M)}{4\pi^{M+2}}\leavevmode\nobreak\
e^{-\alpha}\int_{-\infty}^{\infty}\int_{-\infty}^{\infty}\int_{-\infty}^{\infty}e^{-{\mbox{\boldmath$\phi$}}^{*}(-\alpha{\bf
I}+({{\bf\Sigma}_{k\bar{k}}}-x{\bf\Lambda})(j\omega_{1}+\beta)-j\omega_{2}{\bf
I}){\mbox{\boldmath$\phi$}}}d{\mbox{\boldmath$\phi$}}\leavevmode\nobreak\
e^{-j\omega_{2}}d\omega_{2}\frac{1}{j\omega_{1}+\beta}d\omega_{1}.$ (51)

Next, we first focus on the inner integral

$\int_{-\infty}^{\infty}e^{-{\mbox{\boldmath$\phi$}}^{*}(-\alpha{\bf
I}+({{\bf\Sigma}_{k\bar{k}}}-x{\bf\Lambda})(j\omega_{1}+\beta)-j\omega_{2}{\bf
I}){\mbox{\boldmath$\phi$}}}d{\mbox{\boldmath$\phi$}}.$ (52)

By inspecting the above, we note that it is similar to the Gaussian density
integral with a covariance $\Sigma_{c}$ given by

$\Sigma_{c}=(-\alpha{\bf
I}+({{\bf\Sigma}_{k\bar{k}}}-x{\bf\Lambda})(j\omega_{1}+\beta)-j\omega_{2}{\bf
I})^{-1}.$ (53)

Note that $\Sigma_{c}$ is complex. Hence, $\alpha$ should be chosen to make
the real part of $\Sigma_{c}$ positive definite. Thankfully, the final result
will not depend on the value of $\alpha$ we choose. Here, we are just making
an analogy to the Gaussian integral (see [16] for a formal proof) which gives

$\frac{1}{\pi^{M}}\int_{-\infty}^{\infty}e^{-{\mbox{\boldmath$\phi$}}^{*}(-\alpha{\bf
I}+({{\bf\Sigma}_{k\bar{k}}}-x{\bf\Lambda})(j\omega_{1}+\beta)-j\omega_{2}{\bf
I}){\mbox{\boldmath$\phi$}}}d{\mbox{\boldmath$\phi$}}=\frac{1}{\Big{|}-\alpha{\bf
I}+({{\bf\Sigma}_{k\bar{k}}}-x{\bf\Lambda})(j\omega_{1}+\beta)-j\omega_{2}{\bf
I}\Big{|}}.$ (54)

Consequently, the CDF will take the following form

$F_{s_{k\bar{k}}}(x)=\frac{\Gamma(M)}{4\pi^{2}}\leavevmode\nobreak\
e^{-\alpha}\int_{-\infty}^{\infty}\int_{-\infty}^{\infty}\frac{e^{-j\omega_{2}}}{\Big{|}-\alpha{\bf
I}+({{\bf\Sigma}_{k\bar{k}}}-x{\bf\Lambda})(j\omega_{1}+\beta)-j\omega_{2}{\bf
I}\Big{|}}d\omega_{2}\leavevmode\nobreak\
\frac{1}{(j\omega_{1}+\beta)}d\omega_{1}.$ (55)

At this stage, we focus on the second inner integral with respect to
$\omega_{2}$. To evaluate this integral, we use partial fraction expansion to
represent the determinant as

$\displaystyle\frac{1}{\Pi_{i=1}^{M}(-\alpha+(\sigma_{i}^{k\bar{k}}-\lambda_{i}x)(j\omega_{1}+\beta)-j\omega_{2})}$
$\displaystyle\leavevmode\nobreak\ \leavevmode\nobreak\ \leavevmode\nobreak\
\leavevmode\nobreak\ \leavevmode\nobreak\ \leavevmode\nobreak\
\leavevmode\nobreak\ \leavevmode\nobreak\ \leavevmode\nobreak\
\leavevmode\nobreak\ \leavevmode\nobreak\ \leavevmode\nobreak\
\leavevmode\nobreak\ \leavevmode\nobreak\ \leavevmode\nobreak\
\leavevmode\nobreak\ \leavevmode\nobreak\ \leavevmode\nobreak\
\leavevmode\nobreak\ \leavevmode\nobreak\ \leavevmode\nobreak\
\leavevmode\nobreak\ \leavevmode\nobreak\ \leavevmode\nobreak\
=\frac{1}{(j\omega_{1}+\beta)^{M-1}}\sum_{i=1}^{M}\frac{\eta_{i}}{(-\alpha+(\sigma_{i}^{k\bar{k}}-\lambda_{i}x)(j\omega_{1}+\beta)-j\omega_{2})},$
(56)

where constant $\eta_{i}$ is given by

$\eta_{i}=\frac{1}{\Pi_{j=1,j\neq
i}^{M}[(\sigma_{j}^{k\bar{k}}-\sigma_{i}^{k\bar{k}})-(\lambda_{j}-\lambda_{i})x]},$
(57)

and $\sigma_{i}^{k\bar{k}}$ is defined in (23). We can now use residue theory
to evaluate the integral with respect to $\omega_{2}$. Specifically, we use
the following integral solutions [15]

$\displaystyle\int_{-\infty}^{\infty}(\beta+ix)^{-\nu}e^{-ipx}dx=\frac{2\pi(-p)^{\nu-1}e^{\beta
p}}{\Gamma(\nu)}\leavevmode\nobreak\ \tilde{u}(-p),$ (58)

and

$\displaystyle\int_{-\infty}^{\infty}(\beta-ix)^{-\nu}e^{-ipx}dx=\frac{2\pi
p^{\nu-1}e^{-\beta p}}{\Gamma(\nu)}\leavevmode\nobreak\ \tilde{u}(p),$ (59)

which is valid for $\mbox{Re}(\nu)>0$ and $\mbox{Re}(\beta)>0$. Thus, by
employing the above relations, solution of the integral with respect to
$\omega_{2}$ is found to be

$\frac{1}{2\pi}\int_{-\infty}^{\infty}\frac{e^{-j\omega_{2}}}{\Big{|}-\alpha{\bf
I}+({{\bf\Sigma}_{k\bar{k}}}-x{\bf\Lambda})(j\omega_{1}+\beta)-j\omega_{2}{\bf
I}\Big{|}}d\omega_{2}=\frac{1}{(j\omega_{1}+\beta)^{M-1}}\sum_{i=1}^{M}\eta_{i}e^{\alpha-(\sigma_{i}^{k\bar{k}}-\lambda_{i}x)(j\omega_{1}+\beta)},$
(60)

Eventually, the CDF of $s_{k\bar{k}}$ can be set up as follows

$\displaystyle F_{s_{k\bar{k}}}(x)$ $\displaystyle=$
$\displaystyle\frac{\Gamma(M)}{2\pi}\sum_{i=1}^{M}\eta_{i}\int_{-\infty}^{\infty}\frac{1}{(j\omega_{1}+\beta)^{M}}e^{-(\sigma_{i}^{k\bar{k}}-\lambda_{i}x)(j\omega_{1}+\beta)}d\omega_{1}$
(61)

Finally, after again using the residue theory and (57), the CDF of
$s_{k\bar{k}}$ given in (22) is found.

## References

  * [1] A. H. Sayed, Fundamentals of Adaptive Filtering, New York: Wiley-Interscience, 2003.
  * [2] J. I., Nagumo and A. Noda,  “A learning method for system identification,”  IEEE Transactions on Automatic Control, vol 12, pp. 282-287, 1967.
  * [3] T. Y. Al-Naffouri and A. H. Sayed,  “Transient analysis of data normalized adaptive filters,”  IEEE Transactions on Signal Processing, vol 51, No. 3, pp. 639-652, March, 2003.
  * [4] S. C. Douglas and T. H. Y. Meng,  “Normalized Data Nonlinearities for LMS Adaptation,”  IEEE Transactions on Signal Processing, vol 42, No. 6, pp. 1352-1365, June, 1994.
  * [5] G. Barrault, M. H. Costa, J. C. M. Bermudez and A. Lenzi,  “A new analytical model for the NLMS algorithm,”  Proc. IEEE ICASSP, vol. 4, pp. 41-44, March, 2005.
  * [6] E. M. Lobato, O. J. Tobias, and R. Seara,  “Stochastic model for the NLMS algorithm with correlated Gaussian data,”  Proc. IEEE ICASSP, vol. 3, pp. 760-763. 2006.
  * [7] M. H. Costa and J. C. M. Bermudaz,  “An improved model for the normalized LMS algorithm with gaussian inputs and large number of coefficients,”  Proc. IEEE ICASSP, vol. 2, pp. 1385-1388, 2002.
  * [8] D. T. M. Slock,  “On the convergence behavior of the LMS and the normalized LMS algorithms,”  IEEE Transactions on Signal Processing, vol 41, No. 9, pp. 2811-2825, Sept., 1993.
  * [9] A. Ali, M. Moinuddin, and T. Y. Al-Naffouri,  “The NLMS Is Steady-State Schur-Convex,”  IEEE Signal Processing Letters, vol. 28, pp. 389-393, 2021.
  * [10] M. Tarrab, and A. Feuer,  “Convergence and Performance Analysis of the Normalized LMS algorithm with Uncorrelated Gaussian Data,”  IEEE Transactions on Information Theory, vol 34, No. 4, pp. 680-691, July, 1988.
  * [11] T. Y. Al-Naffouri, M. Moinuddin, and M. S. Sohail,  “Mean Behavior of the NLMS Algorithm for Correlated Gaussian Inputs,”  IEEE Signal Processing Letters, vol. 18, Issue 1, pp 7-10, Jan. 2011.
  * [12] A. M. Mathai and S. B. Provost,  “Quadratic Forms in Random Variables,”  New York: Marcel Dekker, 1992.
  * [13] N. L. Johnson and S. Kotz,  “Continuous Univariate Distributions,”  New York: Houghton Mifflin, vol 2, 1970.
  * [14] B. Hassibi and T. L. Marzetta,  “Multiple-antennas and isotropically random unitary inputs: The received signal density in closed-form,”  IEEE Transactions on Information Theory, vol. 48, No. 6, pp. 1473-1484, June 2002.
  * [15] I. S. Gradshteyn, I. M. Ryzhik,  “Table of integrals, series, and products, corrected and enlarged edition”,  Academic Press, INC, New York, 1980.
  * [16] T. Y. Al-Naffouri and B. Hassibi,  “On the distribution of indefenite quadratic forms in Gaussian random variables,”  International Symposium on Information Theory (ISIT), South Korea, 2009.


instrumentation, and demonstrate how the Bounded-Horizon technique circumvents
the need for augmenting the program with such ghost code.

###  7.1. Implementation

We implemented a prototype of Bounded-Horizon of bound 1 on top of Z3 [DMB08]
and used it within Ivy [MP18] and the framework of [IBI+13].

Our implementation works by adding “guards” that restrict the range of
universal quantifiers to the set of constants where necessary. Technically,
recall that we are considering the satisfiability of
$\textit{Ind}={I}_{S}\land{\delta}_{S}\land{(\neg I^{\prime})}_{S}$.101010
Skolemization is performed via Z3, taking advantage of heuristics that reduce
the number of different Skolem functions. Let $\forall x.\ \theta$ be a
subformula of Ind. If $\theta$ contains function symbol applications111111
This in fact implements the approximation as of Equation 2. The exact bound 1
per Equation 1 can be implemented by a more careful consideration of which
universally quantified variables should be restricted, but this was not
necessary for our examples. , we transform the subformula to $\forall x.\
\bigl{(}\bigvee_{c}{x=c}\bigr{)}\rightarrow\theta$ where $c$ ranges over
$\mathop{\textrm{const}}[\textit{Ind}]$. The resulting formula is then
dispatched to the solver. This is a simple way to encode a bound of 1 on the
depth of instantiations performed (instead of trying instantiations of higher
and higher depth), while leaving room for the solver to perform the necessary
instantiations cleverly. The translation enlarges the formula by
$O(\text{\\#}\text{Consts}\cdot\text{\\#}\forall)$ although the number of
bounded instantiations grows exponentially with $\text{\\#}\forall$. The
exponential explosion is due to combinations of constants in the
instantiation, a problem we defer to the solver.

Our encoding restricts the constants necessary to decide satisfiability of the
formula while avoiding an exponential blowup in the translation. The task of
exploring the space of possible instantiations is left for Z3’s instantiation
heuristics. It not immediate, however, that Z3 is guaranteed to terminate on
the resultant formula, which syntactically does not fall into a decidable
class (despite of encoding bounded instantiations). Fortunately, employing
Model-Based Quantifier Instantiation [GM09], Z3 is guaranteed to terminate on
this formula, as desired. This is because during the Model-Based Quantifier
Instantiation process every instantiation of a universal formula has the same
truth value in the model as an instantiation using one of the existing ground
terms (constants and then $\textnormal{BHT}_{1}$ terms). Z3’s instantiation
engine produces instantiations using existing terms rather than create
superfluous new terms, and so must terminate on the formulas our procedure
produces [Bjø].

An alternative approach of implementation is to integrate the instantiation
bound with the solver’s heuristics more closely (see [BRK+15]). It would also
be interesting to efficiently integrate this approach with resolution based
first-order theorem-provers such as Vampire [KV13].

###  7.2. Examples

We applied the procedure to the incorrect examples of Section 6, and also
successfully verified several correct programs and invariants using bound 1.
These examples are (the examples’ code can be found in [add]):

  * •

The client-server example of Figure 4.

  * •

List reverse [IBI+13], where the invariant states that the $n$ edges (“next”
pointers) are reversed. The invariant is $\forall^{*}\exists^{*}$ due to the
encoding of $n$ via its (reflexive) transitive closure ${n^{*}}$ as explained
in [IBI+13].

  * •

Learning switch [BBG+14], in which the routing tables of the switches in the
network are automatically constructed through observing the source packets
arriving on each switch’s links. The invariant states that in every routing
path, every routing node has a successor.

  * •

Hole-punching firewall [BBG+14], in which the firewall allows a packet from an
external host to enter the network only if the host is recorded as trusted by
the firewall. The invariant states that if a packet from an external host then
is allowed, then there previously was an internal host that contacted the
external host. We explored two modeling alternatives: using a ghost history
relation, or existentially quantifying over time. We elaborate on this topic
and this example below.

  * •

Trusted chain, as explained in Section 6.

  * •

Leader election in a ring [CR79, PMP+16] with the invariant discussed in
Section 6. (See Section 6 for full details.)

##### Derived Relations Over the History

Sometimes expressing verification conditions requires modifications to the
program in which the state is augmented with additional relations, but these
relations cannot be defined as derived relations over the core program
relations. Often the reason is that the property of interest depends not only
on the current program state, but also on previous states in the execution
history. Such a scenario occurs in the example of the _hole-punching
firewall_. In this example, a firewall controls packets entering and leaving
the organization’s network. Packets from outside the organization are allowed
if they originate from a host that is considered trusted. A host
$\textit{host}_{o}$ is considered trusted if some host $\textit{host}_{i}$ in
the organization’s network has previously sent a packet to
$\textit{host}_{o}$. This correctness condition depends on previous states in
the execution history, and cannot be expressed in an inductive invariant
without changing the vocabulary.

A common method to overcome this problem is to introduce _ghost state_ to
record historical information, and _ghost code_ to mutate the ghost state,
implementing this book-keeping. In the hole-punching firewall example, the
user can add a relation $\textit{ever-
pending}(\textit{host}_{1},\textit{host}_{2})$, and add ghost code that adds
the tuple $(\textit{host}_{1},\textit{host}_{2})$ to ever-pending whenever
$\textit{host}_{1}$ sends a packet to $\textit{host}_{2}$.

We observe that it is sometimes possible to think of such ghost relations as
standard derived relations, defined over a vocabulary in which past states are
available, and view the procedure of adding appropriate ghost code as an
instrumentation by a derived relation as defined in this paper (Section 4.1).
The idea is as follows:

In our first-order setting, we can lift the vocabulary to encode the time
explicitly with a classical encoding (see e.g. [Aba89]), by adding a new
parameter $t$ to every relation and constant symbol. In the transition
relation, references to $p(\cdot)$ are replaced by $p(t_{\text{now}},\cdot)$
and $p^{\prime}(\cdot)$ by $p(t_{\text{now}}^{\prime},\cdot)$, where
$t_{\text{now}}$ is a new constant that represents the current time.
$t_{\text{now}}$ is incremented in every transition (according to some total
order on time). The transition relation also needs to include the requirement
that the previous states are not modified by the current transition, meaning
that $\forall t<t_{\text{now}}.\ \forall\overline{x}.\
p(t,\overline{x})\leftrightarrow p^{\prime}(t,\overline{x})$. Call this
modified transition relation $\delta_{t}$.

We now proceed to express the ghost relation as a derived relation over the
history. In the example of the hole-punching firewall, the relation ever-
pending can now be expressed by the derived relation
$\psi(\textit{host}_{1},\textit{host}_{2})\equiv\exists t.\ t\leq
t_{\text{now}}\land\textit{pending}(t,\textit{host}_{1},\textit{host}_{2})$.

With this construction, we can directly use the derived relation in the
inductive invariant instead of the ghost relation. Viewing the addition of the
ghost relation and ghost code as a sound instrumentation, Section 4.1 implies
that an inductive invariant for the program with ghost state induces an
inductive invariant for $\delta_{t}$. This invariant is defined over the
vocabulary that records the entire history, but without the ghost relation
symbol.

The value of this point of view is that the results of this paper imply that
in certain cases the user can prove an invariant expressed over the history
using bounded instantiations with a low bound, _without resorting to ghost
code manipulations_. The reasoning is as follows: If adding the ghost code
does not add existential quantifiers, then augmenting the program with the
ghost code can be thought of as instrumentation without additional
existentials. If, additionally, the derived relation — now defined over the
entire execution history — can be expressed as a combination of universal and
existential properties, Section 4.3 applies, showing that Bounded-Horizon with
a low-bound is guaranteed to prove the inductiveness of the invariant
expressed for $\delta_{t}$, with no need to add the ghost code.

These conditions are satisfied by the hole-punching firewall example. We
manually performed the transformation of the transition relation to a
vocabulary over the history in Ivy, and successfully proved the inductive
invariant with Bounded-Horizon of bound 1.

###  7.3. Evaluation

In this section, we attempt to answer the following questions regarding the
applicability of Bounded-Horizon of bound 1:

  * •

Is the method sufficiently powerful to prove correct inductive invariants of
interesting programs? (Section 7.3.1)

  * •

Can our implementation achieve quick termination (with a partial
counterexample) when standard (complete) methods diverge due to an infinite
counterexample? (Section 7.3.2)

  * •

Is the overhead associated with Bounded-Horizon on correct invariants
reasonable compared to a baseline implementation (which does not bound
instantiation a-priori)? (Section 7.3.3)

Section 7.3 compares the running time of our implementation of Bounded-Horizon
of bound 1 with Z3 as a baseline. “—” means the solver did not terminate in a
60 seconds timeout. We elaborate on each of the questions referring to the
results of this table.

[ht] Experimental results. Program #$\forall$ #Func #Consts
#$\forall^{\downarrow}$ B1 Total B1 Solve Baseline Z3 Client-server 14 1 15 2
58 ms 3 ms 3 ms List reverse 47 3 15 4 319 ms 211 ms 50 ms Learning switch 70
1 7 37 2004 ms 83 ms 91 ms Hole-punching firewall with ghost 15 1 18 3 354 ms
14 ms 14 ms Hole-punching firewall $\exists$ time 32 2 21 3 485 ms 14 ms 14 ms
Trusted chain (correct) 27 1 19 2 435 ms 30 ms 37 ms Leader-election in a ring
(correct) 41 1 21 1 517 ms 33 ms 47 ms Trusted chain (incorrect) 23 15 1 2 393
ms 95 ms — Leader-election in a ring (incorrect) 40 1 20 1 899 ms 417 ms — •
B1 Total is the time in milliseconds for the bound 1 implementation. It is
compared to Baseline Z3 which is the solving time in milliseconds of Ind as is
(with quantifier alternation) by Z3. “—” means the solver did not terminate in
a 60 seconds timeout. B1 Solve measures the solving time of the formula
restricted to bound 1, which demonstrates that most of the overhead occurs
when constructing the formula. #$\forall$ is the number of universal
quantifiers in Ind, #Func the number of different Skolem function symbols, and
#Consts the number of constants. #$\forall^{\downarrow}$ is the number of
universally quantified variables that were restricted in the bound 1 check.
Measurements were performed on a Linux 4.15.0 VM running on a 2.9GHz Intel
i7-7500U CPU, except for client-server and list reverse which were measured on
a 3.5GHz Intel i5-4690 CPU with 8GB RAM running Linux 3.13 x86_64.

##### Summary of Results.

The results are encouraging because they suggest that the termination strategy
of Bounded-Horizon, at least for bound 1, can be combined with existing
instantiation techniques to ensure termination with only a slight performance
penalty. Bounded-Horizon successfully terminating on incorrect examples with a
partial example suggests that the Bounded-Horizon termination criterion may
indeed be useful for “sat” instances on which the solver may diverge.

####  7.3.1. Bound 1 Suffices for Interesting Programs and Invariants

Bound 1 successfully proves the invariant inductive in all correct examples
list in Section 7.3. This demonstrates in practice the power of bounded
instantiations shown theoretically in Section 4.

####  7.3.2. Bound 1 Terminates on Incorrect Invariants

In this section we consider the incorrect invariants of leader election
termination in a ring and trusted chain, outlined in Section 6. On these
examples, our encoding of bounded instantiations allowed Z3 to terminates in
seconds. In contrast, baseline Z3 does not converge in 60 seconds on either of
these examples. The same happens with the first-order theorem prover Vampire
[KV13], invoked on an SMTLIB2 translation of the verification condition. This
demonstrates that the encoding of bounded instantiations outlined in Section
7.1 allows Z3 to terminate efficiently, although to do so the solver must in
theory exhaust all possible bounded instantiations.

####  7.3.3. Bound 1 Has Reasonable Overhead

In this section we consider the correct invariants in Section 7.3. Both
Bounded-Horizon and baseline Z3 successfully prove these inductive correct.
Bounded-Horizon of bound 1 introduces an overhead in this computation; this is
to be expected since the chief benefit of our approach is the termination
guarantee on incorrect examples. We deem this overhead a reasonable price to
ensure termination (in general the user does not know in advance whether the
invariant is inductive or not before querying the solver). Comparing the
columns B1 Total and B1 Solve with Baseline Z3 in Section 7.3, it is apparent
that most of the overhead is due to the transformation of the formula before
it is sent to the solver, which may be improved by further engineering.

##  8\. Related Work

##### Quantifier Instantiation

The importance of formulas with quantifier-alternation for program
verification has led to many developments in the SMT and theorem-proving
communities that aim to allow automated reasoning with such formulas. The
Simplify system [DNS05] promoted the practical usage of quantifier triggers,
which let the user affect the quantifier instantiation procedure in a clever
way. Similar methods are integrated into modern SMT solvers such as Z3
[DMB08]. Recently, a method for annotating the source code with triggers has
been developed for Dafny [LP16]. The notion of instantiation depth is related
to the notions of matching-depth [DNS05] and instantiation-level [GBT09] which
are used for prioritization within the trigger-based instantiation procedure.

In addition to user-provided triggers, many automated heuristics for
quantifier instantiation have been developed, such as Model-Based Quantifier
Instantiation [GM09]. Even when quantifier instantiation is refutation-
complete, it is still important and challenging to handle the SAT cases, which
are especially important for program verification. Accordingly, many works
(e.g., [RTGK13]) consider the problem of model finding.

Local Theory Extensions and Psi-Local Theories [Sof05, IJS08, BRK+15] identify
settings in which limited quantifier instantiations are complete. They show
that completeness is achieved exactly when every partial model can be extended
to a (total) model. In such settings Bounded-Horizon instantiations are
complete for invariant checking. However, Bounded-Horizon can also be useful
when completeness cannot be guaranteed.

Classes of SMT formulas that are decidable by complete instantiations have
been studied by [GM09]. In the uninterpreted fragment, a refined version of
Herbrand’s Theorem generates a finite set of instantiations when the
dependencies are stratified. Bounded-Horizon is a way to bound unstratified
dependencies.

Finally, first-order theorem provers, such as Vampire [KV13] and SPASS
[Wei01], employ other proof techniques such as resolution. These techniques
are also prone to divergence on formulas with quantifier-alternation and in
general unable to generate infinite counterexamples.

##### Natural Proofs

Natural proofs [QGSM13] provide a sound and incomplete proof technique for
deductive verification. The key idea is to instantiate recursive definitions
over the terms appearing in the program. Bounded-Horizon is motivated by a
similar intuition, but focuses on instantiating quantifiers in a way that is
appropriate for the EPR setting.

##### Decidable Logics

Different decidable logics can be used to check inductive invariants. For
example, Monadic second-order logic [HJJ+95] obtains decidability by limiting
the underlying domain to consist of trees only, and in particular does not
allow arbitrary relations, which are useful to describe properties of
programs. There are also many decidable fragments of first-order logic
[BGG01]. Our work aims to transcend the class of invariants checkable by a
reduction to the decidable logic EPR. We note that the example of Section 6
does not fall under the Loosely-Guarded Fragment of first-order logic [Hod02]
due to a use of a transitivity axiom, and does not enjoy the finite-model
property.

##### Abstractions for verification of infinite-state systems

Our work is closely related to abstractions of infinite-state systems. These
abstractions aim at automatically inferring inductive invariants in a sound
way. We are interested in checking if a given invariant is inductive either
for automatic and semi-automatic verification.

The View-Abstraction approach [AHH13, AHH14, AHH15] defines a useful
abstraction for the verification of parameterized systems. This abstraction is
closely related to universally quantified invariants. An extension of this
approach [AHH14] adds contexts to the abstraction, which are used to capture
${\forall^{*}\exists^{*}}$ invariants in a restricted setting where nodes have
finite-state and are only related by specific topologies. Our work is in line
with the need to use ${\forall^{*}\exists^{*}}$ invariants for verification,
but applies in a more general setting (with unrestricted high-arity relations)
at the cost of losing completeness of invariant checking.

Our work is related to the TVLA system [LS00, SRW02] which allows the
programmers to define instrumentation relations. TVLA also employs finite
differencing to infer sound update code for updating instrumentation relations
[RSL10], but generates non-EPR formulas and does not guarantee completeness.
The focus operation in TVLA implements materialization which resembles
quantifier-instantiation. TVLA shows that very few built-in instrumentation
relations can be used to verify many different programs.

##### Instrumentation and Update Formulas

The idea of using instrumentation relations and generating update formulas is
not limited to TVLA and was also used for more predictable SMT verification
[LQ06, LQ08].

##### Instrumentation for Decidable Logics

The technique of instrumentation by derived relations to allow decidable
reasoning is further discussed in a recent work [PLSS17]. Several variants of
Paxos are proved safe using models in the decidable logic of EPR with
stratified functions, whose use is enabled by instrumentation. Efficiently
implementing a bounded instantiations scheme that bounds instantiations only
where they are unstratified is an interesting challenge, in hope of relieving
the need for instrumentation also for such cases.

##  9\. Conclusion

We have provided an initial study of the power of bounded instantiations for
tackling quantifier alternation. This paper shows that quantifier
instantiation with small bounds can simulate instrumentation. This is a step
in order to eliminate the need for instrumenting the program, which can be
error-prone. The other direction, i.e. simulating quantifier instantiation
with instrumentation, was also presented for conceptual purposes, although it
is less appealing from a practical point of view.

We are encouraged by our initial experience that shows that various protocols
can be proven with small instantiation bounds, and that partial models are
useful for understanding the failures of the solver to prove inductiveness.
Some of these failures correspond to non-inductive claims, especially those
due to infinite counterexamples. In the future we hope to leverage this in
effective deductive verification tools, and explore meaningful ways to display
infinite counterexamples to the user. Other interesting directions include
further investigation into the automation of program transformations for the
purpose of verification (of which instrumentation is an example), including
types of ghost code, and the use of Bounded-Horizon for automatically
inferring invariants with quantifier-alternation.

##### Acknowledgments.

We would like to thank Nikolaj Bjørner, Shachar Itzhaky, and Bryan Parno for
helpful discussions, Gilit Zohar-Oren for help and feedback, and the anonymous
referees whose comments have improved the paper. The research leading to these
results has received funding from the European Research Council under the
European Union’s Seventh Framework Programme (FP7/2007–2013) / ERC grant
agreement no [321174], and the European Union’s Horizon 2020 research and
innovation programme (grant agreement No [759102-SVIS]). This research was
partially supported by BSF grant no. 2012259, and by Len Blavatnik and the
Blavatnik Family foundation, the Blavatnik Interdisciplinary Cyber Research
Center, Tel Aviv University, the United States-Israel Binational Science
Foundation (BSF) grants No. 2016260 and 2012259, and the Israeli Science
Foundation (ISF) grant No. 2005/17.

## References

  * [Aba89] Martín Abadi.  The power of temporal proofs.  Theor. Comput. Sci., 65(1):35–83, June 1989.
  * [add] Full code materials.  http://www.cs.tau.ac.il/research/yotam.feldman/papers/tacas17/examples_code.zip.
  * [AHH13] Parosh Aziz Abdulla, Frédéric Haziza, and Lukás Holík.  All for the price of few.  In Verification, Model Checking, and Abstract Interpretation, 14th International Conference, VMCAI 2013, Rome, Italy, January 20-22, 2013\. Proceedings, pages 476–495, 2013.
  * [AHH14] Parosh Aziz Abdulla, Frédéric Haziza, and Lukáš Holík.  Block me if you can!  In International Static Analysis Symposium, pages 1–17. Springer, 2014.
  * [AHH15] Parosh Abdulla, Frédéric Haziza, and Lukáš Holík.  Parameterized verification through view abstraction.  International Journal on Software Tools for Technology Transfer, pages 1–22, 2015.
  * [BBG+14] Thomas Ball, Nikolaj Bjørner, Aaron Gember, Shachar Itzhaky, Aleksandr Karbyshev, Mooly Sagiv, Michael Schapira, and Asaf Valadarsky.  Vericon: towards verifying controller programs in software-defined networks.  In ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI ’14, Edinburgh, United Kingdom - June 09 - 11, 2014, page 31, 2014.
  * [BGG96] E. Börger, E. Grädel, and Y. Gurevich.  The Classical Decision Problem.  Springer-Verlag, 1996.
  * [BGG01] Egon Börger, Erich Grädel, and Yuri Gurevich.  The classical decision problem.  Springer Science & Business Media, 2001.
  * [Bjø] Nikolaj Bjørner.  personal communication.
  * [BRK+15] Kshitij Bansal, Andrew Reynolds, Tim King, Clark W. Barrett, and Thomas Wies.  Deciding local theory extensions via e-matching.  In Computer Aided Verification - 27th International Conference, CAV 2015, San Francisco, CA, USA, July 18-24, 2015, Proceedings, Part II, pages 87–105, 2015.
  * [CR79] Ernest Chang and Rosemary Roberts.  An improved algorithm for decentralized extrema-finding in circular configurations of processes.  Communications of the ACM, 22(5):281–283, 1979.
  * [Dij76] Edsger W. Dijkstra.  A Discipline of Programming.  Prentice-Hall, 1976.
  * [Dij82] Edsger W. Dijkstra.  From predicate transformers to predicates (Dedicated by the Tuesday Afternoon Club to C.A.R. Hoare at the occasion of his being elected Fellow of the Royal Society.).  circulated privately, April 1982.
  * [DMB08] L. De Moura and N. Bjørner.  Z3: An efficient SMT solver.  In TACAS, 2008.
  * [DNS05] David Detlefs, Greg Nelson, and James B. Saxe.  Simplify: a theorem prover for program checking.  J. ACM, 52(3):365–473, 2005.
  * [FLL+02] Cormac Flanagan, K. Rustan M. Leino, Mark Lillibridge, Greg Nelson, James B. Saxe, and Raymie Stata.  Extended static checking for java.  In Proceedings of the 2002 ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI), Berlin, Germany, June 17-19, 2002, pages 234–245, 2002.
  * [FPI+17] Yotam M. Y. Feldman, Oded Padon, Neil Immerman, Mooly Sagiv, and Sharon Shoham.  Bounded quantifier instantiation for checking inductive invariants.  In TACAS, 2017.
  * [GBT09] Yeting Ge, Clark W. Barrett, and Cesare Tinelli.  Solving quantified verification conditions using satisfiability modulo theories.  Ann. Math. Artif. Intell., 55(1-2):101–122, 2009.
  * [GM09] Yeting Ge and Leonardo De Moura.  Complete instantiation for quantified formulas in satisfiabiliby modulo theories.  In International Conference on Computer Aided Verification, pages 306–320. Springer, 2009.
  * [HHK+15] Chris Hawblitzel, Jon Howell, Manos Kapritsos, Jacob R. Lorch, Bryan Parno, Michael L. Roberts, Srinath T. V. Setty, and Brian Zill.  Ironfleet: proving practical distributed systems correct.  In Proceedings of the 25th Symposium on Operating Systems Principles, SOSP, pages 1–17, 2015.
  * [HJJ+95] Jesper G. Henriksen, Jakob L. Jensen, Michael E. Jørgensen, Nils Klarlund, Robert Paige, Theis Rauhe, and Anders Sandholm.  Mona: Monadic second-order logic in practice.  In Tools and Algorithms for Construction and Analysis of Systems, First International Workshop, TACAS ’95, Aarhus, Denmark, May 19-20, 1995, Proceedings, pages 89–110, 1995.
  * [Hoa69] C. A. R. Hoare.  An axiomatic basis for computer programming.  Commun. ACM, 12(10):576–580, 1969.
  * [Hod02] Ian Hodkinson.  Loosely guarded fragment of first-order logic has the finite model property.  Studia Logica, 70(2):205–240, 2002.
  * [IBI+13] Shachar Itzhaky, Anindya Banerjee, Neil Immerman, Aleksandar Nanevski, and Mooly Sagiv.  Effectively-propositional reasoning about reachability in linked data structures.  In CAV, volume 8044 of LNCS, pages 756–772, 2013.
  * [IBR+14] Shachar Itzhaky, Nikolaj Bjørner, Thomas W. Reps, Mooly Sagiv, and Aditya V. Thakur.  Property-directed shape analysis.  In Computer Aided Verification - 26th International Conference, CAV 2014, Held as Part of the Vienna Summer of Logic, VSL 2014, Vienna, Austria, July 18-22, 2014. Proceedings, pages 35–51, 2014.
  * [IJS08] Carsten Ihlemann, Swen Jacobs, and Viorica Sofronie-Stokkermans.  On local reasoning in verification.  In Tools and Algorithms for the Construction and Analysis of Systems, 14th International Conference, TACAS 2008, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2008, Budapest, Hungary, March 29-April 6, 2008. Proceedings, pages 265–281, 2008\.
  * [Imm99] Neil Immerman.  Descriptive complexity.  Graduate texts in computer science. Springer, 1999.
  * [IRR+04] Neil Immerman, Alexander Moshe Rabinovich, Thomas W. Reps, Shmuel Sagiv, and Greta Yorsh.  The boundary between decidability and undecidability for transitive-closure logics.  In CSL, 2004.
  * [KBI+17] Aleksandr Karbyshev, Nikolaj Bjørner, Shachar Itzhaky, Noam Rinetzky, and Sharon Shoham.  Property-directed inference of universal invariants or proving their absence.  J. ACM, 64(1):7:1–7:33, 2017.
  * [KV13] Laura Kovács and Andrei Voronkov.  First-order theorem proving and vampire.  In Computer Aided Verification - 25th International Conference, CAV 2013, Saint Petersburg, Russia, July 13-19, 2013. Proceedings, pages 1–35, 2013.
  * [Lei10] K Rustan M Leino.  Dafny: An automatic program verifier for functional correctness.  In Logic for Programming, Artificial Intelligence, and Reasoning, pages 348–370. Springer, 2010.
  * [LP16] K. Rustan M. Leino and Clément Pit-Claudel.  Trigger selection strategies to stabilize program verifiers.  In Computer Aided Verification - 28th International Conference, CAV 2016, Toronto, ON, Canada, July 17-23, 2016, Proceedings, Part I, pages 361–381, 2016.
  * [LQ06] Shuvendu K. Lahiri and Shaz Qadeer.  Verifying properties of well-founded linked lists.  In Proceedings of the 33rd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2006, Charleston, South Carolina, USA, January 11-13, 2006, pages 115–126, 2006.
  * [LQ08] Shuvendu K. Lahiri and Shaz Qadeer.  Back to the future: revisiting precise program verification using SMT solvers.  In Proceedings of the 35th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2008, San Francisco, California, USA, January 7-12, 2008, pages 171–182, 2008.
  * [LS00] Tal Lev-Ami and Shmuel Sagiv.  TVLA: A system for implementing static analyses.  In Static Analysis, 7th International Symposium, SAS 2000, Santa Barbara, CA, USA, June 29 - July 1, 2000, Proceedings, pages 280–301, 2000\.
  * [MP18] Kenneth L. McMillan and Oded Padon.  Deductive verification in decidable fragments with ivy.  In Static Analysis - 25th International Symposium, SAS 2018, Freiburg, Germany, August 29-31, 2018, Proceedings, pages 43–55, 2018.
  * [Nel89] Greg Nelson.  A generalization of dijkstra’s calculus.  ACM Trans. Program. Lang. Syst., 11(4):517–561, 1989.
  * [Pad18] Oded Padon.  Deductive Verification of Distributed Protocols in First-Order Logic.  PhD thesis, Tel Aviv University, 2018.
  * [PLSS17] Oded Padon, Giuliano Losa, Mooly Sagiv, and Sharon Shoham.  Paxos made epr: Decidable reasoning about distributed protocols.  Proc. ACM Program. Lang., 1(OOPSLA):108:1–108:31, October 2017\.
  * [PMP+16] Oded Padon, Kenneth L. McMillan, Aurojit Panda, Mooly Sagiv, and Sharon Shoham.  Ivy: safety verification by interactive generalization.  In Proceedings of the 37th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2016, Santa Barbara, CA, USA, June 13-17, 2016, pages 614–630, 2016.
  * [QGSM13] Xiaokang Qiu, Pranav Garg, Andrei Stefanescu, and Parthasarathy Madhusudan.  Natural proofs for structure, data, and separation.  In ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI ’13, Seattle, WA, USA, June 16-19, 2013, pages 231–242, 2013.
  * [Ram30] F. P. Ramsey.  On a problem of formal logic.  Proceedings of the London Mathematical Society, s2-30(1):264–286, 1930.
  * [RS67] Joseph R. Shoenfield.  Mathematical Logic.  Addison-Wesley, Reading, Massachusetts, 1967.
  * [RSL10] Thomas W. Reps, Mooly Sagiv, and Alexey Loginov.  Finite differencing of logical formulas for static analysis.  ACM Trans. Program. Lang. Syst., 32(6), 2010.
  * [RTG+13] Andrew Reynolds, Cesare Tinelli, Amit Goel, Sava Krstic, Morgan Deters, and Clark Barrett.  Quantifier instantiation techniques for finite model finding in SMT.  In Automated Deduction - CADE-24 - 24th International Conference on Automated Deduction, Lake Placid, NY, USA, June 9-14, 2013. Proceedings, pages 377–391, 2013.
  * [RTGK13] Andrew Reynolds, Cesare Tinelli, Amit Goel, and Sava Krstic.  Finite model finding in SMT.  In Computer Aided Verification - 25th International Conference, CAV 2013, Saint Petersburg, Russia, July 13-19, 2013. Proceedings, pages 640–655, 2013.
  * [Sof05] Viorica Sofronie-Stokkermans.  Hierarchic reasoning in local theory extensions.  In Automated Deduction - CADE-20, 20th International Conference on Automated Deduction, Tallinn, Estonia, July 22-27, 2005, Proceedings, pages 219–234, 2005.
  * [SRW02] Shmuel Sagiv, Thomas W. Reps, and Reinhard Wilhelm.  Parametric shape analysis via 3-valued logic.  ACM Trans. Program. Lang. Syst., 24(3):217–298, 2002.
  * [Wei01] Christoph Weidenbach.  Combining superposition, sorts and splitting.  In Handbook of Automated Reasoning (in 2 volumes), pages 1965–2013. Elsevier, 2001.

##  Appendix A Undecidability

For a universal formula $I\in\forall^{*}(\Sigma)$, the formula
$I\land\delta\land\neg I^{\prime}$ is in EPR (recall that $\delta$ is
specified in EPR). Hence, checking inductiveness amounts to checking the
unsatisfiability of an EPR formula, and is therefore decidable. The same holds
for $I\in AF(\Sigma)$. However, this is no longer true when quantifier
alternation is introduced. For example, checking inductiveness of
$I\in\forall^{*}\exists^{*}(\Sigma)$ amounts to checking unsatisfiability of a
formula in a fragment for which satisfiability is undecidable. In this section
we show that checking inductiveness of ${\forall^{*}\exists^{*}}$ formulas is
indeed undecidable, even when the transition relation is restricted to EPR.
The undecidability of the problem justifies sound but incomplete algorithms
for checking inductiveness, one of which is the Bounded-Horizon algorithm
(defined in Section 3) which we study in this paper.

##### Finite and infinite structures

We begin by showing that the problem is undecidable when structures, or
program states, are assumed to be finite. This is the intention in most
application domains [Imm99] (including the examples in Section 7), especially
when the program does not involve numerical computations. Nevertheless, in
this paper we mostly concern ourselves with the problem of checking
inductiveness when structures may also be infinite. This is because SMT-based
deductive verification relies on proof techniques from standard first-order
logic, whose semantics are defined over _general_ structures, i.e. both finite
and infinite. We thus establish an undecidability result for this setting as
well. It is interesting to note that the discrepancy between the intended
finiteness of the domain and the proof techniques, which cannot incorporate
this assumption, re-emerges in Section 6.

We refer to _inductiveness over finite structures_ when the validity of
$I\land\delta\rightarrow I^{\prime}$ is considered over finite structures, and
to _inductiveness over general structures_ when it is considered over both
finite and infinite structures.

##### Scope of the proofs.

The undecidability proofs of this section are by reductions from tiling
problems. Although technically it is also possible to prove the results by a
trivial reduction from the satisfiability of ${\forall^{*}\exists^{*}}$
formulas, since invariants for the transition relation true are necessarily
either valid or unsatisfiable, we believe that the proofs presented here
demonstrate the intuition behind the inherent difficulty of checking
inductiveness of ${\forall^{*}\exists^{*}}$ formulas in a more profound and
robust way; the reduction using the transition relation true leaves more room
for questions about decidability of the problem w.r.t. classes of transition
relations more realistic and structured than true. In contrast, the reductions
we present here use transition systems (based on tiling problems) that we
consider rather realistic, so the undecidability of checking
${\forall^{*}\exists^{*}}$ invariants seems inherent rather than an artifact
of just degenerate transition relations.

To further provide intuition, we prove the undecidability of the overarching
problem of checking not only inductiveness of a candidate $I$, but also that
$I$ holds initially and implies a given safety property, as is typically done
when inductive invariants are used as a means to verify safety of a transition
system. Formally, the problem of _checking inductive invariants for safety of
transition systems_ is defined as follows. Given a transition relation
$\delta$ (over $\Sigma\uplus\Sigma^{\prime}$), a sentence $\varphi_{0}$ (over
$\Sigma$) describing the set of initial states, a sentence $\varphi_{{P}}$
(over $\Sigma$) describing the safety property, and a sentence $I$ (the
candidate inductive invariant), the problem is to check whether
$\varphi_{0}\rightarrow I$ (initiation), $I\land\delta\rightarrow I^{\prime}$
(consecution), and $I\rightarrow\varphi_{{P}}$ (safety) are valid (over finite
or general structures). We will consider this problem when
$I\in{\forall^{*}\exists^{*}}$, $\varphi_{0}\in{\forall^{*}}$,
$\varphi_{{P}}\in{\forall^{*}}$ and our reductions will generate instances
where $\varphi_{0}\rightarrow I$ and $I\rightarrow\varphi_{{P}}$ are valid (so
it only remains to check whether $I\land\delta\rightarrow I^{\prime}$ is
valid). With these restrictions, the undecidability of the problem of checking
inductive invariants for safety of transition systems over general structures
implies the undecidability of the problem of checking inductiveness as used
elsewhere in this paper.

We now proceed to state the undecidability results and their proofs. We
present different reductions for the problems of inductiveness over finite
structures and over general structures. Both reductions are from the halting
problem, albeit in opposite directions: Over finite structures, the invariant
is inductive iff there is no halting tiling iff the machine does not halt.
Over general structures, the invariant is inductive iff there is no infinite
lower triangular tiling iff the machine halts. This reflects Trakhtenbrot’s
theorem: over finite structures, model enumeration is possible but not proof
enumeration, while over general structures the situation is reversed.

###  A.1. Inductiveness Over Finite Structures

######  Theorem .

It is undecidable to check given $I\in{\forall^{*}\exists^{*}}(\Sigma)$ and
$\delta\in\textsc{EPR}(\Sigma)$ whether $I$ is inductive for $\delta$ over
finite structures.

The proof is based on a reduction from a variant of tiling problems. We start
by defining the specific tiling problem used in the proof of this theorem:
[[IRR+04]] A _halting-tiling problem_ consists of a finite set of tiles $T$
with designated tiles $T_{\text{start}},T_{\text{halt}}\in T$, along with
horizontal and vertical adjacency relations $\mathcal{H},\mathcal{V}\subseteq
T\times T$. A _solution_ to a halting-tiling problem is an arrangement of
instances of the tiles in a finite rectangular grid (“board”) such that the
tile $T_{\text{start}}$ appears in the top left position, the tilef
$T_{\text{halt}}$ appears in the end of a row (the rightmost position in some
row), and the adjacency relationships $\mathcal{H},\mathcal{V}$ are respected,
meaning: if a tile $t_{2}$ appears immediately to the right of $t_{1}$ it must
hold that $(t_{1},t_{2})\in\mathcal{H}$, and if a tile $t_{2}$ appears
immediately below $t_{1}$ it must hold that $(t_{1},t_{2})\in\mathcal{V}$. The
problem is undecidable [IRR+04]. The proof is by a reduction from the halting
problem: given a Turing machine we can compute a halting-tiling problem such
that the problem has a solution iff the machine halts (on the empty input). In
the reduction, rows represent the tape of the Turing machine as it evolves
over time (computation steps). The tiles encode the location of the head and
the current (control) state of the machine. The horizontal and vertical
constraints ensure that successive tiled rows correspond to a correct step of
the machine, and the locality of constratins is possible by the locality of
computation in a Turing machine. See [BGG96] for further details.

###### Proof of Section A.1.

The proof is by a reduction from non-tilability in the halting-tiling problem
(Section A.1) to the problem of checking inductive invariants for safety of a
transition system over finite structures where the initiation and safety
requirements are valid. We think of the transition relation $\delta$ as
incrementally placing tiles in a rectangle.

##### Vocabulary.

To express locations on the board, we use a total order for both the
horizontal and vertical dimensions of the board. We add an immediate
predecessor relation $j=i-1$ which is true if $j<i$ and there is no element of
the order between $j,i$. We use a constant $0$ for the minimal element of the
order. These notions can be defined using a universally quantified
formula.121212 The assumption that there _exists_ a predecessor is left for
the invariant to state explicitly when necessary, as this is the heart of the
${\forall^{*}\exists^{*}}$ quantification in the proof. A _location_ is a pair
of elements of the order, a _vertical_ and _horizontal_ component. We
sometimes use the term _board order_ to refer to the lexicographic order of
pairs of elements of the order.

The transition system keeps track of the last tile placed on the board by a
relation $M(i,j)$ which is true only for the last updated location. Since the
placing of tiles occurs in a sequential manner we also call this board
location _maximal_ , and a location _active_ if it comes before the maximal
location in the board order. The _active area_ is the set of active locations.

The state of tiles on the board is represented by a set of relations
$\\{T_{k}\\}$, one for each tile type, encoding the locations on the board
where a tile of type $T_{k}$ is placed.

In this proof we also use a constant max to be an element of the total order,
representing the width of the rectangle.

##### Transitions.

In every step the transition system places a valid tile in the next board
location. The next board location is considered while respecting the width of
the rectangle, moving to the next row if the horizontal component of the
current tile is max.

Placing a tile of type $T_{\text{next}}$ on the board is done by an EPR update
of the (two-vocabulary) form

$\begin{split}&\forall i,j.\
M^{\prime}(i,j)\leftrightarrow\left(\left(j=0\land
M(i-1,\textit{max})\right)\lor\left(j\neq 0\land j\leq\textit{max}\land
M(i,j-1)\right)\right)\\\ &\forall i,j.\
T^{\prime}_{\text{next}}(i,j)\leftrightarrow\left(T_{\text{next}}(i,j)\lor
M^{\prime}(i,j)\right)\\\ &\forall i,j.\ T^{\prime}_{k}(i,j)\leftrightarrow
T_{k}(i,j)\qquad\forall T_{k}\neq T_{\text{next}}.\end{split}$ (37)

The transition system nondeterministically chooses a tile $T_{\text{next}}$
type that respects the adjacency relationships. These relationships are with
the tiles in the board location preceding the current location in the
horizontal and vertical components, expressible using the immediate
predecessor relation and existential quantification on these predecessors.
(Note that the existential quantifiers do not need to reside in the scope of
universal quantifiers — they depend only on the current location.) Because the
set of tile types $T$ is finite, expressing the allowed tile types given the
two adjacent locations can be done by a quantifier-free formula. Overall the
EPR formula describing a step of the system consists of a disjunction between
choices for $T_{\text{next}}$. Each of these possible choices is described via
a conjunction of the guard that makes sure that it is legal to place
$T_{\text{next}}$, and a corresponding update to the relation that is a
conjunction of the formulas in LABEL:eqn:undecidability-tile-update.

##### Initial state.

Initially we only have $T_{\text{start}}$ placed in the upper-left corner, so
$\forall i,j.\ T_{\text{start}}(i,j)\leftrightarrow\left(i=0\land j=0\right)$
and $\forall i,j.\ \neg T_{k}(i,j)$ for every other tile type $T_{k}$.

##### Safety property.

The safety property states that the special tile $T_{\text{halt}}$, is not
placed on the board in the end of a row (in a max position) in the active
area.

##### Invariant.

The invariant states that in the active area we have a valid partial tiling.
We require this by a ${\forall^{*}\exists^{*}}$ formula saying that for every
tile placed in an active location (except for the maximal location) there is a
successor tile, placed in the next board location, that conforms to the
(local) ajdacency relations.131313 We specify the requirement in this forward
fashion, rather than requiring that every tile has a valid predecessor, in
order to easily reuse this invariant in the proof of Section A.2.  We also
conjoin the safety property to the invariant.

##### Reduction argument.

The invariant holds for the initial state, and trivially implies the safety
property.

If there exists a valid tiling with $T_{\text{halt}}$ in the end of a row, a
counterexample to induction can be obtained by encoding this valid tiling in
the post-state and that same tiling without $T_{\text{halt}}$, which is the
last-placed tile, in the pre-state.

For the converse, assume that the invariant is not inductive over finite
structures, i.e., there exists a finite counterexample to induction, and show
that there exists a solution to the halting-tiling problem. The reasoning is
as follows: A finite state satisfying the invariant induces a valid finite
partial tiling (defined by the active area of the board in the structure).
Since the transition system always places a tile that respects the adjacency
relations, it is easy to see that a counterexample to induction must be such
that the transition places $T_{\text{halt}}$ on the board in the end of a row,
and that this also induces a valid partial finite tiling in the post-state.
Thus a finite counterexample to induction implies the existence of a valid
finite tiling with $T_{\text{halt}}$ in the end of a row, which is a solution
to the halting-tiling problem.

Thus the invariant is inductive iff the halting-tiling problem does not have a
solution. ∎

###  A.2. Inductiveness Over General Structures

######  Theorem .

It is undecidable to check given $I\in{\forall^{*}\exists^{*}}(\Sigma)$ and
$\delta\in\textsc{EPR}(\Sigma)$ whether $I$ is inductive for $\delta$ over
general (finite and infinite) structures.

The proof is based on a reduction from a variant of tiling problems. We start
by defining the specific tiling problem used in the proof of this theorem:

######  Definition .

A _lower-triangular infinite-tiling problem_ consists of a finite set of tiles
$T$, along with horizontal and vertical adjacency relations
$\mathcal{H},\mathcal{V}\subseteq T\times T$. A _solution_ to a lower-
triangular infinite-tiling problem is an arrangement of instances of the tiles
in the lower-triangular plane (i.e., a total function
$\\{(i,j)\in{\mathbb{N}}\times{\mathbb{N}}\;|\;i\leq j\\}\to T$) where the
adjacency relationships $\mathcal{H},\mathcal{V}$ are respected, meaning: if a
tile $t_{2}$ appears immediately to the right of $t_{1}$ it must hold that
$(t_{1},t_{2})\in\mathcal{H}$, and if a tile $t_{2}$ appears immediately below
$t_{1}$ it must hold that $(t_{1},t_{2})\in\mathcal{V}$.

The problem is undecidable. The proof is by a reduction from the non-halting
problem: given a Turing machine we can compute a lower-triangular infinite-
tiling problem such that the problem has a solution iff the machine does not
halt (on the empty input). The encoding is similar to [IRR+04].

###### Proof of Section A.2.

The proof is by a reduction from non-tilability in the lower-triangular
infinite-tiling problem (Section A.2) to the problem of checking inductive
invariants for safety of a transition system (over general structures) where
the initiation and safety requirements are valid.

We construct a transition relation similar to the one in the proof of Section
A.1, with some changes, as described below.

##### Discussion and motivation.

To provide some intuition to the difference between the reductions, we remark
that both of the proofs in this section are in essence a reduction from the
halting (or non-halting) problem. The proof of Section A.1 encodes runs of the
machine as finite tilings, and asks whether a tiling that represents a
terminating computation, encoded by $T_{\text{halt}}$, is possible. This
reduction is no longer adequate when structures may be infinite. The reason is
that an infinite valid partial tiling may not correspond to reachable
configurations of the Turing machine, so there may be such an infinite tiling
with $T_{\text{halt}}$ even though the Turing machine never halts.141414 One
way to construct such a tiling, using a tile in row $\omega$ of the board, is
utilized in the proof that follows.

In fact, the reduction in this proof must be in the opposite direction: the
invariant should be inductive iff the machine terminates, whereas in the proof
of Section A.1 the invariant is inductive iff the machine does not terminate.
This is because satisfiability is recursively-enumerable over finite
structures and co-recursively-enumerable over general structures (due to the
existence of proofs), which reflects on checking inductiveness through the
satisfiability check of the formula $I\land\delta\land\neg I^{\prime}$.

Thus, we would like to have a counterexample to induction when the machine
never halts, i.e. has an infinite run. As before, runs of the machine are
encoded via tiling, only that now an infinite structure can encode an infinite
run of the machine. (It is not necessary that an infinite tiling represents a
valid infinite run of the machine, but every infinite run can be represented
by such a structure.) We would like to “detect” this situation. Our way to do
this is by the observation that induction on the number of rows, or execution
steps, must hold when the number of rows is finite (but unbounded), as in
Section A.1, but does not necessarily hold when there may be an infinite
number of rows. This idea is implemented by a relation $P$ with the invariant
that it is preserved under successive board locations. In an infinite
structure this does not imply that $P$ is true for all locations. A flag $f$
is used to express a transition that is aware of $P$ not being globally true.

Another technical detail is the lower-triangular formulation of the tiling
problem, which is used to construct the infinite computation of the transition
system by placing a single tile in each step.

Returning to the proof, we describe the reduction and highlight its
differences from the reduction in Section A.1. Following the lower-triangular
formulation of the tiling problem, we restrict the board order to the lower-
triangular part (locations $(i,j)$ such that $i\leq j$) and ignore other
locations when considering successor in the board order.

##### Vocabulary.

We add a relation $P$ over board locations, and a Boolean flag (nullary
predicate) $f$.

##### Transitions.

In each step the transition system places a valid tile in the next board
location, similar to the proof of Section A.1. The difference is that the
criterion for moving to place tiles in the next tile is when the current
location $(i,j)$ has $i=j$ (whereas in Section A.1 the criterion was
$j=\textit{max}$).

To maintain the invariant that $P$ is preserved under successor of active
tiles in the board, when we place a new tile, if $P$ holds for the maximal
location before the step, set $P$ to true for the new maximal location.

If $P$ does not hold for the new maximal location, turn $f$ to false.

##### Initial state.

$P$ is true for the first location $(0,0)$ only, and $f$ is true. In this
proof, initially the board is empty.

##### Safety property.

The safety property now asserts that $f$ is true.

##### Invariant.

As before, the invariant states that the active board represents a valid
partial tiling, i.e. every active tile except for the maximal one has a valid
successor.

The invariant also states that $P$ is preserved under successor of board,
i.e., if $(i_{1},j_{1})$ and $(i_{2},j_{2})$ are successive active board
locations w.r.t. the board order, then if $P$ holds for $(i_{1},j_{1})$ is
must also hold for $(i_{2},j_{2})$. We also conjoin the safety property to the
invariant.

##### Reduction argument.

The invariant holds for the initial state, and trivially implies the safety
property.

Assume that there is no solution to the lower-triangular infinite-tiling
problem, and show that the invariant is inductive. The reasoning is as
follows: A state satisfying the invariant induces a partial valid tiling —
either finite or infinite — over the active area of the board. Since there is
no valid partial tiling with an infinite number of rows, the number of active
locations must be finite (the number of columns in the active domain is
bounded by the number of rows, since we are discussing lower-triangular
tilings). Because $P$ is preserved under successor of the board order, by
induction on the number of locations, $P$ must hold for the maximal location.
After a transition is taken, $f$ remains true. Since the transition system
always places a tile that respects the horizontal and vertical ajdacency
relations and sets $P$ to true for the new maximal location, it is easy to see
that the rest of the invariant is preserved by a transition as well.

For the converse direction, if there is a solution to the lower-triangular
infinite-tiling problem, then there is an infinite structure encoding this
tiling. The transition begins with the infinite valid tiling, with a new
additional row _after_ this infinite sequence of tiled rows. (Recall that the
board dimensions are axiomatized using a total order; the additional row index
corresponds to ordinal $\omega$ of vertical order.) We place some tile in the
first column of this row as in some valid row in the tiling. Note that when
placing tiles in this row we need not worry about vertical constraints,
because they were expressed in a forward fashion, and this row is not a
successor of any other row. The first leftmost location in the new row is set
to be the maximal active one, and we set $P$ to be false for this location.
Note that this does not violate the invariant: $P$ is preserved under
successor of the board location, but nonetheless does not hold for the
location in the additional row (it is not the successor of any location). The
transition will now place a new tile and turn $f$ to false, $P$ does not hold
for the current maximal location, thereby violating the invariant.

Thus the invariant is inductive iff the infinite tiling problem does not have
a solution. ∎