Previous chapter: Closure Properties of the Büchi-recognizable languages (Intersection and Union)

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

In this section, we continue the proof of the closure properties of the Büchi-recognizable languages.

Concatenation of regular Langauge and Büchi-recognizable Language

$$\begin{gathered} \mathbf{\text{Construction 3.3. }}\text{Let }{\mathcal{A}}_1=(\mathrm{\Sigma },Q_1,I_1,T_1,F_1)\text{ be an automaton over finite words that} \\ \text{recognizes the languge }{L}_1\text{, and let }{\mathcal{A}}_2=(\mathrm{\Sigma },Q_2,I_2,T_2,\text{BÜCHI}(F_2))\text{ be a Büchi automaton} \\ \text{over the same alphabet that recognizes }{L}_2.\text{ We construct a Büchi autotmaton } \\ {\mathcal{A}}^{\prime }=(\mathrm{\Sigma },Q^{\prime },I^{\prime },T^{\prime },\text{BÜCHI}(F_2))\text{ with }\mathcal{L}({\mathcal{A}}^{\prime })=L_1\cdot L_2\text{ as follows:} \end{gathered}$$
$\begin{array}{lrll}\cdot & Q^{\prime }& =& Q_1\cup Q_2(\text{w.l.o.g we assume }{Q}_1\cap Q_2=\varnothing )\\ \cdot & I^{\prime }& =& \{\begin{array}{ll}{I}_1& \text{if }{I}_1\cap F_1=\varnothing \\ I_1\cup I_2& \text{otherwise}\end{array}\\ \cdot & T^{\prime }& =& T_1\cup T_2\cup \{(q,\sigma ,q^{\prime })\mid (q,\sigma ,f)\in T_1,f\in F_1,q^{\prime }\in I_2\}\end{array}$

Notation	Explaination
$Q^{\prime }$	Same as Union, we include both automata for concatenation
$I^{\prime }$	We normaly start the the automaton from $I_1$ If $I_1$ is non-empty, otherwise we start at $I_2$
$T^{\prime }$	For any states that can reach the accepting states of $T_1$ with one transition, we create a new transitions that reach the initial states of $T_2$ $(I_2)$

The correctness of this construction is proven by the following theorem.

$$\begin{gathered} \mathbf{\text{Theorem 3.4. }} \\ \mathit{\text{If }}{L}_1\mathit{\text{ is a regular language and }}{L}_2\mathit{\text{ is Büchi-recognizable, then }}{L}_1\cdot L_2\mathit{\text{ is Büchi-recognizable.}} \end{gathered}$$

Explained in Human language

If $I_1$ is non-empty, then we can have a run that starts from $I_1$ to $r(n)$, that is one transition before ${\mathcal{A}}_{\mathcal{1}}$’s accepting states of $f$. Then for next transition we either move to $f$, or we move on to ${\mathcal{A}}_{\mathcal{2}}$ starting from $r(n+1)$.

Previous chapter: $\omega$-regular language

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

In the following we refer the languages recognized by Büchi automata simply as Büchi-recognizable languages. Büchi’s characterization theorem states that the $\omega$-regular languages are exactly Büchi-recognizable languages. To prepare for the proof of Büchi’s theorem, we establish several closure properties of the Büchi-recognizable languages.

Closure Properties of Language Union

$$\begin{gathered} \mathbf{\text{Construction 3.1. }}\text{Let }{L}_1\text{ and }{L}_2\text{ be }\omega \text{-languages recognized by the Büchi automata} \\ {\mathcal{A}}_1=(\mathrm{\Sigma },Q_1,I_1,T_1,\text{BÜCHI}(F_1))\text{ and }{\mathcal{A}}_2=(\mathrm{\Sigma },Q_2,I_2,T_2,\text{BÜCHI}(F_2))\text{, respectively.} \\ \text{We construct}{\mathcal{A}}_{\cup }=(\mathrm{\Sigma },Q_{\cup },I_{\cup },T_{\cup },\text{BÜCHI}(F_{\cup }))\text{ with }\mathcal{L}({\mathcal{A}}_{\cup })=L_1\cup L_2\text{ as follows:} \end{gathered}$$
$\begin{array}{l}\cdot Q_{\cup }=Q_1\cup Q_2(\text{w.l.o.g we assume }{Q}_1\cap Q_2=\varnothing )\\ \cdot I_{\cup }=I_1\cup I_2\cdot T_{\cup }=T_1\cup T_2\cdot F_{\cup }=F_1\cup F_2\end{array}$

The correctness of this construction is proven by the following theorem.

$\mathbf{\text{Theorem 3.2. }}\mathit{\text{If }}{L}_1\mathit{\text{ and }}{L}_2\mathit{\text{ are Büchi-recognizable, then so is }}{L}_1\cup L_2\mathit{\text{.}}$

Formal Proof

We prove that the Büchi automaton ${\mathcal{A}}_{\cup }$ built by ${\mathcal{A}}_1$ and ${\mathcal{A}}_2$ indeed recognizes the union of the languages of the two automata.

$\mathcal{L}({\mathcal{A}}_{\cup })\subseteq \mathcal{L}({\mathcal{A}}_1)\cup \mathcal{L}({\mathcal{A}}_2):$

Previous chapter: Kleene’s Theorem

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

Introduction

$\omega$-regular expression denotes languages over infinite words.
In addition to language union on languages over infinite words, we have 2 operations that convert languages over finite words into languages over infinite words.

$\omega$-regular expression

The collection of $\omega$-regular languages over an alphabet ${\mathrm{\Sigma }}^{\omega }$ is $\mathcal{L}(W)$, where $W$ is a $\omega$-regular expression.
$\omega$-regular expression can be defined as $W:=E^{\omega }\mid E\cdot W\mid W_1+W_2$, where:

• infinite concatenation of a non-empty regular language $E^{\omega }$,
• union of $\omega$-regular languages, $W_1+W_2$, and
• concatenation of regular languages and $\omega$-regular language $E\cdot W$

$\mathbf{\text{Definition 3.3. }}\omega \mathit{\text{-Regular expressions }}\text{are defined as follows:}$
$\begin{array}{l}\cdot \text{If }E\text{ is a regular expression where }\epsilon \notin \mathcal{L}(E)\text{, then }{E}^{\omega }\text{ is an }\omega \text{-regular expression.}\\ \mathcal{L}(E^{\omega })=\mathcal{L}(E{)}^{\omega }\\ \text{where }{L}^{\omega }=\{{\omega }_0{\omega }_1\cdots \mid {\omega }_i\in L,|{\omega }_i|>0\}\text{ for }L\subseteq {\mathrm{\Sigma }}^{\ast }\\ \cdot \text{If }E\text{ is a regular expression and }W\text{ is an }\omega \text{-regular expression,}\\ \text{then }E\cdot W\text{ is an }\omega \text{-regular expression:}\\ \mathcal{L}(E\cdot W)=\mathcal{L}(E)\cdot \mathcal{L}(W)\\ \text{where }{L}_1\cdot L_2=\{\omega \alpha \mid \omega \in L_1,\alpha \in L_2\}\text{ for }{L}_1\subseteq {\mathrm{\Sigma }}^{\ast },L_2\subseteq {\mathrm{\Sigma }}^{\omega }\\ \cdot \text{If }{W}_1\text{ and }{W}_2\text{ are }\omega \text{-regular expressions, then }{W}_1+W_2\text{ is an }\omega \text{-regular expression:}\\ \mathcal{L}(W_1+W_2)=\mathcal{L}(W_1)\cup \mathcal{L}(W_2).\end{array}$

A language over infinite words is $\omega$-regular if it is definable by a $\omega$-regular expression.

---

Previous chapter: The Büchi Acceptance Condition

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

Introduction

Kleene’s theorem states that the set of languages over finite words that can be defined by regular expressions is exactly the set of languages that can be recognized by automata over finite words.

Based on this, we define $\omega$-regular expressions, and finally prove the corresponding theorem for $\omega$-regular languages: Büchi’s characterization theorem.

Regular Expression

Regular expression consist of constants that denote languages of finite words, and
consist of operator symbols that denote operations over these languages.

The collection of regular languages over an alphabet $\mathrm{\Sigma }$ is $\mathcal{L}(E)$, where $E$ is a regular expression.
Regular expression can be defined as $E:=\epsilon \mid \varnothing \mid a\in \mathrm{\Sigma }\mid E+F\mid E\cdot F\mid E^{\ast }$, where:

• empty language: $\epsilon$,
• empty string language: $\varnothing$,
• singleton language: (single letter from alphabet) $a\in \mathrm{\Sigma }$,
• union of regular languages: $E+F$,
• concatenation of regular languages: $E\cdot F$, and
• language with kleene star: $E^{\ast }$.

$\mathbf{\text{Definition 3.1. }}\mathit{\text{Regular expressions }}\text{are defined as follows:}$
$\begin{array}{l}\cdot \text{The constants }\epsilon \text{ and }\varnothing \text{ are regular expressions.}\\ \mathcal{L}(\epsilon )=\{\epsilon \},\mathcal{L}(\varnothing )=\varnothing .\\ \cdot \text{If }a\in \mathrm{\Sigma }\text{ is a symbol, then }a\text{ is a regular expressions.}\\ \mathcal{L}(a)=\{a\}.\\ \cdot \text{If }E\text{ and }F\text{ are regular expressions, then }E+F\text{ is a regular expression:}\\ \mathcal{L}(E+F)=\mathcal{L}(E)\cup \mathcal{L}(F).\\ \cdot \text{If }E\text{ and }F\text{ are regular expressions, then }E\cdot F\text{ is a regular expression:}\\ \mathcal{L}(E\cdot F)=\{uv\mid u\in \mathcal{L}(E),v\in \mathcal{L}(F)\}.\\ \cdot \text{If }E\text{ is a regular expression, then }{E}^{\ast }\text{ is a regular expression.}\\ \mathcal{L}(E^{\ast })=\{u_1{u}_2\dots u_n\mid n\in \mathbb{N},u_i\in \mathcal{L}(E)\text{ for all }0\le i\le n\}.\end{array}$

Previous chapter: Automata over Infinite Words

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

2.3 The Büchi Acceptance Condition

The Büchi Acceptance Condition is given as a set of accepting states $F$.
A run of a Büchi automaton is accepting if some state from this set occurs infinitely often.

Infinite word

For an infinite word $\alpha$ over $\mathrm{\Sigma }$, an Infinity Set of $\alpha$ is denoted as:
$$\text{Inf}(\alpha )=\{\sigma \in \mathrm{\Sigma }\mid \mathrm{\forall }m\in \mathbb{N}.\mathrm{\exists }n\in \mathbb{N}.n\ge m\text{ and }\alpha (n)=\sigma \}$$

Meaning that $\text{Inf}(\alpha )$ is a set of all letters $\sigma$ from the alphabet $\mathrm{\Sigma }$, so that
for all $m$, you can always find $\sigma$ as the n-th letter of $\alpha$ when there exists an $n$ where $n\ge m$.

This denotes the set of all letters of $\mathrm{\Sigma }$ that occur infinitely often in $\alpha$.

Büchi Condition

Previous chapter: Büchi automata (Preliminaries)

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

2.2 Automata over Infinite Words

The operational behavior of an automaton over infinite words is very similar to automaton over finite words:

1. Start with an initial state
2. Automaton constructs a run by reading one letter of the input alphabet at a time, and
   transitioning to a successor state permitted by its transitions.

The major difference between automata over finite and infinite words is the acceptance condition.

$\mathbf{\text{Definition 2.1. }}\text{ An }\mathit{\text{automaton over infinite words }}\text{is a tuple }\mathcal{A}=(\mathrm{\Sigma },Q,I,T,Acc)\text{, where}$
$\begin{array}{l}\cdot \mathrm{\Sigma }\text{ is a finite }\mathit{\text{alphabet}}\\ \cdot Q\text{ is a finite set of }\mathit{\text{states}}\\ \cdot I\subseteq Q\text{ is a subset of }\mathit{\text{initial states}}\\ \cdot T\subseteq Q\times \mathrm{\Sigma }\times Q\text{ is a set of }\mathit{\text{transitions}}\text{, and}\\ \cdot Acc\subseteq Q^{\omega }\text{ is the }\mathit{\text{accepting condition}}\end{array}$

In the following, we refer an automaton over infinite words simply as an automaton.

Runs of Büchi automata

A run in a Büchi automaton has to transition infinitely many times, and starts with the initial state.

Previous chapter: The Logic-Automata Connection

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

2.1 Preliminaries

Basic math notations	Example
Natural numbers	$\mathbb{N}=\{0,1,2,3\dots \}$
Positive Natural numbers	${\mathbb{N}}^{+}=\{1,2,3\dots \}$
Numbers from $n$ to $m$	$[n,m]=\{n,n+1,\dots ,m\}$ For $n,m\in \mathbb{N}$ with $n\le m$
Numbers from $0$ to $m$	$[m]=\{0,1,\dots ,m\}$

$$$$

Alphabet and Letter	Example
Alphabet	a nonempty, finite set of symbols, usually denoted by $\mathrm{\Sigma }$
Letter	elements of an alphabets, denoted by $\sigma$

$$$$

Finite and Infinite Word	Example
Finite Words	concatenation $w=w(0)w(1)\dots w(n-1)$ of finitely many letters of $\mathrm{\Sigma }$
Infinite Words	$\alpha$ (will be explained in chapter 2.3
$n$-th letter of word $w$	$w(n)$ for each $n\in [|w|-1]$
Length of words $w$	$|w|$
set of all finite words	\Sigma^*$
Infinite Words	$\alpha$ (will be explained in chapter 2.3
set of all non-empty finite words	${\mathrm{\Sigma }}^{+}={\mathrm{\Sigma }}^{\ast }\mathrm{\setminus }\{ϵ\}$
set of all infinite words	${\mathrm{\Sigma }}^{\omega }$

$$$$

Language	Example
language over finite words ($\omega$-language)	each subset of ${\mathrm{\Sigma }}^{\ast }$
language over infinite words ($\omega$-language)	each subset of ${\mathrm{\Sigma }}^{\omega }$

Previous chapter: Synthesis

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

Verification or Synthesis

In applications like verification and synthesis, the automata- and game-theoretic machinery is usually “hidden” behind a logical formulation of the problem.

Logics with corresponding Automata

S1S‘s expressiveness exceeds that of LTL, and
S2S‘s expressiveness exceeds that of CTL* (on binary trees)

Logic	Usage	Example
Linear-time temporal logic (LTL)	sets of infinite words	$◻◊{\ell }_1$
Computation-tree logic (CTL / CTL*)	sets of infinite trees	$\mathsf{\text{EF}}{\ell }_1\wedge \mathsf{\text{EF}}{m}_1$
Monadic second-order logic with one successor (S1S)	logic over infinite words	$\mathrm{\forall }x.x\in P\to S(x)\in P$
Monadic second-order logic with two successors (S2S)	logic over infinite binary trees	$\mathrm{\forall }x.x\in P\to S_1(x)\in P\vee S_2(x)\in P$

Explaination

• $◻◊{\ell }_1$
  $P_0$ is infinitely often at location ${\ell }_1$.
• $\mathsf{\text{EF}}{\ell }_1\wedge \mathsf{\text{EF}}{m}_1$
  There exists a computation path in which $P_0$ reaches location ${\ell }_1$, and
  there is a (possibly different) computation path in which $P_1$ reaches location $m_1$.
• $\mathrm{\forall }x.x\in P\to S(x)\in P$
  A (given) set of natural numbers $P$ is either empty, or
  consists of all positions starting from some position of the word.
• $\mathrm{\forall }x.x\in P\to S_1(x)\in P\vee S_2(x)\in P$
  A (given) set of nodes $P$ contains from each node $n\in P$ an entire path starting in $n$.

Previous chapter: Model Checking

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

Synthesis

In synthesis, we check automatically if there exists a program that satisfies a given specification.

If the answer is yes, we construct such a program.

We solve it by determine the winner of a two-player game between a system player and an environment player.

	Task	Goal
System player	choose the outputs of the system	meet the specification
Environment player	choose the inputs of the system	falsify the specification

Therefore, the specification is satisfied if the System player wins.
Such winning strategy can be translated into a program that is guaranteed to satisfy the specification.

Example: coffee machine

In this example, we assume there’s a machine that “outputs coffee” whenever users press a button.

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

Model Checking

Given a system model, we try to check whether it meets its specification automatically and exhaustively.
To describe/represent the system and specification, we use Automata over infinite objects.

Verification Problem

The verification problem can be solved by:

Constructing the intersection of system, with an automaton for the negation of the specification,
then checking whether the language of the resulting automaton is empty.

$\mathbf{\text{Example 1.1. }}\text{Consider the concurrent program }\text{TURN}:$
$$\begin{gathered} \text{local }t\text{: boolean where initially }t\text{ = }false \\ {P}_0::\left[\begin{array}{l}\text{loop forever do}\\ \left[\begin{array}{c}{\ell }_0:\text{await }\mathrm{\neg }t;\\ {\ell }_1:\text{critical;}\\ {\ell }_2:t:=true;\end{array}\right]\end{array}\right]\mid \mid P_1::\left[\begin{array}{l}\text{loop forever do}\\ \left[\begin{array}{c}{m}_0:\text{await }t;\\ m_1:\text{critical;}\\ m_2:t:=false;\end{array}\right]\end{array}\right] \end{gathered}$$

The example above is a simple solution to the mutual exclusion problem:
it ensures that at any given point of time, at most one process is in the critical region.

From Program to automaton

To represent the above program using automaton, we need to define an alphabet $\mathrm{\Sigma }$.