\documentclass[12pt]{article}
\usepackage[utf8]{inputenc}
\usepackage[francais]{babel}
\usepackage{amsmath}
\usepackage{amssymb}
\usepackage{amsthm}
\usepackage{enumitem}
\usepackage{graphicx}
\usepackage{pgf}
\usepackage{tikz}
\usepackage{mathrsfs}
\usepackage{amsfonts}
\usetikzlibrary{chains,automata,arrows,decorations.pathreplacing}

\newcommand{\bigO}[1]{\ensuremath{\mathop{}\mathopen{}\mathcal{O}\mathopen{}\left(#1\right)}}

\title{Les Automates de Büchi}
\author{Jérémy Ledent}
\date{}

\begin{document}
\newcommand{\A}{\ensuremath{\mathcal{A}}}
\newcommand{\B}{\ensuremath{\mathcal{B}}}
\newcommand{\C}{\ensuremath{\mathcal{C}}}
\newcommand{\eqv}{\ensuremath{\sim_{\A}}}

\newtheorem{theo}{Théorème}
\newtheorem{lemme}[theo]{Lemme}

\maketitle


\section{Préliminaires}

Soit $\Sigma$ un alphabet fini.\\
On va s'intéresser à des langages de mots \emph{infinis} sur $\Sigma$. On note $\Sigma^{\omega}$ l'ensemble de tous les mots infinis sur l'alphabet $\Sigma$.
% Définir omega-mot et omega-langage ?

Si $L$ est un langage de mots finis, on note $L^{\omega}$ le langage de mots infinis défini par : 
$$ L^{\omega} = \{ u_0u_1u_2 \ldots u_n \ldots \mid \forall i, u_i \in L \} $$
On étend la grammaire des expressions rationnelles en ajoutant cet opérateur $\omega$ aux opérateurs déjà présents (union, concaténation, étoile). Cela définit récursivement l'ensemble des \emph{$\omega$-expressions}, qui est une extension des expressions régulières (ou langages rationnels).

\begin{enumerate}
\item Donner une $\omega$-expression désignant le langage des mots infinis sur $\Sigma=\{a, b\}$ qui ne contiennent qu'un nombre fini de $a$.
\end{enumerate}

Un \emph{Automate de Büchi Déterministe (DBA)} est donné par un quintuplet $\A = (Q, \Sigma, \delta, q_0, F)$ où :
\begin{itemize}
\item $Q$ est un ensemble fini d'états
\item $\Sigma$ est un alphabet fini
\item $\delta : Q \times \Sigma \rightarrow Q$ est la fonction de transition
\item $q_0$ est un état initial
\item $F \subseteq Q$ est l'ensemble des états finaux
\end{itemize}
Syntaxiquement, un automate de Büchi est identique à un automate fini. La différence réside dans la condition d'acceptation :
on dit que $\A$ accepte un mot infini $u$ si l'on passe une infinité de fois par un état de $F$ sur l'entrée $u$. 
% Flemme de définir correctement un run
On note $L(\A)$ le langage de tous les mots infinis reconnus par $\A$.

\begin{enumerate}[resume]
\item Quel est le langage reconnu par l'automate suivant ?\\
  \begin{tikzpicture}[->,>=stealth',shorten >=1pt,auto,semithick,node distance=2.8cm, /tikz/initial text =]
    \node[initial,state]     (0)                 {$q_0$};
    \node[state]             (1) [right of=0]    {$q_1$};
    \node[accepting,state]   (2) [right of=1]    {$q_2$};
    \path (0) edge [loop above] node {$b$}    (0)
              edge              node {$a$}    (1)
          (1) edge [loop above] node {$a$}    (1)
              edge              node {$b$}    (2)
          (2) edge [bend left]  node {$a, b$} (0);
  \end{tikzpicture}
% Ou autre exemple moins obvious
\end{enumerate}

Comme pour les automates finis, on définit un \emph{Automate de Büchi Non-déterministe (NBA)} en remplaçant la fonction $\delta : Q \times \Sigma \rightarrow Q$ par une relation $\Delta : Q \times \Sigma \times Q$, et on remplace l'état initial $q_0$ par un ensemble d'états initiaux $I$.

\begin{enumerate}[resume]
\item Donner un NBA reconnaissant le langage $(a+b)^* a^{\omega}$.
\item Montrer qu'il n'existe pas de DBA reconnaissant ce langage.
\end{enumerate}


\section{Langages $\omega$-rationnels}

Ainsi, contrairement au cas des automates finis, les NBA sont strictement plus puissants que les DBA. On va maintenant s'intéresser à la classe de langages reconnue par les NBA.

Un \emph{$\omega$-rationnels} est un langage de mots infinis de la forme :
$$ L = \displaystyle \cup_{i = 0}^{n} U_i (V_i)^{\omega} \text{, où } U_i, V_i \text{ sont des langages rationnels.} $$
L'objectif de cette partie est de montrer que les langages reconnus par les NBA sont exactement les langages $\omega$-rationnels.

Soit $\A = (Q, \Sigma, \Delta, I, F)$ un NBA, pour $q,q' \in Q$ on appelle $L_{q,q'}$ le langage \emph{rationnel} reconnu par l'automate fini $(Q, \Sigma, \Delta, \{q\}, \{q'\})$.

\begin{enumerate}[resume]
\item Montrer que
\[ L(\A ) = \cup_{q \in I, q' \in F} L_{q,q'} (L_{q',q'} \setminus \epsilon )^{\omega}. \]
\item Soient $\A = (Q_A, \Sigma, \Delta_A, I_A, F_A)$ et $\B = (Q_B, \Sigma, \Delta_B, I_B, F_B)$ deux NBA, et $\C = (Q_C, \Sigma, \Delta_C, I_C, F_C)$ un automate \emph{fini}. On suppose que $Q_A, Q_B$ et $Q_C$ sont disjoints. Montrer que les langages suivants sont reconnus par des NBA :
\begin{itemize}
\item $L(\A) \cup L(\B)$
\item $L(\C).L(\A)$
\item $L(\C)^{\omega}$ si $\epsilon \notin L(\C)$ \textit{(on pourra supposer d'abord qu'aucune transition de $\Delta_C$ n'arrive sur un état initial de $\C$)}.
\end{itemize}
\item Conclure.
\end{enumerate}


\section{Clôture par complémentation}

L'objectif est maintenant montrer que l'ensemble des langages reconnus par les NBA est clos par complémentation.

Soit $\A = (Q, \Sigma, \delta, I, F)$ un NBA, il faut donc maintenant montrer que le langage $\Sigma^{\omega} \setminus L(\A)$ est reconnu par un NBA.
En fait, on ne va pas construire directement d'automate le reconnaissant : on va montrer qu'il est $\omega$-rationnel. 

Soit la relation $\eqv$ entre les mots \textbf{finis} de $\Sigma^+$ définie comme suit :
$$ u \eqv v \text{ ssi }  \forall p, q \in Q, \left\{\begin{array}{l} p \rightarrow^u q \Leftrightarrow p \rightarrow^v q \\
                                                                      p \rightarrow_F^u q \Leftrightarrow p \rightarrow_F^v q
                                                     \end{array}\right. $$
où on note : 
\begin{itemize} 
\item $p \rightarrow^u q$ : il existe un chemin de $p$ à $q$ dans $\A$ sur l'entrée $u$ ;
\item $p \rightarrow_F^u q$ : il existe un chemin de $p$ à $q$ dans $\A$ sur l'entrée $u$ passant par un état de~$F$.
\end{itemize}

\begin{enumerate}[resume]
\item Montrer que $\eqv$ est bien une relation d'équivalence, et caractériser ses classes d'équivalences en fonction des $L_{q,q'}$ définis plus tôt.
\item Montrer que $\eqv$ a un nombre fini de classes d'équivalences, et que celles-ci sont des langages rationnels.
\end{enumerate}

On va maintenant montrer le lemme suivant :
\begin{lemme}
Tout mot infini $u \in \Sigma^{\omega}$ appartient à un $U.V^{\omega}$, où $U$ et $V$ sont des classes d'équivalence de $\eqv$.
\end{lemme}
On admettra le théorème suivant :
\begin{theo}[Ramsay]
Dans un graphe complet infini où on colore chaque arête avec un ensemble fini de couleurs, il existe un graphe complet infini monochromatique.
\end{theo}
\begin{enumerate}[resume]
\item Démontrer le lemme.\\
 \textit{(indice : considérer les classe d'équivalence comme des ``couleurs'')}
% C'est la question amusante
\item Montrer que pour toutes classes $U$ et $V$, le langage $U.V^{\omega}$ est soit inclus dans $L(\A)$, soit disjoint de $L(\A)$.
\item Conclure.
%\item Question bonus : quelle est la complexité de cette construction en terme de nombre d'états ?
\end{enumerate}

\end{document}