joshua/phd-thesis
Archived
1
Fork 0
Code Activity

Commentaar van Tessa

Browse source
This commit is contained in:
Joshua Moerman 2019-03-13 11:07:09 +01:00
parent a49a2608a9
commit 4ba47d28d9
1 changed files with 27 additions and 18 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

45
content/introduction.tex
View file

@ -75,11 +75,12 @@ The learning algorithm initiates interaction with the teacher by posing queries,
Active learning is in contrast to \emph{passive learning} where all observations are given to the algorithm up front. Active learning is in contrast to \emph{passive learning} where all observations are given to the algorithm up front.
Another paradigm which is relevant for our type of applications is \emph{PAC-learning with membership queries}. 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. Here, the algorithm can again use MQs as before, but the EQs are replaced by random sampling.
So the allowed query is: So the allowed query is:
\description{Random sample queries (EXs)} \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 (i.e., whether $w \in \lang$ or not). If the learner poses this query (there are no parameters), the teacher responds with a random word $w$ together with its label (i.e., whether $w \in \lang$ or not).
\todo{Wat is random? Kansverdeling introduceren?}
Instead of requiring that the learner exactly learns the model, we only require the following. 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. The learner should \emph{probably} return a model which is \emph{approximate} to the target.
@ -94,6 +95,7 @@ But polynomial in what?
The learner has no input, other than the access to a teacher. 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 size of 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. In the case of PAC learning we also require it to be polynomial in the two parameters for confidence.
\todo{Afhankelijk van de verdeling}
Deterministic automata can be efficiently learned in the PAC model. 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). 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).
@ -101,8 +103,8 @@ 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 transformation from exact learning to PAC learning is implemented by simply \emph{testing} the hypothesis with random samples.
This can be postponed until we actually implement a learning algorithm and apply it. 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. When using only EQs, only MQs, or only EXs, then there are hardness results for exact learning of DFAs.
So the combinations MQs + EQs and MQs + EXs have been carefully picked, So the combinations MQs + EQs (for exact learning) and MQs + EXs (for PAC learning) have been carefully picked,
they provide a minimal basis for efficient learning. they provide a minimal basis for efficient learning.
See the book of \citet[KearnsV94] for such hardness results and more information on PAC learning. See the book of \citet[KearnsV94] for such hardness results and more information on PAC learning.
@ -118,10 +120,12 @@ There are plentiful of challenges to solve, such as timing, choosing your alphab
Equivalence queries, however, are in general not doable. Equivalence queries, however, are in general not doable.
Even if we have the (machine) code, it is often way too complicated to check equivalence. 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. That is why we resort to testing with EX queries.
The EX query from PAC learning normally assumes a fixed, unknown, distribution. The EX query from PAC learning normally assumes a fixed, unknown distribution.
\todo{Prob. distribution on words}
In our case, we choose and implement a distribution to test against. In our case, we choose and implement a distribution to test against.
\todo{Concreter: that we use for membership queries.}
This cuts both ways: 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. On one hand, it allows us to only test behaviour we really care 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. 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. Yet, as applications show, this is a useful way of learning software behaviour.
@ -130,7 +134,7 @@ Yet, as applications show, this is a useful way of learning software behaviour.
\startsection \startsection
[title={Applications of Model Learning}] [title={Applications of Model Learning}]
Since this thesis only contains one real-world application of learning in \in{Chapter}[chap:applying-automata-learning], it is good to mention a few others. Since this thesis contains only one real-world application of learning in \in{Chapter}[chap:applying-automata-learning], it is good to mention a few others.
Although we remain in the context of learning software behaviour, the applications are quite different from each other. Although we remain in the context of learning software behaviour, the applications are quite different from each other.
This is by no means a complete list. This is by no means a complete list.
@ -171,13 +175,16 @@ This gave developers opportunities to solve problems before replacing the old co
In this thesis, we will mostly see learning of deterministic automata or Mealy machines. In this thesis, we will mostly see learning of deterministic automata or Mealy machines.
Although this is restrictive as many pieces of software require richer models, it has been successfully applied in the above examples. Although this is restrictive as many pieces of software require richer models, it has been successfully applied in the above examples.
The restrictions include the following. The restrictions include the following.
\todo{Limitations / assumptions}
\startitemize[after] \startitemize[after]
\item The system behaves deterministically. \item The system behaves deterministically.
\item One can reliably reset the system. \item One can reliably reset the system.
\item The system can be modelled with a finite state space. \item The system can be modelled with a finite state space.
This also means that the model does not incorporate time or data. This also means that the model does not incorporate time or data.
\item The set of input actions is finite. \item The set of input actions is finite.
\todo{Alphabet}
\item One knows when the target is reached. \item One knows when the target is reached.
\todo{Weten we wel mbt kansverdeling}
\stopitemize \stopitemize
\description{Research challenge 1: Approximating equivalence queries.} \description{Research challenge 1: Approximating equivalence queries.}
@ -187,6 +194,7 @@ For example, we may require the hypothesis to be correct, provided that the real
Efficiency is important here: Efficiency is important here:
We want to obtain those guarantees fast and we want to quickly find counterexamples when the hypothesis is wrong. We want to obtain those guarantees fast and we want to quickly find counterexamples when the hypothesis is wrong.
Test generation methods is the topic of the first part in this thesis. Test generation methods is the topic of the first part in this thesis.
\todo{to test if hypothesis is correct}
We will review existing algorithms and discuss new algorithms for test generation. We will review existing algorithms and discuss new algorithms for test generation.
\startdescription[title={Research challenge 2: Generalisation to infinite alphabets.}] \startdescription[title={Research challenge 2: Generalisation to infinite alphabets.}]
@ -215,7 +223,7 @@ Concretely, the problem we need to solve is that of \emph{conformance checking}\
The problem is as follows: The problem is as follows:
Given the description of a finite state machine and a black box system, does the system behave exactly as the description? 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). We wish to 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. 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. 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. In this thesis we often assume a \emph{bound on the number of states} of the system.
@ -232,7 +240,7 @@ We will not model the audible output -- that would depend not only on the device
Instead, the only observation we can make is looking how fast the turntable spins. Instead, the only observation we can make is looking how fast the turntable spins.
The device has two buttons: a start-stop button (\playstop) and a speed button (\spin) which toggles between $33 \frac{1}{3}$ rpm and $45$ rpm. The device has two buttons: a start-stop button (\playstop) and a speed button (\spin) which toggles between $33 \frac{1}{3}$ rpm and $45$ rpm.
When turned on, the system starts playing immediately at $33 \frac{1}{3}$ rpm -- this is useful for DJing. When turned on, the system starts playing immediately at $33 \frac{1}{3}$ rpm -- this is useful for DJing.
The intended behaviour of the records player has four states as depicted in \in{Figure}[fig:record-player]. The intended behaviour of the record player has four states as depicted in \in{Figure}[fig:record-player].
\startplacefigure \startplacefigure
[title={Behaviour of a record player modelled as a finite state machine.}, [title={Behaviour of a record player modelled as a finite state machine.},
@ -256,7 +264,7 @@ The intended behaviour of the records player has four states as depicted in \in{
\stopplacefigure \stopplacefigure
Let us consider some faults which could be present in an implementation with four states. Let us consider some faults which could be present in an implementation with four states.
In \in{Figure}[fig:faulty-record-players], two flawed records players are given. In \in{Figure}[fig:faulty-record-players], two flawed record players are given.
In the first (\in{Figure}{a}[fig:faulty-record-players]), the sequence \playstop\,\spin\,\spin\, leads us to the wrong state. In the first (\in{Figure}{a}[fig:faulty-record-players]), the sequence \playstop\,\spin\,\spin\, leads us to the wrong state.
However, this is not immediately observable, the turntable is in a non-spinning state as it should be. However, this is not immediately observable, the turntable is in a non-spinning state as it should be.
The fault is only visible when we press \playstop\, once more: now the turntable is spinning fast instead of slow. The fault is only visible when we press \playstop\, once more: now the turntable is spinning fast instead of slow.
@ -318,7 +326,7 @@ Usually, nominal techniques are introduced in order to solve problems involving
However, we use them in automata theory, specifically to model \emph{register automata}. However, we use them in automata theory, specifically to model \emph{register automata}.
These are automata which have an infinite alphabet, often thought of as input actions with \emph{data}. 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. 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, such as emptiness and equivalence, being undecidable. However, the data cannot be used in an arbitrary way as this would lead to many decision problems, such as emptiness and equivalence, being undecidable.
\footnote{The class of automata with arbitrary data operations is sometimes called \emph{extended finite state machines}.} \footnote{The class of automata with arbitrary data operations is sometimes called \emph{extended finite state machines}.}
A principal concept in nominal techniques is that of \emph{symmetries}. A principal concept in nominal techniques is that of \emph{symmetries}.
@ -462,12 +470,11 @@ Detailed discussion on related work and future directions of research are presen
This chapter introduces test generation methods which can be used for learning or conformance testing. This chapter introduces test generation methods which can be used for learning or conformance testing.
The methods are presented in a uniform way, which allows to give a single proof of completeness for all these methods. The methods are presented in a uniform way, which allows to give a single proof of completeness for all these methods.
Moreover, the uniform presentation gives room to develop new test generation methods. Moreover, the uniform presentation gives room to develop new test generation methods.
One particular contribution (besides the theoretical framework) is the new \emph{hybrid ADS} test generation method.
The main contributions are: The main contributions are:
\startitemize[before, after] \startitemize[before, after]
\item Uniform description of known methods: \in{Theorem}[thm:completeness] (p. \at[thm:completeness]) \item Uniform description of known methods: \in{Theorem}[thm:completeness] (p. \at[thm:completeness])
\item A new proof of completeness: \in{Section}[sec:completeness] (p. \at[sec:completeness]) \item A new proof of completeness: \in{Section}[sec:completeness] (p. \at[sec:completeness])
\item New algorithm and its implementation: \in{Section}[sec:hybrid-ads-impementation] (p. \at[sec:hybrid-ads-impementation]) \item New algorithm (\emph{hybrid ADS}) and its implementation: \in{Section}[sec:hybrid-ads-impementation] (p. \at[sec:hybrid-ads-impementation])
\stopitemize \stopitemize
\stopcontribution \stopcontribution
@ -475,9 +482,9 @@ The main contributions are:
In this chapter we will apply model learning to an industrial case study. In this chapter we will apply model learning to an industrial case study.
It is a unique benchmark as it is much bigger than any of the applications seen before (3410 states and 77 inputs). It is a unique benchmark as it is much bigger than any of the applications seen before (3410 states and 77 inputs).
This makes it challenging to learn a model and the main obstacle is finding counterexamples. This makes it challenging to learn a model and the main obstacle is finding counterexamples.
Here, my main contribution is the new test generation method from \in{Chapter}[chap:test-methods].
The main contribution is: The main contribution is:
\startitemize[before, after] \startitemize[before, after]
\item Application of the \emph{hybrid ADS} algorithm: \in{Section}[sec:testSelection] (p. \at[sec:testSelection])
\item Succesfully learn a large-scale system: \in{Section}[sec:learnResults] (p. \at[sec:learnResults]) \item Succesfully learn a large-scale system: \in{Section}[sec:learnResults] (p. \at[sec:learnResults])
\stopitemize \stopitemize
@ -555,7 +562,7 @@ This is based on a paper under submission:
\cite[entry][MoermanR19]. \cite[entry][MoermanR19].
\stopcontribution \stopcontribution
Besides these chapters in this thesis, the author has published the following papers. Besides these chapters in this thesis, I have published the following papers.
These are not included in this thesis, but a short summary of those papers is presented below. These are not included in this thesis, but a short summary of those papers is presented below.
\startcontribution[title={Complementing Model Learning with Mutation-Based Fuzzing.}] \startcontribution[title={Complementing Model Learning with Mutation-Based Fuzzing.}]
@ -601,6 +608,8 @@ This work was presented at ICGI 2018:
\startsection \startsection
[title=Conclusion and Outlook] [title=Conclusion and Outlook]
\todo{Loopt een beetje door elkaar}
With the current tools for model learning, it is possible to learn big state machines of black box systems. With the current tools for model learning, it is possible to learn big state machines of black box systems.
It involves using the clever algorithms for learning (such as the TTT algorithm by \citenp[Isberner15]) and efficient testing methods (see \in{Chapter}[chap:test-methods]). It involves using the clever algorithms for learning (such as the TTT algorithm by \citenp[Isberner15]) and efficient testing methods (see \in{Chapter}[chap:test-methods]).
However, as the industrial case study from \in{Chapter}[chap:applying-automata-learning] shows, the bottleneck is often in conformance testing. However, as the industrial case study from \in{Chapter}[chap:applying-automata-learning] shows, the bottleneck is often in conformance testing.
@ -608,12 +617,12 @@ However, as the industrial case study from \in{Chapter}[chap:applying-automata-l
In order to improve on this bottleneck, one possible direction is to consider \quote{grey box testing.} In order to improve on this bottleneck, one possible direction is to consider \quote{grey box testing.}
The methods discussed in this thesis are all black box methods, this could be considered as \quote{too pessimistic.} The methods discussed in this thesis are all black box methods, this could be considered as \quote{too pessimistic.}
Often, we do have (parts of the) source code and we do know relationships between different inputs. Often, we do have (parts of the) source code and we do know relationships between different inputs.
The question is how this additional information can be integrated in a principled manner in the learning and testing of systems. A question for future research is how this additional information can be integrated in a principled manner in the learning and testing of systems.
Black box testing still has theoretical challenges. Black box testing still has theoretical challenges.
Current generalisations to non-deterministic systems or language inclusion (such as black box testing for IOCO) often need exponentially big test suites. Current generalisations to non-deterministic systems or language inclusion (such as black box testing for IOCO) often need exponentially big test suites.
Whether this is necessary is unknown (to me), we only have upper bounds but no lower bounds. Whether this is necessary is unknown (to me), we only have upper bounds but no lower bounds.
An interesting approach would be to see if there exists a notion of reduction between test suites. An interesting approach could be to see if there exists a notion of reduction between test suites.
This is analogous to the reductions used complexity theory to prove problems hard, or reductions used in PAC theory to prove learning problems to be inherently unpredictable. This is analogous to the reductions used complexity theory to prove problems hard, or reductions used in PAC theory to prove learning problems to be inherently unpredictable.
Another path taken in this thesis is the research on nominal automata. Another path taken in this thesis is the research on nominal automata.
@ -627,7 +636,7 @@ For instance, we show that \NLStar{} algorithm for non-deterministic automata wo
The nominal learning algorithms can be implemented in just a few hundreds lines of code, much less than the approach taken by, e.g., \citet[Fiterau-Brostean18]. The nominal learning algorithms can be implemented in just a few hundreds lines of code, much less than the approach taken by, e.g., \citet[Fiterau-Brostean18].
In this thesis, we tackle some efficiency issues when computing with nominal sets. In this thesis, we tackle some efficiency issues when computing with nominal sets.
In \in{Chapter}[chap:ordered-nominal-sets] we characterise orbits in order to give a efficient representation (for the total-order symmetry). In \in{Chapter}[chap:ordered-nominal-sets] we characterise orbits in order to give an efficient representation (for the total-order symmetry).
Another result is the fact that some nominal automata can be \quote{compressed} to separated automata, which can be exponentially smaller (\in{Chapter}[chap:separated-nominal-automata]). Another result is the fact that some nominal automata can be \quote{compressed} to separated automata, which can be exponentially smaller (\in{Chapter}[chap:separated-nominal-automata]).
However, the nominal tools still leave much to desired in terms of efficiency. However, the nominal tools still leave much to desired in terms of efficiency.
@ -638,7 +647,7 @@ The results on learning nominal automata in \in{Chapter}[chap:learning-nominal-a
However, there is an interesting twist to this problem. However, there is an interesting twist to this problem.
The test methods from \in{Chapter}[chap:test-methods] can all account for extra states. The test methods from \in{Chapter}[chap:test-methods] can all account for extra states.
For nominal automata, we should be able to cope with extra states \emph{and} extra registers. For nominal automata, we should be able to cope with extra states \emph{and} extra registers.
It will be interesting to see how the test suite grows as these two dimensions increase. It would be interesting to see how the test suite grows as these two dimensions increase.
\stopsection \stopsection