\section{Experimental Comparisons}
 
It is already a commonplace that theoretical estimates of
space and time complexity for decision diagrams are very loose.
It has been shown \cite{wegener00} that for the majority of
\emph{randomly chosen} functions, the performance of decision
diagrams is very poor. However, the modelling languages used
in formal verification seem to result in functions which have
considerably better than worst-case size. 

So it is necessary to turn to experiments in order to compare
the different representations we have proposed in this paper.
We are interested in space complexity of representations, since
memory bounds force an upper limit on the size of the models
we can reason about; and also in time complexity, since we are
concerned with what reasoning we can perform in reasonable
amounts of time. In this section we will discuss experiments
regarding the space complexity; some results on running-time
will appear in the next section along with the case studies.

Our representations vary along two axes. We can vary the
\emph{number of terminal nodes}: either 2, or equal to the
number of elements in the logic. Independently, we can vary
the \emph{branching factor}, the outdegree of non-terminal nodes:
again, either 2, or equal to the number of elements in the logic.
We will explore the independent effects of these two variables.

Thus we perform two experiments to explore the effects of
these two degrees of variation. In the first experiment, we
will hold the branching factor to the size of the logic, and
vary the number of terminal nodes: thus, in representing a
multiple-valued function, we compare the size of a single MDD
with the (shared) size of a set of MBTDDs.

In the second experiment, we keep the number of terminal nodes
fixed at 2, and explore the effects of varying the internal
branching factor: thus we compare the shared size of a set of MBTDDs
in $n$ variables with the shared size of a set (of the same number
of diagrams) of BDD is in $|\J(\lat)|n$ variables.

JUSTIFY THE SET OF LOGICS WE USE.
\subsection{Preliminaries}

DON'T LIKE THIS MUCH. WANT TO INTRODUCE SOME TERMINOLOGY THOUGH.

\begin{definition}
Let $L$ be a lattice. We call $\bot$ and $\top$ the \emph{crisp elements}
of $L$, and denote them by $\crisp(L)$.
A function $f: L^{n} \rightarrow L$ is \emph{crisp-output} if its only
outputs are $\top$ and $\bot$: that is, $f(L^{n})\subseteq \crisp(L)$.
It is \emph{crisp-input} if only inputs in $\crisp(L)$ can lead
to a non-$\bot$ output: $f(L^{n}\backslash \crisp(L)^n)=\{\bot\}$.
\end{definition}

Intuitively, a crisp-output function behaves like a predicate: the inputs
are either accepted or rejected. A crisp-input function, on the other
hand, is only interested in the inputs which are considered ``clearly
defined'' in some sense: others are ignored.

\begin{definition}
For two quasi-boolean lattices $L$, $L'$, a function $h:L\rightarrow L'$
is a \emph{quasi-boolean lattice morphism} if:
\begin{eqnarray*}
h(x \meet_L y) = h(x) \meet_{L'} h(y) \\
h(x \join_L y) = h(x) \join_{L'} h(y) \\
h(\neg_L x) = \neg_{L'} h(x)  \\
\end{eqnarray*}
It can be shown easily that if $h$ is a quasi-boolean lattice morphism,
then $h(\top_L)=\top_{L'}$ and $h(\bot_L)=\bot_{L'}$. So for any
quasi-boolean lattice $L$ there is a \emph{unique} morphism 
$\alpha_L:{\mathbf 2}\rightarrow L$: $\alpha_L(T)=\top_L$ and
$\alpha_L(F)=\bot_L$. Since $\alpha_L({\mathbf 2}=\crisp(L)$,there
is also an inverse $\alpha_L^{-1}:\crisp(L)\rightarrow {\mathbf 2}$.
Using these two mappings we can embed any two-valued function $f$
into $L$ as follows:

$$f'(x_1, \ldots, x_n) = \left\{
  \begin{array}{ll}
    \alpha_L(f(\alpha_L^{-1}(x_1), \ldots, \alpha_L^{-1}(x_n)))
    \mbox{\; if \;} x_1, \ldots, x_n \in \crisp(L) \\
    \bot \mbox{\; otherwise}
  \end{array}
  \right.$$
\noindent yielding $f:L^{n}\rightarrow L$.
\end{definition}

\subsection{Number of Terminal Nodes}

\subsubsection{Methodology}

We anticipate two principal ways in which multiple-valued models
arise. The first is from \emph{inconsistency}: several classical
models are given which are slightly different from one another,
and they are considered ``views'' of the system. From these views,
a combined model which contains full information about the
disagreements between views can be constructed. For instance, if there
are three views, and a transition between states $s$ and $s'$ is present
in the first and third views, but absent in the second, then in the
combined model the transition from $s$ to $s'$ will have the value
TFT in the logic {\bf 8Bool}. A detailed treatment
of this method can be found in \cite{easterbrook01}.

The second is from \emph{underspecification}. In a fully specified
system, transitions may be present or absent. In an incompletely
specified system, some transitions may be marked simply as ``undecided'';
in which case, the value M from {\bf 3QBool} is used for those
transitions. Finite total orders with more values may be used for
different levels of partiality: for more details see (SPIN paper),
(Spanish paper).

Whether inconsistent or underspecified, multiple-valued models will
not differ radically from classical ones, except in the presence
of some multiple-valued transitions. This suggests a method for
constructing multiple-valued models for performance evaluation:
start with a classical model, and change some of the transition values.
This can be seen to yield models with both disagreement \emph{and}
underspecification: changing a transition from $\top$ to a logic
value with some disagreements (say TFT in {\bf 8Bool}) is equivalent
to changing a subset of the views.

We know that classical models have a module structure: that is, they
are built as products of smaller modules by synchronous or 
asynchronous parallel composition. Disagreement or uncertainty arises
at the level of individual modules. If a single transition is
changed in a \emph{module}, then considering that that transition may
occur in parallel with several other transitions in other modules, that
module-level change may result in a large number of changes to
global transition values. 

With this in mind, we propose the following method for perturbing
to the model. We first embed the BDD for the model into $L$.
Then, we
perform the following operation $n$ times:
\begin{enumerate}
\item Choose a path from the root of the diagram to a terminal node.
\item Change the destination of the path from $\top$ or $\bot$ to some in-between value.
\end{enumerate}
MISLEADING: THE TERMINAL NODE STAYS THE SAME. DON'T WANT TO SPEND TOO
MUCH TIME EXPLAINING THIS, THOUGH, SO THAT INACCURACY MAY STAY UNLESS WE
FIND A BETTER EXPLN.
We refer to this operation as ``adding a disagreement'' WE PROBABLY
SHOULDN'T THOUGH; SINCE USED FOR UNDERSPECIFICATION AS WELL. Each path corresponds
to one or more transitions of the model: it may be more, since if a path
does not contain some variable $x_i$ then $x_i$ may take on any value.


We note that creating a multiple-valued model in this fashion
means that any non-crisp input (where some of the variables
are neither $\top$ nor $\bot$) always yields false. We argue
that this has little impact on our results. WHY? ARRGGH I FORGET
AGAIN! HERE'S A SHOT: we are interested in the effect of the number
of terminal nodes. If we take a crisp function, and embed it in
a logic $L$, there is no difference between the sizes of the MDD and
MBTDD representations. If we take that function, and make some of the
non-crisp inputs yield $\top$ as well, the MDD and MBTDD will remain
the same size, though they will grow.

The second assumption we make is that the number of disputed
transitions -- those whose value is neither $\top$ not $\bot$ --
is small by comparison with the number of transitions in the model.

\subsubsection{Results}

Consider how our multiple-valued models are obtained.
We know that if we embed a boolean model into a higher-valued logic,
its MDD and MBTDD representations will be exactly the same size, since
the join-irreducible representations of the outputs will contain either
all join-irreducibles, or none.

We speculate that, for either implementation, the size will increase
with the number of disagreements, though we are unable to say
precisely how. In order to get a better idea, we choose a range of
numbers of disagreements (from 5 to 100) and plot the average MDD and
MBTDD sizes for each logic and each value.

JUSTIFY THE AVERAGING.

From the results, we are able to see that for both MDDs and MBTDDs,
the curve is concave downwards, which suggests that in the range
of parameters used, the effect of subsequent disagreements gradually
decreases. We can speak, then, of the marginal effect of adding another
disagreement.

However, when we compare the results for MDDs with those for MBTDDs,
we see important differences. First of all, we see that for the
same logic and same number of disagreements, MDDs are slightly smaller than 
MBTDDs. We attempt to explain this phenomenon.

At the outset, before any disagreements are added, each MBTDD for the
model is the same as the MDD, so both representations are the same size.
When a change is made, the MDD will grow in size, as we see. However,
\emph{each} of the MBTDDs will be changed in a different way, resulting
in more nodes being added to the set of MBTDDs than were added to the
single MDD. For instance, suppose we are using {\bf 4Bool} as a logic.
Changing an output of TT to TF means that the TF MBTDD will be changed
while the FT MBTDD stays the same as before: so at the very least, we
know that the root node can no longer be shared.
However, because the difference is small, we believe that
there is still a great deal of sharing between the MBTDDs. NOT STRONG
ENOUGH: NEEDS SOME REPHRASING.

FIGURE ILLUSTRATING HOW MOST SHARING IS PRESERVED.

When we look at the different curves for MDDs, we can see that the size
depends on the size of the logic alone. However, for MBTDDs, this is
not the case. We note that there is a dependency on the number of
join-irreducibles in the logic -- for each possible value (2,3,4,5,15)
we see a ``cluster'' of curves.

EXPLAIN WHY DEPENDENCY ON JOIN-IRREDUCIBLES.
STILL THINKING ABOUT HOW TO PHRASE EXPLANATION.

%It is easy to see that there are cases where the MBTDD representation
%of a function will be smaller than the MDD representation. GIVE ONE.

When we look more closely at the variation in speed of growth of MBTDDs, there
are differences even when the number of join-irreducibles
is the same. We notice that, for a given number $k$ of join-irreducibles,
the FTO of $(k+1)$ elements results in the smallest MBTDDs. This
also requires some explanation, which we shall begin with a concrete example.

%We reason that when a disagreement is added, the marginal
%increase in size of the MBTDD is larger when the disagreement affects
%fewer individual MBTDDs. For an FTO, there is exactly one change from
%$\bot$ that only affects a single MBTDD -- all the others will alter
%more than one. But for the $k^2$-valued boolean logic, there will
%be $k$ changes that only affect a single MBTDD. Thus we expect the
%impact of adding disagreements potentially to be greater.

Consider two logics with the same number of join-irreducibles:
{\bf 3QBool} and {\bf 4FTO}. If we change an output from $\bot$, then
with {\bf 3QBool} there is exactly one possible choice -- M -- dictating
the change of exactly one diagram of the MBTDD. With
{\bf 4FTO}, however, there is an equal choice between TF and FT, so either
of the diagrams may be changed.
NEEDS MORE, BUT THIS IS A PLACEHOLDER.

In order to test our hypothesis about this dependency on structure,
we perform an additional experiment.

Brief summary of experiment: use {\bf 3QBool} and {\bf 4Bool}, but only
use one of the intermediate values (say TF, wlog). They have the same
number of join-irreducibles, and the same structure: so we expect
the results to be close to the same, modulo noise.

FIG: Graph, showing that they are.

\subsection{Branching Factor}

\subsubsection{Methodology}

ROUGH:
Embed model into logic $L$. Represent as (set of) BDD and MBTDD.
Compare size.

Reordering?

\subsubsection{Results}

Analytically: for each MBTDD node, we expect to create between
$\log_2 |L|$ and $2 \log_2 |L| -1$ BDD nodes: so the growth factor
should be in this range, modulo any increases in sharing. This
holds only if the function is crisp-input.

% \section{Comparisons}
% \label{sec:comparisons}
% \subsection{Theoretical Expectations}

% \begin{table}[tb]
% %\vspace{-0.2in}
% \begin{center}
% \begin{tabular}{|c|c|c|}
% \hline
% Operation & MBTDD-based & MDD-based\\% & Ratio \\
% \hline\hline $\cup$ and  $\cap$ &
% $\setsiz{\JI{L}}\times\mbox{MBT}(n)^2$ &
%     $\mbox{MDD}(n)^{2}$ \\
% complement &
%  $\setsiz{\JI{L}}\times\mbox{MBT}(n)$ &
%  $\mbox{MDD}(n)$ \\
% % & $\setsiz{\JI{L}}/B$ \\
% back. image &
% $\setsiz{\JI{L}}\times(\mbox{MBT}(n)+\mbox{MBT}(n)\times\mbox{MBT}(2n))$
% & $\mbox{MDD}(n)+\mbox{MDD}(n)\times\mbox{MDD}(2n)$
% %&  $\frac{\setsiz{\JI{L}}}{B} \times \frac{u+uv/B}{u+uv}
% %   \leq \frac{\setsiz{\JI{L}}}{B}$
% \\
% \hline
% \end{tabular}
% \end{center}
% \vspace{-0.1in}
% %\vspace{-0.2in}
% \caption{Running times for operations on {\mvset}s using MBTDDs
% with $j$-cut encoding vs. MDDs.\label{tab:rt}} \vspace{-0.2in}
% \end{table}

% Here we analyze individual operations of the \mvset library:
% union, intersection, complement
% and backward image.  SEMI-GARBAGE!
% We use a Multiple-Valued Binary Terminal
% Decision Diagram (MBTDD)~\cite{devereux01} to represent each
% $j$-cut, denoting the size of a MBTDD for $n$ variables as
% $\mbox{MBT}(n)$. The running time of each operation on a Kripke
% structure is given in the middle column of Table~\ref{tab:rt},
% where $n = |A|$.  For example, Theorem~\ref{thm:cut-intersect}
% allows us to do a pairwise union of each of $\JI{L}$ $j$-cuts,
% taking $\setsiz{\JI{L}} \times \mbox{MBT}(n)^2$ operations.
% Computation of backward image for each of $\JI{L}$ MBTDDs
% consists of a disjunction ($\mbox{MBT}(n)$ operations) of conjunctions
% (Definition~\ref{defn:reln-img}) between the formula
% ($\mbox{MBT}(n)$) and the transition relation ($\mbox{MBT}(2n)$ operations).


% HERE IS SOME STUFF FROM CONCUR.  NEEDS REDOING!

% In this section, we compare the running time of
% the algorithm in this paper with those of our earlier
% algorithms~\cite{chechik01b,chechik01a}. Since the structure of
% the algorithms does not change, the difference in performance is
% in the cost of the four operations on {\mvset}s:  union,
% intersection, complement and backward reachability.

% In our first multiple-valued model-checker~\cite{chechik01a}, we
% encoded each logic value $x$ as a sequence of $\setsiz{\lat}$
% bits, where bit $x$ was on if $x \in L$, and off
% otherwise. In this paper, we encode a logic value $x$ using a
% bit for each $j\in \JI{L}$, which is on only when $j\below x$.
% It is always better than the encoding in~\cite{chechik01a}, and
% thus all operations are faster.
% %, provided, of course, that the
% %underlying lattice is distributive.
% % and for certain
% %lattices closely approaches the information-theoretic lower
% %bound of $\log_2(\setsiz{\lat})$.

% The right-hand column of Table~\ref{tab:rt} lists the running times
% of the four operations for the MDD-based representation of
% {\mvset}s that we used in~\cite{chechik01b}. We refer to the size
% of an MDD on $n$ variables as $\mbox{MDD}(n)$.  Running times for
% MDD operations are similar to those for MBTDD operations; however,
% for a given {\mvset}, the MBTDDs representing the $j$-cuts are
% usually smaller than an MDD representing the whole {\mvset}.

% We can express the performance improvement of the model-checker in
% this paper in terms of the ratio between the average size of an
% MDD and that of an MBTDD for a given set of $n$ variables, which we
% call $\beta$.  The performance
% improvements for the operations in Table~\ref{tab:rt} are
% $\setsiz{\JI{L}}/\beta^{2}$ for unions and intersections, and at
% most $\setsiz{\JI{L}}/\beta$ for complements and backward images.

% We can then assess the overall improvement by estimating $\beta$
% for different types of problem. In the worst case, an MDD and an
% MBTDD can have the same number of non-terminal nodes, making
% $\beta$ roughly 1; then the algorithm of this paper actually
% results in a slowdown. However, our experience indicates that as
% problems get larger, $\beta$ approaches $\setsiz{\lat}$. This
% improvement is because there are typically more common
% sub-expressions in boolean-terminal diagrams than in their
% multi-terminal counterparts, and thus more possibility for
% sharing.  Preliminary experimental results support this analysis.
% Results in Table~\ref{fig:er} were produced by randomly
% generating a pool of sample functions of a given number of
% variables (3 to 6), and then creating the single MDD and the
% collection of $\setsiz{\JI{L}}$ MBTDDs representing the function,
% and taking the average sizes of the individual decision diagrams
% over the sample. We give this issue a fuller treatment
% elsewhere~\cite{devereux01}. Thus, we believe that there is a
% significant speedup when using the model-checking algorithm
% described in this paper.  For unions and intersections this
% speedup can range from $\setsiz{\lat}$ to as much as
% $\setsiz{\lat}^{2}/\log_2 \setsiz{\lat}$, depending on the shape
% of the lattice.
% \begin{table}[htb]
% \begin{center}
% \input{table}
% \end{center}
% %\vspace{-0.2in}
% \caption{Empirical results, for randomly-generated functions, with
% $L=\latstyle{3x3}$.\label{fig:er}} 
% \end{table}

% \subsection{Experimental Results}

%The running times are given in Table~\ref{tab:rt}.  Let $u$ be the size of
%an MDD in $n$ variables, and $v$ be the size of an MDD in $2n$
%variables (for the transition relation.)    We assume that,  Using this,
%we obtain the ratios in the third column of the table.  In general, we
%require MBTDDs in $n$ variables to be smaller than MDDs, on average,
%by a factor of at least $\setsiz{\JI{L}}$, before any speed-up
%begins to accrue by using the representation of this paper.