Gewerkt aan de intro

biblio.bib

@@ -510,6 +510,18 @@
 	bibsource = {dblp computer science bibliography, https://dblp.org}
 }
 
+@phdthesis{Cassel15,
+	title     = {Learning Component Behavior from Tests: Theory and Algorithms for Automata with Data},
+	author    = {Sofia Cassel},
+	year      = {2015},
+	isbn      = {978-91-554-9395-0},
+	issn      = {1651-6214 ; 1311}
+	publisher = {Acta Universitatis Upsaliensis},
+	series    = {Digital Comprehensive Summaries of Uppsala Dissertations from the Faculty of Science and Technology},
+	school    = {Uppsala University, Sweden},
+	url       = {http://urn.kb.se/resolve?urn=urn:nbn:se:uu:diva-265369}
+}
+
 @article{CasselHJS16,
 	author    = {Sofia Cassel and
 	             Falk Howar and
@@ -828,6 +840,17 @@
 	bibsource = {dblp computer science bibliography, https://dblp.org}
 }
 
+@phdthesis{Fiterau-Brostean18,
+	title     = {Active Model Learning for the Analysis of Network Protocols},
+	author    = {Paul Fiterau{-}Brostean},
+	year      = {2018},
+	isbn      = {978-94-028-0963-3}
+	publisher = {[Sl: sn]},
+	series    = {IPA dissertation series; 2018-04},
+	school    = {Radboud University, Nijmegen, The Netherlands},
+	url       = {http://hdl.handle.net/2066/187331}
+}
+
 @article{FujiwaraBKAG91,
 	author    = {Susumu Fujiwara and
 	             Gregor von Bochmann and

content.tex

@@ -6,6 +6,7 @@
 
 
 \startfrontmatter
+\setupwhitespace[none]
 \completecontent
 \completelistoffigures
 \completelistoftables

content/intro-nominal-sets-old.tex

@@ -0,0 +1,223 @@
+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 $\Pm = \{ \pi \colon \atoms \to \atoms \mid \pi \text{ is bijective} \}$ to be the set of permutations of names.
+Together with function composition, $\Pm$ forms a \emph{group}.
+For two elements $a$ and $b$ we define a particular bijection $\swap{a}{b} \in \Pm$ which swaps $a$ and $b$ and leaves all other elements fixed.
+\stopdefinition
+
+It is good to stress that the set of names has no other structure defined on it.
+The names are abstract entities which can be compared for equality, but nothing else.
+\footnote{We can have more structure on the set of atoms, this is discussed in \in{Section}[].}
+This also means that although $a$ and $b$ are distinct names, they are interchangeable.
+If we write $a \in \atoms$, then $a$ can stand for any of the names.
+So if we write $a, b \in \atoms$, then $a$ and $b$ can refer to the same name, i.e., $a = b$.
+In other words, we do not adapt the permutative convention by \citet[?].
+
+As alluded to before, we want to have permutations act on objects constructed from names, such as words, states in an automaton and languages.
+The notion of a group action captures exactly this.
+In most cases we are interested in the group $\Pm$.
+However, in order to be general enough for the next chapters, we introduce group actions for an arbitrary group $G$.
+\todo{Notatie $1$ is groepseenheid, ${\cdot}$ is vermenigvuldiging en werking.}
+
+\startdefinition
+Let $X$ be a set.
+A (left)
+\footnote{Many authors use left actions.
+However, we note that \citet[BojanczykKL14] use a right action.
+For them to have a well-defined group action, their group multiplication 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$).
+Instead of writing $g \cdot x$ we will often write the group action by juxtaposition $g x$.
+We will often write $X$ instead of $(X, {\cdot})$ when the intended action is clear from the context.
+\footnote{One should be cautious, as a set often allows for many different $G$-actions.}
+
+\startexample
+We list several examples of group actions.
+Many of them will be used later in this thesis.
+\startitemize
+\item
+The set $\atoms$ itself admits a natural $\Pm$-action, defined by
+\startformula \pi \cdot a = \pi(a). \stopformula
+The two requirements are easily verified by a routine calculation.
+We will also omit this verification for the upcoming examples.
+\item
+The set of words $\atoms^{*}$ has a $\Pm$-action which is defined point-wise:
+\startformula \pi \cdot a_1 a_2 \ldots a_k = \pi(a_1) \pi(a_2) \ldots \pi(a_k) \stopformula
+\item
+Similarly, the set of infinite words $\atoms^{\omega}$ has such a $\Pm$-action:
+\startformula \pi \cdot a_1 a_2 \ldots = \pi(a_1) \pi(a_2) \ldots \stopformula
+\item
+The empty set always admits a unique $G$-action for any $G$.
+(This is unique since the domain $G \times \emptyset = \emptyset$.)
+\startformula {\cdot} \colon G \times \emptyset \to \emptyset \stopformula
+\item
+The singleton set always admits a unique $G$-action for any $G$.
+(This is unique since the codomain only has just one element.)
+\startformula {\cdot} \colon G \times \{*\} \to \{*\} \stopformula
+\item
+For any set $X$, we can define a $G$-action by defining
+\startformula g \cdot x = x \stopformula
+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.
+\stopitemize
+\stopexample
+
+In the above examples, the non-trivial $\Pm$-sets are all infinite.
+Yet, in a sense, the set $\atoms^{*}$ is bigger than the set $\atoms$.
+To be able to quantify this, we introduce the notion of an orbit.
+
+\startdefinition
+Given a $G$-set $(X, {\cdot})$ and an element $x \in X$, we define the \emph{orbit of $x$} as the set
+\startformula \orb(x) = \{ g x \mid g \in G \}. \stopformula
+\stopdefinition
+
+If for two elements $x, y \in X$ we have $\orb(x) = \orb(y)$, then we say that $x$ and $y$ are in the same orbit.
+This precisely happens if there exists a $g$ such that $g x = y$.
+The relation of \quotation{being in the same orbit} is an equivalence relation (it is reflexive as a group has an identity element, symmetric because of the inverses and transitive because of composition).
+This relation partitions the set $X$ in a collection of orbits:
+\startformula X = \bigcup_{x \in X} \orb(x). \stopformula
+
+We can picture orbits in the following way.
+\todo{PLAATJE}
+As we wish to represent such sets (in order to run algorithms on them), we are especially interested in orbit-finite sets.
+For such sets, we can represent the whole set by a collection of its orbits.
+What remains to be represented are the orbits themselves.
+An easy way to do is, is to choose a representative of the orbit $x \in \orb(x)$. (Any element will do as the other elements can be constructed via the group action.)
+\todo{PLAATJE}
+
+\startexample
+We will describe the orbits for some $\Pm$-sets.
+\startitemize
+\item
+For a trivial $G$-set $X$, each element defines its own orbit, since $\orb(x) = \{ g x \mid g \in G \}$ is a singleton set.
+\item
+The $\Pm$-set $\atoms$ only has \emph{one orbit}.
+To see this, take two (distinct) elements $a, b \in \atoms$ and consider the bijection $\pi = \swap{a}{b}$.
+Then we see that $\pi \cdot a = b$, meaning that $a$ and $b$ are in the same orbit.
+So $\atoms$ is a single-orbit set.
+\item
+Before we tackle $\atoms^{*}$, we will analyse $\atoms^{2}$.
+The set consists of exactly \emph{two orbits}:
+\startformula\startalign
+\NC \{ (a, a) \NC \mid a \in \atoms \} \NR
+\NC \{ (a, b) \NC \mid a, b \in \atoms, a \neq b \} \NR
+\stopalign\stopformula
+This is because a bijection $\pi \in \Pm$ can never send an element of the form $(a, b)$ to an element of the form $(a, a)$ or vice versa.
+It can, however send any element $(a, b)$ to $(c, d)$ and so on.
+\item
+The set $\atoms^{*}$ has \emph{countably many orbits}.
+Since the action preserves the length of a word, we will show that the set has finitely many orbits for each length.
+So consider the set $\atoms^{k}$ with the point-wise action.
+An orbit of $\atoms^{k}$ is precisely determined by specifying which of the $k$ elements are equal to each other.
+This is a partition of $k$ elements, and there exactly $B_k$, the $k$th Bell number, such partitions.
+(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.
+\stopitemize
+\stopexample
+
+Having finitely many orbits is not enough for a finite representation which we can use algorithmically.
+We need an additional finiteness on the elements of a $G$-set,
+namely the existence of a \emph{finite support}.
+In order to define this, we need the notion of a data symmetry.
+
+\startdefinition
+A \emph{data symmetry} is a pair $(\mathcal{D}, G)$, where $\mathcal{D}$ is a structure and $G \leq \Sym(\mathcal{D})$ is a subgroup of the automorphism group of $\mathcal{D}$.
+\stopdefinition
+
+\startdefinition
+Let $X$ be a $G$-set and $x \in X$.
+A set $C \subset \mathcal{D}$ \emph{supports} $x$ if for all $g \in G$ with $g|_C = \id|_C$ we have $g \cdot x = x$.
+
+A $G$-set $X$ is called \emph{nominal} if every element has a finite support.
+\stopdefinition
+
+In a way, if an element is supported by a finite set $C$, it means that the element is somehow constructed from only the elements in $C$.
+We can see this from the definition, as changing any element outside of $C$ will leave the element $x$ fixed.
+
+\startexample
+\startitemize
+\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\}$.
+\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.
+
+
+\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
+G_{< \omega} = \{ \pi \in \Perm \mid \pi(x) \neq x \text{ for finitely many } x \}.
+\stopformula
+This is the subgroup of $\Pm$ of \emph{finite} permutation.
+The set $\{ X \subset \atoms \mid X \text{ is not finite nor co-finite} \}$ has infinitely many orbits when considered as a $G_{< \omega}$-set, but only one orbit as a $\Pm$-set.
+This poses the question which group we should consider (for example, \citet[BojanczykKL14] use the whole group $\Pm$).
+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$.
+
+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.
+\

content/introduction.tex

@@ -5,26 +5,29 @@
   [title={Introduction},
    reference=chap:introduction]
 
-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.
+When I was younger, I often learned how to play with new toys by messing around with them, i.e., by pressing buttons at random, observing its behaviour, pressing more buttons, and so on.
-I would only resort to the manual -- or ask \quotation{experts} -- to confirm my hypotheses.
+Only resorting to the manual -- or asking \quotation{experts} -- to confirm my beliefs on how the toy works.
-Now that I am older, I do mostly the same.
+Now that I am older, I do mostly the same with new devices, new tools, or new software.
-But now I know that this is an established computer science technique, called \emph{model learning}.
+However, now I know that this is an established computer science technique, called \emph{model learning}.
 
-In short, model learning
+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.
+The goal of this technique can be manifold:
-It is \emph{not just random testing}: the information learned during the interaction with the system is actively used to guide following interactions.
+It can be used to reverse-engineer a system, to find bugs in it, to verify properties of the system, 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.
+Additionally, the information learned can be inspected and analysed.
+\todo{We open the box?}
 
-In this thesis, I report my contributions to the field of model learning.
+This thesis is about model learning and related techniques.
-In the first part, I give results concerning \emph{black box testing} of automata.
+In the first part, I present 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.
+In educational science, learning may involve concepts such as teaching, blended learning, and interdisciplinarity.
 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.
@@ -51,7 +54,7 @@ So it makes sense to study a learning paradigm which allows for \emph{queries},
 \footnote{Instead of query learning, people also use the term \emph{active learning}.}
 
 A typical query learning framework was established by \citet[Angluin87].
-In her framework, the learning algorithm may pose two types of queries to a \emph{teacher} (or \emph{oracle}):
+In her framework, the learning algorithm may pose two types of queries to a \emph{teacher}, or \emph{oracle}:
 
 \description{Membership queries (MQs)}
 The learner poses such a query by providing a word $w \in \Sigma^{*}$ to the teacher.
@@ -60,14 +63,18 @@ This type of query is often generalised to more general output, so the teacher r
 In some papers, such a query is then called an \emph{output query}.
 
 \description{Equivalence queries (EQs)}
-The learner can provide a hypothesised description of $\lang$.
+The learner can provide a hypothesised description of $\lang$ to the teacher.
 If the hypothesis is correct, the teacher replies with \kw{yes}.
-If, however, the hypothesis is incorrect, the teacher replies with \kw{no}, together with a counterexample (i.e., a word which is in $\lang$ but not in the hypothesis or vice versa).
+If, however, the hypothesis is incorrect, the teacher replies with \kw{no} together with a counterexample, i.e., a word which is in $\lang$ but not in the hypothesis or vice versa.
 
-With these queries, the learner algorithm is supposed to converge to a correct model.
+By posing many such queries, the learner algorithm is supposed to converge to a correct model.
 This type of learning is hence called \emph{exact learning}.
 \citet[Angluin87] showed that one can do this efficiently for deterministic finite automata DFAs (when $\lang$ is in the class of regular languages).
 
+It should be clear why this is called \emph{query learning} or \emph{active learning}.
+The learning algorithm initiates interaction with the teacher by posing queries, it may construct its own data points and ask for their corresponding label.
+\todo{Nog afzetten tegen passive learning?}
+
 Another paradigm which is relevant for our type of applications is \emph{PAC-learning with membership queries}.
 Here, the algorithm can again use MQs as before, but the EQs are replace by random sampling.
 So the allowed query is:
@@ -77,15 +84,16 @@ If the learner poses this query (there are no parameters), the teacher responds
 
 Instead of requiring that the learner exactly learns the model, we only require the following.
 The learner should \emph{probably} return a model which is \emph{approximate} to the target.
-This gives the name probably approximately correct (PAC).
+This gives the name \emph{probably approximately correct} (PAC).
 Note that there are two uncertainties: the probable and the approximate part.
 Both part are bounded by parameters, so one can determine the confidence.
 
-Of course, we are interested in \emph{efficient} learning algorithms.
+As with many problems in computer science, we are also interested in the \emph{efficiency} of learning algorithms.
-This often means that we require a polynomial number of queries.
+Instead of measuring time or space, we often analyse the number of queries posed by an algorithm.
+Efficiency often means that we require a polynomial number of queries.
 But polynomial in what?
 The learner has no input, other than the access to a teacher.
-We ask the algorithms to be polynomial in the \emph{size of the target} (i.e., the description which has yet to be learned).
+We ask the algorithms to be polynomial in the \emph{size of the target} (i.e., the size of the description which has yet to be learned).
 In the case of PAC learning we also require it to be polynomial in the two parameters for confidence.
 
 Deterministic automata can be efficiently learned in the PAC model.
@@ -103,8 +111,8 @@ So far, all the queries are assumed to be \emph{just there}.
 Somehow, these are existing procedures which we can invoke with \kw{MQ}$(w)$, \kw{EQ}$(H)$, or \kw{EX}$()$.
 This is a useful abstraction when designing a learning algorithm.
 One can analyse the complexity (in terms of number of queries) independently of how these queries are resolved.
-At some point in time, however, one has to implement them.
+Nevertheless, at some point in time one has to implement them.
-In our case of learning software behaviour, membership queries are easy:
+In our case of learning software behaviour, membership queries are easily implemented:
 Simply provide the word $w$ to a running instance of the software and observe the output.
 \footnote{In reality, it is a bit harder than this.
 There are plentiful of challenges to solve, such as timing, choosing your alphabet, choosing the kind of observations to make and being able to faithfully reset the software.}
@@ -118,15 +126,48 @@ On one hand, it allows us to only test behaviour we really case about, on the ot
 We deviate even further from the PAC-model as we sometimes change our distribution while learning.
 Yet, as applications show, this is a useful way of learning software behaviour.
 
-\todo{Aannames: det. reset...}
 
-\todo{Research questions}
+\stopsubsection
+\startsubsection
+  [title={Research challenges}]
+
+Model learning is far from a 
+In this thesis, we will mostly see learning of DFAs or Mealy machines.
+Although this is restrictive as many pieces of software require richer models, it has been successfully applied in many different areas.
+The restrictions include the following.
+\startitemize[after]
+\item The system behaves deterministically.
+\item One can reliably reset the system.
+\item The system can be modelled with a finite state space.
+\item The set of input actions is finite.
+\item One knows when the target is reached.
+\stopitemize
+
+\description{Research challenge 1: Confidence in the hypothesis.}
+Having confidence in a learned model is difficult.
+We have PAC guarantees (as discussed before), but sometimes we may require other guarantees.
+For example, we may require the hypothesis to be correct, provided that the real system is implemented with a certain number of states.
+Efficiency is important here:
+We want to obtain those guarantees fast and we want to find quickly counterexamples when the hypothesis is wrong.
+Test generation methods is the topic of the first part in this thesis.
+We will review existing algorithms and discuss new algorithms for test generation.
+
+\startdescription[title={Research challenge 2: Generalisation to infinite alphabets.}]
+Automata over infinite alphabets are very useful for modelling protocols which involve identifiers or timestamps.
+Not only the alphabet is infinite in these cases, the state-space is as well, since the values have to be remembered.
+In the second part of this thesis, we will see how nominal techniques can be used to tackle this challenge.
+
+Being able to learn automata over an infinite alphabet is not new.
+It has been tackled in the theses of \cite[Aarts14, Fiterau-Brostean18, Cassel15].
+\todo{Dus...}
+\stopdescription
 
 
+\stopsubsection
 \startsubsection
   [title={A few applications of learning}]
 
-Since this thesis only contains one \quote{real-world} application on learning, I think it is good to mention a few others.
+Since this thesis only contains one \quote{real-world} application on learning in \in{Chapter}[chap:applying-automata-learning], I think it is good to mention a few others.
 Although we remain in the context of learning software behaviour, the applications are quite different.
 
 Finite state machine conformance testing is a core topic in testing literature that is relevant for communication protocols and other reactive systems.
@@ -178,12 +219,10 @@ A crucial concept in nominal automata is that of \emph{symmetries}.
 To motivate the use of symmetries, we will look at an example of a register auttomaton.
 In the following automaton we model a (not-so-realistic) login system for a single person.
 The alphabet consists of the following actions:
-\startformula\startalign
+\startformula\startmathmatrix[n=2, distance=1cm]
-\NC \kw{register}(p) \NR
+\NC \kw{register}(p) \NC \kw{logout}() \NR
-\NC \kw{login}(p) \NR
+\NC \kw{login}(p)    \NC \kw{view}()   \NR
-\NC \kw{logout}() \NR
+\stopmathmatrix\stopformula
-\NC \kw{view}() \NR
-\stopalign\stopformula
 The \kw{register} action allows one to set a password $p$.
 This can only be done when the system is initialised.
 The \kw{login} and \kw{logout} actions speak for themselves and the \kw{view} action allows one to see the secret data (we abstract away from what the user actually gets to see here).
@@ -239,232 +278,50 @@ Although this is not really related to automata theory, it was picked up by \cit
 They provide an equivalence between register automata and nominal automata.
 Additionally, they generalise the work on nominal sets to other symmetries.
 
+The symmetries we encounter in this thesis are the following, but other symmetries can be found in the literature.
+\startitemize[after]
+\item
+The \quotation{equality symmetry}.
+Here the domain can be any countably infinite set.
+We can take, for example, the set of string we used before as the domain from which we take passwords.
+No further structure is used on this domain, meaning that any value is just as good as any other.
+The symmetries therefore consist of all bijections on this domain.
+\item
+The \quotation{total order symmetry}.
+In this case, we take a countable infinite set with a dense total order.
+Typically, this means we use the rational numbers, $\Q$, as data values and symmetries which respect the ordering.
+\stopitemize
+
 
 \startsubsection
   [title={What is a nominal set?}]
 
-Before we dive into the relation with automata, we will define the notion of nominal sets.
+So what exactly is a nominal set?
+I will not define it here and leave the formalities to the corresponding chapters.
+It suffices, for now, to think of nominal sets with abstract sets (often infinite) on which a group of symmetries acts.
+The group of symmetries is not just any group, we fix a group of bijections on some fixed data domain.
 
-\startdefinition
+In order to implement such sets algorithmically, we impose two finiteness requirements
-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 $\Pm = \{ \pi \colon \atoms \to \atoms \mid \pi \text{ is bijective} \}$ to be the set of permutations of names.
-Together with function composition, $\Pm$ forms a \emph{group}.
-For two elements $a$ and $b$ we define a particular bijection $\swap{a}{b} \in \Pm$ which swaps $a$ and $b$ and leaves all other elements fixed.
-\stopdefinition
-
-It is good to stress that the set of names has no other structure defined on it.
-The names are abstract entities which can be compared for equality, but nothing else.
-\footnote{We can have more structure on the set of atoms, this is discussed in \in{Section}[].}
-This also means that although $a$ and $b$ are distinct names, they are interchangeable.
-If we write $a \in \atoms$, then $a$ can stand for any of the names.
-So if we write $a, b \in \atoms$, then $a$ and $b$ can refer to the same name, i.e., $a = b$.
-In other words, we do not adapt the permutative convention by \citet[?].
-
-As alluded to before, we want to have permutations act on objects constructed from names, such as words, states in an automaton and languages.
-The notion of a group action captures exactly this.
-In most cases we are interested in the group $\Pm$.
-However, in order to be general enough for the next chapters, we introduce group actions for an arbitrary group $G$.
-\todo{Notatie $1$ is groepseenheid, ${\cdot}$ is vermenigvuldiging en werking.}
-
-\startdefinition
-Let $X$ be a set.
-A (left)
-\footnote{Many authors use left actions.
-However, we note that \citet[BojanczykKL14] use a right action.
-For them to have a well-defined group action, their group multiplication 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$).
-Instead of writing $g \cdot x$ we will often write the group action by juxtaposition $g x$.
-We will often write $X$ instead of $(X, {\cdot})$ when the intended action is clear from the context.
-\footnote{One should be cautious, as a set often allows for many different $G$-actions.}
-
-\startexample
-We list several examples of group actions.
-Many of them will be used later in this thesis.
 \startitemize
 \item
-The set $\atoms$ itself admits a natural $\Pm$-action, defined by
+Finite support.
-\startformula \pi \cdot a = \pi(a). \stopformula
-The two requirements are easily verified by a routine calculation.
-We will also omit this verification for the upcoming examples.
 \item
-The set of words $\atoms^{*}$ has a $\Pm$-action which is defined point-wise:
+Orbit-finite.
-\startformula \pi \cdot a_1 a_2 \ldots a_k = \pi(a_1) \pi(a_2) \ldots \pi(a_k) \stopformula
-\item
-Similarly, the set of infinite words $\atoms^{\omega}$ has such a $\Pm$-action:
-\startformula \pi \cdot a_1 a_2 \ldots = \pi(a_1) \pi(a_2) \ldots \stopformula
-\item
-The empty set always admits a unique $G$-action for any $G$.
-(This is unique since the domain $G \times \emptyset = \emptyset$.)
-\startformula {\cdot} \colon G \times \emptyset \to \emptyset \stopformula
-\item
-The singleton set always admits a unique $G$-action for any $G$.
-(This is unique since the codomain only has just one element.)
-\startformula {\cdot} \colon G \times \{*\} \to \{*\} \stopformula
-\item
-For any set $X$, we can define a $G$-action by defining
-\startformula g \cdot x = x \stopformula
-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.
 \stopitemize
-\stopexample
 
-In the above examples, the non-trivial $\Pm$-sets are all infinite.
-Yet, in a sense, the set $\atoms^{*}$ is bigger than the set $\atoms$.
-To be able to quantify this, we introduce the notion of an orbit.
-
-\startdefinition
-Given a $G$-set $(X, {\cdot})$ and an element $x \in X$, we define the \emph{orbit of $x$} as the set
-\startformula \orb(x) = \{ g x \mid g \in G \}. \stopformula
-\stopdefinition
-
-If for two elements $x, y \in X$ we have $\orb(x) = \orb(y)$, then we say that $x$ and $y$ are in the same orbit.
-This precisely happens if there exists a $g$ such that $g x = y$.
-The relation of \quotation{being in the same orbit} is an equivalence relation (it is reflexive as a group has an identity element, symmetric because of the inverses and transitive because of composition).
-This relation partitions the set $X$ in a collection of orbits:
-\startformula X = \bigcup_{x \in X} \orb(x). \stopformula
-
-We can picture orbits in the following way.
-\todo{PLAATJE}
-As we wish to represent such sets (in order to run algorithms on them), we are especially interested in orbit-finite sets.
-For such sets, we can represent the whole set by a collection of its orbits.
-What remains to be represented are the orbits themselves.
-An easy way to do is, is to choose a representative of the orbit $x \in \orb(x)$. (Any element will do as the other elements can be constructed via the group action.)
-\todo{PLAATJE}
-
-\startexample
-We will describe the orbits for some $\Pm$-sets.
-\startitemize
-\item
-For a trivial $G$-set $X$, each element defines its own orbit, since $\orb(x) = \{ g x \mid g \in G \}$ is a singleton set.
-\item
-The $\Pm$-set $\atoms$ only has \emph{one orbit}.
-To see this, take two (distinct) elements $a, b \in \atoms$ and consider the bijection $\pi = \swap{a}{b}$.
-Then we see that $\pi \cdot a = b$, meaning that $a$ and $b$ are in the same orbit.
-So $\atoms$ is a single-orbit set.
-\item
-Before we tackle $\atoms^{*}$, we will analyse $\atoms^{2}$.
-The set consists of exactly \emph{two orbits}:
-\startformula\startalign
-\NC \{ (a, a) \NC \mid a \in \atoms \} \NR
-\NC \{ (a, b) \NC \mid a, b \in \atoms, a \neq b \} \NR
-\stopalign\stopformula
-This is because a bijection $\pi \in \Pm$ can never send an element of the form $(a, b)$ to an element of the form $(a, a)$ or vice versa.
-It can, however send any element $(a, b)$ to $(c, d)$ and so on.
-\item
-The set $\atoms^{*}$ has \emph{countably many orbits}.
-Since the action preserves the length of a word, we will show that the set has finitely many orbits for each length.
-So consider the set $\atoms^{k}$ with the point-wise action.
-An orbit of $\atoms^{k}$ is precisely determined by specifying which of the $k$ elements are equal to each other.
-This is a partition of $k$ elements, and there exactly $B_k$, the $k$th Bell number, such partitions.
-(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.
-\stopitemize
-\stopexample
-
-Having finitely many orbits is not enough for a finite representation which we can use algorithmically.
-We need an additional finiteness on the elements of a $G$-set,
-namely the existence of a \emph{finite support}.
-In order to define this, we need the notion of a data symmetry.
-
-\startdefinition
-A \emph{data symmetry} is a pair $(\mathcal{D}, G)$, where $\mathcal{D}$ is a structure and $G \leq \Sym(\mathcal{D})$ is a subgroup of the automorphism group of $\mathcal{D}$.
-\stopdefinition
-
-\startdefinition
-Let $X$ be a $G$-set and $x \in X$.
-A set $C \subset \mathcal{D}$ \emph{supports} $x$ if for all $g \in G$ with $g|_C = \id|_C$ we have $g \cdot x = x$.
-
-A $G$-set $X$ is called \emph{nominal} if every element has a finite support.
-\stopdefinition
-
-In a way, if an element is supported by a finite set $C$, it means that the element is somehow constructed from only the elements in $C$.
-We can see this from the definition, as changing any element outside of $C$ will leave the element $x$ fixed.
-
-\startexample
-\startitemize
-\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\}$.
-\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.
 
 
 \stopsubsection
 \startsubsection
-  [title={Nominal automata}]
+  [title={Contributions}]
 
-\todo{Model the example above as nominal automata}
+The following chapters are split into two parts.
+\in{Part}[part:testing] contains material about testing techniques, while \in{Part}[part:nominal] is about nominal techniques.
+Each chapter could be read in isolation.
+However, the chapters do get more technical and mathematical -- espacially in \in{Part}[part:nominal].
 
-
+\description{\in{Chapter}[chap:test-methods].}
-\stopsubsection
+Bla
-\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
-G_{< \omega} = \{ \pi \in \Perm \mid \pi(x) \neq x \text{ for finitely many } x \}.
-\stopformula
-This is the subgroup of $\Pm$ of \emph{finite} permutation.
-The set $\{ X \subset \atoms \mid X \text{ is not finite nor co-finite} \}$ has infinitely many orbits when considered as a $G_{< \omega}$-set, but only one orbit as a $\Pm$-set.
-This poses the question which group we should consider (for example, \citet[BojanczykKL14] use the whole group $\Pm$).
-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$.
-
-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

content/test-methods.tex

@@ -405,7 +405,8 @@ $X \odot \Fam{Y} = \{ xy \mid x \in X, y \in Y_{\delta(s_0, x)} \}$, and
 \footnote{We use the convention that $\cap$ binds stronger than $\cup$.
 In fact, all the operators here bind stronger than $\cup$.}
 \startformula
-(\Fam{X} ; \Fam{Y})_s = X_s \,\cup\, Y_s \!\cap\! \bigcup_{s \sim_{\Fam{X}} t} Y_t.
+(\Fam{X} ; \Fam{Y})_s
+  = X_s \,\cup\, Y_s \!\cap\! \bigcup_{\startsubstack s \sim_{\Fam{X}} t \NR s \not\sim_{\Fam{Y}} t \stopsubstack} Y_t.
 \stopformula
 \stopitemize
 

environment/headers.tex

@@ -1,8 +1,10 @@
 \startenvironment headers
 
 % TOC related
-\setupcombinedlist[content][list={part,chapter,section}]
+\setupcombinedlist[content][list={part,chapter,section}, alternative=c]
 \setuplist[section][margin=1cm, headnumber=no]
+\setuplist[chapter][style=bold]
+\setuplist[part][style=bold]
 
 % How numbers are shown
 \setuphead[part][placehead=yes, align=middle, sectionstarter=Part , sectionstopper=:]
@@ -15,6 +17,7 @@
 
 \setuplabeltext [en] [chapter=Chapter~]
 
+
 % een teller voor alles, prefix is chapter
 \definecounter[lemmata][way=bychapter,prefixsegments=chapter]
 
@@ -37,4 +40,21 @@
 \definestartstop[proofnoqed][before={{\it Proof. }}, after={}]
 
 
+% Front matter met i, ii, etc
+\startsectionblockenvironment[frontpart]
+\setupuserpagenumber[numberconversion=romannumerals]
+\setuppagenumber[number=1]
+\stopsectionblockenvironment
+
+% Rest met gewone cijfers
+\startsectionblockenvironment[bodypart]
+\setuppagenumber[number=1]
+\stopsectionblockenvironment
+
+% Ook in de TOC
+\definestructureconversionset[frontpart:pagenumber][][romannumerals]
+\definestructureconversionset[bodypart:pagenumber] [][numbers]
+\setuplist[chapter][pageconversionset=pagenumber]
+
+
 \stopenvironment