Intro and a bit of formatting
This commit is contained in:
Joshua Moerman
parent
47bc39813f
commit
6fe9e726f3
3 changed files with 99 additions and 36 deletions
|
|
@ -2,11 +2,13 @@
|
|||
\startcomponent introduction
|
||||
|
||||
\startchapter
|
||||
[title={Nominal Techniques and Testing Techniques for Automata Learning},
|
||||
[title={Introduction},
|
||||
reference=chap:introduction]
|
||||
|
||||
Bla
|
||||
|
||||
\startsection
|
||||
[title={Learning and Testing}]
|
||||
[title={Automata Learning}]
|
||||
|
||||
First off, let me sketch the problem.
|
||||
There is some fixed, but unkown to us, language $\lang \subseteq \Sigma^{*}$.
|
||||
|
|
@ -40,12 +42,12 @@ With these queries, the learner algorithm is supposed to converge to a correct m
|
|||
This type of learning is hence called \emph{exact learning}.
|
||||
\citet[DBLP:journals/iandc/Angluin87] showed that one can do this efficiently for deterministic finite automata DFAs (when $\lang$ is in the class of regular languages).
|
||||
|
||||
Another paradigm which is relevant for our type of applications is PAC-learning with membership queries.
|
||||
Here, the algorithm can again use MQs as before, but the EQs are replace by random sampling (by a fixed probability distribution).
|
||||
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:
|
||||
|
||||
\description{Random sample query (EX)}
|
||||
If the learner poses this query (there are no parameters), the teacher will respond with a random word $w$, together with its label $w \in \lang$.
|
||||
\description{Random sample queries (EXs)}
|
||||
If the learner poses this query (there are no parameters), the teacher responds with a random word $w$, together with its label $w \in \lang$.
|
||||
|
||||
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.
|
||||
|
|
@ -53,22 +55,51 @@ This gives the name 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.
|
||||
|
||||
\startremark
|
||||
When using only EQs, only MQs, or only EXs, then there are hardness results for learning DFAs.
|
||||
See the book of \citet[KearnsV94] for such results.
|
||||
\stopremark
|
||||
Of course, we are interested in \emph{efficient} learning algorithms.
|
||||
This 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).
|
||||
In the case of PAC learning we also require it to be polynomial in the two parameters for confidence.
|
||||
|
||||
DFAs can be efficiently learned in the PAC model.
|
||||
In fact, any exact learning algorithm with MQs and EQs can be transformed into a PAC algorithm with MQs (see exercise X in \citenp[KearnsV94]).
|
||||
Deterministic automata can be efficiently learned in the PAC model.
|
||||
In fact, any efficient exact learning algorithm with MQs and EQs can be transformed into an efficient PAC algorithm with MQs (see \citenp[KearnsV94], exercise 8.1).
|
||||
For this reason, we mostly focus on the former type of learning in this thesis.
|
||||
The transformation from exact learning to PAC learning is implemented by simply \emph{testing} the hypothesis with random samples.
|
||||
The number of samples depend on the required precision (i.e., both parameters in the PAC model).
|
||||
The type of testing we will see in later chapter is slightly different, however.
|
||||
We will often choose the probability distribution ourself and even change it between hypotheses.
|
||||
Although the PAC model does not allow this and we do not acquire the promised bounds, we are able to give other guarantees with those testing methods.
|
||||
This can be postponed until we actually implement a learning algorithm and apply it.
|
||||
|
||||
When using only EQs, only MQs, or only EXs, then there are hardness results for learning DFAs.
|
||||
So the combinations MQs + EQs and MQs + EXs have been carefully been picked.
|
||||
They provide a minimal basis for efficient learning.
|
||||
See the book of \citet[KearnsV94] for such hardness results and more information on PAC learning.
|
||||
|
||||
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.
|
||||
In our case of learning software behaviour, membership queries are easy:
|
||||
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.}
|
||||
Equivalence queries, however, are in general not doable.
|
||||
Even if we have the (machine) code, it is often way too complicated to check equivalence.
|
||||
That is why we resort to testing with EX queries.
|
||||
The EX query from PAC learning normally assumes a fixed, unknown, distribution.
|
||||
In our case, we implement a distribution to test against.
|
||||
This cuts both ways:
|
||||
On one hand, it allows us to only test behaviour we really case about, on the other hand the results are only as good as our choice of distribution.
|
||||
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{Gekopieerd van test methods paper.}
|
||||
\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.
|
||||
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.
|
||||
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].
|
||||
|
|
@ -77,13 +108,42 @@ 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].
|
||||
|
||||
|
||||
\stopsubsection
|
||||
\stopsection
|
||||
\startsection
|
||||
[title={Nominal Techniques}]
|
||||
[title={Testing Techniques for Automata}]
|
||||
|
||||
In the second part of this thesis, I will present results related to nominal automata.
|
||||
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].
|
||||
|
||||
The problem is as follows:
|
||||
We are given the description of a finite state machine and a black box system, does the system behave exactly as the description?
|
||||
We wish te determine this by running experiments on the system (as it is black box).
|
||||
It should be clear that this is a hopelessly difficult task, as an error can be hidden arbitrarily deep in the system.
|
||||
That is why we often assume some knowledge of the system.
|
||||
In this thesis we often assume a \emph{bound on the number of states} of the system.
|
||||
Under these conditions, \citet[Moore56] already solved the problem.
|
||||
Unfortunately, his experiment is exponential in size, or in his own words: \quotation{fantastically large.}
|
||||
|
||||
Years later, \citet[DBLP:journals/tse/Chow78, Vasilevskii73] independently designed efficient experiments.
|
||||
In particular, the set of experiments is polynomial in size.
|
||||
These techniques will be discussed in detail in \in{Chapter}[chap:test-methods].
|
||||
More background and other related problems, as well as their complexity results, are well exposed in a survey of \citet[DBLP:journals/tc/LeeY94].
|
||||
|
||||
|
||||
\stopsection
|
||||
\startsection
|
||||
[title={Nominal Techniques for Automata}]
|
||||
|
||||
In the second part of this thesis, I will present results related to \emph{nominal automata}.
|
||||
Usually, nominal techniques are introduced in order to solve problems involving name binding in topics like lambda calculus.
|
||||
However, for our applications it makes more sense to focus more on the symmetries (of names) first and show how this is useful in automata theory.
|
||||
However, we use them to deal with \emph{register automata}.
|
||||
These are automata which have an infinite alphabet, often thought of as input actions with \emph{data}.
|
||||
The control flow of the automaton may actually depend on the data.
|
||||
However, the data cannot be used in an arbitrary way as this would lead to many problems being undecidable.
|
||||
\footnote{The class of automata with arbitrary data operations is sometimes called \emph{extended finite state machines}.}
|
||||
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.
|
||||
|
|
@ -98,6 +158,7 @@ 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).
|
||||
A simple automaton with roughly this behaviour is given in \in{Figure}[fig:login-system].
|
||||
We will only informally discuss its semantics for now.
|
||||
|
||||
\startplacefigure
|
||||
[title={A simple register automaton. The symbol $\ast$ denotes any input otherwise not specified. The $r$ in states $q_1$ and $q_2$ is a register.},
|
||||
|
|
@ -119,7 +180,7 @@ A simple automaton with roughly this behaviour is given in \in{Figure}[fig:login
|
|||
\stopplacefigure
|
||||
|
||||
To model the behaviour nicely, we want the domain of passwords to be infinite.
|
||||
After all, one should allow arbitrarily long passwords.
|
||||
After all, one should allow arbitrarily long passwords to be secure.
|
||||
This means that a register automaton is actually an automaton over an infinite alphabet.
|
||||
|
||||
Common algorithms for automata, such as learning, will not work with an infinite alphabet.
|
||||
|
|
@ -128,11 +189,13 @@ In order to cope with this, we will use the \emph{symmetries} present in the alp
|
|||
|
||||
Let us continue with the example and look at its symmetries.
|
||||
If a person registers with a password \quotation{\kw{hello}} and consequently logins with \quotation{\kw{hello}}, then this is not distinguishable from a person registering and logging in with \quotation{\kw{bye}}.
|
||||
However, a trace $\kw{register}(\kw{hello})\, \kw{login}(\kw{bye})$ is different.
|
||||
This is an example of symmetry:
|
||||
the values \quotation{\kw{hello}} and \quotation{\kw{bye}} can be permuted, or interchanged.
|
||||
Note, however, that the trace $\kw{register}(\kw{hello})\, \kw{login}(\kw{bye})$ is different from the two before.
|
||||
So we see that we cannot simply collapse the whole alphabet into one equivalence class.
|
||||
For this reason, we keep the alphabet infinite and explicitly mention its symmetries.
|
||||
|
||||
Before formalising the permutations, let me remark the the use of symmetries in automata theory is not new.
|
||||
Before formalising symmetries, let me remark the the use of symmetries in automata theory is not new.
|
||||
One of the first to use symmetries was \citet[DBLP:conf/alt/Sakamoto97].
|
||||
He devised an \LStar{} learning algorithm for register automata, much like the one presented in \in{Chapter}[chap:learning-nominal-automata].
|
||||
The symmetries are crucial to reduce the problem to a finite alphabet and use the regular \LStar{} algorithm.
|
||||
|
|
|
|||
|
|
@ -5,11 +5,8 @@
|
|||
[title={FSM-based Test Methods},
|
||||
reference=chap:test-methods]
|
||||
|
||||
\startsection
|
||||
[title={Preliminaries}]
|
||||
|
||||
In this chapter we will discuss some of the theory of test generation methods.
|
||||
From this theoretical discussion we derive a new algorithm: the \emph{hybrid ads methods}, which is applied on a case study in \in{Chapter}[chap:applying-automata-learning].
|
||||
From this theoretical discussion we derive a new algorithm: the \emph{hybrid ads methods}, which is applied on a case study in the next chapter (\in{Chapter}[chap:applying-automata-learning]).
|
||||
A key aspect of such methods is the size of the obtained test suite.
|
||||
On one hand we want to cover as much as the specification as possible.
|
||||
On the other hand: testing takes time, so we want to minimise the size of a test suite.
|
||||
|
|
@ -19,7 +16,7 @@ As we see in the case study of the next chapter, real world software components
|
|||
Such amounts of states go beyond the comparative studies of, for example, \citet[DBLP:journals/infsof/DorofeevaEMCY10, DBLP:journals/infsof/EndoS13].
|
||||
|
||||
|
||||
\startsubsection
|
||||
\startsection
|
||||
[title={Words and Mealy machines}]
|
||||
|
||||
We will focus on Mealy machines, as those capture many protocol specifications and reactive systems.
|
||||
|
|
@ -79,7 +76,6 @@ An example Mealy machine is given in \in{Figure}[fig:running-example].
|
|||
\stopplacefigure
|
||||
|
||||
|
||||
\stopsubsection
|
||||
\startsubsection
|
||||
[title={Testing}]
|
||||
|
||||
|
|
@ -589,11 +585,11 @@ From the figure above we obtain the family $\Fam{Z}$.
|
|||
These families and the refinement $\Fam{Z'};\Fam{H}$ are given below:
|
||||
|
||||
\starttabulate[|l|l|l|]
|
||||
\NC $H_0 = \{aa,b,c\}$ \NC $Z'_0 = \{aa\}$ \NC $(Z';H)_0 = \{aa\}$ \NR
|
||||
\NC $H_1 = \{a\}$ \NC $Z'_1 = \{a\}$ \NC $(Z';H)_1 = \{a\}$ \NR
|
||||
\NC $H_2 = \{aa,b,c\}$ \NC $Z'_2 = \{aa\}$ \NC $(Z';H)_2 = \{aa,b,c\}$ \NR
|
||||
\NC $H_3 = \{a,b,c\}$ \NC $Z'_3 = \{aa\}$ \NC $(Z';H)_3 = \{a,b,c\}$ \NR
|
||||
\NC $H_4 = \{a,b\}$ \NC $Z'_4 = \{aa\}$ \NC $(Z';H)_4 = \{aa,b\}$ \NR
|
||||
\NC $H_0 = \{aa,b,c\}$ \NC $Z'_0 = \{aa\}$ \NC $(Z';H)_0 = \{aa\}$ \NC\NR
|
||||
\NC $H_1 = \{a\}$ \NC $Z'_1 = \{a\}$ \NC $(Z';H)_1 = \{a\}$ \NC\NR
|
||||
\NC $H_2 = \{aa,b,c\}$ \NC $Z'_2 = \{aa\}$ \NC $(Z';H)_2 = \{aa,b,c\}$ \NC\NR
|
||||
\NC $H_3 = \{a,b,c\}$ \NC $Z'_3 = \{aa\}$ \NC $(Z';H)_3 = \{a,b,c\}$ \NC\NR
|
||||
\NC $H_4 = \{a,b\}$ \NC $Z'_4 = \{aa\}$ \NC $(Z';H)_4 = \{aa,b\}$ \NC\NR
|
||||
\stoptabulate
|
||||
\todo{In startformula/startalign zetten}
|
||||
|
||||
|
|
|
|||
|
|
@ -5,10 +5,14 @@
|
|||
|
||||
% How numbers are shown
|
||||
\setuphead[part][placehead=yes, align=middle, sectionstarter=Part , sectionstopper=:]
|
||||
\setuphead[chapter][sectionsegments=chapter]
|
||||
\setuphead[chapter][sectionsegments=chapter, command=\MyChapter]
|
||||
\setuphead[section][sectionsegments=chapter:section]
|
||||
\setuphead[subsection][sectionsegments=section:subsection]
|
||||
\setuphead[subsection][sectionsegments=chapter:section:subsection]
|
||||
|
||||
\define[2]\MyChapter
|
||||
{\framed[frame=off, width=max, align={flushleft,nothyphenated,verytolerant}, offset=0cm, toffset=1cm, boffset=1cm]{#1\\#2}}
|
||||
|
||||
\setuplabeltext [en] [chapter=Chapter~]
|
||||
|
||||
% een teller voor alles, prefix is chapter
|
||||
\definecounter[lemmata][way=bychapter,prefixsegments=chapter]
|
||||
|
|
|
|||
Reference in a new issue