AGV 8.3 -- Translation from Linear Arithmetic to Automata

Previous chapter: Encoding real numbers

This is a learning note of a course in CISPA, UdS. Taught by Bernd Finkbeiner

In this section, we will illustrate the key ideas in the translation from linear arithmetic to automata through a simple example.

Consider the formula $x+y=z$ and the following encoding of the valuation $x\mapsto1$, $y\mapsto1$, $z\mapsto2$:

$$\alpha_\sigma=\begin{bmatrix}0\newline 0\newline 0\end{bmatrix}\begin{bmatrix}0\newline 0\newline 1\end{bmatrix}
\begin{bmatrix}0\newline 0\newline 0\end{bmatrix}\begin{bmatrix}{$}\newline {$}\newline {$}\end{bmatrix}\left(\begin{bmatrix}1\newline 1\newline 0\end{bmatrix}\right)^\omega = \begin{bmatrix}x\newline y\newline z\end{bmatrix} = \begin{bmatrix}1\newline 1\newline 2\end{bmatrix}$$

Homogeneity

A equation is homogenous if there are no constant terms. The key property of homogeneity is that we can simply scaling without being unbounded. In other words, for a homogenous equation $D$, we have:

$D∼0$ (where $∼$ is an arbitrary (in)equality) if and only if, for all $k\in\mathbb{Z},2^k\cdot D∼0$. (Scaling behaviour)

As we can see the equation $x+y=z$ is homogenous, i.e., $D: x+y−z = 0$ and $2^k\cdot x+2^k\cdot y−2^k\cdot z∼0$

We immediately observe that:

• $2^k\cdot D$ has constant sign,
• If $D\neq0$, it is strictly increasing in $k$, and thus
• For any threshold $N$, we will have that $|2^k\cdot D|>N$ for all sufficiently large $k$.

Shifting the ${$}$ Delimiter

The key observation is that multiplying by a power of $2$ = shifting the ${$}$ delimiter in the binary representation.

$$\begin{bmatrix}x\newline y\newline z\end{bmatrix} =
\begin{bmatrix}0\newline 0\newline 0\end{bmatrix}\begin{bmatrix}0\newline 0\newline 1\end{bmatrix}
\begin{bmatrix}0\newline 0\newline 0\end{bmatrix}\begin{bmatrix}{$}\newline{$}\newline{$}\end{bmatrix}
\left(\begin{bmatrix}1\newline 1\newline 0\end{bmatrix}\right)^\omega=
\begin{bmatrix}1\newline 1\newline 2\end{bmatrix},\newline
\begin{bmatrix}2^2\cdot x\newline 2^2\cdot y\newline 2^2\cdot z\end{bmatrix} =
\begin{bmatrix}0\newline 0\newline 0\end{bmatrix}\begin{bmatrix}0\newline 0\newline 1\end{bmatrix}
\begin{bmatrix}0\newline 0\newline 0\end{bmatrix}\begin{bmatrix}1\newline 1\newline 0\end{bmatrix}
\begin{bmatrix}1\newline 1\newline 0\end{bmatrix}\begin{bmatrix}{$}\newline{$}\newline{$}\end{bmatrix}
\left(\begin{bmatrix}1\newline 1\newline 0\end{bmatrix}\right)^\omega=
\begin{bmatrix}2^2\cdot 1\newline 2^2\cdot 1\newline 2^2\cdot 2\end{bmatrix}=
\begin{bmatrix}4\newline 4\newline 8\end{bmatrix},
$$

For any variable $z$, and $t\geq1$, we denote by $z_t$ the integer encoded by the leftmost $t$ digits of $z$ (the ${$}$ is ignored):

$$\begin{bmatrix}x\newline y\newline z\end{bmatrix} =
\begin{bmatrix}0\newline 0\newline 0\end{bmatrix}\begin{bmatrix}0\newline 0\newline 1\end{bmatrix}
\begin{bmatrix}0\newline 0\newline 0\end{bmatrix}\begin{bmatrix}1\newline 1\newline 0\end{bmatrix}
\begin{bmatrix}1\newline 1\newline 0\end{bmatrix}\begin{bmatrix}1\newline 1\newline 0\end{bmatrix}\dots$$

$
\begin{array}{lclc}
\hspace{1cm}\cdot\ x_5 =& -2^4\cdot0+2^3\cdot0+2^2\cdot0+2^1\cdot1+2^0\cdot1&=&3\newline
\hspace{1cm}\cdot\ y_3 =& -2^2\cdot0+2^1\cdot0+2^0\cdot0&=&0\newline
\hspace{1cm}\cdot\ z_4 =& -2^3\cdot0+2^2\cdot1+2^1\cdot0+2^1\cdot0&=&4\newline
\hspace{1cm}\cdot\ z_5 =& -2^4\cdot0+2^3\cdot1+2^1\cdot0+2^2\cdot0+2^0\cdot0&=&8\newline
\end{array}
$

key linear recurrence

We can see the above definition is initialized as $z_1=−c_{z,1}$, and key linear recurrence holds for any variable: $z_{t+1}=2z_t+c_{z,t+1}$, where $c_{z,t+1}$ is the $(t+1)$-th digit from the left in the encoding of $z$.

Now, in our example we can define $D_t=x_t+y_t−z_t$, and by linearity, the same recurrences hold for $D_t$, too:

$$D_1=c_{z,1}-c_{x,1}-c_{y,1}\newline D_{t+1}=2D_t+c_{z,t}-c_{x,t}-c_{y,t}$$

Thus, we have $D_1=0,D_2=−1,D_3=−2$, and $D_t=−2$ for subsequent $t$.

Fractional part

To account for the digits other than the $t$ leftmost digits, we define the fractional part $\lbrack z\rbrack_t = \sum_{i=1}^{\infty}2^{-i}\cdot c_{z,t+i}$.

$$\begin{bmatrix}x\newline y\newline z\end{bmatrix} =
\begin{bmatrix}0\newline 0\newline 0\end{bmatrix}\begin{bmatrix}0\newline 0\newline 1\end{bmatrix}
\begin{bmatrix}0\newline 0\newline 0\end{bmatrix}\begin{bmatrix}1\newline 1\newline 0\end{bmatrix}
\begin{bmatrix}1\newline 1\newline 0\end{bmatrix}\begin{bmatrix}1\newline 1\newline 0\end{bmatrix}\dots$$

$
\begin{array}{lclc}
\hspace{1cm}\cdot\ [x]_1 =& 2^{-1}\cdot0+2^{-2}\cdot0+2^{-3}\cdot1+2^{-4}\cdot1+\dots&=&{1\over4}\newline
\hspace{1cm}\cdot\ [y]_2 =& 2^{-1}\cdot0+2^{-2}\cdot1+2^{-3}\cdot1+2^{-4}\cdot1+\dots&=&{1\over2}\newline
\hspace{1cm}\cdot\ [z]_1 =& 2^{-1}\cdot1+2^{-2}\cdot0+2^{-3}\cdot0+\dots&=&{1\over2}\newline
\hspace{1cm}\cdot\ [z]_3 =& 2^{-1}\cdot0+2^{-2}\cdot0+2^{-3}\cdot0+\dots&=&0\newline
\end{array}
$

Here, we can see $0\leq[z]_t\leq1$, and that $z_t+[z]_t = 2^k\cdot z$ for some $k\in\mathbb{Z}$.

If the $2^k\cdot z$ doesn’t seem intuitive to you, check this out:
let say we have $z=011{$}0111\dots = 3+{1\over2}=3.5$, and we set $t=7$, so $z_7=-2^6\cdot0+2^5\cdot1+2^4\cdot1+2^3\cdot0+2^2\cdot1+2^1\cdot1+2^0\cdot1=55$ and $[z]_7={1\over2}+{1\over4}+{1\over8}+\cdots=1$. Thus we have $z_7+[z]_7 = 56 = 2^4\cdot 3.5$.

We can then extend the definition of fractional part to $D$ in the obvious way: $[D]_t = [x]_t+[y]_t−[z]_t$.
We thus have that $−1\leq [D]_t\leq 2$, and that $D_t+[D]_t=2^k\cdot D$ for some $k$.

1. If $D_t<−2$ for some $t$. then $D_t+[D]_t<0$. For the corresponding $k$, we have that $2^k \cdot D<0$. Therefore $x+y-z<0$ and thus we conclude $x+y<z$.

2. If $D_t>1$ for some $t$, then $D_t+[D]_t>0$. For the corresponding $k$, we have that $2^k \cdot D>0$. Therefore $x+y-z>0$ and thus we conclude $x+y>z$.

3. If $−2\leq D_t\leq 1$ for all $t$, then $|D_t+[D]_t|\leq 3$. For arbitrarily large $k$, $|2^k\cdot D|\leq3$. This implies that $x+y=z$ (only option left)

From Linear Arithmetic to Automaton

From the above deduction, $x+y=z$ holds if and only if $−2\leq D_t\leq 1$. To check whether it holds with an automaton, we use the encoding to compute the sequence $D_t$ term by term, and accept if and only if each term is at least $−2$ and at most $1$.

Indeed, in our example, the sequence of terms is $0,−1,−2,−2,\dots$, and we accept.

As an example, we could also consider a different encoding of $x\mapsto1$, $y\mapsto1$, $z\mapsto2$:

$$\alpha’_\sigma=\begin{bmatrix}0\newline 0\newline 0\end{bmatrix}\begin{bmatrix}1\newline 1\newline 1\end{bmatrix}
\begin{bmatrix}{$}\newline {$}\newline {$}\end{bmatrix}\left(\begin{bmatrix}0\newline 0\newline 1\end{bmatrix}\right)^\omega = \begin{bmatrix}x\newline y\newline z\end{bmatrix} = \begin{bmatrix}1\newline 1\newline 2\end{bmatrix}$$

In this example the sequence of $D_t$ is $0, 1, 1, 1,\dots$, which is again bounded, and we accept.

On the other hand, a rejecting example may look like this:

$$\alpha_{\sigma’}=\begin{bmatrix}0\newline 0\newline 1\end{bmatrix}\begin{bmatrix}1\newline 1\newline 0\end{bmatrix}
\begin{bmatrix}{$}\newline {$}\newline {$}\end{bmatrix}\left(\begin{bmatrix}0\newline 0\newline 0\end{bmatrix}\right)^\omega = \begin{bmatrix}x\newline y\newline z\end{bmatrix} = \begin{bmatrix}1\newline 1\newline -2\end{bmatrix}$$

The sequence of $D_t$ is $1, 4, 8, 15,\dots$, which is out of bounded, and we reject.

---

Next chapter: Homogenous Inequality Testing is Automatic

Further Reading: