\documentclass[leqno,runningheads]{llncs}

\usepackage{amssymb,amsmath}
\usepackage{algorithm,algorithmic}
\usepackage{subfigure}
\usepackage{times}
\usepackage{textcomp}
\usepackage{url}
\usepackage{xspace}
\usepackage{graphicx}

\title{Five Determinisation Algorithms}

\author{Rob van Glabbeek\inst{1,2} \and 
Bas Ploeger\inst{3}\thanks{This author is partially supported by the
Netherlands Organisation for Scientific Research (NWO) under VoLTS grant
number 612.065.410.}}

\institute{National ICT Australia, Locked Bag 6016, Sydney, NSW1466, Australia
\and
School of Computer Science and Engineering, The University of New South Wales,\\
Sydney, NSW 2052, Australia 
\and 
Department of Mathematics and Computer Science, Eindhoven University of Technology,\\
P.O.~Box~513, 5600~MB Eindhoven, The Netherlands}

% 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}\!}\xspace}
\newcommand{\SubsetClossim}{\algof{Subset}{\closure{\ssmin}\!}\xspace}
\newcommand{\SubsetCompsim}{\algof{Subset}{\compression{\ssmin}\!}\xspace}
\newcommand{\Transset}{\algof{Transset}{\idty}\xspace}
\newcommand{\Transsetf}{\algof{Transset}{f}\xspace}
\newcommand{\TranssetCompsim}{\algof{Transset}{\compression{\ssmin}\!}\xspace}

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

\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
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\@.
\pagebreak[1]

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 minimisation of DFAs 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}.

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. 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.\vspace{-1pt}

\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:
$$\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, 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 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'\}$;
		\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{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:\linebreak\mbox{}\vspace{-1.2em}

\begin{figure}[h]
\vspace*{-1.3em}
\centering
\subfigure[]{
\label{fig:expblowup}
\includegraphics{ciaa35a}
}

\vspace{-2mm}
\subfigure[]{
\label{fig:expgap}
\includegraphics{ciaa35b}
}
\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}

\noindent
$\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$ this is indeed the case, which we prove in
\cite{GP08b}, the full version of this paper.
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
\includegraphics{ciaa35c}
}
\hspace{10mm}
\subfigure[]{
\centering
\includegraphics{ciaa35d}
}
\hspace{10mm}
\subfigure[]{
\centering
\includegraphics{ciaa35e}
}
\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 \cite{GP08b}.

\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 \cite{GP08b}.
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
\includegraphics{ciaa35f}
\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 \plat{$\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} \plat{$\compression{\ssmin}$} is now properly
defined on sets of transitions and 
it can be extended to transition tuples in a straightforward manner:
\plat{$\compressionf{\ssmin}{T,b} = (\compressionf{\ssmin}{T},b)$}.
\pagebreak[1]

This way, we obtain two more determinisation algorithms:
\plat{\SubsetCompsim} and \TranssetCompsim.
Their correctness proofs can be found in \cite{GP08b}.

\section{Lattice of Algorithms}

Figure~\ref{fig:alglattice} orders the algorithms described in the
previous sections in a lattice: we draw an arrow from algorithm $A$ to
algorithm $B$ iff for every input NFA, $A$ produces a DFA that is at
most as large as the one produced by $B$.  The algorithms
\SubsetClossim and \TranssetCompsim are in the same class of the
lattice, because they always yield isomorphic DFAs.
The relations of Figure~\ref{fig:alglattice} are substantiated in
\cite{GP08b}; Figures~\ref{fig:expgap},~\ref{fig:dettrans}
and~\ref{fig:simexpgap} provide counterexamples against further inclusions.

\begin{figure}
\vspace{-1em}
\centering
\includegraphics{ciaa35g}
\caption{The lattice of algorithms presented in the previous sections.}
\vspace{-2em}
\label{fig:alglattice}
\end{figure}

\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).

For the benchmarks we consider a one-dimensional cellular automaton
(CA) (see \eg \cite{Wol:02}), which is represented by a function $\rho
: \Sigma^w \to \Sigma$ called the \emph{rule} where $\Sigma$ is an
alphabet and $w$ is the \emph{width} of the automaton.  Given an
infinite sequence $\sigma \in \Sigma^\infty$, a \emph{step} of a CA is
an application of $\rho$ to every $w$-length subsequence of $\sigma$,
which produces a new sequence.  The possible finite sequences
appearing as a continuous subsequence of the infinite sequence
obtained after $n$ steps of a given CA (starting from a random input
sequence) constitute a language that can be described by a DFA
\cite{Wol:84}.  It is known that for some CA rules, the size of these
DFAs increases exponentially in $n$ (\textit{cf}.~\cite{Sut:03}).

For $\Sigma = \{0,1\}$ and $w = 3$, the CA with number 110 has the
following rule:
$$
\begin{array}{llllll}
\rho = \{ & 000 \mapsto 0, & 001 \mapsto 1, & 010 \mapsto 1, & 011
\mapsto 1,\\
          & 100 \mapsto 0, & 101 \mapsto 1, & 110 \mapsto 1, & 111
          \mapsto 0 & \}.
\end{array}
$$
It is known to be computationally universal and to exhibit the
exponential blow-up phenomenon described above.
We have generated the minimal DFAs for steps 1 through 5 of this CA
using the various algorithms presented here.
The most interesting results are those for steps 4 and 5, which are
shown in Table~\ref{tab:celaut-benchmarks}.
\begin{table}[t]
  \centering
  \small
  \begin{tabular}{|l|*{10}{r|}}
    \cline{2-11}
    \multicolumn{1}{c}{} & \multicolumn{5}{|c|}{\bf STEP 4} &
    \multicolumn{5}{|c|}{\bf STEP 5}\\
    \cline{2-11}
    \multicolumn{1}{c}{} & \multicolumn{1}{|c|}{\bf DT} &
    \multicolumn{1}{|c|}{\bf MT} & \multicolumn{1}{|c|}{\bf DS} &
    \multicolumn{1}{|c|}{\bf MS} & \multicolumn{1}{|c|}{$|\D{S}|$} &
    \multicolumn{1}{|c|}{\bf DT} &
    \multicolumn{1}{|c|}{\bf MT} & \multicolumn{1}{|c|}{\bf DS} &
    \multicolumn{1}{|c|}{\bf MS} & \multicolumn{1}{|c|}{$|\D{S}|$}\\
    \hline
    \Subset & 0.6 & 0.4 & 5.4 & 2.0 & 58\,370 & 212.5 & 76.7 & 688.2 &
    267.2 & 7\,663\,165\\
    \hline
    \Transset & 1.0 & 0.4 & 9.0 & 2.0 & 58\,094 & 257.3 & 79.1 & 1\,146.9
    & 263.0 & 7\,541\,248\\
    \hline
    \SubsetClossim & 1.6 & $<$ 0.1 & 2.1 & 0.2 & 4\,720 & 2~739.7 & 1.61 &
    123.2 & 6.3 & 176\,008\\
    \hline
    \SubsetCompsim & $<$ 0.1 & $<$ 0.1 & 0.6 & 0.2 & 4\,745 & 4.3 & 1.4 &
    16.7 & 6.4 & 179\,146\\
    \hline
    \TranssetCompsim & $<$ 0.1 & $<$ 0.1 & 0.7 & 0.2 & 4\,720 & 4.1 & 1.6
    & 22.9 & 6.3 & 176\,008\\
    \hline
  \end{tabular}
  \vspace{3mm}
  \caption{Benchmark results for canonising NFAs of steps 4 and 5 of CA
  110.\newline Legend: {\bf D} = Determinisation,
   {\bf M} = Minimisation, {\bf T} = Time (sec), {\bf S} =
    Space (peak memory use, MB), $|\D{S}|$ = Size of DFA after determinisation.}
  \label{tab:celaut-benchmarks}
\end{table}
The input NFA has 228 states for step 4 and 1\,421 for step 5;
the minimal DFAs have sizes 1\,357 and 18\,824 respectively.
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.

\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.
On these examples, the algorithms that use a function to reduce the
computed sets, convincingly outperformed the others.

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 also remark that our optimisations to subset construction are
particularly beneficial in cases where normal subset construction leaves
a large gap between the generated DFA and the minimal one.

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

\bibliographystyle{plain}

\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 {Proceedings of the Symposium on \sl 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 {Proceedings of the Third International Workshop on \sl Computer-Aided Verification}, LNCS 575, Springer, pp. 255--265.

\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 To appear in Proc. 20th Int. Conf. on
  {\sl  Computer Aided Verification}, LNCS, Springer.

\bibitem{GP08b}
{ R.J.~van Glabbeek \& B.~Ploeger} (2008):
\newblock {\em Five Determinisation Algorithms}.
\newblock CS-Report 08-14, Eindhoven University of Technology.

\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 Proceedings 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 Theor.~Comput.~Sci.} 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 {Proceedings of the 12th International Conference on \sl Logic for Programming, Artificial Intelligence, and Reasoning}, 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}

\end{document}
