%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %% %% %% 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 \; ij) \longrightarrow \neg X(j)) \, \wedge\\ & \text{(does not contain the last element)}\\ & \forall j\; (\neg \exists k \; (ki \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}