\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}