meer intro

content/introduction.tex

@@ -5,17 +5,43 @@
   [title={Introduction},
    reference=chap:introduction]
 
-Bla
+When I was younger, I often learned how to use new toys by playing around with them, i.e., by pressing button randomly, and observing its behaviour.
+I would only resort to the manual -- or ask \quotation{experts} -- to confirm my hypotheses.
+Now that I am older, I do mostly the same.
+But now I know that this is an established computer science technique, called \emph{model learning}.
+
+In short, model learning
+\footnote{There are many names for the type of learning, such as \emph{active automata learning}.
+The generic name \quotation{model learning} is chosen as a counterpoint to model checking.}
+is a automated technique to construct a model -- often a type of \emph{automaton} -- from a black box system.
+The aim of this is to reverse-engineer the system, to find bugs, to verify, or to understand the system in one way or another.
+It is \emph{not just random testing}: the information learned during the interaction with the system is actively used to guide following interactions.
+
+In this thesis, I report my contributions to the field of model learning.
+In the first part, I give results concerning \emph{black box testing} of automata.
+Testing is a crucial part in learning software behaviour and often remains a bottleneck in applications of model learning.
+In the second part, I show how \emph{nominal techniques} can be used to learn automata over structured infinite alphabets.
+This was directly motivated by work on learning networks protocols which rely on identifiers or sequence numbers.
+
+But before we get ahead of ourselves, we should first understand what we mean by learning, as learning means very different things to different people.
+For pedagogics scientist learning may involve concepts such as teachers, scholars, blended learning, and active learning.
+Data scientist may think of data compression, feature extraction, and neural networks.
+In this thesis we are mostly concerned with software verification.
+But even in the field of verification several types of learning are relevant.
+
 
 \startsection
-  [title={Automata Learning}]
+  [title={Model Learning}]
 
-First off, let me sketch the problem.
+In the context of software verification, we often look at stateful computation with inputs and outputs.
-There is some fixed, but unkown to us, language $\lang \subseteq \Sigma^{*}$.
+For this reason, it makes sense to look at \emph{words}, or \emph{traces}.
-This can be a language of natural speech, a property in model checking, a set of traces from a protocol, etc.
+For an alphabet $\Sigma$, we denote the set of words by $\Sigma^{*}$.
+
+The learning problem is defined as follows.
+There is some fixed, but unknown to us, language $\lang \subseteq \Sigma^{*}$.
+This language may define the behaviour of a software component, a property in model checking, a set of traces from a protocol, etc.
 We wish to infer a description of $\lang$ by only using finitely many words.
 Note that this is not an easy task, as $\lang$ is often infinite.
-\todo{Waarom sequentiele data?}
 
 Such a learning problem can be stated and solved in a variety of ways.
 In the applications we do in our research group, we often try to infer a model of a software component.
@@ -94,6 +120,8 @@ Yet, as applications show, this is a useful way of learning software behaviour.
 
 \todo{Aannames: det. reset...}
 
+\todo{Research questions}
+
 
 \startsubsection
   [title={A few applications of learning}]
@@ -113,6 +141,8 @@ learning embedded controller software \cite[DBLP:conf/icfem/SmeenkMVJ15], learni
 \startsection
   [title={Testing Techniques for Automata}]
 
+\todo{Even lang maken als Nominal Techniques.}
+
 An important step in automata learning is equivalence checking.
 Normally, this is abstracted away and done by an oracle, but we intend to implement such an oracle ourselves for our applications.
 Concretely, the problem we need to solve is that of \emph{conformance checking}\footnote{It is also known as \emph{machine verification} or \emph{fault detection}.} and this was first described by \citet[Moore56].
@@ -287,18 +317,6 @@ For any set $X$, we can define a $G$-action by defining
 for all the elements $x \in X$.
 Such an action is called \emph{trivial}.
 Note that the action on $\emptyset$ and $\{*\}$ are trivial, but the $\Pm$-actions on $\atoms$, $\atoms^{*}$ and $\atoms^{\omega}$ are not trivial.
-\item
-Another interesting non-trivial example is the set $\Pm$ itself.
-There are three different interesting actions one can define:
-\startformula\startalign
-\NC \pi \cdot_{l} \sigma \NC = \pi \sigma \NR
-\NC \pi \cdot_{r} \sigma \NC = \sigma \pi^{-1} \NR
-\NC \pi \cdot_{c} \sigma \NC = \pi \sigma \pi^{-1} \NR
-\stopalign\stopformula
-Here the group multiplication is written by juxtaposition.
-The first two actions are \emph{left-multiplication} and \emph{right-multiplication} respectively.
-The latter is called \emph{conjugation}.
-For each of them, one can verify the requirements.
 \stopitemize
 \stopexample
 
@@ -353,23 +371,6 @@ This is a partition of $k$ elements, and there exactly $B_k$, the $k$th Bell num
 (As we have seen for $k = 2$, the second Bell number is $B_2 = 2$.
 This quantity grows exponential in $k$.)
 This shows that the set $\atoms^{*} = \bigcup_k \atoms^{k}$ has countably many orbits.
-\item
-The set $\atoms^{\omega}$ has \emph{uncountably many orbits}.
-To see this, fix two distinct elements $a, b \in \atoms$.
-Now, let $\sigma \in 2^{\omega}$ be an element of the Cantor space.
-We define the following sequence $x^{\sigma} \in \atoms^{\omega}$:
-\startformula\startalign
-\NC x^{\sigma}_0     \NC = a \NR
-\NC x^{\sigma}_{i+1} \NC =
-  \startmathcases
-  \NC a, \NC if $\sigma(i) = 0$ \NR
-  \NC b, \NC if $\sigma(i) = 1$ \NR
-  \stopmathcases \NR
-\stopalign\stopformula
-Now for two distinct elements $\sigma, \tau \in 2^{\omega}$, the elements $x^{\sigma}$ and $x^{\tau}$ are different.
-More importantly, their orbits $\orb(x^{\sigma})$ and $\orb(x^{\tau})$ are different too.
-This shows that there is an injective map from $2^{\omega}$ to the orbits of $\atoms^{\omega}$.
-This concludes that $\atoms^{\omega}$ has uncountably many orbits.
 \stopitemize
 \stopexample
 
@@ -397,21 +398,50 @@ We can see this from the definition, as changing any element outside of $C$ will
 \item
 The sets $\atoms$, $\atoms^{k}$, $\atoms^{*}$ are all nominal.
 For an element $a_1 a_2 \ldots a_k \in \atoms^{*}$, its support is simply given by $\{a_1, a_2, \ldots, a_k\}$.
-\item
-The set $\atoms^{\omega}$ is \emph{not} nominal.
-To see this, let us order the elements of $\atoms$ as $\atoms = \{ a_1, a_2, a_3, \ldots \}$.
-Now the element $a_1 a_2 a_3 \in \atoms^{\omega}$ is not finitely supported.
-\todo{fs subset van $\atoms^{\omega}$?}
-\item
-The set $\{ X \subset \atoms \mid X \text{ is not finite nor co-finite} \}$ (with the group action given by direct image) is a single orbit set, but it is not a nominal set.
 \stopitemize
 \stopexample
 
 These examples show that being orbit-finite and nominal are orthogonal properties.
+\todo{Een voorbeeld is uitgesteld.}
 There are $G$-sets which are orbit-finite, but non-nominal.
 Conversely, there are nominal sets which are not orbit-finite.
 
-\startremark
+
+\stopsubsection
+\startsubsection
+  [title={Nominal automata}]
+
+\todo{Model the example above as nominal automata}
+
+
+\stopsubsection
+\startsubsection
+  [title={More interesting examples of nominal sets}]
+
+The set $\atoms^{\omega}$ has \emph{uncountably many orbits}.
+To see this, fix two distinct elements $a, b \in \atoms$.
+Now, let $\sigma \in 2^{\omega}$ be an element of the Cantor space.
+We define the following sequence $x^{\sigma} \in \atoms^{\omega}$:
+\startformula\startalign
+\NC x^{\sigma}_0     \NC = a \NR
+\NC x^{\sigma}_{i+1} \NC =
+  \startmathcases
+  \NC a, \NC if $\sigma(i) = 0$ \NR
+  \NC b, \NC if $\sigma(i) = 1$ \NR
+  \stopmathcases \NR
+\stopalign\stopformula
+Now for two distinct elements $\sigma, \tau \in 2^{\omega}$, the elements $x^{\sigma}$ and $x^{\tau}$ are different.
+More importantly, their orbits $\orb(x^{\sigma})$ and $\orb(x^{\tau})$ are different too.
+This shows that there is an injective map from $2^{\omega}$ to the orbits of $\atoms^{\omega}$.
+This concludes that $\atoms^{\omega}$ has uncountably many orbits.
+
+The set $\atoms^{\omega}$ is \emph{not} nominal.
+To see this, let us order the elements of $\atoms$ as $\atoms = \{ a_1, a_2, a_3, \ldots \}$.
+Now the element $a_1 a_2 a_3 \in \atoms^{\omega}$ is not finitely supported.
+\todo{fs subset van $\atoms^{\omega}$?}
+
+The set $\{ X \subset \atoms \mid X \text{ is not finite nor co-finite} \}$ (with the group action given by direct image) is a single orbit set, but it is not a nominal set.
+
 The last example above needs a bit more clarification.
 In the book of \citet[Pitts13], the group of permutations is defined to be
 \startformula
@@ -423,7 +453,18 @@ This poses the question which group we should consider (for example, \citet[DBLP
 For nominal sets, there is no difference: nominal $G_{< \omega}$-sets and nominal $\Pm$-sets are equivalent, as shown by \citet[Pitts13].
 It is only for non-nominal sets that we can distinguish them.
 We will mostly work with the set of all permutations $\Pm$.
-\stopremark
+
+Another interesting non-trivial example is the set $\Pm$ itself.
+There are three different interesting actions one can define:
+\startformula\startalign
+\NC \pi \cdot_{l} \sigma \NC = \pi \sigma \NR
+\NC \pi \cdot_{r} \sigma \NC = \sigma \pi^{-1} \NR
+\NC \pi \cdot_{c} \sigma \NC = \pi \sigma \pi^{-1} \NR
+\stopalign\stopformula
+Here the group multiplication is written by juxtaposition.
+The first two actions are \emph{left-multiplication} and \emph{right-multiplication} respectively.
+The latter is called \emph{conjugation}.
+For each of them, one can verify the requirements.
 
 
 \stopsubsection