joshua/phd-thesis
Archived
1
Fork 0
Code Activity

Tweaks

Browse source
This commit is contained in:
Joshua Moerman 2019-01-08 15:16:48 +01:00
parent fbb9a1b941
commit 4a92b104bb
8 changed files with 26 additions and 14 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

9
biblio.bib
View file

@ -2330,6 +2330,15 @@
@book{Bojanczyk18,
author = {Miko{\l}aj Boja{\'{n}}czyk},
title = {Slightly Infinite Sets},
publisher = {Draft December 4, 2018},
year = {2018},
url = {https://www.mimuw.edu.pl/~bojan/upload/main-6.pdf}
}
@inproceedings{BojanczykKLT13, @inproceedings{BojanczykKLT13,
author = {Miko{\l}aj Boja{\'{n}}czyk and author = {Miko{\l}aj Boja{\'{n}}czyk and
Bartek Klin and Bartek Klin and

4
content.tex
View file

@ -11,7 +11,7 @@
\midaligned{\framed[width=12cm,align=center,offset=2cm,frame=off]{Nominal Techniques \& Black Box Testing for Automata Learning}} \midaligned{\framed[width=12cm,align=center,offset=2cm,frame=off]{Nominal Techniques \& Black Box Testing for Automata Learning}}
\switchtobodyfont[12pt] \switchtobodyfont[12pt]
\midaligned{Joshua Moerman} \midaligned{Joshua Moerman}
\midaligned{7 January 2019} \midaligned{8 January 2019}
\stop \stop
\page[yes] \page[yes]
@ -24,6 +24,7 @@
\startbodymatter \startbodymatter
\setupheadertexts[{\sc {\getmarking[chapter]}}][\pagenumber][\pagenumber][{\sc Chapter {\getmarking[chapternumber]}}]
\component content/introduction \component content/introduction
\startpart[title={Testing Techniques}, reference=part:testing] \startpart[title={Testing Techniques}, reference=part:testing]
@ -41,6 +42,7 @@
\startbackmatter \startbackmatter
\setupheadertexts[{\sc References}][\pagenumber][\pagenumber][{\sc References}]
\switchtobodyfont[8pt] \switchtobodyfont[8pt]
\title{References} \title{References}
\placelistofpublications \placelistofpublications

1
content/introduction.tex
View file

@ -383,6 +383,7 @@ However, nominal sets are defined in a more elementary way.
The nominal sets we will soon see are introduced by \citet[GabbayP02] to solve certain problems in name binding in abstract syntaxes. The nominal sets we will soon see are introduced by \citet[GabbayP02] to solve certain problems in name binding in abstract syntaxes.
Although this is not really related to automata theory, it was picked up by \citet[BojanczykKL14], Although this is not really related to automata theory, it was picked up by \citet[BojanczykKL14],
who provide an equivalence between register automata and nominal automata. who provide an equivalence between register automata and nominal automata.
(This equivalence is exposed in more detail in the book of \citet[Bojanczyk18].)
Additionally, they generalise the work on nominal sets to other symmetries. Additionally, they generalise the work on nominal sets to other symmetries.
The symmetries we encounter in this thesis are listed below, but other symmetries can be found in the literature. The symmetries we encounter in this thesis are listed below, but other symmetries can be found in the literature.

2
content/minimal-separating-sequences.tex
View file

@ -2,7 +2,7 @@
\startcomponent minimal-separating-sequences \startcomponent minimal-separating-sequences
\startchapter \startchapter
[title={Minimal Separating Sequences \\ for All Pairs of States}, [title={Minimal Separating Sequences\\for All Pairs of States},
reference=chap:minimal-separating-sequences] reference=chap:minimal-separating-sequences]
\midaligned{~ \midaligned{~

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

@ -64,9 +64,9 @@ This is relevant for name abstraction \citep[Pitts13], and has also been studied
We apply these connections between nominal sets and renaming sets in the context of automata theory. We apply these connections between nominal sets and renaming sets in the context of automata theory.
Nominal automata are an elegant model for recognising languages over infinite alphabets. Nominal automata are an elegant model for recognising languages over infinite alphabets.
They are expressively equivalent to the more classical register automata, They are expressively equivalent to the more classical register automata (\citenp[Bojanczyk18], Theorem 6.5),
and have appealing properties that register automata lack, such as unique minimal automata. and have appealing properties that register automata lack, such as unique minimal automata.
However, moving from register automata to nominal automata can lead to an exponential blow-up in the number of states \citep[BojanczykKL14]. However, moving from register automata to nominal automata can lead to an exponential blow-up in the number of states.
\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.
@ -153,7 +153,7 @@ The powerset $\pow(X)$ of a nominal set is not nominal in general; the restricti
If $M$ is a group, then the notion of support can be simplified by using inverses. If $M$ is a group, then the notion of support can be simplified by using inverses.
To see this, first note that, given elements $g_1, g_2 \in M$, $g_1|_C = g_2|_C$ can equivalently be written as $g_1 g_2^{-1}|_C = \id|_C$. To see this, first note that, given elements $g_1, g_2 \in M$, $g_1|_C = g_2|_C$ can equivalently be written as $g_1 g_2^{-1}|_C = \id|_C$.
Second, the statement $x g_1 = x g_2$ can be expressed as $x g_1 g_2^{-1} = x$. Second, the statement $x g_1 = x g_2$ can be expressed as $x g_1 g_2^{-1} = x$.
Hence, $C$ is a support iff $g|_C = \id_C$ implies $gx = x$ for all $g$, which is the standard definition for nominal sets over a group \citep[BojanczykKL14, Pitts13]. Hence, $C$ is a support iff $g|_C = \id_C$ implies $gx = x$ for all $g$, which is the standard definition for nominal sets over a group \citep[Pitts13].
Surprisingly, \citet[GabbayH08] show a similar characterisation also holds for $\sb$-sets. Surprisingly, \citet[GabbayH08] show a similar characterisation also holds for $\sb$-sets.
Moreover, recall that every $\sb$-set is also a $\perm$-set; the associated notions of support coincide on nominal $\sb$-sets, as shown by the following result. Moreover, recall that every $\sb$-set is also a $\perm$-set; the associated notions of support coincide on nominal $\sb$-sets, as shown by the following result.
In particular, this means that the forgetful functor restricts to $U \colon \sbnom \to \permnom$. In particular, this means that the forgetful functor restricts to $U \colon \sbnom \to \permnom$.

12
content/test-methods.tex
View file

@ -1118,12 +1118,12 @@ If two states $s, t$ are related by a bisimulation, then $s \sim t$.
We use a slight generalisation of the bisimulation proof technique, callend \emph{bisimulation up-to}. We use a slight generalisation of the bisimulation proof technique, callend \emph{bisimulation up-to}.
This allows one to give a smaller set $R$ which extends to a bisimulation. This allows one to give a smaller set $R$ which extends to a bisimulation.
A good introduction of these up-to techniques is given by \citet[BonchiP15] or the thesis of \citet[Rot17]. A good introduction of these up-to techniques is given by \citet[BonchiP15] or the thesis of \citet[Rot17].
In our case we use bisimulation \emph{up-to equivalence}. In our case we use bisimulation \emph{up-to ${\sim}$-union}.
The following lemma can be found in the given references. The following lemma can be found in the given references.
\startdefinition \startdefinition
Let $M$ be a Mealy machine. Let $M$ be a Mealy machine.
A relation $R \subseteq S \times S$ is called a \defn{bisimulation up-to equivalence} if for every $(s, t) \in R$ we have A relation $R \subseteq S \times S$ is called a \defn{bisimulation up-to ${\sim}$-union} if for every $(s, t) \in R$ we have
\startitemize \startitemize
\item equal outputs: $\lambda(s, a) = \lambda(t, a)$ for all $a \in I$, and \item equal outputs: $\lambda(s, a) = \lambda(t, a)$ for all $a \in I$, and
\item related successor states: $(\delta(s, a), \delta(t, a)) \in R$ \emph{or} $\delta(s, a) \sim \delta(t, a)$ for all $a \in I$. \item related successor states: $(\delta(s, a), \delta(t, a)) \in R$ \emph{or} $\delta(s, a) \sim \delta(t, a)$ for all $a \in I$.
@ -1131,7 +1131,7 @@ A relation $R \subseteq S \times S$ is called a \defn{bisimulation up-to equival
\stopdefinition \stopdefinition
\startlemma[reference=lem:bisim-upto] \startlemma[reference=lem:bisim-upto]
Any bisimulation up-to equivalence is contained in a bisimulation. Any bisimulation up-to ${\sim}$-union is contained in a bisimulation.
\stoplemma \stoplemma
We fix a specification $M$ which has a minimal representative with $n$ states and an implementation $M'$ with at most $n+k$ states. We fix a specification $M$ which has a minimal representative with $n$ states and an implementation $M'$ with at most $n+k$ states.
@ -1165,7 +1165,7 @@ Second, we show that the reached states are bisimilar.
Define the relation $R = \{(\delta(s_0, p), \delta'(s_0', p)) \mid p \in P \cdot I^{\leq k}\}$. Define the relation $R = \{(\delta(s_0, p), \delta'(s_0', p)) \mid p \in P \cdot I^{\leq k}\}$.
Note that for each $(s, i) \in R$ we have $s \sim_{W_s} i$. Note that for each $(s, i) \in R$ we have $s \sim_{W_s} i$.
For each state $i \in M'$ there is a state $s \in M$ such that $(s, i) \in R$, since we reach all states in both machines by $P \cdot I^{\leq k}$. For each state $i \in M'$ there is a state $s \in M$ such that $(s, i) \in R$, since we reach all states in both machines by $P \cdot I^{\leq k}$.
We will prove that this relation is in fact a bisimulation up-to equivalence. We will prove that this relation is in fact a bisimulation up-to ${\sim}$-union.
For output, we note that $(s, i) \in R$ implies $\lambda(s, a) = \lambda'(i, a)$ for all $a$, For output, we note that $(s, i) \in R$ implies $\lambda(s, a) = \lambda'(i, a)$ for all $a$,
since the machines agree on $P \cdot I^{\leq k+1}$. since the machines agree on $P \cdot I^{\leq k+1}$.
@ -1175,7 +1175,7 @@ We also know that we tested $i_2$ with the set $W'_t$.
So we have: So we have:
\startformula s_2 \sim_{W'_{s_2}} i_2 \sim_{W_t} t. \stopformula \startformula s_2 \sim_{W'_{s_2}} i_2 \sim_{W_t} t. \stopformula
By the second assumption, we conclude that $s_2 \sim t$. By the second assumption, we conclude that $s_2 \sim t$.
So $s_2 \sim t$ and $(t, i) \in R$, which means that $R$ is a bisimulation up-to equivalence. So $s_2 \sim t$ and $(t, i) \in R$, which means that $R$ is a bisimulation up-to ${\sim}$-union.
Moreover, $R$ contains the pair $(s_0, s'_0)$. Moreover, $R$ contains the pair $(s_0, s'_0)$.
By using \in{Lemma}[lem:bisim-upto] and \in{Lemma}[lem:bisim], we conclude that the initial $s_0$ and $s'_0$ are equivalent. By using \in{Lemma}[lem:bisim-upto] and \in{Lemma}[lem:bisim], we conclude that the initial $s_0$ and $s'_0$ are equivalent.
\stopproof \stopproof
@ -1186,7 +1186,7 @@ This proof is very similar to the completeness proof by \citet[Chow78].
In the first part we argue that all states are visited by using some sort of counting and reachability argument. In the first part we argue that all states are visited by using some sort of counting and reachability argument.
Then in the second part we show the actual equivalence. Then in the second part we show the actual equivalence.
To the best of the authors knowledge, this is first $m$-completeness proof which explicitly uses the concept of a bisimulation. To the best of the authors knowledge, this is first $m$-completeness proof which explicitly uses the concept of a bisimulation.
Using a bisimulation allows us to slightly generalise and use bisimulation up-to equivalence, dropping the the often-assumed requirement that $M$ is minimal. Using a bisimulation allows us to slightly generalise and use bisimulation up-to ${\sim}$-union, dropping the the often-assumed requirement that $M$ is minimal.
\startlemma \startlemma
Let $\Fam{W'}$ be a family of state identifiers for $M$. Let $\Fam{W'}$ be a family of state identifiers for $M$.

2
environment.tex
View file

@ -5,7 +5,7 @@
\setupexternalfigures[directory={images,../images}] \setupexternalfigures[directory={images,../images}]
% \definemode[afloop][yes] \definemode[afloop][yes]
% \definemode[draft][yes] % \definemode[draft][yes]
\environment bib \environment bib

4
environment/headers.tex
View file

@ -7,8 +7,8 @@
\setuplist[part][style=bold, height=broad, starter={Part }, stopper={:}] \setuplist[part][style=bold, height=broad, starter={Part }, stopper={:}]
% How numbers are shown % How numbers are shown
\setuphead[part][placehead=yes, command=\MyPart] \setuphead[part][placehead=yes, command=\MyPart, header=empty]
\setuphead[chapter][sectionsegments=chapter, command=\MyChapter] \setuphead[chapter][sectionsegments=chapter, command=\MyChapter, header=empty]
\setuphead[section][sectionsegments=section] \setuphead[section][sectionsegments=section]
\setuphead[subsection][sectionsegments=section:subsection] \setuphead[subsection][sectionsegments=section:subsection]