joshua/phd-thesis
Archived
1
Fork 0
Code Activity

Wijzigingen tav de reviews van onze fossacs inzending

Browse source
This commit is contained in:
Joshua Moerman 2019-01-11 15:43:03 +01:00
parent a2022293cc
commit 9515d42802
4 changed files with 34 additions and 12 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

11
biblio.bib
View file

@ -2077,6 +2077,17 @@
bibsource = {dblp computer science bibliography, https://dblp.org} bibsource = {dblp computer science bibliography, https://dblp.org}
} }
@phdthesis{Schoepp06,
author = {Ulrich Sch{\"{o}}pp},
title = {Names and binding in type theory},
school = {University of Edinburgh, {UK}},
year = {2006},
url = {http://hdl.handle.net/1842/1203},
timestamp = {Mon, 05 Sep 2016 19:00:20 +0200},
biburl = {https://dblp.org/rec/bib/phd/ethos/Schopp06},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{SchutsHV16, @inproceedings{SchutsHV16,
author = {Mathijs Schuts and author = {Mathijs Schuts and
Jozef Hooman and Jozef Hooman and

4
content.tex
View file

@ -10,11 +10,13 @@
\midaligned{\framed[width=12cm,align=center,offset=2cm,frame=off]{Nominal Techniques and Black Box Testing for Automata Learning}} \midaligned{\framed[width=12cm,align=center,offset=2cm,frame=off]{Nominal Techniques and Black Box Testing for Automata Learning}}
\switchtobodyfont[12pt] \switchtobodyfont[12pt]
\midaligned{Joshua Moerman} \midaligned{Joshua Moerman}
\midaligned{Radboud University}
\midaligned{Nijmegen, the Netherlands}
\midaligned{11 January 2019} \midaligned{11 January 2019}
\stop \stop
\page[yes] \page[yes]
\setupwhitespace[none] \setupwhitespace[small]
\completecontent \completecontent
%\completelistoffigures %\completelistoffigures
%\completelistoftables %\completelistoftables

27
content/separated-nominal-automata.tex
View file

@ -70,14 +70,14 @@ However, moving from register automata to nominal automata can lead to an expone
\footnote{Here \quote{number of states} refers to the number of orbits in the state space.} \footnote{Here \quote{number of states} refers to the number of orbits in the state space.}
As a motivating example, we consider a language modelling an $n$-bounded FIFO queue. As a motivating example, we consider a language modelling an $n$-bounded FIFO queue.
The input alphabet is given by $\Sigma = \{ \Put(a) \mid a \in \atoms \} \cup \{ \Pop \}$, and the output alphabet by $O = \atoms \cup \{ \Null \}$. The input alphabet is given by $\Sigma = \{ \Put(a) \mid a \in \atoms \} \cup \{ \Pop \}$, and the output alphabet by $O = \atoms \cup \{ \perp \}$ (here $\perp$ is a \emph{null} value).
The language $L_n \colon \Sigma^* \to O$ maps a sequence of queue operations to the resulting top element when starting from the empty queue, or to $\Null$ if this is undefined. The language $L_n \colon \Sigma^* \to O$ maps a sequence of queue operations to the resulting top element when starting from the empty queue, or to $\perp$ if this is undefined.
The language $L_n$ can be recognised by a nominal automaton, but this requires an exponential number of states in $n$, as the automaton distinguishes internally between all possible equalities among elements in the queue. The language $L_n$ can be recognised by a nominal automaton, but this requires an exponential number of states in $n$, as the automaton distinguishes internally between all possible equalities among elements in the queue.
Based on the observation that $L_n$ is a nominal renaming set, we can come up with a \emph{linear} automata-theoretic representation. Based on the observation that $L_n$ is a nominal renaming set, we can come up with a \emph{linear} automata-theoretic representation.
To this end, we define the new notion of \emph{separated nominal automaton}, where the transition function is only defined for pairs of states and letters with a disjoint support (\in{Section}[sec:automata]). To this end, we define the new notion of \emph{separated nominal automaton}, where the transition function is only defined for pairs of states and letters with a disjoint support (\in{Section}[sec:automata]).
Using the aforementioned categorical framework, we find that such separated automata recognise languages which are nominal renaming sets. Using the aforementioned categorical framework, we find that such separated automata recognise languages which are nominal renaming sets.
Separated nominal automata can be much smaller than classical nominal automata recognising the same language. Although separated nominal automata are not as expressive as classical nominal automata, they can be much smaller.
In particular, in the FIFO example, the reachable part of the separated automaton obtained from the original nominal automaton has $n+1$ states, thus dramatically reducing the number of states. In particular, in the FIFO example, the reachable part of the separated automaton obtained from the original nominal automaton has $n+1$ states, thus dramatically reducing the number of states.
We expect that such a reduction is useful in many applications, such as automata learning (\in{Chapter}[chap:learning-nominal-automata]). We expect that such a reduction is useful in many applications, such as automata learning (\in{Chapter}[chap:learning-nominal-automata]).
@ -230,11 +230,11 @@ An important example is the set $\atoms^{(\ast)}$ of separated words over the at
\stopexample \stopexample
The separated product gives rise to another symmetric closed monoidal structure on $\permnom$, with $1$ as unit, and the exponential object given by \emph{magic wand} $X \wandto Y$. The separated product gives rise to another symmetric closed monoidal structure on $\permnom$, with $1$ as unit, and the exponential object given by \emph{magic wand} $X \wandto Y$.
An explicit characterisation of $X \wandto Y$ is not needed in the remainder of this chapter, but for a complete presentation we briefly recall the description from \citet[Clouston13] (see also the book of \citenp[Pitts13]). An explicit characterisation of $X \wandto Y$ is not needed in the remainder of this chapter, but for a complete presentation we briefly recall the description from \citet[Schoepp06] (see also the book of \citenp[Pitts13] and the paper of \citenp[Clouston13]).
First, define a $\perm$-action on the set of partial functions $f \colon X \rightharpoonup Y$ by $(g \cdot f)(x) = g \cdot f(g^{-1} \cdot x)$ if $f(g^{-1} \cdot x)$ is defined. First, define a $\perm$-action on the set of partial functions $f \colon X \rightharpoonup Y$ by $(g \cdot f)(x) = g \cdot f(g^{-1} \cdot x)$ if $f(g^{-1} \cdot x)$ is defined.
Now, such a partial function $f \colon X \rightharpoonup Y$ is called \emph{separating} if $f$ is finitely supported, $f(x)$ is defined iff $f \separated x$, and $\supp(f) = \bigcup_{x \in \dom(f)} \supp(f(x)) \setminus \supp(x)$. Now, such a partial function $f \colon X \rightharpoonup Y$ is called \emph{separating} if $f$ is finitely supported, $f(x)$ is defined iff $f \separated x$, and $\supp(f) = \bigcup_{x \in \dom(f)} \supp(f(x)) \setminus \supp(x)$.
Finally, $X \wandto Y = \{f \colon X \rightharpoonup Y \mid f \text{ is separating}\}$. Finally, $X \wandto Y = \{f \colon X \rightharpoonup Y \mid f \text{ is separating}\}$.
See \citet[Clouston13] for a proof and explanation. We refer to the thesis of \citet[Schoepp06] (Section 3.3.1) for a proof and explanation.
\startremark[reference=rem:atom-abstr] \startremark[reference=rem:atom-abstr]
The special case $\atoms \wandto Y$ coincides with $[\atoms]Y$, the set of \emph{name abstractions} \citep[Pitts13]. The special case $\atoms \wandto Y$ coincides with $[\atoms]Y$, the set of \emph{name abstractions} \citep[Pitts13].
@ -629,6 +629,12 @@ These automata represent nominal languages which are $\sb$-equivariant, essentia
Our main result is that, if a \quote{classical} nominal automaton (over $\perm$) represents a language $L$ which is $\sb$-equivariant, then $L$ can also be represented by a separated nominal automaton. Our main result is that, if a \quote{classical} nominal automaton (over $\perm$) represents a language $L$ which is $\sb$-equivariant, then $L$ can also be represented by a separated nominal automaton.
The latter can be exponentially smaller (in number of orbits) than the original automaton, as we show in a concrete example. The latter can be exponentially smaller (in number of orbits) than the original automaton, as we show in a concrete example.
\startremark
We will work with a general output set $O$ instead of just acceptance.
The reason for this is that $\sb$-equivariant functions $L \colon \atoms \to 2$ are not very interesting: they are defined purely by the length of the input.
By using more general output $O$, we may still capture interesting behaviour, e.g., the automaton in \in{Example}[ex:fifo].
\stopremark
\startdefinition[reference=def:nominal-aut] \startdefinition[reference=def:nominal-aut]
Let $\Sigma, O$ be $\perm$-sets, called input/output alphabet respectively. Let $\Sigma, O$ be $\perm$-sets, called input/output alphabet respectively.
\startitemize \startitemize
@ -664,12 +670,12 @@ We model a bounded FIFO queue of size $n$ as a nominal Moore automaton, explicit
The input alphabet $\Sigma$ and output alphabet $O$ are as follows: The input alphabet $\Sigma$ and output alphabet $O$ are as follows:
\startformula \startformula
\Sigma = \{ \Put(a) \mid a \in \atoms \} \cup \{ \Pop \}, \Sigma = \{ \Put(a) \mid a \in \atoms \} \cup \{ \Pop \},
\qquad O = \atoms \cup \{ \Null \}. \qquad O = \atoms \cup \{ \perp \}.
\stopformula \stopformula
The input alphabet encodes two actions: The input alphabet encodes two actions:
putting a new value on the queue and popping a value. putting a new value on the queue and popping a value.
The output is either a value (the front of the queue) or $\Null$ if the queue is empty. The output is either a value (the front of the queue) or $\perp$ if the queue is empty.
A queue of size $n$ is modelled by the automaton $(Q, \delta, o, q_0)$ defined as follows. A queue of size $n$ is modelled by the automaton $(Q, \delta, o, q_0)$ defined as follows.
\startformula \startformula
Q = \atoms^{\leq n} \cup \{ \perp \}, Q = \atoms^{\leq n} \cup \{ \perp \},
@ -677,7 +683,7 @@ Q = \atoms^{\leq n} \cup \{ \perp \},
\qquad o(a_1 \ldots a_k) = \qquad o(a_1 \ldots a_k) =
\startmathcases \startmathcases
\NC a_1 \NC if $k \geq 1$ \NR \NC a_1 \NC if $k \geq 1$ \NR
\NC \Null \NC otherwise \NR \NC \perp \NC otherwise \NR
\stopmathcases \stopmathcases
\stopformula \stopformula
\startformula \startformula
@ -697,7 +703,7 @@ Q = \atoms^{\leq n} \cup \{ \perp \},
\delta(\bot, x) = \bot \delta(\bot, x) = \bot
\stopformula \stopformula
The automaton is depicted in \in{Figure}[fig:fifo] for the case $n = 3$. The automaton is depicted in \in{Figure}[fig:fifo] for the case $n = 3$.
The language accepted by this automaton assigns to a word $w$ the first element of the queue after executing the instructions in $w$ from left to right, and $\Null$ if the input is ill-behaved, i.e., $\Pop$ is applied to an empty queue or $\Put(a)$ to a full queue. The language accepted by this automaton assigns to a word $w$ the first element of the queue after executing the instructions in $w$ from left to right, and $\perp$ if the input is ill-behaved, i.e., $\Pop$ is applied to an empty queue or $\Put(a)$ to a full queue.
\startplacefigure \startplacefigure
[title={The FIFO automaton from \in{Example}[ex:fifo] with $n = 3$. [title={The FIFO automaton from \in{Example}[ex:fifo] with $n = 3$.
@ -727,7 +733,6 @@ The language accepted by this automaton assigns to a word $w$ the first element
\stopplacefigure \stopplacefigure
\stopexample \stopexample
\startdefinition[reference=def:sep-aut] \startdefinition[reference=def:sep-aut]
Let $\Sigma, O$ be $\perm$-sets. Let $\Sigma, O$ be $\perm$-sets.
A \emph{separated language} is an equivariant map of the form $\Sigma^{(*)} \to O$. A \emph{separated language} is an equivariant map of the form $\Sigma^{(*)} \to O$.
@ -844,7 +849,7 @@ The converse inclusion of the above proposition does certainly not hold, as show
Let $\mathcal{A}$ be the automaton modelling a bounded FIFO queue (for some $n$), from \in{Example}[ex:fifo]. Let $\mathcal{A}$ be the automaton modelling a bounded FIFO queue (for some $n$), from \in{Example}[ex:fifo].
The $\perm$-nominal language $L$ accepted by $\mathcal{A}$ is $\sb$-equivariant: it is closed under application of arbitrary substitutions. The $\perm$-nominal language $L$ accepted by $\mathcal{A}$ is $\sb$-equivariant: it is closed under application of arbitrary substitutions.
The separated automaton $\mathcal{A}_*$ is given simply be restricting the transition function to $Q \sepprod \Sigma$, i.e., a $\Put(a)$-transition from a state $w \in Q$ exists only if $a$ does not occur in $w$. The separated automaton $\mathcal{A}_*$ is given simply by restricting the transition function to $Q \sepprod \Sigma$, i.e., a $\Put(a)$-transition from a state $w \in Q$ exists only if $a$ does not occur in $w$.
The separated language $S$ accepted by this new automaton is the restriction of the nominal language of $\mathcal{A}$ to separated words. The separated language $S$ accepted by this new automaton is the restriction of the nominal language of $\mathcal{A}$ to separated words.
By \in{Theorem}[thm:separated-sb-lang], we have $L = U(\overline{S})$. By \in{Theorem}[thm:separated-sb-lang], we have $L = U(\overline{S})$.
Hence, the separated automaton $\mathcal{A}_*$ represents $L$, essentially by closing the associated separated language $S$ under all substitutions. Hence, the separated automaton $\mathcal{A}_*$ represents $L$, essentially by closing the associated separated language $S$ under all substitutions.

4
environment.tex
View file

@ -56,6 +56,10 @@ This chapter is based on the following publication:
\define\referencesifcomponent{\doifnotmode{everything}{\startsubject[title={References}]\switchtobodyfont[9pt]\placelistofpublications\stopsubject}} \define\referencesifcomponent{\doifnotmode{everything}{\startsubject[title={References}]\switchtobodyfont[9pt]\placelistofpublications\stopsubject}}
\doifnotmode{everything}
{\setupheadertexts[{\sc {\getmarking[chapter]}}][\pagenumber][\pagenumber][{\sc Chapter {\getmarking[chapternumber]}}]}
\usemodule[algorithmic] \usemodule[algorithmic]
\setupalgorithmic[align=middle,numbercolor=darkgray] % center line numbers \setupalgorithmic[align=middle,numbercolor=darkgray] % center line numbers
\setupalgorithmic[before={\startframedtext[width=0.85\textwidth,offset=none,frame=off]},after={\stopframedtext}] % To enable linenumbers in a float \setupalgorithmic[before={\startframedtext[width=0.85\textwidth,offset=none,frame=off]},after={\stopframedtext}] % To enable linenumbers in a float