AGV 4.2 -- Complementation of deterministic Büchi Automata

Previous chapter: Deterministic vs. Nondeterministic Büchi Automata

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

Introduction

For regular languages, Complementation is very simple: one translates a given complete deterministic automaton $\mathcal{A}$ that recognizes some language $L\subseteq\Sigma^*$ into an automaton $\mathcal{A’}$ that recognizes the complement $\Sigma^*\setminus L$ by complementing the set of final states, i.e., $F’=Q\setminus F$.

For deterministic Büchi automata, the construction is tricky, because it introduces nondeterminism

$\textbf{Construction 4.1. }\text{Let }\mathcal{A}=(\Sigma,Q,I,T,\small\text{BÜCHI} \normalsize(F))\text{ be a complete deterministic Büchi}$ $\text{automaton, where we assume w.l.o.g. that } Q\neq\varnothing. \text{ We construct a Büchi automaton}$ $\mathcal{A’}=(\Sigma,Q’,I’,T’,\small\text{BÜCHI} \normalsize (F’))\text{ with }\mathcal{L}(\mathcal{A’})=\Sigma^\omega\setminus\mathcal{L}(\mathcal{A})\text{ as follows:}$

$\begin{array}{lrll}
\hspace{1cm} \cdot &Q’&=&(Q\times\lbrace 0\rbrace)\cup((Q\setminus F)\times\lbrace 1\rbrace)\newline
\hspace{1cm} \cdot &I’&=&I\times\lbrace 0\rbrace\newline
\hspace{1cm} \cdot &T’&=&\lbrace ((q,0),\sigma,(q’,i))\mid(q,\sigma,q’)\in T,i\in\lbrace 0,1\rbrace,(q’,i)\in Q’\rbrace \cup \newline
\hspace{1cm} \ &&&\lbrace ((q,1),\sigma,(q’,1))\mid(q,\sigma,q’)\in T,q’,q’\in Q\setminus F\rbrace\newline
\hspace{1cm} \cdot &F’&=&(Q\setminus F)\times\lbrace 1\rbrace
\end{array}$

Explaination
$Q’$ Uses two copies of the given automaton $\mathcal{A}$, mark them seperately using $\lbrace 0\rbrace$ and $\lbrace 1\rbrace$, notice that all accpeting states from $\lbrace 1\rbrace$ are eliminated
$I’$ The complemented automaton starts from initial states from $\lbrace 0\rbrace$.
$T’$ The switch from $\lbrace 0\rbrace$ and $\lbrace 1\rbrace$ happens nondeterministically. And once you enter the second copy $\lbrace 1\rbrace$, it stays forever.
$F’$ The automaton $\mathcal{A’}$ accepts if the run ends up in the second copy, which means that, on the unique run of $\mathcal{A}$ on the input word, the accepting states of $\mathcal{A}$ are only visited finitely often.

Note that the resulting automaton is nondeterministic. This is, in general, unavoidable.

This is because there are languages, such as $L=(b^*a)^\omega$ where the language itself is recognizable by a deterministic Buchi automaton, while its complement $\Sigma^\omega\setminus L$ can only be recognized by a nondeterministic Büchi automaton.

$\textbf{Theorem 4.3. }\textit{For every deterministic Büchi automaton }\mathcal{A}\textit{, there exists a Büchi automaton }\mathcal{A’}$ $\textit{ such that }\mathcal{L}(\mathcal{A’})=\Sigma^\omega \setminus\mathcal{L}(\mathcal{A}).$

Read more

AGV 4.1 -- Deterministic vs. Nondeterministic Büchi Automata

Previous chapter: Büchi’s Characterization Theorem

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

Introduction

In the theory of automata over finite words, we have Rabin-Scott powerset construction, which converts a nondeterministic automaton over finite words into a deterministic automaton that recognizes the same language. This shows that nondeterminism does not make automata over finite words more expressive (but makes it more concise as the construction produces an exponential number of states).

The situation is different for Büchi automata: even though the language $L = (a+b)^*b^\omega$ is clearly Büchi-recognizable, there is, as the following theorem shows, no deterministic Büchi automaton that recognizes L.

Deterministic vs. nondeterministic Büchi automata

$\textbf{Theorem 4.1. }\textit{Language $L=(a+b)^*b^\omega$ is not recognizable by deterministic Büchi Automata}$

Starting a base case $b^\omega$, we add $(a+b)$ as the prefix one by one. Can we express the kleene star?
That is, is the automaton only accept finitely many $(a+b)$?

Proof

Assume, by way of contradiction, that $L$ is recognizable by the deterministic Büchi automaton $\mathcal{A}=(\Sigma,Q,I,T,\small\text{BÜCHI}\normalsize(F))$. Since $\alpha_0=b^\omega$ is in $L$, there is an unique run

Read more

AGV 3.5 -- Büchi's Characterization Theorem

Previous chapter: Closure Properties of the Büchi-recognizable languages (Concatenations)

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

We are now ready to prove Büchi’s Characterization Theorem, a result from 1962.

$\textbf{Theorem 3.6. }\text{(Büchi’s Characterization Theorem) }$ $\textit{An $\omega$-language is Büchi-recognizable iff it is $\omega$-regular.}$

Explained in Human language

p.s. Büchi-recognizable means the language can be described by a Büchi automata.

“$\Leftarrow$”
We have to prove if the language is $\omega$-regular, then it is Büchi-recognizable.
In section 3.2, we learn that an $\omega$-regular language contains 3 operators:

  • union of $\omega$-regular languages, $W_1+W_2$ (proved by Theorem 3.2),
  • infinite concatenation of a non-empty regular language $E^\omega$ (proved by Theorem 3.4), and
  • concatenation of regular languages and $\omega$-regular language $E\cdot W$ (proved by Theorem 3.5)

“$\Rightarrow$”
We have to prove if the language is Büchi-recognizable, then it is $\omega$-regular.
Here, we try to construct a Büchi-recognizable using all $\omega$-regular operators.

We begin by constructing a regular language $W_{q,q’}$. Words of the language $w$ is accepted by some finite-word automata, with a pair of state $q,q’\in Q$ being the initial and accepting states respectively.

Read more

AGV 3.4 -- Closure Properties of the Büchi-recognizable languages (Concatenations)

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

$\textbf{Construction 3.3. } \text{Let }\mathcal{A}_1=(\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 = (\Sigma,Q_2,I_2,T_2,\small\text{BÜCHI}\normalsize (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’}=(\Sigma,Q’,I’,T’,\small\text{BÜCHI}\normalsize (F_2))\text{ with }\mathcal{L}(\mathcal{A’})=L_1\cdot L_2\text{ as follows:}$

$\begin{array}{lrll}
\hspace{1cm} \cdot &Q’&=&Q_1\cup Q_2 \hspace{0.7cm}(\text{w.l.o.g we assume }Q_1\cap Q_2=\varnothing)\newline
\hspace{1cm} \cdot &I’&=&\biggl\lbrace \begin{array}{ll}I_1 & \ \text{if }I_1\cap F_1=\varnothing\newline
I_1\cup I_2 & \ \text{otherwise}\end{array} \newline
\hspace{1cm} \cdot &T’&=&T_1\cup T_2\cup\lbrace (q,\sigma,q’)\mid(q,\sigma,f)\in T_1,f\in F_1,q’\in I_2\rbrace \newline
\end{array}$

Notation Explaination
$Q’$ Same as Union, we include both automata for concatenation
$I’$ We normaly start the the automaton from $I_1$ If $I_1$ is non-empty, otherwise we start at $I_2$
$T’$ 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.

$\textbf{Theorem 3.4. }$ $\text{If }\textit{$L_1$ is a regular language and $L_2$ is Büchi-recognizable, then $L_1\cdot L_2$ is Büchi-recognizable.}$

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_1}$’s accepting states of $f$. Then for next transition we either move to $f$, or we move on to $\mathcal{A_2}$ starting from $r(n+1)$.

Read more

AGV 3.3 -- Closure Properties of the Büchi-recognizable languages (Intersection and Union)

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

$\textbf{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=(\Sigma,Q_1,I_1,T_1,\small\text{BÜCHI}\normalsize (F_1))\text{ and }\mathcal{A}_2 = (\Sigma,Q_2,I_2,T_2,\small\text{BÜCHI}\normalsize (F_2))\text{, respectively.}$ $\text{We construct }\mathcal{A}_\cup=(\Sigma, Q_\cup, I_\cup,T_\cup,\small\text{BÜCHI}\normalsize (F_\cup))\text{ with }\mathcal{L}(\mathcal{A}_\cup)=L_1\cup L_2\text{ as follows:}$
$\begin{array}{l}\newline
\hspace{1cm} \cdot \ Q_\cup=Q_1\cup Q_2 \hspace{1cm}(\text{w.l.o.g we assume }Q_1\cap Q_2=\varnothing)\newline
\hspace{1cm} \cdot \ I_\cup=I_1\cup I_2 \ \hspace{1cm} \cdot \ T_\cup=T_1\cup T_2 \ \hspace{1cm} \cdot \ F_\cup=F_1\cup F_2 \newline
\end{array}$

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

$\textbf{Theorem 3.2. }\text{If }\textit{$L_1$ and $L_2$ are Büchi-recognizable, then so is $L_1\cup L_2$.}$

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

Read more

AGV 3.2 -- $\omega$-regular language

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

$\textbf{Definition 3.3. } \textit{$\omega$-Regular expressions } \text{are defined as follows:}$
$\begin{array}{l}
\hspace{1cm} \cdot \ \text{If $E$ is a regular expression where $\varepsilon\notin\mathcal{L}(E)$, then $E^\omega$ is an $\omega$-regular expression.}\newline
\hspace{1cm} \ \ \mathcal{L}(E^\omega) = \mathcal{L}(E)^\omega\newline
\hspace{1cm} \ \ \text{where } L^\omega =\lbrace \omega_0\omega_1\dots\mid\omega_i\in L,|\omega_i|>0\rbrace \text{ for } L\subseteq\Sigma^* \newline
\hspace{1cm} \cdot \ \text{If $E$ is a regular expression and $W$ is an $\omega$-regular expression,}\newline
\hspace{1cm} \ \ \text{then $E\cdot W$ is an $\omega$-regular expression:}\newline
\hspace{1cm} \ \ \mathcal{L}(E\cdot W) = \mathcal{L}(E)\cdot\mathcal{L}(W)\newline
\hspace{1cm} \ \ \text{where } L_1 \cdot L_2=\lbrace \omega\alpha\mid\omega\in L_1,\alpha\in L_2\rbrace \text{ for } L_1 \subseteq\Sigma^*, L_2 \subseteq\Sigma^\omega\newline
\hspace{1cm} \cdot \ \text{If $W_1$ and $W_2$ are $\omega$-regular expressions, then $W_1+W_2$ is an $\omega$-regular expression:}\newline
\hspace{1cm} \ \ \mathcal{L}(W_1+W_2) = \mathcal{L}(W_1)\cup\mathcal{L}(W_2) .\newline
\end{array}$

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


Read more

AGV 3.1 -- Kleene's Theorem

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 $\Sigma$ is $\mathcal{L}(E)$, where $E$ is a regular expression.
Regular expression can be defined as $E := \varepsilon\mid\varnothing\mid a\in\Sigma\mid E+F\mid E\cdot F\mid E^* $, where:

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

$\textbf{Definition 3.1. } \textit{Regular expressions } \text{are defined as follows:}$
$\begin{array}{l}\hspace{1cm} \cdot \ \text{The constants }\varepsilon\text{ and }\varnothing\text{ are regular expressions.}\newline
\hspace{1cm} \ \ \mathcal{L}(\varepsilon) = \lbrace\varepsilon\rbrace ,\mathcal{L}(\varnothing)=\varnothing.\newline
\hspace{1cm} \cdot \ \text{If }a\in\Sigma\text{ is a symbol, then }a\text{ is a regular expressions.}\newline
\hspace{1cm} \ \ \mathcal{L}(a) = \lbrace a\rbrace .\newline
\hspace{1cm} \cdot \ \text{If }E\text{ and }F\text{ are regular expressions, then }E+F\text{ is a regular expression:}\newline
\hspace{1cm} \ \ \mathcal{L}(E+F) = \mathcal{L}(E)\cup\mathcal{L}(F) .\newline
\hspace{1cm} \cdot \ \text{If }E\text{ and }F\text{ are regular expressions, then }E\cdot F\text{ is a regular expression:}\newline
\hspace{1cm} \ \ \mathcal{L}(E\cdot F) = \lbrace uv\mid u\in\mathcal{L}(E),v\in\mathcal{L}(F)\rbrace.\newline
\hspace{1cm} \cdot \ \text{If }E\text{ is a regular expression, then }E^*\text{ is a regular expression.}\newline
\hspace{1cm} \ \ \mathcal{L}(E^{\ast}) = \lbrace u_1u_2\dots u_n\mid n\in\mathbb{N},u_i\in\mathcal{L}(E)\text{ for all }0\leq i\leq n\rbrace.\end{array}$

Read more

AGV 2.3 -- The Büchi Acceptance Condition

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 $\Sigma$, an Infinity Set of $\alpha$ is denoted as:
$$\text{Inf}(\alpha) = \lbrace\sigma\in\Sigma\mid\forall m\in\mathbb{N}.\exists n\in\mathbb{N}.n\geq m \text{ and } \alpha(n)=\sigma\rbrace$$

Meaning that $\text{Inf}(\alpha)$ is a set of all letters $\sigma$ from the alphabet $\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\geq m$.

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

Büchi Condition

Read more

AGV 2.2 -- Automata over Infinite Words

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.

$\textbf{Definition 2.1. } \text{ An } \textit{automaton over infinite words } \text{is a tuple }\mathcal{A} = (\Sigma,Q,I,T,Acc)\text{, where}$
$\begin{array}{l}
\hspace{1cm} \cdot \ \Sigma \text{ is a finite } \textit{alphabet} \newline
\hspace{1cm} \cdot \ Q \text{ is a finite set of } \textit{states} \newline
\hspace{1cm} \cdot \ I \subseteq Q \text{ is a subset of } \textit{initial states} \newline
\hspace{1cm} \cdot \ T \subseteq Q \times \Sigma \times Q \text{ is a set of } \textit{transitions} \text{, and} \newline
\hspace{1cm} \cdot \ Acc \subseteq Q^\omega \text{ is the } \textit{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.

Read more

AGV 2.1 -- Büchi automata (Preliminaries)

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} = \lbrace 0,1,2,3\dots\rbrace$
Positive Natural numbers $\mathbb{N}^+ = \lbrace 1,2,3\dots\rbrace$
Numbers from $n$ to $m$ $[n,m] = \lbrace n,n+1,\dots,m\rbrace$ For $n,m\in \mathbb{N}$ with $n\leq m$
Numbers from $0$ to $m$ $[m] = \lbrace 0,1,\dots,m\rbrace$

$$$$

Alphabet and Letter Example
Alphabet a nonempty, finite set of symbols, usually denoted by $\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 $\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 $\Sigma^+ = \Sigma^* \backslash \lbrace \epsilon \rbrace$
set of all infinite words $\Sigma^\omega$

$$$$

Language Example
language over finite words ($\omega$-language) each subset of $\Sigma^*$
language over infinite words ($\omega$-language) each subset of $\Sigma^\omega$
Read more
Your browser is out-of-date!

Update your browser to view this website correctly.&npsb;Update my browser now

×