% The Chicago Journal of Theoretical Computer Science, Volume 1995, Article 3
% Published by MIT Press, Cambridge, Massachusetts USA
% Copyright 1995 by Massachusetts Institute of Technology
%
\newtoks\rstyle
\rstyle={cjlook}
%
\ifx\documentclass\undeftex
\documentstyle[v1.1,published]{cjstruct}
\else
\documentclass[v1.1,published]{cjstruct}
\fi
%
% Local resources for this article.
%
\usestyleresource{amstex}
\usestyleresource{amscd}
\usestyleresource{amssymb}
\usestyleresource{epic}
\ifltwoe\else\usestyleresource{bezier}\fi
%
% Local macro definitions for this article.
%
\catcode`\@=11
\ifx\nopagebreakbeginpar\undeftex
  \newcommand{\nopagebreakbeginpar}{\@beginparpenalty10000}
\fi
\ifx\nopagebreakendpar\undeftex
  \newcommand{\nopagebreakendpar}{\@endparpenalty10000}
\fi
\catcode`\@=12
%
\ifltwoe\else\newcommand{\emph}[1]{{\em #1\/}}\fi
\ifltwoe\else\newcommand{\textit}[1]{{\it #1\/}}\fi
\ifltwoe\else\newcommand{\textbf}[1]{{\bf #1\/}}\fi
\ifltwoe\else\newcommand{\textup}[1]{{\rm #1}}\fi
\ifltwoe\else\newcommand{\mathcal}[1]{{\cal #1}}\fi
\ifltwoe\else\newcommand{\upshape}{\fontshape{n}\selectfont}\fi
%
\newcommand{\prooffontshape}{\upshape}
\newcommand{\exampfontshape}{\upshape}
%
\newcommand{\tightspace}[1]{\mathord{#1}}
\newcommand{\hatcapstrut}{\rule{0ex}{2.5ex}}
%
\ifltwoe\else\newcommand{\qbezier}{\bezier{300}}\fi
%
\newcommand{\condval}[1]{\left\{\begin{array}{ll}#1\end{array}\right.}
\newcommand{\logicimplies}{\Longrightarrow}
\newcommand{\logicimplied}{\Longleftarrow}
\newcommand{\logicand}{\wedge}
\newcommand{\Rabcond}[1]{\mathcal{#1}}
\newcommand{\setof}[2]{\{\,#1\mid#2\,\}}
\newcommand{\setsize}[1]{\mathopen{|}#1\mathclose{|}}
\newcommand{\setintsct}{\cap}
\newcommand{\setunion}{\cup}
\newcommand{\setdiff}{\mathbin{\backslash}}
\newcommand{\setcomp}[1]{\overline{#1}}
\newcommand{\nodelevel}[1]{\mathopen{|}#1\mathclose{|}}
\newcommand{\prefix}{\mathbin{\restriction}}
\newcommand{\hca}{\mathbin{\uparrow}}
\newcommand{\concat}{\cdot}
\newcommand{\pfgt}{\mathrel{\underset{\concat}{>}}}
\newcommand{\pflt}{\mathrel{\underset{\concat}{<}}}
\newcommand{\pfleq}{\mathrel{\underset{\concat}{\leq}}}
\newcommand{\emptyvec}{%
  \mathchoice{\mathord{\mbox{\(\displaystyle\langle\,\rangle\)}}}%
             {\mathord{\mbox{\(\langle\,\rangle\)}}}%
             {\mathord{\mbox{\(\scriptstyle\langle\,\rangle\)}}}%
             {\mathord{\mbox{\(\scriptscriptstyle\langle\,\rangle\)}}}%
}
%
\newcommand{\powerset}[1]{\mathcal{P}#1}
\newcommand{\oftype}{\mathpunct{:}}
\newcommand{\funcspace}[2]{#1\mathbin{\rightarrow}#2}
\newcommand{\partfuncspace}[2]{#1\mathbin{\rightharpoonup}#2}
\newcommand{\dom}{\operatorname{dom}}
\newcommand{\automtrans}[1]{\stackrel{#1}{\rightarrow}}
\newcommand{\automlang}{L}
%
\mathstyleclass{\colsetasgn}{\mathord}{\textit}
\newcommand{\satisfy}{\vDash}
%
\newcommand{\vect}[1]{\langle#1\rangle}
\mathstyleclass{\prog}{\mathord}{\textbf}
\newcommand{\progvar}[1]{#1}
\newcommand{\assigned}{\mathrel{:=}}
\mathstyleclass{\testcond}{\mathord}{\textit}
\newcommand{\progcond}{\rightarrow}
\newcommand{\at}{\mathord{\textup{at}}}
%
\newcommand{\Rabinrel}[1]{\vartriangleright_{#1}}
%
\newcommand{\hatparenskip}{\,}
%
% end of local macro definitions for this article
%
\begin{document}
%
\begin{articleinfo}
%
\publisher{The MIT Press}
%
\publishercomment{%
  {\Large
    \begin{center}
      Volume 1995, Article 3\\
      \textit{20 September 1995}
    \end{center}
  }
  \par\noindent
  ISSN 1073--0486\@. MIT Press Journals, 55 Hayward St., Cambridge, MA
  02142 USA; (617)253-2889;
  \emph{journals-orders@mit.edu, journals-info@mit.edu}\@.
  Published one article at a time in \LaTeX\ source form on the
  Internet\@. Pagination varies from copy to copy\@. For more
  information and other articles see:
  \begin{itemize}
    \item \emph{http://www-mitpress.mit.edu/jrnls-catalog/chicago.html}
    \item \emph{http://www.cs.uchicago.edu/publications/cjtcs/}
    \item \emph{gopher.mit.edu}
    \item \emph{gopher.cs.uchicago.edu}
    \item anonymous \emph{ftp} at \emph{mitpress.mit.edu}
    \item anonymous \emph{ftp} at \emph{cs.uchicago.edu}
  \end{itemize}
\sentence
}
%
\copyrightstmt{%
  \copyright 1995 The Massachusetts Institute of Technology\@.
  Subscribers are licensed to use journal articles in a variety of
  ways, limited only as required to insure fair attribution to authors
  and the journal, and to prohibit use in a competing commercial
  product\@. See the journal's World Wide Web site for further
  details\@. Address inquiries to the Subsidiary Rights Manager, MIT
  Press Journals; (617)253-2864;
  \emph{journals-rights@mit.edu}\@.\pagebreak[2]
}
%
\journal{Chicago\nolinebreak[1] Journal of Theoretical Computer\nolinebreak[1] Science}
%
\journalcomment{%
  The \emph{Chicago Journal of Theoretical Computer Science}
  is a peer-reviewed scholarly
  journal in theoretical computer science\@. The journal is committed
  to providing a forum for significant results on theoretical
  aspects of all topics in computer science\@.
  \par
  \begin{trivlist}
    \item[\emph{Editor in chief:}] Janos Simon
    \item[\emph{Consulting editors:}]
      Joseph Halpern, Stuart A.\ Kurtz, Raimund Seidel
    \item[\emph{Editors:}]
      \begin{tabular}[t]{lll}
        Martin Abadi & Greg Frederickson & John Mitchell \\
        Pankaj Agarwal & Andrew Goldberg & Ketan Mulmuley \\
        Eric Allender & Georg Gottlob & Gil Neiger \\
        Tetsuo Asano & Vassos Hadzilacos & David Peleg \\
        Laszl\'o Babai & Juris Hartmanis & Andrew Pitts \\
        Eric Bach & Maurice Herlihy & James Royer \\
        Stephen Brookes & Stephen Homer & Alan Selman \\
        Jin-Yi Cai & Neil Immerman & Nir Shavit \\
        Anne Condon & Paris Kanellakis & Eva Tardos \\
        Cynthia Dwork & Howard Karloff & Sam Toueg \\ 
        David Eppstein & Philip Klein & Moshe Vardi \\
        Ronald Fagin & Phokion Kolaitis & Jennifer Welch \\
        Lance Fortnow & Stephen Mahaney & Pierre Wolper \\
        Steven Fortune & Michael Merritt
      \end{tabular}
    \vspace{1ex}
    \item[\emph{Managing editor:}] Michael J.\ O'Donnell
    \vspace{1ex}
    \item[\emph{Electronic mail:}] \emph{chicago-journal@cs.uchicago.edu}
  \end{trivlist}
\sentence
}
%
\bannerfile{cjtcs-banner.tex}
%
\volume{1995}
%
\articleid{3}
%
\selfcitation{
     @article{cj95-03,
       author={Nils Klarlund and Dexter Kozen},
       title={Rabin Measures},
       journal={Chicago Journal of Theoretical Computer Science},
       volume={1995},
       number={3},
       publisher={MIT Press},
       month={September},
       year={1995}
     }
}
%
\begin{retrievalinfo}
\end{retrievalinfo}
%
\title{Rabin Measures}
\shorttitle{Rabin Measures}
\collectiontitle{}
\begin{authorinfo}
%
% Correction to error in cjstruct.sty version 1.1.
%
\def\fixversion{1.1}
\ifx\cjversion\fixversion
  \renewcommand{\printname}[1]{
    \global\authorstring={#1}
    \global\authorstrue
    \ifinfo\item Printed name: #1\fi
  }
\fi
%
% End of correction.
%
   \printname{Nils Klarlund}
   \collname{}{Klarlund, Nils}
   \begin{institutioninfo}
       \instname{University of Aarhus}
       \department{Department of Computer Science}
       \address{}{Aarhus}{}{Denmark}{DK-8000}
   \end{institutioninfo}
   \begin{institutioninfo}
       \instname{Danish National Research Foundation}
       \department{Centre for Basic Research in Computer Science}
   \end{institutioninfo}
   \email{klarlund@daimi.aau.dk}
\end{authorinfo}
%
\begin{authorinfo}
   \printname{Dexter Kozen}
   \collname{}{Kozen, Dexter}
   \begin{institutioninfo}
       \instname{Cornell University}
       \department{Department of Computer Science}
       \address{}{Ithaca}{NY}{USA}{14853}
   \end{institutioninfo}
   \email{kozen@cs.cornell.edu}
\end{authorinfo}
%
\shortauthors{Klarlund and Kozen}
%
\support{%
Nils Klarlund was partially supported by a research stipend from the
University of Aarhus, Denmark; an Alice \& Richard Netter Scholarship
of the Thanks to Scandinavia Foundation, Inc., USA; and
Forskerakademiet, Denmark\@. Part of this research was carried out while
the author was with IBM T.\ J.\ Watson Research Center, NY,
USA\@. Dexter Kozen was partially supported by NSF grant
CCR-8901061\@.%
}
%
\begin{editinfo}
  \submitted{20}{9}{1994}\reported{31}{1}{1995}
  \submitted{18}{5}{1995}\reported{21}{5}{1995}
  \submitted{23}{5}{1995}\reported{6}{6}{1995}\published{20}{9}{1995}
\end{editinfo}
\end{articleinfo}
%
\begin{articletext}
\begin{abstract}
%
\apar{Abstract-1}
\emph{Rabin conditions} are a general class of properties of infinite
sequences that encompass most known automata-theoretic acceptance
conditions and notions of fairness\@. In this paper, we introduce a
concept, called a \emph{Rabin measure}, which in a precise sense
expresses progress for each transition toward satisfaction of the
Rabin condition\@.
%
\apar{Abstract-2}
We show that these measures of progress are linked to the
Kleene-Brouwer ordering of recursion theory\@. This property is used
in~\cite{cj95-03-19} to establish an exponential upper bound
for the complementation of automata on infinite trees\@.
%
\apar{Abstract-3}
When applied to termination problems under fairness constraints, Rabin
measures eliminate the need for syntax-dependent, recursive
applications of proof rules\@.
%
\end{abstract}
%
This article is a revised version of~\cite{cj95-03-20}\@. Compared to
the earlier version, the notion of Rabin measure has been simplified
in order to be consistent with the use of the present results
in~\cite{cj95-03-19}\@.
%
\asection{1}{Introduction}
%
\apar{1-1}
This paper is concerned with infinite sequences and their properties
that are true or false in the limit\@. Such properties arise in the
study of fairness, temporal logic, and \(\omega\)-automata\@. In all
these areas, \emph{Rabin conditions} \cite{cj95-03-25,cj95-03-28},
which express temporal properties in a special disjunctive normal
form, play a major role\@. (They are also called \emph{pairs
conditions}\@.) In the theory of fairness, Rabin conditions describe
termination under \emph{general fairness constraints}, which include
\emph{strong fairness} expressing that commands that are infinitely
often enabled are infinitely often executed\@. In temporal logic, Rabin
conditions can be used to model a variety of liveness properties\@. In
the theory of \(\omega\)-automata, Rabin conditions are pivotal,
because they allow \(\omega\)-regular languages to be expressed by
deterministic automata~\cite{cj95-03-25}\@.
%
\apar{1-2}
Because temporal conditions are often crucial to understanding the
behavior of concurrent and distributed programs, a large number of
proof methods for Rabin conditions and simpler conditions have been
proposed in the context of fairness
\cite{cj95-03-3,cj95-03-4,cj95-03-5,cj95-03-9,cj95-03-8,cj95-03-10,cj95-03-22,cj95-03-33},
temporal logic \cite{cj95-03-23,cj95-03-27}, or automata theory
\cite{cj95-03-1,cj95-03-2,cj95-03-12,cj95-03-24,cj95-03-34}\@. The
essence of some of the proposed methods is obscured by syntactic
transformations; others are limited to simple temporal formulas or
expressed in rather involved automata-theoretical terms\@.
%
\apar{1-3}
In this paper we address a fundamental question underlying several of
the previous approaches: How can one explain, in terms of local
conditions and without transformations, that a graph satisfies a Rabin
condition\@? Our contribution is a concept, called a \emph{Rabin
measure}, which mathematically quantifies progress for transitions
toward satisfying a Rabin condition\@. Thus a Rabin measure expresses
closeness to satisfaction of the Rabin condition in the same way a
well-founded set expresses closeness to program termination\@.
%
\apar{1-4}
The main result of our paper is that a graph satisfies a Rabin
condition if and only if it has a Rabin measure\@. Although this is not
surprising from a recursion-theoretic point of view (the problem is
complete for \(\Pi^1_1\)), the result is important because Rabin
measures can be used to verify properties expressible by temporal
formulas in a certain disjunctive normal form\@. Previous research has
concentrated on temporal formulas in conjunctive form; such formulas
can be verified by verifying each conjunct separately\@. Disjunctive
formulas are significantly more difficult, and no system to date has
been able to handle them without transformations\@.
%
\apar{1-5} 
Our treatment exhibits a link between verification with Rabin
conditions and certain constructs in classical recursion theory\@.
Specifically, we show that the transfinite well-orders that arise in
such verification problems are all obtained in a natural way, as the
Kleene-Brouwer ordering on the set of paths in certain finite-path
trees\@. The ``helpful directions'' (see~\cite{cj95-03-8}) arise simply and
naturally in this context and can be explained completely in these
terms\@.
%
\apar{1-6}
Rabin measures are useful for studying automata on infinite objects\@.
In~\cite{cj95-03-16}, it is shown how the concept can be used to
complement Streett automata on infinite words\@. For automata on
infinite trees, the results of the present article are used to
establish that complementation can take place with only an exponential
blow-up~\cite{cj95-03-19}\@. These applications rely on the
relationship to the Kleene-Brouwer ordering, and do not follow from
previous attempts at explaining progress for Rabin conditions\@.
%
\asection{2}{Related Work}
%
\apar{2-1}
Alpern and Schneider~\cite{cj95-03-1,cj95-03-2} used deterministic
B\"uchi automata as a specification method\@. They obtained a
verification method for nondeterministic B\"uchi automata using the
fact that every such automaton can be converted to a Boolean
combination, in conjunctive normal form, of deterministic B\"uchi
automata\@. Vardi~\cite{cj95-03-34} proposed \emph{rank predicates} as
a very general approach to verification, where specifications were
subjected to certain automata-theoretic transformations\@. The
resulting automata define incorrect computations and have a
B\"uchi-type acceptance condition, which yields an explanation of
helpful directions for the transformed verification problem\@.
\ifx\customadjust\undeftex\else\customadjust\fi
%
\apar{2-2}
Inspired by the ideas in~\cite{cj95-03-34}, Manna and Pnueli gave
verification conditions for
\(\forall\)-automata~\cite{cj95-03-24}\@. These conditions are
expressively equivalent to B\"uchi automata, although there is no
known easy conversion of a B\"uchi automaton into a
\(\forall\)-automaton\@. Sistla \cite{cj95-03-32} considered deterministic
automata with acceptance conditions given as temporal formulas on
automaton states with the modalities \(F^\infty(f)\) (infinitely often
\(f\)) and \(G^\infty(f)\) (almost always \(f\))\@. He showed that
sound and complete verification conditions exist for automata that are
in a special conjunctive normal form in which each conjunct is a
particularly simple disjunction\@.
%
\apar{2-3}
For temporal logic specifications, assertional proof methods such
as~\cite{cj95-03-23,cj95-03-27} are limited to quite
simple temporal formulas that express properties like ``leads to'' and
``always\@.'' A general approach to verification with finite temporal
formulas was proposed in~\cite{cj95-03-29}\@. It is based on
establishing a direct correspondence between the program and the
temporal formula, assigning a well-founded ordering to every program
state\@. The verification conditions depend on inductively defined
predicates on temporal formulas, and are rather complicated\@.
%
\apar{2-4}
In the area of fairness, complete verification methods for termination
were given
in~\cite{cj95-03-9,cj95-03-8,cj95-03-10,cj95-03-22,cj95-03-21,cj95-03-33}\@.
These methods are based on \emph{helpful directions}, and on the
iterative use of proof rules applied to syntactically transformed
programs\@. In~\cite[Section 2.1]{cj95-03-8}, a variation of this method
based on relativizing the proof rules to state predicates is
presented\@. This avoids syntactic transformations, but the method is
still dependent on repeated applications of proof rules\@. Similarly,
the ranking arguments in~\cite{cj95-03-6} are
iterative\@. In both cases, our Rabin measures may be viewed as
arranging the information of all steps into one mathematical
structure\@. Explicit ranks for the \emph{parity
condition}~\cite{cj95-03-26} (which is a restricted kind of Rabin
condition) were defined in~\cite{cj95-03-7}\@.
%
\apar{2-5}
The methods of \emph{explicit schedulers} developed
in~\cite{cj95-03-3,cj95-03-4,cj95-03-5} involve
transforming programs by adding auxiliary variables that are
nondeterministically assigned values determining fair computations\@.
For an extensive treatment of fairness based on helpful directions and
explicit schedulers, see~\cite{cj95-03-8}\@.
%
\apar{2-6}
The shuffling of colors in a Rabin measure is reminiscent of the {\em
Later Appearance Record} of~\cite{cj95-03-11}, which is used
to explain how certain restricted memory strategies arise for infinite
games played according to a Muller acceptance condition\@.
In~\cite{cj95-03-19}, it is shown how Rabin measures yield
memory-less strategies for games with Rabin winning conditions\@.
%
\apar{2-7}
\emph{Progress measures} were introduced in~\cite{cj95-03-13} as a
generic concept for quantifying how each step of a program contributes
to bringing a computation closer to its specification, given in terms
of a limit condition\@. There it is shown that progress measures exist
for a variety of program specifications, including those involving
nondeterminism, fairness, and infinitary temporal logics\@. For the
general setting of the verification problem as studied
in~\cite{cj95-03-34}, rank predicates and progress measures are essentially
equivalent~\cite{cj95-03-35} and their existence is in essence
expressed by the Kleene-Suslin Theorem of descriptive set
theory~\cite{cj95-03-18}\@.
%
\apar{2-8}
The paper~\cite{cj95-03-17} reformulates the notion of Rabin measure
presented here, so that it can be better used in program
verification\@. Also, the completeness proof presented
in~\cite{cj95-03-17} is simplified for the case that the underlying
program contains no cycles\@.
%
\apar{2-9}
The verification method in~\cite{cj95-03-15} is based on the liminf
concept, and also involves a variation on the Kleene-Brouwer
ordering\@. Although applicable to a larger class of properties (in
terms of the Borel classification), this method is dependent on
characterizing finite computations, not states, and cannot be used
without introducing history information\@. The method of
\cite{cj95-03-15} can be extended to general simulation and
bisimulation concepts~\cite{cj95-03-18}\@.
%
\asection{3}{Rabin Conditions}
%
\apar{3-1}
A \emph{graph} \(G=(V,E)\) consists of a countable set of vertices (or
states) \(V\) and a set of directed edges \(E\subseteq V\times V\)\@.
A \emph{Rabin pair} \((R, I)\) on \(V\) consists of a set
\(R \subseteq V\) of \emph{reconfirming} states and a set
\(I\subseteq V\) of \emph{invalidating} states\@. We say that an
infinite sequence \(v_0,v_1,\ldots\) of states \emph{satisfies}
\((R,I)\), and we write \(v_0,v_1,\ldots\satisfy(R,I)\), if there are
infinitely many \(k\) such that \(v_k\in R\) and only finitely many
\(k\) such that \(v_k\in I\)\@.
%
\apar{3-2}
A \emph{Rabin condition} (or \emph{Rabin assignment}) \(\Rabcond{C}\)
is a set \(\setof{(R_\chi,I_\chi)}{\chi\in X}\) of Rabin pairs\@. Here
\(X\) is a finite set of \emph{colors}, and Rabin pair
\((R_\chi,I_\chi)\) is said to have color \(\chi\)\@. We assume that no
pair in \(\Rabcond{C}\) is repeated, and say that
\(\setsize{\Rabcond{C}}=\setsize{X}\) is the \emph{size} of
\(\Rabcond{C}\)\@. The set \(R_\chi\) is the set of
\(\chi\)-reconfirming states, and \(I_\chi\) is the set of
\(\chi\)-invalidating states\@. For technical reasons, we always assume
without loss of generality that \(0\in X\) and that \(I_0=\emptyset\)
(one can always add the pair \((\emptyset,\emptyset)\) without
changing the semantics of satisfaction defined next)\@. We say that an
infinite sequence \(v_0,v_1,\ldots\) \emph{satisfies} \(\Rabcond{C}\),
and we write \(v_0,v_1,\ldots\satisfy\Rabcond{C}\), if for some
\(\chi\), \(v_0,v_1,\ldots\satisfy(R_\chi,I_\chi)\)\@. We say that a
graph \(G=(V,E)\) satisfies a Rabin condition \(\Rabcond{C}\) on
\(V\), and we write \(G\satisfy\Rabcond{C}\), if every infinite path
\(v_0,v_1,\ldots\) in \(G\) satisfies \(\Rabcond{C}\)\@.
%
\asection{4}{Pointer Trees}
%
\apar{4-1}
Rabin measures are based on pointer trees, also called direction
trees\@. Let \(\omega_1\) be the set of countable ordinals\@. A
\emph{pointer tree} \(T\) is a countable prefix-closed subset of
\(\omega_1^*\), the set of finite sequences of countable ordinals\@.
Each sequence \(t=\vect{t^1,\ldots,t^\ell}\) in \(T\) represents a
\emph{node}, which has \emph{children} \(t\concat\vect{d}\in T\), where
``\(\concat\)'' denotes concatenation of sequences\@. Here
\(d\in\omega_1\) is the \emph{pointer} to \(t\concat\vect{d}\) from
\(t\)\@. If \(t'\) is a prefix of \(t\in T\), then \(t'\) is called an
\emph{ancestor} of \(t\) and we write \(t'\pfleq t\)\@. We visualize
pointer trees as growing upward; see Figure~1, where
children are depicted from left to right in descending order\@.
%
\begin{figure*}
\begin{center}
%
\setlength{\unitlength}{0.00275em}%
\begin{picture}(2808,3440)(4243,-6394)
\put(4976,-3211){\circle{200}}
\put(5176,-3211){\makebox(0,0)[l]{\(\vect{1,0,2}\)}}
\put(5621,-4178){\line(-2,3){589}}
\put(5676,-4261){\circle{200}}
\put(5876,-4261){\makebox(0,0)[l]{\(\vect{1,0}\)}}
\put(4921,-5228){\line(-2,3){589}}
\put(5031,-5228){\line(2,3){589}}
\put(4976,-5311){\circle{200}}
\put(5176,-5311){\makebox(0,0)[l]{\(\vect{1}\)}}
\put(7225,-6361){\makebox(0,0)[l]{level \(0\)}}
\put(7225,-5311){\makebox(0,0)[l]{level \(1\)}}
\put(7225,-4261){\makebox(0,0)[l]{level \(2\)}}
\put(7225,-3211){\makebox(0,0)[l]{level \(3\)}}
\put(5085,-5881){\makebox(0,0)[l]{\(1\)}}
\put(4276,-4261){\circle{200}}
\put(4476,-4261){\makebox(0,0)[l]{\(\vect{1,2}\)}}
\put(5450,-3661){\makebox(0,0)[l]{\(2\)}}
\put(4976,-6253){\line(0,1){842}}
\put(4976,-6353){\circle{200}}
\put(5176,-6353){\makebox(0,0)[l]{\(\emptyvec\)}}
\put(4800,-4787){\makebox(0,0)[l]{\(2\)}}
\put(5500,-4794){\makebox(0,0)[l]{\(0\)}}
\end{picture}
\end{center}
\afigcap{1}{A pointer tree\@.}
\end{figure*}
%
Every sequence of pointers \(t^1,t^2,\ldots\) (finite or infinite)
denotes a \emph{path} \(\emptyvec,\vect{t^1},\vect{t^1,t^2},\ldots\)
(finite or infinite) in \(T\), provided each
\(\vect{t^1,\ldots,t^\ell}\in T\)\@. The \emph{level}
\(\nodelevel{t}\) of a node \(t=\vect{t^1,\ldots,t^l}\) is the number
\(l\); the level of \(\emptyvec\) is \(0\)\@. The \emph{prefix up to
level \(n\)} of \(t=\vect{t^1,\ldots,t^l}\) is
\(\vect{t^1,\ldots,t^{\min\{l,n\}}}\), denoted \(t\prefix n\)\@. The
\emph{height} of \(T\) is the maximum node level (if it
exists)\@. \(T\) is \emph{path-finite} if there are no infinite paths
in \(T\)\@. A \emph{common ancestor} of nodes \(t\) and \(t'\) is a
node \(\tilde{t}\) that is an ancestor of both of \(t\) and of
\(t'\)\@. The common ancestor at the highest level is the
\emph{highest common ancestor}, written \(t\hca t'\)\@.
%
\apar{4-2}
A simple but central lemma about the infinite sequences of nodes in a
pointer tree is:
%
\begin{alabsubtext}{Lemma}{1}{Highest Common Ancestor Lemma}
Let \(t_0, t_1,\ldots\) be an infinite sequence of nodes in a
path-finite pointer tree \(T\)\@. Then there is a node \(t\) that is
a common ancestor of \(t_k,t_{k+1}\) for almost all \(k\), and the
highest common ancestor for infinitely many \(k\)\@.
\end{alabsubtext}
\sentence
%
\begin{alabsubtext}{Proof of Lemma}{1}{}
\prooffontshape
%
Let \(T'\) be the set of nodes that are almost always ancestors of
\(t_k\)\@. Then \(T'\) contains \(\emptyvec\) and is linearly ordered
by the prefix relation, since for all \(t\), \(t'\) in \(T'\), there
eventually exists \(t_k\) such that both \(t\) and \(t'\) are
ancestors of \(t_k\), and the ancestors of every node are linearly
ordered\@. Since \(T\) contains only finite paths, \(T'\) has a unique
maximal element, which satisfies the desired conditions\@.
%
{\nopagebreakbeginpar\markendlst{}}
\end{alabsubtext}
%
\begin{alabsubtext}{Definition}{1}{Kleene-Brouwer Ordering}
The strict ordering \(\succ\) on \(T\) is defined by: \(t\succ t'\)
if and only if either \(t \pflt t'\), or else the highest common
ancestor of \(t\) and \(t'\) is at level \(l\), \(t^{l+1}\) and
\({t'}^{l+1}\) are defined, and \(t^{l+1}>{t'}^{l+1}\)\@. The nonstrict
ordering \(\succeq\) is defined as \(t\succeq t'\) if and only if
\(t\succ t'\) or \(t=t'\)\@.
\end{alabsubtext}
%
In other words \(t\succeq t'\) if \(t\) is an ancestor of \(t'\) or if
\(t'\) branches off to the right of \(t\) (assuming \(T\) is depicted
as in Figure~1\@). \(\succeq\) is a total order on \(T\)\@.
%
\begin{alabsubtext}{Lemma}{2}{Kleene-Brouwer Ordering Lemma}
If \(T\) is path-finite, then \(\succ\) is a well-ordering of \(T\)\@.
\end{alabsubtext}
%
\begin{alabsubtext}{Proof of Lemma}{2}{}
\prooffontshape
%
See~\cite{cj95-03-30} or use Lemma~1\@.
{\nopagebreakbeginpar\markendlst{}}
\end{alabsubtext}
%
\apar{4-3}
Rabin measures are based on coloring pointer trees\@.
%
\begin{alabsubtext}{Definition}{2}{}
A \emph{colored pointer tree} \((T,\xi)\) is a pointer tree \(T\) with
a partial mapping \(\xi\oftype\partfuncspace{T}{X}\), where \(X\) is a set of
\emph{colors}, assigning a color \(\xi(t)\in X\) to each node \(t\) in
\(\dom\xi\) so that:
%
\begin{itemize}
\item the root is colored \(0\), i.e., \(\xi(\emptyvec)=0\);
\item each node that is not a leaf receives some color; and
\item all colors along a path starting in the root are distinct\@.
\end{itemize}
%
\end{alabsubtext}
%
Thus, a colored pointer tree has height at most \(\setsize{X}\)\@.
%
\asection{5}{Rabin  Measures}
%
\apar{5-1}
A Rabin measure for a graph with a Rabin condition consists of a
colored pointer tree and a mapping that assigns a node in the tree to
each vertex in the graph\@. These nodes, or \emph{progress values},
quantify progress toward the Rabin condition if they are related in a
certain way on every transition\@.
%
\begin{alabsubtext}{Definition}{3}{}
Let \(G=(V,E)\) be a graph, and let
\(\Rabcond{C}=\setof{(R_\chi,I_\chi)}{\chi\in X}\) be a Rabin condition
on \(G\)\@. A \emph{Rabin progress measure} (or just \emph{Rabin
measure}) for \((G,\Rabcond{C})\) is a triple \((\mu,T,\xi)\), where
\(\mu\oftype\funcspace{V}{T}\) and \((T,\xi)\) is a colored pointer
tree, such that:
%
\begin{itemize}
\item[(I)] for all \(v\in V\) and all \(\chi\in\mu(v)\),
  \(v\notin I_\chi\), and
\item[(R)] for all \((u,v)\in E\), \(u\Rabinrel{\mu}v\),
\end{itemize}
%
where \(u\Rabinrel{\mu}v\) if and only if
\begin{itemize}
\item[] \(\mu(u)\succ\mu(v)\), or
\item[] there exists a common ancestor \(t\pfleq\xi(\mu(u)\hca\mu(v))\)
  such that \(v\in R_{\xi(t)}\)\@.
\end{itemize}
\end{alabsubtext}
%
The value \(\mu(v)\) designates a path in \(T\) from the root to the
node \(\mu(v)\)\@. The sequence of colors on this path indicates a
prioritization of hypotheses about Rabin pairs: The closer it is to
the bottom, the more likely a pair is to be the one satisfied in the
limit\@.
%
\apar{5-2}
Requirement (I) states that all hypotheses correspond to pairs that
are not invalidated\@. Requirement (R) states that on a transition from
\(u\) to \(v\), either the progress value decreases from \(u\) to
\(v\) or one of the pairs described by the common part of \(\mu(u)\)
and \(\mu(v)\) is reconfirmed\@. The colors at or below the highest
common ancestor indicate the ``helpful directions,'' that is, the
pairs that have been singled out for satisfaction in the limit\@. It is
shown below how (R) insures that some color is reconfirmed infinitely
often, and how (I) insures that the color is invalidated only finitely
many times\@.
%
\begin{figure*}
\begin{center}
%
\setlength{\unitlength}{0.00275em}
\begin{picture}(4487,2593)(1598,-3922)
\put(1876,-3311){\line(0,1){1300}}
\put(1876,-3661){\circle{700}}
\put(1876,-3661){\makebox(0,0){\(0\)}}
\put(1876,-1661){\circle{700}}
\qbezier(5573,-3442)(6573,-2661)(5573,-1908)
\put(5573,-1908){\vector(-1,1){0}}
{\thicklines\dottedline{50}(4976,-3661)(2226,-3661)}
\put(2226,-3661){\vector(-1,0){0}}
\put(5326,-3661){\circle{700}}
\put(5326,-3661){\makebox(0,0){\(\#\)}}
\put(5851,-3886){\makebox(0,0)[lb]{\(v_0\)}}
\put(2000,-2611){\makebox(0,0)[l]{\(0\)}}
\qbezier(5079,-3442)(4079,-2661)(5079,-1908)
\put(5079,-3442){\vector(1,-1){0}}
{\thicklines\dottedline{50}(4976,-1661)(2226,-1661)}
\put(2226,-1661){\vector(-1,0){0}}
\put(5326,-1661){\circle{700}}
\put(5851,-1886){\makebox(0,0)[lb]{\(v_1\)}}
\end{picture}
\end{center}
\afigcap{2}{A colored pointer tree and a graph with Rabin measure\@.}
\end{figure*}
%
\apar{5-3}
In Figure~2, we have shown a graph \(G\) (to the right) with vertices
\(v_0\) and \(v_1\)\@. The Rabin condition \(\Rabcond{C}\) of the
graph consists of the pair \((R_0,I_0)\), where the set \(X\) is
\(\{0\}\), and \(R_0=\{v_0\}\) consists of the node marked \(\#\), and
\(I_0=\emptyset\)\@. Thus, every infinite path in \(G\) runs through
a reconfirming state infinitely often, and
\(G\satisfy\Rabcond{C}\)\@. This fact can also be established by the
existence of a Rabin measure\@. We use the colored pointer tree shown
to the left\@. Its root is labeled with the color \(0\) and the node
\(\vect{0}\) is not labeled with a color\@. The measure is as
indicated by the dotted arrows, i.e.,\ \(\mu(v_0)=\emptyvec\) and
\(\mu(v_1)=\vect{0}\)\@. On the transition from \(v_0\) to \(v_1\),
the value of the measure decreases according to the Kleene-Brouwer
ordering, and on the transition from \(v_1\) to \(v_0\), the value of
the measure also decreases, since the root is a common ancestor with a
color that is reconfirmed\@.
%
\apar{5-4}
Another more complicated situation involving two colors
(\(X=\{0,1\}\)) is shown in Figure~3\@.
%
\begin{figure*}
\begin{center}
%
\setlength{\unitlength}{0.00275em}%
\begin{picture}(7262,5500)(848,-3893)
{\thicklines\bezier{160}(6779,661)(2530,2909)(282,-1339)}
\put(282,-1339){\vector(-2,-3){0}}
\put(7026,64){\vector(0,-1){1300}}
\put(7026,414){\circle{700}}
\put(7026,414){\makebox(0,0){\(-\)}}
\put(7626,714){\makebox(0,0)[lb]{\(v_3\)}}
{\thicklines\dottedline{50}(6676,-3586)(1736,-3586)}
\put(1736,-3586){\vector(-1,0){0}}
\qbezier(7273,-3339)(9026,-1886)(7273,167)
\put(7273,167){\vector(-1,1){0}}
\put(7026,-3586){\circle{700}}
\put(7026,-3586){\makebox(0,0){\(\#\)}}
\put(7626,-3886){\makebox(0,0)[lb]{\(v_0\)}}
\put(1562,-3295){\line(2,3){945}}
\put(1174,-3295){\line(-2,3){945}}
\put(1368,-3586){\circle{700}}
\put(1368,-3586){\makebox(0,0){\(0\)}}
\put(2701,-1236){\line(0,1){1300}}
\put(2701,-1586){\circle{700}}
\put(2701,-1586){\makebox(0,0){\(1\)}}
\put(35,-1586){\circle{700}}
\put(2701,414){\circle{700}}
{\thicklines\dottedline{50}(4676,-1586)(3051,-1586)}
\put(3051,-1586){\vector(-1,0){0}}
\qbezier(5273,-1339)(6026,-586)(6779,-1339)
\put(6779,-1339){\vector(1,-1){0}}
\put(5026,-1586){\circle{700}}
\put(5026,-1586){\makebox(0,0){\(+\)}}
\put(4501,-1886){\makebox(0,0)[rb]{\(v_1\)}}
{\thicklines\bezier{85}(6889,-1264)(5863,1576)(2948,661)}
\put(2948,661){\vector(-2,-1){0}}
\put(7026,-1936){\vector(0,-1){1300}}
\qbezier(5273,-1833)(6026,-2586)(6779,-1833)
\put(5273,-1833){\vector(-1,1){0}}
\put(7026,-1586){\circle{700}}
\put(7626,-1886){\makebox(0,0)[lb]{\(v_2\)}}
\put(900,-2586){\makebox(0,0)[l]{\(1\)}}
\put(2200,-2586){\makebox(0,0)[l]{\(0\)}}
\put(2836,-586){\makebox(0,0)[l]{\(0\)}}
\end{picture}
\end{center}
\afigcap{3}{Tree, graph, measure, with two nontrivial colors\@.}
\end{figure*}
%
Here \(R_0=\{v_0\}\), \(I_0=\emptyset\), \(R_1=\{v_1\}\) (the node
marked \(+\)), and \(I_1=\{v_3\}\) (the node marked \(-\))\@.
%
\apar{5-5}
The main result of this article is:
%
{\nopagebreakbeginpar
\begin{alabsubtext}{Theorem}{1}{}
\(G\satisfy\Rabcond{C}\) if and only if \((G,\Rabcond{C})\) has a
Rabin measure\@.
\end{alabsubtext}
\sentence
}
%
\begin{alabsubtext}{Proof of Theorem}{1 (\protect\(\logicimplied\protect\))}{}
\prooffontshape
%
\apar{Proof of Theorem 1-1}
Let \(v_0,v_1,\ldots\) be an infinite path in \(G\) and let
\(t_k=\mu(v_k)\)\@. By Lemma~1 (Highest Common Ancestor), there is a
node \(t\) that is (a) almost always a common ancestor and (b)
infinitely often the highest common ancestor of \(t_k,t_{k+1}\)\@. Let
\(l=\nodelevel{t}\)\@. Next, we prove that there exists
\(\hat{t}\pflt t\) such that \(v_0,v_1,\ldots\) satisfies the Rabin
pair \((R_{\xi(\hat{t}\hatparenskip)},I_{\xi(\hat{t}\hatparenskip)})\)\@.
%
\apar{Proof of Theorem 1-2}
First, assume for a contradiction that for all \(\hat{t}\pfleq t\),
\(v_k\in R_{\xi(\hat{t}\hatparenskip)}\) holds only finitely
often\@. Thus by (a) there is a \(K\) such that for all \(k\geq K\),
either (1) there is a \(t_{k}'\) with
\(t\pflt t_k'\pfleq t_k\hca t_{k+1}\) and with
\(v_k\in R_{\xi(t_{k}')}\), or (2) \(t_k\succ t_{k+1}\)\@.
%
\apar{Proof of Theorem 1-3}
In case (1), \(t_k,t_{k+1}\pfgt t\) and
\(t_k\prefix(l+1)=t_{k+1}\prefix(l+1)\)\@. In case (2), which holds
infinitely often by assumption and by (b),
\(t_k\prefix(l+1)\succ t_{k+1}\prefix(l+1)\), since \(t_k\succ t_{k+1}\)
and \(t\) is the highest common ancestor of \(t_k\) and
\(t_{k+1}\)\@. Thus
\(t_K\prefix(l+1)\succeq t_{K+1}\prefix(l+1)\succeq\cdots\) and
infinitely many inequalities are strict\@. This contradicts the
Kleene-Brouwer Ordering Lemma\@. Thus it holds infinitely often that
\(v_k\in R_{\xi(\hat{t}\hatparenskip)}\) for some \(\hat{t}\pfleq t\)\@.
%
\apar{Proof of Theorem 1-4}
Second, by (I) it follows that \(v_k\notin
I_{\xi(\hat{t}\hatparenskip)}\) holds from some point on due to~(a)\@.
{\nopagebreakbeginpar\markendlst{Proof of Theorem 1
(\(\logicimplied\))}}
\end{alabsubtext}
%
We prove the \((\logicimplies)\) portion in Section~6.3\@.
%
\asection{6}{Construction of Rabin Measures}
%
\apar{6-1}
We show how to construct a Rabin measure for \((G,\Rabcond{C})\),
where \(G=(V,E)\) is a graph that satisfies a Rabin condition
\(\Rabcond{C}=\setof{(R_\chi,I_\chi)}{\chi\in X}\)\@.
%
\asubsection{6.1}{Color Set Assignments}
%
\apar{6.1-1}
We need some definitions before stating a key lemma\@. Let
\(\powerset{C}\) denote the class of subsets of \(C\)\@. A \emph{color
set assignment} is a map
\(\colsetasgn{CS}\oftype\funcspace{V}{\powerset{C}}\), where \(C\) is
a countable set of colors; \({\colsetasgn{CS}}\hatparenskip\)
associates a nonempty set of \emph{enabled} colors
\({\colsetasgn{CS}}(v)\subseteq C\) to each vertex \(v\in V\)\@. A set
\(W\subseteq V\) is \emph{\(\chi\)-enabled} if and only if, for all
\(v\in W\), \(\chi\in\colsetasgn{CS}(v)\)\@. An infinite path
\(v_0,v_1,\ldots\) is \emph{eventually \(\chi\)-enabled} if and only
if there is a \emph{\(\chi\)-enabled} suffix
\(v_k,v_{k+1},\ldots\)\@. A color set assignment is \emph{permissible}
if and only if every infinite path is eventually \(\chi\)-enabled for
some~\(\chi\)\@.
%
\apar{6.1-2}
The set of \emph{descendants} \(\Rabcond{R}(v)\) of a vertex \(v\) in
a graph \(G\) is the set of all \(v'\) such that there is path from
\(v\) to \(v'\)\@. Note that \(v\in\Rabcond{R}(v)\)\@. The key lemma~is:
%
\begin{alabsubtext}{Lemma}{3}{}
Let \(G=(V,E)\) be a countable graph\@. If
\(\colsetasgn{CS}\oftype\funcspace{V}{\powerset{C}}\) is a permissible
color set assignment, then there is a vertex \(v\) and a color
\(\chi\) such that \(\Rabcond{R}(v)\) is \(\chi\)-enabled\@.
\end{alabsubtext}
\sentence
%
Before proving the lemma, we recall that a set \(Z\) is \emph{nowhere
dense} if there is no nonempty open set \(O\) such that
\(O\setintsct Z\) is dense in \(O\)\@. We will use:
%
\begin{alabsubtext}{Theorem}{2}{The Baire Category Theorem}
Let \(M\) be a complete metric space\@. Then \(M\) is not a countable
union of nowhere-dense sets\@. In particular, \(M\) is not a countable
union of closed sets that contain no basic open sets\@.
\end{alabsubtext}
\sentence
%
\begin{alabsubtext}{Proof of Lemma}{3}{}
\prooffontshape
%
\apar{Proof of Lemma 3-1}
For every finite path \(u\) in \(G\), define \(B_u\) and \(M\) by
%
\begin{eqnarray*}
B_u & = & \setof{u\concat w}{u\concat w 
  \mbox{ is a path (finite or infinite) in }G}\\
M & = & \setof{w}{w\mbox{ is a path (finite or infinite) in }G}
\end{eqnarray*}
\sentence
%
\apar{Proof of Lemma 3-2}
The \(B_u\)s form a subbasis for a topology over \(M\), where the open
sets are unions of \(B_u\)s\@. \(M\) is a complete metric
space\@.\footnote{%
The metric can be given, for example, as:
%
\[
d(w,w')=
  \condval{%
    0 & \mbox{if }w=w'\\
    1/i & \mbox{if }w_i\neq w'_i\mbox{ and }w_j=w'_j\mbox{ for }1\leq j<i\\
    1/(i+1) & \mbox{if }w\mbox{ is a prefix of }w'\mbox{ of length }i\\
    1/(i+1) & \mbox{if }w'\mbox{ is a prefix of }w\mbox{ of length }i
  }
\]
\sentence
}
%
\apar{Proof of Lemma 3-3}
For a finite path \(u\) in \(G\), and for \(\chi\in C\), define the
set
\[F_{u,\chi}=\setof{u\concat w}{w\mbox{ is \(\chi\)-enabled}}\]
which is closed\@. Every finite path \(u\) is contained in
\(F_{u,\chi}\) for all \(\chi\), and every infinite path \(w\) is in
\(F_{u,\chi}\), for some \(u\) and \(\chi\), by the assumption that
\(w\) is eventually \(\chi\)-enabled\@. Thus
\(M=\bigcup_{u,\chi}F_{u,\chi}\)\@.
%
\apar{Proof of Lemma 3-4}
By the Baire Category Theorem, some \(F_{u,\chi}\) contains a basic
open set, i.e., contains some \(B_v\)\@. Consequently,
\(\Rabcond{R}(v)\) is \(\chi\)-enabled\@.
{\nopagebreakbeginpar\markendlst{Proof of Lemma 3}}
\end{alabsubtext}
%
\asubsection{6.2}{Colorings}
%
\apar{6.2-1}
Lemma~3 can be applied transfinitely to a graph to yield a stronger
result\@. We need a few definitions\@. Let \(C\) be a countable set of
colors\@. A \emph{\(C\)-coloring} \(c\) of a set \(V\) is a total
mapping \(c\oftype\funcspace{V}{C}\)\@. A coloring \(c\) \emph{obeys}
a color set assignment \(\colsetasgn{CS}\) if and only if, for all
\(v\in V\), \(c(v)\in \colsetasgn{CS}(v)\)\@. An infinite path
\(v_0,v_1,\ldots\) is \emph{eventually \(\chi\)-stable} with respect
to \(c\), where \(\chi\in C\), if for almost all \(i\),
\(c(v_i)=\chi\)\@. A coloring \(c\) is \emph{eventually stable} if
every infinite path is eventually \(\chi\)-stable for some \(\chi\)\@.
A set \(W\subseteq V\) is \emph{monochromatic} with respect to \(c\)
if there is \(\chi\in C\) such that for all \(v\in W\),
\(c(v)=\chi\)\@.
%
\begin{alabsubtext}{Lemma}{4}{}
%
Let \(G=(V,E)\) be a graph\@. If \(\colsetasgn{CS}\) is a
permissible color set assignment, then there is an eventually stable
coloring \(c\oftype\funcspace{V}C\) obeying \(\colsetasgn{CS}\) and
a partition \(\Rabcond{S}=\setof{W_\theta}{\theta<\gamma}\) of \(V\),
where \(\gamma\) is a countable ordinal, such that:
%
\begin{itemize}
\item[(a)] each \(W_\theta\) is monochromatic; and
\item[(b)] if \((v,v')\in E\), \(v\in W_\theta\), and
  \(v'\in W_{\theta'}\), then \(\theta\geq\theta'\)\@.
\end{itemize}
\end{alabsubtext}
%
\begin{alabsubtext}{Proof of Lemma}{4}{}
\prooffontshape
%
{\sloppy
\apar{Proof of Lemma 4-1}
We apply Lemma~3 transfinitely\@. More precisely, Lemma~3 is first
applied to yield a vertex \(v\) in \(G\) such that \(\Rabcond{R}(v)\)
is \(\chi\)-enabled for some~\(\chi\)\@. Define \(W_0=\Rabcond{R}(v)\)
and \(c(v)=\chi\) for \(v\in W_0\)\@. Then remove \(W_0\) from \(G\)
and apply Lemma~3 again to define \(W_1\) in a similar manner\@. By
transfinite induction, this process induces a partition of \(G\) into
\(\gamma\) classes, where \(\gamma\) is a countable ordinal\@.
}
%
\apar{Proof of Lemma 4-2}
Then (a) is satisfied according to the definition of \(c\)\@. Also,
(b) is satisfied, because every vertex is removed along with all its
successors in the remaining graph\@.
{\nopagebreakbeginpar\markendlst{Proof of Lemma 4}}
\end{alabsubtext}
%
\asubsection{6.3}{Proof of Theorem~1 (\protect\(\logicimplies\protect\))}
%
\apar{6.3-1}
\begin{alabsubtext}{Proof of Theorem}{1 (\protect\(\logicimplies\protect\))}{}
\prooffontshape
%
\apar{Proof of Theorem 1-5}
Let \(G=(V,E)\) be a graph that satisfies a finite Rabin condition
\(\Rabcond{C}\)\@. To construct a measure \((\mu,(T,\xi))\) of
\((G,\Rabcond{C})\), we use the algorithm \(\prog{AssignRabin}\) in
Figure~4\@.
%
\begin{figure*}
\fbox{\parbox[t]{\textwidth}{%
\begin{algorithm}{informal}{}
\(\prog{AssignRabin}(t,Y,\chi):\)
%
\begin{enumerate}
%
\item[1.] \(\xi(t)\assigned\chi\)
%
\item[] \(\widehat{W}\assigned W(t)\setdiff R_\chi\) 
%
\item[2.] Use Lemma~4 on \(G\setdiff\widehat{W}\) with color set
assignment \(\colsetasgn{CS}^{\setcomp{Y\setunion\{\chi\}}}\)
(explained in the text) to obtain a coloring \(c\) and a partition
\(\Rabcond{S}=\setof{W_\theta}{\theta<\gamma}\) of \(\widehat{W}\).
%
\item[3.] For each class \(W_\theta\) of \(\Rabcond{S}\):
%
\begin{enumerate}
%
\item[(a)] \(T\assigned T\setunion\{t\concat\vect{\theta}\}\)
%
\item[(b)] \(W({t\concat\vect{\theta}})\assigned W_\theta\)
%
\end{enumerate}
%
\item[4.] For each \(\chi'\)-colored class \(W_\theta\) of
  \(\Rabcond{S}\), where \(\chi'\in X\):
%
\begin{enumerate}
%
\item[] \(\prog{AssignRabin}(t\concat\vect{\theta},Y\setunion\{\chi\},\chi')\)
%
\end{enumerate}
\end{enumerate}
\end{algorithm}
%
}}
\afigcap{4}{Algorithm \protect\(\prog{AssignRabin}\protect\)\@.}
%
\end{figure*}
%
The algorithm builds the tree \((T,\xi)\) and labels each node
\(t\neq\emptyvec\) of \(T\) with a set \(W(t)\subseteq V\), which is
to be the set of vertices mapped by \(\mu\) to nodes having \(t\) as
an ancestor\@. The purpose of \(\prog{AssignRabin}(t, Y, \chi)\) is to
assign color \(\chi\) to node \(t\) and to define the children
\(t\concat\vect{\theta}\) of node \(t\)\@. Each child receives a label
\(W(t\concat\vect{\theta})\), which is a subset of \(W(t)\)\@. The set
\(Y\) denotes the colors that have already been assigned to the proper
ancestors of \(t\)\@.
%
\apar{Proof of Theorem 1-6}
\begin{itemize}
%
\item Initially, \(\prog{AssignRabin}\) is applied with parameters
  \((\emptyvec,\emptyset, 0)\), and the tree \(T\) consists of only the
  root \(\emptyvec\) with label \(W(\emptyvec)=V\)\@.
%
\item In Step 1 of \(\prog{AssignRabin}\), node \(t\) is assigned color
  \(\chi\), and \(\widehat{W}=W(t)\setdiff R_\chi\) is the set of
  states in \(W(t)\) that are not \(\chi\)-reconfirming\@.
%
\item In Step 2, Lemma~4 is used to obtain a partition
  \(\Rabcond{S}=\setof{W_\theta}{\theta<\gamma}\) of \(\widehat{W}\) and
  a coloring \(c\) of \(\widehat{W}\)\@. Informally, the color set
  assignment \(\colsetasgn{CS}^{\setcomp{Y\setunion\{\chi\}}}\)
  expresses the set of colors that are not invalidating and that have
  not already been considered\@. More precisely, the color set assignment
  \(\colsetasgn{CS}^{\setcomp{Y\setunion\{\chi\}}}\) assigns to vertex
  \(v\) the set of colors \(\chi'\in X\) such that
  \(\chi'\notin Y\setunion\{\chi\}\) and \(v\notin I_{\chi'}\); however,
  if this set is empty, then the color set assigned is \(\{\bot_v\}\),
  where \(\bot_v\) is a distinct dummy color, different from any color
  defined elsewhere\@. Thus the set \(C\) of all colors is
  \(X\setunion\setof{\bot_v}{v\in V}\)\@.
%
\item In Step 3, a child \(t\concat\vect{\theta}\) is added to \(t\) for
  each class \(W_\theta\) of \(\Rabcond{S}\) and
  \(t\concat\vect{\theta}\) is labeled \(W_\theta\)\@.
%
\item Finally, in Step 4, descendants of each child not assigned a dummy
  color are constructed by further applications of \(\prog{AssignRabin}\)\@.
%
\end{itemize}
%
\apar{Proof of Theorem 1-7}
To explain the construction of \(\mu\) and to prove that Lemma~4 can
indeed always be used in Step 2, we need some terminology\@. We say
that a subset \(W\subseteq V\) is \emph{\(\chi\)-non\-recon\-firm\-ing} if
\(W\setintsct R_\chi=\emptyset\) and that \(W\) is
\emph{\(\chi\)-non\-inval\-idat\-ing} if \(W\setintsct I_\chi=\emptyset\)\@.
A subset \(W\subseteq V\) is \emph{\(Y\)-non\-recon\-firm\-ing} if it is
\(\chi\)-non\-recon\-firm\-ing for each \(\chi\) in \(Y\)\@. Similarly, a
subset \(W\subseteq V\) is \emph{\(Y\)-non\-inval\-idat\-ing} if it is
\(\chi\)-non\-inval\-idat\-ing for each \(\chi\) in \(Y\)\@.
%
\begin{alabsubtext}{Claim}{1}{}
{\sloppy
For each application of the inductive procedure
\(\prog{AssignRabin}(t,Y,\chi)\) starting with
\(\prog{Assign\-Rabin}(\emptyvec,\emptyset,0)\), the following hold:
%
\begin{itemize}
\item \(Y\subseteq X\) and \(\setsize{Y}=\nodelevel{t}\);
\item \(\chi\in X\setdiff Y\); 
\item \(W(t)\) is \(Y\)-non\-recon\-firm\-ing; and
\item \(W(t)\) is \((Y\setunion\{\chi\})\)-non\-inval\-idat\-ing\@.
\end{itemize}
}
\end{alabsubtext}
%
\begin{alabsubtext}{Proof of Claim}{1}{}
{\sloppy
\prooffontshape
%
\apar{Proof of Claim 1-1}
(By induction) This is true for the first application
\(\prog{AssignRabin}(\emptyvec,\emptyset,0)\)
because
\(\setsize{Y}=\setsize{\emptyset}=\nodelevel{\emptyvec}=\nodelevel{t}=0\);
\(\chi=0\); and \(W(t)=W(\emptyvec)=V\), which is
\(\emptyset\)-non\-recon\-firm\-ing and, since \(I_0=\emptyset\),
\(\{0\}\)-non\-inval\-idat\-ing\@.
%
\apar{Proof of Claim 1-2}
When
\(\prog{AssignRabin}(t\concat\vect{\theta},Y\setunion\{\chi\},\chi')\)
is applied from within \(\prog{AssignRabin}\) in Step 4, it may be
assumed by the induction hypothesis that
\(\setsize{Y}=\nodelevel{t}\), \(\chi\in X\setdiff Y\), and \(W(t)\)
is \((Y\setunion\{\chi\})\)-non\-inval\-idat\-ing and
\(Y\)-non\-recon\-firm\-ing\@.
%
\apar{Proof of Claim 1-3}
It follows that \(Y\setunion\{\chi\}\subseteq X\) and
\(\setsize{Y\setunion\{\chi\}}=\nodelevel{t\concat\vect{\theta}}\)\@.
Also, by definition of the color set assignment in Step 2,
\(\chi'\in X\setdiff(Y\setunion\{\chi\})\)\@. Furthermore, since
\(W_\theta\) is \(\chi'\)-non\-inval\-idat\-ing by this definition,
\(W_\theta\) is
\((Y\setunion\{\chi\}\setunion\{\chi'\})\)-non\-inval\-idat\-ing\@.
Finally, since \(W_\theta\) is \(\chi\)-non\-recon\-firm\-ing (because
\(W_\theta\subseteq\hatcapstrut\widehat{W}=W\setdiff R_\chi\)), it follows that
\(W(t\concat\vect{\theta})=W_\theta\) is
\((Y\setunion\{\chi\})\)-non\-recon\-firm\-ing\@.
}
{\nopagebreakbeginpar\markendlst{Proof of Claim 1}}
\end{alabsubtext}
%
\apar{Proof of Theorem 1-8}
To see that Lemma~4 is applicable in Step 2 of \(\prog{AssignRabin}\),
we prove:
%
\begin{alabsubtext}{Claim}{2}{}
%
{\sloppy
In every application of \(\prog{AssignRabin}\),
\(\colsetasgn{CS}^{\setcomp{Y\setunion\{\chi\}}}\) is permissible for
\(\hatcapstrut\widehat{W}\); in fact, every infinite path in \(W\) is
eventually \(\widehat{\chi}\)-enabled for some
\(\widehat{\chi}\in X\setdiff(Y\setunion\{\chi\})\)\@.
}
\end{alabsubtext}
\sentence
%
\begin{alabsubtext}{Proof of Claim}{2}{}
{\sloppy
\prooffontshape
%
\apar{Proof of Claim 2-1}
Consider an application \(\prog{AssignRabin}(t,Y,\chi)\)\@. By
Claim~1, it follows that \(\hatcapstrut\widehat{W}\) defined in Step~1 of
\(\prog{AssignRabin}\) is \((Y\setunion\{\chi\})\)-non\-inval\-idat\-ing and
\((Y\setunion\{\chi\})\)-non\-recon\-firm\-ing\@. Now let \(v_0,v_1,\ldots\)
be an infinite path in \(\hatcapstrut\widehat{W}\)\@. It is
\((Y\setunion\{\chi\})\)-non\-recon\-firm\-ing because
\(\hatcapstrut\widehat{W}\) is
\((Y\setunion\{\chi\})\)-non\-recon\-firm\-ing\@. Hence by the assumption
that \(G\satisfy\Rabcond{C}\),
\(v_0,v_1,\ldots\satisfy(R_{\hat{\chi}},I_{\hat{\chi}})\) for some
\(\hat{\chi}\in X\setdiff(Y\setunion\{\chi\})\)\@. In particular,
\(v_0,v_1,\ldots\) is eventually \(\hat{\chi}\)-enabled with respect
to the color set assignment
\(\colsetasgn{CS}^{\setcomp{Y\setunion\{\chi\}}}\) of
\(\hatcapstrut\widehat{W}\)\@.
}
{\nopagebreakbeginpar\markendlst{Proof of Claim 2}}
\end{alabsubtext}
%
\apar{Proof of Theorem 1-9}
Now, to show that all nodes constructed are at level
\(\leq\setsize{X}=\setsize{\Rabcond{C}}\), we note that if
\(\nodelevel{t}=\setsize{X}-1\), then since
\(\setsize{Y}=\nodelevel{t}\) and \(\chi\notin Y\) (by Claim~1,
\(Y\setunion\{\chi\}=X\))\@. In that case, the color set assignment of
Step 2 assigns to each vertex \(v\) only the dummy color \(\bot_v\);
thus, \(\prog{AssignRabin}\) is not further applied in Step 4\@. It
follows that \(\prog{AssignRabin}\) defines a tree \(T\) of height at
most \(\setsize{X}\)\@. The tree has the following properties:
%
\begin{alabsubtext}{Claim}{3}{}
%
\begin{enumerate}
%
\item[(a)] For every \(t\in T\) with \(\nodelevel{t}<\setsize{X}\),
  \[\setof{W(t\concat\vect{\theta})}{t\concat\vect{\theta}\in T}\]
  is a partition of \(W(t)\setdiff R_{\xi(t)}\)\@.
%
\item[(b)] For each \(v \in V\) there is a unique maximal list
  \(t=\vect{t^1,\ldots,t^n}\) with \(1\leq n\leq\setsize{X}\) such that
  \(v\in W(t)\)\@.
%
\end{enumerate}
\end{alabsubtext}
\sentence
%
\begin{alabsubtext}{Proof of Claim}{3}{}
\prooffontshape
% 
(a) holds for \(t=\emptyvec\), because \(W(\emptyvec)=V\) and
\(\hatcapstrut\widehat{W}\) formed in \(\prog{AssignRabin}\) is
\(W(\emptyvec)\setdiff R_{\xi(\emptyvec)}\)=\(V\setdiff R_0\); thus
Lemma~4 in Step 2 and the definition of children in Step 4 yield a
partition \(\setof{W(\vect{\theta})}{\vect{\theta}\in T}\) of
\(W(\emptyvec)\setdiff R_{\xi(\emptyvec)}\)\@. Similarly, by
induction it can been seen that (a) holds for all \(t\in T\) with
\(\nodelevel{t}<\setsize{X}\)\@.
%
Part (b) follows from (a)\@.
{\nopagebreakbeginpar\markendlst{Proof of Claim 3}}
\end{alabsubtext}
%
\apar{Proof of Theorem 1-10}
Using Claim~3b, we define \(\mu\oftype\funcspace{V}{T}\) by
\(\mu(v)=\vect{t^1,\ldots,t^n}\)\@. Now let us prove that (I) and (R)
are satisfied\@.
%
\begin{itemize}
\item[(I)] Note that if \(t\pfleq\mu(v)\) and \(\chi=\xi(t)\) is
  defined, then by Claim~1, \(W(t)\) is \(\chi\)-non\-inval\-idat\-ing\@. Thus
  in particular, \(v\notin I_{\chi}\)\@.
%
\item[(R)] Let \((u,v)\in E\)\@. If there is a color \(\chi\) of a
  common ancestor of \(\mu(u)\) and \(\mu(v)\) such that
  \(v\in R_{\chi}\), then (R) is trivially satisfied\@. So we may
  assume that for the highest common ancestor \(\hat{t}\),
  \(v\notin R_{\xi(\hat{t}\hatparenskip)}\)\@. Then
  \(\nodelevel{\mu(v)}>\nodelevel{\hat{t}}\) by Claim~3a\@. Consider
  the application
  \(\prog{AssignRabin}(\hat{t},Y,\xi(\hat{t}\hatparenskip))\)\@.
  \par If \(u\in R_{\xi(\hat{t}\hatparenskip)}\), then
  \(\mu(u)=\hat{t}\) because
  \(u\notin\widehat{W}=W(t)\setdiff R_{\xi(\hat{t}\hatparenskip)}\)\@. Thus
  \(\mu(u)=\hat{t}\succ\mu(v)\), because
  \(\nodelevel{\mu(v)}>\nodelevel{\hat{t}}\)\@. Otherwise, if
  \(u\notin R_{\xi(\hat{t}\hatparenskip)}\), then by Claim~3a, there
  are \(\theta\) and \(\theta'\) such that \(u\in W_\theta\) and
  \(v\in W_{\theta'}\)\@. Since \(\hat{t}\concat\theta\) is a prefix
  of \(\mu(u)\), \(\hat{t}\concat\theta'\) is a prefix of \(\mu(v)\),
  and \(\hat{t}\) is the highest common ancestor of \(\mu(u)\) and
  \(\mu(v)\), it follows that \(\theta\neq\theta'\)\@. Then by
  Lemma~4, \(\theta>\theta'\), because \((u,v)\in E\)\@. Therefore,
  \(\mu(u)\succ\mu(v)\)\@. Thus in all cases (R) holds\@.
%
\nopagebreakendpar
\end{itemize}
{\nopagebreakbeginpar\markendlst{Proof of Theorem 1 (\(\logicimplies\))}}
\end{alabsubtext}
%
\asection{7}{Application to Fairness}
%
\apar{7-1}
Our results apply to proving program termination under a general
fairness constraint
\(\Rabcond{C}=\{(\phi_1,\psi_1),\ldots,(\phi_N,\psi_N)\}\), which is
defined in \cite{cj95-03-9} and \cite[p.\ 112]{cj95-03-8}\@. Each
\((\phi_\chi,\psi_\chi)\), \(1\leq\chi\leq N\) consists of an
\emph{enabling condition} \(\phi_\chi\) and an \emph{action condition}
\(\psi_\chi\), both of which are program-state predicates\@. An
infinite computation of \(P\) is \emph{unfair} if it satisfies
\(\Rabcond{C}\) regarded as a Rabin condition, i.e., if for some
\(\chi\), the enabling condition \(\phi_\chi\) is satisfied infinitely
often and the action condition \(\psi_\chi\) is satisfied only
finitely often\@. A program \(P\) fairly terminates if every infinite
computation of \(P\) is unfair, i.e.,\ if \(P\) viewed as a graph
(where nodes are states and edges are transitions) satisfies
\(\Rabcond{C}\)\@. Thus to show fair termination of \(P\), we can use
Theorem~1\@.
%
\apar{7-2}
\begin{alabsubtext}{Example}{1}{}
\exampfontshape
%
\apar{Example 1-1}
Program \(P_{ex}\), shown in Figure~5,
%
\begin{figure*}
\[
\begin{array}{rrlclcll}
*[ & a: & \progvar{x}=0 & & & \progcond & \progvar{y}\assigned\progvar{y}+1\\
 & b: & \progvar{x}=0 & \logicand & \testcond{even}(\progvar{y}) & \progcond &
    \progvar{x}\assigned 1\\
 & c: & \progvar{x}\neq0 & \logicand & \progvar{y}\neq0 & \progcond &
    \progvar{y}\assigned\progvar{y}-1\\
 & d: & \progvar{x}\neq0 & \logicand & \progvar{y}\neq0 & \progcond &
    \progvar{z}\assigned\progvar{z}+1 & ]
\end{array}
\]
\afigcap{5}{The program \protect\(P_{ex}\protect\)\@.}
\end{figure*}
%
\begin{figure*}
%
\setlength{\unitlength}{0.00275em}%
\begin{picture}(12000,5100)(-350,-4350)
\put(5250,-4000){\circle{700}}
\put(5250,-4000){\makebox(0,0){\(t\)}}
\drawline[100](4923,-3875)(0,-2350)
\put(1950,-2800){\makebox(0,0)[l]{\(2\omega\)}}
\put(0,-2000){\circle{700}}
\put(0,-2000){\makebox(0,0){\(b\)}}
\put(100,-1400){\makebox(0,0)[l]{\(\at a\mbox{ and }y\mbox{ even}\)}}
\drawline[100](4941,-3835)(1809,-2165)
\put(3450,-2800){\makebox(0,0)[l]{\(\omega\)}}
\put(1500,-2000){\circle{700}}
\put(1950,-2000){\makebox(0,0)[l]{\(\at b\)}}
\put(3500,-2000){\makebox(0,0){\(\cdots\)}}
\drawline[100](5127,-3672)(4500,-2350)
\put(4800,-2800){\makebox(0,0)[l]{\(2i\tightspace{+}1\)}}
\put(4500,-2000){\circle{700}}
\put(4500,-2000){\makebox(0,0){\(c\)}}
\put(4150,-1000){\makebox(0,0)[l]{\(\at d\mbox{ and }y=i\)}}
\drawline[100](5373,-3672)(6000,-2350)
\put(5900,-2800){\makebox(0,0)[l]{\(2i\)}}
\put(6000,-2000){\circle{700}}
\put(5650,-1400){\makebox(0,0)[l]{\(\at c\mbox{ and }y=i\)}}
\put(7000,-2000){\makebox(0,0){\(\cdots\)}}
\drawline[100](5559,-3835)(8650,-2165)
\put(7900,-2800){\makebox(0,0)[l]{\(3\)}}
\put(9000,-2000){\circle{700}}
\put(9000,-2000){\makebox(0,0){\(c\)}}
\put(8650,-1000){\makebox(0,0)[l]{\(\at d\mbox{ and }y=1\)}}
\drawline[100](5577,-3875)(10500,-2350)
\put(9600,-2800){\makebox(0,0)[l]{\(2\)}}
\put(10500,-2000){\circle{700}}
\drawline(0,-1650)(0,-350)
\put(100,-800){\makebox(0,0)[l]{\(0\)}}
\put(10150,-1400){\makebox(0,0)[l]{\(\at c\mbox{ and }y=1\)}}
\put(0,0){\circle{700}}
\put(-350,600){\makebox(0,0)[l]{\(\at a\mbox{ and }y\mbox{ odd}\)}}
\end{picture}
%
\afigcap{6}{The pointer tree, its coloring, and the measure\@.}
\end{figure*}
%
is taken from \cite{cj95-03-10} and can also be found in
\cite{cj95-03-8}\@. The variables \(\progvar{x}\), \(\progvar{y}\), and
\(\progvar{z}\) take on non-negative integer values\@. Program
\(P_{ex}\) terminates under the assumption of \emph{strong fairness}:
For every infinite computation there is some guarded command \(l\)
that is unfairly executed, i.e., infinitely often enabled but only
finitely often executed\@. Thus the fairness constraint
\(\Rabcond{C}\) can be written
\[\{(\phi_a,\psi_a),(\phi_b,\psi_b),(\phi_c,\psi_c),(\phi_d,\psi_d),
(\phi_t,\psi_t)\}\] where the pair \((\phi_l,\psi_l)\),
\(l=a,b,c,d\), denotes that command \(l\) is unfairly executed\@. Thus
\(\phi_l\) is the guard of \(l\), and \(\psi_l\) is a predicate
denoting that \(l\) is the guarded command to be executed\@. The
additional pair
\((\phi_t,\psi_t)=(\testcond{false},\testcond{false})\) is introduced
for technical reasons to account for progress toward termination\@.
%
\apar{Example 1-2}
To prove that \(G(P_{ex})\satisfy\Rabcond{C}\), we define a progress
measure \((\mu,(T,\xi))\)\@. The tree \(T\) is
\[\{\emptyvec,\vect{2},\vect{3},\ldots,\vect{\omega},
\vect{2\omega},\vect{2\omega,0}\}\] and the coloring \(\xi\) is
defined by
\[\xi(\emptyvec)=t,\xi(\vect{2\omega})=b,\mbox{ and }
\xi(\vect{k})=c,\mbox{ where }k<\omega\mbox{ and }k\mbox{ is odd}\]
\sentence
See Figure~6, where also the mapping \(\mu\) is indicated\@.
Formally, \(\mu\) is defined by:
%
\[
\mu(x,y)=
  \condval{%
    \vect{2\omega,0} & \mbox{if }\at a\mbox{ and }y\mbox{ is odd} \\
    \vect{2\omega} & \mbox{if }\at a\mbox{ and }y\mbox{ is even}\\
    \vect{\omega} & \mbox{if }\at b\\
    \vect{2y+1} & \mbox{if }\at d\\
    \vect{2y} & \mbox{if }\at c
  }
\]
%
where \(y\) denotes the value of program variable \(\progvar{y}\) and
\(\at l\) denotes that the program counter is at \(l\)\@.
%
\apar{Example 1-3}
For the program \(P_{ex}\), it can be verified that (I) holds\@. For
example, the colors of nodes on the path to \(\vect{2\omega,0}\)
consists of \(b\) alone, and \(\psi_{b}\) is certainly false when
\(a\) is selected for execution\@. With each iteration of the loop,
the value of \(\mu\) changes according to (R)\@. For example,
consider the case when \(\progvar{x}=0\), \(\progvar{y}\) is odd, and \(a\)
is executed with \(a\) also being the new value of the program
counter\@. Then \(\mu\) changes from \(\vect{2\omega,0}\) to
\(\vect{2\omega}\) and \(b\) is the label of a common ancestor and
\(\phi_{b}=(x=0\logicand\testcond{even}(y))\) is satisfied in the new
state, whence (R) holds\@.
{\nopagebreakbeginpar\markendlst{Example 1}}
\end{alabsubtext}
%
The termination proof of the program \(P_{ex}\) in
\cite{cj95-03-8,cj95-03-10} involves reasoning, not only about the
original program, but also about two transformed programs\@.
%
\apar{7-3}
In practice, it is convenient to reformulate the notion of Rabin
measure so that condition (I) expresses that on a transition from
\(u\) to \(v\) only the colors of common ancestors of \(u\) and \(v\)
should not be invalidating\@. Other changes make it possible to define
concisely both \(T\) and \(\mu\) by assertions in the program text as
described in~\cite{cj95-03-17}\@.
%
\asection{8}{Automata-Theoretic Applications}
%
\apar{8-1}
The verification problem for automata has been widely studied and can
be formulated as follows\@. An automaton \(A_P\), called a
\emph{program automaton}, satisfies an automaton \(A_S\), called a
\emph{specification automaton}, if the language \(\automlang(A_P)\)
defined by \(A_P\) is a subset of the language \(\automlang(A_S)\)
defined by \(A_S\), i.e., if every behavior of \(A_P\) is a behavior
of \(A_S\)\@.
%
\apar{8-2}
In this section we indicate how Rabin measures solve the problem of
finding verification conditions for proving that a program satisfies a
specification given by a deterministic Rabin automaton\@. Combined
with Safra's result~\cite{cj95-03-31}, this yields a verification
method for specifications given as nondeterministic finite-state
B\"uchi automata\@.
%
\apar{8-3}
An \emph{automaton} \(A=(\Sigma,V,\automtrans{},V^0)\) consists of a
countable \emph{alphabet} \(\Sigma\), a countable \emph{state space}
\(V\), a \emph{transition relation}
\(\automtrans{}\subseteq V\times\Sigma\times V\), and a set of
\emph{initial states} \(V^0\subseteq V\)\@. If \(V^0\) and all sets
\(\setof{v'}{v\automtrans{e}v'}\) have at most one element, then
\(A\) is \emph{deterministic}\@. A \emph{run} (computation) of \(A\)
over a behavior \(e_0,e_1,\ldots\) is an infinite sequence of states
\(v_0\automtrans{e_0}v_1\automtrans{e_1}\cdots\) with
\(v_0\in V^0\)\@. A behavior \(e_0,e_1,\ldots\) is \emph{accepted by}
\(A\) if there is a run of \(A\) over \(e_0,e_1,\ldots\)\@. The
\emph{language} or \emph{property} \(\automlang(A)\) \emph{accepted by} \(A\)
is the set of behaviors of \(A\)\@.
%
\apar{8-4}
A \emph{deterministic Rabin automaton}
\(A=(\Sigma,V,\automtrans{},\{v^0\},\Rabcond{C})\) is defined as a
deterministic automaton, but in addition it is equipped with a Rabin
condition \(\Rabcond{C}\) on \(V\)\@. A run
\(v_0\automtrans{e_o}v_1\automtrans{e_1}\cdots\) of a Rabin automaton
\(A\) over a behavior \(e_0,e_1,\ldots\) is \emph{accepting} if
\(v_0,v_1,\ldots\satisfy\Rabcond{C}\)\@. The language
\(\automlang(A)\) \emph{accepted by} \(A\) is the set of behaviors
whose run is accepting\@.
%
\apar{8-5}

We can now use Rabin measures to solve the verification problem
\(\automlang(A_P)\subseteq \automlang(A_S)\), where the program
automaton
\(A_P=(\Sigma,V_P,\automtrans{}_{\scriptscriptstyle P},V_P^0)\)
is nondeterministic and the specification automaton
\(A_S=(\Sigma, V_{\scriptscriptstyle S},
\automtrans{}_{\scriptscriptstyle S},\{s^0\},\Rabcond{C})\) is a
deterministic Rabin automaton\@. In fact, it suffices to notice that
\(\automlang(A_P)\subseteq\automlang(A_S)\) holds if and only if all
paths in the reachable part of the joint state graph (formed by the
automata-theoretic product of \(\automlang(A_P)\) and
\(\automlang(A_S)\)) satisfy the Rabin condition \(\Rabcond{C}\)\@.
%
\begin{alabsubtext}{Corollary}{1}{of Theorem~1}
Let \(A_P\) be an automaton and let \(A_S\) be a deterministic Rabin
automaton\@. Then \(\automlang(A_P)\subseteq\automlang(A_S)\) if and
only if there is progress measure for \(\Rabcond{C}\) on the jointly
reachable states\@.
\end{alabsubtext}
%
\apar{8-6}
For further applications see~\cite{cj95-03-14}, where the method for
Rabin automata is extended to the \(\forall\)-automata
of~\cite{cj95-03-24} and applied to simplify the method
of~\cite{cj95-03-2}\@.
%
\asection{9}{Acknowledgments}
%
\apar{9-1}
Thanks to two anonymous referees for useful comments\@. We are also
grateful to the managing editor, Michael J.\ O'Donnell, for his
careful help in polishing the article.
%
\end{articletext}
%
\begin{articlebib}
%
\bibliographystyle{\the\rbibstyle}
\bibliography{cj95-03}
%
\end{articlebib}
%
\end{document}