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.

1. Introduce a logic with a (slightly) restricted syntax from S1S,
2. Show that the restriction does not come at the cost of expressive power, and
3. 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$$

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

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:

Previous chapter: Linear Arithmetic (Theory)

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

Introduction

In last section, we have seen the definiton of Linera Arithmetic, which is similar to S1S. Let see how we can apply it in math and moreover, the connection between logic and automata.

Encoding Real Numbers

We can encode any real number $x\in\mathbb{R}$ into the form $(0+1)(0+1)^\ast{$}(0+1)^\omega$ in two steps:

Step 1

For a real number $x\in\mathbb{R}$, represent it as a pair $(x_I,x_F)$ so that $x=x_I+x_F$.
integer part = $x_I\in\mathbb{Z}$, and fractional part = $x_F\in[0, 1]$, a real number between $0$ and $1$ (both inclusive)

For example, the $1.5 = (1, 0.5)$, and $-{2\over 3}=(−1, {1\over3})$. Note that integers always have two different representations depends on setting the fractional part as $0$ or $1$, and Negative sign can only be represented using the integer part. For example $3=(2,1)$ or $(3,0)$

Step 2

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$$

Previous chapter: From LTL to Alternating Büchi Automata

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

Introduction

The translation from alternating to nondeterministic automata is based on a representation of runs as directed acyclic graphs (DAGs). The idea is similar to the DAG representation we used in the complementation construction for nondeterministic Büchi automata in Section 5.

There the DAG was used to represent the set of all runs of the nondeterministic automaton. The complement automaton would then ”guess” the DAG level-by-level. Here, the DAG is used to represent the branches of a (single) run of the alternating automaton. The idea is illustrated in the following example.

Example

$\textbf{Definition 7.5. } \text{ A } \textit{run DAG }\text{ of an alternating Büchi automaton }\mathcal{A}\text{ on an infinite word }\alpha\text{ is a}\newline\text{DAG }(V,E)\text{, with }V\subseteq Q\times\mathbb{N}\text{ and }(q_0,0)\in V\text{, where}$

$\begin{array}{ll} \hspace{0.5cm} \cdot & E\subseteq \bigcup_{i\in\mathbb{N}}(Q\times\lbrace i\rbrace)\times(Q\times\lbrace i+1\rbrace) \newline \hspace{0.5cm} \cdot & \forall(q,i)\in V \ . \ \exists Y\subseteq Q\text{ s.t. } \newline & Y\models\delta(q,\alpha(i)),Y\times\lbrace i+1\rbrace\subseteq V\text{ and }\lbrace(q,i)\rbrace\times (Y\times\lbrace i+1\rbrace)\subseteq E.\end{array}$

• Every vertices are expressed in (state, letter index)
• Edges are all possible paths from current state $q$

A run DAG is accepting if every infinite path has infinitely many visits to $F\times\mathbb{N}$.

Previous chapter: Alternating Büchi Automata

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

Introduction

It is usually much simpler to translate a logical formula into an alternating automaton than into a nondeterministic automaton. We illustrate this with the translation of LTL formulas into equivalent alternating Büchi automata. The states are simply the subformulas of the given formula and their negations (this set is called the closure of the formula). The transition function is derived from the expansion laws of the logic.

For example, an Until formula $\varphi_1\ \mathcal{U}\ \varphi_2$ holds if:

• $\varphi_2$ holds or
• $\varphi_1$ holds and the entire formula holds in the next step.

The boolean formula produced by the transition function from the state $\varphi_1\ \mathcal{U}\ \varphi_2$ is therefore:

• a disjunction $(\wedge)$ between the transition function for $\varphi_2$ and
• a conjunction $(\vee)$ between the transition function for $\varphi_1$ and the state $\varphi_1\ \mathcal{U}\ \varphi_2$.

From LTL to Alternating Automata

$\textbf{Construction 7.1. }\text{Let }\varphi\text{ be an LTL formula. We construct the alternating Büchi automaton }\newline\mathcal{A_\varphi}=(\Sigma,Q,\varphi,\delta,\small\text{BÜCHI} \normalsize(F))\text{ using:}$
$\begin{array}{ll}
\hspace{0.5cm} \cdot \ Q = \text{closure}(\varphi):=\lbrace\psi,\neg\psi\mid\psi\text{ is subformula of }\varphi\rbrace \newline
\hspace{0.5cm} \cdot \ \delta(p,a)= \left\lbrace \begin{array}{ll}\textit{true}&\text{if }p\in a\newline \textit{false}&\text{if }p\not\in a\end{array}\right. &\cdot \ \delta(\neg\psi,a)=\overline{\delta(\psi,a)}\newline
\hspace{0.5cm} \cdot \ \delta(\psi_1\wedge\psi_2,a)=\delta(\psi_1,a)\wedge\delta(\psi_2,a) &\cdot \ \delta(\psi_1\vee\psi_2,a)=\delta(\psi_1,a)\vee\delta(\psi_2,a)\newline
\hspace{0.5cm} \cdot \ \delta(\psi_1\ \mathcal{U}\ \psi_2,a)=\delta(\psi_2,a)\vee(\delta(\psi_1,a)\wedge\psi_1\ \mathcal{U}\ \psi_2)&\cdot \ \delta(\bigcirc\psi,a)=\psi\newline
\hspace{0.5cm} \cdot \ F = \lbrace\neg(\psi_1\ \mathcal{U}\ \psi_2)\in\text{clousure}(\varphi)\rbrace
\end{array}\newline$
$\text{where we define }\overline{\varphi}=\neg\varphi\text{ for all other }\psi\in Q\text{ and }\overline{\ \cdot\ }\text{ for }\psi,\psi_1,\psi_2\in Q\text{ via:}$
$\begin{array}{ll}
\hspace{0.5cm} \cdot \ \overline{\neg\varphi}=\varphi
\hspace{0.5cm} \cdot \ \overline{\psi_1\wedge\psi_2}=\overline{\psi_1}\vee\overline{\psi_2}
\hspace{0.5cm} \cdot \ \overline{\psi_1\vee\psi_2}=\overline{\psi_1}\wedge\overline{\psi_2}
\hspace{0.5cm} \cdot \ \overline{\textit{true}}=\overline{\textit{false}}
\hspace{0.5cm} \cdot \ \overline{\textit{false}}=\overline{\textit{true}}
\end{array}$

Previous chapter: S1S$_0$ and Büchi-recognizable Language

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

Introduction

Logics are often significantly more concise than automata. For example, in the translation from S1S to Büchi automata in the proof of Theorem 6.4, each negation increases the size of the Büchi automaton exponentially, resulting in a non-elementary number of states. The blow-up when translating LTL formulas is less dramatic, but still exponential. In this section, we show that the conciseness of the logic and the automata can be brought closer together when the automata are equipped with both nondeterministic and universal choices.

Alternating Automata

Nondeterministic and Universal

In previous sections, we discussed a lot about Nondeterministic transitions. Here we introduce a new concept Universal transitions for our new automaton called alternating automaton. We allow for both types of choices by defining, for each state and input letter, a positive Boolean formula over the successor states.

Choices	Symbol	Definition
Nondeterministic	disjunction $(\vee)$	the suffix of an input word is accepted by SOME successor state
Universal	conjunction $(\wedge)$	the suffix of an input word is accepted by ALL successor states

Positive Boolean Formulas $\ \mathbb{B}^+(X)$

$\textbf{Definition 7.1. } \text{The }\textit{positive Boolean formulas }\text{over a set }X\text{, denoted }\mathbb{B}^+(X)\text{, are the formulas}\newline\text{built from elements of }X\text{, conjunction }\wedge\text{, disjunction }\vee,\textit{ true}\text{ and }\textit{false.}$

Previous chapter: Express QPTL using S1S

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

Introduction

To prepare for the proof that every S1S-definable language is Büchi-recognizable, we show in the following lemma that we can focus on a restricted sublogic, called S1S$_0$, which is defined by the following grammar:

$$\varphi::=0\in X\mid x\in Y\mid x=0\mid x=y\mid x=S(y)\mid \neg\varphi\mid\varphi\wedge\varphi\mid\exists x.\varphi\mid\exists X.\varphi$$

• Membership tests $(\in)$: variables $(x,y,\dots)$ and $0$ only
• Equalities $(=)$: variables $(x,y,\dots)$, $0$ and a single successor operation $(S(t))$ only
  • i.e. $S(S(t))$ is not allowed.

Complex formula in S1S can then be simplified by introducing additional variables.

From S1S to S1S$_0$

$\textbf{Lemma 6.1. } \textit{For every S1S formula }\varphi\textit{ there is an S1S}_0\text{ formula }\varphi’\textit{ such that }\mathcal{L}(\varphi)=\mathcal{L}(\varphi’).$

Proof

Previous chapter: Monadic Second-Order Logic of One Successor (S1S)

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

Introduction

We already showed, in Theorem 6.2, that every Büchi-recognizable language is QPTL-definable. We now complete a full circle by showing that every QPTL-definable language is S1S-definable, and that every S1S-definable language is Büchi-recognizable. Hence, QPTL, S1S, and Büchi automata are equally expressive.

$\textbf{Theorem 6.3. } \textit{Every QPTL-definable language is S1S-definable.}$

Proof

In section 6.4, we defined the language of QPTL as: $\mathcal{L}(\varphi)=\lbrace\alpha\in{(2^{AP’})}^{\omega}\mid\alpha\models\varphi\rbrace$, and

In section 6.5, we defined the language of S1S as: $\mathcal{L}(\varphi)=\lbrace \alpha_{\sigma_1,\sigma_2}\in(2^{V’_1\cup V’_2})^\omega\mid\sigma_1,\sigma_2\models\varphi\rbrace$

Notice main difference comes from $\alpha\models\varphi$ and $\sigma_1,\sigma_2\models\varphi$. Also, QPTL uses propositions but S1S uses term. We thus define S1S formula as $T(\varphi,t)$, where $\varphi$ is a QPTL-formula over $AP$ and $t$ is a S1S-term. Lastly, with $V_2=AP$, we can now define a S1S formula for all $\alpha\in(2^{AP})^\omega$,

$$\alpha\lbrack\lbrack t\rbrack_{\sigma_1},\infty\rbrack\models_{QPTL}\varphi\hspace{0.5cm}\text{iff}\hspace{0.5cm}\sigma_1,\sigma_2\models_{S1S}T(\varphi,t)\varphi,\hspace{1cm}\text{where }\ \sigma_2:P\mapsto\lbrace i\in\mathbb{N}\mid P\in\alpha(i)\rbrace$$