Previous chapter: Homogenous Inequality Testing is Automatic
This is a learning note of a course in CISPA, UdS. Taught by Bernd Finkbeiner
Introduction
With all the setup in the previous sections, We are now ready to prove the main result of this chapter.
$\textbf{Theorem 8.1. }\textit{Let }\varphi\textit{ be a linear arithmetic formula. We can effectively construct a Büchi}\newline\textit{Automaton }\mathcal{A}\textit{ such that }\mathcal{L(A)}=\lbrace\alpha_\sigma\mid\sigma\models\varphi\rbrace$
We follow the same strategy as for the analogous result for S1S in Section 6.7.
- Introduce a logic with a (slightly) restricted syntax from S1S,
- Show that the restriction does not come at the cost of expressive power, and
- Use structural induction on restricted-syntax formulas to construct our desired automata.
Restricted Linear Arithmetic
The formulas of syntactically restricted linear arithmetic are defined by the following grammar:
$$\varphi::=z=1\mid g_1x_1+\dots+g_\ell x_\ell\leq h_1 y_1+\dots+h_m y_m\mid\neg\varphi\mid\varphi\wedge\varphi\mid\exists x.\varphi$$
where $z, x_1,\dots,x_\ell,y_1,\dots,y_m\in V$ are variables, and $p_1,\dots,p_\ell,q_1,\dots,q_m$ are positive constants. The restriction is that all inequalities must be homogenous, except $z=1$ being the only non-homogenous relation.
homogenous inequalities conversion
In fact, “all inequalities must be homogenous” is not a semantic restrictionm, since we can always convert non-homogenous inequalities into a homogenous version:
For a formula $\varphi_0$ contains non-homogenous inequalities, first replace all constants $r$ by $r\cdot z$, where $z$ is a fresh variable to obtain $\varphi’_0$, then replace $\varphi_0$ with $\varphi::=\exists z. (z=1\wedge\varphi’_0)$.
For example, $\varphi_0::=y\leq2,\varphi_0’::=y\leq2\cdot z,$ now we have $\varphi_0::=\exists z. (z=1\wedge(y\leq2\cdot z)))$
To include all possible expression of the real number $1$, the encoding must be a word of the form $00^\ast(1{$} 0^\omega + {$} 1^\omega)$. It is thus trivial to construct an automaton corresponding to $z=1$.
From Linear Arithmetic to Automata
We use Construction 8.1 to construct automata for homogenous inequalities. Note that the construction works even when one of the sides of the inequality is equal to $0$ (i.e., the empty sum).
Now we start with inductive cases. Recall that for any $k$ we can construct an automaton $\mathcal{L(A_{\textsf{valid},k})}$ that checks whether a word $\alpha\in(\lbrace 0,1\rbrace^k\cup\lbrace{$}\rbrace)^k)^\omega$ is a well-formed encoding of some valuation $\sigma$ to $k$ free variables.
Negation $\mathcal{A_{\neg\varphi}}$
The Büchi automaton $\mathcal{A_{\neg\varphi}}$ is obtained through complementation and intersection of Büchi automata.
Let $\varphi$ have $k$ free variables. For negation, we have
$$\mathcal{L(A_{\neg\varphi})}=((\lbrace 0,1\rbrace^k\cup\lbrace{$}\rbrace)^k)^\omega\setminus\mathcal{L(A_\varphi)})\cap\mathcal{L(A_{\textsf{valid},k})}$$
Conjunction $\mathcal{A_{\varphi_1\wedge\varphi_2}}$
$\mathcal{A_{\varphi_1\wedge\varphi_2}}$ can be obtained similarly straightforward through the intersection of two Büchi automata because
$$\mathcal{L(A_{\varphi_1\wedge\varphi_2})}=\mathcal{L(A_{\varphi_1})}\cap\mathcal{L(A_{\varphi_2})}$$
Existential Quantification
To handle projection, i.e. construct $\mathcal{A_{\exists x.\varphi}}$ from $\mathcal{A_{\varphi}}$, we first try to see their difference:
- $\mathcal{A_{\varphi}}$ runs over the alphabet $\lbrace 0, 1\rbrace^{k+1}\cup\lbrace{$}\rbrace^{k+1}$ and reads the encoding of a valuation of $\lbrace x,y_1,\dots, y_k\rbrace$.
- $\mathcal{A_{\exists x.\varphi}}$ runs over the alphabet $\lbrace 0, 1\rbrace^k\cup\lbrace{$}\rbrace^k$ and reads the encoding of a valuation of $\lbrace y_1,\dots, y_k\rbrace$,
Same as before, the principle behind the construction is to create a automaton that simulate identical behaviour with the absence of $x$. This is simple for most of the transitions except for the initial transition.
For a automaton that does not contain $x$, it has to “guess” an encoding of $x$ such that $\varphi(x,y_1,\dots, y_k)$ holds. However, the given encoding of the valuation of $\lbrace y_1,\dots, y_k\rbrace$ may not be appropriately padded.
For example, let $y_1 = 1$ and we encode it as $01{$}0^\omega$. If we guess $x=4$, then two digits of integer part is not enough. The encoding must be “padded” so to synchronize “may be” accepted by $\mathcal{A_{\varphi}}$:
$$\begin{bmatrix}x\newline y_1\end{bmatrix}=\begin{bmatrix}0\newline 0\end{bmatrix}
\begin{bmatrix}1\newline 0\end{bmatrix}\begin{bmatrix}0\newline 0\end{bmatrix}
\begin{bmatrix}0\newline 1\end{bmatrix}\begin{bmatrix}{$}\newline{$}\end{bmatrix}\left(\begin{bmatrix}0\newline 0\end{bmatrix}\right)^\omega$$
Therefore, when we convert from $c_y$ to $(c_x, c_y)$, We have to repeat the first letter $c_{y,n}$ as padding:
$$(a_{x,n+j}, a_{y,n})(a_{x,n+j−1}, a_{y,n})\dots(a_{x,n}, a_{y,n}).$$
Since $c_{y,n}$ is simply repeating, creating transition for each letter of $a_x$ unnecessarily enlarge the size of the automaton. Instead, we can make one initial transition that encapsulate the full padding of the first letter of $c_y$.
$$(q,(c_{x,1},c_{y_1},\dots,c_{y_k})\dots(c_{x,n},c_{y_1},\dots,c_{y_k}),q’)\in T’$$
$\textbf{Construction 8.2. } \text{Let }x,y_1,\dots, y_k\text{ be free variables in the linear arithmetic formula }\varphi,\text{ and}$
$$\mathcal{A_\varphi}=(\lbrace 0, 1\rbrace^{k+1}\cup\lbrace{$}\rbrace^{k+1},Q,I,T,\small\text{BÜCHI}\normalsize (F))$$
$\text{be a Büchi Automaton such that }\mathcal{L(A)}=\lbrace\alpha_\sigma\mid\sigma\models\varphi\rbrace.\text{ We construct a Büchi Automaton}$
$$\mathcal{A_{\exists x.\varphi}}=(\lbrace 0, 1\rbrace^{k}\cup\lbrace{$}\rbrace^{k},Q\cup\textsf{Inits},\textsf{Inits},T’,\small\text{BÜCHI}\normalsize (F))$$
$\text{such that }\mathcal{L(A_{\exists x.\varphi})}=\lbrace\alpha_\sigma\mid\sigma\models\exists x.\varphi\rbrace\text{ as follows.}$
$\begin{array}{l}
\hspace{1cm} \cdot \ \textsf{Inits}=\lbrace(q,\star)\mid q\in I\rbrace\newline
\hspace{1cm} \cdot \ (q,(c_{y_1},\dots,c_{y_k}),q’)\in T’\text{ if and only if there exists }c_x\text{ such that }(q,(c_x,c_{y_1},\dots,c_{y_k}),q’)\in T’\newline
\hspace{1cm} \cdot \ ((q,\star),(c_{y_1},\dots,c_{y_k}),q’)\in T’\text{ if and only if there exists a word }c_{x,1}\dots c_{x,n}\in\lbrace0,1\rbrace^{+}\newline
\hspace{1cm} \ \text{ such that }(q,(c_{x,1},c_{y_1},\dots,c_{y_k})\dots(c_{x,n},c_{y_1},\dots,c_{y_k}),q’)\in T’\end{array}$
Two remarks are in order:
We extended the transition relation $T$ to $Q\times\Sigma^+\times Q$: if $(q,u,q’)\in T$ and $(q’,v,q’’)\in T$, then $(q,uv,q’’)\in T$ (where $\Sigma^+ = \Sigma\Sigma^\ast$).
The transitions from the freshly added initial states can be readily determined, via, for example, a depth-first search by considering an appropriate subgraph induced by the automaton $\mathcal{A_\varphi}$.
This concludes the final inductive case, and, hence, the proof of Theorem 8.1.
Next chapter: Automata-based LTL Model Checking with Sequential Circuits
Please cite the source for reprints, feel free to verify the sources cited in the article, and point out any errors or lack of clarity of expression. You can comment in the comments section below or email to GreenMeeple@yahoo.com