\documentclass[leqno,a4paper,twoside]{article}

\usepackage{amssymb,amsmath,amsthm}
\usepackage{algorithm,algorithmic}
\usepackage{subfigure,rotating}
\usepackage{times}
\usepackage{textcomp}
\usepackage{stmaryrd}
\usepackage{url}
\usepackage{tikz}
\usepackage{xspace}
\usepackage{graphicx}
\graphicspath{{./plots/}}
\usetikzlibrary{automata}

% For the techreport:
\setlength\oddsidemargin{0.78in}
\setlength\evensidemargin{\oddsidemargin}
\usepackage{fancyhdr}
\fancypagestyle{techreport}{\fancyhf{}%
\fancyhead[LE,RO]{\thepage}%
\fancyhead[LO]{Five Determinisation Algorithms}%
\fancyhead[RE]{Rob van Glabbeek \& Bas Ploeger}%
}
\pagestyle{techreport}
% End for the techreport

\title{Five Determinisation Algorithms}

\newcommand{\aff}[1]{\small{#1}}
\newcommand{\eml}[1]{\normalsize{\sf #1}}

\author{
Rob van Glabbeek\makebox[0pt][l]{$^{1,2}$}\\
\eml{rvg@cs.stanford.edu}
\and
Bas Ploeger\makebox[0pt][l]{$^3$\thanks{This author is partially supported by the
Netherlands Organisation for Scientific Research (NWO) under VoLTS grant
number 612.065.410.}}\\
\eml{s.c.w.ploeger@tue.nl}
\and 
\aff{$^1$ National ICT Australia, Locked Bag 6016, Sydney, NSW1466,
Australia}\\[2mm]
\aff{$^2$ School of Computer Science and Engineering, The University of
New South Wales}\\[-2pt]
\aff{Sydney, NSW 2052, Australia}\\[2mm]
\aff{$^3$ Department of Mathematics and Computer Science, Eindhoven University of Technology}\\[-2pt]
\aff{P.O.~Box~513, 5600~MB Eindhoven, The Netherlands}
}

\date{}

% theorem-like environments
\newtheorem{theorem}{Theorem}
\newtheorem{proposition}{Proposition}
\newtheorem{lemma}{Lemma}
\newtheorem{corollary}{Corollary}
\newtheorem{example}{Example}
\theoremstyle{definition}
\newtheorem{definition}{Definition}

% proof environment using less space			
\renewenvironment{proof}{\begin{trivlist} \item[\hspace{\labelsep}\it Proof.]}%
{\end{trivlist}}

% squeeze the tabular environment (less space between columns)
\setlength{\tabcolsep}{1.4pt}

% Latin abbreviations
\newcommand{\ie}{\textit{i.e.}\ }
\newcommand{\eg}{\textit{e.g.}\ }

% itemize using less space
\renewenvironment{itemize}{\begin{list}{$\bullet$}{\leftmargin 18pt
                        \labelwidth\leftmargini\advance\labelwidth-\labelsep
                        \topsep 4pt \itemsep 2pt \parsep 2pt}}{\end{list}}

% \in using less space (for correct implicite scoping)
\newcommand{\inp}{\mathbin\in}

% algorithmic redefs
\renewcommand{\algorithmicrequire}{\textbf{Pre:}}
\renewcommand{\algorithmicensure}{\textbf{Post:}}

% shorthands for fonts in math environments 
\newcommand{\mc}[1]{\ensuremath{\mathcal{#1}}}
\newcommand{\mr}[1]{\ensuremath{\mathrm{#1}}}
\newcommand{\ms}[1]{\ensuremath{\mathsf{#1}}}

\newfont{\fsc}{eusm10}      % frenchscript letters

% power set
\newcommand{\power}[1]{\mbox{\fsc P}(#1)}

% identity function
\newcommand{\idty}{\mc{I}}

% empty string
\newcommand{\emptystring}{\ensuremath{\varepsilon}}

% booleans
\newcommand{\BB}{\ensuremath{\mathbb{B}}}
\newcommand{\bimp}{\mathbin{\Leftrightarrow}}
\newcommand{\imp}{\mathbin{\Rightarrow}}

% a labelled transition with an NFA as subscript
\newcommand{\ltrans}[2]{\mathbin{\xrightarrow{#1}_{\!\mc{#2}}}}

% shorthands for NFA subscripting
\newcommand{\M}[1]{\ensuremath{#1_{\mc{M}}}}
\newcommand{\D}[1]{\ensuremath{#1_{\mc{D}}}}
\newcommand{\N}[1]{\ensuremath{#1_{\mc{N}}}}

% language and traces of a state in context of an NFA/LTS
\newcommand{\lang}[2]{\ensuremath{\mc{L}_{\mc{#1}}(#2)}}
\newcommand{\trac}[2]{\ensuremath{\ms{Tr}_{\mc{#1}}(#2)}}

% language preorder and equivalence
\newcommand{\lgeq}{\mathbin{\equiv_L}}
\newcommand{\lgin}{\mathbin{\sqsubseteq_L}}
\newcommand{\nlgin}{\mathbin{\not\sqsubseteq_L}}
\newcommand{\lgni}{\mathbin{\sqsupseteq_L}}

% trace preorder and equivalence
\newcommand{\treq}{\mathbin{\equiv_T}}
\newcommand{\trin}{\mathbin{\sqsubseteq_T}}
\newcommand{\ntrin}{\mathbin{\not\sqsubseteq_T}}

% simulation preorder and equivalence
\newcommand{\smin}{\stackrel{\raisebox{-3pt}{$\textstyle\subset\,$}}%
{\raisebox{-3pt}{$\scriptstyle\rightarrow$}}} % simulation inclusion

% small simulation inclusion for use in subscripts
\newcommand{\ssmin}{\stackrel{\raisebox{-3pt}{$\scriptstyle\subset\,$}}%
{\raisebox{-2pt}{$\scriptscriptstyle\rightarrow$}}}

\newcommand{\smeq}{\stackrel{\rightarrow}{\raisebox{0pt}[1pt][0pt]%
{$\scriptstyle \leftarrow$}}}			% simulation

% closure
\newcommand{\closure}[1]{\ensuremath{\ms{close}_{\mathord{#1}}}}
\newcommand{\closuref}[2]{\ensuremath{\closure{#1}(#2)}}
\newcommand{\compression}[1]{\ensuremath{\ms{compress}_{\mathord{#1}}}}
\newcommand{\compressionf}[2]{\ensuremath{\compression{#1}(#2)}}

% compression
\DeclareMathOperator{\comprop}{\downarrow\hspace{-0.15em}}
\newcommand{\compr}[1]{\ensuremath{\comprop #1}}

% transition tuple of a state
\newcommand{\trans}[1]{\ensuremath{\ms{trans}(#1)}}
\newcommand{\tuple}[1]{\ensuremath{\ms{tuple}(#1)}}

% compound state of a set of states
\newcommand{\comp}[1]{\ensuremath{#1_{\flat}}}

% name of an algorithm
\newcommand{\algo}[1]{\textsc{#1}}
\newcommand{\algof}[2]{\ensuremath{\algo{#1}(#2)}}

% Shorthands for various algorithms
\renewcommand{\Subset}{\algof{Subset}{\idty}\xspace}
\newcommand{\Subsetf}{\algof{Subset}{f}\xspace}
\newcommand{\SubsetClos}{\algof{Subset}{\closure{\lgin}\hspace{-1pt}}\xspace}
\newcommand{\SubsetClossim}{\algof{Subset}{\closure{\ssmin}\hspace{-1pt}}\xspace}
\newcommand{\SubsetCompsim}{\algof{Subset}{\compression{\ssmin}\hspace{-1pt}}\xspace}
\newcommand{\Transset}{\algof{Transset}{\idty}\xspace}
\newcommand{\Transsetf}{\algof{Transset}{f}\xspace}
\newcommand{\TranssetClossim}{\algof{Transset}{\closure{\ssmin}\hspace{-1pt}}\xspace}
\newcommand{\TranssetCompsim}{\algof{Transset}{\compression{\ssmin}\hspace{-1pt}}\xspace}

% no vertical space
\newcommand{\plat}[1]{\raisebox{0pt}[0pt][0pt]{$#1$}}

% redefine TiKZ style for a state to allow for smaller states
\tikzstyle{state}=[circle,draw,inner sep=2pt]

% comments
\definecolor{darkgreen}{rgb}{0,.6,0}
\newcommand{\Rob}[1]{{\color{darkgreen}#1}} % added or changed by Rob.
                                        % approve by omitting the \Rob environment

\newcommand{\Bas}[1]{{\color{red} #1}} % added or changed by Bas.
                                        % approve by omitting the \Bas environment

\begin{document}
\maketitle

\begin{abstract}

\noindent Determinisation of nondeterministic finite automata is a
well-studied problem that plays an important role in compiler theory
and system verification.  In the latter field, one often encounters
automata consisting of millions or even billions of states. On such
input, the memory usage of analysis tools becomes the major
bottleneck. In this paper we present several determinisation
algorithms, all variants of the well-known subset construction, that
aim to reduce memory usage and produce smaller output automata.  One
of them produces automata that are already minimal.  We apply our
algorithms to determinise automata that describe the possible
sequences appearing after a fixed-length run of cellular automaton
110, and obtain a significant improvement in both memory and time
efficiency.

\end{abstract}

\section{Introduction}

Finite state automata (or finite state machines) are an established and
well-studied model of computation.
From a theoretical point of view, they are an interesting object of
study because they are expressive yet conceptually easy to understand
and intuitive.
They find applications in compilers, natural language processing, system
verification and testing, but also in fields outside of (theoretical)
computer science like switching circuits and chip design.
Over the years, many flavours and variants of finite state machines have
been defined and studied for a large variety of purposes.

One of the most classic and elementary type of finite state machine is
the \emph{nondeterministic finite automaton} (NFA). Typical applications
of finite state automata involve checking whether some sequence of symbols meets
some syntactic criterion, such as displaying a prescribed pattern or
being correct input for a given program, a problem that can often be
recast as checking whether that sequence is accepted by a given NFA\@.

A more restrictive type of automaton is the \emph{deterministic finite
automaton} (DFA).  DFAs are as expressive as NFAs, in the sense that
for every NFA there exists a DFA that is \emph{language equivalent}
(\ie accepts the same input sequences). Contrary to NFAs, for any
DFA there
is a trivial linear time, constant space, online algorithm to check
\pagebreak[2]
whether an input sequence is accepted or not. Consequently,
lexical-analyser generators like \textsc{Lex} work on DFAs, and so do
many implementations of \textsc{grep}. For this reason, in many
applications it pays to convert NFAs into DFAs, even though the
worst-case time and space complexities of this conversion are
exponential in the size of the input NFA\@.

Once a language equivalent DFA of an NFA has been found, it is usually
minimised to obtain the smallest such DFA.  This minimal DFA is unique
and the problem of finding it for a given NFA is called the
\emph{canonisation problem}.

Another application of NFAs is in the realm of \emph{process theory}
and \emph{system verification} where they are used to model the
behaviour of distributed systems. Typically, both a specification and
an implementation of a system are represented as NFAs, and the
question arises whether the execution sequences of one NFA are a
subset of those of another. This is the \emph{trace inclusion
problem}. Although PSPACE-hard in general, this problem is decidable in
PTIME once the NFAs are converted into equivalent DFAs.

As we see, in both the canonisation problem and the trace inclusion
problem, determinisation plays an essential role.
The standard determinisation algorithm is called \emph{subset
construction} (see \eg \cite{HU:79}).
Although the determinisation problem is EXPTIME-hard, this algorithm
is renowned for its good performance in practice.
For DFA minimisation a lot of algorithms have been proposed, of
which Watson presents a taxonomy and performance analyses
\cite{Wat:95}.
The algorithm with the best time complexity is by Hopcroft
\cite{Hop:71}: $\mc{O}(n \log n)$ where $n$ is the number of states in
the input DFA.

Another algorithm for canonisation is by Brzozowski \cite{Brz:63}. It
generates the minimal DFA directly from an input NFA by repeating the
process of ``reversing'' and determinising the automaton twice.
Tabakov and Vardi compare both approaches to canonisation
experimentally by running them on randomly generated automata \cite{TV:05}.
They show that the ``subset-Hopcroft'' approach performs best overall
and for smaller transition densities, but for larger transition
densities Brzozowski's algorithm is faster.

On some NFAs, the exponential blow-up by subset construction is
unavoidable. However, we have encountered NFAs for which subset
construction consumes a lot of memory and generates a DFA that is much
larger than the minimal DFA.  Therefore, our main goal is to find
algorithms that are more memory efficient and produce smaller DFAs
than subset construction.

In this paper we present five determinisation algorithms based
on subset construction. For all of them we prove correctness.
One
algorithm generates the minimal DFA directly and hence is a
\emph{canonisation algorithm}. However, it calculates language
inclusion as a subroutine; as deciding language inclusion is
PSPACE-complete, it is unattractive to use in an implementation.
The other four produce a DFA that is not necessarily minimal but is
usually smaller than the DFA produced by subset construction.

We have implemented subset construction and these four new algorithms.
We have benchmarked these implementations by running them on NFAs that
describe patterns on the lines of a cellular automaton's evolution
and on randomly generated automata. We
compare the implementations on the time and memory needed for the
complete canonisation process (\ie including minimisation) and the size
of the DFA after determinisation. 

\section{Preliminaries} \label{sec:prelim}

\paragraph{Finite automata.}
A \emph{nondeterministic finite automaton} (NFA) \mc{N} is a tuple $(\N{S},$
$\N{\Sigma},$ $\N{\delta},$ $\N{i},$ $\N{F})$ where $\N{S}$ is a finite
set of states, $\N{\Sigma}$ is a finite input alphabet, $\N{\delta}
\subseteq \N{S} \times \N{\Sigma} \times \N{S}$ is a transition
relation, $\N{i} \in \N{S}$ is the initial state and $\N{F} \subseteq
\N{S}$ is a set of final (or accepting) states.
A \emph{deterministic finite automaton} (DFA) is an NFA \mc{D} such that for all
$p \!\in\! \D{S}$ and $a \!\in\! \D{\Sigma}$ there is precisely one $q \!\in\! \D{S}$ such
that $(p,a,q) \in \D{\delta}$.


In graphical representations of DFAs we also allow states that have
\emph{at most} one outgoing $a$-transition for each alphabet symbol $a$.
Formally speaking, these abbreviate the DFA obtained by adding a
non-accepting \emph{sink} state as the target of all missing
transitions.  Note that adding such a state preserves language
equivalence (defined below).

For any alphabet $\Sigma$, $\Sigma^*$ denotes the set of all finite strings over
$\Sigma$ and $\emptystring \in \Sigma^*$ denotes the empty string. Any subset of
$\Sigma^*$ is called a \emph{language over $\Sigma$}. For any states $p,q \in
\N{S}$ of an NFA \mc{N} and string $\sigma \in \N{\Sigma}^*$ with $\sigma =
\sigma_1 \cdots \sigma_n$ and $\sigma_1, \ldots, \sigma_n \in
\N{\Sigma}$ for some $n\geq 0$, we
write \plat{p \ltrans{\sigma}{N} q} to denote the fact that:\vspace{-1ex}
$$\exists p_0, \ldots, p_n \in \N{S} \,.\, p_0=p  \,\land\,
p_n = q \,\land\, (p_0,\sigma_1,p_1),
\ldots, (p_{n-1},\sigma_n,p_n) \in \N{\delta}.$$

\paragraph{Language semantics.}
The \emph{language of a state} $p \in \N{S}$ of an NFA \mc{N} is defined as:
$\lang{N}{p} = \{ \sigma \in \N{\Sigma}^* \mid \exists q \in \N{F} \,.\, p
\ltrans{\sigma}{N} q \}$.
The \emph{language of an NFA} \mc{N} is defined as: $\lang{}{\mc{N}} =
\lang{N}{\N{i}}$.
For any NFAs \mc{N} and \mc{M} and states $p\in \N{S}$ and $q\in \M{S}$,
$p$ is {\it language included} in $q$, denoted $p \lgin q$, iff
$\lang{N}{p} \subseteq \lang{M}{q}$.
Moreover, $p$ and $q$ are {\it language equivalent}, denoted $p \lgeq
q$, iff $p \lgin q \land q \lgin p$.
An NFA \mc{N} is {\it language included} in an NFA \mc{M} iff $\N{i}
\lgin \M{i}$ and \mc{N} and \mc{M} are {\it language equivalent} iff
$\N{i} \lgeq \M{i}$.

\paragraph{Simulation semantics.}
Given NFAs \mc{N} and \mc{M}, a relation $R \subseteq \N{S} \times
\M{S}$ is a \emph{simulation} iff for any $p\in \N{S}$ and $q\in \M{S}$,
$p \mathrel{R} q$ implies:
\begin{itemize}
  \item $p\in \N{F} \imp q \in \M{F}$ and
  \item $\forall a\in \N{\Sigma} \,.\, \forall p' \in \N{S} \,.\, p \ltrans{a}{N} p' \;\imp\;
    \exists q' \in \M{S} \,.\, q \ltrans{a}{M} q' \,\land\, p' \mathrel{R} q'$.
\end{itemize}
Given NFAs \mc{N} and \mc{M}, for any $p\in \N{S}$ and $q\in \M{S}$:
\begin{itemize}
  \item $p$ is {\it simulated by} $q$, denoted $p \smin q$, iff there exists a
    simulation $R$ such that $p\mathrel{R}q$;
  \item $p$ and $q$ are \emph{simulation equivalent}, denoted $p \smeq q$, iff
    $p \smin q \land q \smin p$;
\end{itemize}

\noindent Clearly $p \smin q$ implies $p \lgin q$.

\paragraph{Subset construction.}
The subset construction (or powerset construction) is the standard way
of determinising a given NFA.
For reasons that will become apparent in the next sections, we slightly
generalise the normal algorithm by augmenting it with a function $f$ on
sets of states of the input NFA, which is applied to every generated set.
The algorithm is Algorithm~\ref{alg:subset} and shall be referred to as
\Subsetf.
It takes an NFA $\mc{N}$ and generates a DFA $\mc{D}$.
Of course, it should be the case that $\mc{N} \lgeq \mc{D}$, which
depends strongly on the function $f$.
For normal subset construction, \Subset, where
  $\idty$ is the identity function, it is known that
the language of $\mc{N}$ is indeed preserved.
In Appendix~\ref{app:Subset} we show that the same holds for
\Subsetf, for any function $f$ that satisfies $f(P)\lgeq P$ for
every set of states $P\subseteq\N{S}$.
In the sequel, whenever we use the term ``subset construction'' we mean
the normal algorithm, \ie \Subset.

It is known that in the worst case, determinisation yields a DFA that
is exponentially larger than the input NFA. An example of an NFA that gives rise
to such an exponential blow-up is the NFA that accepts the language specified by
the regular expression $\Sigma^* x \Sigma^n$ for some alphabet $\Sigma$, $x \in
\Sigma$ and $n \geq 0$. Figure~\ref{fig:expblowup} shows
the NFA for $\Sigma = \{a,b\}$ and $x=a$. This NFA has $n+2$ states,
whereas the corresponding DFA has $2^{n+1}$ states and is already
minimal. 

An interesting thing to note is that if the initial state were accepting
(Figure~\ref{fig:expgap}), the minimal DFA would consist of only one
state with an $a,b$-loop: the accepted language has become $\Sigma^*$.
However, subset construction still produces the exponentially larger DFA
first, which should then be reduced to obtain the single-state, minimal
DFA\@.


\begin{algorithm}[t]
\begin{algorithmic}[1]
\REQUIRE $\mc{N}=(\N{S},\N{\Sigma},\N{\delta},\N{i},\N{F})$ is an NFA
\ENSURE $\mc{D}=(\D{S},\D{\Sigma},\D{\delta},\D{i},\D{F})$ is a DFA
\\
\STATE $\D{\Sigma} := \N{\Sigma}$; $\D{\delta} := \emptyset$; $\D{i} :=
f(\{\N{i}\})$; $\D{F} := \emptyset$;
\STATE $\D{S} := \{ \D{i} \}$; $\mr{todo} := \{ \D{i}
\}$; $\mr{done} := \emptyset$;
\WHILE {$\mr{todo} \neq \emptyset$}
\STATE pick a $P \in \mr{todo}$;
\FORALL {$a \in \N{\Sigma}$}
\STATE $P' := f(\{ p' \in \N{S} \mid \exists p \in P \,.\, p \ltrans{a}{N}
p' \})$;
\label{line:main1}
\STATE $\D{S} := \D{S} \cup \{P'\}$;
\STATE $\D{\delta} := \D{\delta} \cup \{(P,a,P')\}$;
\label{line:main2}
\STATE $\mr{todo} := \mr{todo} \cup ( \{P'\} \setminus \mr{done} )$;
\ENDFOR
\IF {$\exists p \inp P \,.\; p \inp \N{F}$}
\STATE $\D{F} := \D{F} \cup \{P\}$;
\label{line:accepting}
\ENDIF
\STATE $\mr{todo} := \mr{todo} \setminus \{ P \}$;
\STATE $\mr{done} := \mr{done} \cup \{ P \}$;
\ENDWHILE
\end{algorithmic}
\caption{The \Subsetf determinisation algorithm} \label{alg:subset}
\end{algorithm}


\begin{algorithm}[t]
	\begin{algorithmic}[1]
		\REQUIRE $\mc{N}=(\N{S},\N{\Sigma},\N{\delta},\N{i},\N{F})$ is an NFA
    \ENSURE $\mc{D}=(\D{S},\D{\Sigma},\D{\delta},\D{i},\D{F})$ is a DFA 
		\\
    \STATE $\D{\Sigma} := \N{\Sigma}$; $\D{\delta} := \emptyset$; $\D{i}
    :=
    f(\tuple{\N{i}})$; $\D{F} := \emptyset$;
		\STATE $\D{S} := \{ \D{i} \}$; $\mr{todo} := \{ \D{i} \}$;
    $\mr{done} :=
		\emptyset$;
		\WHILE {$\mr{todo} \neq \emptyset$}
		\STATE pick a $P \in \mr{todo}$;
		\FORALL {$a \in \Sigma$}
		\STATE $\plat{P' := f(\; \bigcup_{(a,p) \in \ms{set}(P)}
    \trans{p},\; \exists (a,p) \in \ms{set}(P) \,.\, p \in \N{F} \;)}$;
    \label{line:trans-main1}
		\STATE $\D{S} := \D{S} \cup \{P'\}$;
    \label{line:trans-main1b}
		\STATE $\D{\delta} := \D{\delta} \cup \{(P,a,P')\}$;
    \label{line:trans-main2}
		\STATE $\mr{todo} := \mr{todo} \cup ( \{P'\} \setminus \mr{done} )$;
		\ENDFOR
    \IF {$\ms{fin}(P)$}
    \label{line:trans-fin1}
		\STATE $\D{F} := \D{F} \cup \{P\}$;
		\ENDIF
    \label{line:trans-fin2}
		\STATE $\mr{todo} := \mr{todo} \setminus \{ P \}$;
		\STATE $\mr{done} := \mr{done} \cup \{ P \}$;
		\ENDWHILE
	\end{algorithmic}
  \caption{The \Transsetf determinisation algorithm}\label{alg:transset}
\end{algorithm}

\section{Determinisation using Transition Sets} \label{sec:transset}

In this section we show that subset construction can just as well be done on
sets of transitions as on sets of states.
We observe that the contribution of an NFA state $p$ to the behaviour of
a DFA state $P$ consists entirely of $p$'s outgoing
transitions. We no longer think of a DFA state as being a set of NFA
states, but rather a set of NFA \emph{transitions}.

\begin{figure}[bhtp]
\vspace*{-.8em}
\centering
\subfigure[]{
\label{fig:expblowup}
\begin{tikzpicture}[node distance=1.3cm,auto,>=stealth]
  \node[state,initial,initial text=] (0) {$p_0$};
  \node[state] (1) [right of=0] {$p_1$};
  \node (dots) [right of=1] {$\cdots$};
  \node[state] (n) [right of=dots] {$p_n$};
  \node[state,accepting] (np1) [right of=n] {$p_{n+1}$};
  \path[->] (0) edge [loop above] node {$a,b$} ()
                edge node {$a$} (1)
            (1) edge node {$a,b$} (dots)
            (dots) edge node {$a,b$} (n)
            (n) edge node {$a,b$} (np1);
\end{tikzpicture}}
\vspace*{-.4em}
\subfigure[]{
\label{fig:expgap}
\begin{tikzpicture}[node distance=1.3cm,auto,>=stealth]
  \node[state,initial,initial text=,accepting] (0) {$q_0$};
  \node[state] (1) [right of=0] {$q_1$};
  \node (dots) [right of=1] {$\cdots$};
  \node[state] (n) [right of=dots] {$q_n$};
  \node[state,accepting] (np1) [right of=n] {$q_{n+1}$};
  \path[->] (0) edge [loop above] node {$a,b$} ()
                edge node {$a$} (1)
            (1) edge node {$a,b$} (dots)
            (dots) edge node {$a,b$} (n)
            (n) edge node {$a,b$} (np1);
\end{tikzpicture}}
\caption{Two NFAs of size $\mc{O}(n)$ for which subset construction
produces a DFA of size $\mc{O}(2^n)$. Here initial states are
marked by unlabelled incoming arrows, and final states by double
circles. In case (a) this DFA is already minimal; in case (b) the
minimal DFA has size 1.}
\end{figure}

\begin{definition}\rm
  Given an NFA \mc{N}, a \emph{transition tuple} is a pair $(T,b)$ where $T \in
  \power{\N{\Sigma} \times \N{S}}$ is a set of transitions and $b \in \BB$ is a
  boolean.
\end{definition}

\noindent
For every transition tuple $(T,b)$ we define the projection functions
\ms{set} and \ms{fin} as: $\ms{set}(T,b) = T$ and $\ms{fin}(T,b) = b$.
For every state $p\!\in\! \N{S}$ of NFA $\mc{N}$, $\trans{p}$ is the
set of outgoing transitions of $p$ and $\tuple{p}$ is the
transition tuple belonging to $p$: 
\[
\begin{array}{ll}
\trans{p} & = \{ (a,q) \in \N{\Sigma} \times \N{S}\, \mid\, p
\ltrans{a}{N} q \}\\
\tuple{p} & = (\trans{p}, p \in \N{F}).
\end{array}
\]

\noindent
The DFA state $P \subseteq \N{S}$ now corresponds to the transition
tuple $(T,b)$ where $T = \bigcup_{p\in P} \trans{p}$ and $b \equiv
\exists p \!\in\! P \,.\; p \!\in\! \N{F}$. We need the boolean $b$ to indicate
whether the DFA state is final as this can no longer be determined from
the elements of the set. Only the labels and target states of
the transitions are stored because the source states are irrelevant and
would only make the sets unnecessarily large.

Given NFA \mc{N}, the \emph{language of a transition} $(a,p) \inp
\N{\Sigma} \times \N{S}$ is defined
as: $\lang{N}{a,p} = \{ a \sigma \inp \N{\Sigma}^*\, \mid\, \sigma \inp
\lang{N}{p} \}$.
The \emph{language of a set of transitions} $T$ is defined as $\lang{N}{T} =
\bigcup_{t\inp T} \lang{N}{t}$ and the \emph{language of a transition
tuple} $(T,b)$ is defined as:
\[
\lang{N}{T,b} = \lang{N}{T}\ \cup\ \left\{
\begin{array}{ll}
  \{\emptystring\} & \mbox{if $\phantom\neg b$}\\ 
  \emptyset & \mbox{if $\neg b$.}
\end{array} \right.
\]
Language inclusion and equivalence for transitions and transition
tuples can now be defined in the usual way by means of set inclusion and
equality.

The determinisation algorithm that uses transition tuples is
Algorithm~\ref{alg:transset}. We shall refer to it as
\Transsetf where $f$ is a function on transition tuples. 
Again, language preservation depends on the specific function $f$ being
used. For $f = \idty$ --- and more generally when $f$ satisfies
  $f(P)\lgeq P$ for each transition tuple $P$ --- this is indeed the
case, which we prove in Appendix~\ref{app:Transsetf}.
Using \Transset for determinisation can give a smaller DFA than
\Subset as is shown by the example in Figure~\ref{fig:dettrans}. Here,
\Transset happens to produce the minimal DFA directly.
This is generally not the case: on the NFA of Figure~\ref{fig:expgap}, \Transset
generates a DFA of size $2^{n+1}$, while the minimal DFA has size 1.

\begin{figure}[t]
\centering
\subfigure[]{
\centering
\begin{tikzpicture}[node distance=1.2cm,auto,>=stealth]
  \node[state,initial above,initial text=] (0) {$p_0$};
  \node[state] (2) [below of=0] {$p_2$};
  \node[state] (1) [left of=2] {$p_1$};
  \node[state] (3) [right of=2] {$p_3$};
  \node[state,accepting] (4) [below of=2] {$p_4$};
  \path[->]
  (0)	edge node [swap] {$a$} (1)
      edge node {$b$} (2)
      edge node {$b$} (3)
  (1)	edge node [swap] {$a,b$} (4)
  (2)	edge node {$a$} (4)
  (3)	edge node {$b$} (4);
\end{tikzpicture}}
\hspace{10mm}
\subfigure[]{
\centering
\begin{tikzpicture}[node distance=1.2cm,auto,>=stealth]
  \node[state,initial above,initial text=] (0) {$q_0$};
  \node[state] (2) [below right of=0] {$q_2$};
  \node[state] (1) [below left of=0] {$q_1$};
  \node[state,accepting] (3) [below left of=2] {$q_3$};
  \path[->]
  (0)	edge node [swap] {$a$} (1)
      edge node {$b$} (2)
  (1)	edge node [swap] {$a,b$} (3)
  (2)	edge node {$a,b$} (3);
\end{tikzpicture}}
\hspace{10mm}
\subfigure[]{
\centering
\begin{tikzpicture}[node distance=1.2cm,auto,>=stealth]
  \node[state,initial above,initial text=] (0) {$r_0$};
  \node[state] (1) [below of=0] {$r_1$};
  \node[state,accepting] (2) [below of=1] {$r_2$};
  \path[->]
  (0)	edge node {$a,b$} (1)
  (1)	edge node {$a,b$} (2);
\end{tikzpicture}}
\caption{NFA (a) for which the DFA produced by \Subset (b) is larger than
the (minimal) DFA produced by \Transset (c).}\label{fig:dettrans}
\end{figure}

\section{Determinisation using Closures}\label{sec:closure}

We introduce a \emph{closure} operation that can be used in the
\algo{Subset} algorithm instead of the identity function $\idty$.
It aims to add NFA states to a given DFA state (\ie a set of NFA states)
without affecting its language.
This results in an algorithm that generates smaller DFAs.
In particular, we show that if the criterion to add a state is chosen
suitably, \algo{Subset} with closure is an algorithm that
produces the minimal DFA directly.

\begin{definition}\label{def:closure}\rm
For any set of states $P \subseteq \N{S}$ of an NFA \mc{N} and relation
$\mathord\sqsubseteq \subseteq \N{S} \times \power{\N{S}}$, 
the \emph{closure} of $P$ under
$\sqsubseteq$, $\closuref{\sqsubseteq}{P}$, is defined as:
$$\closuref{\sqsubseteq}{P} = \{ p \in \N{S} \mid p \sqsubseteq P \}.$$
\end{definition}

\noindent
The language preorder $\lgin$ can be lifted to operate on states and
sets of states in the following way.
Define the \emph{language of a set of states} $P$ of an NFA \mc{N} as:
$\lang{N}{P} = \bigcup_{p \in P} \lang{N}{p}$.
Language equivalence and inclusion can now be defined on any combination
of states and sets of states, in terms of set equivalence and
inclusion.
For instance, for a state $p \in \N{S}$ and a set of states $P \subseteq
\N{S}$ , $p \lgin P$ holds if $\lang{N}{p} \subseteq \lang{N}{P}$.

Applying this, the algorithm \SubsetClos generates the minimal DFA that
is language equivalent to the input NFA.
This statement is proven in Appendix~\ref{app:Subsetclos}.

\section{Simulation Preorder}\label{sec:simul}

Although it ensures that the output DFA of
\SubsetClos is minimal, language inclusion is an
unattractive preorder to use.
Deciding language inclusion is PSPACE-complete \cite{SM:73} which
implies that known algorithms have an exponential time complexity.
Moreover, most algorithms involve a determinisation step
which would render our optimisation useless.

The simulation preorder $\smin$ \cite{Par:81} is finer than language
inclusion on NFAs, meaning it relates fewer NFAs.
However, considering its PTIME complexity (see \eg
\cite{BP:95,HHK:95}), it is an attractive way to
``approximate'' language inclusion (see also \cite{DHT:92}).
Hence, as a more practical alternative to \SubsetClos we define the
algorithm \SubsetClossim.
The required lifting of $\smin$ to states and sets of states is
as follows.
For any state $p \in \N{S}$ and set of states $P \subseteq \N{S}$ of an
NFA \mc{N}, we have $p \smin P$ iff:
\begin{itemize}
  \item $p \inp \N{F} \imp \exists q \inp P \,.\; q \inp \N{F}$ and
  \item there exists a simulation $R \subseteq \N{S} \times \N{S}$
  such that:
  \item[] $\forall a\inp \N{\Sigma} \,.\, \forall p' \in \N{S} \,.\; p
    \ltrans{a}{N} p' \;\imp\; \exists q,q' \inp \N{S} \,.\; q \inp P \land
    q \ltrans{a}{N} q' \,\land\, p' \mathrel{R} q'$.
\end{itemize}

\noindent
The correctness of \SubsetClossim is established in Appendix~\ref{app:Subsetclossim}.
The example in Figure~\ref{fig:simexpgap} shows not only that the
resulting DFA is no longer minimal, but moreover that it can be
exponentially larger than the minimal DFA. This NFA contains a pattern
that repeats itself $n$ times for any $n \geq 1$. It is based on the NFA of
Figure~\ref{fig:expgap} interwoven with a pattern that prevents
\SubsetClossim from merging states that will later turn out to be
equivalent. The NFA accepts the language
given by the regular expression \plat{(a \mid b)^*}.

\begin{figure}[t]
\centering
\begin{tikzpicture}[node distance=1.3cm,auto,>=stealth]
  \tikzstyle{ptrn}=[color=red]
  \node[state,initial,initial text=,accepting] (p0) {$p_0$};
  \node[state,accepting] (p2) [below of=p0] {$p_2$};
  \node[state,accepting] (p1) [above of=p0] {$p_1$};
  \node[state] (p3) [right of=p0] {$p_3$};
  \node[state] (p4) [right of=p3] {$p_4$};
  \node[state,ptrn] (p11) [above right of=p4] {$p_{1,1}$};
  \node[state,ptrn] (p12) [below right of=p4] {$p_{1,2}$};
  \node[state,ptrn] (p13) [below right of=p11] {$p_{1,3}$};
  \node[ptrn] (dots) [right of=p13,xshift=-0.1cm] {$\cdots$};
  \node (pnm15) [right of=dots,xshift=-0.6cm] {$\phantom {p_{x,y}}$};
  \node[state,ptrn] (pn1) [above right of=pnm15] {$p_{n,1}$};
  \node[state,ptrn] (pn2) [below right of=pnm15] {$p_{n,2}$};
  \node[state,ptrn] (pn3) [below right of=pn1] {$p_{n,3}$};
  \node[state] (p5) [right of=pn3] {$p_{5}$};
  \node[state,accepting] (p6) [right of=p5] {$p_{6}$};
  \path[->]
  (p0)  edge [bend left] node {$a,b$} (p1)
        edge [bend right,swap] node {$a,b$} (p2)
        edge node {$a$} (p3)
  (p1)  edge [bend left] node {$a$} (p0)
  (p2)  edge [bend right,swap] node {$b$} (p0)
  (p3)  edge node {$a$} (p4)
  (p4)  edge [ptrn] node {$a,b$} (p11)
        edge [ptrn,swap] node {$a,b$} (p12)
  (p11) edge [ptrn] node {$a$} (p13)
  (p12) edge [ptrn,swap] node {$b$} (p13)
  (pnm15) edge [ptrn] node {$a,b$} (pn1)
        edge [ptrn,swap] node {$a,b$} (pn2)
  (pn1) edge [ptrn] node {$a$} (pn3)
  (pn2) edge [ptrn,swap] node {$b$} (pn3)
  (pn3) edge node {$a,b$} (p5)
  (p5) edge node {$a,b$} (p6);
\end{tikzpicture}
\caption{NFA of size $\mc{O}(n)$ for which
$\algof{Subset}{\closure{\protect\ssmin}}$ generates a DFA of size $\mc{O}(2^n)$
for any $n\geq 1$. The minimal DFA has 1 state.}
\label{fig:simexpgap}
\end{figure}

\section{Determinisation using Compressions}\label{sec:compressions}

Algorithm \SubsetClossim adds all simulated states to a generated set of
states.
Another option would be to remove all redundant states from such a set.
More specifically, we remove every state that is simulated by another
state in the set.
For this operation to be well-defined, it is essential that no two
different states in the set are simulation equivalent.
This can be achieved by minimising the input NFA using simulation
equivalence prior to determinisation. In turn, this amounts to
computing the simulation preorder that was already necessary in the
first place.

\begin{definition}\label{def:compr}\rm
Given a set $P$ such that $\neg \exists p,q \in P \,.\, p \neq q \land p
\smeq q$. Then
$\compressionf{\ssmin}{P}$ denotes the \emph{compression} of $P$
under $\smin$ and is defined as:
\[
\compressionf{\ssmin}{P} = \{ p \in P \mid \forall q \in P \,.\, p
\neq q \imp p \not\smin q \}.
\]
\end{definition}

\noindent
The function $\compression{\ssmin}$ can be used not only for sets of
states but also for transition tuples. For that, we
first define $\smin$ on the transitions of an NFA \mc{N} as follows. For any
$(a,p), (b,q) \in \N{\Sigma} \times \N{S}$, we have $(a,p) \smin (b,q)$
iff $a = b$ and $p \smin q$.
By Definition~\ref{def:compr} $\compression{\ssmin}$ is now properly
defined on sets of transitions and 
it can be extended to transition tuples in a straightforward manner:
$\compressionf{\ssmin}{T,b} = (\compressionf{\ssmin}{T},b)$.

This way, we obtain two more determinisation algorithms:
\plat{\SubsetCompsim} and \TranssetCompsim.
Their correctness proofs are included in
Appendices~\ref{app:Subsetcompsim} and~\ref{app:Transsetcompsim},
respectively.

\section{Lattice of Algorithms}

We order the algorithms described in the previous sections in a
lattice. The ordering $\preceq$ on the algorithms is as follows: $A \preceq B$
iff for every input NFA, $A$ produces a DFA that is at most as large
as the one produced by $B$. The lattice is depicted in
Figure~\ref{fig:alglattice} where an arrow from $A$ to $B$ denotes that
$A \preceq B$.

\begin{figure}
\centering
\begin{tikzpicture}[>=stealth]
  \node (s)     at (0,4) {\Subset};
  \node (t)     at (1.5,3) {\Transset};
  \node (cpsim) at (-1.5,3) {\SubsetCompsim};
  \node (cpclsim) at (0,2) {\SubsetClossim, \TranssetCompsim};
  \node (cl)    at (0,1) {\SubsetClos};
  \path[->]
    (cl) edge (cpclsim)
    (cpclsim) edge (t)
              edge (cpsim)
    (t) edge (s)
    (cpsim) edge (s);
\end{tikzpicture}
\caption{The lattice of algorithms presented in the previous sections.}
\label{fig:alglattice}
\end{figure}

\SubsetClossim and \TranssetCompsim are in the same class of the
lattice, because these algorithms always yield isomorphic DFAs.
This statement is substantiated in Appendix~\ref{app-lattice}, as well
as the validity of the other $\preceq$-relations of Figure~\ref{fig:alglattice}.
The following shows that the lattice is complete, in the sense that
there are no further $\preceq$-relations between our algorithms:
\begin{itemize}
  \item \SubsetClos is the unique $\preceq$-smallest algorithm because it
    is the only one that always generates the minimal DFA;
  \item $\SubsetCompsim \not\preceq \Transset$ by the example in
    Figure~\ref{fig:dettrans};
  \item $\Transset \not\preceq \SubsetCompsim$ 
    by the example in Figure~\ref{fig:expgap}.
\end{itemize}

\section{Implementation and Benchmarks}\label{sec:impl_bench}

We have implemented the algorithms \Subset,
\Transset, \SubsetClossim, \plat{\SubsetCompsim}
and \plat{\TranssetCompsim} in the C++ programming language. A set of
states or transitions is stored as a tree with the elements in the
leaves. All subtrees are shared among the sets to improve memory
efficiency. A hash table provides fast and efficient lookup of existing
subtrees.

The benchmarks are performed on a 32-bits architecture computer having
two Intel Xeon 3.06~GHz CPUs and 4~GB of RAM.
It runs Fedora Core~8 Linux, kernel~2.6.23.
The code is compiled using the GNU C++ compiler (version~4.1.2).

Every benchmark starts off by minimising the NFA using simulation
equivalence. For this we have implemented our partitioning algorithm
\cite{GP:08} which is based on \cite{GPP:03} and
also computes the simulation preorder on the states of the
resulting NFA. Every determinisation algorithm is applied to this
minimised NFA, after which the resulting DFA is minimised
by the tool \textsf{ltsmin} of the
{\textmu}CRL toolset \cite{mCRLWeb,GR:01} (version 2.18.1).

\subsection{Cellular Automaton 110}

\begin{figure}
  \centering
  \subfigure[Rule 110]{\label{fig:ca-example-rule}
  \includegraphics{r110}
  }\\
  \subfigure[Evolution]{\label{fig:ca-example-evol}
  \includegraphics[scale=0.6]{r110-100x50}}
  \caption{Example of a cellular automaton (rule 110).}
  \label{fig:ca-example}
\end{figure}

In his book \cite{Wol:02}, Wolfram studies cellular automata as a model of
computation. A \emph{cellular automaton} consists of a line of white or black
cells\footnote{Actually, a wide variety of cellular automata can be defined. We
consider a basic type here with two colours and a ``neighbourhood'' of 1.
} of
which the colours are changed in every step of the automaton. The colour of a
cell in the next step of the automaton's computation depends on its current
colour and those of its left- and right-hand neighbours, as specified by a
so-called \emph{rule}. An example is given in Figure~\ref{fig:ca-example}. The
rule is depicted in Figure~\ref{fig:ca-example-rule}. For example, it specifies
that if a cell is black and both of its neighbours are black, then that cell
becomes white in the next step of the automaton's evolution (cf.\ the leftmost
part of the rule).

From Figure~\ref{fig:ca-example-rule}, it is easy to see that there are 256 such
rules. The rules can be numbered uniquely in a straightforward way by taking the
bottom row and reading 0 for a white cell and 1 for a black cell. This gives the
number for that rule in binary notation. For example, the rule in
Figure~\ref{fig:ca-example-rule} has number 110 in decimal notation (01101110
in binary).

Figure~\ref{fig:ca-example-evol} shows the \emph{evolution} of this
automaton.
The first line is the initial state, for which the colours of the cells have
been chosen randomly. Every successive line shows the next step in the evolution
and is computed by applying the rule to every subsequence of length 3 on the
previous line. 
The line of white or black cells on which the rule operates can be
  chosen to be two-way infinite or
  cyclic. Figure~\ref{fig:ca-example-evol} is an example of the latter:
the lines are assumed to ``wrap'', meaning that the left-hand
neighbour of a cell in the leftmost column is the cell in the rightmost column
of the same line, and vice versa. Here, we have chosen a line width of 100 cells
and the first 50 steps of the evolution are depicted.

In general, a one-dimensional cellular automaton can be formally
represented by a function $\rho : \Sigma^w \to \Sigma$, the
rule, where $\Sigma$ is an alphabet and $w \geq 1$ is the
\emph{width} of the automaton.
Given an infinite sequence $\sigma \inp \Sigma^\infty$, a \emph{step}
of a CA is an application of $\rho$ to every $w$-length subsequence of
$\sigma$, which produces a new infinite sequence.
In the example of Figure~\ref{fig:ca-example-rule} we have
$\Sigma = \{\mathrm{white},\mathrm{black}\}$, $w = 3$ and $\rho$ is as
depicted.
In Figure~\ref{fig:ca-example-evol} we assume that
the infinite sequences $\sigma \inp \Sigma^\infty$ are periodic with a
period of 100 cells, and only one period is displayed.
Periodicity of the input sequence guarantees that the successive
sequences are also periodic, with a period of the same size.

Wolfram classifies cellular automata based on the complexity of the patterns
that emerge in their evolutions. Four classes are distinguished of which class~1
contains the simplest automata and class~4 the most complex. An example of a
class~1 automaton is the one with rule number 0, which simply colours every cell
white in the first step and retains this state in subsequent steps. The complex
pattern of Figure~\ref{fig:ca-example-evol} identifies automaton 110 as a
class~4 automaton. Moreover, Wolfram has shown that the 110 automaton is
\emph{universal} or \emph{Turing complete}, which means it can perform exactly
the same computations a Turing machine can. To be precise: given a
(possibly universal) Turing machine $M$, there are finite sequences
$\rho,\nu \inp \{\mathrm{white},\mathrm{black}\}^*$ as well as an
encoding of any (finite) input sequence $\sigma$ of $M$ as a finite
sequence $\sigma'\inp \{\mathrm{white},\mathrm{black}\}^*$, such that
the behaviour of $M$ on the input $\sigma$ is in some sense mimicked
(through a complicated encoding) by the evolution of cellular
automaton 110 on the infinite input sequence composed of $\sigma'$,
flanked on the left by infinitely many repetitions of $\rho$ and on the
right by infinitely many repetitions of $\nu$.

\begin{figure}
\vspace{-3pt}
  \centering
  \subfigure[0 steps]{\label{fig:step0}
    \begin{minipage}[t]{2cm}
    \centering
    \begin{tikzpicture}[node distance=2cm,auto,>=stealth]
      \node[state,initial left,initial text=] (p0) {};
      \path[->] (p0) edge [loop above] node {$w,b$} ();
    \end{tikzpicture}
    \end{minipage}}
  \hspace{0.5cm}
  \subfigure[1 step]{\label{fig:step1}
    \begin{tikzpicture}[node distance=1.5cm,auto,>=stealth]
      \node[state,initial left,initial text=] (p0) {};
      \node[state] (p1) [below left of=p0] {};
      \node[state] (p2) [below right of=p0] {};
      \node[state] (p3) [below of=p2] {};
      \node[state] (p4) [below of=p1] {};
      \path[->] (p0) edge [loop above] node {$b$} ()
                     edge node [swap] {$w$} (p1)
                (p1) edge [loop left] node {$w$} ()
                     edge node {$b$} (p2)
                (p2) edge node {$w$} (p3)
                     edge node [swap] {$b$} (p0)
                (p3) edge [loop right] node {$w$} ()
                     edge node [swap] {$b$} (p4)
                (p4) edge node {$b$} (p1);
    \end{tikzpicture}}
    \caption{Minimal DFAs describing the possible sequences of white and black
    cells that can occur after 0 steps (a) and 1 step (b) of cellular automaton
    110.}
\vspace{-6pt}
\end{figure}

As described in \cite{Wol:84}, the possible finite sequences
appearing as a continuous subsequence of the infinite sequence
obtained after $n$ steps of a given cellular automaton (starting from a random input
sequence) constitute a language that can be described by a DFA.
For example, the DFA that describes the possible sequences after 0
steps of cellular automaton 110 is depicted in Figure~\ref{fig:step0}: any
sequence of white or black cells is allowed. The DFA after 1 step is shown in
Figure~\ref{fig:step1}. Both DFAs are minimal.
Here every state can be considered final, except for omitted sink states
(see Section~\ref{sec:prelim}).
It is known that for some rules, the size of these
DFAs increases exponentially in $n$ (\textit{cf}.~\cite{Sut:03}).
Rule~110 exhibits this phenomenon.

\begin{table}[p]
  \centering
  \begin{tabular}{|l|r|r|r|r|r|r|r|}
    \multicolumn{1}{l@{~~}}{size of input NFA: \hfill 800}\\
    \multicolumn{1}{l@{~~}}{after applying \algo{sim}: \hfill 228}\\
    \cline{2-8}
    \multicolumn{1}{l@{~~}}{minimal DFA: \hfill 1\,357} &
    \multicolumn{7}{|c|}{\bf STEP 4} \\
    \cline{2-8}
    \multicolumn{1}{c}{} & \multicolumn{1}{|c|}{\algo{sim}\bf T} &
    \multicolumn{1}{|c|}{\bf DT} & \multicolumn{1}{|c|}{\bf MT} &
    \multicolumn{1}{|c|}{\algo{sim}\bf S} & \multicolumn{1}{|c|}{\bf DS} &
    \multicolumn{1}{|c|}{\bf MS} & \multicolumn{1}{|c|}{$|\D{S}|$} \\
    \hline
    \Subset &\multicolumn{1}{|c|}{$-$}& 2.55 & 1.08 &
    \multicolumn{1}{|c|}{$-$} & 15.4 & 5.3 & 152\,804\\
    \hline
    \Transset &\multicolumn{1}{|c|}{$-$}& 1.87 & 0.60
    &\multicolumn{1}{|c|}{$-$}& 18.0 & 3.3 & 94\,473\\
    \hline
    \Subset after \algo{sim} & 0.06 & 0.6 & 0.4 & 0.4 & 5.4 & 2.0 & 58\,370\\
    \hline
    \Transset after \algo{sim} & 0.06 & 1.0 & 0.4 & 0.4 & 9.0 & 2.0 & 58\,094\\
    \hline
    \SubsetClossim & 0.06 & 1.6 & $<$ 0.1 & 0.4 & 2.1 & 0.2 & 4\,720\\
    \hline
    \SubsetCompsim & 0.06 & $<$ 0.1 & $<$ 0.1 & 0.4 & 0.6 & 0.2 & 4\,745\\
    \hline
    \TranssetCompsim & 0.06 & $<$ 0.1 & $<$ 0.1 & 0.4 & 0.7 & 0.2 & 4\,720\\
    \hline
    \multicolumn{8}{c}{}\\
    \multicolumn{8}{c}{}\\
    \multicolumn{1}{l@{~~}}{size of input NFA: \hfill 5\,224}\\
    \multicolumn{1}{l@{~~}}{after applying \algo{sim}: \hfill 1\,421}\\
    \cline{2-8}
    \multicolumn{1}{l@{~~}}{minimal DFA: \hfill 18\,824} &
    \multicolumn{7}{|c|}{\bf STEP 5} \\
    \cline{2-8}
    \multicolumn{1}{c}{} & \multicolumn{1}{|c|}{\algo{sim}\bf T} &
    \multicolumn{1}{|c|}{\bf DT} & \multicolumn{1}{|c|}{\bf MT} &
    \multicolumn{1}{|c|}{\algo{sim}\bf S} & \multicolumn{1}{|c|}{\bf DS} &
    \multicolumn{1}{|c|}{\bf MS} & \multicolumn{1}{|c|}{$|\D{S}|$} \\
    \hline
    \Subset & \multicolumn{1}{|c|}{$-$} & 1250.3 & 179.3 &
    \multicolumn{1}{|c|}{$-$} & 1966.4 & 623.8 & 17\,960\,608\\
    \hline
    \Transset & \multicolumn{1}{|c|}{$-$} & 525.1 & 121.6 &
    \multicolumn{1}{|c|}{$-$} & 1376.5 & 418.3 & 12\,083\,653\\
    \hline
    \Subset after \algo{sim} & 2.28 & 212.5 & 76.7 & 5.9 & 688.2 & 267.2 & 7\,663\,165 \\
    \hline
    \Transset after \algo{sim} & 2.28 & 257.3 & 79.1 & 5.9 & 1\,146.9 & 263.0 & 7\,541\,248 \\
    \hline
    \SubsetClossim & 2.28 & 2~739.7 & 1.6 & 5.9 & 123.2 & 6.3 & 176\,008 \\
    \hline
    \SubsetCompsim & 2.28 & 4.3 & 1.4 & 5.9 & 16.7 & 6.4 & 179\,146 \\
    \hline
    \TranssetCompsim & 2.28 & 4.1 & 1.6 & 5.9 & 22.9 & 6.3 & 176\,008 \\
    \hline
    \multicolumn{8}{c}{}\\
    \multicolumn{8}{c}{}\\
    \multicolumn{1}{l@{~~}}{size of input NFA: \hfill 73\,905}\\
    \multicolumn{1}{l@{~~}}{after applying \algo{sim}: \hfill 18\,934}\\
    \cline{2-8}
    \multicolumn{1}{l@{~~}}{minimal DFA: \hfill 136\,401} &
    \multicolumn{7}{|c|}{\bf STEP 6} \\
    \cline{2-8}
    \multicolumn{1}{c}{} & \multicolumn{1}{|c|}{\algo{sim}\bf T} &
    \multicolumn{1}{|c|}{\bf DT} & \multicolumn{1}{|c|}{\bf MT} &
    \multicolumn{1}{|c|}{\algo{sim}\bf S} & \multicolumn{1}{|c|}{\bf DS} &
    \multicolumn{1}{|c|}{\bf MS} & \multicolumn{1}{|c|}{$|\D{S}|$} \\
    \hline 
    \Subset &  \multicolumn{1}{|c|}{$-$}  & $\dagger$ & $\dagger$ &
    \multicolumn{1}{|c|}{$-$} & $\dagger$ & $\dagger$ & $\dagger$\\
    \hline
    \Transset &  \multicolumn{1}{|c|}{$-$}  & $\dagger$ & $\dagger$ &
    \multicolumn{1}{|c|}{$-$} & $\dagger$ & $\dagger$ & $\dagger$\\
    \hline 
    \Subset after \algo{sim} & 1343.8 & $\dagger$ & $\dagger$ & 433.1 & $\dagger$ & $\dagger$ & $\dagger$\\
    \hline
    \Transset after \algo{sim} & 1343.8 & $\dagger$ & $\dagger$ & 433.1 & $\dagger$ & $\dagger$ & $\dagger$\\
    \hline
    \SubsetClossim & 1343.8 & $>$ 160\,000 & ? & 433.1 & ? & ? & ?\\
    \hline
    \SubsetCompsim & 1343.8 & 1\,467.2 & 90.0 & 433.1 & 770.9 & 244.9 & 7\,100\,549\\
    \hline
    \TranssetCompsim & 1343.8 & 241.9 & 88.4 & 433.1 & 770.9 & 234.4 & 6\,770\,155\\
    \hline
  \end{tabular}
  \vspace{3mm}
  \caption{Benchmark results for canonising NFAs of steps 4, 5 and 6 of CA
  110.\newline Legend: {\algo{sim}} = Minimisation modulo
  simulation equivalence prior to determinisation,
   {\bf D} = Determinisation,
   {\bf M} = Minimisation, {\bf T} = Time (sec), {\bf S} =
    Space (peak memory use, MB), $|\D{S}|$ = Size of DFA after
    determinisation, $\dagger$ = out of memory, ? = not measured.}
  \label{tab:celaut-benchmarks}
\end{table}

We have generated the minimal DFAs for steps 1 through 6 of this CA
using the various algorithms presented here.
We ran the algorithms \Subset and \Transset with and without
minimisation of the input NFA modulo simulation equivalence prior to
determinisation. It turns out that the costs in time and memory of this
prior minimisation step is very small compared to the costs of the
subsequent determinisation process, and that it makes makes the overall
algorithm much more efficient. 
In order to run the algorithms \SubsetCompsim or \TranssetCompsim,
prior minimisation modulo $\smeq$ is required. For \SubsetClossim
we always minimise modulo $\smeq$ as well, as we have to
calculate the simulation relation between the states of the NFA anyway.

The most interesting results are those for steps 4 through 6, which are
shown in Table~\ref{tab:celaut-benchmarks}.
On step 6, algorithms \Subset and \Transset ran out of memory on our
4~GB computer.
We terminated \SubsetClossim prematurely after roughly 44 hours of
computation and did not measure its memory consumption.
The algorithms that use $\compression{\ssmin}$ clearly outperform the
others, in both memory and time efficiency.
Every algorithm that uses a function other than $\idty$ generates a DFA
that is an order of magnitude smaller than that of its
$\idty$-counterpart.

\subsection{Random Automata}

\begin{figure}
\centering
\input{plots/minsize-100.tex}
\caption{Mean and standard deviation of size of minimal DFA for $N=100$}
\label{fig:minsize-100}
\end{figure}

In \cite{TV:05}, Tabakov and Vardi experimentally evaluate the performance of
several automata algorithms by running them on randomly generated automata.
In their model, the randomly generated NFAs have an alphabet $\Sigma =
\{0,1\}$.
The parameters that can be set by the user are the number of states $N$, the
\emph{transition density} $r$, and the \emph{final state density} $f$.
The transition density indicates the ratio of the number of transitions
to the number of states $N$ for a given label $a \in \Sigma$.
The final state density indicates the ratio of the number of final
states $|F|$ to the total number of states $N$.
For example, if we choose $N=20$, $r = 2.0$, and $f = 0.4$, the
resulting NFA will have $20$ states, $40$ $0$-labelled transitions, $40$
$1$-labelled transitions, and $8$ final states.

The generated automaton need not be connected: for every label $a\in \Sigma$
transitions are added by repeatedly choosing two states $s,t$ at random and
adding transition $(s,a,t)$ only if it does not already exist, until the number
of $a$-transitions equals (or exceeds) $r \cdot N$.
So, if the transitions are chosen poorly or the transition density is
not high enough, not all states are reachable from the initial state.

For our experiments, we let $N$ range from $10$ to $100$ with steps of
$10$, $r$ ranges from $0.25$ to $4.0$ with steps of $0.25$, and $f$
ranges from $0.0$ to $1.0$ with steps of $0.2$.
For every combination of parameter values, we generate $100$ random NFAs,
giving a grand total of $96\,000$ automata.
All these automata are first of all minimised modulo simulation
equivalence; this step is the same for all algorithms and not included
in our measurements.
Each of the resulting automata is determinised in turn by each of the 
algorithms and subsequently minimised.
The time, peak memory and size of the intermediate DFA of each run of an
algorithm are measured.
For each combination of parameter values and a determinisation algorithm
we compute the mean of the $100$ measurements.

\begin{figure}
\centering
\input{plots/minsize-0_40.tex}
\caption{Mean size of minimal DFA for $f = 0.40$}
\label{fig:minsize-f0.40}
\end{figure}

For $N = 100$ we have plotted the size of the minimal DFA in
Figure~\ref{fig:minsize-100}.
Every data point is the mean (solid line) or standard deviation (dashed
line) of the $100$ minimal DFAs that were generated for that point.
We see the same phenomena already noticed by Tabakov and Vardi:
apart from the case $f = 0$, the
final state density does not have a noteworthy effect on the size of the
minimal DFA, but the transition density does.
The mean size shows a clear peak at $r = 1.25$.
For this value, the standard deviation is about as large as the mean,
indicating that there's quite some variance in the minimal DFA sizes.
For example, for $r = 1.25$ and $f = 0.40$ the mean is $44\,213$, the
standard deviation is $36\,182$ and the sizes of the minimal DFAs range
from $296$ to $179\,757$.
For other values of $N$ the plot has the same shape as that of
Figure~\ref{fig:minsize-100}.

Because the final state density does not seem to influence the results
that much, we fix $f = 0.40$.
Again we plot the mean size of the minimal DFA but this time with the
size of the NFA ($N$) along the $y$-axis, see
Figure~\ref{fig:minsize-f0.40}.
We see that the NFA size really matters for values of $r$ that are in
the range of $0.75$ to $1.50$.
Outside of this range, the size of the minimal DFA remains almost
constant as the size of the NFA increases.
At $r = 1.25$ the effect of the NFA size is most dramatic: the mean size
of the minimal DFA at $N = 100$ is more than $2\,000$ times as large as
the mean size at $N = 10$.

As mentioned above, the value of $f$ does not seem to influence the results that
much, so we fix it at $f = 0.40$. In Appendix~\ref{app:random-plots1} we have
plotted for various values of $r$ the peak memory usage, total running time and
size of the intermediate DFAs of canonisation using each of the four algorithms
against the size of the input NFA $N$. Again, every data point is the mean of
$100$ experiments. 

Just looking at the sizes of the intermediate DFAs
(Section~\ref{app:sizeplots}), we see that, for all values of $r$ and $N$,
\Subset and \SubsetCompsim generate significantly larger DFAs than the
other algorithms.
For $r \leq 1.00$ these DFAs are very close (if not equal) to the minimal DFAs.
We also see that for $r > 3$ the DFA generated by \Transset is slightly
larger than the ones generated by \SubsetClossim and \TranssetCompsim.
Note that the measurements are in accordance with our lattice.

On the time plots of Section~\ref{app:timeplots}, it is clear that
\Subset is the fastest algorithm.
Note that a mean value of $1 \cdot 10^{-4}$ indicates that the runs were
too fast to allow proper measuring.
\SubsetCompsim is as fast as \Subset for $0.25 \leq r \leq 1$, but for
larger $r$-values it becomes slower, ending up in 4th place for $r > 2$.
Overall, \TranssetCompsim can be considered the slowest algorithm.

Regarding memory consumption (Section~\ref{app:memplots}), the \Subsetf
algorithms overall perform better than the \Transsetf algorithms, with
\SubsetClossim being the most memory efficient.
The curves for \SubsetCompsim closely follow the ones for
  \Subset, but for $r<2$ \SubsetCompsim performs somewhat better.
Given the fact that \SubsetClossim produces the same DFA as
\TranssetCompsim, the former is preferable as it has better time and
space performance. Overall, \Subset and \SubsetClossim perform the
best. \SubsetClossim appears to use around 20\% less memory overall,
but is by far not as fast.


\section{Conclusions}\label{sec:concl}

We have presented a schematic generalisation of the well-known subset
construction algorithm that allows for a function to be applied to every
generated set of states.
We have given a similar scheme for a variant of subset construction that
operates on sets of transitions rather than states.
Next, we instantiated these schemes with several set-expanding or
-reducing functions to obtain various determinisation algorithms.
One of these algorithms even produces the minimal DFA directly, but its
use of the PSPACE-hard language preorder renders it impractical.
As our aim is to reduce the average-case workload in practice, we
instead use
the PTIME-decidable simulation preorder in the other algorithms.
We have classified all presented algorithms in a lattice, based on the
sizes of the DFAs they produce.
This is a natural criterion, as the worst-case complexities are the same
for all algorithms.
To assess their performance, we have implemented and benchmarked them.
The case study comprised NFAs describing patterns in the elementary
cellular automaton with rule number 110 and randomly generated NFAs.
On the cellular automaton examples, the algorithms that use a
function to reduce the computed sets, convincingly outperformed the
others.
On the random automata, three of the algorithms generated smaller
DFAs than subset construction, which led to less memory
consumption in some cases.
In particular, our algorithm \SubsetClossim systematically
  outperforms the standard subset construction in memory consumption. 
However, the gain is relatively small, and goes at the expense of the
speed of the algorithm.

Based on our algorithm schemes, many more algorithms can be constructed
by substituting various functions, depending on the specific needs and
applications.
Moreover, the functions we defined here could be equipped with any suitable
preorder or partial order, \eg from the linear time -- branching time
spectrum.

We believe
that our optimisations to subset construction are
particularly beneficial in cases where normal subset construction
is known to leave
a large gap between the generated DFA and the minimal one.
Our first case study deals with such a situation and supports this theory.

\paragraph{Acknowledgements.} We would like to thank Jan Friso Groote, Tim
Willemse and Sebastian Maneth for valuable ideas, discussions and/or
comments.

\bibliographystyle{plain}
%\bibliography{paper}
\begin{thebibliography}{10}

\bibitem{BP:95}
{ B.~Bloom \& R.~Paige} (1995):
\newblock {\em Transformational design and implementation of a new efficient solution to the ready simulation problem.}
\newblock {\sl Science of Computer Programming} 24(3), pp. 189--220.

\bibitem{Brz:63}
{ J.A. Brzozowski} (1963):
\newblock {\em Canonical regular expressions and minimal state graphs for definite events.}
\newblock In {\sl {\rm Proceedings of the Symposium on} Mathematical Theory of Automata}, MRI Symposia Series, vol. 12, Polytechnic Press, Polytechnic Institute of Brooklyn, pp. 529--561.

\bibitem{mCRLWeb}
{ CWI}:
\newblock {\em {{\textmu}CRL Toolset Home Page}.}
\newblock \url{http://www.cwi.nl/~mcrl/}.

\bibitem{DHT:92}
{ D.L. Dill, A.J. Hu \& H.~Wong-Toi} (1992):
\newblock {\em Checking for language inclusion using simulation preorders.}
\newblock In {\sl {\rm Proceedings of the Third International Workshop on} Computer-Aided Verification {\rm (CAV'92)}}, LNCS 575, Springer, pp. 255--265.

\bibitem{FB:94}
{ R.W. Floyd \& R.~Beigel} (1994):
\newblock {\em The Language of Machines}.
\newblock Freeman.

\bibitem{GPP:03}
{ R.~Gentilini, C.~Piazza \& A.~Policriti} (2003):
\newblock {\em From bisimulation to simulation: Coarsest partition problems.}
\newblock {\sl Journal of Automated Reasoning} 31(1), pp. 73--103.

\bibitem{GP:08}
{ R.J.~van Glabbeek \& B.~Ploeger} (2008):
\newblock {\em Correcting a space-efficient simulation algorithm.}
\newblock CS-Report 08-06, Eindhoven University of Technology.
\newblock To appear in Proceedings 20th International Conference on {\sl Computer Aided Verification} (CAV'08), LNCS, Springer.

\bibitem{GR:01}
{ J.F. Groote \& M.A. Reniers} (2001):
\newblock {\em Algebraic process verification.}
\newblock In J.A. Bergstra, A.~Ponse \& S.A. Smolka, editors: {\sl Handbook of Process Algebra}, Elsevier, pp. 1151--1208.

\bibitem{HHK:95}
{ M.R. Henzinger, T.A. Henzinger \& P.W. Kopke} (1995):
\newblock {\em Computing simulations on finite and infinite graphs.}
\newblock In {\sl {\rm 36th Annual Symposium on} Foundations of Computer Science {\rm ({FOCS}'95)}}, IEEE Computer Society Press, pp. 453--462.

\bibitem{Hop:71}
{ J.E. Hopcroft} (1971):
\newblock {\em An $n \log n$ algorithm for minimizing states in a finite automaton.}
\newblock In Z.~Kohavi, editor: {\sl Theory of Machines and Computations}, Academic Press, pp. 189--196.

\bibitem{HU:79}
{ J.E. Hopcroft \& J.D. Ullman} (1979):
\newblock {\em Introduction to Automata Theory, Languages, and Computation}.
\newblock Addison-Wesley.

\bibitem{Par:81}
{ D.M.R. Park} (1981):
\newblock {\em Concurrency and automata on infinite sequences.}
\newblock In {\sl {\rm Proc. 5th {GI}-Conference on} Theoretical Computer Science}, LNCS 104, Springer, pp. 167--183.

\bibitem{SM:73}
{ L.J. Stockmeyer \& A.R. Meyer} (1973):
\newblock {\em Word problems requiring exponential time.}
\newblock In {\sl {\rm Proc.~5th Annual ACM Symposium on} Theory of Computing {\rm (STOC'73)}}, ACM, pp. 1--9.

\bibitem{Sut:03}
{ K.~Sutner} (2003):
\newblock {\em The size of power automata.}
\newblock {\sl Theoretical Computer Science} 295(1-3), pp. 371--386.

\bibitem{TV:05}
{ D.~Tabakov \& M.Y. Vardi} (2005):
\newblock {\em Experimental evaluation of classical automata constructions.}
\newblock In {\sl {\rm Proceedings of the 12th International Conference on} Logic for Programming, Artificial Intelligence, and Reasoning {\rm (LPAR'05)}}, LNCS 3835, Springer, pp. 396--411.

\bibitem{Wat:95}
{ B.W. Watson} (1995):
\newblock {\em Taxonomies and Toolkits of Regular Language Algorithms}.
\newblock PhD thesis, Technische Universiteit Eindhoven.

\bibitem{Wol:84}
{ S.~Wolfram} (1984):
\newblock {\em Computation theory of cellular automata.}
\newblock {\sl Communications in Mathematical Physics} 96(1), pp. 15--57.

\bibitem{Wol:02}
{ S.~Wolfram} (2002):
\newblock {\em A New Kind of Science}.
\newblock Wolfram Media, Inc.

\end{thebibliography}

\newpage
\appendix

\section{Correctness of \Subsetf}
\label{app:Subset}

We need the following lemma, for which it is important to understand
that a set of NFA states $P$ denotes a set of states in \mc{N} but must
be regarded as only a single state in \mc{D}.

\begin{lemma}\label{lem:lnpeqldp}
  Let $\mc{D}$ be obtained by applying $\Subsetf$ on the NFA
  $\mc{N}$, where the function $f: \power{S_\mc{N}} \to
  \power{S_\mc{N})}$ satisfies $\lang{N}{f(Q)}=\lang{N}{Q}$ for any
  $Q\subseteq\N{S}$.
  Then for any $P \in \D{S}$ it holds that $\lang{N}{P} = \lang{D}{P}$.
\end{lemma}

\begin{proof}
We show set inclusion both ways.
\begin{itemize}
  \item We prove that $\sigma \in \lang{N}{P}$ implies $\sigma \in
    \lang{D}{P}$ for any $\sigma \in \N{\Sigma}$ and $P\in\D{S}$
    by induction on the length of $\sigma$.\\[1ex]
	%
  \emph{Base:} $\sigma = \emptystring$. Let $P\inp\D{S}$, and
    assume $\sigma \in \lang{N}{P}$.
    Then there exists a $p \in P$ such that $\emptystring \in
    \lang{N}{p}$, and hence $p \inp \N{F}$. By
    line~\ref{line:accepting} of
    Algorithm~\ref{alg:subset} we have $P\inp\D{F}$ and thus
    $\emptystring \in \lang{D}{P}$.\\[1ex]
	%
  \emph{Step:} $\sigma = a\rho$ for some $a \inp \N{\Sigma}$ and $\rho \inp
  \N{\Sigma}^*$. Let $P\inp\D{S}$ and assume $\sigma \inp \lang{N}{P}$.
    Then there exists a $p \inp P$ such that $\sigma \inp \lang{N}{p}$.
    Hence there is a $q \inp \N{S}$ such that \plat{p \ltrans{a}{N} q} and
    $\rho\inp\lang{N}{q}$. Since $p \inp P$ and \plat{p \ltrans{a}{N} q},
    $\Subsetf$ (lines \ref{line:main1}--\ref{line:main2})
    ensures that \plat{P \ltrans{a}{D}f(Q)}
    for some $Q \subseteq \N{S}$ with $q\inp Q$.
    We have $\rho\inp\lang{N}{q} \subseteq\lang{N}{Q} = \lang{N}{f(Q)}$,
    and thus, by induction, $\rho \in \lang{D}{f(Q)}$. This implies
    $a\rho \inp \lang{D}{P}$.
	
  \item We prove that $\sigma \in \lang{D}{P}$ implies $\sigma \in
    \lang{N}{P}$ for any $\sigma \in \N{\Sigma}$ and $P\in\D{S}$
    by induction on the length of $\sigma$.\\[1ex]
	%
  \emph{Base:} $\sigma = \emptystring$. Assume $\sigma \inp \lang{D}{P}$.
  Then $P \inp \D{F}$ so there exists a $p \inp
  P$ such that $p \inp \N{F}$. For this $p$, $\emptystring \inp \lang{N}{p}$. Then also
  $\emptystring \inp \bigcup_{q \inp P} \lang{N}{q}$ and thus
  $\emptystring \inp
  \lang{N}{P}$.\\[1ex]
	%
  \emph{Step:} $\sigma = a\rho$ for some $a \inp \D{\Sigma}$ and $\rho \inp
  \D{\Sigma}^*$.  Let $P\inp\D{S}$ and assume $\sigma \inp \lang{D}{P}$.
  Then there exists a $P' \inp \D{S}$ such that
  \plat{P\ltrans{a}{D}P'} and $\rho \inp \lang{D}{P'}$. By induction
  \mbox{$\rho \inp \lang{N}{P'}$}. We know that $P' \mathbin= f(Q)$
  where \plat{Q = \{ q \inp \N{S} \mid \exists p \inp P\ .\ p
  \ltrans{a}{N} q \}}. As $\lang{N}{f(Q)}=\lang{N}{Q}$,
  we have $\rho \inp
  \lang{N}{Q}$. Because $\lang{N}{Q} = \bigcup_{q \inp Q}\lang{N}{q}$, there
  exists a $q \inp Q$ such that $\rho \inp \lang{N}{q}$ and hence
    there is a $p
  \inp P$ such that \plat{p \ltrans{a}{N} q}. Now $a\rho \inp \lang{N}{p}$ for that
  $p$ and thus we obtain $\sigma \inp \lang{N}{P}$.\qed
\end{itemize}
\end{proof}

\noindent By Lemma~\ref{lem:lnpeqldp} we are now allowed to use language
equivalence and inclusion without specifying whether we mean language
equivalence (resp.\ inclusion) between sets of states in an NFA
or single states in the generated DFA.

\begin{theorem}\label{thm:subsetf correct}
  Let $\mc{D}$ be obtained by applying $\Subsetf$ on the NFA
  $\mc{N}$, where the function $f: \power{S_\mc{N}} \to
  \power{S_\mc{N})}$ satisfies $\lang{N}{f(Q)}=\lang{N}{Q}$ for any
  $Q\subseteq\N{S}$.
 Then $\mc{D}$ is deterministic and language equivalent to \mc{N}.
\end{theorem}

\begin{proof}
    It can be easily seen from the algorithm that
    for each combination of $P \in \D{S}$ and $a \in \D{\Sigma}$, precisely one
    tuple  $(P,a,P')$ for some $P' \in \D{S}$ is added to $\D{\delta}$. Hence
    \mc{D} is deterministic.
We derive $\mc{D}\lgeq\mc{N}$ using
    Lemma~\ref{lem:lnpeqldp}:\\[1ex]
\small\mbox{}\hfill
$\lang{}{\mc{D}}
= \lang{D}{\D{i}}
= \lang{D}{f({\{\N{i}\}})}
\stackrel{\rm L\ref{lem:lnpeqldp}}{=} \lang{N}{f({\{\N{i}\}})}
= \lang{N}{\{\N{i}\}}
= \lang{N}{\N{i}}
=  \lang{}{\mc{N}}$\qed
\end{proof}

\subsection{Correctness of \SubsetClos}
\label{app:Subsetclos}

For any set of states $P$ in an NFA $\mc{N}$, $\closuref{\lgin}{P}$
contains all states that are language included in $P$. In particular,
because $p \lgin P$ for all $p \inp P$, we have that $P \subseteq
\closuref{\lgin}{P}$.

\begin{proposition}\label{thm:PeqclosP}
For any set of states $P \subseteq \N{S}$, it holds that $P \lgeq
\closuref{\lgin}{P}$.
\end{proposition}

\begin{proof}
Let $Q := \closuref{\lgin}{P}$. 
We show that $P \lgin Q$
and $Q \lgin P$:
\begin{itemize}
  \item $P \lgin Q$: using the fact that $P \subseteq
    Q$, we
    derive: $\lang{N}{P} = \bigcup_{p \in P} \lang{N}{p} \subseteq \bigcup_{p
    \in Q} \lang{N}{p} =
    \lang{N}{Q}$, hence $P \lgin Q$;
  \item $Q \lgin P$: for all $p \in Q$ we know (by definition)
    that $p \lgin P$, \ie $\lang{N}{p} \subseteq \lang{N}{P}$. Thus:
    $\lang{N}{Q} = \bigcup_{p \in Q} \lang{N}{p} \subseteq
    \lang{N}{P}$, hence $Q \lgin P$. \qed
\end{itemize}
\end{proof}

\begin{theorem}\label{thm:closure correct}
Given an NFA \mc{N}, \SubsetClos constructs the
minimal DFA that is language equivalent to \mc{N}.
\end{theorem}

\begin{proof}
It follows immediately from Theorem~\ref{thm:subsetf correct} and
Proposition~\ref{thm:PeqclosP} that the NFA \mc{D} constructed by
\SubsetClos is a DFA that is language equivalent to \mc{N}.

\mc{D} is minimal if there is no DFA that is language
    equivalent to \mc{D} and has fewer states than \mc{D}. It is known that this
    follows directly if we prove that there is no pair of different states in
    \mc{D} that are language equivalent (see for instance Corollary~4.24 in
    \cite{FB:94}). Suppose \mc{D} contains states $P$ and $Q$ such that $P
    \lgeq Q$ and for some $T,U \subseteq \N{S}$, $P = \closuref{\lgin}{T}$ and $Q =
    \closuref{\lgin}{U}$. Then for all $p \inp P$ we have $p \lgin P \lgeq Q =
    \closuref{\lgin}{U} \lgeq U$,
    by Proposition~\ref{thm:PeqclosP}. Because $Q = \{ q \in \N{S} \mid q \lgin
    U \}$ we see that $p \in Q$ and thus that $P \subseteq Q$. By symmetry we
    have that $Q \subseteq P$. Hence $P = Q$. \qed
\end{proof}

\subsection{Correctness of $\protect\SubsetClossim$}
\label{app:Subsetclossim}

\begin{proposition}\label{prop:subsetclossim}
For any set of states $P \subseteq \N{S}$, it holds that $P \lgeq
\closuref{\ssmin}{P}$.
\end{proposition}

\begin{proof}
Let $Q := \closuref{\ssmin}{P} = \{q \in \N{S} \mid q \smin P\}$.
We show that $P \lgeq Q$:
\begin{itemize}
  \item $P \lgin Q$: this follows immediately from $P \subseteq Q$;
  \item $Q \lgin P$:  By induction on the length of $\sigma \in \N{\Sigma}$
  we show that $\sigma\inp\lang{N}{Q}$ implies $\sigma\inp\lang{N}{P}$.
  If $\emptystring \inp \lang{N}{Q}$ then $\emptystring \inp
  \lang{N}{q}$ for some $q\inp Q$. Hence $q \in \N{F}$.
  It must be that $q\smin P$. Thus $\exists p \inp P.~p \inp \N{F}$
  and therefore $\emptystring \inp \lang{N}{p} \subseteq \lang{N}{P}$.

  If $a\rho \inp \lang{N}{Q}$ then there is a $q \inp Q$ and $q'\inp
  \N{S}$ such that $q \ltrans{a}{N} q'$ and $\rho \inp \lang{N}{q'}$.
  It must be that $q\smin P$, so there exists a simulation $R
  \subseteq \N{S} \times \N{S}$ such that \plat{\exists p,p' \inp \N{S}.~p
  \inp P \wedge p \ltrans{a}{N}p' \wedge q' R p'}.
  Therefore, $q' \smin p'$ and hence $q' \lgin p'$, so $\rho \inp
  \lang{N}{p'}$. It follows that $a\rho \inp \lang{N}{P}$.
\qed
\end{itemize}
\end{proof}

\begin{theorem}
Given an NFA \mc{N}, \SubsetClossim constructs a DFA that is language
equivalent to \mc{N}.
\end{theorem}

\begin{proof}
Immediate from Theorem~\ref{thm:subsetf correct} and
Proposition~\ref{prop:subsetclossim}.
\qed\end{proof}

\subsection{Correctness of $\protect\SubsetCompsim$}
\label{app:Subsetcompsim}

\paragraph{Note:} In this section we fix an NFA \mc{N} that is minimal
under simulation equivalence.

\begin{proposition}\label{prop:subsetcomp}
For any set of states $P \subseteq \N{S}$, it holds that $P \lgeq
\compressionf{\ssmin}{P}$.
\end{proposition}

\begin{proof}
Let $Q := \compressionf{\ssmin}{P}$. 
We show that $P \lgin Q$ and $Q \lgin P$:
\begin{itemize}
  \item $P \lgin Q$: for any $p \inp P$ there is a $q\inp Q$ with
  $p\smin q$ and hence $p \lgin q$. Thus
    $\lang{N}{P} = \bigcup_{p \in P} \lang{N}{p} \subseteq \bigcup_{q
    \in Q} \lang{N}{q} = \lang{N}{Q}$, so $P \lgin Q$;
  \item $Q \lgin P$: this follows immediately from $Q \subseteq P$. \qed
\end{itemize}
\pagebreak[2]
\end{proof}

\begin{theorem}
When applied to \mc{N}, \SubsetCompsim constructs a DFA that is language
equivalent to \mc{N}.
\end{theorem}

\begin{proof}
Immediate from Theorem~\ref{thm:subsetf correct} and
Proposition~\ref{prop:subsetcomp}.
\qed\end{proof}

\section{Correctness of \Transsetf}
\label{app:Transsetf}

\begin{proposition}\label{prp:lang_eq_tuple}
  Given NFA \mc{N}, for any $p \in \N{S}$: $p \lgeq \tuple{p}$.
\end{proposition}

\begin{proof}
Let $p \in \N{S}$ and $S = \{\emptystring\}$ if $p \in \N{F}$ and $S =
\emptyset$ otherwise.
We derive:\\[1ex]
\mbox{~~}\hfill$\begin{array}[b]{ll}
\lang{N}{p} & = \{ \sigma \in \N{\Sigma}^* \mid \exists q \in \N{F}
\,.\, p \ltrans{\sigma}{N} q \}\\
& = \{ a\sigma \in \N{\Sigma}^* \mid \exists q \in \N{F} \,.\, p
\ltrans{a\sigma}{N} q \} \cup S\\
& = \{ a\sigma \in \N{\Sigma}^* \mid \exists q \in \N{S} \,.\, p
\ltrans{a}{N} q \land \sigma \in \lang{N}{q} \} \cup S\\
& = \{ a\sigma \in \N{\Sigma}^* \mid \exists (a,q) \in \trans{p} \,.\,
\sigma \in \lang{N}{q} \} \cup S\\
& = \bigcup_{(a,q)\in \trans{p}} \{ a\sigma \in \N{\Sigma}^* \mid
\sigma \in \lang{N}{q} \} \cup S\\
& = \bigcup_{t \in \trans{p}} \lang{N}{t} \cup S\\
& = \lang{N}{\trans{p}} \cup S\\
& = \lang{N}{\tuple{p}}.
\end{array}$
\hfill\mbox{\qed}
\end{proof}
%
We need the following lemma, in which a transition tuple $(T,b)$ is
regarded as such in the input NFA \mc{N}, but is regarded as a single
state in the output NFA \mc{D}.

\begin{lemma}\label{lem:langD_eq_tuple}
 Let $\mc{N}$ be an NFA and $f: \power{\N{\Sigma} \times \N{S}} \times
 \BB \to \power{\N{\Sigma} \times \N{S}} \times \BB$ such that
 $\lang{N}{f(T,b)} = \lang{N}{T,b}$ for all transition tuples $(T,b)$.
 Let $\mc{D}$ be obtained by applying $\Transsetf$ to $\mc{N}$.
 For any $(T,b) \inp \D{S}$, it holds that $\lang{N}{T,b} =
 \lang{D}{T,b}$.
\end{lemma}

\begin{proof}
We show that $\sigma \inp \lang{N}{T,b} \;\bimp\; \sigma \inp \lang{D}{T,b}$
for any $\sigma \inp \N{\Sigma}^*$ and $(T,b) \inp \D{S}$ by induction
on the length of $\sigma$.\vspace{-1ex}
\begin{trivlist}

\item \textit{Base:} $\sigma = \emptystring$. Let $(T,b) \inp \D{S}$.
Then
  $ 
  \emptystring \inp \lang{N}{T,b}
  \Leftrightarrow b 
  \stackrel{*}{\Leftrightarrow} (T,b) \inp \D{F} 
  \Leftrightarrow \emptystring \inp \lang{D}{T,b} $,
  where $*$ follows from
  lines~\ref{line:trans-fin1}--\ref{line:trans-fin2} of \Transsetf.

\item \textit{Step:} $\sigma = a\rho$ for some $a \inp \N{\Sigma}$ and
  $\rho \inp \N{\Sigma}^*$. We assume
  for any transition tuple $(T',b') \inp \D{S}$:
  \[\label{lem:langD_eq_tuple:IH}\tag{IH} 
  \rho \inp \lang{N}{T',b'} \bimp \rho \inp \lang{D}{T',b'} \]
  and derive, for any $(T,b) \inp \D{S}$:
  \[
  \begin{array}{@{}l@{~}l@{}}
  a\rho \inp \lang{N}{T,b}
  & \bimp\; a\rho \inp \lang{N}{T} 
  \;\bimp\; a\rho \inp \bigcup_{t\inp T} \lang{N}{t}\\
  & \bimp\; a\rho \inp \bigcup_{(a,p) \inp T} \lang{N}{a,p}
  \; \bimp\; \rho \inp \bigcup_{(a,p) \inp T} \lang{N}{p}\\
  & \mathbin{\stackrel{*}{\bimp}}\; \rho \inp \bigcup_{(a,p) \inp T}
  \lang{N}{\tuple{p}}\\
  & \bimp\; \rho \inp \bigcup_{(a,p) \inp T} \big( \lang{N}{\trans{p}} \cup
  \left\{ \begin{array}{@{}c@{~}l@{}}
    \{\emptystring\} & \mbox{if $p \inp \N{F}$}\\
    \emptyset & \mbox{if $p \mathbin{\not\in} \N{F}$}
  \end{array} \right. \big)\\
  & \bimp\; \rho \inp \bigcup_{(a,p) \inp T} \lang{N}{\trans{p}} \cup
  \left\{ \begin{array}{@{}c@{~}l@{}}
    \{\emptystring\} & \mbox{if $\phantom\neg \exists (a,p) \inp T \,.\,
    p \inp \N{F}$}\\
    \emptyset & \mbox{if $\neg \exists (a,p) \inp T \,.\, p \inp \N{F}$}
  \end{array} \right.\\
  & \bimp\; \rho \inp \lang{N}{\bigcup_{(a,p) \inp T} \trans{p},
  \exists (a,p) \in T \,.\, p \in \N{F}}\\
  & \bimp\; \rho \inp \lang{N}{f(\bigcup_{(a,p) \inp T} \trans{p},
  \exists (a,p) \in T \,.\, p \in \N{F})}\\
  & \mathbin{\stackrel{\dagger}{\bimp}}\; \rho \inp
  \lang{D}{f(\bigcup_{(a,p) \inp T} \trans{p}, \exists (a,p) \in T \,.\,
  p \in \N{F})}\\
  & \mathbin{\stackrel{\ddagger}{\bimp}}\; a\rho \inp \lang{D}{T,b}
  \end{array}
  \]
  where at $*$ we used Proposition~\ref{prp:lang_eq_tuple}; at $\dagger$
  we used \eqref{lem:langD_eq_tuple:IH} and the fact that
  lines~\ref{line:trans-main1}--\ref{line:trans-main1b} of \Transsetf
  ensure that $f(\ldots) \inp \D{S}$; and at $\ddagger$ we used that
  line~\ref{line:trans-main2} of \Transsetf ensures that $(T,b)
  \ltrans{a}{D} f(\ldots)$. \qed
\end{trivlist}
\end{proof}

\begin{theorem}\label{thm:transsetf correct}
 Let $\mc{N}$ be an NFA and $f: \power{\N{\Sigma} \times \N{S}} \times
 \BB \to \power{\N{\Sigma} \times \N{S}} \times \BB$ such that
 $\lang{N}{f(T,b)} = \lang{N}{T,b}$ for all transition tuples $(T,b)$.
 Let $\mc{D}$ be obtained by applying $\Transsetf$ to $\mc{N}$.
 Then $\mc{D}$ is deterministic and language equivalent to \mc{N}.
\end{theorem}

\begin{proof}
It can be easily seen from the algorithm that for each combination of $P
\in \D{S}$ and $a \in \D{\Sigma}$, precisely one tuple $(P,a,P')$ for
some $P' \in \D{S}$ is added to $\D{\delta}$.  Hence \mc{D} is
deterministic.
We derive $\mc{D}\lgeq\mc{N}$ as follows:
$$
\begin{array}{ll}
\lang{}{\mc{D}} 
& = \lang{D}{\D{i}} 
= \lang{D}{f(\tuple{\N{i}})} 
\stackrel{*}{=} \lang{N}{f(\tuple{\N{i}})}\\
& = \lang{N}{\tuple{\N{i}}} 
\stackrel{\dagger}{=} \lang{N}{\N{i}} 
= \lang{}{\mc{N}}
\end{array}$$
where at $*$ we used Lemma~\ref{lem:langD_eq_tuple} and at $\dagger$ we
used Proposition~\ref{prp:lang_eq_tuple}.
\qed
\end{proof}

\subsection{Correctness of \Transset}
\label{app:Transset}

As the identity function $\idty$ trivially
satisfies $\lang{N}{T,b} = \lang{N}{\idty(T,b)}$, the following result
follows immediately from Theorem~\ref{thm:transsetf correct}.

\begin{corollary}
Let \mc{D} be obtained by applying \Transset to an NFA \mc{N}. Then
\mc{D} is deterministic and language equivalent to \mc{N}.
\qed\end{corollary}

\subsection{Correctness of $\protect\TranssetCompsim$}
\label{app:Transsetcompsim}

\paragraph{Note:} In this section we fix an NFA \mc{N} that is minimal
under simulation equivalence.

\begin{proposition}\label{prp:comprtuple}
For any transition tuple $(T,b)$: $\lang{N}{T,b} =
\lang{N}{\compressionf{\ssmin}{T,b}}$.
\end{proposition}

\begin{proof}
Let $U := \compressionf{\ssmin}{T}$.
We have to show that:
\[
\lang{N}{T} \cup\ \left\{
\begin{array}{ll}
	\{\emptystring\} & \mbox{if $\phantom\neg b$}\\
	\emptyset & \mbox{if $\neg b$}
\end{array} \right.
\quad=\quad
\lang{N}{U} \cup\ \left\{
\begin{array}{ll}
	\{\emptystring\} & \mbox{if $\phantom\neg b$}\\
	\emptyset & \mbox{if $\neg b$}
\end{array} \right.
\]
which follows naturally if $\lang{N}{T} = \lang{N}{U}$.
For any $t \inp T$ there is a $u \inp U$ with $t \smin u$ and hence $t
\lgin u$. Thus: $\lang{N}{T} = \bigcup_{t
\in T} \lang{N}{t} \subseteq \bigcup_{t \in U} \lang{N}{t} = \lang{N}{U}$.
Because $U \subseteq T$, we also have that $\lang{N}{U} \subseteq
\lang{N}{T}$. Hence $\lang{N}{T} = \lang{N}{U}$. \qed
\end{proof}

\begin{theorem}
Let \mc{D} be obtained by applying \TranssetCompsim to \mc{N}. Then
\mc{D} is deterministic and language equivalent to \mc{N}.
\end{theorem}

\begin{proof}
This follows immediately from Proposition~\ref{prp:comprtuple}
and Theorem~\ref{thm:transsetf correct}.\qed
\end{proof}

\section{Correctness of the Lattice of Algorithms}
\label{app-lattice}

Given an NFA $\mc{N}$, let $\mc{D}(\Subsetf)$ denote the DFA generated
from $\mc{N}$ by algorithm \Subsetf, and likewise for the algorithms
$\Transsetf$.  For $P\subseteq \N{S}$ let $$P/a := \{q \inp \N{S} \mid
\exists p\inp P.~ p\ltrans{a}{N}q\},$$ so that line~\ref{line:main1} of
Algorithm~\ref{alg:subset} can be rewritten as $P' := f(P/a)$.  It
follows that $S_{\mc{D}(\Subsetf)}$ is the smallest set $S\subseteq
\power{\N{S}}$ that contains $f(\{\N{i}\})$ and satisfies
\begin{equation}
P \inp S \Rightarrow f(P/a)\inp S\,.
\label{induction}
\end{equation}
Likewise, for $P$ a transition tuple, let
$$P\mathord\sslash a := (\bigcup_{(a,p) \in \ms{set}(P)}
    \trans{p},\; \exists (a,p) \in \ms{set}(P) \,.\, p \in \N{F})\,,$$
so that line~\ref{line:trans-main1} of Algorithm~\ref{alg:transset}
can be rewritten as $P' := f(P\mathord\sslash a)$.
Moreover, for $P \subseteq \N{S}$ we define\vspace{-1ex}
$$\tuple{P} := (\bigcup_{p\in P}\trans{p}, \exists {p\inp P}.~p \inp \N{F})\,.$$
It follows that $S_{\mc{D}(\Transsetf)}$ is the smallest
$S\subseteq \power{\N{S}}$ that contains $f(\tuple{\N{i}})$, which
equals $f(\tuple{\{\N{i}\}})$, and
satisfies $P \inp S \Rightarrow f(P\mathord\sslash a)\inp S$.

The following definition extends the operator $\closure{\ssmin}$,
originally defined on sets of states, to transition tuples.
The result of applying the operator remains a set of states.
\begin{definition}\label{def:closure-trans}\rm
For any state $p \in \N{S}$ and transition tuple $(T,b)$ we write $p
\smin (T,b)$ iff 
\begin{itemize}
  \item $p \inp \N{F} \imp b$ and
  \item $\forall a\inp \N{\Sigma} \,.\, \forall p' \in \N{S} \,.\; p
    \ltrans{a}{N} p' \;\imp\; \exists (a,q') \inp T \,.\; p' \smin q'$.
\end{itemize}
For any transition tuple $P$ of an NFA \mc{N} we define
$\closuref{\ssmin}{P} := \{ p \in \N{S} \mid p \ssmin P \}$.
\end{definition}

\begin{lemma}\label{crux}
Let $\mc{N}$ be an NFA, $a\inp\N{\Sigma}$ and $P \subseteq \N{S}$. Then
\begin{itemize}
\item[\rm 1.] $\tuple{P}\mathord\sslash a = \tuple{P/a}$,
\item[\rm 2.] \plat{\compression{\ssmin}(P/a) \subseteq \compression{\ssmin}(P)/ a},
\item[\rm 3.] \plat{\compression{\ssmin}(\compression{\ssmin}(P)/ a) = \compression{\ssmin}(P/a)},
\item[\rm 4.] \plat{\closure{\ssmin}(P/a) \supseteq \closure{\ssmin}(P)/ a},
\item[\rm 5.] \plat{\closure{\ssmin}(\closure{\ssmin}(P)/ a) = \closure{\ssmin}(P/a)},
\item[\rm 6.] \plat{\closure{\ssmin}(P) = \closure{\ssmin}(\compression{\ssmin}(P))},
\item[\rm 7.] \plat{\closure{\ssmin}(P) = \closure{\ssmin}(\tuple{P})},
\item[\rm 8.] \plat{\compression{\ssmin}(\tuple{P}) = \compression{\ssmin}(\tuple{\closure{\ssmin}(P)})}.
\end{itemize}
\end{lemma}
\begin{proof}
Ad 1.
Note that $(a,p) \inp \ms{set}(\tuple{P}) \Leftrightarrow p \inp (P/a)$.
Hence\vspace{-1ex} $$\tuple{P}\mathord\sslash a
\begin{array}[t]{@{~}l}
= (\bigcup_{(a,p) \in \ms{set}(\tuple{P})} \trans{p},\;
  \exists (a,p) \in \ms{set}(\tuple{P}) \,.\, p \in \N{F})\\
= (\bigcup_{p\inp(P/a)} \trans{p},\; \exists p \inp (P/a) \,.\, p \in \N{F})\\
= \tuple{P/a}.\vspace{-1ex}
\end{array}$$
Ad 2. Let \plat{p' \in \compression{\ssmin}(P/a)}. Then $p' \inp P/a$, so
$\exists p\inp P.~p\ltrans{a}{N}p'$. In fact, the set of all $p\inp P$
with \plat{p\ltrans{a}{N}p'} is ordered by $\smin$, and we take a
$\smin$-maximal $p$ within that set.
Suppose, towards a contradiction, that $\exists q\inp P.~q \neq p
\wedge p\smin q$. Take that $q$. Then, by definition of simulation,
\plat{\exists q'\inp \N{S}.~q\ltrans{a}{N}q' \wedge p'\smin q'},
so $q'\inp P/a$. By construction, $q'\neq p'$.
Hence \plat{p'\mathbin{\not\in} \compression{\ssmin}(P/a)}.
So $\nexists q\inp P.~q\neq p \wedge p\smin q$, and thus $p \inp \compression{\ssmin}(P)$.
Hence $p' \inp \compression{\ssmin}(P)/ a$.
\\[1ex]
Ad 3. By Lemma~\ref{crux}.2 we have\\[1ex]
$\compression{\ssmin}(P/a)\mathbin=
\compression{\ssmin}(\compression{\ssmin}(P/a))
\mathbin\subseteq
\compression{\ssmin}(\compression{\ssmin}(P)/a)$.\\[1ex]
On the other hand, $\compression{\ssmin}(P) \subseteq P$ (by Definition~\ref{def:compr})
so $\compression{\ssmin}(P)/ a \subseteq P/a$ and thus
$\compression{\ssmin}(\compression{\ssmin}(P)/ a) \subseteq \compression{\ssmin}(P/a)$.
\pagebreak[2]
\\[1ex]
Ad 4. Let \plat{p' \in \closure{\ssmin}(P)/a}.
Then \plat{\exists p\inp \closure{\ssmin}(P).~p\ltrans{a}{N}p'}. Take that $p$.
So $p \smin P$.
Hence, $\exists q,q' \inp\N{S}~.~q \inp P \wedge q \ltrans{a}{N} q'
\wedge p' \smin q'$. Therefore, $q'\inp P/a$ and $p' \inp \closure{\ssmin}(P/a)$.
(In the latter step we use that if $p \smin q$ and $q \inp Q$ then
surely $p \smin Q$.)
\\[1ex]
Ad 5. By Lemma~\ref{crux}.4 we have\\[1ex]
\centerline{$\closure{\ssmin}(P/a)\mathbin=
\closure{\ssmin}(\closure{\ssmin}(P/a))
\mathbin\supseteq
\closure{\ssmin}(\closure{\ssmin}(P)/a)$.}\\[1ex]
Moreover, $\closure{\ssmin}(P) \supseteq P$
so $\closure{\ssmin}(P)/ a \supseteq P/a$ and thus
$\closure{\ssmin}(\closure{\ssmin}(P)/ a) \supseteq \closure{\ssmin}(P/a)$.
\\[1ex]
Ad 6. As \plat{\compression{\ssmin}(P)\subseteq P} we have 
\plat{\closure{\ssmin}(\compression{\ssmin}(P)) \subseteq \closure{\ssmin}(P)}.
\\
For the other direction, note that $p \inp P$ implies \plat{\exists
q\inp\compression{\ssmin}(P)~.~p \smin q}. From this it easily follows
that $p \smin P$ implies \plat{p \smin\compression{\ssmin}(P)}, which in
turn yields \plat{\closure{\ssmin}(P) \subseteq \closure{\ssmin}(\compression{\ssmin}(P))}.
\\[1ex]
Ad 7. This can be restated as $p \smin P \Leftrightarrow p \smin
\tuple{P}$, which follows directly from the definitions.
\\[1ex]
Ad 8. $\ms{fin}(\compression{\ssmin}(\tuple{\closure{\ssmin}(P)}))\mathbin=
\ms{fin}(\tuple{\closure{\ssmin}(P)})\mathbin=
\exists{p\mathbin{\smin}\! P}.~ p \inp \N{F}\linebreak=
\exists{q\inp P}.~ q \inp \N{F}=
\ms{fin}(\tuple{P})=
\ms{fin}(\compression{\ssmin}(\tuple{P}))$.

Furthermore,
$\ms{set}(\compression{\ssmin}(\tuple{P})) \subseteq
 \ms{set}(\compression{\ssmin}(\tuple{\closure{\ssmin}(P)}))$,\vspace{-1pt}
because $P \subseteq \closure{\ssmin}(P)$.
Finally, take $(a,p') \inp \ms{set}(\tuple{\closure{\ssmin}(P)})\setminus \ms{set}(\tuple{P})$.\vspace{-3pt}
Then $p\ltrans{a}{N}p'$ for some $p \smin P$.
Hence $\exists q,q' \inp \N{S} .\; q \inp P \land
    q \ltrans{a}{N} q' \,\land\, p' \smin q'$.
Therefore $(a,q')\inp \ms{set}(\tuple{P})$, so $(a,p')\neq(a,q')$, and $(a,p')\smin (a,q')$,
from which we obtain \plat{(a,p')\not\in
\ms{set}(\compression{\ssmin}(\tuple{\closure{\ssmin}(P)}))} by Definition~\ref{def:compr}.
This implies that $\ms{set}(\compression{\ssmin}(\tuple{\closure{\ssmin}(P)}))
\subseteq \ms{set}(\compression{\ssmin}(\tuple{P}))$.
\qed\end{proof}

\begin{theorem}
$\Transset \preceq\Subset$.
\end{theorem}

\begin{proof}
A straightforward induction on (\ref{induction}), using
Lemma~\ref{crux}.1 at the induction step, yields
\begin{equation}
S_{\mc{D}(\Transset)} = \{\tuple{P} \mid P \in S_{\mc{D}(\Subset)}\}.
\label{trans-sub}
\end{equation}
This immediately implies that
$|S_{\mc{D}(\Transset)}| \leq |S_{\mc{D}(\Subset)}|$. (Note that we do
need not have an equality here, because if might be that
$\tuple{P}=\tuple{Q}$ for different $P,Q \in S_{\mc{D}(\Subset)}$.)\,
Hence $\Transset \preceq \Subset$.
\qed\end{proof}

\begin{theorem}
$\SubsetCompsim \preceq\Subset$.
\end{theorem}

\begin{proof}
A straightforward induction on (\ref{induction}), using
Lemma~\ref{crux}.3 at the induction step, yields
\begin{equation}
S_{\mc{D}(\SubsetCompsim)} = \{\compression{\ssmin}(P) \mid P \in S_{\mc{D}(\Subset)}\}.
\label{comp-idty}
\end{equation}
Hence $|S_{\mc{D}(\SubsetCompsim)}| \leq |S_{\mc{D}(\Subset)}|$, from
which the theorem follows.
\qed\end{proof}

\begin{theorem}
$\SubsetClossim \preceq\SubsetCompsim$.
\end{theorem}

\begin{proof}
By a similar induction as in the previous proof, this time using
Lemma~\ref{crux}.5, we obtain
\begin{equation}
S_{\mc{D}(\SubsetClossim)} = \{\closure{\ssmin}(P) \mid P \in S_{\mc{D}(\Subset)}\}.
\label{clos-idty}
\end{equation}
In combination with (\ref{comp-idty}) and Lemma~\ref{crux}.6 this yields
\[
\begin{array}[t]{c@{~}l}
S_{\mc{D}(\SubsetClossim)}
&\stackrel{(\ref{clos-idty})}{=}
 \{\closure{\ssmin}(P) \mid P \in S_{\mc{D}(\Subset)}\}\\
&\stackrel{\ref{crux}.6}{=}
 \{\closure{\ssmin}(\compression{\ssmin}((P)) \mid P \in S_{\mc{D}(\Subset)}\}\\
&\stackrel{(\ref{comp-idty})}{=}
 \{\closure{\ssmin}(P) \mid P \in S_{\mc{D}(\SubsetCompsim)}\}\,.
\end{array}
\]
Hence $|S_{\mc{D}(\SubsetCompsim)}| \leq |S_{\mc{D}(\SubsetCompsim)}|$.
\qed\end{proof}

\noindent
In the following lemma, whose proof is similar to the previous one, we
employ a relation $\subseteq$ between transition tuples defined by
$(T,b) \subseteq (T',b')$ iff $T \subseteq T'$ and $b \imp b'$.

\begin{lemma}\label{crux-transset}
Let $\mc{N}$ be an NFA, $a\inp\N{\Sigma}$ and $P$ a transition tuple. Then
\begin{itemize}
\item[\rm 1.] \plat{\compression{\ssmin}(P\mathord\sslash a) \subseteq \compression{\ssmin}(P)\mathord\sslash  a)},
\item[\rm 2.] \plat{\compression{\ssmin}(\compression{\ssmin}(P)\mathord\sslash  a) = \compression{\ssmin}(P\mathord\sslash a)},
\item[\rm 3.] \plat{\closure{\ssmin}(P) = \closure{\ssmin}(\compression{\ssmin}(P))}.
\qed
\end{itemize}
\end{lemma}

\begin{theorem}
$\TranssetCompsim \preceq\Transset$.
\end{theorem}

\begin{proof}
A straightforward induction using Lemma~\ref{crux-transset}.2, yields
\begin{equation}
S_{\mc{D}(\TranssetCompsim)} = \{\compression{\ssmin}(P) \mid P \in S_{\mc{D}(\Transset)}\}.
\label{comp-idty-trans}
\end{equation}
Hence $|S_{\mc{D}(\TranssetCompsim)}| \leq |S_{\mc{D}(\Transset)}|$.
\qed\end{proof}

\begin{theorem}
$\TranssetCompsim \preceq\SubsetClossim$.
\end{theorem}

\begin{proof}
From (\ref{trans-sub}), (\ref{clos-idty}), (\ref{comp-idty-trans}) and Lemma~\ref{crux}.8 we obtain
\[
\begin{array}[t]{c@{~}l}
S_{\mc{D}(\TranssetCompsim)}
&\stackrel{(\ref{comp-idty-trans})}{=}
 \{\compression{\ssmin}(P) \mid P \in S_{\mc{D}(\Transset)}\}\\
&\stackrel{(\ref{trans-sub})}{=}
 \{\compression{\ssmin}(\tuple{P}) \mid P \in S_{\mc{D}(\Subset)}\}\\
&\stackrel{\ref{crux}.8}{=}
 \{\compression{\ssmin}(\tuple{\closure{\ssmin}(P)}) \mid P \in S_{\mc{D}(\Subset)}\}\\
&\stackrel{(\ref{clos-idty})}{=}
 \{\compression{\ssmin}(\tuple{P}) \mid P \in S_{\mc{D}(\SubsetClossim)}\}\,.\\
\end{array}
\]
Hence $|S_{\mc{D}(\TranssetCompsim)}| \leq |S_{\mc{D}(\SubsetClossim)}|$.
\qed\end{proof}

\begin{theorem}
$\SubsetClossim \preceq \TranssetCompsim$.
\end{theorem}

\begin{proof}
From (\ref{trans-sub}), (\ref{clos-idty}), (\ref{comp-idty-trans}) and
Lemmas~\ref{crux}.7 and~\ref{crux-transset}.3 we obtain
\[
\begin{array}[t]{c@{~}l}
S_{\mc{D}(\SubsetClossim)}
&\stackrel{(\ref{clos-idty})}{=}
 \{\closure{\ssmin}(P) \mid P \in S_{\mc{D}(\Subset)}\}\\
&\stackrel{\ref{crux}.7}{=}
 \{\closure{\ssmin}(\tuple{P}) \mid P \in S_{\mc{D}(\Subset)}\}\\
&\stackrel{(\ref{trans-sub})}{=}
 \{\closure{\ssmin}(P) \mid P \in S_{\mc{D}(\Transset)}\}\\
&\stackrel{\ref{crux-transset}.3}{=}
 \{\closure{\ssmin}(\compression{\ssmin}(P)) \mid P \in S_{\mc{D}(\Transset)}\}\\
&\stackrel{(\ref{comp-idty-trans})}{=}
 \{\closure{\ssmin}(P) \mid P \in S_{\mc{D}(\TranssetCompsim)}\}\,.
\end{array}
\]
Hence $|S_{\mc{D}(\SubsetClossim)}| \leq
|S_{\mc{D}(\TranssetCompsim)}|$.  \qed\end{proof} By the last two
theorems we have $|S_{\mc{D}(\SubsetClossim)}| =
|S_{\mc{D}(\TranssetCompsim)}|$ for any input NFA $\mc{N}$. Thus, the
surjective function $\closure{\ssmin}$ from
$S_{\mc{D}(\TranssetCompsim)}$ to $S_{\mc{D}(\SubsetClossim)}$
constructed in the last proof must be a bijection. It is not hard to
see that it therefore is an isomorphism.

\section{Plots for random automata}\label{app:random-plots1}

\subsection{DFA Size} \label{app:sizeplots}

\begin{center}
\input{plots/size-10-0_40.tex}
\mbox{}\vspace{-1ex}
\input{plots/size-20-0_40.tex}
\newpage
\input{plots/size-30-0_40.tex}
\mbox{}\vspace{1em}
\input{plots/size-40-0_40.tex}
\vspace{2em}
\input{plots/size-50-0_40.tex}
\vspace{2em}
\input{plots/size-60-0_40.tex}
\vspace{2em}
\input{plots/size-70-0_40.tex}
\vspace{2em}
\input{plots/size-80-0_40.tex}
\vspace{2em}
\input{plots/size-90-0_40.tex}
\vspace{2em}
\input{plots/size-100-0_40.tex}
\end{center}

\subsection{Time} \label{app:timeplots}

\begin{center}
\input{plots/time-10-0_40.tex}
\mbox{}\vspace{1em}
\input{plots/time-20-0_40.tex}
\vspace{2em}
\newpage
\input{plots/time-30-0_40.tex}
\mbox{}\vspace{1em}
\input{plots/time-40-0_40.tex}
\vspace{2em}
\input{plots/time-50-0_40.tex}
\vspace{2em}
\input{plots/time-60-0_40.tex}
\vspace{2em}
\input{plots/time-70-0_40.tex}
\vspace{2em}
\input{plots/time-80-0_40.tex}
\vspace{2em}
\input{plots/time-90-0_40.tex}
\vspace{2em}
\input{plots/time-100-0_40.tex}
\end{center}

\subsection{Memory} \label{app:memplots}

\begin{center}
\input{plots/mem-10-0_40.tex}
\mbox{}\vspace{1em}
\input{plots/mem-20-0_40.tex}
\vspace{2em}
\newpage
\input{plots/mem-30-0_40.tex}
\mbox{}\vspace{1em}
\input{plots/mem-40-0_40.tex}
\vspace{2em}
\input{plots/mem-50-0_40.tex}
\vspace{2em}
\input{plots/mem-60-0_40.tex}
\vspace{2em}
\input{plots/mem-70-0_40.tex}
\vspace{2em}
\input{plots/mem-80-0_40.tex}
\vspace{2em}
\input{plots/mem-90-0_40.tex}
\vspace{2em}
\input{plots/mem-100-0_40.tex}
\end{center}

\end{document}
