AGV 8.1 -- Linear Arithmetic (Theory)

Previous chapter: Translating Alternating to Nondeterministic automata

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

Introduction

In the previous sections, we have seen that the automata machinery can be applied to logical problems by translating formulas into automata. We now study another application of the powerful connection between logic and automata, this time in the setting of real numbers.

Theory of Linear Arithmetic

Definitions and Semantics

Let $V$ be a set of (first-order) variables. The terms of linear arithmetic are defined by the following grammar:

$$t::=0\mid1\mid x\mid t+t$$

The formulas of linear arithmetic are defined by the following grammar, where $x\in V$ is a variable:

$$\varphi::=t\leq t\mid\neg\varphi\mid\varphi\wedge\varphi\mid\exists x.\varphi$$

Additionally, we allow the usual boolean connectives and introduce the following abbreviations:

$$\begin{array}{lrllllrll}
\cdot&n&:=&\overbrace{1+1+\dots+1}^{n\text{ times}},&\hspace{2cm}&\cdot&nx&:=&\overbrace{x+x+\dots+x}^{n\text{ times}},\newline
\cdot&t\geq t’&:=&t’\leq t,&\hspace{2cm}&\cdot&t<t’&:=&t\leq t’\wedge\neg(t=t’)\newline
\cdot&t=t’&:=&t\leq t’\wedge t\geq t’,&\hspace{2cm}&\cdot&t>t’&:=&t’<t
\end{array}$$

The semantics of a formula is given relative to a valuation $\sigma:V\rightarrow\mathbb{R}$ that assigns to each variable a real number. The value of a term is then defined as follows:

$$\begin{array}{llll}
\hspace{1cm}\cdot\ \lbrack 0\rbrack_{\sigma} = 0 &
\hspace{1cm}\cdot\ \lbrack 1\rbrack_{\sigma} = 1 &
\hspace{1cm}\cdot\ \lbrack x\rbrack_{\sigma} = \sigma(x) &
\hspace{1cm}\cdot\ \lbrack t+u\rbrack_{\sigma} =\lbrack t\rbrack_{\sigma}+\lbrack u\rbrack_{\sigma}\end{array}$$

$\models$ is the smallest relation that satisfies the following:

$$\begin{array}{lllllllllllll}
\cdot&\sigma\models t\leq u&\text{ iff }&\lbrack t\rbrack_{\sigma}\leq\lbrack u\rbrack_{\sigma}\newline
\cdot&\sigma\models\neg\varphi&\text{ iff }&\sigma\neg\models\varphi\newline
\cdot&\sigma\models\varphi_0\wedge\varphi_1&\text{ iff }&\sigma\models\varphi_0\text{ and }\sigma\models\varphi_1\newline
\cdot&\sigma\models\exists x.\varphi&\text{ iff }&\text{there is an }a\in\mathbb{R}\ \text{ s.t. }\ \sigma’\models\varphi\ \text{ and }\ \sigma’(y)=\left\lbrace\begin{array}{cll}\sigma(y)&\text{if}&y\neq x\newline a&\text{if}&y=x\end{array}\right.
\end{array}$$

Let $V’\subseteq V$ be the set of free variables occurring in the formula $\varphi$. The solutions of $\varphi$ are the set of all valuations $\sigma$ of $V’$ such that $\sigma\models\varphi$.

Example

formula	Solution Space	Explaination
$x−1\geq1$	$\lbrace x\mapsto a\in\mathbb{R}\mid a\geq2\rbrace$	$x$ can be any real number, as long as it has to be larger than 2.
$\exists y.\ x−1\geq y$	$\lbrace x\mapsto a\mid a\in\mathbb{R}\rbrace$	For any real number $y$, we can always find an $x$ that is larger than $y$ after minus 1.

---

Next chapter: Encoding real numbers

Further Reading: