\project thesis
\startcomponent introduction

\startchapter
  [title={Pakkende titel},
   reference=chap:introduction]

\startsection
  [title={Learning and Testing}]

\todo{Gekopieerd van test methods paper.}

Finite state machine conformance testing is a core topic in testing literature that is relevant for communication protocols and other reactive systems.
The combination of conformance testing and automata learning is applied in practice and it proves to be an effective way of finding bugs \cite[Joeri], replacing legacy software \cite[Philips], or inferring models to be used in model checking \cite[MeinkeSindhu].

Several model learning applications:
learning embedded controller software \cite[DBLP:conf/icfem/SmeenkMVJ15], learning the TCP protocol \cite[DBLP:conf/cav/Fiterau-Brostean16] and learning the MQTT protocol \cite[DBLP:conf/icst/TapplerAB17].


\stopsection
\startsection
  [title={Nominal Techniques}]

The theory of nominal sets has been introduced to cope with name binding.
Dealing with names is very common in computer science and several techniques exist to do this.
For example, one can use a meta language to talk about bound and free variables.
This is easy enough to use in theoretical research, but can be a burden to implement (there is quite a bit of bookkeeping).
Another way is to use some sort of normal form, for example, by naming things with numbers (sequentially).
One example of such a numbering scheme is using de Bruijn indices.


\citet[GabbayP02] introduced a third option, based on nominal techniques.
Instead of relying on the meta level, we declare names to really exist:
\startformula
\atoms = \{ a, b, c, \ldots \}.
\stopformula
Here we understand that $a$ and $b$ are different names and these names can be directly used in lambda terms or other objects.
(These names do not stand for variables!
The names exist in their own right.)
As a consequence, we can describe lambda terms such as
\startformula
\lambda x . a \quad \text{and} \quad \lambda x . b \, .
\stopformula
These two lambda terms are distinct, since they are constructed with different names.
In order to talk about equivalence, we introduce permutations.
If we write $\swap{a}{b}$ for the permutation which swaps $a$ and $b$, then we can relate the two lambda terms as follows.
\startformula
\swap{a}{b} \lambda x . a = \lambda x . b
\stopformula
How the permutations act on objects other than names will be explained later.
This way we can relate the two terms, without talking about free or bound variables.
We only talk about the names and permutations we declared.

The idea that names and permutations are sufficient was picked up by \citet[DBLP:journals/corr/BojanczykKL14].
They show that besides abstract syntax, nominal techniques are also interesting when modelling automata over infinite alphabets.
Here the infinite alphabet will be the set of names and the automaton should respect the permutations.
We will see why this is a natural way to model such automata in the next section.


\startsubsection
  [title={What is a nominal set?}]

Before we dive into the relation with automata, we will define the notion of nominal sets.

\startdefinition
Fix a countable, infinite set $\atoms = \{ a, b, \ldots \}$ of \emph{names} (sometimes called \emph{atoms}).
The elements of $\atoms$ bare no relationship to natural numbers, or other standard mathematical entities.

Define $\Perm(\atoms) = \{ \pi \colon \atoms \to \atoms \mid \pi \text{ is bijective} \}$ to be the set of permutations of atoms.
Together with function composition, $\Perm(\atoms)$ forms a group.
\stopdefinition

As noted before, we want to let permutations act on objects constructed from names (such as lambda terms).
The notion of a group action captures exactly this.
In most cases we are interested in the group $\Perm(\atoms)$.
However, in order to be general enough for the next chapters, we introduce group actions for an arbitrary group $G$.

\startdefinition
Let $X$ be a set.
A (left)
\footnote{Most authors use left actions. However, we note that \citet[DBLP:journals/corr/BojanczykKL14] use a right action. For them to have a well-defined group action, their group composition has to be defined as $g \cdot f = f \circ g$ (i.e., reverse function composition).}
\emph{$G$-action} is a function ${\cdot} \colon G \times X \to X$ satisfying:
\startformula\startalign[n=3]
\NC 1 \cdot x            \NC = x                    \NC \quad \forall x \in X \NR
\NC (g \cdot h) \cdot x  \NC = g \cdot (h \cdot x)  \NC \quad \forall x \in X, \forall g,h \in G \NR
\stopalign\stopformula
A set together with a $G$-action, $(X, {\cdot})$, is called a \emph{$G$-set}.
\stopdefinition

It is worth noting that we generally fix $G$ but we consider many sets with a $G$-action.
In a way all these sets will have the same symmetries (namely $G$).


\stopsubsection
\stopsection
\referencesifcomponent
\stopchapter
\stopcomponent