934 lines
60 KiB
TeX
934 lines
60 KiB
TeX
\project thesis
|
|
\startcomponent ordered-nominal-sets
|
|
|
|
\startchapter
|
|
[title={Fast Computations on Ordered Nominal Sets},
|
|
reference=chap:ordered-nominal-sets]
|
|
|
|
\midaligned{~
|
|
\author[width=0.5\hsize]{David Venhoek \\ Radboud University}
|
|
\author[width=0.5\hsize]{Joshua Moerman \\ Radboud University}
|
|
}
|
|
\midaligned{~
|
|
\author[width=0.5\hsize]{Jurriaan Rot \\ Radboud University}
|
|
}
|
|
|
|
\startabstract
|
|
We show how to compute efficiently with nominal sets over the total order symmetry by developing a direct representation of such nominal sets and basic constructions thereon.
|
|
In contrast to previous approaches, we work directly at the level of orbits, which allows for an accurate complexity analysis.
|
|
The approach is implemented as the library \ONS{}~(Ordered Nominal Sets).
|
|
|
|
Our main motivation is nominal automata, which are models for recognising languages over infinite alphabets.
|
|
We evaluate \ONS{} in two applications:
|
|
minimisation of automata and active automata learning.
|
|
In both cases, \ONS{} is competitive compared to existing implementations and outperforms them for certain classes of inputs.
|
|
\stopabstract
|
|
|
|
\basedon[VenhoekMR18]
|
|
|
|
\page
|
|
|
|
|
|
Automata over infinite alphabets are natural models for programs with unbounded data domains.
|
|
Such automata, often formalised as \emph{register automata}, are applied in modelling and analysis of communication protocols, hardware, and software systems (see \citenp[BojanczykKL14, DAntoniV17, GrigoreT16, KaminskiF94, MontanariP97, Segoufin06] and references therein).
|
|
Typical infinite alphabets include sequence numbers, timestamps, and identifiers.
|
|
This means one can model data flow in such automata beside the basic control flow provided by ordinary automata.
|
|
Recently, it has been shown in a series of papers that such models are amenable to learning \citep[AartsFKV15, BolligHLM13, CasselHJS16, DrewsD17, MoermanS0KS17, Vaandrager17] with the verification of (closed source) TCP implementations by \citet[Fiterau-Brostean16] as a prominent example.
|
|
|
|
A foundational approach to infinite alphabets is provided by the notion of \emph{nominal set}, originally introduced in computer science as an elegant formalism for name binding \citep[GabbayP02, Pitts16].
|
|
Nominal sets have been used in a variety of applications in semantics, computation, and concurrency theory (see \citenp[Pitts13] for an overview).
|
|
\citet[BojanczykKL14] introduce \emph{nominal automata}, which allow one to model languages over infinite alphabets with different symmetries.
|
|
Their results are parametric in the structure of the data values.
|
|
Important examples of data domains are ordered data values (e.g., timestamps) and data values that can only be compared for equality (e.g., identifiers).
|
|
In both data domains, nominal automata and register automata are equally expressive.
|
|
|
|
Important for applications of nominal sets and automata are implementations.
|
|
A couple of tools exist to compute with nominal sets.
|
|
Notably, \NLambda{} \citep[KlinS16] and \LOIS{} \citep[KopczynskiT16, KopczynskiT17] provide a general purpose programming language to manipulate infinite sets.
|
|
\footnote{Other implementations of nominal techniques that are less directly related to our setting (Mihda, Fresh OCaml, and Nominal Isabelle) are discussed in \in{Section}[sec:related].}
|
|
Both tools are based on SMT solvers and use logical formulas to represent the infinite sets.
|
|
These implementations are very flexible, and the SMT solver does most of the heavy lifting, which makes the implementations themselves relatively straightforward.
|
|
Unfortunately, this comes at a cost as SMT solving is in general {\sc Pspace}-hard.
|
|
Since the formulas used to describe sets tend to grow as more calculations are done, running times can become unpredictable.
|
|
|
|
In this chapter, we use a direct representation based on symmetries and orbits, to represent nominal sets.
|
|
We focus on the \emph{total order symmetry}, where data values are rational numbers and can be compared for their order.
|
|
Nominal automata over the total order symmetry are more expressive than automata over the equality symmetry (i.e., traditional register automata of \citenp[KaminskiF94]).
|
|
A key insight is that the representation of nominal sets from \citet[BojanczykKL14] becomes rather simple in the total order symmetry; each orbit is presented solely by a natural number, intuitively representing the number of variables or registers.
|
|
|
|
\noindent
|
|
Our main contributions include the following.
|
|
\startitemize[after]
|
|
\item
|
|
We develop the \emph{representation theory} of nominal sets over the total order symmetry.
|
|
We give concrete representations of nominal sets, their products, and equivariant maps.
|
|
\item
|
|
We provide \emph{time complexity bounds} for operations on nominal sets such as intersections and membership.
|
|
Using those results we give the time complexity of Moore's minimisation algorithm (generalised to nominal automata) and prove that it is polynomial in the number of orbits.
|
|
\item
|
|
Using the representation theory, we are able to \emph{implement nominal sets in a C++ library} \ONS{}.
|
|
The library includes all the results from the representation theory (sets, products, and maps).
|
|
\item
|
|
We \emph{evaluate the performance} of \ONS{} and compare it to \NLambda{} and \LOIS{}, using two algorithms on nominal automata:
|
|
minimisation \citep[BojanczykL12] and automata learning \citep[MoermanS0KS17].
|
|
We use randomly generated automata as well as concrete, logically structured models such as FIFO queues.
|
|
For random automata, our methods are drastically faster than the other tools.
|
|
On the other hand, \LOIS{} and \NLambda{} are faster in minimising the structured automata as they exploit their logical structure.
|
|
In automata learning, the logical structure is not available a-priori, and \ONS{} is faster in most cases.
|
|
\stopitemize
|
|
|
|
The structure of this chapter is as follows.
|
|
\in{Section}[sec:nomsets] contains background on nominal sets and their representation.
|
|
\in{Section}[sec:total-order] describes the concrete representation of nominal sets, equivariant maps and products in the total order symmetry.
|
|
\in{Section}[sec:impl] describes the implementation \ONS{} with complexity results, and \in{Section}[sec:appl] the evaluation of \ONS{} on algorithms for nominal automata.
|
|
Related work is discussed in \in{Section}[sec:related], and future work in \in{Section}[sec:fw].
|
|
|
|
|
|
\startsection
|
|
[title={Nominal sets},
|
|
reference=sec:nomsets]
|
|
|
|
Nominal sets are infinite sets that carry certain symmetries, allowing a finite representation in many interesting cases.
|
|
We recall their formalisation in terms of group actions, following \citet[BojanczykKL14, Pitts13], to which we refer for an extensive introduction.
|
|
|
|
|
|
\startsubsection
|
|
[title={Group actions}]
|
|
|
|
Let $G$ be a group and $X$ be a set.
|
|
A \emph{(left) $G$-action} is a function ${\cdot} \colon G \times X \to X$ satisfying $1 \cdot x = x$ and $(h g) \cdot x = h \cdot (g \cdot x)$ for all $x \in X$ and $g, h \in G$.
|
|
A set $X$ with a $G$-action is called a \emph{$G$-set} and we often write $g x$ instead of $g \cdot x$.
|
|
The \emph{orbit} of an element $x \in X$ is the set $\{g x \mid g \in G\}$.
|
|
A $G$-set is always a disjoint union of its orbits (in other words, the orbits partition the set).
|
|
We say that $X$ is \emph{orbit-finite} if it has finitely many orbits, and we denote the number of orbits by $N(X)$.
|
|
|
|
A map $f \colon X \to Y$ between $G$-sets is called \emph{equivariant} if it preserves the group action, i.e., for all $x \in X$ and $g \in G$ we have $g \cdot f(x) = f(g \cdot x)$.
|
|
If an equivariant map $f$ is bijective, then $f$ is an \emph{isomorphism} and we write $X \cong Y$.
|
|
A subset $Y \subseteq X$ is equivariant if the corresponding inclusion map is equivariant.
|
|
The \emph{product} of two $G$-sets $X$ and $Y$ is given by the Cartesian
|
|
product $X \times Y$ with the point-wise group action on it, i.e., $g (x, y) = (g x, g y)$.
|
|
Union and intersection of $X$ and $Y$ are well-defined if the two
|
|
actions agree on their common elements.
|
|
|
|
|
|
\stopsubsection
|
|
\startsubsection
|
|
[title={Nominal sets}]
|
|
|
|
A \emph{data symmetry} is a pair $(\mathcal{D}, G)$ where $\mathcal{D}$ is a set and $G$ is a subgroup of $\Sym(\mathcal{D})$, the group of bijections on $\mathcal{D}$.
|
|
Note that the group $G$ naturally acts on $\mathcal{D}$ by defining $g x = g(x)$.
|
|
In the most studied instance, called the \emph{equality symmetry}, $\mathcal{D}$ is a countably infinite set and $G = \Sym(\mathcal{D})$.
|
|
In this chapter, we focus on the \emph{total order symmetry} given by $\mathcal{D} = \Q$ and $G = \{\pi \mid \pi \in \Sym(\Q), \pi \text{ is monotone}\}$.
|
|
|
|
Let $(\mathcal{D}, G)$ be a data symmetry and $X$ be a $G$-set.
|
|
A set of data values $S\subseteq \mathcal{D}$ is called a \emph{support} of an element $x \in X$ if for all $g\in G$ with $\forall s \in S: g s = s$ we have $g x = x$.
|
|
A $G$-set $X$ is called \emph{nominal} if every element $x\in X$ has a finite support.
|
|
|
|
\startexample
|
|
We list several examples for the total order symmetry.
|
|
The set $\Q^2$ is nominal as each element $(q_1, q_2) \in \Q^2$ has the finite set $\{q_1, q_2\}$ as its support.
|
|
The set has the following three orbits:
|
|
\startformulas
|
|
\startformula \{(q_1, q_2) \mid q_1 < q_2\} \stopformula
|
|
\startformula \{(q_1, q_2) \mid q_1 = q_2\} \stopformula
|
|
\startformula \{(q_1, q_2) \mid q_1 > q_2\}. \stopformula
|
|
\stopformulas
|
|
|
|
For a set $X$, the set of all subsets of size $n \in \N$ is denoted by $\mathcal{P}_n(X) = \{Y \subseteq X \mid \#Y = n\}$.
|
|
The set $\mathcal{P}_n(\Q)$ is a single-orbit nominal set for each $n$, with the action defined by direct image: $g Y = \{ g y \mid y \in Y \}$.
|
|
The group of monotone bijections also acts by direct image on the full power set $\mathcal{P}(\Q)$, but this is \emph{not} a nominal set.
|
|
For instance, the set $\mathbb{Z} \in \mathcal{P}(\Q)$ of integers has no finite support.
|
|
\stopexample
|
|
|
|
|
|
If $S \subseteq \mathcal{D}$ is a support of an element $x \in X$, then any set $S' \subseteq \mathcal{D}$ such that $S \subseteq S'$ is also a support of $x$.
|
|
A set $S \subset \mathcal{D}$ is a \emph{least finite support} of $x \in X$ if it is a finite support of $x$ and $S \subseteq S'$ for any finite support $S'$ of $x$.
|
|
The existence of least finite supports is crucial for representing orbits.
|
|
Unfortunately, even when elements have a finite support, in general they do not always have a least finite support.
|
|
A data symmetry $(\mathcal{D}, G)$ is said to \emph{admit least supports} if every element of every nominal set has a least finite support.
|
|
Both the equality and the total order symmetry admit least supports.
|
|
(\citenp[BojanczykKL14] give additional (counter)examples of data symmetries admitting least supports.)
|
|
Having least finite supports is useful for a finite representation.
|
|
Henceforth, we will write \emph{least support} to mean least finite support.
|
|
|
|
Given a nominal set $X$, the size of the least support of an element $x \in X$ is denoted by $\dim(x)$, the \emph{dimension} of $x$.
|
|
We note that all elements in the orbit of $x$ have the same dimension.
|
|
For an orbit-finite nominal set $X$, we define $\dim(X) = \max \{ \dim(x) \mid x \in X \}$.
|
|
For a single-orbit set $O$, observe that $\dim(O) = \dim(x)$ where $x$ is any element $x \in O$.
|
|
|
|
|
|
\stopsubsection
|
|
\startsubsection
|
|
[title={Representing nominal orbits},
|
|
reference=subsec:nomorbit]
|
|
|
|
We represent nominal sets as collections of single orbits.
|
|
The finite representation of single orbits is based on the theory of \citet[BojanczykKL14], which uses the technical notions of \emph{restriction} and \emph{extension}.
|
|
We only briefly report their definitions here.
|
|
However, the reader can safely move to the concrete representation theory in \in{Section}[sec:total-order] with only a superficial understanding of \in{Theorem}[representation_tuple] below.
|
|
|
|
The \emph{restriction} of an element $\pi \in G$ to a subset $C \subseteq \mathcal{D}$, written as $\pi|_C$, is the restriction of the function $\pi \colon \mathcal{D} \to \mathcal{D}$ to the domain $C$.
|
|
The restriction of a group $G$ to a subset $C \subseteq \mathcal{D}$ is defined as $G|_C = \{\pi|_C \mid \pi \in G,\, \pi C = C\}$.
|
|
The \emph{extension} of a subgroup $S \le G|_C$ is defined as $\ext_G(S) = \{\pi \in G \mid \pi|_C \in S\}$.
|
|
For $C \subseteq \mathcal{D}$ and $S\le G|_C$, define $[C,S]^{ec} = \{\{g s \mid s \in \ext_G(S)\}\mid g\in G\}$, i.e., the set of right cosets of $\ext_G(S)$ in $G$.
|
|
Then $[C,S]^{ec}$ is a single-orbit nominal set.
|
|
|
|
Using the above, we can formulate the representation theory from \citet[BojanczykKL14].
|
|
This gives a finite description for all single-orbit nominal sets $X$, namely a finite set $C$ together with some of its symmetries.
|
|
|
|
\starttheorem[reference=representation_tuple]
|
|
Let $X$ be a single-orbit nominal set for a data symmetry $(\mathcal{D}, G)$ that admits least supports and let $C \subseteq \mathcal{D}$ be the least support of some element $x \in X$.
|
|
Then there exists a subgroup $S \le G|_C$ such that $X \cong [C,S]^{ec}$.
|
|
\stoptheorem
|
|
|
|
The proof by \citet[BojanczykKL14] uses a bit of category theory:
|
|
it establishes an equivalence of categories between single-orbit sets and the pairs $(C, S)$.
|
|
We will not use the language of category theory much in order to keep the chapter self-contained.
|
|
|
|
|
|
\stopsubsection
|
|
\stopsection
|
|
\startsection
|
|
[title={Representation in the total order symmetry},
|
|
reference=sec:total-order]
|
|
|
|
This section develops a concrete representation of nominal sets over the total order symmetry, as well as their equivariant maps and products.
|
|
It is based on the abstract representation theory from \in{Section}[subsec:nomorbit].
|
|
From now on, by \emph{nominal set} we always refer to a nominal set over the total order symmetry.
|
|
Hence, our data domain is $\Q$ and we take $G$ to be the group of monotone bijections.
|
|
|
|
|
|
\startsubsection
|
|
[title={Orbits and nominal sets},
|
|
reference=sec:orbits-and-nominal-set]
|
|
|
|
From the representation in \in{Section}[subsec:nomorbit], we find that any single-orbit set $X$ can be represented as a tuple $(C,S)$.
|
|
Our first observation is that the finite group $S$ of \quote{local symmetries} in this representation is always trivial, i.e., $S = I$, where $I = \{1\}$ is the trivial group.
|
|
This follows from the following lemma and $S \le G|_C$.
|
|
|
|
\startlemma[reference=group_trivial]
|
|
For every finite subset $C \subset \Q$, we have $G|_C = I$.
|
|
\stoplemma
|
|
|
|
Immediately, we see that $(C, S) = (C, I)$, and hence that the orbit is fully represented by the set $C$.
|
|
A further consequence of \in{Lemma}[group_trivial] is that each \emph{element} of an orbit can be uniquely identified by its least support.
|
|
This leads us to the following characterisation of $[C,I]^{ec}$.
|
|
\startlemma[reference=orbitrep]
|
|
Given a finite subset $C \subset \Q$, we have $[C,I]^{ec} \cong \mathcal{P}_{\#C}(\Q)$.
|
|
\stoplemma
|
|
|
|
By \in{Theorem}[representation_tuple] and the above lemmas, we can represent an orbit by a single integer $n$, the size of the least support of its elements.
|
|
This naturally extends to (orbit-finite) nominal sets with multiple orbits by using a multiset of natural numbers, representing the size of the least support of each of the orbits.
|
|
These multisets are formalised here as functions $f \colon \N \to \N$.
|
|
|
|
\startdefinition[reference=def:present-nom]
|
|
Given a function $f \colon \N \to \N$, we define a nominal set $[f]^{o}$ by
|
|
\startformula
|
|
\[f\]^{o} = \bigcup_{\startsubstack n \in \N \NR 1 \le i \le f(n) \stopsubstack} \{i\} \times \mathcal{P}_n(\Q).
|
|
\stopformula
|
|
\stopdefinition
|
|
|
|
\startproposition[reference=thm:pres-nom]
|
|
For every orbit-finite nominal set $X$, there is a function $f \colon \N \to \N$ such that $X \cong [f]^{o}$ and the set $\{n \mid f(n) \neq 0\}$ is finite.
|
|
Furthermore, the mapping between $X$ and $f$ is one-to-one (up to isomorphism of nominal sets) when restricting to $f \colon \N \to \N$ for which the set $\{n\mid f(n) \ne 0\}$ is finite.
|
|
\stopproposition
|
|
|
|
The presentation in terms of a function $f \colon \N \to \N$ enforces that there are only finitely many orbits of any given dimension.
|
|
The first part of the above proposition generalises to arbitrary nominal sets by replacing the codomain of $f$ by the class of all sets and adapting \in{Definition}[def:present-nom] accordingly.
|
|
However, the resulting correspondence will no longer be one-to-one.
|
|
|
|
As a brief example, let us consider the set $\Q \times \Q$.
|
|
The elements $(a, b)$ split in three orbits, one for $a < b$, one for $a = b$ and one for $a > b$.
|
|
These have dimension 2, 1 and 2 respectively, so the set $\Q \times \Q$ is represented by the multiset $\{1, 2, 2\}$.
|
|
|
|
|
|
\stopsubsection
|
|
\startsubsection
|
|
[title={Equivariant maps},
|
|
reference=sec:eq-maps]
|
|
|
|
We show how to represent equivariant maps, using two basic properties.
|
|
Let $f \colon X \to Y$ be an equivariant map.
|
|
The first property is that the direct image of an orbit (in $X$) is again an orbit (in $Y$),
|
|
that is to say, $f$ is defined \quote{orbit-wise}.
|
|
Second, equivariant maps cannot introduce new elements in the support (but they can drop them).
|
|
More precisely:
|
|
|
|
\startlemma[reference=lem:eqiorbit]
|
|
Let $f \colon X \to Y$ be an equivariant map, and $O\subseteq X$ a single orbit.
|
|
The direct image $f(O) = \{f(x) \mid x \in O\}$ is a single-orbit nominal set.
|
|
\stoplemma
|
|
|
|
\startlemma[reference=eqimap_contained]
|
|
Let $f \colon X \to Y$ be an equivariant map between two nominal sets $X$ and $Y$.
|
|
Let $x\in X$ and let $C$ be a support of $x$.
|
|
Then $C$ supports $f(x)$.
|
|
\stoplemma
|
|
|
|
Hence, equivariant maps are fully determined by associating two pieces of information for each orbit in the domain:
|
|
the orbit on which it is mapped and a string denoting which elements of the least support of the input are preserved.
|
|
These ingredients are formalised in the first part of the following definition.
|
|
The second part describes how these ingredients define an equivariant function.
|
|
\in{Proposition}[eqimap_rep] then states that every equivariant function can be described in this way.
|
|
|
|
\startdefinition[reference=def:eqmap]
|
|
Let $H = \{(I_1, F_1, O_1), \ldots, (I_n, F_n, O_n)\}$ be a finite set of tuples where the $I_i$'s are disjoint single-orbit nominal sets, the $O_i$'s are single-orbit nominal sets with $\dim(O_i) \leq \dim(I_i)$, and the $F_i$'s are bit strings of length $\dim(I_i)$ with exactly $\dim(O_i)$ ones.
|
|
|
|
Given a set $H$ as above, we define $f_H \colon \bigcup I_i \to \bigcup O_i$ as the unique equivariant function such that, given $x \in I_i$ with least support $C$, $f_H(x)$ is the unique element of $O_i$ with support $\{C(j) \mid F_i(j) = 1\}$, where $F_i(j)$ is the $j$-th bit of $F_i$ and $C(j)$ is the $j$-th smallest element of $C$.
|
|
\stopdefinition
|
|
|
|
\startproposition[reference=eqimap_rep]
|
|
For every equivariant map $f \colon X \to Y$ between orbit-finite nominal sets $X$ and $Y$ there is a set $H$ as in \in{Definition}[def:eqmap] such that $f = f_H$.
|
|
\stopproposition
|
|
|
|
Consider the example function $\min \colon \mathcal{P}_3(\Q) \to \Q$ which returns the smallest element of a 3-element set.
|
|
Note that both $\mathcal{P}_3(\Q)$ and $\Q$ are single orbits.
|
|
Since for the orbit $\mathcal{P}_3(\Q)$ we only keep the smallest element of the support, we can thus represent the function $\min$ with $H = \{(\mathcal{P}_3(\Q), 100, \Q)\}$.
|
|
|
|
|
|
\stopsubsection
|
|
\startsubsection
|
|
[title={Products},
|
|
reference=subsec:products]
|
|
|
|
The product $X \times Y$ of two nominal sets is again a nominal set and hence, it can be represented itself in terms of the dimension of each of its orbits as shown in \in{Section}[sec:orbits-and-nominal-set].
|
|
However, this approach has some disadvantages.
|
|
|
|
\startexample[reference=ex:product]
|
|
We start by showing that the orbit structure of products can be non-trivial.
|
|
Consider the product of $X = \Q$ and the set $Y = \{(a,b) \in \Q^2 \mid a < b\}$.
|
|
This product consists of \emph{five} orbits, more than one might naively expect from the fact that both sets are single-orbit:
|
|
\startformula\startalign[width=broad]
|
|
\NC \{(a,(b,c)) \mid a,b,c \in \Q, a < b < c\}, \NC \quad \{(a,(a,b)) \mid a,b \in \Q, a < b\}, \NR
|
|
\NC \{(b,(a,c)) \mid a,b,c \in \Q, a < b < c\}, \NC \quad \{(b,(a,b)) \mid a,b \in \Q, a < b\}, \NR
|
|
\NC \{(c,(a,b)) \mid a,b,c \in \Q, a < b < c\}. \NC \NR
|
|
\stopalign\stopformula
|
|
\stopexample
|
|
|
|
We find that this product is represented by the multiset $\{2,2,3,3,3\}$.
|
|
Unfortunately, this is not sufficient to accurately describe the product as it abstracts away from the relation between its elements with those in $X$ and $Y$.
|
|
In particular, it is not possible to reconstruct the projection maps from such a representation.
|
|
|
|
The essence of our representation of products is that each orbit $O$ in the product $X \times Y$ is described entirely by the dimension of $O$ together with the two (equivariant) projections $\pi_1 \colon O \to X$ and $\pi_2 \colon O \to Y$.
|
|
This combination of the orbit and the two projection maps can already be represented using \in{Propositions}[thm:pres-nom] and \in{}[eqimap_rep].
|
|
However, as we will see, a combined representation for this has several advantages.
|
|
For discussing such a representation, let us first introduce what it means for tuples of a set and two functions to be isomorphic:
|
|
|
|
\startdefinition
|
|
Given nominal sets $X, Y, Z_1$ and $Z_2$, and equivariant functions $l_1 \colon Z_1 \to X$, $r_1 \colon Z_1 \to Y$, $l_2 \colon Z_2 \to X$ and $r_2 \colon Z_2 \to Y$, we define $(Z_1, l_1, r_1) \cong (Z_2, l_2, r_2)$ if there exists an isomorphism $h \colon Z_1 \to Z_2$ such that $l_1 = l_2 \circ h$ and $r_1 = r_2 \circ h$.
|
|
\stopdefinition
|
|
|
|
Our goal is to have a representation that, for each orbit $O$, produces a tuple $(A, f_1, f_2)$ isomorphic to the tuple $(O, \pi_1, \pi_2)$.
|
|
The next lemma gives a characterisation that can be used to simplify such a representation.
|
|
|
|
\startlemma[reference=lm:supp-product]
|
|
Let $X$ and $Y$ be nominal sets and $(x, y) \in X \times Y$.
|
|
If $C$, $C_x$, and $C_y$ are the least supports of $(x, y)$, $x$, and $y$ respectively, then $C = C_x \cup C_y$.
|
|
\stoplemma
|
|
|
|
With \in{Proposition}[eqimap_rep] we represent the maps $\pi_1$ and $\pi_2$ by tuples $(O, F_1, O_1)$ and $(O, F_2, O_2)$ respectively.
|
|
Using \in{Lemma}[lm:supp-product] and the definitions of $F_1$ and $F_2$, we see that at least one of $F_1(i)$ and $F_2(i)$ equals $1$ for each $i$.
|
|
|
|
We can thus combine the strings $F_1$ and $F_2$ into a single string $P \in \{L, R, B\}^{*}$ as follows.
|
|
We set $P(i) = L$ when only $F_1(i)$ is $1$, $P(i) = R$ when only $F_2(i)$ is $1$, and $P(i) = B$ when both are $1$.
|
|
The string $P$ fully describes the strings $F_1$ and $F_2$.
|
|
This process for constructing the string $P$ gives it two useful properties.
|
|
The number of $L$s and $B$s in the string gives the size dimension of $O_1$.
|
|
Similarly, the number of $R$s and $B$s in the string gives the dimension of $O_2$.
|
|
We will call strings with that property \emph{valid}.
|
|
In conclusion, to describe a single orbit of the product $X \times Y$, a valid string $P$ together with the images of $\pi_1$ and $\pi_2$ is sufficient.
|
|
|
|
\startdefinition[reference=def:orbstringdef]
|
|
Let $P \in \{L,R,B\}^{*}$, and $O_1 \subseteq X$, $O_2 \subseteq Y$ be single-orbit sets. Given a tuple $(P, O_1, O_2)$, where the string $P$ is valid, define
|
|
\startformula
|
|
\[(P,O_1,O_2)\]^t = (\mathcal{P}_{|P|}(\Q), f_{H_1}, f_{H_2}),
|
|
\stopformula
|
|
where $H_i = \{(\mathcal{P}_{|P|}(\Q), F_i, O_i)\}$
|
|
and the string $F_1$ is defined as the string $P$ with $L$s and $B$s replaced by $1$s and $R$s by $0$s.
|
|
The string $F_2$ is similarly defined with the roles of $L$ and $R$ swapped.
|
|
\stopdefinition
|
|
|
|
\startproposition[reference=orbstring]
|
|
There exists a one-to-one correspondence between the orbits $O \subseteq X \times Y$, and tuples $(P, O_1, O_2)$ satisfying $O_1 \subseteq X$, $O_2 \subseteq Y$, and where $P$ is a valid string, such that $[(P,O_1,O_2)]^{t} \cong (O, \pi_1|_O, \pi_2|_O)$.
|
|
\stopproposition
|
|
|
|
From the above proposition it follows that we can generate the product $X \times Y$ simply by enumerating all valid strings $P$ for all pairs of orbits $(O_1, O_2)$ of $X$ and $Y$.
|
|
Given this, we can calculate the multiset representation of a product from the multiset representations of both factors.
|
|
|
|
\starttheorem[reference=thm:prod-combinatorics]
|
|
For $X \cong [f]^{o}$ and $Y \cong [g]^{o}$ we have $X \times Y \cong [h]^{o}$, where
|
|
\startformula
|
|
h(n) = \sum_{\startsubstack 0 \le i, j \le n \NR i+j \ge n \stopsubstack} f(i) g(j) {{n}\choose{j}}{{j}\choose{n-i}}.
|
|
\stopformula
|
|
\stoptheorem
|
|
|
|
\startexample
|
|
To illustrate some aspects of the above representation, let us use it to calculate the product of \in{Example}[ex:product].
|
|
First, we observe that both $\Q$ and $S = \{(a,b) \in \Q^2 \mid a < b\}$ consist of a single orbit.
|
|
Hence any orbit of the product corresponds to a triple $(P, \Q, S)$, where the string $P$ satisfies $|P|_L+|P|_B = \dim(\Q) = 1$ and $|P|_R+|P|_B = \dim(S) = 2$.
|
|
We can now find the orbits of the product $\Q \times S$ by enumerating all strings satisfying these equations.
|
|
This yields
|
|
\startitemize
|
|
\item LRR, corresponding to the orbit $\{(a,(b,c)) \mid a,b,c \in \Q, a < b < c\}$,
|
|
\item RLR, corresponding to the orbit $\{(b,(a,c)) \mid a,b,c \in \Q, a < b < c\}$,
|
|
\item RRL, corresponding to the orbit $\{(c,(a,b)) \mid a,b,c \in \Q, a < b < c\}$,
|
|
\item RB, corresponding to the orbit $\{(b,(a,b)) \mid a,b \in \Q, a < b\}$, and
|
|
\item BR, corresponding to the orbit $\{(a,(a,b)) \mid a,b \in \Q, a < b\}$.
|
|
\stopitemize
|
|
Each product string fully describes the corresponding orbit.
|
|
To illustrate, consider the string BR.
|
|
The corresponding bit strings for the projection functions are $F_1 = 10$ and $F_2 = 11$.
|
|
From the lengths of the string we conclude that the dimension of the orbit is $2$.
|
|
The string $F_1$ further tells us that the left element of the tuple consists only of the smallest element of the support.
|
|
The string $F_2$ indicates that the right element of the tuple is constructed from both elements of the support.
|
|
Combining this, we find that the orbit is $\{(a,(a,b)) \mid a,b \in \Q, a < b\}$.
|
|
\stopexample
|
|
|
|
|
|
\stopsubsection
|
|
\startsubsection
|
|
[title={Summary}]
|
|
|
|
We summarise our concrete representation in the following table.
|
|
\in{Propositions}[thm:pres-nom], \in{}[eqimap_rep] and \in{}[orbstring] correspond to the three rows in the table.
|
|
|
|
\placetable[here][tab:overview]{Overview of representation.}
|
|
\starttabulate[|l|p|]
|
|
\NC \emph{Object} \NC \emph{Representation} \NC\NR
|
|
\HL %----------------------------------------
|
|
\NC Single orbit $O$ \NC Natural number $n = \dim(O)$ \NC\NR
|
|
\NC Nominal set $X = \bigcup_i O_i$ \NC Multiset of these numbers \NC\NR
|
|
\HL %----------------------------------------
|
|
\NC Map from single orbit $f \colon O \to Y$ \NC The orbit $f(O)$ and a bit string $F$ \NC\NR
|
|
\NC Equivariant map $f \colon X \to Y$ \NC Set of tuples $(O, F, f(O))$, one for each orbit \NC\NR
|
|
\HL %----------------------------------------
|
|
\NC Orbit in a product $O \subseteq X \times Y$ \NC The corresponding orbits of $X$ and $Y$, and a string $P$ relating their supports \NC\NR
|
|
\NC Product $X \times Y$ \NC Set of tuples $(P, O_X, O_Y)$, one for each orbit \NC\NR
|
|
\stoptabulate
|
|
|
|
Notice that in the case of maps and products, the orbits are inductively represented using the concrete representation.
|
|
As a base case we can represent single orbits by their dimension.
|
|
|
|
|
|
\stopsubsection
|
|
\stopsection
|
|
\startsection
|
|
[title={Implementation and Complexity of ONS},
|
|
reference=sec:impl]
|
|
|
|
The ideas outlined above have been implemented in the \cpp{} library \ONS{}
|
|
\footnote{\ONS{} can be found at \href{https://github.com/davidv1992/ONS}.}
|
|
The library can represent orbit-finite nominal sets and their products, (disjoint) unions, and maps.
|
|
A full description of the possibilities is given in the documentation included with \ONS{}.
|
|
|
|
As an example, the following program computes the product from \in{Example}[ex:product].
|
|
Initially, the program creates the nominal set $A$, containing the entirety of $\Q$.
|
|
Then it creates a nominal set $B$, such that it consists of the orbit containing the element $(1,2) \in \Q \times \Q$.
|
|
For this, the library determines to which orbit of the product $\Q \times \Q$ the element $(1,2)$ belongs, and then stores a description of the orbit as described in \in{Section}[sec:total-order].
|
|
Note that this means that it internally never needs to store the element used to create the orbit.
|
|
The function \kw{nomset_product} then uses the enumeration of product strings mentioned in \in{Section}[subsec:products] to calculate the product of $A$ and $B$.
|
|
Finally, it prints a representative element for each of the orbits in the product.
|
|
These elements are constructed based on the description of the orbits stored, filled in to make their support equal to sets of the form $\{1, 2, \ldots, n\}$.
|
|
|
|
\starttyping
|
|
nomset<rational> A = nomset_rationals();
|
|
nomset<pair<rational, rational>> B({rational(1),rational(2)});
|
|
|
|
auto AtimesB = nomset_product(A, B); // compute the product
|
|
for (auto orbit : AtimesB)
|
|
cout << orbit.getElement() << " ";
|
|
\stoptyping
|
|
|
|
\noindent
|
|
Running this gives the following output
|
|
(where {\tt /1} signifies the denominator):
|
|
|
|
\starttyping
|
|
(1/1,(2/1,3/1)) (1/1,(1/1,2/1)) (2/1,(1/1,3/1))
|
|
(2/1,(1/1,2/1)) (3/1,(1/1,2/1))
|
|
\stoptyping
|
|
|
|
Internally, \kw{orbit} is implemented following the theory presented in \in{Section}[sec:total-order], storing the dimension of the orbit it represents.
|
|
It also contains sufficient information to reconstruct elements given their least support, such as the product string for orbits resulting from a product.
|
|
The class \kw{nomset} then uses a standard set data structure to store the collection of orbits contained in the nominal set it represents.
|
|
|
|
In a similar way, \kw{eqimap} stores equivariant maps by associating each orbit in the domain with the image orbit and the string representing which of the least support to keep.
|
|
This is stored using a map data structure.
|
|
For both nominal sets and equivariant maps, the underlying data structure is currently implemented using trees.
|
|
|
|
|
|
\startsubsection
|
|
[title={Complexity of operations}]
|
|
|
|
Using the concrete representation of nominal sets, we can determine the complexity of common operations.
|
|
To simplify such an analysis, we will make the following assumptions:
|
|
\startitemize
|
|
\item The comparison of two orbits takes $O(1)$.
|
|
\item Constructing an orbit from an element takes $O(1)$.
|
|
\item Checking whether an element is in an orbit takes $O(1)$.
|
|
\stopitemize
|
|
These assumptions are justified as each of these operations takes time proportional to the size of the representation of an individual orbit, which in practice is small and approximately constant.
|
|
For instance, the orbit $\mathcal{P}_n(\Q)$ is represented by just the integer $n$ and its type.
|
|
|
|
\starttheorem[reference=thmcomplexity]
|
|
If nominal sets are implemented with a tree-based set structure (as in \ONS{}), the complexity of the following set operations is as follows.
|
|
Recall that $\Nsize(X)$ denotes the number of orbits of $X$.
|
|
We use $p$ and $f$ to denote functions implemented in whatever way the user wants, which we assume to take $O(1)$ time.
|
|
The software assumes these are equivariant, but this is not verified.
|
|
|
|
\placetable[here][tab:complexity]{Time complexity of operations on nominal sets.}
|
|
\starttabulate[|r|l|]
|
|
\NC \emph{Operation} \VL \emph{Complexity} \NC\NR
|
|
\HL
|
|
\NC Test $x \in X$ \VL $O(\log \Nsize(X))$ \NC\NR
|
|
\NC Test $X\subseteq Y$ \VL $O(\min(\Nsize(X)+\Nsize(Y), \Nsize(X)\log \Nsize(Y)))$ \NC\NR
|
|
\NC Calculate $X \cup Y$ \VL $O(\Nsize(X)+\Nsize(Y))$ \NC\NR
|
|
\NC Calculate $X \cap Y$ \VL $O(\Nsize(X)+\Nsize(Y))$ \NC\NR
|
|
\NC Calculate $\{x \in X \mid p(x)\}$ \VL $O(\Nsize(X))$ \NC\NR
|
|
\NC Calculate $\{f(x) \mid x \in X\}$ \VL $O(\Nsize(X)\log \Nsize(X))$ \NC\NR
|
|
\NC Calculate $X\times Y$ \VL $O(\Nsize(X\times Y)) \,\subseteq\, O(3^{\dim(X)+\dim(Y)}\Nsize(X)\Nsize(Y))$ \NC\NR
|
|
\stoptabulate
|
|
\stoptheorem
|
|
|
|
\startproofnoqed
|
|
Since most parts are proven similarly, we only include proofs for the first and last item.
|
|
|
|
\description{Membership.}
|
|
To decide $x \in X$, we first construct the orbit containing $x$, which is done in constant time.
|
|
Then we use a logarithmic lookup to decide whether this orbit is in our set data structure.
|
|
Hence, membership checking is $O(\log(\Nsize(X)))$.
|
|
|
|
\startdescription[title={Products.}]
|
|
Calculating the product of two nominal sets is the most complicated construction.
|
|
For each pair of orbits in the original sets $X$ and $Y$, all product strings need to be generated.
|
|
Each product orbit itself is constructed in constant time.
|
|
By generating these orbits in-order, the resulting set takes $O(\Nsize(X \times Y))$ time to construct.
|
|
|
|
We can also give an explicit upper bound for the number of orbits in terms of the input.
|
|
Recall that orbits in a product are represented by strings of length at most $\dim(X)+\dim(Y)$.
|
|
(If the string is shorter, we pad it with one of the symbols.)
|
|
Since there are three symbols ($L, R$ and $B$), the product of $X$ and $Y$ will have at most $3^{\dim(X)+\dim(Y)}\Nsize(X)\Nsize(Y)$ orbits.
|
|
It follows that taking products has time complexity of $O(3^{\dim(X)+\dim(Y)}\Nsize(X)\Nsize(Y))$.
|
|
\QED
|
|
\stopdescription
|
|
\stopproofnoqed
|
|
|
|
|
|
\stopsubsection
|
|
\stopsection
|
|
\startsection
|
|
[title={Results and evaluation in automata theory},
|
|
reference=sec:appl]
|
|
|
|
In this section we consider applications of nominal sets to automata theory.
|
|
As mentioned in the introduction, nominal sets are used to formalise languages over infinite alphabets.
|
|
These languages naturally arise as the semantics of register automata.
|
|
The definition of register automata is not as simple as that of ordinary finite automata.
|
|
Consequently, transferring results from automata theory to this setting often requires non-trivial proofs.
|
|
Nominal automata, instead, are defined as ordinary automata by replacing finite sets with orbit-finite nominal sets.
|
|
The theory of nominal automata is developed by \citet[BojanczykKL14] and it is shown that many, but not all, algorithms from automata theory transfer to nominal automata.
|
|
|
|
As an example we consider the following language on rational numbers:
|
|
\startformula
|
|
\Lint = \{ a_1 b_1 \cdots a_n b_n \mid a_i, b_i \in \Q, a_i < a_{i+1} < b_{i+1} < b_i \text{ for all } i \}.
|
|
\stopformula
|
|
We call this language the \emph{interval language} as a word $w \in \Q^{\ast}$ is in the language when it denotes a sequence of nested intervals.
|
|
This language contains arbitrarily long words.
|
|
For this language it is crucial to work with an infinite alphabet as for each finite set $C \subset \Q$, the restriction $\Lint \cap C^{\ast}$ is just a finite language.
|
|
Note that the language is equivariant: $w \in \Lint \iff wg \in \Lint$ for any monotone bijection $g$, because nested intervals are preserved by monotone maps.
|
|
\footnote{The $G$-action on words is defined point-wise: $g (w_1 \ldots w_n) = (g w_1) \ldots (g w_n)$.}
|
|
Indeed, $\Lint$ is a nominal set, although it is not orbit-finite.
|
|
|
|
Informally, the language $\Lint$ can be accepted by the automaton depicted in \in{Figure}[fig:lint-minimal].
|
|
Here we allow the automaton to store rational numbers and compare them to new symbols.
|
|
For example, the transition from $q_2$ to $q_3$ is taken if any value $c$ between $a$ and $b$ is read and then the currently stored value $a$ is replaced by $c$.
|
|
For any other value read at state $q_2$ the automaton transitions to the sink state $q_4$.
|
|
Such a transition structure is made precise by the notion of nominal automata.
|
|
|
|
\startplacefigure
|
|
[title={Example automaton that accepts the language $\Lint$.},
|
|
reference=fig:lint-minimal]
|
|
\hbox{\starttikzpicture[node distance=3.5cm]
|
|
\node (S 0) [state] {$q_0$};
|
|
\node (S 1) [state, right of=S 0] {$q_1(a)$};
|
|
\node (S 2) [state, accepting, right of=S 1] {$q_2(a,b)$};
|
|
\node (S 3) [state, right of=S 2] {$q_3(a,b)$};
|
|
\node (S 4) [state, below=1.5cm of S 2] {$q_4$};
|
|
|
|
\path[->]
|
|
(S 0) edge node[above] {$a$} (S 1)
|
|
(S 1) edge node[above] {$b > a$} (S 2)
|
|
(S 1) edge[bend right] node[below left] {$b \le a$} (S 4)
|
|
(S 2) edge[bend left=10] node[above,align=center] {$a<c<b$\\$a \leftarrow c$} (S 3)
|
|
(S 3) edge[bend left=10] node[below,align=center] {$a<c<b$\\$b \leftarrow c$} (S 2)
|
|
(S 2) edge[bend right=10] node[left] {$c \le a$} (S 4)
|
|
(S 2) edge[bend left=10] node[right] {$c \ge b$} (S 4)
|
|
(S 3) edge[bend left] node[above left] {$c \le a$} (S 4)
|
|
(S 3) edge[bend left=60] node[below right] {$c \ge b$} (S 4)
|
|
(S 4) edge[loop below] node [below] {$a$} (S 4);
|
|
\stoptikzpicture}
|
|
\stopplacefigure
|
|
|
|
\startdefinition
|
|
A \emph{nominal language} is an equivariant subset $L \subseteq A^{*}$ where $A$ is an orbit-finite nominal set.
|
|
\stopdefinition
|
|
|
|
\startdefinition
|
|
A \emph{nominal deterministic finite automaton} is a tuple $(S,A,F,\delta)$, where $S$ is an orbit-finite nominal set of states, $A$ is an orbit-finite nominal set of symbols, $F \subseteq S$ is an equivariant subset of final states, and $\delta \colon S \times A \to S$ is the equivariant transition function.
|
|
|
|
Given a state $s \in S$, we define the usual acceptance condition: a word $w \in A^{*}$ is \emph{accepted} if $w$ denotes a path from $s$ to a final state.
|
|
\stopdefinition
|
|
|
|
The automaton in \in{Figure}[fig:lint-minimal] can be formalised as a nominal deterministic finite automaton as follows.
|
|
Let $S = \{ q_0, q_4 \} \cup \{ q_1(a) \mid a \in \Q \} \cup \{ q_2(a, b) \mid a < b \in \Q \} \cup \{ q_3(a, b) \mid a < b \in \Q \}$ be the set of states, where the group action is defined as one would expect.
|
|
The transition we described earlier can now be formally defined as $\delta(q_2(a,b), c) = q_3(c,b)$ for all $a < c < b \in \Q$.
|
|
By defining $\delta$ on all states accordingly and defining the final states as $F = \{ q_2(a, b) \mid a < b \in \Q \}$, we obtain a nominal deterministic automaton $(S, \Q, F, \delta)$.
|
|
The state $q_0$ accepts the language $\Lint$.
|
|
|
|
We implement two algorithms on nominal automata, minimisation and learning, to benchmark \ONS{}.
|
|
The performance of \ONS{} is compared to two existing libraries for computing with nominal sets, \NLambda{} and \LOIS{}.
|
|
The following automata will be used.
|
|
|
|
|
|
\startsubsubject
|
|
[title={Random automata}]
|
|
|
|
As a primary test suite, we generate random automata as follows.
|
|
The input alphabet is always $\Q$ and the number of orbits and dimension $k$ of the state space $S$ are fixed.
|
|
For each orbit in the set of states, its dimension is chosen uniformly at random between $0$ and $k$, inclusive.
|
|
Each orbit has a probability $\frac{1}{2}$ of consisting of accepting states.
|
|
|
|
To generate the transition function $\delta$, we enumerate the orbits of $S \times \Q$ and choose a target state uniformly from the orbits $S$ with small enough dimension.
|
|
The bit string indicating which part of the support is preserved is then sampled uniformly from all valid strings. We will denote these automata as rand$_{N(S),k}$.
|
|
The choices made here are arbitrary and only provide basic automata.
|
|
We note that the automata are generated orbit-wise and this may favour our tool.
|
|
|
|
|
|
\stopsubsubject
|
|
\startsubsubject
|
|
[title={Structured automata}]
|
|
|
|
Besides random automata we wish to test the algorithms on more structured automata.
|
|
We define the following automata.
|
|
|
|
\description{FIFO($n$)}
|
|
Automata accepting valid traces of a finite FIFO data structure of size $n$.
|
|
The alphabet is defined by two orbits: $\{\kw{Put}(a) \mid a \in \Q \}$ and $\{\kw{Get}(a) \mid a \in \Q \}$.
|
|
|
|
\description{$ww(n)$} Automata accepting the language of words of the form $ww$, where $w \in \Q^{n}$.
|
|
|
|
\description{$\Lmax$} The language $\Lmax = \{ w a \in \Q^{*} \mid a = \max(w_1, \dots, w_n) \}$ where the last symbol is the maximum of previous symbols.
|
|
|
|
\description{$\Lint$} The language accepting a series of nested intervals, as defined before.
|
|
|
|
In \in{Table}[minimize_results] we report the number of orbits for each automaton.
|
|
The first two classes of automata are described in \in{Chapter}[chap:learning-nominal-automata].
|
|
These two classes are also equivariant w.r.t. the equality symmetry.
|
|
|
|
Extra structure allows the automata to be encoded more efficiently, as we do not need to encode a transition for each orbit in $S \times A$.
|
|
Instead, a more symbolic encoding is possible.
|
|
Both \LOIS{} and \NLambda{} allow to use this more symbolic representation.
|
|
Our tool, \ONS{}, only works with nominal sets and the input data needs to be provided orbit-wise.
|
|
Where applicable, the automata listed above were generated using the code from \citet[MoermanS0KS17], ported to the other libraries as needed.
|
|
|
|
|
|
\stopsubsubject
|
|
\startsubsection
|
|
[title={Minimising nominal automata}]
|
|
|
|
For languages recognised by nominal DFAs, a Myhill-Nerode theorem holds which relates states to right congruence classes \citep[BojanczykKL14].
|
|
This guarantees the existence of unique minimal automata.
|
|
We say an automaton is \emph{minimal} if its set of states has the least number of orbits and each orbit has the smallest dimension possible.
|
|
\footnote{Abstractly, an automaton is minimal if it has no proper quotients.
|
|
Minimal deterministic automata are unique up to isomorphism.}
|
|
We generalise Moore's minimisation algorithm to nominal DFAs (\in{Algorithm}[alg:moore]) and analyse its time complexity using the bounds from \in{Section}[sec:impl].
|
|
|
|
\startplacealgorithm
|
|
[title={Moore's minimisation algorithm for nominal DFAs.},
|
|
reference=alg:moore]
|
|
\startalgorithmic
|
|
\REQUIRE{Nominal automaton $M = (S,A,F,\delta)$}
|
|
\ENSURE{Minimal nominal automaton equivalent to $M$}
|
|
\startlinenumbering
|
|
\STATE $i \gets 0$
|
|
\STATE ${\equiv_{-1}} \gets S \times S$
|
|
\STATE ${\equiv_{0}} \gets F \times F \cup (S\backslash F)\times (S\backslash F)$
|
|
\WHILE{${\equiv_i} \ne {\equiv_{i-1}}$\startline[line:loop]}
|
|
\STATE ${\equiv_{i+1}} \gets \{ (q_1, q_2) \mid (q_1, q_2) \in {\equiv_i} \wedge \forall a \in A, (\delta(q_1, a), \delta(q_2, a)) \in {\equiv_i} \}$\someline[line:main-work]
|
|
\STATE $i \gets i+1$
|
|
\ENDWHILE\stopline[line:loop]
|
|
\STATE $E \gets S/_{\equiv_i}$
|
|
\STATE $F_E \gets \{e \in E \mid \forall s \in e, s \in F\}$
|
|
\STATE Let $\delta_E$ be the map such that, if $s \in e$ and $\delta(s, a) \in e'$, then $\delta_E(e, a) = e'$
|
|
\RETURN $(E,A,F_E,\delta_E)$
|
|
\stoplinenumbering
|
|
\stopalgorithmic
|
|
\stopplacealgorithm
|
|
|
|
\starttheorem[reference=thm:moore]
|
|
The runtime complexity of Moore's algorithm on nominal deterministic automata is $O(3^{5k} k \Nsize(S)^3 \Nsize(A))$, where $k=\dim(S\cup A)$.
|
|
\stoptheorem
|
|
|
|
\startproof
|
|
This is shown by counting operations, using the complexity results of set operations stated in \in{Theorem}[thmcomplexity].
|
|
We first focus on the while loop on \inline[line:loop].
|
|
The runtime of an iteration of the loop is determined by \inline[line:main-work], as this is the most expensive step.
|
|
Since the dimensions of $S$ and $A$ are at most $k$, computing $S \times S \times A$ takes $O(\Nsize(S)^2 \Nsize(A) 3^{5k})$.
|
|
Filtering $S \times S$ using that then takes $O(\Nsize(S)^2 3^{2k})$.
|
|
The time to compute $S \times S \times A$ dominates, hence each iteration of the loop takes $O(\Nsize(S)^2 \Nsize(A) 3^{5k})$.
|
|
|
|
Next, we need to count the number of iterations of the loop.
|
|
Each iteration of the loop gives rise to a new partition, refining the previous partition.
|
|
Furthermore, every partition generated is equivariant. Note that this implies that each refinement of the partition does at least one of two things:
|
|
distinguish between two orbits of $S$ previously in the same element(s) of the partition, or distinguish between two members of the same orbit previously in the same element of the partition.
|
|
The former can happen only $\Nsize(S)-1$ times, as after that there are no more orbits lumped together.
|
|
The latter can only happen $\dim(S)$ times per orbit, because each such a distinction between elements is based on splitting on the value of one of the elements of the support.
|
|
Hence, after $\dim(S)$ times on a single orbit, all elements of the support are used up. Combining this, the longest chain of partitions of $S$ has length at most $O(k \Nsize(S))$.
|
|
|
|
Since each partition generated in the loop is unique, the loop cannot run for more iterations than the length of the longest chain of partitions on $S$.
|
|
It follows that there are at most $O(k \Nsize(S))$ iterations of the loop, giving the loop a complexity of $O(k \Nsize(S)^3 \Nsize(A) 3^{5k})$
|
|
|
|
The remaining operations outside the loop have a lower complexity than that of the loop, hence the complexity of Moore's minimisation algorithm for a nominal automaton is $O(k \Nsize(S)^3 \Nsize(A) 3^{5k})$.
|
|
\stopproof
|
|
|
|
The above theorem shows in particular that minimisation of nominal automata is fixed-parameter tractable (FPT) with the dimension as fixed parameter.
|
|
The complexity of \in{Algorithm}[alg:moore] for nominal automata is very similar to the $O((\#S)^3 \#A)$ bound given by a naive implementation of Moore's algorithm for ordinary DFAs.
|
|
This suggest that it is possible to further optimise an implementation with similar techniques used for ordinary automata.
|
|
|
|
|
|
\startsubsubject
|
|
[title={Implementations}]
|
|
|
|
We implemented the minimisation algorithm in \ONS{}.
|
|
For \NLambda{} and \LOIS{} we used their implementations of Moore's minimisation algorithm \citep[KlinS16, KopczynskiT16, KopczynskiT17].
|
|
For each of the libraries, we wrote routines to read in an automaton from a file and,
|
|
for the structured test cases, to generate the requested automaton.
|
|
For \ONS{}, all automata were read from file.
|
|
The output of these programs was manually checked to see if the minimisation was performed correctly.
|
|
|
|
|
|
\stopsubsubject
|
|
\startsubsubject
|
|
[title={Results}]
|
|
|
|
The results (shown in \in{Table}[minimize_results]) for random automata show a clear advantage for \ONS{}, which is capable of running all supplied testcases in less than one second.
|
|
This in contrast to both \LOIS{} and \NLambda{}, which take more than $2$ hours on the largest random automata.
|
|
|
|
\startplacetable
|
|
[title={Running times for \in{Algorithm}[alg:moore] implemented in the three libraries.
|
|
$N(S)$ is the size of the input and $N(S^{\text{min}})$ the size of the minimal automaton.
|
|
For \ONS{}, the time used to generate the automaton is reported separately (in grey).
|
|
Timeouts are indicated by $\infty$.},
|
|
list={Running times for minimisation.},
|
|
reference=minimize_results]
|
|
\starttabulate[|l|c|c|cg{.}|cg{.}|cg{.}|cg{.}|][distance=none]
|
|
\NC Type \NC $\Nsize(S)$ \NC $\Nsize(S^{\text{min}})$ \VL \ONS{} (s) \NC \color[darkgray]{Gen (s)} \VL \NLambda{} (s) \VL \LOIS{} (s) \NC\NR
|
|
\HL
|
|
\NC rand$_{5,1}$ (x10) \NC 5 \NC n/a \VL 0.02 \NC \color[darkgray]{n/a} \VL 0.82 \VL 3.14 \NC\NR
|
|
\NC rand$_{10,1}$ (x10) \NC 10 \NC n/a \VL 0.03 \NC \color[darkgray]{n/a} \VL 17.03 \VL 92 \NC\NR
|
|
\NC rand$_{10,2}$ (x10) \NC 10 \NC n/a \VL 0.09 \NC \color[darkgray]{n/a} \VL 2114 \VL $\infty$ \NC\NR
|
|
\NC rand$_{15,1}$ (x10) \NC 15 \NC n/a \VL 0.04 \NC \color[darkgray]{n/a} \VL 87 \VL 620 \NC\NR
|
|
\NC rand$_{15,2}$ (x10) \NC 15 \NC n/a \VL 0.11 \NC \color[darkgray]{n/a} \VL 3346 \VL $\infty$ \NC\NR
|
|
\NC rand$_{15,3}$ (x10) \NC 15 \NC n/a \VL 0.46 \NC \color[darkgray]{n/a} \VL $\infty$ \VL $\infty$ \NC\NR
|
|
\HL
|
|
\NC FIFO($2$) \NC 13 \NC 6 \VL 0.01 \NC \color[darkgray]{0.01} \VL 1.37 \VL 0.24 \NC\NR
|
|
\NC FIFO($3$) \NC 65 \NC 19 \VL 0.38 \NC \color[darkgray]{0.09} \VL 11.59 \VL 2.4 \NC\NR
|
|
\NC FIFO($4$) \NC 440 \NC 94 \VL 39.11 \NC \color[darkgray]{1.60} \VL 76 \VL 14.95 \NC\NR
|
|
\NC FIFO($5$) \NC 3686 \NC 635 \VL $\infty$ \NC \color[darkgray]{39.78} \VL 402 \VL 71 \NC\NR
|
|
\HL
|
|
\NC $ww(2)$ \NC 8 \NC 8 \VL 0.00 \NC \color[darkgray]{0.00} \VL 0.14 \VL 0.03 \NC\NR
|
|
\NC $ww(3)$ \NC 24 \NC 24 \VL 0.19 \NC \color[darkgray]{0.02} \VL 0.88 \VL 0.16 \NC\NR
|
|
\NC $ww(4)$ \NC 112 \NC 112 \VL 26.44 \NC \color[darkgray]{0.25} \VL 3.41 \VL 0.61 \NC\NR
|
|
\NC $ww(5)$ \NC 728 \NC 728 \VL $\infty$ \NC \color[darkgray]{6.37} \VL 10.54 \VL 1.80 \NC\NR
|
|
\HL
|
|
\NC $\Lmax$ \NC 5 \NC 3 \VL 0.00 \NC \color[darkgray]{0.00} \VL 2.06 \VL 0.03 \NC\NR
|
|
\NC $\Lint$ \NC 5 \NC 5 \VL 0.00 \NC \color[darkgray]{0.00} \VL 1.55 \VL 0.03 \NC\NR
|
|
\stoptabulate
|
|
\stopplacetable
|
|
|
|
The results for structured automata show a clear effect of the extra structure.
|
|
Both \NLambda{} and \LOIS{} remain capable of minimising the automata in reasonable amounts of time for larger sizes.
|
|
In contrast, \ONS{} benefits little from the extra structure.
|
|
Despite this, it remains viable: even for the larger cases it falls behind significantly only for the largest FIFO automaton and the two largest $ww$ automata.
|
|
|
|
|
|
\stopsubsubject
|
|
\stopsubsection
|
|
\startsubsection
|
|
[title={Learning nominal automata}]
|
|
|
|
Another application that we implemented in \ONS{} is \emph{automata learning}.
|
|
The aim of automata learning is to infer an unknown regular language $\lang$.
|
|
We use the framework of active learning as set up by \citet[Angluin87]
|
|
where a learning algorithm can query an oracle to gather information about $\lang$.
|
|
Formally, the oracle can answer two types of queries:
|
|
\startitemize
|
|
\item \emph{membership queries}, where a query consists of a word $w \in A^{*}$ and the oracle replies whether $w \in \lang$, and
|
|
\item \emph{equivalence queries}, where a query consists of an automaton $\mathcal{H}$ and the oracle replies positively if $\lang(\mathcal{H}) = \lang$ or provides a counterexample if $\lang(\mathcal{H}) \neq \lang$.
|
|
\stopitemize
|
|
With these queries, the \LStar{} algorithm can learn regular languages efficiently \citep[Angluin87].
|
|
In particular, it learns the unique minimal automaton for $\lang$ using only finitely many queries.
|
|
The \LStar{} algorithm has been generalised to \nLStar{} in order to learn \emph{nominal} regular languages.
|
|
In particular, it learns a nominal DFA (over an infinite alphabet) using only finitely many queries.
|
|
We implement \nLStar{} in the presented library and compare it to its previous implementation in \NLambda{}.
|
|
The algorithm is not polynomial, unlike the minimisation algorithm described above.
|
|
However, the authors conjecture that there is a polynomial algorithm.
|
|
\footnote{See \href{joshuamoerman.nl/papers/2017/17popl-learning-nominal-automata.html} for a sketch of the polynomial algorithm.}
|
|
\todo{\emph{The authors} ben ik...}
|
|
For the correctness, termination, and comparison with other learning algorithms see \in{Chapter}[chap:learning-nominal-automata].
|
|
|
|
|
|
\startsubsubject
|
|
[title={Implementations}]
|
|
|
|
Both implementations in \NLambda{} and \ONS{} are direct implementations of the pseudocode for \nLStar{} with no further optimisations.
|
|
The authors of \LOIS{} implemented \nLStar{} in their library as well.
|
|
\footnote{Can be found on \href{github.com/eryxcc/lois/blob/master/tests/learning.cpp}.}
|
|
They reported similar performance as the implementation in \NLambda{} (private communication).
|
|
Hence we focus our comparison on \NLambda{} and \ONS{}.
|
|
We use the variant of \nLStar{} where counterexamples are added as columns instead of prefixes.
|
|
|
|
The implementation in \NLambda{} has the benefit that it can work with different symmetries.
|
|
Indeed, the structured examples, FIFO and $ww$, are equivariant w.r.t. the equality symmetry as well as the total order symmetry.
|
|
For that reason, we run the \NLambda{} implementation using both the equality symmetry and the total order symmetry on those languages.
|
|
For the languages $\Lmax$, $\Lint$ and the random automata, we can only use the total order symmetry.
|
|
|
|
To run the \nLStar{} algorithm, we implement an external oracle for the membership queries.
|
|
This is akin to the application of learning black box systems (see \citenp[Vaandrager17]).
|
|
For equivalence queries, we constructed counterexamples by hand.
|
|
All implementations receive the same counterexamples.
|
|
We measure CPU time instead of real time, so that we do not account for the external oracle.
|
|
|
|
|
|
\stopsubsubject
|
|
\startsubsubject
|
|
[title={Results}]
|
|
|
|
The results (\in{Table}[learning_results]) for random automata show an advantage for \ONS{}.
|
|
Additionally, we report the number of membership queries,
|
|
which can vary for each implementation as some steps in the algorithm depend on the internal ordering of set data structures.
|
|
|
|
In contrast to the case of minimisation,
|
|
the results suggest that \NLambda{} cannot exploit the logical structure of FIFO$(n)$, $\Lmax$ and $\Lint$ as it is not provided a priori.
|
|
For $ww(2)$ we inspected the output on \NLambda{} and saw that it learned some logical structure (e.g., it outputs $\{ (a, b) \mid a \neq b \}$ as a single object instead of two orbits $\{ (a, b) \mid a < b \}$ and $\{ (a, b) \mid b < a \}$).
|
|
This may explain why \NLambda{} is still competitive.
|
|
For languages which are equivariant for the equality symmetry, the \NLambda{} implementation using the equality symmetry can learn with much fewer queries.
|
|
This is expected as the automata themselves have fewer orbits.
|
|
It is interesting to see that these languages can be learned more efficiently by choosing the right symmetry.
|
|
|
|
\startplacetable
|
|
[title={Running times and number of membership queries for the \nLStar{} algorithm.
|
|
For \NLambda{} we used two version: \NLambda{}$^{\mathit{ord}}$ uses the total order symmetry \NLambda{}$^{\mathit{eq}}$ uses the equality symmetry.
|
|
Timeouts are indicated by $\infty$.},
|
|
list={Running times for automata learning.},
|
|
reference=learning_results]
|
|
\starttabulate[|l|c|c|cg(.)|r|cg(.)|r|cg(.)|r|][distance=none]
|
|
\NC \NC \NC \VL \NC \ONS{} \VL \NC \NLambda{}$^{\mathit{ord}}$ \VL \NC \NLambda{}$^{\mathit{eq}}$ \NC\NR
|
|
\NC Model \NC $\Nsize(S)$ \NC $\dim(S)$ \VL time (s) \NC MQs \VL time (s) \NC MQs \VL time (s) \NC MQs \NC\NR
|
|
\HL
|
|
\NC rand$_{5,1}$ \NC 4 \NC 1 \VL 127 \NC 2321 \VL 2391 \NC 1243 \VL \NC \NC\NR
|
|
\NC rand$_{5,1}$ \NC 5 \NC 1 \VL 0.12 \NC 404 \VL 2434 \NC 435 \VL \NC \NC\NR
|
|
\NC rand$_{5,1}$ \NC 3 \NC 0 \VL 0.86 \NC 499 \VL 1819 \NC 422 \VL \NC \NC\NR
|
|
\NC rand$_{5,1}$ \NC 5 \NC 1 \VL $\infty$ \NC n/a \VL $\infty$ \NC n/a \VL \NC \NC\NR
|
|
\NC rand$_{5,1}$ \NC 4 \NC 1 \VL 0.08 \NC 387 \VL 2097 \NC 387 \VL \NC \NC\NR
|
|
\HL
|
|
\NC FIFO$(1)$ \NC 3 \NC 1 \VL 0.04 \NC 119 \VL 3.17 \NC 119 \VL 1.76 \NC 51 \NC\NR
|
|
\NC FIFO$(2)$ \NC 6 \NC 2 \VL 1.73 \NC 2655 \VL 392 \NC 3818 \VL 40.00 \NC 434 \NC\NR
|
|
\NC FIFO$(3)$ \NC 19 \NC 3 \VL 2794 \NC 298400 \VL $\infty$ \NC n/a \VL 2047 \NC 8151 \NC\NR
|
|
\HL
|
|
\NC $ww(1)$ \NC 4 \NC 1 \VL 0.42 \NC 134 \VL 2.49 \NC 77 \VL 1.47 \NC 30 \NC\NR
|
|
\NC $ww(2)$ \NC 8 \NC 2 \VL 266 \NC 3671 \VL 228 \NC 2140 \VL 30.58 \NC 237 \NC\NR
|
|
\NC $ww(3)$ \NC 24 \NC 3 \VL $\infty$ \NC n/a \VL $\infty$ \NC n/a \VL $\infty$ \NC n/a \NC\NR
|
|
\HL
|
|
\NC $\Lmax$ \NC 3 \NC 1 \VL 0.01 \NC 54 \VL 3.58 \NC 54 \VL \NC \NC\NR
|
|
\NC $\Lint$ \NC 5 \NC 2 \VL 0.59 \NC 478 \VL 83 \NC 478 \VL \NC \NC\NR
|
|
\stoptabulate
|
|
\stopplacetable
|
|
|
|
|
|
\stopsubsubject
|
|
\stopsubsection
|
|
\stopsection
|
|
\startsection
|
|
[title={Related work},
|
|
reference=sec:related]
|
|
|
|
As stated in the introduction, \NLambda{} by \citet[KlinS16] and \LOIS{} by \citet[KopczynskiT16] use first-order formulas to represent nominal sets and use SMT solvers to manipulate them.
|
|
This makes both libraries very flexible and they indeed implement the equality symmetry as well as the total order symmetry.
|
|
As their representation is not unique, the efficiency depends on how the logical formulas are constructed.
|
|
As such, they do not provide complexity results.
|
|
In contrast, our direct representation allows for complexity results (\in{Section}[sec:impl]) and leads to different performance characteristics (\in{Section}[sec:appl]).
|
|
|
|
A second big difference is that both \NLambda{} and \LOIS{} implement a \quotation{programming paradigm} instead of just a library.
|
|
This means that they overload natural programming constructs in their host languages (\haskell{} and \cpp{} respectively).
|
|
For programmers this means they can think of infinite sets without having to know about nominal sets.
|
|
|
|
It is worth mentioning that an older (unreleased) version of \NLambda{} implemented nominal sets with orbits instead of SMT solvers \citep[BojanczykBKL12].
|
|
However, instead of characterising orbits (e.g., by its dimension), they represent orbits by a representative element.
|
|
\citet[KlinS16] reported that the current version is faster.
|
|
|
|
The theoretical foundation of our work is the main representation theorem by \citet[BojanczykKL14].
|
|
We improve on that by instantiating it to the total order symmetry and distil a concrete representation of nominal sets.
|
|
As far as we know, we provide the first implementation of their representation theory.
|
|
|
|
Another tool using nominal sets is Mihda by \citet[FerrariMT05].
|
|
Here, only the equality symmetry is implemented.
|
|
This tool implements a translation from $\pi$-calculus to history-dependent automata (HD-automata) with the aim of minimisation and checking bisimilarity.
|
|
The implementation in OCaml is based on \emph{named sets}, which are finite representations for nominal sets.
|
|
The theory of named sets is well-studied and has been used to model various behavioural models with local names.
|
|
For those results, the categorical equivalences between named sets, nominal sets and a certain (pre)sheaf category have been exploited \citep[CianciaKM10, CianciaM10].
|
|
The total order symmetry is not mentioned in their work.
|
|
We do, however, believe that similar equivalences between categories can be stated.
|
|
Interestingly, the product of named sets is similar to our representation of products of nominal sets: pairs of elements together with data which denotes the relation between data values.
|
|
|
|
Fresh OCaml by \citet[ShinwellP05] and Nominal Isabelle by \citet[UrbanT05] are
|
|
both specialised in name-binding and $\alpha$-conversion used in proof systems.
|
|
They only use the equality symmetry and do not provide a library for manipulating nominal sets.
|
|
Hence they are not suited for our applications.
|
|
|
|
On the theoretical side, there are many complexity results for register automata \citep[GrigoreT16, MurawskiRT15].
|
|
In particular, we note that problems such as emptiness and equivalence are NP-hard depending on the type of register automaton.
|
|
This does not easily compare to our complexity results for minimisation.
|
|
One difference is that we use the total order symmetry, where the local symmetries are always trivial (\in{Lemma}[group_trivial]).
|
|
As a consequence, all the complexity required to deal with groups vanishes.
|
|
Rather, the complexity is transferred to the input of our algorithms, because automata over the equality symmetry require more orbits when expressed over the total order symmetry.
|
|
Another difference is that register automata allow for duplicate values in the registers.
|
|
In nominal automata, such configurations will be encoded in different orbits.
|
|
\todo{Equivalentie is polynomiaal: \cite[MurawskiRT18].}
|
|
|
|
Orthogonal to nominal automata, there is the notion of symbolic automata \citep[DAntoniV17, MalerM17].
|
|
These automata are also defined over infinite alphabets but they use predicates on transitions, instead of relying on symmetries.
|
|
Symbolic automata are finite state (as opposed to infinite state nominal automata) and do not allow for storing values.
|
|
However, they do allow for general predicates over an infinite alphabet, including comparison to constants.
|
|
|
|
|
|
\stopsection
|
|
\startsection
|
|
[title={Conclusion and Future Work},
|
|
reference=sec:fw]
|
|
|
|
We presented a concrete finite representation for nominal sets over the total order symmetry.
|
|
This allowed us to implement a library, \ONS{}, and provide complexity bounds for common operations.
|
|
The experimental comparison of \ONS{} against existing solutions for automata minimisation and
|
|
learning show that our implementation is much faster in many instances.
|
|
As such, we believe \ONS{} is a promising implementation of nominal techniques.
|
|
|
|
A natural direction for future work is to consider other symmetries, such as the equality symmetry.
|
|
Here, we may take inspiration from existing tools such as Mihda (see \in{Section}[sec:related]).
|
|
Another interesting question is whether it is possible to translate a nominal automaton over the total order symmetry which accepts an equality language to an automaton over the equality symmetry.
|
|
This would allow one to efficiently move between symmetries.
|
|
Finally, our techniques can potentially be applied to timed automata by exploiting the intriguing connection between the nominal automata that we consider and timed automata \citep[BojanczykL12].
|
|
|
|
|
|
\stopsection
|
|
\startsubject
|
|
[title={Acknowledgement}]
|
|
|
|
We would like to thank Szymon Toru\'{n}czyk and Eryk Kopczy\'{n}ski for their prompt help when using the \LOIS{} library.
|
|
For general comments and suggestions we would like to thank Ugo Montanari and Niels van der Weide.
|
|
At last, we want to thank the anonymous reviewers for their comments.
|
|
|
|
\stopsubject
|
|
\referencesifcomponent
|
|
\stopchapter
|
|
\stopcomponent
|