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 restriction: for a formula $\varphi_0$ contains non-homogenous inequalities, we replace all constants $r$ by $r\cdot z$, where $z$ is a fresh variable to obtain $\varphi’_0$, and 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)))$
The encoding of the real number $1$ 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$.
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).
We now move on to the 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.
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})}$$
The required Büchi automaton $\mathcal{A_{\neg\varphi}}$ is thus obtained through complementation and intersection of Büchi automata.
The case of conjunction is similarly straightforward. We obtain the required automaton 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})}$$
Finally, we handle projection, i.e. construct $\mathcal{A_{\exists x.\varphi}}$ from $\mathcal{A_{\varphi}}$. Note that the former 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$ while the latter runs over $\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$.
As usual, the main idea is to “guess” an encoding of x such that $\varphi(x,y_1,\dots, y_k)$ holds. However, a small technical hurdle arises: 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$ be given as $01{$}0^\omega$. If the guess is $x=4$, the encoding must be “padded” so the collective encoding is synchronized as $(0, 0)(1, 0)(0, 0)(0, 1)({$}, {$})(0, 0)ω$ and may be accepted by $\mathcal{A_{\varphi}}$.
In other words, while cy is usually emulates the transition of a guessed letter $(c_x, c_y)$, the first letter $a_{y,n}$ of our encoding must emulate the transition of a (non-empty) guess word
$$(a_{x,n+j}, a_{y,n})(a_{x,n+j−1}, a_{y,n})\dots(a_{x,n}, a_{y,n}).$$
$\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
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