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