\section{Background}
\label{sec:background}
In this section we describe the background for multi-valued model-checking.
We begin the section with discussion of multi-valued logics and then proceed
by discussing \mvset{s} -- data structures for representing and reasoning
about multi-valued sets of entities.  In the case
of multi-valued model-checking, the entities are states and transitions.

\subsection{Quasi-Boolean Logic}
\label{logics} 
Our approach to modeling makes use of an entire
family of multi-valued logics. Rather than giving a complete
axiomatization for each logic, we  give a semantics by
defining conjunction, disjunction and negation on the truth
values of the logic, and restrict ourselves to logics where these
operations are well-defined, and satisfy commutativity,
associativity etc. Such properties can be easily guaranteed if we
require that the truth values of the logic form a lattice.
We describe the types of lattices used in our model-checker.

\begin{figure}[tb]
\begin{center}
\begin{boxedminipage}[htb]{5.5in}
\psfig{figure=lattices.ps,width=5.3in}
\end{boxedminipage}
\caption{\label{fig:alllattices} Some lattices:
(a) \latstyle{2}, the classical logic
lattice; (b) \latstyle{3}, a 3-valued lattice representing 
uncertainty; (c) \latstyle{2x2}, a 4-valued lattice
representing disagreement; (d) Belnap's 4-valued lattice
representing inconsistent information;
(e) a lattice \latstyle{3x3}; (f) a non-quasi-boolean lattice.   Join-irreducible elements are shown in bold.
Lattices in (a)-(e) are quasi-boolean.}
\end{center}
\vspace{-0.2in}
\end{figure}

\begin{definition}
\label{def:lat}
\emph{Lattice} is a partial order (${\cal L}$, $\sqsubseteq$) for
which a unique greatest lower bound 
and least upper bound exist for each finite set of elements.
\end{definition}
Given lattice elements $a$ and $b$, their greatest lower
bound is referred to as \emph{meet} and denoted by $a \sqcap b$,
whereas their least upper bound is referred to as \emph{join}
and denoted by $a \sqcup b$.
Meet and join over an empty set
are
referred to as \emph{top} and \emph{bottom}, respectively:
$$\begin{array}{lcll}
\top & \eqdef & \sqcap \{\} & \; \; \; \mbox{($\top$ definition)}\\
\bot & \eqdef & \sqcup \{\} & \; \; \; \mbox{($\bot$ definition)}
\end{array}$$

Before identifying lattice
properties, we define \emph{equality} over lattice elements:
$$\begin{array}{ll}
a = b \; \eqdef \; a \under b \; \wedge \; b \under a & \; \; \; \mbox{(equality)}
\end{array}$$
%The partial order operation $a \sqsubseteq b$ means
%``$b$ is at least as true as $a$''. 
The following properties hold
for all lattices:
$$\begin{array}{rclrcll}
a \sqcup a & = & a & a \sqcap a & = & a & \; \; \; \mbox{(idempotence)}\\
a \sqcup b & = & b \sqcup a &  a \sqcap b & = & b \sqcap a &
\; \; \; \mbox{(commutativity)}\\
a \sqcup (b \sqcup c) & = & (a \sqcup b) \sqcup c &
\; \; \; a \sqcap (b \sqcap c) & = & (a \sqcap b) \sqcap c &
\; \; \; \mbox{(associativity)}
\end{array}$$
\noindent
Figure~\ref{fig:alllattices} gives examples of a few lattices.
For example, for the lattice \latstyle{2x2} in Figure~\ref{fig:alllattices}(c),
TF $\meet$ FT = FF, whereas TF $\join$ FT = TT.
Note that when the logic is
classical, i.e. represented by the lattice \latstyle{2}, $\meet$ and
$\join$ operations are conventionally referred to as $\wedge$ and $\vee$,
respectively.  We will use these notations interchangeably when the
interpretation is clear from the context.
Further, in the lattices in Figure~\ref{fig:alllattices}(a)-(e) $\top$ is
labeled `T' (or `TT') and $\bot$ is labeled `F' (or `FF'). We adopt
the convention of labeling $\top$ and $\bot$ in this way in all our
lattices, although in principle $\top$ and $\bot$ might be labeled
differently.   

\begin{definition}
A lattice is \emph{distributive} if
$$\begin{array}{rcll}
a \sqcup (b \sqcap c) & = & (a \sqcup b) \sqcap (a \sqcup c) & \; \; \mbox{\emph{(distributivity)}}\\
a \sqcap (b \sqcup c) & = & (a \sqcap b) \sqcup (a \sqcap c) & \\
\end{array}$$
\end{definition}
\noindent All lattices in Figure~\ref{fig:alllattices} are distributive.

%\begin{definition}
%A lattice is \emph{complete} if the least upper bound and the greatest lower bound for
%each subset of elements of the lattice is an element of the lattice.  Every complete
%lattice has a top ($\top$) and a bottom ($\bot$).
%$$\begin{array}{rcll}
%\bot & = & \sqcap {\cal L} & \; \; (\bot \;  \mbox{\emph{characterization}})\\
%\top & = & \sqcup {\cal L} & \; \; (\top \; \mbox{\emph{characterization}})
%\end{array}$$
%\end{definition}
%For example, in the lattices in Figure~\ref{fig:alllattices} $\top$ is
%labeled `T' (or `TT') and $\bot$ is labeled `F' (or `FF'). We adopt
%the convention of labeling $\top$ and $\bot$ in this way in all our
%lattices, although in principle $\top$ and $\bot$ might be labeled
%differently.   Also, we only use lattices that have a finite number of
%elements. Every finite lattice is complete.
In this paper we only use lattices that have a finite number of
elements.

\begin{definition}
\label{qblattice}
A distributive lattice (${\cal L}$, $\sqsubseteq$) is
\emph{quasi-boolean}~\cite{bolc92} (also called \emph{De
  Morgan}~\cite{dunn99}) iff there exists a lattice dual automorphism
with period 2 for it.
\end{definition}

\begin{theorem}
  Let (${\cal L}$, $\sqsubseteq$) be a quasi-boolean lattice, and
  $\neg$ be a lattice dual automorphism with period 2 defined for it.
  Then:
$$\begin{array}{rcllrcll}
\neg(a \sqcap b) & = & \neg a \sqcup \neg b & \; \; {\rm (De \; Morgan)} \; \; &
\neg\neg a  & = & a & \; \; {\rm (\neg \; involution)}\\
\neg(a \sqcup b) & = & \neg a \sqcap \neg b & &
%a = b & \Leftrightarrow & \neg a = \neg b & \; \; {\rm (\neg \; bijective)}\\
a \sqsubseteq b & \Leftrightarrow & \neg a \sqsupseteq \neg b & \; \; {\rm (\neg \; antimonotonic)}\\
%\neg \bot & = & \top & \; \; {\rm (\bot negation)}\\
%\neg \top & = & \bot & \; \; {\rm (\top negation)}\\
\end{array}$$
where $a, b$ are elements of (${\cal L}$, $\sqsubseteq$).  Thus, $\neg
a$ is a \emph{quasi-complement} of $a$.
\end{theorem}
The family of multi-valued logics we use are exactly those logics
whose truth values form a quasi-boolean distributive lattice. 
\begin{definition}
A \emph{quasi-boolean logic} is a triple (${\cal L}$, $\sqsubseteq$, $\neg$),
where: 

\begin{itemize}
\item (${\cal L}$, $\sqsubseteq$) is a distributive quasi-boolean lattice;
\item  Conjunction and disjunction operators are $\meet$ and $\join$
of (${\cal L}$, $\sqsubseteq$); 
\item The partial order operation $a \sqsubseteq b$ means
``$b$ is more true than $a$'';
\item Negation of the logic is the operator $\neg$, a lattice
dual automorphism with period 2.
\end{itemize}
\end{definition}

\noindent
The identification of a suitable
negation operator is greatly simplified by the observation that all
quasi-boolean lattices are symmetric about their horizontal axes.
All lattices in Figure~\ref{fig:alllattices}(a)-(e) exhibit horizontal symmetry
and thus are quasi-boolean, whereas  the lattice in Figure~\ref{fig:alllattices}(f) is not.
The easiest way to define negation is through horizontal symmetry; however,
other ways are also possible.
For example,
in \latstyle{2x2} shown in
Figure~\ref{fig:alllattices}(c), $\neg$TF = FT, $\neg$FT = TF.  However, in
Belnap's 4-valued lattice in Figure~\ref{fig:alllattices}(d), proposed for
reasoning about inconsistent
databases~\cite{belnap77,anderson75},
$\neg$N = N, $\neg$B = B.    Thus, the two lattices are isomorphic,
but the logics defined on them are not.

Finally, we
define additional operators the usual way:
$$\begin{array}{lcll}
a \rightarrow b & \eqdef & \neg a \sqcup b & \; \; \; \mbox{(material implication)}\\
a \leftrightarrow b & \eqdef & (a \rightarrow b) \; \sqcap \; (b \rightarrow a)
& \; \; \; \mbox{(equivalence)}
\end{array}$$

Before proceeding, we review the concept of join-irreducilibity
for distributive lattices.

\begin{definition}\cite{davey90}
\label{defn:join-irreducible}
An element \( j \) in \( \lat \) is \emph{join-irreducible} iff $j \neq \bot$
and for any \( x \) and \( y \) in \( \lat \), \( j=x\join y \)
implies \( j=x \) or \( j=y \).  Dually, an element $m$ is
\emph{meet-irreducible} iff $m \neq \top$ and for any $x$ and $y$,
$m = x \meet y$ implies $m=x$ or $m=y$.
\end{definition}

In other words, \( j \) cannot be further decomposed into the
join of other elements in the lattice, and $m$ cannot be further
decomposed into the meet of other elements in the lattice, just as
prime numbers cannot be further factored into the product of
other natural numbers. For example, the join-irreducible elements of the
lattice \latstyle{3x3} in Figure~\ref{fig:alllattices}(e), shown in
bold, are \{MF, TF, FM, FT\}. We denote the sets of all
join-irreducible and meet-irreducible elements of a lattice $L$ by
\( \JI{L} \) and $\MI{L}$, respectively.

Every element of a finite lattice can be
defined as a join of all  join-irreducible elements
below it:
\begin{theorem}\cite{davey90}
\label{thm:join-rep} Let $\ell$ be any element in a lattice
($\lat, \below$). Then $\ell  = \bigjoin \{j \in \JI{L}
\mid j \below \ell\}$.
\end{theorem}

\noindent
For example, in the lattice shown in Figure~\ref{fig:alllattices}(e),
$\mathrm{TT}=\bigjoin \{\mathrm{MF}, \mathrm{TF}, \mathrm{FM},
\mathrm{FT}\}$, $\mathrm{TM}=\bigjoin \{\mathrm{MF}, \mathrm{TF},
\mathrm{FM}\}$, $\mathrm{FF}=\bigjoin \emptyset$, and so on.
Thus, each element of a lattice can be represented uniquely by a subset
of join-irreducibles.
For example,
$\mathrm{TT}= \{\mathrm{MF}, \mathrm{TF}, \mathrm{FM}\}$.


\subsection{Multi-Valued Sets and Relations}
\label{sec:mvset}
Multi-valued model-checking algorithms can be naturally described
using a data structure that encapsulates reasoning about
operations on sets of
states in which a property holds.  Such operations include
union, intersection, complement, and backward image for computing
predecessors.  Given a logic, we can treat these as
operations over multi-valued sets:  sets whose membership functions
are multi-valued.  We define the concept of multi-valued
sets and relations over quasi-boolean logics here.

In classical set theory, a
set is defined by a boolean predicate, also called a {\it
membership function}. Typically, it is written using the {\it set
comprehension notation}: a predicate $P$ defines the set $S\!
=\!\{x \mid P(x) \}$. For instance, if $P = \lambda x \!\in\!
nat \cdot 0 \leq x \leq 10$, then $S$ is the set of all integers
between 0 and 10 inclusive.
If, instead of using a boolean membership function, we allow the
membership function to range over a lattice, we obtain a {\it
multiple-valued} set theory in which it is possible to make
statements like ``element $x$ is more in a set \mvstyle{S} than element
$y$''. We call the resulting sets \emph{\mvset{}s}
and refer
to them using a special font, e.g., $\mvstyle{S}$.

Given a logic $L=(\lat, \below, \neg)$, we define a multiple-valued
set theory relative to it. For an \mvset \mvstyle{S} and a candidate
element $x$, we use $\mvstyle{S}(x)$ to denote the membership degree
of $x$ in \mvstyle{S}. In the classical case, this amounts to
representing a set by its characteristic function.

\begin{figure}[tb]
\begin{center}
\begin{boxedminipage}[b]{3.1in}
\psfig{figure=callee-both.ps,width=2.7in}
\end{boxedminipage}
\end{center}
\vspace{-0.1in}
\caption{\label{fig:callee} 
A merge between two versions of a callee's view of a phone system
(from~\cite{easterbrook01}).}
\end{figure}

\begin{figure}[tb]
\begin{center}
\begin{boxedminipage}[b]{6.4in}
\psfig{figure=mvsetex.ps,width=6.3in}
\end{boxedminipage}
\end{center}
\vspace{-0.1in}
\caption{\label{fig:mill}
(a) The 4-valued set of states reflecting values of ${\tt Connected}$ in
the Callee system; (b) The 4-valued set of states reflecting values of ${\tt Offhook}$; (c) A union of \mvset{s} in (a) and (b); (d) A multiple-valued
complement of the \mvset in (a).} 
\end{figure}

We will illustrate \mvset{s} and other concepts in this
paper using a model reflecting two different views on what
the callee portion of a phone should do.  This example
is from~\cite{easterbrook01}.  SAY MORE ABOUT IT.  
To distinguish between names of states and variables in our
examples, the former are capitalized, so ${\tt DIALTONE}$
is a state, whereas ${\tt Offhook}$ is a variable.
This model
uses the lattice \latstyle{2x2} in Figure~\ref{fig:alllattices}(c)
to represent disagreement.
For example, the value of a transition between states ${\tt CONNECT}$
and ${\tt IDLE}$ is FT, indicating that this transition was
specified in the second model but not in the first.  The models
also disagree on the value of variable ${\tt Connected}$ in state
${\tt RINGTONE}$, which is reflected in the combined model by assigning
it value TF.  By convention of classical state machines, we do not show 
transitions with value FF.  

We can use the lattice \latstyle{2x2} to encode information
about values of variable ${\tt Connected}$ in different
states of the Callee system.  We refer to this \mvset
as $\mv{{\tt Connected}}$.  Each value $\ell$
of \latstyle{2x2} is associated with a
set of states where ${\tt Connected}$ has value $\ell$.  For example,
${\tt Connected}$ is TT in $\{{\tt CONNECT}\}$, TF in $\{{\tt RINGTONE}\}$,
FF in $\{{\tt IDLE}, {\tt DIALTONE}\}$ and FT nowhere.
This \mvset
can be graphically represented as shown in Figure~\ref{fig:mill}(a),
where the structure corresponds to that of the underlying lattice.


We extend some standard set operations to the multiple-valued
case by lifting the lattice meet and join operations, as follows:
$$\begin{array}{rcll}
(\mvstyle{S} \capL \mvstyle{S}')(x) & \eqdef  & (\mvstyle{S}(x) \meet \mvstyle{S}'(x))
       & \; \; \; (\mbox{Multiple-valued intersection}) \\
(\mvstyle{S} \cupL \mvstyle{S}')(x) & \eqdef  & (\mvstyle{S}(x) \join \mvstyle{S}'(x))
       & \; \; \; (\mbox{Multiple-valued union}) 
%S \underL S' & \eqdef & \forall x \cdot (S(x) \under S'(x)) &
%    \; \; \; (\mbox{Set inclusion})\\
%S = S' & \eqdef & \forall x \cdot ( S(x)=S'(x)) &
%    \; \; \; (\mbox{Extensional equality}) 
\end{array}$$

\noindent
For example, in computing the union of \mvset{}s $\mv{{\tt Connected}}$
and $\mv{{\tt Offhook}}$ given in Figure~\ref{fig:mill}(a) and (b),
respectively, we note that in state ${\tt DIALTONE}$, 
${\tt Connected}$ is FF and ${\tt Offhook}$ is TT.  Thus,
$$(\mv{{\tt Connected}} \cupL
\mv{{\tt Offhook}})\bigl( {\tt DIALTONE} \bigr) = \mbox{TT} \sqcup \mbox{FF}
= \mbox{TT}$$ 
The set representing this union is given in Figure~\ref{fig:mill}(c).

We can also extend
the notion of {\it set complement} to the
multiple-valued case, by defining it in terms of the
quasi-complement of $L$, and denoting it with a bar:


$$ \begin{array}{rcll}
\overline{\mvstyle{S}}(x) & \eqdef &  \neg (\mvstyle{S}(x)) &
    \; \; \; (\mbox{Multiple-valued complement}) 
\end{array}$$

\noindent Mv-set $\overline{\mv{{\tt Connected}}}$ is given in Figure~\ref{fig:mill}(d).

We then obtain the expected properties:
$$\begin{array}{rcll}
\overline{\mvstyle{S} \cupL \mvstyle{S}'} & = & \overline{\mvstyle{S}} \capL \overline{\mvstyle{S}'} &
    \; \; \; (\mbox{De Morgan 1}) \\
\overline{\mvstyle{S} \capL \mvstyle{S}'} & = & \overline{\mvstyle{S}} \cupL \overline{\mvstyle{S}'} &
    \; \; \; (\mbox{De Morgan 2}) \\
\mvstyle{S} \underL \mvstyle{S}' & = & \overline{\mvstyle{S}'} \underL \overline{\mvstyle{S}} &
    \; \; \; (\mbox{antimonotonicity})
\end{array}$$

We now define some additional concepts for {\mvset}s that are not
needed in the classical set theory but we will use later in this
paper.

\begin{definition}
\label{defn:mv-derivatives} Support, Core, $\ell$-cut, and
$\ell$-clip of a multi-valued set \mvstyle{S}: 
$$\begin{array}{rcll}
\supp(\mvstyle{S}) & \eqdef & \{x \mid \mvstyle{S}(x) \neq \bot\} & \; \; \mbox{{\rm (Support)}} \\
\core(\mvstyle{S}) & \eqdef & \{x \mid \mvstyle{S}(x)=\top\} & \; \; \mbox{{\rm (Core)}} \\
\cutp{\ell}(\mvstyle{S}) & \eqdef & \{x \mid  \ell \sqsubseteq \mvstyle{S}(x)\}
&
    \; \; \mbox{($\ell${\rm-cut})} \\
\clipp{\ell}(\mvstyle{S}) & \eqdef & \{x \mid  \mvstyle{S}(x) \sqsubseteq
\ell\} &
    \; \; \mbox{($\ell${\rm-clip})} 
\end{array}$$
\end{definition}

\noindent All of these operations create classical sets. Support,
cut, and core are standard concepts from fuzzy set
theory~\cite{zadeh65}; clip is a new operation, which we shall
need to prove a later result. 
For example,
$$\begin{array}{lcl}
\supp(\mv{{\tt Connected}}) & = & \{{\tt CONNECT}, {\tt RINGTONE}\}\\
\core(\mv{{\tt Connected}}) & = & \{{\tt CONNECT}\}\\
\cutp{\mbox{TF}}(\mv{{\tt Connected}}) & = & \{{\tt CONNECT}, {\tt RINGTONE}\}\\
\cutp{\mbox{FT}}(\mv{{\tt Connected}}) & = & \{{\tt CONNECT}\}\\
\clipp{\mbox{TF}}(\mv{{\tt Connected}}) & = & \{{\tt IDLE}, {\tt RINGTONE}, {\tt DIALTONE}\}\\
\clipp{\mbox{FT}}(\mv{{\tt Connected}}) & = & \{{\tt IDLE}, {\tt DIALTONE}\}
\end{array}$$

Following the conventions
of fuzzy set theory, we identify an explicit universe of
discourse $U$, rather than use an undefinable set of all
possible entities.  Mv-sets can be thought of as functions from elements
of $U$ to the underlying logic; therefore,
$U=\cutp{\bot}\!(\mvstyle{S})$. 

Now we extend the concept of degrees of membership in an {\mvset}
to degrees of relatedness of two entities. This concept,
formalized by \emph{multiple-valued relations}, allows us to
define multiple-valued transitions in state machine models.  

\begin{definition}
\label{defn:reln-img} A multiple-valued relation \mvstyle{R} on two
sets $S$ and $T$ is an {\mvset} over $S \times T$.  $S$ and $T$
are referred to as \mvstyle{R}'s \emph{source} and \emph{destination}, respectively.
\end{definition}

\noindent

For example, the multiple-valued relation representing values of
transitions between pairs of states in the Callee system is given in
Figure~\ref{fig:rel}(a).  This relation, referred to as \mvstyle{T}, is over
$S \times S$, where $S$ is the set of all states of the Callee.  


\begin{definition} 
\label{def:forback}
The
\emph{forward image} $\forwimg{\mvstyle{R}}(\mvstyle{Q})$ of an {\mvset} \mvstyle{Q} over $S$
under relation \mvstyle{R} is
$$\forwimg{\mvstyle{R}}(\mvstyle{Q}) \eqdef \lambda t \cdot \bigsqcup_{s \in S} (\mvstyle{Q}(s) \meet \mvstyle{R}(s,t))$$
\noindent The \emph{backward image} $\backimg{\mvstyle{R}}(\mvstyle{Q})$ of an
{\mvset} \mvstyle{Q} over $T$ under relation \mvstyle{R} is
$$\backimg{\mvstyle{R}}(\mvstyle{Q}) \eqdef \lambda s \cdot \bigsqcup_{t \in T} (\mvstyle{Q}(t)\meet \mvstyle{R}(s,t))$$
\end{definition}

\noindent Intuitively, a forward image of an \mvset \mvstyle{Q} over the relation
\mvstyle{R} means computing all elements reachable from \mvstyle{Q} by \mvstyle{R}, where
multi-valued memberships of \mvstyle{R} and \mvstyle{Q} are taken into consideration.
Similarly, a backward image of an \mvset \mvstyle{Q} over \mvstyle{R} is computing
all elements that can reach \mvstyle{Q} by \mvstyle{R}.
Given an {\mvset} over $S$, its forward image under the
relation \mvstyle{R} is an {\mvset} over $T$; likewise, an
{\mvset} over $T$ has an {\mvset} over $S$ as its backward
image. 

\begin{figure}[tb]
\begin{center}
\begin{boxedminipage}[b]{6.3in}
\psfig{figure=rel.ps,width=6.0in}
\end{boxedminipage}
\end{center}
\vspace{-0.1in}
\caption{\label{fig:rel} 
(a) The multiple-valued relation between pairs of states of the Callee system;
(b) Forward image of $\mv{{\tt Connected}}$ over the relation in (a);
(c) Backward image of $\mv{{\tt Connected}}$ over the relation in (a).}
\end{figure}

The forward and the backward images of $\mv{{\tt Connected}}$ (see Figure~\ref{fig:mill}(a)) 
under the multiple-valued relation between states of the Callee system (Figure~\ref{fig:rel}(a))
are shown in Figure~\ref{fig:rel}(b) and (c), respectively.  For example,
in computing forward image of ${\tt IDLE}$, we get
$$\bigsqcup_{s \in S} \mv{{\tt Connected}}(s) \meet \mvstyle{T}(s, {\tt IDLE}) =
(\mbox{FF} \meet \mbox{TT}) \join (\mbox{FF} \meet \mbox{TT}) \join
(\mbox{TT} \meet \mbox{FT}) \join (\mbox{FT} \meet \mbox{TT})  = \mbox{FT}
\join \mbox{TF} = \mbox{TT}$$
When we compute backward image of  ${\tt IDLE}$, we get
$$\bigsqcup_{t \in S} \mv{{\tt Connected}}(t) \meet \mvstyle{T}({\tt IDLE}, t) =
(\mbox{FF} \meet \mbox{TT}) \join (\mbox{FF} \meet \mbox{FF}) \join
(\mbox{TT} \meet \mbox{FF}) \join (\mbox{TF} \meet \mbox{TT})  = \mbox{TF}$$

\begin{theorem}[\cite{chechik01i}]
\label{thm:backimage}
If $L$ = (\{T, F\}, $\sqsubseteq$, $\neg$), i.e., $L$ is
the classical logic, then
\mvstyle{R} becomes a boolean relation, and \mvstyle{Q} becomes a classical set.
\end{theorem}

In this paper we will not use forward image.  It is defined here for symmetry.