AGV 8.4 -- Homogenous Inequality Testing is Automatic

Previous chapter: Translation from Linear Arithmetic to Automata

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

Introduction

In the previous section, we used $x+y=z$ as an example. By extend that into a more general inequality

$$g_1x_1+\dots+g_\ell x_\ell\leq h_1y_1+\dots +h_my_m$$

where $x_1,\dots,x_\ell,y_1,\dots,y_m$ are free variables, and $g_1,\dots,g_\ell,h_1,\dots,h_m$ are positive integer constants. Such inequality can be described by a Büchi automaton.

$\textbf{Lemma 8.1. }\textit{Let }\lbrace x_1,\dots,x_\ell,y_1,\dots,y_m\textit{ be a set of free variables, and let }g_1,\dots,g_\ell,h_1,\dots,h_m\newline\textit{be positive integer constants. There exists a Büchi automaton }\mathcal{A}\textit{ such that}$

$$\mathcal{L(A)}=\lbrace\alpha_\sigma\mid\sigma\models g_1x_1+\dots+g_\ell g_\ell\leq h_1 y_1+\dots+h_m y_m\rbrace$$

It is easy to start with constructing an automaton $\mathcal{A}_{\textsf{valid},\ell+m}$ that checks whether the word $\alpha_\sigma$ is well-formed:

1. checks that the separation symbol $({$},\dots,{$})$ occurs exactly once, and
2. the separation symbol does not appear at the beginning of the word.

A Generalize Example

• $D:\sum_{i}g_ix_i-\sum_{j}h_jy_j\leq0$, where $G=\sum_{i}g_i$, and $H=\sum_{j}h_j$. We define the

• $D_t$ = integer part, $[D]_t$ = fractional part, and observe that for all $t$:

$$D_1=-\sum_{i}g_ic_{x_{i},1}-(-\sum_{j}h_jc_{y_{j},1})=\sum_{j}h_jc_{y_{j},1}-\sum_{i}g_ic_{x_{i},1},\newline D_{t+1}=2D_t+\sum_{i}g_ic_{x_{i},t+1}-\sum_{j}h_jc_{y_{j},t+1},\newline -H\leq[D]_t\leq G.$$

The trichotomy is also completely analogous.

• If, for some $t$, we have $D_t>H$, we have that $D>0$, and the formula is violated.
• If, for some $t$, we have $D_t<−G$, we have that $D<0$, and the formula is satisfied.
• If, for all $t$, we have $−G\leq D_t\leq H$ we have that $D=0$, and the formula is satisfied.

Our automaton construction keeps track of $D_t$ using the recurrence above. Due to the trichotomy, we only need compute $D_t$ precisely as long as it is at least $−G$ and at most $H$.

Thus, we have 3 types of states in the automaton:

1. initialization state
2. Precise value states within $−G,\dots,0,\dots,H$ of $D_t$
3. trap states ($D_t$ has crossed $−G (−\infty)$ or $H (\infty)$)

$\textbf{Construction 8.1. } \text{Let }x_1,\dots,x_\ell,y_1,\dots,y_m\text{ be free variables, and let }g_1,\dots,g_\ell,\text{ and}\newline h_1,\dots,h_m,\text{ be positive integer constants with }\sum_{i}g_i=G\text{ and }\sum_{j}h_j=H\text{. We construct a}\newline\text{(deterministic) Büchi Automaton}\mathcal{A}=(\Sigma,Q,I,T,\small\text{BÜCHI}\normalsize (F))\text{, such that}$

$$\mathcal{L(A)}=\lbrace\alpha_\sigma\mid\sigma\models g_1x_1+\dots+g_\ell g_\ell\leq h_1 y_1+\dots+h_m y_m\rbrace \hspace{1cm}\text{ as follows,}$$

$\begin{array}{l}\hspace{1cm} \cdot \ \Sigma=\lbrace {$}^{l+m}\cup(\lbrace0,1\rbrace^\ell\times\lbrace0,1\rbrace^m)\rbrace\hspace{1cm}((\ell\text{+m)-fold Cartesian product)}\newline
\hspace{1cm} \cdot \ Q=\lbrace\textsf{init},-\infty,-G,-G+1,\dots,-1,0,1,\dots,H,\infty\rbrace\newline
\hspace{1cm} \cdot \ I=\lbrace\textsf{init}\rbrace\newline
\hspace{1cm} \cdot \ F=\lbrace-\infty,-G,-G+1,\dots,-1,0,1,\dots,H\rbrace\newline
\hspace{1cm} \cdot \ T\text{ is defined as follows:}\newline
\hspace{1.5cm} 1. \ (\textsf{init},(c_{x_1},\dots,c_{y_m}),q’))\in T\text{ if and only if }q’\in\sum_{j}h_jc_{y_j}-\sum_{i}g_ic_{x_i}\newline
\hspace{1.5cm} 2. \ (q,({$}\dots{$}),q)\in T\text{ for all }q\in Q\setminus\lbrace\textsf{init}\rbrace,\newline
\hspace{1.5cm} 3. \ (q_\infty,c,q_\infty)\in T\text{ for all }c\in\Sigma,q_\infty\in\lbrace-\infty,\infty\rbrace,\newline
\hspace{1.5cm} 4. \ \text{For }q\in\lbrace-G,\dots,0,\dots,H\rbrace,(q,(c_{x_1},\dots,c_{y_m}),q’)\in T\text{ if and only if }q’=\textsf{next}\text{, where}\newline
\end{array}$
$$\textsf{next}=\left\lbrace\begin{array}{cll}
2q+\sum_{i}g_ic_{x_{i}}-\sum_{j}h_jc_{y_{j}}&\text{if}&-G\leq2q+\sum_{i}g_ic_{x_{i}}-\sum_{j}h_jc_{y_{j}}\leq H \newline
\infty&\text{if}&2q+\sum_{i}g_ic_{x_{i}}-\sum_{j}h_jc_{y_{j}}> H \newline
-\infty&\text{if}&2q+\sum_{i}g_ic_{x_{i}}-\sum_{j}h_jc_{y_{j}} <-G \end{array}\right.$$

Explanation

All possible transitions are those the criterion we mentioned above (according to the numbering):

1. $D_1=\sum_{j}h_jc_{y_{j},1}-\sum_{i}g_ic_{x_{i},1}$
2. The separation symbol does not appear at the beginning of the word.
3. $D_t$ has crossed $−G (−\infty)$ or $H (\infty)$ move to trap states and cannot leave
4. According to the trichotomy, we only need compute $D_t$ precisely as long as it is $−G\leq D_t\leq H$.

This completes the proof of Lemma 8.1. We remark that the same construction also works to check the following:

• Strict Inequality: $g_1x_1+\dots+g_\ell x_\ell < h_1y_1+\dots +h_my_m$ (by setting $F=\lbrace−\infty\rbrace$),
• Equality: $g_1x_1+\dots+g_\ell x_\ell = h_1y_1+\dots +h_my_m$ (by setting $F=\lbrace−G,\dots,H\rbrace$),
• Reverse Inequality: $g_1x_1+\dots+g_\ell x_\ell \geq h_1y_1+\dots +h_my_m$ (by setting $F=\lbrace−G,\dots,H,\infty\rbrace$),
• Reverse Strict Inequality: $g_1x_1+\dots+g_\ell x_\ell > h_1y_1+\dots +h_my_m$ (by setting $\infty\rbrace$).

---

Next chapter: From Linear Arithmetic to Automata

Further Reading: