% The Chicago Journal of Theoretical Computer Science, Volume 1996, Article 1
% Published by MIT Press, Cambridge, Massachusetts USA
% Copyright 1996 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 macro definitions for this article.
%
\ifx\deceased\undeftex
  \newcommand{\deceased}[1]{\dag#1}
\fi
%
\catcode`\@=11
\ifx\nopagebreakbeginpar\undeftex
  \newcommand{\nopagebreakbeginpar}{\@beginparpenalty10000}
\fi
\ifx\nopagebreakendpar\undeftex
  \newcommand{\nopagebreakendpar}{\@endparpenalty10000}
\fi
\ifx\nopagebreakinteritem\undeftex
  \newcommand{\nopagebreakinteritem}{\@itempenalty10000}
\fi
\catcode`\@=12
%
\ifltwoe\else\newcommand{\emph}[1]{{\em #1\/}}\fi
\ifltwoe\else\newcommand{\textit}[1]{{\it #1\/}}\fi
\ifltwoe\else\newcommand{\textup}[1]{{\rm #1\/}}\fi
\ifltwoe\else\newcommand{\upshape}{\fontshape{n}\selectfont}\fi
%
\newcommand{\prooffontshape}{\upshape}
%
\newcommand{\tuple}[1]{(#1)}
%
\newcommand{\setof}[2]{\{\,#1\mid#2\,\}}
\newcommand{\oftype}{\mathpunct{:}}
\newcommand{\funcspace}[2]{#1\mathbin{\rightarrow}#2}
\newcommand{\funcset}[2]{#2^{#1}}
\newcommand{\powerset}[1]{2^{#1}}
\newcommand{\setcomp}[1]{\overline{#1}}
\newcommand{\setintsct}{\cap}
%
\newcommand{\succeeds}{\rhd}
%
\newcommand\nohyphenl[1]{{\discretionary{}{}{}{#1}}}
\newcommand\nohyphenr[1]{{{#1}\discretionary{}{}{}}}
%
% Macros for the publisher's comment
%
% The circle R symbol for a registered trade name is adapted from the
% circled c copyright symbol defined in The TeXBook by Donald Knuth.
%
\def\registered{{\ooalign
    {\hfil\raise.07ex\hbox{{\scriptsize\textup{R}}}\hfil\crcr\mathhexbox20D}}}
%
% end of local macro definitions for this article
%
\begin{document}
%
\begin{articleinfo}
%
\publisher{The MIT Press}
%
\publishercomment{%
  {\Large
    \begin{center}
      Volume 1996, Article 1\\
      \textit{9 February 1996}
    \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
  \par\noindent
  The \emph{Chicago Journal of Theoretical Computer Science} is
  abstracted or indexed in \emph{Research Alert\registered,
  SciSearch\registered, Current Contents\registered/Engineering
  Computing \& Technology, CompuMath Citation Index\registered.}
}
%
\copyrightstmt{%
  \copyright 1996 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 & \deceased{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{1996}
%
\articleid{1}
%
\selfcitation{
     @article{cj96-01,
       author={Moshe Y. Vardi},
       title={Rank Predicates vs.\ Progress Measures in
         Concurrent-Program Verification}
       journal={Chicago Journal of Theoretical Computer Science},
       volume={1996},
       number={6},
       publisher={MIT Press},
       month={September},
       year={1996}
     }
}
%
\begin{retrievalinfo}
\end{retrievalinfo}
%
\title{Rank Predicates vs.\ Progress Measures in Concurrent-Program
  Verification}
\shorttitle{Rank Predicates vs.\ Progress 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{Moshe Y. Vardi}
   \collname{}{Vardi, Moshe Y.}
   \begin{institutioninfo}
       \instname{Rice University}
       \department{Department of Computer Science}
       \address{6100 S. Main Street, Mail Stop 132}{Houston}{TX}{USA}{77005-1892}
   \end{institutioninfo}
   \email{vardi@cs.rice.edu}
% \URL{http://www.cs.rice.edu/~vardi}
\end{authorinfo}
%
\shortauthors{Vardi}
%
\support{
  \sloppy Work done at the IBM Almaden
  \nohyphenl{Research}~\nohyphenr{Center\@.}\par%
}
%
\begin{editinfo}
  \submitted{9}{1}{1995}\reported{8}{3}{1995}
  \submitted{14}{9}{1995}\reported{1}{12}{1995}
  \submitted{16}{12}{1995}\reported{17}{12}{1995}\published{9}{2}{1996}
\end{editinfo}
\end{articleinfo}
%
\begin{articletext}
%
\begin{abstract}
%
\apar{Abstract-1}
This note describes a direct relationship between rank predicates
and progress measures in concurrent-program verification\@.
\end{abstract}
% 
\asection{1}{Introduction}
%
\apar{1-1}
In \cite{cj96-01-12,cj96-01-13,cj96-01-14}, we presented an
automata-theoretic framework that unified several trends in the area
of concurrent-program verification\@. At the foundation of that
framework is the observation (due to G.~Plotkin) that \emph{recursive
\(\omega\)-automata} can express all \(\Sigma^1_1\) sets of
computations\@. Using this observation it was shown how to extend the
\emph{helpful-directions} methodology of \cite{cj96-01-02,cj96-01-09}
to verification with respect to all \(\Sigma^1_1\) fairness conditions
and \(\Pi^1_1\) correctness conditions\@. The technical notion
underlying this methodology is that of \emph{rank predicate}, which
defines some ranking of program states by means of elements of some
well-founded sets\@.
%
\apar{1-2}
Another approach to concurrent-program verification was pursued
by Klarlund. The intuition behind his approach is described by the
following paraphrase of ideas from
\cite{cj96-01-07,cj96-01-03,cj96-01-04,cj96-01-05,cj96-01-08,cj96-01-06}\@:
%
\begin{quote}
A \emph{progress measure} is a mapping on program states that quantifies
how close each state is to satisfying a property about infinite
computations\@. On every program transition the progress measure must
change in a way ensuring that the computation converges toward the
property\@.
\end{quote}
%
We show that there is a direct relationship between rank predicates and
progress measures\@.
%
\asection{2}{Background}
%
\asubsection{2.1}{Languages and Automata}
%
\apar{2.1-1}
An \emph{\(\omega\)-word} \(w\) is a function
\(w\oftype\funcspace{\omega}{\omega}\)\@. (One can view \(w\) as an
\(\omega\)-word over the alphabet
\(\setof{i}{\exists j\mbox{ s.t.\ }w(j)=i}\)\@.) In this paper, a
\emph{language} is a set of \(\omega\)-words, i.e., a subset of
\(\funcset{\omega}{\omega}\)\@. A language \(L\) is \(\Sigma_1^1\) if
it is the projection of an arithmetical relation, i.e., there is an
arithmetical relation
\(R\subseteq\funcset{\omega}{\omega}\times\funcset{\omega}{\omega}\)
such that \(L=\setof{w}{\exists u\mbox{ s.t.\ }R(w,u)}\)\@. A language
\(L\) is \(\Pi_1^1\) if its complement is a \(\Sigma^1_1\)
language\@. (See \cite{cj96-01-11} for basic concepts in recursion
theory\@.)
%
\apar{2.1-2}
A \emph{table} \(T\) is a tuple \(\tuple{S,S^0,\alpha}\), where \(S\)
is a (possibly countably infinite) set of \emph{states},
\(S^0\subseteq S\) is the set of \emph{starting} states, and
\(\alpha\subseteq S\times\omega\times S\) is the \emph{transition
relation}\@. \(T\) is said to be \emph{recursive} in case \(S\),
\(S^0\), and \(\alpha\) are recursive\@. A \emph{run} \(r\) of \(T\)
\emph{on} the word \(w\) is a sequence
\(r\oftype\funcspace{\omega}{S}\) such that \(r(0)\in S^0\) and
\(\tuple{r(i),w(i),r(i+1)}\in\alpha\) for all \(i\geq 0\)\@.
%
\apar{2.1-3}
Automata are tables with \emph{acceptance conditions}\@. A
\emph{Wolper automaton} has a vacuous acceptance condition, so it is
just a table \(T=\tuple{S,S^0,\alpha}\)\@. It \emph{accepts} a word
\(w\) if it has a run on \(w\)\@. A \emph{B\"{u}chi automaton} \(A\)
is a pair \(\tuple{T,F}\), where \(T=\tuple{S,S^0,\alpha}\) is a
table and \(F\subseteq S\)\@. \(A\) accepts a word \(w\) if there is a
run \(r\) of \(T\) on \(w\) such that for infinitely many \(i\)'s we
have \(r(i)\in F\)\@. \(A\) is recursive if \(T\) and \(F\) are
recursive\@. The language accepted by an automaton \(A\), consisting
of all \(\omega\)-words accepted by \(A\), is denoted \(L_\omega(A)\)\@.
%
\apar{2.1-4}
The following theorem, which follows easily from \emph{Kleene's Normal
Form Theorem}, asserts that Wolper automata and B\"{u}chi automata
have the same expressive power: they both can define all
\(\Sigma^1_1\) languages\@.
%
\begin{alabsubtext}{Theorem}{2.1}{\protect\cite{cj96-01-12,cj96-01-13,cj96-01-14}}
Let \(L\) be a language\@. The following are equivalent\@:
%
\begin{itemize}
\item \(L\) is a \(\Sigma_1^1\) language\@.
\item There is a recursive Wolper automaton \(A\) such that
  \(L=L_\omega(A)\)\@.
\item There is a recursive B\"{u}chi automaton \(A\) such that
  \(L=L_\omega(A)\)\@.
\end{itemize}
%
\end{alabsubtext}
%
\asubsection{2.2}{Program Verification}
%
\apar{2.2-1}
Rather than restrict ourselves to a particular programming language,
we use here an abstract model for nondeterministic programs (we model
concurrency by nondeterminism)\@. A \emph{program} \(P\) is a triple
\(\tuple{W,I,R}\), where \(W\) is a set of \emph{program states},
\(I\subseteq W\) is a set of \emph{initial states}, and \(R\subseteq W^2\)
is a binary \emph{transition relation} on \(W\)\@. A computation is a
sequence \(\sigma\) in \(W^\omega\) such that \(\sigma(0)\in I\) and
\(\tuple{\sigma(i),\sigma(i+1)}\in R\) for all \(i\geq 0\)\@.%
%
\footnote{%
For simplicity we assume that the program has only infinite
computations\@. A terminating computation is assumed to loop forever
in its last state\@.%
}
%
The set of computations of \(P\) is denoted by \(L_\omega (P)\)\@. Given
that programs are supposed to be effective, we require that \(W\), \(R\),
and \(I\) are recursive sets\@.
%
\apar{2.2-2}
We assume some means of specifying fairness and correctness\@. The
fairness condition is used to specify what computations are considered
to be ``fair,'' i.e., the scheduling of nondeterministic choices is
not too pathological\@. Thus, only computations that satisfy the
fairness condition need be considered when the program is verified\@.
The correctness condition is used to express the performance required
of a computation; in other words, this is what the user demands of the
computation\@. Instead of focusing on concrete specification languages,
we can view the fairness and correctness conditions abstractly as sets
of \(\omega\)-words\@.
%
\apar{2.2-3}
Given a fairness condition \(\Phi\) and a correctness condition \(\Psi\),
the program \(P\) is \emph{correct with respect to} \(\tuple{\Phi,\Psi}\)
if every computation of \(P\) that satisfies \(\Phi\) also satisfies
\(\Psi\), that is, if \(L_\omega(P)\setintsct\Phi\subseteq\Psi\)\@. Our
approach is applicable when the fairness condition is a \(\Sigma^1_1\)
language and the correctness condition is a \(\Pi^1_1\) language\@. In
that case, the intersection of fairness and incorrectness, i.e.,
\(\Phi\setintsct\setcomp{\Psi}\), is a \(\Sigma^1_1\) language, and, by
Theorem~2.1, can be expressed by a recursive B\"{u}chi
automaton or by a recursive Wolper automaton\@. Thus, let
\(A_{\Phi,\Psi}=\tuple{S,S_0,\alpha,F}\) be a recursive automaton such
that \(L_\omega(A_{\Phi,\Psi})=\Phi\setintsct\setcomp{\Psi}\), then \(P\)
is correct with respect to \(\tuple{\Phi,\Psi}\) precisely when
\(L_\omega(P)\setintsct L_\omega(A_{\Phi,\Psi})\) is empty\@.
%
\asection{3}{Rank Predicates}
%
\apar{3-1}
The crux of the approach is to define a \emph{rank predicate} on pairs
consisting of program states and automata states\@.
% 
\begin{alabsubtext}{Theorem}{3.1}{\protect\cite{cj96-01-12,cj96-01-13,cj96-01-14}}
Let \(P=\tuple{W,I,R}\) be a recursive program, let \(\Phi\) be a
\(\Sigma^1_1\) language, and let \(\Psi\) be a \(\Pi^1_1\) language\@. Let
\(A_{\Phi,\Psi}=\tuple{S,S_0,\alpha,F}\) be a B\"{u}chi automaton such
that \(L_\omega(A_{\Phi,\Psi})=\Phi\setintsct\setcomp{\Psi}\)\@. Then \(P\)
is correct with respect to \(\tuple{\Phi,\Psi}\) iff there exists an
ordinal \(\kappa\) and a rank predicate
\(\rho\subseteq\powerset{W\times S\times\kappa}\) such that the
following holds:
%
\begin{itemize}
\item for all \(u\in I\) and \(p\in S_0\), we have that
  \(\rho(u,p,\kappa)\) holds,
\item for all \(u,v\in W\) and \(p,q\in S\), if \(\rho(u,p,\mu)\) holds,
  \(\tuple{u,v}\in R\), and \(\tuple{p,u,q}\in\alpha\), then
  \(\rho(v,q,\nu)\) holds for some \(\nu\leq\mu\), and
\item for all \(u,v\in W\) and \(p,q\in S\), if \(\rho(u,p,\mu)\) holds,
  \(\tuple{u,v}\in R\), \(\tuple{p,u,q}\in\alpha\), and \(p\in F\), then
  \(\rho(v,q,\nu)\) holds for some \(\nu<\mu\)\@.
\end{itemize}
%
\end{alabsubtext}
%
\apar{3-2}
The conditions in the theorem get simpler if we assume that
\(A_{\Phi,\Psi}\) is a Wolper automaton, i.e., when we take \(F=S\)\@.
%
\begin{alabsubtext}{Corollary}{3.2}{}
Let \(P=\tuple{W,I,R}\) be a recursive program, let \(\Phi\) be a
\(\Sigma^1_1\) language, and let \(\Psi\) be a \(\Pi^1_1\) language\@. Let
\(A_{\Phi,\Psi}=\tuple{S,S_0,\alpha}\) be a Wolper automaton such that
\(L_\omega(A_{\Phi,\Psi})=\Phi\setintsct\setcomp{\Psi}\)\@. Then \(P\) is
correct with respect to \(\tuple{\Phi,\Psi}\) iff there exists an
ordinal \(\kappa\) and a rank predicate
\(\rho\subseteq\powerset{W\times S\times\kappa}\) such that the
following holds:
%
\begin{itemize}
\item for all \(u\in I\) and \(p\in S_0\), we have that \(\rho(u,p,\kappa)\)
  holds, and
\item for all \(u,v\in W\) and \(p,q\in S\), if \(\rho(u,p,\mu)\) holds,
  \(\tuple{u,v}\in R\), and \(\tuple{p,u,q}\in\alpha\), then
  \(\rho(v,q,\nu)\) holds for some \(\nu<\mu\)\@.
\end{itemize}
%
\end{alabsubtext}
%
\asection{4}{Progress Measures}
%
\apar{4-1}
A \emph{progress measure} labels each program state with an element in
an ordered set such that each program transition decreases the rank of
the label
\cite{cj96-01-07,cj96-01-03,cj96-01-04,cj96-01-05,cj96-01-08,cj96-01-06}\@.
Intuitively, the assigned label measures the progress that a
computation makes toward meeting its specification\@. The goal is to
show that a progress measure exists for \(P\) if and only if all
computations of \(P\) satisfy a given specification\@.
%
\apar{4-2}
We now show that there is a direct connection between rank predicates
and progress measures\@. Let \(P=\tuple{W,I,R}\) be a recursive program
and let \(A_{\Phi,\Psi}=\tuple{S,S_0,\alpha,F}\) be a B\"{u}chi
automaton for the intersection of fairness and incorrectness\@.
%
\apar{4-3}
Consider now the set \(Z_\kappa=W\times\powerset{S\times\kappa}\) for an
ordinal \(\kappa\)\@. Let \(A,B\subseteq S\times\kappa\), and let
\(u,v\in W\)\@. Then \(x=\tuple{u,A}\) and \(y=\tuple{v,B}\) are in
\(Z_\kappa\)\@. We say that \(x\) \emph{succeeds} \(y\), denoted
\(x\succeeds y\), if the following holds:
%
\begin{itemize}
\nopagebreakinteritem
\item if \(\tuple{p,\mu}\in A\) and \(\tuple{p,u,q}\in\alpha\), then
  \(\tuple{q,\nu}\in B\), for some \(\nu\leq\mu\),
\item if \(\tuple{p,\mu}\in A\), \(\tuple{p,u,q}\in\alpha\), and
  \(p\in F\), then \(\tuple{q,\nu}\in B\), for some \(\nu<\mu\)\@.
\end{itemize}
%
We say that \(x\) is \emph{grounded} if for all \(p\in S_0\) we have that
\(\tuple{p,\kappa}\in A\)\@.
%
\apar{4-4}
A \emph{progress measure} of \(P\) \emph{with respect} to \(A_{\Phi,\Psi}\) is
a mapping \(\beta\oftype\funcspace{W}{Z_\kappa}\) for some ordinal \(\kappa\)
such that:
%
\begin{itemize}
\nopagebreakinteritem
\item \(\beta(u)=\tuple{u,A}\) for some \(A\subseteq S\times\kappa\),
\item if \(\tuple{u,v}\in R\) then \(\beta(u)\succeeds\beta(v)\), and
\item if \(u\in I\) then \(\beta(u)\) is grounded\@.
\end{itemize}
%
\begin{alabsubtext}{Theorem}{4.1}{}
Let \(P=\tuple{W,I,R}\) be a recursive program, let \(\Phi\) be a
\(\Sigma^1_1\) language, and let \(\Psi\) be a \(\Pi^1_1\) language\@.
Let \(A_{\Phi,\Psi}=\tuple{S,S_0,\alpha,F}\) be a B\"{u}chi automaton
such that \(L_\omega(A_{\Phi,\Psi})=\Phi\setintsct\setcomp{\Psi}\)\@.
Then \(P\) is correct with respect to \(\tuple{\Phi,\Psi}\) iff it
has a progress measure with respect to \(A_{\Phi,\Psi}\)\@.
\end{alabsubtext}
%
\begin{alabsubtext}{Proof of Theorem}{4.1}{}
\prooffontshape\ \relax
%
\paragraph{If:}
Let \(\beta\oftype\funcspace{W}{Z_\kappa}\) be a progress measure of
\(P\) with respect to \(A_{\Phi,\Psi}\) for some ordinal \(\kappa\)\@.
Define a rank predicate
\(\rho\subseteq\powerset{W\times S\times\kappa}\) as follows:
\(\rho(u,p,\mu)\) holds iff \(\beta(u)=\tuple{u,A}\) and
\(\tuple{p,\mu}\in A\)\@. It is easy to verify that \(\rho\)
satisfies the conditions of Theorem~3.1; it follows that \(P\) is
correct with respect to \(\tuple{\Phi,\Psi}\)\@.
%
\paragraph{Only if:}
Let \(\rho \subseteq\powerset{W\times S\times\kappa}\) be the rank
predicate given by Theorem~3.1\@. Consider now the function
\(\beta\oftype\funcspace{W}{Z_\kappa}\) defined by
\[\beta(u)=\tuple{u,\setof{\tuple{p,\mu}}{\rho(u,p,\mu)\mbox{ holds}}}\]
\sentence
It is easy to see that \(\beta\) is a progress measure of \(P\) with respect
to \(A_{\Phi,\Psi}\)\@.
%
{\nopagebreakbeginpar\markendlst{}}
\end{alabsubtext}
% 
\asection{5}{Discussion}
%
\apar{5-1} The above results show that progress measures can be
derived in a direct manner from rank predicates and vice
versa\@. Thus, their existence is guaranteed for programs that are
correct with respect to \(\Sigma^1_1\) fairness conditions and
\(\Pi^1_1\) correctness conditions\@. As is shown in
\cite{cj96-01-01,cj96-01-03}, the analog of Theorem~2.1 holds also in
a topological (rather than a recursion-theoretical) setting%
%
\footnote{%
One can define a topology on \(\omega^\omega\) by taking the basic
neighborhoods to be the balls \(\mbox{\textit{Ball}}(j_1,\dots,j_k)=
\setof{v\in\omega^\omega}{v(i)=j_i\mbox{ for }0\leq i\leq k}\) for
\(k\geq 0\) and \(j_1,\dots,j_k\in\omega\), yielding the \emph{Baire
space} \cite{cj96-01-10}\@.%
}
%
(i.e., a language is \emph{analytic} iff it can be defined by means of
a Wolper automaton and iff it can be defined by means of a B\"{u}chi
automaton), which means that Theorem~3.1 and Corollary~3.2 can also be
stated in a topological setting\@. Thus, these results are broad
enough to cover many cases of interest, and in particular they cover
the Rabin fairness conditions of \cite{cj96-01-07}, the safety
correctness conditions of \cite{cj96-01-08}, and the strong fairness
conditions of \cite{cj96-01-05}\@.
%
\apar{5-2}
Consequently, the goal of research in this area should not be merely
to prove the existence of progress measures, but rather to prove the
existence of progress measures with some \emph{desirable}
properties\@. It is the intended application of progress
measures---\emph{concurrent-program verification}---that should
determine what properties ought to be desired\@. Indeed, while
Theorem~4.1 just proves the existence of progress measures, the
progress measures defined by Klarlund possess specific, interesting
properties that are spelled out in the various papers
\cite{cj96-01-07,cj96-01-03,cj96-01-04,cj96-01-05,cj96-01-08,cj96-01-06}\@.
%
\end{articletext}
%
\begin{articlebib}
%
\bibliographystyle{\the\rbibstyle}
\bibliography{cj96-01}
%
\end{articlebib}
%
\end{document}