%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%                                                                %%
%%         Automata and Logic (CSC2428)  Lecture 1                %%
%%                                                                %%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%


\documentclass[11pt,titlepage]{article}

%\usepackage{charter}
\usepackage{amsmath}
\usepackage{amssymb}
\usepackage{amsfonts}
\usepackage{exscale}
%\usepackage{calc}
%\usepackage{epsfig}
%\usepackage{url}
%\usepackage{notations}
%\usepackage{longtable}
\setlength{\textwidth}{17cm}
\setlength{\oddsidemargin}{-0.24cm}
\setlength{\evensidemargin}{-0.24cm}
\setlength{\topmargin}{-0.7cm}
\setlength{\headheight}{0cm}
\setlength{\textheight}{23.4cm}
\setlength{\headsep}{0cm}



\title{Automata and Logic (CSC2428) \\ Lecture 1}

\date{January 13, 2005}

\author{Prof. Leonid Libkin \\ notes by Anya Tafliovich}

\begin{document}

\maketitle


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\section{Introduction}
\label{sec:introduction}


Connections between logic and automata, in particular between monadic
second order logic and various finite state machines, date back to the
late 1950s. They helped prove major results about automata and also
led to some of the most powerful techniques for proving decidability
results. More recently, they found applications in a variety of areas,
such as formal methods and databases.


\subsection{Course prerequisites}
\label{sec:prerequisites}

Some knowledge of propositional logic, predicate calculus, and string
automata.


\subsection{Course topics}
\label{sec:topics}

The course covers the basics of the logic / automata connections, and
looks into several CS applications.


We start with the classic results from 1950s --- automata on finite
strings and trees (both ranked and unranked) and relationship  to
monadic second-order logic and first-order logic. We then move to
infinite strings and deal with B\"uchi automata and logics, such as
monadic second-order logic, first-order logic, and linear time logic
for expressing temporal properties over infinite strings. Then we
consider infinite binary trees, monadic second-order logic and Rabin
automata, and prove Rabin's decidability theorem. We derive some
powerful results from it, in particular decidability for pushdown
systems.

The rest depends on how much time we have, but ideally we
should also cover branching time logic, CTL* over infinite binary
trees, alternating automata and the $\mu$-calculus, and automatic
structures over strings and trees.

The topics not covered in the lectures will be left for students'
presentations at the end of the course.


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\section{Automata on finite strings}

A \emph{non-deterministic finite state automaton} (NFA) $\mathcal{A}$
is a tuple
%
\begin{equation*}
\label{eq:nfa}
\mathcal{A} = ( \Sigma, Q, q_0, F, \delta) \text{, where}
\end{equation*}
%
\begin{enumerate}
\item $\Sigma$ is an alphabet \\
      Note: $\Sigma^*$ is a set of (finite) strings over $\Sigma$
\item $Q$ is a set of states
\item $q_0$ is an initial state
\item $F$ is a set of final states
\item $\delta : Q \times \Sigma \rightarrow 2^Q$ is a transition function
\end{enumerate}

\noindent
If $s$ is a string of length $n$, then $\lambda_s$ is a
\emph{labeling function} from positions to members of the alphabet,
$\lambda_s : \{0,\hdots,n-1\} \rightarrow \Sigma$ .\\

\noindent
For example, if $s$ is the string $abaaba$, then the labeling
function labels $\lambda_s(0)=a$ , $\lambda_s(1)=b$ , etc.\\

\noindent
Then the string can be represented by a tuple
$ S = ( \{0, \hdots, n-1\}, \lambda_s ) $ . \\

\noindent
A \emph{run} $\rho_{\mathcal{A}, S} : \{0,\hdots,n-1 \} \rightarrow Q$
of automaton $\mathcal{A}$ on a string $S$ is:
%
\begin{align*}
\label{eq:run}
& \rho_{\mathcal{A}, S} (0) \in \delta(q_0, \lambda_s(0)) \\
& \rho_{\mathcal{A}, S} (i+1) \in 
   \delta (\rho_{\mathcal{A}, S}(i), \lambda_s(i+1))
\end{align*}


\noindent
A run $\rho_{\mathcal{A}, S}$ is \emph{accepting} iff 
$\rho_{\mathcal{A}, S}(n-1) \in F$ .\\

\noindent
An automaton $\mathcal{A}$ \emph{accepts} a string $S$ iff there
exists an accepting run of $\mathcal{A}$ on $S$ .\\

\noindent
The \emph{language} accepted by automaton $\mathcal{A}$ is
$L(\mathcal{A}) = \{ s \in \Sigma^* \; | \; \mathcal{A} \text{
  accepts } s \}$ . \\

\noindent
An automaton $\mathcal{A}$ is \emph{deterministic} iff
\begin{equation*}
\label{eq:dfa}
\forall q \in Q \; \forall a \in \Sigma \;\; | \delta(q,a) | \leq 1
\end{equation*}
i. e. for each $s \in \Sigma^*$, there is exactly one run
$\rho_{\mathcal{A}, S}$ . Note that a transition function of a DFA is
$\delta : Q \times \Sigma \rightarrow Q$ . \\


\noindent
\textbf{Result}: NFA = DFA (i.e. they accept exactly the same
languages).\\

\noindent
\textbf{Theorem}:
If $\mathcal{A}$ in an NFA then there is a DFA $\mathcal{A'}$, such that
$L(\mathcal{A}) = L(\mathcal{A'})$ .\\

\noindent
\textbf{Proof (Power-set construction)}:\\
Suppose $\mathcal{A} = (\Sigma, Q, q_0, F, \delta)$, then we construct
$\mathcal{A'}$ as follows:
%
\begin{alignat*}{2}
\label{eq:powerset}
 & \mathcal{A'} = ( \Sigma, 2^Q, \{q_0\}, F', \delta') \text{, where}\qquad
  && F'=\{ X \subseteq Q\; | \;  X \cap F \neq \emptyset \} \\
 &&& \delta' : 2^Q \times \Sigma \rightarrow 2^Q \; , \;
   \delta'(X,a) = \underset{q \in X}{\bigcup} \delta(q,a)
\end{alignat*}


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\section{Logic background}
\label{sec:logic}


\subsection{First-order predicate calculus (FO)}
\label{sec:fo}

\subsubsection{Syntax}
\label{sec:fosyntax}

\noindent
A \emph{vocabulary} $\sigma$ is:
\begin{enumerate}
\item function symbols: $f_1, f_2, \hdots$ of non-negative arities
  $m_1, m_2, \hdots$
\item constant symbols (zero-ary function symbols): $c_1, c_2, \hdots$ 
\item predicate symbols: $P_1, P_2, \hdots$ of positive arities $n_1,
  n_2, \hdots$
\end{enumerate}

\noindent
FO \emph{terms} and FO \emph{formulae}:
\noindent
\\(assume an infinite supply of variables)

\begin{enumerate}
% terms
\item each variable $x$ is a term\\
  Free variables (FV) : $x$
\item if $t_1, \hdots, t_k$ are terms and $f$ is a $k$-ary function
  symbol, then $f(t_1, \hdots, t_k)$ is a term\\
  FV : $\underset{i}{\bigcup}$ FV($t_i$)
\item each constant symbol $c_i$ is a term\\
  FV : none

% formulae
\item if $t_1, \hdots, t_k$ are terms and $P$ is a $k$-ary predicate symbol,
  then $P(t_1, \hdots, t_k)$ is an \emph{atomic} formula\\
  FV : $\underset{i}{\bigcup}$ FV($t_i$)
\item if $t$ and $t'$ are terms, then $t=t'$ is a formula\\
  FV : FV($t$) $\cup$ FV($t'$)
\item if $\phi$ and $\psi$ are formulae and $x$ is a variable, then
  $\phi \wedge \psi$, $\phi \vee \psi$, $\neg \phi$, $\exists x
  \phi$, and $\forall x \phi$ are formulae\\
  FV : FV($\phi$) $\cup$ FV($\psi$), FV($\phi$) $\cup$ FV($\psi$),
  FV($\phi$), FV($\phi$) - $x$, and FV($\phi$) - $x$, respectively

\end{enumerate}


%-----------------------------------------------------------------------

\subsubsection{Semantics (Tarski semantics)}
\label{sec:fosem}

\noindent
An \emph{interpretation} (or a \emph{structure}) $\mathcal{M}$ is:
\begin{equation*}
\label{eq:fo_int}
  \mathcal{M} = (U, f_1^\mathcal{M}, f_2^\mathcal{M}, \hdots,
  c_1^\mathcal{M},  c_2^\mathcal{M}, \hdots, 
  P_1^\mathcal{M}, P_2^\mathcal{M}, \hdots )
\end{equation*}
where
\begin{enumerate}
\item $U$ is the \emph{universe}: a non-empty set
\item $f_i^{\mathcal{M}} : U^{n_i} \rightarrow U$, where $n_i$ is the
  arity of the function symbol $f_i$
\item $c_i^\mathcal{M} \in U$
\item $P_i^\mathcal{M}$ of arity $n_i$ is a subset of $U^{n_i}$
\end{enumerate}

\noindent
Each term $t(\overline{x})$, where $|\overline{x}|=m$, is assigned an
element $t^\mathcal{M}(\overline{a}) \in U$, where $\overline{a} \in U^{m}$
is defined by a corresponding object assignment.\\

\noindent
For a formula $\psi$, $\mathcal{M} \vDash \psi$, meaning $\mathcal{M}$
\emph{satisfies} $\psi$, (under some object assignment) is defined by:

\begin{enumerate}
\item $\mathcal{M} \vDash t_1(\overline{a}) = t_2(\overline{a})$ iff
  $t_1^{\mathcal{M}}(\overline{a}) = t_2^{\mathcal{M}}(\overline{a})$

\item $\mathcal{M} \vDash P(t_1(\overline{a}),\hdots,t_k(\overline{a}))$
  iff
  $(t_1^{\mathcal{M}}(\overline{a}),\hdots,t_k^{\mathcal{M}}(\overline{a}))
    \in P^\mathcal{M}$

\item $\mathcal{M} \vDash \neg \psi$ iff $\mathcal{M} \nvDash \psi$

\item $\mathcal{M} \vDash \psi \wedge \phi$ iff 
  $\mathcal{M} \vDash \psi$ and $\mathcal{M} \vDash \phi$

\item $\mathcal{M} \vDash \psi \vee \phi$ iff 
  $\mathcal{M} \vDash \psi$ or $\mathcal{M} \vDash \phi$

\item $\mathcal{M} \vDash \exists x \; \psi(\overline{a}, x)$ iff 
  $\mathcal{M} \vDash \psi(\overline{a}, b)$ for some $b \in U$

\item $\mathcal{M} \vDash \forall x \; \psi(\overline{a}, x)$ iff 
  $\mathcal{M} \vDash \psi(\overline{a}, b)$ for every $b \in U$
\end{enumerate}


%=======================================================================

\subsection{Representing strings as structures}

To represent a string by a structure, we define a vocabulary:
\begin{enumerate}
\item a binary predicate symbol $<$ and
\item predicate symbols $P_a, P_b, \hdots$ for every $a, b, \hdots \in
  \Sigma$
\end{enumerate}

\noindent
A string $s \in \Sigma^*$, $|s|=n$, is then represented by the
following structure $\mathcal{M}_s$:
%
\begin{alignat*}{2}
  &\mathcal{M}_s = (U,
                    <^{\mathcal{M}_s},
                    P_a^{\mathcal{M}_s}, P_b^{\mathcal{M}_s}, \hdots)
   \text{, where  } && U = \{0, \hdots, n-1\},\\
  &&& <^{\mathcal{M}_s} \text{ is a binary } < \text{ on numbers, and}\\
  &&&  P_a^{\mathcal{M}_s} = 
      \{ i \leq n-1 | a \text{ occurs in position } i \text{ in }s \}
\end{alignat*}

\noindent
For example, consider a string $abaab$. The structure $\mathcal{M}$
corresponding to this string is:
\begin{alignat*}{2}
  &( \{0,1,2,3,4\}, < , P_a, P_b ) 
        \text{,  where  } &&P_a = \{0,2,3\} \text{ and}\\
  &                       &&P_b = \{1,4\}  
\end{alignat*}


\noindent
Consider another example. A property ``$a$ occurs before $b$ in a
string'' can be represented by the following FO formula:
$$ \exists i \; \exists j \; i<j \wedge P_a(i) \wedge P_b(j)$$  

\noindent
A property ``every $a$ must be preceded by a $b$ in a string'' can be
represented by the following FO formula:
$$ \forall i \; P_a(i) \longrightarrow \exists j<i \; P_b(j) $$
where we use the symbol $\longrightarrow$ for material implication
(i.e. $(A \longrightarrow B) = (\neg A \vee B)$).


%=======================================================================

\subsection{Monadic second-order logic (MSO)}
\label{sec:mso}

Monadic second order logic adds quantification over sets to
first-order calculus.

\subsubsection{Syntax}
\label{sec:msosyntax}

We add \emph{second-order variables}, i.e. variables that range over
subsets of the universe, to the vocabulary of FO. We denote second-order 
variables by capital letters.\\

\noindent
MSO terms and MSO formulae:
\begin{enumerate}
\item all FO terms and all FO formulae
\item if $X$ is a second-order variable and $t$ is a term, then $X(t)$
  is a formula
\item if $\psi$ is a formula, then $\exists X \psi$ and $\forall X
  \psi$ are also formulae
\end{enumerate}

%-----------------------------------------------------------------------

\subsubsection{Semantics}
\label{sec:msosem}

We have an interpretation (or a structure) $\mathcal{M}$, as before.\\

\noindent
Each term $t(\overline{x})$, where $|\overline{x}|=m$ is assigned an
element $t^\mathcal{M}(\overline{a}) \in U$, where $\overline{a} \in U^{m}$
is defined by a corresponding object assignment.\\

\noindent
Each formula $\psi(\overline{x}, \overline{X})$, where
$|\overline{X}|=m$, is assigned an element $\psi(\overline{a},
\overline{S})$, where $\overline{S}=(S_1,\hdots,S_m)$, $S_i \subseteq
U$ is defined by a corresponding object assignment.\\

\noindent
For a formula $\psi$, $\mathcal{M} \vDash \psi$, meaning $\mathcal{M}$
\emph{satisfies} $\psi$, (under some object assignment) is defined by:

\begin{enumerate}
\item all rules from FO

\item for $\psi(\overline{x},X) = X(t(\overline{x}))$, 
  $\mathcal{M} \vDash \psi (\overline{a}, S)$ iff 
  $t^{\mathcal{M}}(\overline{a}) \in S$
  
\item $\mathcal{M} \vDash \exists X \; \psi(X, \hdots)$ iff there exists
  some $X \subseteq U$, such that $\mathcal{M} \vDash \psi (S, \hdots)$

\item $\mathcal{M} \vDash \forall X \; \psi(X, \hdots)$ iff for every
  $X \subseteq U$, $\mathcal{M} \vDash \psi (S, \hdots)$
\end{enumerate}


\noindent
Consider the following example:

Given a regular expression $(aa)^*$, find a sentence $\psi \in
MSO$, such that $s \in L((aa)^*) \text{ iff } \mathcal{M}_s \vDash
\psi$.
%
\begin{align*}
 \psi =\!=
   \forall i \; P_a(i) \wedge \exists X \; 
   & \forall j\; (\neg \exists k \; (k>j) \longrightarrow \neg X(j)) \, \wedge\\
   & \text{(does not contain the last element)}\\
   & \forall j\; (\neg \exists k \; (k<j) \longrightarrow X(j)) \, \wedge\\
   &\text{(contains the first element)}\\
   &\forall i,j\; (j>i \wedge \forall k(j>k \longrightarrow i \geq k)
     \longrightarrow (X(j) \longleftrightarrow \neg X(i)))\\
   &\text{(contains every other element)}\\
\end{align*}


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%


\section{B\"uchi 1959 results}
\label{sec:buchi59}

A language $L \subseteq \Sigma^*$ is \emph{definable} in a logic
$\mathcal{L}$ if there is a sentence $\psi$ of $\mathcal{L}$, such
that
\begin{equation*}
  L = \{ s \in \Sigma^* \; | \; \mathcal{M}_s \vDash \psi \} = L(\psi)
\end{equation*}

\noindent
For example, if $\psi$ is the formula from the above example, then
$L(\psi) = L ( (aa)^* )$.\\


\noindent
\textbf{Theorem (B\"uchi 1959)}:
\noindent
A language is regular iff it is definable in MSO.\\

\noindent
\textbf{Proof 1 (easy direction)}:\\

\noindent
Here we prove that a regular language is definable in MSO: given a
regular language $L \subseteq \Sigma^*$, we need to construct a
sentence $\psi \in MSO$, such that $L = L(\psi)$.\\

\noindent
Recall that a language is regular iff it is accepted by some DFA.\\
Let $\mathcal{A} = (\Sigma, Q, q_0, F, \delta)$ be a DFA, such that
$L(\mathcal{A}) = L$.

\noindent
We now produce $\psi_{\mathcal{A}}$, such that $\mathcal{M}_s \vDash
\psi_{\mathcal{A}}$ iff a (unique) run of $\mathcal{A}$ on $s$ ends in
an accepting state, i.e. $\mathcal{A}$ accepts $s$. Assume that
$Q=\{q_0,\hdots,q_{k-1}\}$. Then

\begin{align*}
 \psi_{\mathcal{A}} =\!= & \exists X_0,\hdots,X_{k-1} \\
   &\forall x 
   \left(  
     \underset{i=0}{\overset{k-1}{\bigvee}} X_i(x) \wedge
     \neg \underset{i\neq j}{\bigvee} \exists (X_i(x) \wedge X_j(x))
   \right)\\
   &\text{($X_i$'s partition the universe)}\\
   \wedge\;\; &\forall x 
   \left (
     (\forall y \; x \leq y) \longrightarrow 
     \underset{a \in \Sigma}{\bigwedge} (P_a(x) \longrightarrow X_i(x))
   \right)
     \text{ , where } q_i = \delta(q_0,a)\\
   &\text{(position $0$ is in $X_i$, where $q_i=\delta(q_0,a)$,
           where $a$ is the first symbol)}\\
   \wedge\;\; & \forall x \forall y 
     \left (
       (x < y \wedge \neg \exists z (x < z \wedge z < y))
       \longrightarrow
       \underset{\underset{i \leq k}{a \in \Sigma}}{\bigwedge}
       (X_i(x) \wedge P_a(y) \longrightarrow X_j(y))
     \right)\\
    &\qquad \text{ , where } q_j = \sigma(q_i, a)\\
   &\text{(if position $m$ is in $X_i$, the symbol in position $m+1$}\\
   &\text{is $a$, then position $m+1$ is in $X_j$, where $q_j=\delta(q_i, a)$)}\\
   \wedge\;\; & \forall x
   \left(
     \forall y (y \leq x) \longrightarrow \underset{q_i \in
       F}{\bigvee} X_i(x)
   \right)\\
   &\text{(if $m$ is the last position, then $m \in X_i$, where $q_i \in F$)}
\end{align*}


\noindent
\textbf{Proof 2 (hard direction)}:\\

\noindent
Here we prove that a language definable in MSO is regular. There are
two complications: $(1)$ we have two kinds of variables (first- and
second-order) and $(2)$ we cannot do induction on sentences (not
formulae!)

\noindent
We cope with the first complication by introducing MSO$_0$, in which:
\begin{enumerate}
\item all variables are second-order
\item $Sng(X)$ iff $|X|=1$
\item $Less(X, Y)$ iff $X={x}$, $Y={y}$, and $x < y$
\item $ X \subseteq Y $
\end{enumerate}

\noindent
Fact: MSO = MSO$_0$\\

\noindent
We will deal with the second complication in the next lecture
\end{document}

