\project thesis
\startcomponent learning-nominal-automata

\startchapter
  [title={Learning Nominal Automata},
   reference=chap:learning-nominal-automata]

\todo{Auteurs en moet ik ook support noemen van de andere auteurs? Keywords?}

\startabstract
We present an Angluin-style algorithm to learn nominal automata, which are acceptors of languages over infinite (structured) alphabets.
The abstract approach we take allows us to seamlessly extend known variations of the algorithm to this new setting.
In particular we can learn a subclass of nominal non-deterministic automata.
An implementation using a recently developed Haskell library for nominal computation is provided for preliminary experiments.
\stopabstract


\startsection
  [title={Introduction}]

Automata are a well established computational abstraction with a wide range of applications, including modelling and verification of (security) protocols, hardware, and software systems.
In an ideal world, a model would be available before a system or protocol is deployed in order to provide ample opportunity for checking important properties that must hold and only then the actual system would be synthesized from the verified model.
Unfortunately, this is not at all the reality:
Systems and protocols are developed and coded in short spans of time and if mistakes occur they are most likely found after deployment.
In this context, it has become popular to infer or learn a model from a given system just by observing its behaviour or response to certain queries.
The learned model can then be used to ensure the system is complying to desired properties or to detect bugs and design possible fixes.

Automata learning, or regular inference, is a widely used technique for creating an automaton model from observations.
The original algorithm by \cite[authoryears][DBLP:journals/iandc/Angluin87] works for deterministic finite automata, but since then has been extended to other types of automata, including Mealy machines and I/O automata (see \cite[left=,right=,righttext={\sectionmark 8.5}][DBLP:phd/de/Niese2003] and \cite[left=,right=][DBLP:conf/concur/AartsV10]), and even a special class of context-free grammars.
\todo{Deze nog citeren \cite[DBLP:conf/colt/AngluinC97]?}
Angluin's algorithm is sometimes referred to as {\em active learning}, because it is based on direct interaction of the learner with an oracle (\quotation{the Teacher}) that can answer different types of queries.
This is in contrast with \emph{passive} learning, where a fixed set of positive and negative examples is given and no interaction with the system is possible.

In this paper, staying in the realm of active learning, we will extend Angluin's algorithm to a richer class of automata.
We are motivated by situations in which a program model, besides control flow, needs to represent basic data flow, where data items are compared for equality (or for other theories such as total ordering).
In these situations, values for individual symbols are typically drawn from an infinite domain and automata over \emph{infinite alphabets} become natural models, as witnessed by a recent trend \cite[DBLP:conf/dlt/BolligHLM13, DBLP:conf/ictac/AartsFKV15,DBLP:conf/popl/DAntoniV14, DBLP:journals/corr/BojanczykKL14, DBLP:journals/fac/CasselHJS16].

One of the foundational approaches to formal language theory for infinite alphabets uses the notion of nominal sets \cite[DBLP:journals/corr/BojanczykKL14].
The theory of nominal sets originates from the work of Fraenkel in 1922, and they were originally used to prove the independence of the axiom of choice and other axioms.
They have been rediscovered in Computer Science by Gabbay and Pitts \cite[Pitts13], as an elegant formalism for modeling name binding, and since then they form the basis of many research projects in the semantics and concurrency community.
In a nutshell, nominal sets are infinite sets equipped with symmetries which make them finitely representable and tractable for algorithms.
We make crucial use of this feature in the development of a learning algorithm. 

Our main contributions are the following.
\startitemize
\item A generalization of Angluin's original algorithm to nominal automata.
The generalization follows a generic pattern for transporting computation models from finite sets to nominal sets, which leads to simple correctness proofs and opens the door to further generalizations.
The use of nominal sets with different symmetries also creates potential for generalization, e.g., to languages with time features \cite[DBLP:conf/icalp/BojanczykL12] or data dependencies represented as graphs \cite[DBLP:journals/tcs/MontanariS14]. 
\item An extension of the algorithm to nominal non-deterministic automata (nominal NFAs).
To the best of our knowledge, this is the first learning algorithm for non-deterministic automata over infinite alphabets.
It is important to note that, in the nominal setting, NFAs are strictly more expressive than DFAs.
We learn a subclass of the languages accepted by nominal NFAs, which includes all the languages accepted by nominal DFAs.
The main advantage of learning NFAs directly is that they can provide exponentially smaller automata when compared to their deterministic counterpart.
This can be seen both as a generalization and as an optimization of the algorithm.
\item An implementation using our recently developed Haskell library tailored to nominal computation -- NLambda \cite[DBLP:journals/corr/KlinS16].
Our implementation is the first non-trivial application of a novel programming paradigm of functional programming over infinite structures, which allows the programmer to rely on convenient intuitions of searching through infinite sets in finite time. 
\stopitemize

The paper is organized as follows.
In \in{Section}[sec:overview], we present an overview of our contributions (and the original algorithm) highlighting the challenges we faced in the various steps.
In \in{Section}[sec:prelim], we revise some basic concepts of nominal sets and automata.
\in{Section}[sec:nangluin] contains the core technical contributions of our paper: The new algorithm and proof of correctness.
In \in{Section}[sec:nondet], we describe an algorithm to learn nominal non-deterministic automata.
\in{Section}[sec:impl] contains a description of NLambda, details of the implementation, and results of preliminary experiments.
\in{Section}[sec:related] contains a discussion of related work. We conclude the paper with a discussion section where also future directions are presented. 

\stopsection
\startsection
  [title={Overview of the Approach},
   reference=sec:overview]

In this section, we give an overview of the work developed in the paper through examples.
We will start by explaining the original algorithm for regular languages over finite alphabets, and then explain the challenges in extending it to nominal languages.

Angluin's algorithm \LStar{} provides a procedure to learn the minimal DFA accepting a certain (unknown) language $\lang$.
The algorithm has access to a \emph{teacher} which answers two types of queries:
\startitemize
\item \emph{membership queries}, consisting of a single word $w \in A^{\ast}$, to which the teacher will reply whether $w \in \lang$ or not;
\item \emph{equivalence queries}, consisting of a hypothesis DFA $H$, to which the teacher replies {\bf yes} if $\lang(H) = \lang$, and {\bf no} otherwise, providing a counterexample $w \in \lang(H) \triangle \lang$ ($\triangle$ denotes the symmetric difference of two languages).
\stopitemize
The learning algorithm works by incrementally building an {\em observation table}, which at each stage contains partial information about the language $\lang$.
The algorithm is able to fill the table with membership queries.
As an example, and to set notation, consider the following table (over $A=\{a, b\}$).

\starttikzpicture
\matrix[matrix of nodes](tab)
{
 \phantom{$\epsilon$} & {$\epsilon$} & $a$ & $aa$ \\
 $\epsilon$ & $0$ & $0$ & $1$ \\
 $a$ & $0$ & $1$ & $0$ \\
 $b$ & $0$ & $0$ & $0$ \\
};
\draw (tab-1-1.south west) -| (tab-1-4.south east);
\draw (tab-2-1.south west) -| (tab-2-4.south east);
\draw (tab-1-1.north east) -| (tab-4-1.south east);
\draw[decorate, decoration=brace] (tab-1-2.north) -- node[above]{$E$} (tab-1-4.north) ;
\draw[decorate, decoration=brace] (tab-4-1.west) -- node[left]{$S \cup S \Lext A$} (tab-2-1.west);

\node[fit=(tab-2-2)(tab-2-3)(tab-2-4), dotted, draw, inner sep=-2pt] (r1) {};
\node[fit=(tab-3-2)(tab-3-3)(tab-3-4), dotted, draw, inner sep=-2pt] (r2) {};
\node[fit=(tab-4-2)(tab-4-3)(tab-4-4), dotted, draw, inner sep=-2pt] (r3) {};

\node[right=1cm of tab](row){$row \colon S \cup S \Lext A \to 2^E$};
\node[below=0em of row](rowd){$row(u)(v) = 1 \iff uv \in \lang$};

\draw[->, shorten >=10pt, dotted] (r1.east) -- (row.west);
\draw[->, shorten >=10pt, dotted] (r2.east) -- (row.west);
\draw[->, shorten >=10pt, dotted] (r3.east) -- (row.west);
\stoptikzpicture

This table indicates that $\lang$ contains at least $aa$ and definitely does not contain the words $\epsilon, a, b, ba, baa, aaa$.
Since $row$ is fully determined by the language $\lang$, we will from now on refer to an observation table as a pair $(S,E)$, leaving the language $\lang$ implicit.

Given an observation table $(S,E)$ one can construct a deterministic automaton $M(S,E) = (Q,q_0,\delta,F)$ where
\startitemize
\item $Q = \{row(s)\mid s\in S\}$ is a finite set of states;
\item $F = \{ row (s) \mid s\in S, row(s)(\epsilon)=1\} \subseteq Q$ is the set of final states;
\item $q_0 = row(\epsilon)$ is the initial state;
\item $\delta\colon Q\times A \to Q$ is the transition function given by $\delta(row(s),a) = row(sa)$.
\stopitemize
For this to be well-defined, we need to have $\epsilon \in S$ (for the initial state) and $\epsilon \in E$ (for final states), and for the transition function there are two crucial properties of the table that need to hold:
Closedness and consistency.
An observation table $(S,E)$ is {\em closed} if for all $t\in S \Lext A$ there exists an $s \in S$ such that $row(t) = row(s)$.
An observation table $(S,E)$ is {\em consistent} if, whenever $s_1$ and $s_2$ are elements of $S$ such that $row(s_1) = row(s_2)$, for all $a \in A$, $row(s_1 a) = row(s_2 a)$.
Each time the algorithm constructs an automaton, it poses an equivalence query to the teacher.
It terminates when the answer is {\bf yes}, otherwise it extends the table with the counterexample provided.

\startplacealgorithm[title={The \LStar{} learning algorithm from \cite[authoryears][DBLP:journals/iandc/Angluin87].}, reference=alg:alg]
\startalgorithmic
\startlinenumbering
\STATE $S,E \gets \{\epsilon\}$ 
\REPEAT
	\WHILE{$(S, E)$ is not closed or not consistent\someline[line:checks]}
		\IF{$(S, E)$ is not closed\someline[line:begin-closed]}
		\STATE find $s_1\in S$, $a \in A$ such that
		\STATE \hfill $row(s_1a) \neq row(s)$ for all $s\in S$\someline[line:clos-witness]
		\STATE $S\gets S\cup \{s_1a\}$ \someline[line:addrow-clos]
		\ENDIF\someline[line:end-closed]
		\IF{$(S, E)$ is not consistent\someline[line:begin-const]}
		\STATE find $s_1, s_2 \in S$, $a \in A$, and $e\in E$ such that
		\STATE \hfill $row(s_1) = row(s_2)$ and $\lang(s_1 a e) \neq \lang(s_2 a e)$\someline[line:cons-witness]
		\STATE $E\gets E\cup \{ae\}$
		\ENDIF
	\ENDWHILE\someline[line:end-const]
	\STATE Make the conjecture $M(S,E)$\someline[line:conj]
	\IF{the Teacher replies {\bf no}, with a counter-example $t$\someline[line:counter-ex]}
	\STATE $S\gets S\cup pref(t)$ \someline[line:addrow-ex]
	\ENDIF
\UNTIL{the Teacher replies {\bf yes} to the conjecture $M(S,E)$}
\RETURN $M(S,E)$
\stoplinenumbering
\stopalgorithmic
\stopplacealgorithm

\startsubsection
  [title={Simple Example of Execution},
   reference=sec:execution_example_original]

Angluin's algorithm is displayed in \in{Algorithm}[alg:alg]. Throughout this section, we will consider the language(s)
\startformula
\lang_n = \left{ ww \mid w \in A^{\ast}, |w| = n \right}
\stopformula
If the alphabet $A$ is finite then $\lang_n$ is regular for any $n \in \N$, and there is a finite DFA accepting it. 

The language $\lang_1 = \{ aa , bb \}$ looks trivial, but the minimal DFA recognizing it has as many as 5 states.
Angluin's algorithm will terminate in (at most) 5 steps.
We illustrate some relevant ones.

\startstep{1}
We start from $S, E = \{\epsilon\}$, and we fill the entries of the table below by asking membership queries for $\epsilon$, $a$ and $b$.
The table is closed and consistent, so we construct the hypothesis $\autom_1$.
\todo{tikz \tt 134-155}

The Teacher replies {\bf no} and gives the counterexample $aa$, which is in $\lang_1$ but it is not accepted by $\autom_1$.
Therefore, line 12 of the algorithm is triggered and we set $S \gets S \cup \{a, aa\}$.
\stopstep

\startstep{2}
The table becomes the one on the left below.
It is closed, but not consistent:
Rows $\epsilon$ and $a$ are identical, but appending $a$ leads to different rows, as depicted.
Therefore, line 9 is triggered and an extra column $a$, highlighted in red, is added.
The new table is closed and consistent and a new hypothesis $\autom_2$ is constructed.
\todo{tikz \tt 163-219}

The Teacher again replies {\bf no} and gives the counterexample $bb$, which should be accepted by $\autom_2$ but it is not. Therefore we put $S \gets S \cup \{b,bb\}$.
\stopstep

\startstep{3}
The new table is the one on the left.
It is closed, but $\epsilon$ and $b$ violate consistency, when $b$ is appended.
Therefore we add the column $b$ and we get the table on the right, which is closed and consistent.
The new hypothesis is $\autom_3$.
\todo{tikz \tt 228-296}

The Teacher replies {\bf no} and provides the counterexample $babb$, so $S \gets S \cup \{ba,bab\}$.
\stopstep

\startstep{4}
One more step brings us to the correct hypothesis $\autom_4$ (details are omitted).
\todo{tikz \tt 304-323}
\stopstep

\stopsubsection
\startsubsection
  [title={Learning Nominal Languages},
   reference=ssec:nom-learning]

Consider now an infinite alphabet $A = \{a,b,c,d,\dots\}$.
The language $\lang_1$ becomes $\{aa,bb,cc,dd,\dots\}$.
Classical theory of finite automata does not apply to this kind of languages, but one may draw an infinite deterministic automaton that recognizes $\lang_1$ in the standard sense:
\todo{tikz \tt 330-355}

where $\xrightarrow{A}$ and $\xrightarrow{\neq a}$ stand for the infinitely-many transitions labelled by elements of $A$ and $A \setminus \{a\}$, respectively.
This automaton is infinite, but it can be finitely presented in a variety of ways, for example:
\todo{tikz \tt 361-378}

One can formalize the quantifier notation above (or indeed the \quotation{dots} notation above that) in  several ways.
A popular solution is to consider finite {\em register automata} \cite[DBLP:journals/tcs/KaminskiF94, DBLP:journals/tocl/DemriL09], i.e., finite automata equipped with a finite number of registers where alphabet letters can be stored and later compared for equality.
Our language $\lang_1$ is recognized by a simple automaton with four states and one register.
The problem of learning registered automata has been successfully attacked before
\cite[DBLP:conf/vmcai/HowarSJC12].

In this paper, however, we will consider nominal automata \cite[DBLP:journals/corr/BojanczykKL14] instead.
These automata ostensibly have infinitely many states, but the set of states can be finitely presented in a way open to effective manipulation.
More specifically, in a nominal automaton the set of states is subject to an action of permutations of a set $\EAlph$ of {\em atoms}, and it is finite up to that action.
For example, the set of states of $\autom_5$ is:
\startformula
\{q_0,q_3,q_4\} \cup \{q_a \mid a\in A\}
\stopformula
and it is equipped with a canonical action of permutations $\pi \colon \EAlph \to \EAlph$ that maps every $q_a$ to $q_{\pi(a)}$, and leaves $q_0$, $q_3$ and $q_4$ fixed.
Technically speaking, the set of states has four {\em orbits} (one infinite orbit and three fixed points) of the action of the group of permutations of $\EAlph$.
%
Moreover, it is required that in a nominal automaton the transition relation is {\em equivariant}, i.e., closed under the action of permutations.
The automaton $\autom_5$ has this property:
For example, it has a transition $q_a\stackrel{a}{\longrightarrow} q_3$, and for any $\pi \colon \EAlph \to \EAlph$ there is also a transition $\pi(q_a) = q_{\pi(a)}\stackrel{\pi(a)}{\longrightarrow} q_3 = \pi(q_3)$.

Nominal automata with finitely many orbits of states are equi-expressive with finite register automata \cite[DBLP:journals/corr/BojanczykKL14], but they have an important theoretical advantage:
They are a direct reformulation of the classical notion of finite automaton, where one replaces finite sets with orbit-finite sets and functions (or relations) with equivariant ones.
A research programme advocated in \cite[DBLP:journals/corr/BojanczykKL14, DBLP:conf/popl/BojanczykBKL12] is to transport various computation models, algorithms and theorems along this correspondence.
This can often be done with remarkable accuracy, and our paper is a witness to this.
Indeed, as we shall see, nominal automata can be learned with an algorithm that is almost a verbatim copy of the classical Angluin's one.

Indeed, consider applying Angluin's algorithm to our new language $\lang_1$.
The key idea is to change the basic data structure:
Our observation table $(S,E)$ will be such that \emph{$S$ and $E$ are equivariant subsets of $A^{\ast}$}, i.e., they are closed under the canonical action of atom permutations.
In general, such a table has {\em infinitely many rows and columns}, so the following aspects of \in{Algorithm}[alg:alg] seem problematic:

\description{\inline{line}[line:checks]} closedness and consistency tests range over infinite sets;

\description{\inline{line}[line:clos-witness] and \inline{line}[line:cons-witness]} finding witnesses for closedness or consistency violations potentially require checking all infinitely many rows;
\todo{Is hetzelfde als die hierboven. Doe maar line 4 en 9: oneindige checks. Extra clause over $S$ en $E$ oneindig?}

\description{\inline{line}[line:addrow-ex]} every counterexample $t$ has only infinitely many prefixes, so it is not clear how one would construct an infinite set $S$ in finite time.
However, an infinite $S$ is necessary for the algorithm to ever succeed, because no finite automaton recognizes $\lang_1$. 

At this stage, we need to observe that due to equivariance of $S$, $E$ and $\lang_1$, the following crucial properties hold:

\description{(P1)} the sets $S$, $S \Lext A$ and $E$ admit a \emph{finite} representation up to permutations;

\description{(P2)} the function $row$ is such that $row(\pi(s))(\pi(e)) = row(s)(e)$, for all $s \in S$ and $e \in E$, so the observation table admits a finite symbolic representation.

Intuitively, checking closedness and consistency, and finding a witness for their violations, can be done effectively on the representations up to permutations {\bf (P1)}.
This is sound, as $row$ is invariant w.r.t. permutations {\bf (P2)}.

We now illustrate these points through a few steps of the algorithm for $\lang_1$.

\startstep{1'}
We start from $S, E = \{ \epsilon \}$.
We have $S \Lext A = A$, which is infinite but admits a finite representation.
In fact, for any $a \in A$, we have $A = \{ \pi(a) \mid \text{$\pi$ is a permutation}\}$.
Then, by {\bf (P2)}, $row(\pi(a))(\epsilon) = row(a)(\epsilon) = 0$, for all $\pi$, so the first table can be written as:
\todo{tikz \tt 411-434}

It is closed and consistent.
Our hypothesis is $\autom_1'$, where $\delta_{\autom_1'}(row(\epsilon),x) = row(x) = q_0$, for all $x \in A$.
As in {\bf Step 1}, the Teacher replies with the counterexample $aa$.
\stopstep

\startstep{2'} 
By equivariance of $\lang_1$, the counterexample tells us that \emph{all} words of length 2 with two repeated letters are accepted.
Therefore we extend $S$ with the (infinite!) set of such words.
The new symbolic table is:
\todo{tikz \tt 440-452}

The lower part stands for elements of $S \Lext A$.
For instance, $ab$ stands for words obtained by appending a fresh letter to words of length 1 (row $a$).
It can be easily verified that all cases are covered. Notice that the table is different from that of {\bf Step 2}:
A single $b$ is not in the lower part, because it can be obtained from $a$ via a permutation. The table is closed. 

Now, for consistency we need to check $row(\epsilon x) = row(ax)$, for all $a,x \in A$.
Again, by {\bf (P2)}, it is enough to consider rows of the table above.
Consistency is violated, because $row(a) \neq row(aa)$.
We found a \quotation{symbolic} witness $a$ for such violation.
In order to fix consistency, while keeping $E$ equivariant, we need to add columns for all $\pi(a)$.
The resulting table is 
\todo{tikz \tt 457-470}

where non-specified entries are $0$.
Only finitely many entries of the table are relevant:
$row(s)$ is fully determined by its values on letters in $s$ and on just one letter not in $s$.
For instance, we have $row(a)(a) = 1$ and $row(a)(a') = 0$, for all $a' \in A \setminus \{ a \}$.
The table is trivially consistent.

Notice that this step encompasses both {\bf Step 2} and {\bf 3}, because the rows $b$ and $bb$ added by {\bf Step 2} are already represented by $a$ and $aa$.
The hypothesis automaton is
\todo{tikz \tt 475-488}

This is again incorrect, but one additional step will give the correct hypothesis automaton, shown earlier in \in{?}[eq:aut]).
\stopstep

\stopsubsection
\startsubsection
  [title={Generalization to Non-Deterministic Automata}]

Since our extension of Angluin's \LStar{} algorithm stays close to her original development, exploring extensions of other variations of \LStar{} to the nominal setting can be done in a systematic way.
We will show  how to extend the algorithm \NLStar{} for learning NFAs by \cite[authoryears][DBLP:conf/ijcai/BolligHKL09].
This has practical implications: It is well-known that NFAs are exponentially more succinct than DFAs.
This is true also in the nominal setting. However, there are challenges in the extension that require particular care.
\startitemize
\item Nominal NFAs are strictly more expressive than nominal DFAs.
We will show that the nominal version of \NLStar{} terminates for all nominal NFAs that have a corresponding nominal DFA and, more surprisingly, that it is capable of learning some languages that are not accepted by nominal DFAs.
\item Language equivalence of nominal NFAs is undecidable.
This does not affect the correctness proof, as it assumes a teacher which is able to answer equivalence queries accurately.
For our implementation, we will describe heuristics that produce correct results in many cases.
\stopitemize
For the learning algorithm the power of non-determinism means that we can make some shortcuts during learning:
If we want to make the table closed, we were previously required to find an equivalent row in the upper part; now we may find a sum of rows which, together, are equivalent to an existing row.
This means that in some cases fewer rows will be added for closedness.

\stopsubsection
\stopsection
\placelistofpublications
\stopcomponent

