diff --git a/biblio.bib b/biblio.bib index 5dc8115..82053b0 100644 --- a/biblio.bib +++ b/biblio.bib @@ -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, author = {Miko{\l}aj Boja{\'{n}}czyk and Bartek Klin and diff --git a/content.tex b/content.tex index 4d320e6..024209a 100644 --- a/content.tex +++ b/content.tex @@ -11,7 +11,7 @@ \midaligned{\framed[width=12cm,align=center,offset=2cm,frame=off]{Nominal Techniques \& Black Box Testing for Automata Learning}} \switchtobodyfont[12pt] \midaligned{Joshua Moerman} -\midaligned{7 January 2019} +\midaligned{8 January 2019} \stop \page[yes] @@ -24,6 +24,7 @@ \startbodymatter +\setupheadertexts[{\sc {\getmarking[chapter]}}][\pagenumber][\pagenumber][{\sc Chapter {\getmarking[chapternumber]}}] \component content/introduction \startpart[title={Testing Techniques}, reference=part:testing] @@ -41,6 +42,7 @@ \startbackmatter +\setupheadertexts[{\sc References}][\pagenumber][\pagenumber][{\sc References}] \switchtobodyfont[8pt] \title{References} \placelistofpublications diff --git a/content/introduction.tex b/content/introduction.tex index e6e03cc..ba5d4a6 100644 --- a/content/introduction.tex +++ b/content/introduction.tex @@ -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. 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. +(This equivalence is exposed in more detail in the book of \citet[Bojanczyk18].) 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. diff --git a/content/minimal-separating-sequences.tex b/content/minimal-separating-sequences.tex index 2c15d5a..80662c5 100644 --- a/content/minimal-separating-sequences.tex +++ b/content/minimal-separating-sequences.tex @@ -2,7 +2,7 @@ \startcomponent minimal-separating-sequences \startchapter - [title={Minimal Separating Sequences \\ for All Pairs of States}, + [title={Minimal Separating Sequences\\for All Pairs of States}, reference=chap:minimal-separating-sequences] \midaligned{~ diff --git a/content/separated-nominal-automata.tex b/content/separated-nominal-automata.tex index 5e72d35..b1275d7 100644 --- a/content/separated-nominal-automata.tex +++ b/content/separated-nominal-automata.tex @@ -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. 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. -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.} 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. 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$. -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. 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$. diff --git a/content/test-methods.tex b/content/test-methods.tex index 9c5be65..5dfc284 100644 --- a/content/test-methods.tex +++ b/content/test-methods.tex @@ -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}. 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]. -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. \startdefinition 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 \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$. @@ -1131,7 +1131,7 @@ A relation $R \subseteq S \times S$ is called a \defn{bisimulation up-to equival \stopdefinition \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 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}\}$. 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}$. -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$, 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: \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$. -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)$. 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 @@ -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. 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. -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 Let $\Fam{W'}$ be a family of state identifiers for $M$. diff --git a/environment.tex b/environment.tex index daccc64..e634ea7 100644 --- a/environment.tex +++ b/environment.tex @@ -5,7 +5,7 @@ \setupexternalfigures[directory={images,../images}] -% \definemode[afloop][yes] +\definemode[afloop][yes] % \definemode[draft][yes] \environment bib diff --git a/environment/headers.tex b/environment/headers.tex index 293e2d5..e353f3d 100644 --- a/environment/headers.tex +++ b/environment/headers.tex @@ -7,8 +7,8 @@ \setuplist[part][style=bold, height=broad, starter={Part }, stopper={:}] % How numbers are shown -\setuphead[part][placehead=yes, command=\MyPart] -\setuphead[chapter][sectionsegments=chapter, command=\MyChapter] +\setuphead[part][placehead=yes, command=\MyPart, header=empty] +\setuphead[chapter][sectionsegments=chapter, command=\MyChapter, header=empty] \setuphead[section][sectionsegments=section] \setuphead[subsection][sectionsegments=section:subsection]