\documentstyle[doublespace]{article}

\include{psfig}
\include{epsf}

\addtolength{\topmargin}{-11mm}
\addtolength{\textwidth}{9mm}
\addtolength{\textheight}{10mm}

\newtheorem{theorem}{Theorem}[section]
\newtheorem{lemma}[theorem]{Lemma}
\newtheorem{proposition}[theorem]{Proposition}
\newtheorem{corollary}[theorem]{Corollary}
\newtheorem{example}{Example}[section]
\newtheorem{definition}{Definition}

\def\EndProof{ \quad \vrule width 1ex height 1ex depth 0pt  }

\newenvironment{proof}{\noindent{\bf Proof}:}{\EndProof}
\newenvironment{conjecture}{\noindent{\bf Conjecture}: \em}{}
\newenvironment{notation}{\noindent{\bf Notation}: \em}{}

\setstretch{1.5}

\begin{document}

\title{\bf Equivalences for Fair Kripke Structures}
\author{Adnan Aziz\thanks{Department of ECE, University of Texas, Austin, TX 78712}
\and Felice Balarin\thanks{Cadence Berkeley Labs, Berkeley CA 94704}
\addtocounter{footnote}{-1}
\and Vigyan Singhal\footnotemark
\and Robert Brayton\thanks{Department of EECS, University of California, Berkeley, CA 94720}
\addtocounter{footnote}{-1}
\and Alberto Sangiovanni-Vincentelli\footnotemark}

\date{}
\maketitle

\newpage

\begin{abstract}

We extend the notion of bisimulation to Kripke structures with fairness.
We define equivalences that preserve fairness and are akin to bisimulation.
Specifically we define an equivalence 
and show that it is  
complete in the sense that it is the coarsest equivalence that preserves
the logic CTL$^{\ast}$ interpreted with respect to the fair paths.
The addition of fairness might cause two Kripke structures,
which can be distinguished by a CTL$^{\ast}$ formula, to become
indistinguishable by any CTL formula.
We define a  weaker equivalence 
that is the weakest equivalence  preserving
CTL interpreted on the fair paths.
As a consequence of our proofs, we also obtain characterizations of states in
the fair structure
in terms of CTL$^{\ast}$ and CTL formulae.

\end{abstract}

\newpage

\section{Introduction}
Branching time propositional temporal logic
has been found very useful in the
automatic verification of concurrent finite-state systems \cite{clarke92}.
Systems are modeled using labeled state transition structures
called Kripke or temporal structures \cite{emerson90}.
Properties are expressed as formulae
from a branching-time temporal logic. 

One of the simplest such logics is
CTL (Computational Tree Logic) described in \cite{clarke86}. While
the problem of model-checking CTL formulae of a Kripke structure is
of polynomial complexity~\cite{emerson90}, CTL suffers in expressiveness.
The richer logic CTL$^{\ast}$, described in \cite{emerson86},
adds the power of linear-time propositional logic to CTL, and
subsumes both CTL and PLTL (Propositional Linear Time Logic).
However, the problem of model-checking becomes PSPACE-complete~\cite{clarke86}.

At the initial stages of top-down verification driven 
design methodologies~\cite{kurshan93}, nondeterminism provides a powerful
mechanism for modeling abstract designs.
However, nondeterminism can introduce too much behavior.
Fairness  is used to restrict analysis to those infinite 
paths in the Kripke structure which satisfy some
specification, which is evaluated over the infinite path.
A major limitation of CTL is that it cannot express correctness
under fairness constraints~\cite{emerson90}. 

The logic FairCTL allows the specification of a 
CTL formula $p$ along with a path formula $\phi$.
The fairness constraint $\phi$ is a pure path formula, specifically a Boolean
combination of the set of infinitary linear-time operators
applied to propositional arguments~\cite[page 1063]{emerson90}. The path
quantifiers in the syntax of the formula 
now range over only those infinite paths which meet
the fairness constraint $\phi$.
In \cite{clarke86}, a more general specification ${\mbox{CTL}}^{\scriptsize \mbox F}$ is allowed,
where the fairness constraints can refer to individual states. Such fine granularity  allows
us to distinguish between two different states which 
cannot be distinguished by any propositional temporal logic formulae.
The notion of fairness used
in our paper is the extension of \cite{emerson90}, where we allow
the infinitary linear-time operators in $\phi$ to refer to state
labels also.
The model-checking problem for FairCTL (and ${\mbox{CTL}}^{\scriptsize \mbox F}$) can be solved in polynomial
time. 

Often, it is more natural to think of the fairness constraints as part
of the system specification, instead of part of the property being verified.
We will refer to Kripke structures with fairness constraints
as fair-Kripke structures,
and the problem of checking a CTL (or CTL$^{\ast}$) formula
on a fair-Kripke structure as the fair--CTL (or fair--CTL$^{\ast}$) model-checking.
Since we allow the fairness constraints to be Boolean combinations of
infinitary linear-time operators applied to {\em state labels}, 
the fair-Kripke structure specification is as powerful as 
any kind of $\omega$-automaton~\cite{safra_thesis}, and in fact 
is essentially a syntactic variant on the theme 
of $\omega$-automata~\cite{thomas90}.


Browne, Clarke and Grumberg~\cite{browne88}
proved that bisimulation equivalence~\cite{milner89} on Kripke structures
is exactly the weakest equivalence that
preserves all CTL and CTL$^{\ast}$ formulae.
In doing so, they constructed CTL
formulae which characterized Kripke structures up to bisimulation
equivalence. 
As a corollary, they showed that
any two Kripke structures which can be distinguished by a CTL$^{\ast}$ formula
can also be distinguished by a CTL formula. 
In this paper, we
solve an open problem proposed in~\cite{browne88}, namely that  of characterizing
fair-Kripke structures up to  equivalence over branching-time temporal logics.

We show that, unlike ordinary Kripke structures,
there exists a pair of fair-Kripke structures which can be distinguished
by a CTL$^{\ast}$ formula, whereas no CTL formula can
distinguish these two. In fact, these two structures are not even
trace equivalent, which is surprising because in the case of ordinary
Kripke structures bisimulation equivalence is the finest equivalence
and trace equivalence is the coarsest equivalence in the
linear-time --- branching-time spectrum \cite{vanglabbeek_thesis}.

Since, for fair-Kripke structures, the notion of equivalence
is different for CTL and CTL$^{\ast}$ formulae, we provide two
different extensions of bisimulation equivalence which deal with
fairness constraints. 
${\cal E}^{fair}$-bisimulation
characterizes states in
fair-Kripke structures with respect to equivalence over CTL formulae,
and 
${\cal E}^{fair{\ast}}$-bisimulation
characterizes states in
fair-Kripke structures with respect to equivalence over CTL$^{\ast}$
formulae. 

The problem of fair--CTL$^{\ast}$ model-checking can be
solved using the algorithm for 
CTL$^{\ast}$ model-checking by
introducing a new atomic proposition for each state in the Kripke structure.
and then transforming the 
formula using these additional atomic propositions~\cite{clarke86}.
However, this means that the characterization of states in Kripke structures for CTL$^{\ast}$
equivalence as shown in~\cite{browne88} does not solve the problem of
characterizing states in {\em fair} Kripke structures,
since the additional atomic propositions result in the ability of CTL to
differentiate {\em all} states.  Again, this is especially
important when one considers fairness constraints as part of
the {\em system} specification.


 

The remainder of this paper is organized as follows: In Section~2 we
give the definitions of fair-Kripke structures and CTL/CTL$^{\ast}$
syntax and semantics on such structures.
In Section~3, the relationship between bisimulation and CTL/CTL$^{\ast}$
model-checking is reviewed. In 
Section~4 we present the definitions of ${\cal E}^{fair{\ast}}$--bisimulation and 
${\cal E}^{fair}$--bisimulation, and prove completeness results for both equivalences.
We conclude in Section~5 with plans for 
future research and applications of our results.



\section{Definitions}

\subsection{Sequences}
A {\em finite sequence} on a set $A$ is a function whose range is $A$ and
domain is a prefix of the set of 
natural numbers, $\omega = \{0,1,2,\ldots\}$.  An {\em infinite sequence}
on $A$ is a function mapping $\omega$ to $A$.  We will denote the finite sequence $\alpha$
by $\langle a_0, a_1, \cdots, a_{n-1}\rangle$; an infinite sequence $\beta$ will be 
written as $\langle b_0, b_1, b_2,\cdots \rangle$.  
Given a sequence $\alpha$ (finite or infinite), we will denote by 
$[\alpha]_k$ the $k$-th element in the sequence, i.e., $\alpha(k)$.
The elements of the range that occur infinitely often in an infinite sequence $\alpha$ will
be denoted by $\mbox{\tt inf}(\alpha)$.

The {\em length} of a finite sequence
is the cardinality of its domain.  Given finite sequences $\alpha_1$ and $\alpha_2$, 
of length $l_{a_1}$ and $l_{a_2}$ respectively,
we define the {\em concatenation} of $\alpha_1$ and $\alpha_2$ to be the sequence $\alpha$
of length $l_{a_1} + l_{a_2}$ taking value $\alpha_1(k)$ when $k < l_{a_1}$, and
$\alpha_2(k - l_{a_1})$, when $ k \geq l_{a_1}$; this will be denoted by $\alpha_1 \cdot \alpha_2$.
The notion of concatenation readily extends to the case where $\alpha_2$ is an infinite sequence.

For a finite nonempty sequence $\alpha$ of length $l_{\alpha}$, we use 
$\alpha^{\omega}$ to denote the infinite sequence which for any
natural number $k$ evaluates to $\alpha_{k \bmod l_{\alpha}}$.
Given any infinite sequence $\alpha$ and natural number $k$, 
the $k$-th prefix of $\alpha$ is the finite sequence $\langle \alpha(0),
\alpha(1),\cdots,\alpha(k-1)\rangle$, and the $k$-th suffix of $\alpha$ is the sequence
$\langle \alpha(k), \alpha(k+1), \alpha(k+2),\cdots \rangle$. Observe that $\alpha$ is the concatenation
of its $k$-th prefix with its $k$-th suffix.


\subsection{Fair Kripke Structures}

A Kripke structure $K$  is a triple $( S,T,{\cal L} ) $, where
\begin{enumerate}
\item $S$ is a finite set of {\em states}.
\item $T \subset S \times S$ is the {\em transition relation}.
\item ${\cal L} : S \rightarrow 2^{AP}$ is the {\em labeling function} and $AP$ is the underlying set
		of {\em atomic propositions}.
\end{enumerate}
The infinite sequence of states $\sigma = \langle  s_0, s_1, s_2, s_3, \cdots \rangle $
is said to be a {\em path} starting at state $s_0$ if for every $k$ we have $T(s_k,s_{k+1})$.

Intuitively, fairness conditions express restrictions on the infinitary behavior 
of the system; a path is said to be {\em fair} if is satisfies the condition.
Various formalisms exist for defining fair paths, e.g., B\"{u}chi (variously
{\em weak} or {\em unconditional}), Streett (variously {\em strong } or
{\em conditional}), 
Rabin, and 
Muller conditions \cite{safra_thesis,thomas90}. 
An important observation is that in all these formalisms,  fairness
of the path is a function of the set of states occurring
infinitely often on the path. 

\begin{definition}
\rm
A {\bf Muller Fairness condition} (MFC) $f$ on Kripke structure $K$ is characterized by a class ${\cal C} = 
\{M_1,M_2,\ldots,M_n\} $ of subsets of $S$; the path $\sigma$ is fair,
if and only if the set of states occurring infinitely often in $\sigma$,
(denoted by  {\tt inf}$(\sigma)$) is an element of  ${\cal C}$.
The sets $M_i$ will be referred to as the {\bf Muller fair} subsets. 
We will use ${\cal F}^{f}_{s_0}$ to denote the set of all paths starting at $s_0$
that satisfy the MFC~$f$.
\end{definition}

Since in all formalisms of fairness it is the case that fairness
of a path is a function of the set of states occurring
infinitely often on the path, 
Muller conditions can express arbitrary constraints on the set of infinitary states.
Thus without loss of generality,
we will restrict our analysis to Kripke structures with Muller fairness conditions,
which will be referred to as {\bf fair-Kripke structures}, denoted by the 4-tuple $(S,T,{\cal L}, f)$.
Also, to simplify analysis we will always assume that every state lies on a fair path.
This is not a serious restriction; note  that under Muller fairness conditions,
one can compute the set of states lying on a fair path by simple strongly connected 
components calculation~\cite{clr90}.




\subsection{CTL/CTL$^{\ast}$ Model Checking on fair-Kripke structures}

There are two types of formulae in CTL and CTL$^{\ast}$: state formulae (which are true or false
in a specific state), and path formulae (which are true or false along a specific path).
Let AP be the set of atomic propositions. A state formula is given by the following syntax:
\begin{enumerate}
\item \underline{a}  if a $\in$ AP.
\item If ${f}_1$ and ${f}_2$ are  state formula, then so are $\neg{f}_1$
and ${f}_1 \vee f_2$.
\item If $g$ is a path formula, then $\exists g$ and $\forall g$ are state formulae.
\end{enumerate}
A path formula is given by the following syntax:
\begin{enumerate}
\item A state formula
\item If $g_1$ and $g_2$ are path formulae, then so are 
$\neg g_1$ and $g_1 \vee g_2$.
\item If $g_1$ and $g_2$ are path formulae, then so are $X g_1$ and $g_1 U g_2$.
\end{enumerate}

CTL$^{\ast}$ is the set of state formulae that are generated by the above rules;
CTL is a subset of CTL$^{\ast}$ in which the path formulae are restricted to be:
\begin{enumerate}
\item If $f_1$ and $f_2$ are state formulae then $X f_1$ and $f_1 U f_2$ are path formulae.
\end{enumerate}
This clause replaces clauses 1--3 from the previous definition of path formula.


Given a fair-Kripke structure $K = (S,R,{\cal L},f)$, 
state and path formulae are interpreted over states and fair paths as defined below. The formulae
$f_1$ and $f_2$ are state formulae, and $g_1$ and $g_2$ are path formulae.

\begin{enumerate}

\item $s_0 \models$  \underline{a} if and only if $a \in {\cal L}(s_0)$

\item $s_0 \models \neg{f_1}$  \mbox{if and only if} $s_0 \not\models {f_1}$, and
			$s_0 \models {f}_1 \vee f_2$ \mbox{if and only if} 
			$s_0 \models {f}_1$ or $s_0 \models {f}_2$

\item 

\begin{enumerate}
\item $s_0 \models \exists g_1$ if and only if there exists a {\bf fair} path  $\pi$
	starting at $s_0$ such that $\pi \models g_1$, and  
\item
	$s_0 \models \forall g_1$ if and only if for all {\bf fair} paths $\pi$
	starting at $s_0$, $\pi \models g_1$
\end{enumerate}

\item $\pi \models f_1$ if and only if $[\pi]_0 \models f_1$

\item $\pi \models \neg g_1$ if and only if $\pi \not\models g_1$, and
		$\pi \models g_1 \vee g_2$ if and only if $\pi \models g_1$ or $\pi \models g_2$

\item 
\begin{enumerate}
\item $\pi \models X g_1$ if and only if $\pi^1 \models g_1$
\item  $\pi \models g_1 U g_2$ if and only if there exists a $k \geq 0$ such that $\pi^k \models g_2$
	and for all $0 \leq j < k, \,\, \pi^j \models g_1$
\end{enumerate}

\end{enumerate}

It will be convenient to denote $k$ concatenations of the next time operator $X$ by $X^k$.
Given a path formula $g_1$, we will use the 
abbreviation $G g_1$ to denote the CTL$^\ast$ path formula
$\neg  (\mbox{\tt TRUE}\, U\, \neg g_1 )$, where {\tt TRUE} is a logical tautology.
It can be shown that the formulae of CTL presented above can be transformed into
logically equivalent formula which use only $\exists X$, $\exists U$, and
$\exists G$ as temporal connectives~\cite{emerson90}.  

\section{Equivalences preserving CTL/CTL$^{\ast}$ }

Let  $K = ( S, T, {\cal L} )$ be a Kripke structure.
An equivalence relation ${\cal E} \subset S \times S$ is said to be a bisimulation on $K$
if the following holds:
\begin{eqnarray}\label{eqn:bisim}
{\cal E}(s,t)     &   \Rightarrow     &   \big({\cal L}(s) = {\cal L}(t)\big) \wedge \nonumber \\
                        &                       &   \,\,\, \forall s' \Big( T(s,s') \rightarrow \exists t' \big( T(t,t') \wedge {\cal E}(s',t')\big)\Big) \wedge \nonumber \\
                        &                       &   \,\,\, \forall t' \Big( T(t,t') \rightarrow \exists s' \big( T(s,s') \wedge {\cal E}(s',t')\big)\Big) 
\end{eqnarray}

Observe:
\begin{enumerate}
\item the identity relation satisfies the above, and 
\item given any two distinct bisimulations ${\cal E}_1$ and ${\cal E}_2$,
their union, i.e., ${\cal E}_1 \cup {\cal E}_2$, is also a bisimulation.
\end{enumerate}
From the above two observations, it follows that there exists a unique maximal
bisimulation, which will be denoted by ${\cal E}^{bis}$.

In the absence of fairness conditions on the paths through the Kripke structure, Browne, Clarke,
and Grumberg prove the following soundness and completeness result~\cite{browne88}:

\begin{theorem}\label{theorem:bisim-CTL}
\rm
Let $K$ be a Kripke structure, and 
and $s$ and $t$ be states from $K$. Then ${\cal E}^{bis}(s,t)$   if and only if there 
is no CTL$^\ast$
formula $\phi$ such that $s\models \phi $ and $t \not\models \phi$.
\end{theorem}

They construct CTL formulae that characterize states and 
structures up to bisimulation equivalence.
As a corollary, they note that states in a Kripke structure that can be differentiated
by a formula of CTL$^\ast$ can also be differentiated by a formula of CTL. 

\section{Equivalences on fair-Kripke structures}
\label{sec-bis}

In the presence of fairness, states that have the same branching structure
may have different infinitary behavior. In the fair-Kripke structure
defined in Figure~\ref{fig:fairdiff},
the Muller fairness condition is $\{U_1, V_1\}$ (shown in the dotted boxes),  and the set
of APs is $\{a,b\}$.
States $s_0$ and $t_0$ have identical finite branching structure,
but state $t_0$ satisfies the CTL formula $ \exists G  a$ (there exists a path  on which
$a$ is always true), while $s_0 \not\models \exists G  a$.

% \begin{figure}
% \centerline{\ \psfig{figure=fairdiff.eps,width=8cm}}
% \caption{\ \label{fig:fairdiff} States that agree on all CTL formulae in the absence of fairness}
% \end{figure}

\begin{figure}[b]
\centerline{\ \epsfbox{fairdiff.eps}}
\caption{\ \label{fig:fairdiff} States that agree on all CTL formulae in the absence of fairness}
\end{figure}


In this section we define two equivalences on the states of fair-Kripke structures.
We prove completeness results with respect to  CTL$^{\ast}$ and
CTL, using arguments analogous to those in~\cite{browne88}.
Essentially, our equivalences incorporate fairness constraints by requiring that states
be equivalent on all fair paths. We show that it suffices to examine a restricted class of paths,
namely the rational paths defined below.

\begin{definition}
\rm
A path $\sigma$ is a {\em rational path} if there 
exist natural numbers $N$ and $M$  such that 
 for every natural number $i$ greater than $N$ it is the case
that $[\sigma]_{N+i} = [\sigma]_{N + (i \bmod M) }$.
Thus rational paths are those which end in a cycle.
\end{definition}

Given an equivalence relation ${\cal E}$ on the state space of a Kripke
structure, we extend it to an equivalence ${\cal E}^{\omega}$ on paths through the
Kripke structure as follows: ${\cal E}^{\omega}(\sigma, \tau)$ holds exactly when 
for every natural number $i$, we have ${\cal E}([\sigma]_i , [\tau]_i)$.
In the sequel, we will overload ${\cal E}$ and use it when we mean ${\cal E}^{\omega}$;
we will refer to $\sigma$ and $\tau$ as being ${\cal E}$-equivalent.

\subsection{Equivalences preserving CTL$^\ast$ on fair-Kripke structures}

\begin{definition}\label{defn:fairbisim}
\rm
Let $K$ be a fair-Kripke structure $(S,T,{\cal L},f)$.
An equivalence relation  ${\cal E} \subset S \times S$ is said to be a
$fair\ast$ bisimulation if for any $(s,t) \in {\cal E}$ the following are true:
\begin{enumerate}
\item $\big( {\cal L}(s) = {\cal L}(t) \big)$, and 
\item for every fair rational path $\sigma$  starting at $s$
               there exists a fair rational path $\tau$  starting at $t$ such that
                                                ${\cal E}(\sigma, \tau)$, and
\item for every fair rational path $\tau$  starting at $t$
               there exists a fair rational path $\sigma$  starting at $s$ such that
                                                ${\cal E}(\tau, \sigma)$.
\end{enumerate}
The relation ${\cal E}^{fair{\ast}}$ is defined to be 
the coarsest relation that is a $fair\ast$ bisimulation.
\end{definition}

The soundness of this definition follows in a manner analogous 
to that of the definition of ${\cal E}^{bis}$,  as given in 
Section~\ref{sec-bis}.

%%%%%%

At first glance, the definition of ${\cal E}^{fair{\ast}}$ appears unnatural in that it restricts
the paths $\sigma$ and $\tau$ to be rational.  However, we will later prove (cf.~Lemma~\ref{lemma:simple})
that if we drop the requirement of rationality, the resulting equivalence relation
is equal to ${\cal E}^{fair{\ast}}$ given in Definition~\ref{defn:fairbisim}.
Note that under the assumption that every state lies on a fair path, the ${\cal E}^{fair{\ast}}$
relation is finer than bisimulation.

The ${\cal E}^{fair{\ast}}$-bisimilarity relation is the natural extension
to bisimulation in the presence of fairness in the sense that 
the following soundness and completeness result holds:

\begin{theorem}\label{thm:CTLstar}
\rm
Let $s$ and $t$ be states in  a fair-Kripke structure $K = ( S,T,{\cal L}, f)$. 
Then ${\cal E}^{fair\ast}(s,t)$ if and only if there is no CTL$^{\ast}$
formula   $\phi$ such that $s\models \phi$ and $t\not\models \phi$.
\end{theorem}


\begin{proof}
\rm
Proving soundness, i.e., that 
${\cal E}^{fair\ast}(s,t) \Rightarrow$ for every CTL$^{\ast}$ formula $\phi$ we have
$s \models \phi$ if and only if $ t \models \phi$ is straightforward;
simply use induction on the length of the CTL$^{\ast}$ formulae.

To show completeness, i.e., that  $\neg{\cal E}^{fair\ast}(s,t) \Rightarrow$ there
exists a formula $\phi$ of CTL$^{\ast}$ such that $s \models \phi \,\, \wedge
 \,\, t \not\models \phi$, we  first define a series of equivalence relations
$E_0,E_1,\ldots$ as follows:

\begin{enumerate}
\item $E_0(s,t)$ if and only if ${\cal L}(s) = {\cal L}(t)$.
\item $E_{k+1}(s,t)$ if and only if
\begin{enumerate}
\item for every fair rational path $ \sigma $ starting at $s$
there is a fair rational path $\tau $ starting at $t$  which is $E_k$-equivalent to $\sigma$, and
\item for every fair rational path $ \tau $ starting at $t$
there is a fair rational path $\sigma $ starting at $s$  which is $E_k$-equivalent to $\tau$.
\end{enumerate}
\end{enumerate}

Observe that $E_{l+1}(s,t) \subseteq E_{l}(s,t)$.
Also every equivalence in the sequence
contains the equality relation. Since the state 
space is finite, the sequence converges to a fixed point
in some finite number of steps, i.e., there is some $k$ such that $E_{k+1} = E_{k}$,
which we will refer to as $E_{\infty}$.

Note that $E_{\infty}$ satisfies Conditions~1--3 of Definition~\ref{defn:fairbisim}, 
and hence $E_{\infty}$
must lie in ${\cal E}^{fair\ast}$, since by definition, ${\cal E}^{fair\ast}$ is the coarsest
relation satisfying these conditions.  Thus, if we show that states which are 
not $E_{\infty}$-equivalent can be differentiated by CTL$^{\ast}$ formulae, we will have
shown that states which are not ${\cal E}^{fair\ast}$-equivalent can be 
differentiated by CTL$^{\ast}$ formulae.


We now characterize states up to $E_l$-equivalence by CTL$^{\ast}$-equivalence.
This is done by induction on $l$. Specifically we will prove that 
\begin{enumerate}
\item If $\neg\big(E_l(s,t)\big)$ then there is a CTL$^{\ast}$ formula 
$d_l(s,t)$ such that for each state $v$ which is $E_l$-equivalent to $s$ we have
$v \models d_l(s,t)$, and $t \not\models d_l(s,t)$.
\item For every state $s$, there is a 
CTL$^{\ast}$ formula $C_l(s)$ such that for every state
$t$  we have $t \models C_l(s)$  if and only if $E_l(s,t)$.
\end{enumerate}

The formula $d_l(s,t)$ 
distinguishes between $t$ and  states  $E_l$-equivalent to $s$;
the formula $C_l(s)$ characterizes $E_l$-equivalence
to state $s$ within the fair-Kripke structure.

If we let $C_l(s)$ be the conjunction of $C_{l-1}(s)$ and $d_l(s,t)$ for every $t$ which is not
$E_l$-related to $s$, the second assertion follows immediately. Now it is necessary to show how 
to construct $d_l(s,t)$ by induction on $l$.

{\bf Base Case:}$(l=0)$\\
Let $\{p_i\}$ be the set of atomic propositions in ${\cal L}(s)$ and $\{q_j\}$ be the
set of atomic propositions in $\mbox{AP} - {\cal L}(s)$. Now let 
$d_0(s,t)  = {\bigwedge}_{i} \underline{p_i} \wedge {\bigwedge}_{j} \neg \underline{q_j}$. It is clear that
this formula is only true in states with exactly the same labeling as $s$.
Thus the base case is established.

{\bf Induction Hypothesis (IH):}\\
Assume the result is true for $l$. We will show it for $l+1$.

Let $s$ and $t$ be any states in the structure such that $\neg \big( E_{l+1}(s,t) \big)$. 
This can only happen
if there is a fair rational path from  $s$ for which there is no $E_l$-corresponding fair rational path out
of $t$, or there is a fair rational path from $t$ for which there is no $E_l$-corresponding fair rational path out
of $s$. In the latter case, we will use the argument below to find a $d_{l+1}(t,s)$ such that 
$t \models d_{l+1}(t,s)$ and $s \not\models d_{l+1}(t,s)$. We can negate this formula
to obtain the desired $d_{l+1}(s,t).$

Let $\sigma = \langle s_0, s_1, s_2, \cdots, s_{N-1}\rangle \cdot \langle s_{N}, \cdots, 
s_{N+k-1}\rangle^{\omega}$ 
be a fair rational path from $s$ with no corresponding path from $t$,
where we take $s_0 = s$ for notational convenience. 

First define the CTL$^{\ast}$ path formulae $\mbox{\tt stem}_{l+1}(s,t)$ to be
\begin{eqnarray*}
\mbox{\tt stem}_{l+1}(s,t) & = &  C_l(s_0) \, \wedge  \, X C_l(s_{1}) \wedge X^{2} C_l(s_{2}) \wedge \, 
\cdots  \, \wedge X^{N-1} C_l(s_{N-1})
\end{eqnarray*}
Now define the  path formula $\mbox{\tt cycle}_{l+1}(s,t)$ to be
\begin{eqnarray*}
\mbox{\tt cycle}_{l+1}(s,t) & = & C_l(s_N) \, \wedge  \, X C_l(s_{N+1}) \wedge X^{2} C_l(s_{N+2}) \wedge \, 
\cdots  \, \wedge X^{k-1} C_l(s_{N+k-1}) 
\end{eqnarray*}
Then  define the CTL$^{\ast}$ path formulae $\mbox{\tt repeat}^{i}_{l+1}(s,t)$ for 
$i \in \{0,1,\ldots,k-1\}$ to be
\begin{eqnarray*}
\mbox{\tt repeat}^{i}_{l+1}(s,t) & = & \big( C_l(s_{N+i})  \rightarrow X^{k} C_l(s_{N+i}) \big)
\end{eqnarray*}
Finally, define the path formula $\mbox{\tt path}_{l+1}(s,t)$ to be
\begin{eqnarray*}
\mbox{\tt path}_{l+1}(s,t) & = &   \mbox{\tt stem}_{l+1}(s,t) \; \; \wedge \\
		&  &   X^N \big ( \mbox{\tt cycle}_{l+1}(s,t) \big)\; \;  \wedge  \\
		&  &   X^N \bigg ( G \Big ( \bigwedge_{i=0}^{k-1} \mbox{\tt repeat}^{i}_{l+1}(s,t)  
					\Big ) \bigg )
\end{eqnarray*}
%%%%%%%

%% OLD First define the CTL$^{\ast}$ formulae $\mbox{\tt cycle}^{i}_{l+1}(s,t)$, for
%% OLD $i \in \{1,\ldots,k\}$
%% OLD \begin{eqnarray*}
%% OLD \mbox{\tt cycle}^{i}_{l+1}(s,t) & = & ( C_{l}(s_{N+1+(i-1) \bmod k}) \wedge X (C_{l}(s_{N+1+(i) \bmod k}) \wedge X ( C_{l}(s_{N+1+(i+1) \bmod k} ) \\
%% OLD 			&	&	\,\,\,\cdots \,\,\, X C_{l}(s_{N+1+(i+k-2)\bmod k} )) \cdots )
%% OLD \end{eqnarray*}
%% OLD Let $\mbox{\tt cycle}_{l+1}(s,t)$ be the path formula given below:
%% OLD \begin{eqnarray*}
%% OLD \mbox{\tt cycle}_{l+1}(s,t)    & = & \mbox{\tt cycle}^{1}_{l+1}(s,t) \,\, \vee \,\, \mbox{\tt cycle}^{2}_{l+1}(s,t)  \,\, \ldots \,\, \mbox{\tt cycle}^{k}_{l+1}(s,t) 
%% OLD \end{eqnarray*}
%% OLD A path will model $\mbox{\tt cycle}_{l+1}(s,t)$ if and only if the $k$-th   prefix of 
%% OLD the path is $E_{l}$-equivalent to  a cyclic permutation of the $k$-th   prefix of $\sigma$.

%% OLD Now define $\mbox{\tt path}_{l+1}(s,t)$ as below:
%% OLD \begin{eqnarray*}
%% OLD \mbox{\tt path}_{l+1}(s,t)	& = & ( C_{l}(s_1) \wedge X ( C_{l}( s_2) \wedge X ( C_{l}(s_3) \wedge \cdots X ( C_{l}(s_{N}) \wedge \\
			%% OLD &	&	\,\,\, [ X C_{l}(s_{N+1} )\wedge X ( C_{l}(s_{N+2}) \ldots X ( C_{l}(s_{N+k})) ] \wedge \\
			%% OLD &	&	\,\,\, [X\,G\, (\mbox{\tt cycle}_{l+1}(s,t))] )\cdots )
%% OLD \end{eqnarray*}

\begin{proposition}
\rm
A path $\upsilon$ satisfies the path formula $\mbox{\tt path}_{l+1}(s,t)$ if and only if
it is $E_l$-equivalent to the path~$\sigma$.
\end{proposition}

\begin{proof}
The ``if'' part is straightforward; the $E_l$-equivalent fair path will satisfy 
$\mbox{\tt path}_{l+1}(s,t)$.

We now prove the ``only if'' part.
Observe that states $[\upsilon]_0, [\upsilon]_1, \ldots, [\upsilon]_{N-1}$
must satisfy $C_l(s_0), C_l(s_{1}), \ldots, C_l(s_{N-1})$ respectively. By the
IH, any state satisfying $C_l(u)$ must be $E_l$-equivalent to $u$.
Hence, the $N$-th prefix of $\upsilon$ is $E_l$-equivalent to the $N$-th prefix of $\sigma$.

Now consider the $N$-th suffix of $\upsilon$.  Again, by construction of $\mbox{\tt cycle}_{l+1}(s,t)$,
the states $[\upsilon]_N, [\upsilon]_{N+1}, \ldots, [\upsilon]_{N+k-1}$ must satisfy
$C_l(s_N),  C_l(s_{N+1}), \ldots, C_l(s_{N+k-1})$ respectively.  Again invoking the IH, we see
that states $[\upsilon]_N, [\upsilon]_{N+1}, \ldots, [\upsilon]_{N+k-1}$ are $E_l$-equivalent to 
$[\sigma]_N, [\sigma]_{N+1}, \ldots, [\sigma]_{N+k-1}$ respectively.  

Since $\upsilon^N$ satisfies $G \Big ( \bigwedge_{i=0}^{k-1} \mbox{\tt repeat}^{i}_{l+1}(s,t)  
                                        \Big )$, we see that 
for each $i \in \{0,1,\ldots,k-1\}$, we have $[\upsilon]_{N+i}$ satisfies 
$\mbox{\tt repeat}^{i}_{l+1}(s,t)$. 
Hence by the IH, all states of the form 
$[\upsilon]_{N+i+\lambda \cdot k}$, where $\lambda$ is an arbitrary natural number, 
are $E_l$-equivalent.  Thus $N$-th suffix of $\upsilon$ is $E_l$-equivalent to the 
$N$-th suffix of  of $\sigma$.
This proves the proposition.
\end{proof}

Now define $d_{l+1}(s,t)$ to be the state formula  $\exists \,\mbox{\tt path}_{l+1}(s,t)$.
Clearly, the state $s$ satisfies $d_{l+1}(s,t)$ (take $\sigma$ to be the witness),  
as does any state $E_l$-equivalent to $s$ (since $E_l$-equivalence implies the existence
of a path $E_l$-equivalent to $\sigma$). Furthermore, since there does not exist a 
path from $t$ which is $E_l$-equivalent to $\sigma$, 
$t$ does not satisfy $d_{l+1}(s,t)$.
\end{proof}

In Definition~\ref{defn:fairbisim}, states were taken to be equivalent
over rational fair paths. The following lemma demonstrates that equivalence over
rational fair paths implies equivalence over {\em all} fair paths, establishing
a more intuitive characterization of ${\cal E}^{fair\ast}$-bisimulation.

\begin{lemma}\label{lemma:simple}
\rm
Let $K$ be a given fair-Kripke structure. Let ${\cal E}$ be an equivalence
relation on states satisfying the following:
\begin{eqnarray*}
{\cal E}(s, t ) & \Leftrightarrow & \big( {\cal L}(s) = {\cal L}(t) \big) \wedge\nonumber\\
		&	&	\big(\mbox{for every fair rational path}\, \sigma\, \mbox{starting at }\, s \, \nonumber\\%
		&	&			\,\,\,\mbox{ there exists a fair rational path}\,  \tau \, \mbox{starting at } t \, \mbox{such that\, }%
						{\cal E}(\sigma, \tau)\big) \wedge \nonumber \\
		&	&	\big(\mbox{for every fair rational path}\, \tau\, \mbox{starting at }\, t \nonumber \\%
		&	&			\,\,\,\mbox{there exists fair rational path}\,\sigma\,\mbox{starting at }\,s\,\mbox{such that\, }%
						{\cal E}(\sigma, \tau)\big) 
\end{eqnarray*}
Then ${\cal E}$ preserves equivalence across all fair paths, i.e.,
for every fair path $\sigma$ starting at $s$ there exists a fair path $\tau$
starting at  $t$ such that ${\cal E}(\sigma, \tau)$, and for every fair path
$\tau$ starting at $t$ there exists a fair path $\sigma$ starting at $s$ 
such that ${\cal E}(\tau, \sigma)$.
\end{lemma}



\begin{proof}
\rm
Let $\{ {\cal C}_1, {\cal C}_2, \ldots, {\cal C}_n\}$ be the equivalence  classes of ${\cal E}$.
Define an alphabet $\Sigma = \{c_1,c_2,\ldots,c_n\}$ corresponding to the equivalence classes.
Define the $\omega$-language $L_s$ over $\Sigma$ as $L_s = \{x \in \Sigma^{\omega} \mid \exists \sigma
\in {\cal F}^{f}_{s} \,\, \mbox{such that } \,\, (\forall i) \, [\sigma]_i \in {\cal C}([x]_i)\}$, 
where ${\cal C} : \{ {\cal C}_1, {\cal C}_2, \ldots, {\cal C}_n\} \rightarrow \Sigma $
maps alphabets to their corresponding equivalence classes.
Observe that $L_s$ is $\omega$-regular~\cite{thomas90},
since the fair-Kripke structure can be viewed as a Muller 
automaton, with the output at a state being the symbol of $\Sigma$ 
corresponding to its equivalence class.
Similarly, define the $\omega$-regular language $L_t = \{y \in \Sigma^{\omega} \mid \exists \tau
\in {\cal F}^{f}_{t} \,\, \mbox{such that } \,\, \forall i \, [\tau]_i \in {\cal C}([y]_i)\}$.

It is clear that given any fair path $\sigma$ starting at $s$, there is a fair path $\tau$ 
starting at $t$ which is ${\cal E}$-equivalent to $\sigma$, and vice versa, if and only
if $L_s = L_t$.

Note that if $W_1$ and $W_2$ are two $\omega$-regular languages over the same alphabet, and they
agree on all rational words (i.e., words that are ultimately periodic), then they are in fact equal;
this follows from the following observation: Let $W$ be the  symmetric difference of $W_1$ and $W_2$,
i.e., $W = (W_1 \cap \bar{W_{2}}) \cup (\bar{W_{1}} \cap W_2)$. Then $W$ is $\omega$-regular, and so is non-empty
if and only if it contains a rational word~\cite{thomas90}.
But $W_1$ and $W_2$ contain exactly the same set of 
rational words; consequently $W$ is empty, and so $W_1 = W_2$.

Since $L_1$ and $L_2$ agree on all rational words (because $s$ and $t$ agree on all rational paths),
it follows that $L_1 = L_2$, and so $s$ and $t$ must agree on all paths, proving the lemma.
\end{proof}

\subsubsection{Upper bounds on computing ${\cal E}^{fair\ast}$ }

The previous lemma can be used to derive a PSPACE upper
bound on the complexity of deciding ${\cal E}^{fair\ast}$ for
Kripke structures with practical forms of expressing fairness.
Specifically, we consider the case of  B\"uchi fairness constraints, which due
to their succinctness relative to Muller fairness constraints are more meaningful in practice. 

A B\"uchi fairness 
constraint is a subset $B$ of the state space of the Kripke structure;
a path $\sigma$ is fair if {\tt inf}$(\sigma)  \cap B \neq \emptyset$.

\begin{proposition}
\rm
The ${\cal E}^{fair\ast}$ equivalence relation can be computed in PSPACE
for Kripke structures with B\"uchi fairness constraints.
\end{proposition}

\begin{proof}
Consider the equivalences $E_0,E_1,\ldots$ as defined in the proof of Theorem~\ref{thm:CTLstar}.
Observe that $E_{k+1}$ can be derived from $E_k$ by viewing the Kripke structure
as a B\"uchi automaton where the state label is the $E_k$-equivalence
class to which it belongs, and the acceptance is the corresponding 
B\"uchi fairness constraint. The relation  $E_{k+1}$ is simply
the language equivalence relation on the states of this automaton~\cite{thomas90}.

Since ${\cal E}^{fair\ast} = E_\infty$ is reached from $E_0$ in at most $n$ steps, where
$n$ is the number of states, it is clear that the fair bisimulation relation
can be computed using a polynomial number of calls to trace equivalence
on B\"uchi automata which are no larger than the original Kripke structure.
Trace equivalence for B\"uchi automata is known to be complete for PSPACE~\cite{sistla87}.
Consequently, ${\cal E}^{fair\ast}$ can be decided
in PSPACE for Kripke structures with such fairness constraints. 
\end{proof}

Given the close relationship
between trace equivalence and fair bisimilarity shown above,
it is reasonable to conjecture that 
deciding fair bisimilarity is as hard as deciding
trace equivalence which is  PSPACE-complete; this was proved by
Kupferman and Vardi~\cite{ok96}, who used a reduction from the universality
problem for regular expressions, similar to that used to show trace universality
is PSPACE-hard~\cite{hopcroft79,stockmeyer74}.


\subsection{Equivalences preserving CTL on fair-Kripke structures }
\label{sec-CTL}

The logic CTL is a subset of the logic CTL$^{\ast}$ where nesting of path operators
is not allowed, i.e., every path operator must be immediately preceded by a path quantifier.
Since it is a subset of CTL$^{\ast}$, it follows from Theorem~\ref{thm:CTLstar} that 
states that are ${\cal E}^{fair\ast}$-equivalent must agree on all CTL formulae.
However the converse is not true, as was illustrated  by
Clarke and Draghicescu~\cite{clarke-88} as part of their proof of the fact that 
the CTL$\ast$ property $A(FGp)$ is not expressible in CTL. We reproduce their
argument below.

Consider the states $s_1$ and $t_1$ in Figure~\ref{fig:cntrex}.
\begin{figure}[b]
% \centerline{\ \psfig{figure=cntrex.eps,width=8cm}}
\centerline{\ \epsfbox{cntrex.eps}}
\caption{\ \label{fig:cntrex} States that agree on all CTL formulae but can be differentiated by CTL$^{\ast}$ }
\end{figure}
\begin{enumerate}
\item The set of atomic propositions is $\{a,b\}$, the set of APs true at $s_1$ and $t_1$ is $\{a\}$,
the set of APs true at $s_2$ and $t_2$ is $\{b\}$.
\item The fairness conditions are of Muller type. The sets $U_1 = \{s_1\}$, $U_2 = \{s_1,s_2\}$, and
$V_1 = \{t_1\}$ are the fair Muller sets, i.e., fair  paths are those in which the infinitary set of states
is exactly one of $U_1,U_2,V_1$.
\end{enumerate}
State $s_1$ can not be differentiated from $t_1$ by any CTL formula, since the only difference 
is the fact that there are paths from $s_1$ on which $b$ occurs infinitely often, and CTL can not
express $\exists GF \phi$, i.e., there exists a path such that infinitely often $\phi$ 
is true. This fact was first proved by Emerson and Clarke~\cite{emerson-icalp-81};
a considerably shorter proof was presented by Clarke and Draghicescu~\cite{clarke-88}.
See~\cite[page 1029]{emerson90} for a proof sketch.

More formally, the equivalence of $s_1$ and $t_1$ with respect to all CTL formula can 
be proved by using induction on the length of the formula.

It is surprising that the set of output traces from $s_1$ is not equal to the set 
of output traces 
from $t_1$; consider for example the trace $\langle a, b\rangle^{\omega}$. This in contrast to the fact
that in the absence of fairness constraints states that are bisimilar equivalent must have the same
set of traces. 

We can still characterize states that agree on all CTL formula as shown in the following theorem.

\begin{definition}\label{defn:CTL}
\rm 

Let $K$ be a fair-Kripke structure $(S,T,{\cal L},f)$.
An equivalence relation  ${\cal E} \subset S \times S$ is said to be a
$fair$ bisimulation if for any $(s,t) \in {\cal E}$ the following are true:
\begin{enumerate}
\item 	$ {\cal L}(s) = {\cal L}(t) $, and 
\item 	for every fair rational path $\sigma$ starting at $s$,  and every $N$ and  $k$ such that 
	$\sigma = \langle s, s_1, s_2, \cdots, s_{N-1}\rangle  \cdot \langle s_{N},
	s_{N+1}, \cdots, s_{N+k-1}\rangle^{\omega}$
	there exists a fair rational path $\tau$ starting at $t$
	such that  for every $i \in \{0,1,\ldots,N-1\}$, it is true that 
	${\cal E}([\sigma]_i,[\tau]_i)$ and for every $i \geq N$
	it is true that $[\tau]_i$ is  ${\cal E}$-equivalent to some state in $\mbox{\tt inf}(\sigma)$, and 
\item 
for every fair rational path $\tau$ starting at $t$,  and every $N$ and  $k$ such that
        $\tau = \langle t, t_1, \cdots, t_{N-1}\rangle  \cdot \langle t_{N}, 
        t_{N+1}, \cdots, t_{N+k-1}\rangle^{\omega}$
        there exists a fair rational path $\sigma$ starting at $s$
        such that  for every $i \in \{0,1,\ldots,N-1\}$, it is true that
        ${\cal E}([\tau]_i,[\sigma]_i)$ and for every $i \geq N$
        it is true that $[\sigma]_i$ is ${\cal E}$-equivalent to some state in $\mbox{\tt inf}(\tau)$.
\end{enumerate}
The relation ${\cal E}^{fair}$ is defined to be 
the coarsest relation that is a $fair$ bisimulation.
\end{definition}
The soundness of this definition follows in a manner analogous 
to that of the definition of ${\cal E}^{bis}$,  as given in 
Section~\ref{sec-bis}.

In the sequel, given an equivalence relation ${\cal E}$ on states and a fair path $\tau$,
we will say that  $\tau$ ${\cal E}$-corresponds to a 
fair rational path $\sigma$ if for every $N$ and  $k$ such that 
                        $\sigma = \langle s_0, s_1, s_2, \cdots, s_{N-1}\rangle \cdot \langle s_{N}, 
                        s_{N+1}, \cdots, s_{N+k-1}\rangle^{\omega}$,
for every $i \in \{0,1,\ldots,N-1\}$, it is true that 
                        ${\cal E}([\sigma]_i,[\tau]_i)$ and for every $i \geq N$,
we have $[\tau]_i$ is  ${\cal E}$-equivalent to some state in $\mbox{\tt inf}(\sigma)$


The ${\cal E}^{fair}$-bisimilarity relation is the natural extension
to bisimulation when model checking
CTL on fair-Kripke structures in the sense that 


\begin{theorem}\label{thm:CTL}
\rm
Let $s$ and $t$ be states in  a fair-Kripke structure $K = ( S,T,{\cal L}, f)$. 
Then ${\cal E}^{fair}(s,t)$ if and only if there is no CTL
formula   $\phi$ such that $s\models \phi$ and $t\not\models \phi$.
\end{theorem}


\begin{proof}
\rm

First we consider soundness, i.e., 
that ${\cal E}^{fair}(s,t) \Rightarrow $ for any CTL formula $\phi$,
state $ s \models \phi$ if and only if state $t \models \phi$.  Unlike in Theorem~\ref{thm:CTLstar},
this is not trivial to show, and we present the proof.

We proceed by  induction
on the length of the formula.

{\bf Base Case:}  $\phi = $ \underline{a} where a $ \in \mbox{AP}$. It follows from the definition
of ${\cal E}^{fair}$ that ${\cal L}(s) = {\cal L}(t)$, and so
$s \models$  \underline{a} if and only if $t \models$  \underline{a}. Hence the
base case is proved.

{\bf Inductive Step:} 
\begin{enumerate}
\item $\phi = \neg\phi_1$ --- Follows from elementary propositional logic.
\item $\phi = (\phi_1 \vee \phi_2 )$ --- Follows from elementary propositional logic.
\item $\phi = \exists X (\phi_1)$ ---  Observe that ${\cal E}^{fair}(s,t)$ implies that we must have
				$\forall s' \Big( T(s ,s') \,\, \Rightarrow \,\, \exists t' \big(T( t , t')
				\wedge {\cal E}^{fair} (s',t') \big)\Big)$.
This follows from the fact that $s'$ can be 
continued to a fair rational path, and so there must be a corresponding
fair rational path from $t$. The state $t'$ can be taken to be 
the state following $t$ in this path.
From this observation and the IH, it follows that 
$\exists s' \big( T(s , s') \wedge s' \models \phi_1 \big)$ if and only if 
$\exists t' \big( T(t , t') \wedge t' \models \phi_1 \big)$.
The converse, namely to show  
$t \models \phi \,\,\Rightarrow s \models \phi$, follows by symmetry.

\item $\phi = \exists ( \phi_1 U \phi_2 )$ --- Suppose $s \models \phi$. Then  from the 
semantics of CTL, it follows that there exists a fair path $ \sigma = \langle s, s_1, s_2, \cdots \rangle $ 
such that  there is a natural number $N$ for which 
for all natural numbers $i$ such that $i < N$ we have $[\sigma]_i \models \phi_1$ and 
$ [\sigma]_N \models \phi_2$. 
Reasoning as above, there must exist a finite sequence
			$\langle t, t_1, t_2, \cdots t_{N}\rangle$ such that 
for every $i \leq N$ we have ${\cal E}^{fair}(s_i,t_i)$.
			Hence by the IH, for every $i < N $ it must be the case that $t_i \models \phi_1$,
			and $t_N \models \phi_2$.
			This finite path can be extended to an infinite path, since every state 
			is assumed to lie on a fair path, and this infinite path satisfies 
			$ \phi_1 U \phi_2 $. Thus $t \models \phi $. 
			The converse, namely to show  
			$t \models \phi \,\,\Rightarrow s \models \phi$, follows by symmetry.

\item  $\phi = \exists G (\phi_1)$ --- Suppose $s \models \phi$. Then must be a fair rational path $\sigma$
such that for each $i$, we have $[\sigma]_i \models \phi$. 
Since $\sigma$ is rational, it can be expressed as a sequence 
$\langle s, s_1, s_2, \cdots, s_{N-1}\rangle \cdot \langle s_{N},
s_{N+1}, \cdots, s_{N+k-1}\rangle^{\omega}$.
 Because $s$ is ${\cal E}^{fair}$-equivalent to $t$, it follows that
there is a fair rational path $\tau$ ${\cal E}^{fair}$-corresponding to $\sigma$.
Since $\sigma \models G (\phi_1)$, it follows that every state
on $\sigma$ satisfies $\phi_1$. Since every state on the path $\tau$ is ${\cal E}^{fair}$-equivalent 
to some state on $\sigma$, and the induction hypothesis requires that states that are
${\cal E}^{fair}$-equivalent agree on all CTL formula of length less than the length of $\phi$,
it follows that all states on $\tau$ satisfy $\phi_1$; thus $t \models \phi$. 
The converse, namely to show
$t \models \phi \,\,\Rightarrow s \models \phi$, follows by symmetry.
\end{enumerate}%induction

Hence by induction, states that are $E_{\infty}$-equivalent satisfy exactly the same set of
CTL formula.  This completes the proof of  soundness.

We now show completeness, i.e., that 
states which are not ${\cal E}^{fair}$-equivalent can be differentiated
by CTL. We  proceed in a manner similar to that  in the proof of Theorem~\ref{thm:CTLstar}.


First we define the series of equivalences $E_0,E_1,\ldots$ as follows:
\begin{enumerate}
\item $E_0(s,t)$ if and only if ${\cal L}(s) = {\cal L}(t)$.
\item $E_{l +1}(s,t)$ if and only if 
\begin{enumerate}
\item for every fair rational path $\sigma$ from $s$, there is an $E_l$-corresponding 
				fair rational path $\tau$  from $t$, and 
\item for every fair rational path $\tau$ from $t$, there is a  an $E_l$-corresponding
                                fair rational path $\sigma$  from $t$.
\end{enumerate}
\end{enumerate}

Observe that $E_{l+1}(s,t) \subseteq  E_{l}(s,t)$. 
Also every equivalence in the sequence
contains the equality relation (the binary relation where an element is related only
to itself). Since the state space is finite the sequence converges to a fixed point
in some finite number of steps, i.e., there is some $k$ such that $E_{k+1} = E_{k}$,
which we will refer to as $E_{\infty}$.

Notice that $E_{\infty}$ satisfies Conditions 1--3 in Definition~\ref{defn:CTL}, and hence $E_{\infty}$
must lie in ${\cal E}^{fair}$, since by definition, ${\cal E}^{fair}$ is the coarsest
relation satisfying Conditions 1--3 in Definition~\ref{defn:CTL}.  Thus if we show that states which are 
not $E_{\infty}$-equivalent can be differentiated by CTL formulae, we will have
shown that states which are not ${\cal E}^{fair}$-equivalent  can be 
differentiated by CTL formulae.

We now characterize states up to $E_l$-equivalence by CTL formulae. This is done by induction
on $l$. Specifically we will demonstrate:

\begin{enumerate}
\item If $\neg\big(E_l(s,t)\big)$ then there is a CTL formula 
$d_l(s,t)$ such that every state $v$ which is $E_l$ to $s$ satisfies  $v \models d_l(s,v)$,
and $t \not\models d_l(s,t)$, and,
\item for every state $s \in S$, there
is a formula of CTL $C_l(s)$ such that for every state
$t$ it is true that $t \models C_l(s)$ if and only if $E_l(s,t)$.
\end{enumerate}
The formula $d_l(s,t)$ distinguishes between $t$ and states $E_l$-equivalent to $s$
and $C_l(s)$ is a formula that characterizes $E_l$-equivalence to state $s$ within the
fair-Kripke structure.

If we let $C_l(s)$ be a conjunction of $C_{l-1}(s)$ and $d_l(s,t)$ for every $t$ which is not
$E_l$-related to s, the second assertion follows immediately. Now it is necessary to show how 
to construct $d_l(s,t)$ by induction on $l$.


{\bf Base Case:}(l=0)\\
Let $\{p_i\}$ be the set of atomic propositions in ${\cal L}(s)$ and $\{q_j\}$ be the
set of atomic propositions in $\mbox{AP} - {\cal L}(s)$. Now let 
$d_0(s,t) = {\bigwedge}_{i} \underline{p_i} \wedge {\bigwedge}_{j} \neg \underline{q_j}$. It is clear that
this formula is only true in states with exactly the same labeling as $s$.
Thus the base case is established.

{\bf Induction:}\\
Assume the result is true for $l$. We will show it for $l+1$.

Let $s$ and $t$ be any states in the structure such that $\neg \big(E_{l+1}(s,t)\big)$. This can only
happen if there is a fair rational  path from $s$ with no $E_l$-corresponding (in the sense used
in Definition~\ref{defn:CTL}) fair rational  path from $t$, 
or there is a fair rational  path from  $t$ for which there is no $E_l$-corresponding fair 
rational  path out
of $s$. In the latter case, we will use the argument below to find a $d_{l+1}(t,s)$ such that 
$t \models d_{l+1}(t,s)$ and $s \not\models d_{l+1}(t,s)$. We can negate this formula
to obtain the desired $d_{l+1}(s,t)$.

Let $\sigma = \langle s, s_1, \cdots, s_{N-1}\rangle \cdot 
\langle s_{N+1}, \cdots, s_{N+k}\rangle^{\omega}$ be  a fair rational path from
$s$ with no $E_l$-corresponding fair rational path from $t$.

First define the CTL formula $\mbox{\tt infinite}_{l+1}(s,t)$
as below:
\begin{eqnarray*}
\mbox{\tt infinite}_{l+1}(s,t) & = & \exists G \Big( C_l(s_{N}) \vee C_l(s_{N+1}) \vee \cdots \vee C_l(s_{N+k-1})\Big)
\end{eqnarray*}

Now define  $d_{l+1}(s,t)$:
\begin{eqnarray*}
d_{l+1}(s,t)	&= &	C_l(s) \wedge \exists X \Big( C_l(s_1) \wedge \exists X \Big( C_l(s_2)
					\wedge  \cdots \wedge \exists X \Big(C_l(s_{N-1}) \wedge  \\
		&  &	\,\,\, \exists X \big( \mbox{\tt infinite}_{l+1}(s,t) \big ) \Big ) \cdots \Big )
\end{eqnarray*}

\begin{proposition}
\rm
A state $u$ satisfies $d_{l+1}(s,t)$  if and only if  lies at the beginning of 
a fair  path which $E_l$-corresponds  to $\sigma$. 
\end{proposition}

\begin{proof}
The ``if'' part is straightforward; the $E_l$-corresponding fair path will provide the
existential witnesses.

We now prove the ``only if'' part.
Since $u$ satisfies $d_{l+1}(s,t)$, the formula $C_l(s)$
must be true at $u$.  Furthermore,  there must be a successor state for which 
$C_l(s_1)$ is true, and $ \exists X \big( C_l(s_2)\wedge  \cdots \wedge 
\exists X \big(C_l(s_{N-1}) \wedge  \exists X \big( \mbox{\tt infinite}_{l+1}(s,t) \big) \cdots \big) $
is also true; call this state $u_1$.
Continuing in this manner, we see that there must be a finite sequence of states
$\langle u, u_1, u_2, \cdots, u_{N-1}\rangle$ which 
satisfy $C_l(s), C_l(s_1), \cdots, C_l(s_{N-1})$ respectively.
Furthermore, $u_{N-1}$ satisfies  $\exists X \big( \mbox{\tt infinite}_{l+1}(s,t) \big)$; 
hence $u_{N-1}$ has a successor state from which 
there is a fair path on which every state satisfies some $C_l(s_i)$, where 
$i \in \{N, N+1,\ldots, N+k-1\}$;
call this path $\upsilon$.  Consider the path $\langle u, u_1,\cdots, u_{N-1} \rangle  \cdot \upsilon$.
By the IH, states which satisfy $C_l(r)$ must be $E_l$-equivalent to $r$, and so the path
$\langle u, u_1 \cdots u_{N-1} \rangle \cdot \upsilon$ must $E_l$-correspond to 
$\sigma$, proving the proposition.
\end{proof}

Since the  state $t$ does not  lie at the beginning of a fair  path which $E_l$-corresponds  to 
$\sigma$, it does not satisfy the formula $d_{l+1}(s,t)$.
\end{proof}

\subsection{$\forall$CTL$^\ast$, similarity and fairness}

The logic $\forall$CTL$^\ast$ is the subset of CTL$^\ast$ state formulae
where negations occur only on the atomic 
propositions, and all path quantifiers are universal. It has been argued that this logic
suffices to express most commonly encountered specifications,
and that it is well suited to reasoning about compositional designs~\cite{grumberg91}.

Let  $K = ( S, T, {\cal L} )$ be a Kripke structure. The relation ${\cal F}^{sim} \subset S \times S$
is said to be a {\em simulation relation} if for all $(s,t) \in S \times S$
it  satisfies the following:
\begin{eqnarray}\label{eqn:sim}
{\cal F}^{sim}(s,t)     &   \Rightarrow     &   \big({\cal L}(s) = {\cal L}(t)\big) \wedge \nonumber \\
                        &                       &   \,\,\, \forall t' \Big( T(t,t') \rightarrow \exists s' \big( T(s,s') \wedge {\cal F}^{sim}(s',t')\big)\Big)
\end{eqnarray}
State $s$ is said to {\em simulate} $t$ when there exists a simulation relation ${\cal F}^{sim}$ such that
${\cal F}^{sim}(s,t)$; if $s$ simulates $t$ and $t$ simulates $s$ then $s$ and $t$ are said to be {\em similar}.
It is straightforward to show the existence and uniqueness of a maximal equivalence relation on $S$ where
equivalent states are similar; this relation is referred to as {\em similarity}.

The relationship between $\forall$CTL$^\ast$ and similarity  is completely
analogous to the relationship between CTL$^\ast$ and bisimulation.
Grumberg and Long~\cite{grumberg94} introduced the notion of a fair simulation
relation for fair-Kripke structures.
They proved fair simulation is sound with respect to $\forall$CTL$^\ast$, i.e.,
if state $s$ fair simulates  state $t$, then all formulae in the
logic $\forall$CTL$^\ast$ which hold at $s$ also hold at $t$. Their definition of fair simulation
is completely analogous to the definition of fair bisimulation given in this paper. However,
they did not prove any completeness results, which are substantially more difficult
to show than soundness results.
The techniques in our paper can  be trivially extended
to demonstrate that the fair similarity relation is the weakest equivalence
preserving $\forall$CTL$^\ast$ over fair-Kripke structures.

\section{Conclusion and Future Work}

We have defined state equivalences on Kripke structures that 
incorporate fairness. These equivalences were shown to be complete
in the sense that they are the weakest equivalences preserving
branching time logics interpreted on the structures. 
Furthermore we characterized the equivalence classes by
formulae from the logic.


We have developed approximations
to the complete equivalence that can be efficiently computed for 
B\"{u}chi, Rabin, and Streett fairness conditions.
These are used in a hierarchical procedure for 
minimizing systems of interacting state machines~\cite{aziz94e}.
We plan to continue developing generalized notions of equivalence
that are property specific, and can be used to reduce or abstract
components in large designs~\cite{aziz94b}.
We are also developing adequate notions of bisimulation for 
more complex designs, such as those which include uninterpreted functions,
or timing/statistical functionality.


\bibliography{adnan_refs}
\bibliographystyle{plain}

\end{document}
