joshua/phd-thesis
Archived
1
Fork 0
Code Activity

Learning Nom Autom.

Browse source
This commit is contained in:
Joshua Moerman 2018-08-07 16:15:28 +02:00
parent 56de3e67c4
commit a41524b7c8
6 changed files with 492 additions and 7 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

67
biblio.bib
View file

@ -365,6 +365,41 @@
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/birthday/JacobsS14a,
author = {Bart Jacobs and
Alexandra Silva},
title = {Automata Learning: {A} Categorical Perspective},
booktitle = {Horizons of the Mind. {A} Tribute to Prakash Panangaden - Essays Dedicated
to Prakash Panangaden on the Occasion of His 60th Birthday},
pages = {384--406},
year = {2014},
crossref = {DBLP:conf/birthday/2014panangaden},
url = {https://doi.org/10.1007/978-3-319-06880-0\_20},
doi = {10.1007/978-3-319-06880-0\_20},
timestamp = {Tue, 23 May 2017 01:06:47 +0200},
biburl = {https://dblp.org/rec/bib/conf/birthday/JacobsS14a},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@proceedings{DBLP:conf/birthday/2014panangaden,
editor = {Franck van Breugel and
Elham Kashefi and
Catuscia Palamidessi and
Jan Rutten},
title = {Horizons of the Mind. {A} Tribute to Prakash Panangaden - Essays Dedicated
to Prakash Panangaden on the Occasion of His 60th Birthday},
series = {Lecture Notes in Computer Science},
volume = {8464},
publisher = {Springer},
year = {2014},
url = {https://doi.org/10.1007/978-3-319-06880-0},
doi = {10.1007/978-3-319-06880-0},
isbn = {978-3-319-06879-4},
timestamp = {Tue, 23 May 2017 01:06:45 +0200},
biburl = {https://dblp.org/rec/bib/conf/birthday/2014panangaden},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/tcs/KaminskiF94,
author = {Michael Kaminski and
Nissim Francez},
@ -412,6 +447,22 @@
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/iandc/MalerP95,
author = {Oded Maler and
Amir Pnueli},
title = {On the Learnability of Infinitary Regular Sets},
journal = {Inf. Comput.},
volume = {118},
number = {2},
pages = {316--326},
year = {1995},
url = {https://doi.org/10.1006/inco.1995.1070},
doi = {10.1006/inco.1995.1070},
timestamp = {Thu, 18 May 2017 09:54:20 +0200},
biburl = {https://dblp.org/rec/bib/journals/iandc/MalerP95},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/tcs/MontanariS14,
author = {Ugo Montanari and
Matteo Sammartino},
@ -450,3 +501,19 @@
title={Nominal sets: Names and symmetry in computer science},
year={2013}
}
@article{DBLP:journals/iandc/RivestS93,
author = {Ronald L. Rivest and
Robert E. Schapire},
title = {Inference of Finite Automata Using Homing Sequences},
journal = {Inf. Comput.},
volume = {103},
number = {2},
pages = {299--347},
year = {1993},
url = {https://doi.org/10.1006/inco.1993.1021},
doi = {10.1006/inco.1993.1021},
timestamp = {Thu, 18 May 2017 09:54:18 +0200},
biburl = {https://dblp.org/rec/bib/journals/iandc/RivestS93},
bibsource = {dblp computer science bibliography, https://dblp.org}
}

402
content/learning-nominal-automata.tex
View file

@ -52,7 +52,7 @@ It is important to note that, in the nominal setting, NFAs are strictly more exp
We learn a subclass of the languages accepted by nominal NFAs, which includes all the languages accepted by nominal DFAs.
The main advantage of learning NFAs directly is that they can provide exponentially smaller automata when compared to their deterministic counterpart.
This can be seen both as a generalization and as an optimization of the algorithm.
\item An implementation using our recently developed Haskell library tailored to nominal computation -- NLambda \cite[DBLP:journals/corr/KlinS16].
\item An implementation using our recently developed Haskell library tailored to nominal computation -- NLambda, or \NLambda{}, by \cite[authoryears][DBLP:journals/corr/KlinS16].
Our implementation is the first non-trivial application of a novel programming paradigm of functional programming over infinite structures, which allows the programmer to rely on convenient intuitions of searching through infinite sets in finite time.
\stopitemize
@ -139,12 +139,12 @@ It terminates when the answer is {\bf yes}, otherwise it extends the table with
\IF{$(S, E)$ is not consistent\someline[line:begin-const]}
\STATE find $s_1, s_2 \in S$, $a \in A$, and $e\in E$ such that
\STATE \hfill $row(s_1) = row(s_2)$ and $\lang(s_1 a e) \neq \lang(s_2 a e)$\someline[line:cons-witness]
\STATE $E\gets E\cup \{ae\}$
\STATE $E \gets E\cup \{ae\}$
\ENDIF
\ENDWHILE\someline[line:end-const]
\STATE Make the conjecture $M(S,E)$\someline[line:conj]
\IF{the Teacher replies {\bf no}, with a counter-example $t$\someline[line:counter-ex]}
\STATE $S\gets S\cup pref(t)$ \someline[line:addrow-ex]
\STATE $S \gets S\cup \pref(t)$ \someline[line:addrow-ex]
\ENDIF
\UNTIL{the Teacher replies {\bf yes} to the conjecture $M(S,E)$}
\RETURN $M(S,E)$
@ -330,6 +330,402 @@ This means that in some cases fewer rows will be added for closedness.
\stopsubsection
\stopsection
\startsection
[title={Preliminaries},
reference=sec:prelim]
We recall the notions of nominal sets, nominal automata and nominal regular languages (see \cite[DBLP:journals/corr/BojanczykKL14] for a detailed account).
Let $\EAlph$ be a countable set and let $\Perm(\EAlph)$ be the set of \emph{permutations on $\EAlph$}, i.e., the bijective functions $\pi \colon \EAlph \to \EAlph$.
Permutations form a group where the identity permutation $\id$ is the unit element, inverse is functional inverse and multiplication is function composition.
A \emph{nominal set} \cite[Pitts13] is a set $X$ plus a function $\cdot \colon \Perm(\EAlph) \times X \to X$, interpreting permutations over $X$.
Such function must be a \emph{group action} of $\Perm(\EAlph)$, i.e., it must satisfy $\id \cdot x = x$ and $\pi \cdot (\pi' \cdot x) = (\pi \circ \pi') \cdot x$.
We say that a finite $A \subseteq \EAlph$ \emph{supports} $x \in X$ whenever, for all $\pi$ acting as the identity on $A$, we have $\pi \cdot x = x$.
In other words, permutations that only move elements outside $A$ do not affect $x$.
The support of $x \in X$, denoted $\supp(x)$, is the smallest finite set supporting $x$.
We require nominal sets to have \emph{finite support}, meaning that $\supp(x)$ exists for all $x \in X$.
The \emph{orbit} $\orb(x)$ of $x \in X$ is the set of elements in $X$ reachable from $x$ via permutations, explicitly
\startformula
\orb(x) = \{ \pi \cdot x \mid \pi \in \Perm(\EAlph) \} .
\stopformula
Then $X$ is \emph{orbit-finite} whenever it is a union of finitely many orbits.
Given a nominal set $X$, a subset $Y \subseteq X$ is \emph{equivariant} if it is preserved by permutations, i.e., $\pi \cdot y \in Y$, for all $y \in Y$.
In other words, $Y$ is a union of some orbits of $X$.
This definition extends to the notion of an equivariant relation $R \subseteq X \times Y$, by setting $\pi \cdot (x, y) = (\pi \cdot x, \pi \cdot y)$, for $(x,y) \in R$; similarly for relations of greater arity.
The \emph{dimension} of nominal set $X$ is the maximal size of $\supp(x)$, for any $x \in X$.
Every orbit-finite set has finite dimension.
We define $\EAlph^{(k)} = \{ (a_1, \ldots, a_k) \mid \text{$a_i \neq a_j$ for $i \neq j$}\}$.
For every single-orbit nominal set $X$ with dimension $k$, there is a surjective equivariant map
\startformula
f_X \colon \EAlph^{(k)} \to X .
\stopformula
This map can be used to get an upper bound for the number of orbits of $X_1 \times \dots \times X_n$, for $X_i$ a nominal set with $l_i$ orbits and dimension $k_i$.
Suppose $O_i$ is an orbit of $X_i$.
Then we have a surjection
\startformula
\EAlph^{(k_i)} \times \cdots \times \EAlph^{(k_n)}
\xrightarrow{f_{O_1} \times \cdots \times f_{O_n}} O_1 \times \cdots \times O_n
\stopformula
stipulating that the codomain cannot have more orbits than the domain.
Let $f_\EAlph(\{k_i\})$ denote the number of orbits of $\EAlph^{(k_1)} \times \cdots \times \EAlph^{(k_n)}$, for any finite sequence of natural numbers $\{k_i\}$.
We can form at most $l = l_1 l_2 \ldots l_n$ tuples of the form $O_1 \times \cdots \times O_n$, so $X_1 \times \cdots \times X_n$ has at most $l f_\EAlph(k_1, \ldots, k_n)$ orbits.
For $X$ single-orbit, the \emph{local symmetries} are defined by the group
\startformula
\{ g \in S_k \mid f(x_1, \ldots, x_k) = f(x_{g(1)}, \ldots, x_{g(k)}) \text{ for all } x_i \in X \},
\stopformula
where $k$ is the dimension of $X$ and $S_k$ is the \emph{symmetric group} of permutations over $k$ distinct elements.
NFAs on sets have a finite state space.
We can define \emph{nominal} NFAs, with the requirement that the state space is orbit-finite and the transition relation is equivariant.
A nominal NFA is a tuple $(Q, A, Q_0, F, \delta)$, where:
\startitemize
\item $Q$ is an orbit-finite nominal set of \emph{states};
\item $A$ is an orbit-finite nominal alphabet;
\item $Q_0, F \subseteq Q$ are equivariant subsets of \emph{initial} and \emph{final states};
\item $\delta \subseteq Q \times A \times Q$ is an equivariant \emph{transition relation}.
\stopitemize
A nominal DFA is a special case of nominal NFA where $Q_0 = \{ q_0 \}$ and the transition relation is an equivariant function $\delta \colon Q \times A \to Q$.
Equivariance here can be rephrased as requiring $\delta(\pi \cdot q, \pi \cdot a) = \pi \cdot \delta(q,a)$.
In most examples we take the alphabet to be $A = \EAlph$, but it can be any orbit-finite nominal set.
For instance, $A = Act \times \EAlph$, where $Act$ is a finite set of actions, represents actions $act(x)$ with one parameter $x \in \EAlph$ (actions with arity $n$ can be represented via $n$-fold products of $\EAlph$).
A language $\lang$ is \emph{nominal regular} if it is recognized by a nominal DFA.
The theory of nominal regular languages recasts the classical one using nominal concepts.
A nominal Myhill-Nerode-style \emph{syntactic congruence} is defined: $w, w' \in A^{\ast}$ are \emph{equivalent} w.r.t. $\lang$, written $w \equiv_\lang w'$, whenever
\startformula
wv \in \lang \iff w'v \in \lang
\stopformula
for all $v \in A^{\ast}$.
This relation is equivariant and the set of equivalence classes $[w]_\lang$ is a nominal set.
\starttheorem
(Myhill-Nerode theorem for nominal sets \cite[DBLP:journals/corr/BojanczykKL14])
Let $\lang$ be a regular nominal language.
The following conditions are equivalent:
\startitemize[m]
\item the set of equivalence classes of $\equiv_\lang$ is orbit-finite;
\item $\lang$ is recognized by a nominal DFA.
\stopitemize
\stoptheorem
Unlike what happens for ordinary regular languages, nominal NFAs and nominal DFAs \emph{are not equi-expressive}.
Here is an example of a language accepted by a nominal NFA, but not by a nominal DFA:
\startformula
\lang_{eq} = \left{ a_1 \dots a_n \mid a_i = a_j, \text{for some } i < j \in \left{1, \ldots, n\right} \right}.
\stopformula
In the theory of nominal regular languages, several problems are decidable:
Language inclusion and minimality test for nominal DFAs.
Moreover, orbit-finite nominal sets can be finitely-represented, and so can be manipulated by algorithms.
This is the key idea underpinning our implementation.
\startsubsection
[title={Different Atom Symmetries},
reference=sec:other-symms]
An important advantage of nominal set theory as considered by \cite[authoryears][DBLP:journals/corr/BojanczykKL14] is that it retains most of its properties when the structure of atoms $\EAlph$ is replaced with an arbitrary infinite relational structure subject to a few model-theoretic assumptions.
An example alternative structure of atoms is the total order of rational numbers $(\Q, <)$, with the group of monotone bijections of $\Q$ taking the role of the group of all permutations.
The theory of nominal automata remains similar, and an example nominal language over the atoms $(\Q,<)$ is:
\startformula
\left{ a_1 \ldots a_n \mid a_i \leq a_j, \text{for some } i < j \in \left{1, \ldots, n\right} \right}
\stopformula
which is recognized by a nominal DFA over those atoms.
To simplify the presentation, in this paper we concentrate on the \quotation{equality atoms} only.
Also our implementation of nominal learning algorithms is restricted to equality atoms.
However, both the theory and the implementation can be generalized to other atom structures, with the \quotation{ordered atoms} $(\Q, <)$ as the simplest other example.
We leave the details of this for a future extended version of this paper.
\stopsubsection
\stopsection
\startsection
[title={Angluin's Algorithm for Nominal DFAs},
reference=sec:nangluin]
In our algorithm, we will assume a teacher as described at the start of \in{Section}[sec:overview].
In particular, the teacher is able to answer membership queries and equivalence queries, now in the setting of nominal languages.
We fix a target language $\lang$, which is assumed to be a nominal regular language.
The learning algorithm for nominal automata, \nLStar{}, will be very similar to \LStar{} in \in{Figure}[fig:alg].
In fact, we only change the following lines:
\placeformula[eq:changes]
\startformula
6' S \gets S \cup \orb(sa) \\
9' E \gets E \cup \orb(ae) \\
12' S \gets S \cup \pref(\orb(t))
\stopformula
The basic data structure is an \emph{observation table} $(S, E, T)$ where $S$ and $E$ are orbit-finite subsets of $A^{\ast}$ and $T \colon S \cup S \Lext A \times E \to 2$ is an equivariant function defined by $T(se) = \lang(se)$ for each $s \in S \cup S \Lext A$ and $e \in E$.
Since $T$ is determined by $\lang$ we omit it from the notation.
Let $row \colon S \cup S \Lext A \to 2^E$ denote the curried counterpart of $T$.
Let $u \sim v$ denote the relation $row(u) = row(v)$.
\startdefinition
The table is called \defn{closed} if for each $t \in S \Lext A$ there is a $s \in S$ with $t \sim s$.
The table is called \defn{consistent} if for each pair $s_1, s_2 \in S$ with $s_1 \sim s_2$ we have $s_1 a \sim s_2 a$ for all $a \in A$.
\stopdefinition
The above definitions agree with the abstract definitions given by \cite[authoryears][DBLP:conf/birthday/JacobsS14a] and we may use some of their results implicitly.
The intuition behind the definitions is as follows.
Closedness assures us that for each state we have a successor state for each input.
Consistency assures us that each state has at most one successor for each input.
Together it allows us to construct a well-defined minimal automaton from the observations in the table.
The algorithm starts with a trivial observation table and tries to make it closed and consistent by adding orbits of rows and columns, filling the table via membership queries.
When the table is closed and consistent it constructs a hypothesis automaton and poses an equivalence query.
The pseudocode for the nominal version is the same as listed in \in{Algorithm}[alg:alg], modulo the changes displayed in (\in[eq:changes]).
However, we have to take care to ensure that all manipulations and tests on the (possibly) infinite sets $S, E$ and $A$ terminate in finite time.
We refer to \cite[authoryears][DBLP:journals/corr/BojanczykKL14, Pitts13] for the full details on how to represent these structures and provide a brief sketch here.
The sets $S, E, A$ and $S \Lext A$ can be represented by choosing a representative for each orbit.
The function $T$ in turn can be represented by cells $T_{i,j} \colon \orb(s_i) \times \orb(e_j) \to 2$ for each representative $s_i$ and $e_j$.
Note, however, that the product of two orbits may consist of several orbits, so that $T_{i,j}$ is not a single boolean value.
Each cell is still orbit-finite and can be filled with only finitely many membership queries.
Similarly the curried function $row$ can be represented by a finite structure.
To check whether the table is closed, we observe that if we have a corresponding row $s \in S$ for some $t \in S \Lext A$, this holds for any permutation of $t$.
Hence it is enough to check the following: For all representatives $t \in S \Lext A$ there is a representative $s \in S$ with $row(t) = \pi \cdot row(s)$ for some permutation $\pi$.
Note that we only have to consider finitely many permutations, since the support is finite and so we can decide this property.
Furthermore if the property does not hold, we immediately find a witness represented by $t$.
Consistency is a bit more complicated, but it is enough to consider the set of inconsistencies, $\left{(s_1, s_2, a, e) \mid row(s_1) = row(s_2) \wedge row(s_1 a)(e) \neq row(s_2 a)(e)\right}$.
It is an equivariant subset of $S \times S \times A \times E$ and so it is orbit-finite.
Hence we can decide emptiness and obtain representatives if it is non-empty.
Constructing the hypothesis happens in the same way as before (\in{Section}[sec:overview]), where we note the state space is orbit-finite since it is a quotient of $S$.
Moreover the function $row$ is equivariant, so all structure ($Q_0$, $F$ and $\delta$) is equivariant as well.
The representation given above is not the only way to represent nominal sets.
For example, first-order definable sets can be used as well \cite[DBLP:journals/corr/KlinS16].
From now on we assume to have set theoretic primitives so that each line in \in{Algorithm}[alg:alg] is well defined.
\startsubsection
[title={Correctness}]
To prove correctness we only have to prove that the algorithm terminates, that is, only finitely many hypotheses will be produced.
Correctness follows trivially from termination since the last step of the algorithm is an equivalence query to the teacher inquiring whether an hypothesis automaton accepts the target language.
We start out by listing some facts about observation tables.
\startlemma
[reference=lem:row_equiv]
%\label{lem:nerode_approx}
The relation $\sim$ is an equivariant equivalence relation.
Furthermore, for all $u, v \in S$ we have that $u \equiv_\lang v$ implies $u \sim v$.
\stoplemma
\in{Lemma}[lem:row_equiv] implies that at any stage of the algorithm the number of orbits of $S / {\sim}$ does not exceed the number of orbits of the minimal acceptor with state space $A^{\ast} / {\equiv_\lang}$ (recall that $\equiv_\lang$ is the nominal Myhill-Nerode equivalence relation).
Moreover, the following lemma shows that the dimension of the state space never exceeds the dimension of the minimal acceptor.
Recall that the dimension is the maximal size of the support of any state, which is different than the number of orbits.
\startlemma
[reference=lem:nerode_support]
We have $\supp([u]_{\sim}) \subseteq \supp([u]_{\equiv_\lang}) \subseteq \supp(u)$ for all $u \in S$.
\stoplemma
\startlemma
The automaton constructed from a closed and consistent table is minimal.
\stoplemma
\startproof
Follows from the categorical perspective given by \cite[authoryears][DBLP:conf/birthday/JacobsS14a].
\stopproof
We note that the constructed automaton is consistent with the table (we use that the set $S$ is prefix-closed and $E$ is suffix-closed \cite[DBLP:journals/iandc/Angluin87]).
The following lemma shows that there are no strictly \quotation{smaller} automata consistent with the table.
So the automaton is not just minimal, it is minimal w.r.t. the table.
\startlemma
[reference=lem:minimal_wrt_table]
Let $H$ be the automaton associated with a closed and consistent table $(S, E)$.
If $M'$ is an automaton consistent with $(S, E)$ (meaning that $se \in \lang(M') \iff se \in \lang(H)$ for all $s \in S \cup S \Lext A$ and $e \in E$) and $M'$ has at most as many orbits as $H$,
then there is a surjective map $f \colon Q_{M'} \to Q_H$.
If moreover
\startitemize
\item $M'$s dimension is bounded by the dimension of $H$, i.e., $\supp(m) \subseteq \supp(f(m))$ for all $m \in Q_M'$, and
\item $M'$ has no fewer local symmetries than $H$, i.e., $\pi \cdot f(m) = f(m)$ implies $\pi \cdot m = m$ for all $m \in Q_M'$,
\stopitemize
then $f$ defines an isomorphism $M' \cong H$ of nominal DFAs.
\stoplemma
\startproof
(All maps in this proof are equivariant.)
Define a map $row' \colon Q_M' \to 2^E$ by restricting the language map $Q_M' \to 2^{A^{\ast}}$ to $E$.
First, observe that $row'(\delta'(q_0', s)) = row(s)$ for all $s \in S \cup S \Lext A$, since $\epsilon \in E$ and $M'$ is consistent with the table.
Second, we have $\{ row'(\delta'(q_0', s)) \mid s \in S \} \subseteq \{ row'(q) \mid q \in M' \}$.
Let $n$ be the number of orbits of $H$.
The former set has $n$ orbits by the first observation, the latter set has at most $n$ orbits by assumption.
We conclude that the two sets (both being equivariant) must be equal.
That means that for each $q \in M'$ there is a $s \in S$ such that $row'(q) = row(s)$.
We see that $row' \colon M' \twoheadrightarrow \{ row'(\delta'(q_0', s)) \mid s \} = H$ is a surjective map.
Since a surjective map cannot increase the dimensions of orbits and the dimensions of $M'$ are bounded, we note that the dimensions of the orbits in $H$ and $M'$ have to agree.
Similarly, surjective maps preserve local symmetries.
This map must hence be an isomorphism of nominal sets.
Note that $row'(q) = row'(\delta'(q_0', s))$ implies $q = \delta'(q_0', s)$.
It remains to prove that it respects the automaton structures.
It preserve the initial state: $row'(q_0') = row(\delta'(q_0', \epsilon)) = row(\epsilon)$.
Now let $q \in M'$ be a state and $s \in S$ such that $row'(q) = row(s)$.
It preserves final states: $q \in F' \iff row'(q)(\epsilon) = 1 \iff row(s)(\epsilon) = 1$.
Finally, it preserves the transition structure:
\startformula
row'(\delta'(q, a)) = row'(\delta'(\delta'(q_0', s), a))
= row'(\delta'(q_0', sa)) = row(sa) = \delta(row(s), a)
\stopformula
\stopproof
The above proof is an adaptation of Angluin's proof for automata over sets.
We will now prove termination of the algorithm by proving that all steps are productive.
\starttheorem
[reference=thm:termination]
The algorithm terminates and is hence correct.
\stoptheorem
\startproof
Provided that the if-statements and set operations terminate, we are left proving that
the algorithm adds (orbits of) rows and columns only finitely often.
We start by proving that a table can be made closed and consistent in finite time.
If the table is not closed, we find a row $s_1 \in S \Lext A$ such that $row(s_1) \neq row(s)$ for all $s \in S$.
The algorithm then adds the orbit containing $s_1$ to $S$.
Since $s_1$ was nonequivalent to all rows, we find that $S \cup \orb(t) / {\sim}$ has strictly more orbits than $S / {\sim}$.
Since orbits of $S/\sim$ cannot be more than those of $A^{\ast} / {\equiv_\lang}$, this happens finitely often.
Columns are added in case of an inconsistency.
Here the algorithm finds two elements $s_1, s_2 \in S$ with $row(s_1) = row(s_2)$ but $row(s_1 a e) \neq row(s_2 a e)$ for some $a \in A$ and $e \in E$.
Adding $a e$ to $E$ will ensure that $row'(s_1) \neq row'(s_2)$ ($row'$ is the function belonging to the updated observation table).
If the two elements $row'(s_1), row'(s_2)$ are in different orbits, the number of orbits is increased.
If they are in the same orbit, we have $row'(s_2) = \pi \cdot row'(s_1)$ for some permutation $\pi$. Using $row(s_1) = row(s_2)$ and $row'(s_1) \neq row'(s_2)$ we have:
\startformula
row(s_1) = \pi \cdot row(s_1) \qquad
row'(s_1) \neq \pi \cdot row'(s_1)
\stopformula
Consider all such $\pi$ and suppose there is a $\pi$ and $x \in \supp(row(s_1))$ such that $\pi \cdot x \notin \supp(row(s_1))$.
Then we find that $\pi \cdot x \in \supp(row'(s_1))$, and so the support of the row has grown.
By \in{Lemma}[lem:nerode_support] this happens finitely often.
Suppose such $\pi$ and $x$ do not exist, then we consider the finite group $R = \left{\rho|_{\supp([s_1]_{\sim})} \mid row(s_1) = \rho \cdot row(s_1) \right}$.
We see that $\left{\rho|_{\supp([s_1]_{\sim})} \mid row'(s_1) = \rho \cdot row'(s_1) \right}$ is a proper subgroup of $R$.
So, adding a column in this case decreases the size of the group $R$, which can happen only finitely often.
In this case a local symmetry is removed.
In short, the algorithm will succeed in producing a hypothesis in each round.
It remains to prove that it needs only finitely many equivalence queries.
Let $(S, E)$ be the closed and consistent table and $H$ its corresponding hypothesis.
If it is incorrect, then a second hypothesis $H'$ will be constructed which is consistent with the old table $(S, E)$.
The two hypotheses are nonequivalent, as $H'$ will handle the counter example correctly and $H$ does not.
Therefore, $H'$ will have at least one orbit more, one local symmetry less, or one orbit will have strictly bigger dimension (\in{Lemma}[lem:minimal_wrt_table]),
all of which can only happen finitely often.
\stopproof
We remark that all the lemmas and proofs as above are close to the original ones of Angluin.
However, two things are crucially different.
First, adding a column does not always increase the number of (orbits of) states.
It can happen that by adding a column a bigger support is found or that a local symmetry is broken.
Second, the new hypothesis does not necessarily have more states, again it might have bigger dimensions or less local symmetries.
From the proof \in{Theorem}[thm:termination] we observe moreover that the way we handle counterexamples is not crucial.
Any other method which ensures a nonequivalent hypothesis will work.
In particular our algorithm is easily adapted to include optimizations such as the ones by \cite[authoryears][DBLP:journals/iandc/RivestS93, DBLP:journals/iandc/MalerP95], where counterexamples are added as columns.
\stopsubsection
\startsubsection
[title={Example}]
\todo{Figure \tt 186-257}
Consider the target automaton in \in{Figure}[fig:ex] and an observation table $T_1$ at some stage during the algorithm.
We remind the reader that the table is represented in a symbolic way:
The sequences in the rows and columns stand for whole orbits and the cells denote functions from the product of the orbits to $2$.
Since the cells can consist of multiple orbits, where each orbit is allowed to have a different value, we use a formula to specify which orbits have a $1$.
The table $T_1$ at some stage of the algorithm has to be checked for closedness and consistency.
We note that it is definitely closed.
For consistency we check the rows $row(\epsilon)$ and $row(a)$ which are equal.
Observe, however, that $row(\epsilon b)(\epsilon) = 0$ and $row(ab)(\epsilon) = 1$, so we have an inconsistency.
The algorithm adds the orbit $\orb(b)$ as column and extends the table, obtaining $T_2$.
We note that, in this process, the number of orbits did grow, as the two rows are split.
Furthermore we see that both $row(a)$ and $row(ab)$ have empty support in $T_1$, but not in $T_2$,
because $row(a)(a')$ depends on $a'$ being equal or different from $a$, similarly for $row(ab)(a')$.
The table $T_2$ is still not consistent as we see that $row(ab) = row(ba)$ but $row(abb)(c) = 1$ and $row(bab)(c) = 0$.
Hence the algorithm adds the columns $\orb(bc)$, obtaining table $T_3$.
We note that in this case, no new orbits are obtained and no support has grown.
In fact, the only change here is that the local symmetry between $row(ab)$ and $row(ba)$ is removed.
This last table, $T_3$, is closed and consistent and will produce the correct hypothesis.
\stopsubsection
\startsubsection
[title={Query Complexity},
reference=ssec:lstar-compl]
In this section, we will analyse the number of queries made by the algorithm in the worst case.
Let $M$ be the minimal target automaton with $n$ orbits and of dimension $k$.
We will use $\log$ in base two.
\startlemma[reference=lem:bound_eq]
The number of equivalence queries $E_{n,k}$ is $\bigO(n k \log k)$.
\stoplemma
\startproof
By \in{Lemma}[lem:minimal_wrt_table] each hypothesis will be either
1) bigger in the number of orbits, which is bounded by $n$, or
2) bigger in the dimension of an orbit, which is bounded by $k$ or
3) smaller in local symmetries of an orbit.
For the last part we want to know how long a subgroup series of the permutation group $S_k$ can be.
This is bounded by the number of divisors of $k!$, as each subgroup divides the order of the group.
We can easily bound the number of divisors of any $m$ by $\log m$ and so
one can at take a subgroup at most $k \log k$ times when starting with $S_k$.
Since the hypothesis will grow monotonically in the number of orbits and for each orbit will grow monotonically w.r.t. the remaining two dimensions, the number of equivalence queries is bound by $n + n (k + k \log k)$.
\stopproof
Next we will give a bound for the size of the table.
\startlemma
The table has at most $n + m E_{n,k}$ orbits in $S$ with sequences of at most length $n + m$,
where $m$ is the length of the longest counter example given by the teacher.
The table has at most $n (k + k \log k + 1)$ orbits in $E$ of at most length $n (k + k \log k + 1)$
\stoplemma
\startproof
In the termination proof we noted that rows are added at most $n$ times.
In addition (all prefixes of) counter examples are added as rows which add another $m E_{n,k}$ rows.
Obviously counter examples are of length at most $m$ and are extended at most $n$ times, making the length at most $m + n$ in the worst case.
For columns we note that one of three dimensions approaches a bound similarly to the proof of \in{Lemma}[lem:bound_eq].
So at most $n (k + k \log k + 1)$ columns are added.
Since they are suffix closed, the length is at most $n (k + k \log k + 1)$.
\stopproof
Let $p$ and $l$ denote respectively the dimension and the number of orbits of $A$.
\startlemma
The number of orbits in the lower part of the table, $S \Lext A$, is bounded by $(n + m E_{n,k}) l f_\EAlph( p(n+m), p)$.
\stoplemma
\startproof
Any sequence in $S$ is of length at most $n+m$, so it contains at most $p(n+m)$ distinct atoms.
When we consider $S \Lext A$, the extension can either reuse atoms from those $p(n+m)$, or none at all.
Since the extra letter has at most $p$ distinct atoms, the set $\EAlph^{(p(n+m)) } \times \EAlph^{(p)}$ gives a bound $f_\EAlph(p(n+m),p)$ for the number of orbits of $O_S \times O_A$, with $O_X$ an orbit of $X$.
Multiplying by the number of such ordered pairs, namely $(n + m E_{n,k})l$, gives a bound for $S \Lext A$.
\stopproof
Let $C_{n,k,m} = (n + m E_{n,k}) (l f_\EAlph(p(n+m), p) + 1) n (k + k \log k + 1)$ be the maximal number of cells in the table.
We note that this number is polynomial in $k, l, m$ and $n$ but not in $p$.
\startcorollary
The number of membership queries is bounded by $C_{n,k,m} f_\EAlph(p (n + m), p n (k + k \log k + 1))$.
\stopcorollary
\stopsubsection
\stopsection
\startsection
[title={Learning Non-Deterministic Nominal Automata},
reference=sec:nondet]
\stopsection
\stopchapter
\placelistofpublications
\stopcomponent

9
environment.tex
View file

@ -18,8 +18,13 @@
\defineenumeration[definition][text=Definition]
\defineenumeration[example][text=Example]
\defineenumeration[lemma][text=Lemma]
\defineenumeration[theorem][text=Theorem]
\defineenumeration[corollary][text=Corollary]
\defineenumeration[fact][text=Fact?] % niet nodig?
\setupenumeration[definition,example,lemma,fact][alternative=serried,width=fit,right=.]
\setupenumeration[definition,example,lemma,theorem,corollary,fact][alternative=serried,width=fit,right=.]
\definestartstop[proof][before={{\it Proof. }}, after={\hfill$\square$}]
\definefloat[algorithm][algorithms]
@ -56,5 +61,7 @@
%\showlayout
%\showboxes
%\showframe
%\setupparagraphnumbering[state=start,style=italic,distance=0pt]
\stopenvironment

2
environment/bib.tex
View file

@ -3,7 +3,7 @@
\usebtxdefinitions[apa]
\usebtxdataset[../biblio.bib]
\setupbtx[apa:cite][etallimit=2]
\setupbtx[apa:cite][etallimit=2,separator:4={ and }]
% The dblp database ignores Pauls nice a-breve and s-comma
\btxremapauthor [Paul Fiterau{-}Brostean] [Paul Fiterău-Broștean]

5
environment/font.tex
View file

@ -17,9 +17,10 @@
%\definefallbackfamily[myfamily] [mm] [TeX Gyre Pagella Math][range=uppercasescript,rscale=1.05]
% (Neo) Euler heeft niet alle symbolen, maar Pagella wel
\definefallbackfamily[mainfamily] [mm] [TeX Gyre Pagella Math] [range=0x0266D-0x0266F,rscale=0.95] % sharp and flat
\definefallbackfamily[mainfamily] [mm] [TeX Gyre Pagella Math] [range=0x025B3] % triangle
\definefallbackfamily[mainfamily] [mm] [TeX Gyre Pagella Math] [range={0x025A1,0x025B3}] % triangle, square
% Neo Euler voor wiskunde. Merk op dat dit niet cursief is!
\definefontfamily[mainfamily] [mm] [Neo Euler]
\definefontfamily[mainfamily] [mm] [Neo Euler] [rscale=0.95]
% \definefontfamily[mainfamily] [mm] [Latin Modern Math]
% Gebruik het font
\setupbodyfont[mainfamily,10pt]

14
environment/notation.tex
View file

@ -3,6 +3,9 @@
\define[1]\Fam{\mathcal{#1}}
\define\lang{\mathcal{L}}
\define\autom{\mathcal{A}}
\define\bigO{\mathcal{O}}
\define\pref{pref}
% L* algorithms
\define\LStar{{\tt L}$^{\ast}$}
@ -10,8 +13,19 @@
\define\nLStar{$\nu$\LStar}
\define\nNLStar{$\nu$\NLStar}
% Libraries
\define\ONS{{\sc Ons}}
\define\NLambda{{\sc N}$\lambda$}
\define\LOIS{{\sc Lois}}
% Maths
\define\N{\naturalnumbers}
\define\Q{\rationals}
\define\EAlph{\mathbb{A}}
\define\Perm{Perm}
\define\id{id}
\define\supp{{\tt supp}}
\define\orb{{\tt orb}}
% language extension
\define\Lext{{\cdot}}