Multiple-valued logics provide an interesting
alternative to classical boolean logic for modeling and reasoning
about systems.  By allowing additional truth values,
they support the explicit modeling of uncertainty and
disagreement.  In particular, multiple-valued logics can be applied
to the modeling of software behavior, especially the exploratory
modeling used in the early stage of requirements engineering and
architectural design, to verify properties of models that contain
uncertainty or disagreement.  For these reasons, we are interested
in constructing a symbolic multiple-valued model-checker. We have
identified a useful family of multiple-valued logics whose truth
values form quasi-boolean lattices. The properties of these logics
are described in~\cite{chechik01a}.

Multiple-valued logic also has hardware design applications.
The survey of Dubrova \cite{dubrova99} gives two uses for multiple-valued logic
in circuit design. In the first use, multiple-valued logic is only used
for representation, simulation, and verification of circuits: the underlying
implementation technology will still be standard two-valued logic. However,
there are advantages to grouping binary input and output variables into
single values in a multiple-valued logic. More recently, circuits directly implemented on multi-level digital logic have
also become practical. This is the second use. It has been suggested
that logic with more than two levels will assist in reducing the
number of connections of an integrated circuit.

The work of H\"{a}hnle et al \cite{hahnle93} offers
yet another application of multiple-valued logic in the hardware domain:
switch-level verification of circuits. Switch-level modeling is one level
of abstraction below gate-level modeling: interconnections between
transistors are explicitly modeled, and signal levels other than
on or off are possible. 

Both circuits and state-based system specifications can be
modelled as functions from inputs to outputs, which
are frequently represented by decision diagrams \cite{bryant86}. A
decision diagram is a rooted, directed acyclic graph, whose non-terminal
nodes are labelled with input variables, and whose terminal nodes are
labelled with possible output values: the function is evaluated by
an appropriate traversal of the graph.
These data structures have, in most cases, the useful property of canonicity:
identical functions are represented by the same structure. There is
an extensive literature dealing with decision diagrams for
functions with binary inputs and either binary or numeric-valued outputs;
the survey of Bryant \cite{bryant95} reviews much of this work.

Existing variations of decision diagrams can be divided into two
broad classes: those which change the branching factor of internal
nodes, the number of terminal nodes, and the number of roots, but do
not annotate either nodes or edges with additional information; and
those which do add such annotations.

Variations which add no additional annotation continue to enjoy
the property of canonicity, which remains guaranteed by reducedness
and orderedness. However,
the addition of annotation, particulary edge annotation, often
makes canonicity harder to guarantee: additional conditions may have to be
imposed. Edge-annotated decision diagrams from numeric-valued functions
(such as edge-valued and factored-edge-valued decision diagrams) require

In this paper, we shall review decision diagrams used in representation
of multiple-valued logic functions, and focus in particular on the use
of edge annotation. Influenced by the mod-$p$ decision diagrams of
Sack et al. \cite{sack00}, which give a potentially more efficient
representation for multiple-valued functions (with finite outputs) which
lacks canonicity, we suggest annotating edges with cyclic-shift operators
on the function output range, and give conditions for maintaining
canonicity.

We have implemented this class of decision diagrams, and give
experimental results on the number of nodes they require to represent
some standard benchmarks.