Chicago Journal of Theoretical Computer Science

The MIT Press

Volume 1995, Article 3 20 September 1995

ISSN 1073–0486. MIT Press Journals, 55 Hayward St., Cambridge, MA 02142 USA; (617)253-2889; journals-orders@mit.edu, journals-info@mit.edu. Published one article at a time in L^{A}TEX source form on the Internet. Pagination varies from copy to copy. For more information and other articles see:

• http://www-mitpress.mit.edu/jrnls-catalog/chicago.html

• http://www.cs.uchicago.edu/publications/cjtcs/

• gopher.mit.edu

• gopher.cs.uchicago.edu

• anonymous ftp at mitpress.mit.edu

• anonymous ftp at cs.uchicago.edu Klarlund and Kozen Rabin Measures (Info)

\begin{matrix}c \\ ◯ \end{matrix}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; journals-rights@mit.edu.

The 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.

Editor in chief: Janos Simon

Consulting editors: Joseph Halpern, Stuart A. Kurtz, Raimund Seidel

Editors:

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ó 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

Managing editor: Michael J. O’Donnell

Electronic mail: chicago-journal@cs.uchicago.edu

[ii]

Rabin Measures

Nils Klarlund  Dexter Kozen

20 September, 1995

Abstract

Rabin conditions are a general class of properties of infinite se-

Abstract-1

quences that encompass most known automata-theoretic acceptance conditions and notions of fairness. In this paper, we introduce a concept, called a Rabin measure, which in a precise sense expresses progress for each transition toward satisfaction of the Rabin condition.

We show that these measures of progress are linked to the Kleene-

Abstract-2

Brouwer ordering of recursion theory. This property is used in [Kla94b] to establish an exponential upper bound for the complementation of automata on infinite trees.

When applied to termination problems under fairness constraints,

Abstract-3

Rabin measures eliminate the need for syntax-dependent, recursive applications of proof rules.

This article is a revised version of [KK91]. 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 [Kla94b].

1 Introduction

This paper is concerned with infinite sequences and their properties that

1-1

are true or false in the limit. Such properties arise in the study of fairness, temporal logic, and ω-automata. In all these areas, Rabin conditions [McN66, Rab69], which express temporal properties in a special disjunctive normal form, play a major role. (They are also called pairs conditions.) In the theory of fairness, Rabin conditions describe termination under general

Klarlund and Kozen Rabin Measures §1

1 fairness constraints, which include 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 ω-automata, Rabin conditions are pivotal, because they allow ω-regular languages to be expressed by deterministic automata [McN66].

Because temporal conditions are often crucial to understanding the be-

1-2

havior 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 [AO83, APS84, DH86, FK84, Fra86, GFMdR85, Mai89, SdRG89], temporal logic [MP84, OL82], or automata theory [AS87, AS89, Jon87, MP87, Var91]. 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.

In this paper we address a fundamental question underlying several of

1-3

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 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.

The main result of our paper is that a graph satisfies a Rabin condition

1-4

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 Π_{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.

Our treatment exhibits a link between verification with Rabin conditions

1-5

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 [Fra86]) arise simply and naturally in this context and can be explained completely in these terms.

Rabin measures are useful for studying automata on infinite objects.

1-6

In [Kla91], it is shown how the concept can be used to complement Streett 2 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 [Kla94b]. These applications rely on the relationship to the Kleene-Brouwer ordering, and do not follow from previous attempts at explaining progress for Rabin conditions.

2 Related Work

Alpern and Schneider [AS87, AS89] used deterministic Büchi automata as

2-1

a specification method. They obtained a verification method for nondeterministic Büchi automata using the fact that every such automaton can be converted to a Boolean combination, in conjunctive normal form, of deterministic Büchi automata. Vardi [Var91] proposed 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üchi-type acceptance condition, which yields an explanation of helpful directions for the transformed verification problem.

Inspired by the ideas in [Var91], Manna and Pnueli gave verification con-

2-2

ditions for ∀-automata [MP87]. These conditions are expressively equivalent to Büchi automata, although there is no known easy conversion of a Büchi automaton into a ∀-automaton. Sistla [Sis87] considered deterministic automata with acceptance conditions given as temporal formulas on automaton states with the modalities F^{∞}(f) (infinitely often f) and G^{∞}(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.

For temporal logic specifications, assertional proof methods such as [MP84,

2-3

OL82] 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 [RFG88]. 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.

In the area of fairness, complete verification methods for termination were

2-4

given in [FK84, Fra86, GFMdR85, Mai89, LPS81, SdRG89]. These methods are based on helpful directions, and on the iterative use of proof rules applied

3 to syntactically transformed programs. In [Fra86, Section 2.1], 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 [EJ88] 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 parity condition [Mos84] (which is a restricted kind of Rabin condition) were defined in [EJ91].

The methods of explicit schedulers developed in [AO83, APS84, DH86]

2-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 [Fra86].

The shuffling of colors in a Rabin measure is reminiscent of the Later

2-6

Appearance Record of [GH82], which is used to explain how certain restricted memory strategies arise for infinite games played according to a Muller acceptance condition. In [Kla94b], it is shown how Rabin measures yield memoryless strategies for games with Rabin winning conditions.

Progress measures were introduced in [Kla90a] as a generic concept for

2-7

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 [Var91], rank predicates and progress measures are essentially equivalent [Var94] and their existence is in essence expressed by the Kleene-Suslin Theorem of descriptive set theory [Kla94a].

The paper [Kla92b] reformulates the notion of Rabin measure presented

2-8

here, so that it can be better used in program verification. Also, the completeness proof presented in [Kla92b] is simplified for the case that the underlying program contains no cycles.

The verification method in [Kla92a] is based on the liminf concept, and

2-9

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 [Kla92a] can be extended to general simulation and bisimulation concepts [Kla94a].

4

3 Rabin Conditions

A graph G = (V, E) consists of a countable set of vertices (or states) V and

3-1

a set of directed edges E ⊆ V × V. A Rabin pair (R, I) on V consists of a set R ⊆ V of reconfirming states and a set I ⊆ V of invalidating states. We say that an infinite sequence v_{0}, v_{1}, … of states satisfies (R, I), and we write v_{0}, v_{1}, … ⊨ (R, I), if there are infinitely many k such that v_{k} ∈ R and only finitely many k such that v_{k} ∈ I.

3-2 A Rabin condition (or Rabin assignment) C is a set { (R_{χ}, I_{χ}) | χ ∈ X } of Rabin pairs. Here X is a finite set of colors, and Rabin pair (R_{χ}, I_{χ}) is said to have color χ. We assume that no pair in C is repeated, and say that |C| = |X| is the size of C. The set R_{χ} is the set of χ-reconfirming states, and I_{χ} is the set of χ-invalidating states. For technical reasons, we always assume without loss of generality that 0 ∈ X and that I_{0} = ∅ (one can always add the pair (∅, ∅) without changing the semantics of satisfaction defined next). We say that an infinite sequence v_{0}, v_{1}, … satisfies C, and we write v_{0}, v_{1}, … ⊨ C, if for some χ, v_{0}, v_{1}, … ⊨ (R_{χ}, I_{χ}). We say that a graph G = (V, E) satisfies a Rabin condition C on V, and we write G ⊨ C, if every infinite path v_{0}, v_{1}, … in G satisfies C.

4 Pointer Trees

Rabin measures are based on pointer trees, also called direction trees. Let ω_{1}

4-1

be the set of countable ordinals. A pointer tree T is a countable prefix-closed subset of ω_{1}^{∗}, the set of finite sequences of countable ordinals. Each sequence t = ⟨t^{1}, …, t^{ℓ}⟩ in T represents a node, which has children t · ⟨d⟩ ∈ T, where “·” denotes concatenation of sequences. Here d ∈ ω_{1} is the pointer to t · ⟨d⟩ from t. If t′ is a prefix of t ∈ T, then t′ is called an ancestor of t and we write t′ ≤_{·} t. We visualize pointer trees as growing upward; see Figure 1, where children are depicted from left to right in descending order. Every sequence of pointers t^{1}, t^{2}, … (finite or infinite) denotes a path ⟨ ⟩, ⟨t^{1}⟩, ⟨t^{1}, t^{2}⟩, … (finite or infinite) in T, provided each ⟨t^{1}, …, t^{ℓ}⟩ ∈ T. The level |t| of a node t = ⟨t^{1}, …, t^{l}⟩ is the number l; the level of ⟨ ⟩ is 0. The prefix up to level n of t = ⟨t^{1}, …, t^{l}⟩ is ⟨t^{1}, …, t^{min{l,n}}⟩, denoted t ↾ n. The height of T is the maximum node level (if it exists). T is path-finite if there are no infinite paths in T. A common ancestor of nodes t and t′ is a node t̃ that is an ancestor of both of t and of t′. The common ancestor at the highest level is

5

[figure: ⟨1, 0, 2⟩; ⟨1, 0⟩; ⟨1⟩; level 0; level 1; level 2; level 3; 1; ⟨1, 2⟩; 2; ⟨ ⟩; 2; 0]

Figure 1: A pointer tree.

the highest common ancestor, written t ↑ t′.

A simple but central lemma about the infinite sequences of nodes in a

4-2

pointer tree is:

Lemma 1 (Highest Common Ancestor Lemma) Let t_{0}, t_{1}, … 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.

Proof of Lemma 1 Let T′ be the set of nodes that are almost always ancestors of t_{k}. Then T′ contains ⟨ ⟩ 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.

□

Definition 1 (Kleene-Brouwer Ordering) The strict ordering ≻ on T is defined by: t ≻ t′ if and only if either t <_{·} 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 ⪰ is defined as t ⪰ t′ if and only if t ≻ t′ or t = t′.

In other words t ⪰ 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). ⪰ is a total order on T.

Lemma 2 (Kleene-Brouwer Ordering Lemma) If T is path-finite, then ≻ is a well-ordering of T.

6 Proof of Lemma 2 See [Rog67] or use Lemma 1.

□

Rabin measures are based on coloring pointer trees.

4-3

Definition 2 A colored pointer tree (T, ξ) is a pointer tree T with a partial mapping ξ: T ⇀ X, where X is a set of colors, assigning a color ξ(t) ∈ X to each node t in dom ξ so that:

• the root is colored 0, i.e., ξ(⟨ ⟩) = 0;

• each node that is not a leaf receives some color; and

• all colors along a path starting in the root are distinct. Thus, a colored pointer tree has height at most |X|.

5 Rabin Measures

A Rabin measure for a graph with a Rabin condition consists of a colored

5-1

pointer tree and a mapping that assigns a node in the tree to each vertex in the graph. These nodes, or progress values, quantify progress toward the Rabin condition if they are related in a certain way on every transition. Definition 3 Let G = (V, E) be a graph, and let C = { (R_{χ}, I_{χ}) | χ ∈ X } be a Rabin condition on G. A Rabin progress measure (or just Rabin measure) for (G, C) is a triple (μ, T, ξ), where μ: V → T and (T, ξ) is a colored pointer tree, such that: (I) for all v ∈ V and all χ ∈ μ(v), v ∉ I_{χ}, and (R) for all (u, v) ∈ E, u ▷_{μ} v, where u ▷_{μ} v if and only if

μ(u) ≻ μ(v), or

there exists a common ancestor t ≤_{·} ξ(μ(u) ↑ μ(v)) such that v ∈ R_{ξ(t)}.

[figure: 0; #; v_{0}; 0; v_{1}]

Figure 2: A colored pointer tree and a graph with Rabin measure.

The value μ(v) designates a path in T from the root to the node μ(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.

Requirement (I) states that all hypotheses correspond to pairs that are

5-2

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 μ(u) and μ(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.

In Figure 2, we have shown a graph G (to the right) with vertices v_{0} and

5-3

v_{1}. The Rabin condition 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} = ∅. Thus, every infinite path in G runs through a reconfirming state infinitely often, and G ⊨ 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 ⟨0⟩ is not labeled with a color. The measure is as indicated by the dotted arrows, i.e., μ(v_{0}) = ⟨ ⟩ and μ(v_{1}) = ⟨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.

Another more complicated situation involving two colors (X = {0, 1}) is

5-4

shown in Figure 3. Here R_{0} = {v_{0}}, I_{0} = ∅, R_{1} = {v_{1}} (the node marked +), and I_{1} = {v_{3}} (the node marked −).

8

[figure: −; v_{3}; #; v_{0}; 0; 1; +; v_{1}; v_{2}; 1; 0; 0]

Figure 3: Tree, graph, measure, with two nontrivial colors.

The main result of this article is:

5-5

Theorem 1 G ⊨ C if and only if (G, C) has a Rabin measure.

Proof of Theorem 1 (⟸) Let v_{0}, v_{1}, … be an infinite path in G and let

Proof of Theorem 1-1

t_{k} = μ(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 = |t|. Next, we prove that there exists t̂<_{·} t such that v_{0}, v_{1}, … satisfies the Rabin pair (R_{ξ(t̂)}, I_{ξ(t̂)}).

First, assume for a contradiction that for all t̂ ≤_{·} t, v_{k} ∈ R_{ξ(t̂)} holds only

Proof of Theorem 1-2

finitely often. Thus by (a) there is a K such that for all k ≥ K, either (1)

there is a t′_{k} with t <_{·} t′_{k} ≤_{·} t_{k} ↑ t_{k+1} and with v_{k} ∈ R_{ξ(t′_{k})}, or (2) t_{k} ≻ t_{k+1}.

In case (1), t_{k}, t_{k+1} >_{·} t and t_{k} ↾ (l + 1) = t_{k+1} ↾ (l + 1). In case (2), which

Proof of Theorem 1-3

holds infinitely often by assumption and by (b), t_{k} ↾ (l + 1) ≻ t_{k+1} ↾ (l + 1), since t_{k} ≻ t_{k+1} and t is the highest common ancestor of t_{k} and t_{k+1}. Thus t_{K}↾(l+1) ⪰ t_{K+1}↾(l+1) ⪰ ⋯ and infinitely many inequalities are strict. This contradicts the Kleene-Brouwer Ordering Lemma. Thus it holds infinitely often that v_{k} ∈ R_{ξ(t̂)} for some t̂≤_{·} t.

Proof of Theorem 1-4 Second, by (I) it follows that v_{k} ∉ I_{ξ(t̂)} holds from some point on due to (a).

Klarlund and Kozen Rabin Measures §6.1

Proof of Theorem 1 (⟸) □ 9 We prove the (⟹) portion in Section 6.3.

6 Construction of Rabin Measures

We show how to construct a Rabin measure for (G, C), where G = (V, E) is

6-1

a graph that satisfies a Rabin condition C = { (R_{χ}, I_{χ}) | χ ∈ X }.

6.1 Color Set Assignments

We need some definitions before stating a key lemma. Let PC denote the

6.1-1

class of subsets of C. A color set assignment is a map CS: V →PC, where C is a countable set of colors; CS associates a nonempty set of enabled colors CS(v) ⊆ C to each vertex v ∈ V. A set W ⊆ V is χ-enabled if and only if, for all v ∈ W, χ ∈ CS(v). An infinite path v_{0}, v_{1}, … is eventually χ-enabled if and only if there is a χ-enabled suffix v_{k}, v_{k+1}, . . .. A color set assignment is permissible if and only if every infinite path is eventually χ-enabled for some χ.

The set of descendants R(v) of a vertex v in a graph G is the set of all v′

6.1-2

such that there is path from v to v′. Note that v ∈ R(v). The key lemma is:

Lemma 3 Let G = (V, E) be a countable graph. If CS: V → PC is a permissible color set assignment, then there is a vertex v and a color χ such that R(v) is χ-enabled.

Before proving the lemma, we recall that a set Z is nowhere dense if there is no nonempty open set O such that O ∩ Z is dense in O. We will use:

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.

Proof of Lemma 3 For every finite path u in G, define B_{u} and M by

Proof of Lemma 3-1

B_{u} = { u · w | u · w is a path (finite or infinite) in G }
M = { w | w is a path (finite or infinite) in G }

10 The B_{u}s form a subbasis for a topology over M, where the open sets are

Proof of Lemma 3-2

unions of B_{u}s. M is a complete metric space.^{1} For a finite path u in G, and for χ ∈ C, define the set

Proof of Lemma 3-3

F_{u,χ} = { u · w | w is χ-enabled}

which is closed. Every finite path u is contained in F_{u,χ} for all χ, and every infinite path w is in F_{u,χ}, for some u and χ, by the assumption that w is eventually χ-enabled. Thus M = ⋃_{u,χ} F_{u,χ}.

Proof of Lemma 3-4 By the Baire Category Theorem, some F_{u,χ} contains a basic open set, i.e., contains some B_{v}. Consequently, R(v) is χ-enabled.

Proof of Lemma 3 □

6.2 Colorings

Lemma 3 can be applied transfinitely to a graph to yield a stronger result.

6.2-1

We need a few definitions. Let C be a countable set of colors. A C-coloring c of a set V is a total mapping c: V → C. A coloring c obeys a color set assignment CS if and only if, for all v ∈ V, c(v) ∈ CS(v). An infinite path v_{0}, v_{1}, … is eventually χ-stable with respect to c, where χ ∈ C, if for almost all i, c(v_{i}) = χ. A coloring c is eventually stable if every infinite path is eventually χ-stable for some χ. A set W ⊆ V is monochromatic with respect to c if there is χ ∈ C such that for all v ∈ W, c(v) = χ.

Lemma 4 Let G = (V, E) be a graph. If CS is a permissible color set assignment, then there is an eventually stable coloring c: V → C obeying CS and a partition S = { W_{θ} | θ < γ } of V, where γ is a countable ordinal, such that:

(a) each W_{θ} is monochromatic; and

(b) if (v, v′) ∈ E, v ∈ W_{θ}, and v′ ∈ W_{θ′}, then θ ≥ θ′.

d(w, w′) = \{ \begin{matrix}0 & if w = w′ \\ 1/i & if w_{i} ≠ w′_{i} and w_{j} = w′_{j} for 1 ≤ j < i \\ 1/(i + 1) & if w is a prefix of w′ of length i \\ 1/(i + 1) & if w′ is a prefix of w of length i \end{matrix}

11 Proof of Lemma 4 We apply Lemma 3 transfinitely. More precisely, Lemma 3

1The metric can be given, for example, as:

Proof of Lemma 4-1

is first applied to yield a vertex v in G such that R(v) is χ-enabled for some χ. Define W_{0} = R(v) and c(v) = χ for v ∈ 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 γ classes, where γ is a countable ordinal.

Then (a) is satisfied according to the definition of c. Also, (b) is satisfied,

Proof of Lemma 4-2

because every vertex is removed along with all its successors in the remaining graph.

Proof of Lemma 4 □

6.3 Proof of Theorem 1 (⟹)

6.3-1

Proof of Theorem 1 (⟹) Let G = (V, E) be a graph that satisfies a

Proof of Theorem 1-5

finite Rabin condition C. To construct a measure (μ, (T, ξ)) of (G, C), we use the algorithm AssignRabin in Figure 4. The algorithm builds the tree (T, ξ) and labels each node t ≠ ⟨ ⟩ of T with a set W (t) ⊆ V, which is to be the set of vertices mapped by μ to nodes having t as an ancestor. The purpose of AssignRabin(t, Y, χ) is to assign color χ to node t and to define the children t · ⟨θ⟩ of node t. Each child receives a label W (t · ⟨θ⟩), which is a subset of W (t). The set Y denotes the colors that have already been assigned to the proper ancestors of t.

Proof of Theorem 1-6

• Initially, AssignRabin is applied with parameters (⟨ ⟩, ∅, 0), and the tree T consists of only the root ⟨ ⟩ with label W (⟨ ⟩) = V.

• In Step 1 of AssignRabin, node t is assigned color χ, and Ŵ = W (t)\ R_{χ} is the set of states in W (t) that are not χ-reconfirming.

• In Step 2, Lemma 4 is used to obtain a partition S = { W_{θ} | θ < γ } of Ŵ and a coloring c of Ŵ. Informally, the color set assignment CS\overline{Y ∪\{χ\}} expresses the set of colors that are not invalidating and that have not already been considered. More precisely, the color set assignment CS\overline{Y ∪\{χ\}} assigns to vertex v the set of colors χ′ ∈ X such that χ′ ∉ Y ∪ {χ} and v ∉ I_{χ′}; however, if this set is empty, then the

12 AssignRabin(t, Y, χ) :

1. ξ(t) := χ Ŵ := W (t) \ R_{χ}

2. Use Lemma 4 on G \ Ŵ with color set assignment CS\overline{Y ∪\{χ\}} (explained in the text) to obtain a coloring c and a partition S = { W_{θ} | θ < γ } of Ŵ.

3. For each class W_{θ} of S:

(a) T := T ∪ {t · ⟨θ⟩}

(b) W (t · ⟨θ⟩) := W_{θ}

4. For each χ′-colored class W_{θ} of S, where χ′ ∈ X:

AssignRabin(t · ⟨θ⟩, Y ∪ {χ}, χ′)

Figure 4: Algorithm AssignRabin. color set assigned is {⊥_{v}}, where ⊥_{v} is a distinct dummy color, different from any color defined elsewhere. Thus the set C of all colors is X ∪ { ⊥_{v} | v ∈ V }.

• In Step 3, a child t · ⟨θ⟩ is added to t for each class W_{θ} of S and t · ⟨θ⟩ is labeled W_{θ}.

• Finally, in Step 4, descendants of each child not assigned a dummy color are constructed by further applications of AssignRabin.

To explain the construction of μ and to prove that Lemma 4 can indeed

Proof of Theorem 1-7

always be used in Step 2, we need some terminology. We say that a subset W ⊆ V is χ-nonreconfirming if W ∩R_{χ} = ∅ and that W is χ-noninvalidating if W ∩ I_{χ} = ∅. A subset W ⊆ V is Y -nonreconfirming if it is χ-nonrecon-firming for each χ in Y. Similarly, a subset W ⊆ V is Y -noninvalidating if it is χ-noninvalidating for each χ in Y.

Claim 1 For each application of the inductive procedure AssignRabin(t, Y, χ) starting with AssignRabin(⟨ ⟩, ∅, 0), the following hold:

• Y ⊆ X and |Y | = |t|;

• χ ∈ X \ Y;

• W (t) is Y -nonreconfirming; and

• W (t) is (Y ∪ {χ})-noninvalidating.

Proof of Claim 1 (By induction) This is true for the first application

Proof of Claim 1-1

AssignRabin(⟨ ⟩, ∅, 0) because |Y | = |∅| = |⟨ ⟩| = |t| = 0; χ = 0; and W (t) = W (⟨ ⟩) = V, which is ∅-nonreconfirming and, since I_{0} = ∅, {0}-non-invalidating.

When AssignRabin(t · ⟨θ⟩, Y ∪ {χ}, χ′) is applied from within

Proof of Claim 1-2

AssignRabin in Step 4, it may be assumed by the induction hypothesis that |Y | = |t|, χ ∈ X \ Y, and W (t) is (Y ∪ {χ})-noninvalidating and Y -non-reconfirming.

It follows that Y ∪{χ} ⊆ X and |Y ∪{χ}| = |t·⟨θ⟩|. Also, by definition of

Proof of Claim 1-3

the color set assignment in Step 2, χ′ ∈ X \(Y ∪{χ}). Furthermore, since W_{θ}

14 is χ′-noninvalidating by this definition, W_{θ} is (Y ∪ {χ} ∪ {χ′})-noninvalidat-ing. Finally, since W_{θ} is χ-nonreconfirming (because W_{θ} ⊆ Ŵ = W \ R_{χ}), it follows that W (t · ⟨θ⟩) = W_{θ} is (Y ∪ {χ})-nonreconfirming.

Proof of Claim 1 □

To see that Lemma 4 is applicable in Step 2 of AssignRabin, we prove:

Proof of Theorem 1-8

Claim 2 In every application of AssignRabin, CS\overline{Y ∪\{χ\}} is permissible for Ŵ; in fact, every infinite path in W is eventually χ̂-enabled for some χ̂ ∈ X \ (Y ∪ {χ}).

Proof of Claim 2 Consider an application AssignRabin(t, Y, χ). By Claim 1,

Proof of Claim 2-1

it follows that Ŵ defined in Step 1 of AssignRabin is (Y ∪ {χ})-noninval-idating and (Y ∪{χ})-nonreconfirming. Now let v_{0}, v_{1}, … be an infinite path in Ŵ. It is (Y ∪ {χ})-nonreconfirming because Ŵ is (Y ∪ {χ})-nonrecon-firming. Hence by the assumption that G ⊨ C, v_{0}, v_{1}, … ⊨ (Rχ̂, Iχ̂) for some χ̂ ∈ X \ (Y ∪ {χ}). In particular, v_{0}, v_{1}, … is eventually χ̂-enabled with respect to the color set assignment CS\overline{Y ∪\{χ\}} of Ŵ.

Proof of Claim 2 □

Now, to show that all nodes constructed are at level ≤ |X| = |C|, we

Proof of Theorem 1-9

note that if |t| = |X| − 1, then since |Y | = |t| and χ ∉ Y (by Claim 1, Y ∪ {χ} = X). In that case, the color set assignment of Step 2 assigns to each vertex v only the dummy color ⊥_{v}; thus, AssignRabin is not further applied in Step 4. It follows that AssignRabin defines a tree T of height at most |X|. The tree has the following properties:

Claim 3 (a) For every t ∈ T with |t| < |X|,

{ W (t · ⟨θ⟩) | t · ⟨θ⟩ ∈ T }

is a partition of W (t) \ R_{ξ(t)}.

(b) For each v ∈ V there is a unique maximal list t = ⟨t^{1}, …, t^{n}⟩ with 1 ≤ n ≤ |X| such that v ∈ W (t).

15 Proof of Claim 3 (a) holds for t = ⟨ ⟩, because W (⟨ ⟩) = V and Ŵ formed in AssignRabin is W (⟨ ⟩) \ R_{ξ(⟨ ⟩)}=V \ R_{0}; thus Lemma 4 in Step 2 and the definition of children in Step 4 yield a partition { W (⟨θ⟩) | ⟨θ⟩ ∈ T } of W (⟨ ⟩) \ R_{ξ(⟨ ⟩)}. Similarly, by induction it can been seen that (a) holds for all t ∈ T with |t| < |X|. Part (b) follows from (a).

Proof of Claim 3 □

Using Claim 3b, we define μ: V → T by μ(v) = ⟨t^{1}, …, t^{n}⟩. Now let us

Proof of Theorem 1-10

prove that (I) and (R) are satisfied.

(I) Note that if t ≤_{·} μ(v) and χ = ξ(t) is defined, then by Claim 1, W (t) is χ-noninvalidating. Thus in particular, v ∉ I_{χ}.

(R) Let (u, v) ∈ E. If there is a color χ of a common ancestor of μ(u) and μ(v) such that v ∈ R_{χ}, then (R) is trivially satisfied. So we may assume that for the highest common ancestor t̂, v ∉ R_{ξ(t̂)}. Then |μ(v)| > |t̂| by Claim 3a. Consider the application AssignRabin(t̂, Y, ξ(t̂)).

If u ∈ R_{ξ(t̂)}, then μ(u) = t̂ because u ∉ Ŵ = W (t) \ R_{ξ(t̂)}. Thus μ(u) = t̂ ≻ μ(v), because |μ(v)| > |t̂|. Otherwise, if u ∉ R_{ξ(t̂)}, then by Claim 3a, there are θ and θ′ such that u ∈ W_{θ} and v ∈ W_{θ′}. Since t̂· θ is a prefix of μ(u), t̂· θ′ is a prefix of μ(v), and t̂ is the highest common ancestor of μ(u) and μ(v), it follows that θ ≠ θ′. Then by Lemma 4, θ > θ′, because (u, v) ∈ E. Therefore, μ(u) ≻ μ(v). Thus in all cases (R) holds.

Proof of Theorem 1 (⟹) □

7 Application to Fairness

Our results apply to proving program termination under a general fairness

7-1

constraint C = {(ϕ_{1}, ψ_{1}), …, (ϕ_{N}, ψ_{N})}, which is defined in [FK84] and [Fra86, p. 112]. Each (ϕ_{χ}, ψ_{χ}), 1 ≤ χ ≤ N consists of an enabling condition ϕ_{χ} and an action condition ψ_{χ}, both of which are program-state predicates. An infinite computation of P is unfair if it satisfies C regarded as a Rabin condition, i.e., if for some χ, the enabling condition ϕ_{χ} is satisfied infinitely often and the action condition ψ_{χ} is satisfied only finitely often. A program

16

∗[ a : x = 0  → y := y + 1
b : x = 0 ∧ even(y) → x := 1
c : x ≠ 0 ∧ y ≠ 0 → y := y − 1
d : x ≠ 0 ∧ y ≠ 0 → z := z + 1 ]

Figure 5: The program P_{ex}.

[figure: t; 2ω; b; ata and y even; ω; atb; ⋯; 2i+1; c; atd and y = i; 2i; atc and y = i; ⋯; 3; c; atd and y = 1; 2; 0; atc and y = 1; ata and y odd]

Figure 6: The pointer tree, its coloring, and the measure.

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 C. Thus to show fair termination of P, we can use Theorem 1.

7-2

Example 1 Program P_{ex}, shown in Figure 5, is taken from [GFMdR85]

Example 1-1

and can also be found in [Fra86]. The variables x, y, and z take on nonnegative integer values. Program P_{ex} terminates under the assumption of 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 C can be written

{(ϕ_{a}, ψ_{a}), (ϕ_{b}, ψ_{b}), (ϕ_{c}, ψ_{c}), (ϕ_{d}, ψ_{d}), (ϕ_{t}, ψ_{t})}

where the pair (ϕ_{l}, ψ_{l}), l = a, b, c, d, denotes that command l is unfairly executed. Thus ϕ_{l} is the guard of l, and ψ_{l} is a predicate denoting that

17 l is the guarded command to be executed. The additional pair (ϕ_{t}, ψ_{t}) = (false, false) is introduced for technical reasons to account for progress toward termination.

To prove that G(P_{ex}) ⊨ C, we define a progress measure (μ, (T, ξ)). The

Example 1-2

tree T is

{⟨ ⟩, ⟨2⟩, ⟨3⟩, …, ⟨ω⟩, ⟨2ω⟩, ⟨2ω, 0⟩}

and the coloring ξ is defined by

ξ(⟨ ⟩) = t, ξ(⟨2ω⟩) = b, and ξ(⟨k⟩) = c, where k < ω and k is odd

See Figure 6, where also the mapping μ is indicated. Formally, μ is defined by:

μ(x, y) = \{ \begin{matrix}⟨2ω, 0⟩ & if ata and y is odd \\ ⟨2ω⟩ & if ata and y is even \\ ⟨ω⟩ & if atb \\ ⟨2y + 1⟩ & if atd \\ ⟨2y⟩ & if atc \end{matrix}

where y denotes the value of program variable y and atl denotes that the program counter is at l.

For the program P_{ex}, it can be verified that (I) holds. For example, the

Example 1-3

colors of nodes on the path to ⟨2ω, 0⟩ consists of b alone, and ψ_{b} is certainly false when a is selected for execution. With each iteration of the loop, the value of μ changes according to (R). For example, consider the case when x = 0, y is odd, and a is executed with a also being the new value of the program counter. Then μ changes from ⟨2ω, 0⟩ to ⟨2ω⟩ and b is the label of a common ancestor and ϕ_{b} = (x = 0 ∧ even(y)) is satisfied in the new state, whence (R) holds.

Example 1 □

The termination proof of the program P_{ex} in [Fra86, GFMdR85] involves reasoning, not only about the original program, but also about two transformed programs.

In practice, it is convenient to reformulate the notion of Rabin measure

7-3

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 μ by assertions in the program text as described in [Kla92b].

18

8 Automata-Theoretic Applications

The verification problem for automata has been widely studied and can be

8-1

formulated as follows. An automaton A_{P}, called a program automaton, satisfies an automaton A_{S}, called a specification automaton, if the language L(A_{P}) defined by A_{P} is a subset of the language L(A_{S}) defined by A_{S}, i.e., if every behavior of A_{P} is a behavior of A_{S}.

In this section we indicate how Rabin measures solve the problem of

8-2

finding verification conditions for proving that a program satisfies a specification given by a deterministic Rabin automaton. Combined with Safra’s result [Saf88], this yields a verification method for specifications given as nondeterministic finite-state Büchi automata.

An automaton A = (Σ, V, →, V^{0}) consists of a countable alphabet Σ, a

8-3

countable state space V, a transition relation →⊆ V × Σ × V, and a set of initial states V^{0} ⊆ V. If V^{0} and all sets { v′ | v →^{e} v′ } have at most one element, then A is deterministic. A run (computation) of A over a behavior e_{0}, e_{1}, … is an infinite sequence of states v_{0} →^{e_{0}} v_{1} →^{e_{1}} ⋯ with v_{0} ∈ V^{0}. A behavior e_{0}, e_{1}, … is accepted by A if there is a run of A over e_{0}, e_{1}, . . .. The language or property L(A) accepted by A is the set of behaviors of A.

A deterministic Rabin automaton A = (Σ, V, →, {v^{0}}, C) is defined as a

8-4

deterministic automaton, but in addition it is equipped with a Rabin condition C on V. A run v_{0} →^{e_{o}} v_{1} →^{e_{1}} ⋯ of a Rabin automaton A over a behavior e_{0}, e_{1}, … is accepting if v_{0}, v_{1}, … ⊨ C. The language L(A) accepted by A is the set of behaviors whose run is accepting.

8-5

We can now use Rabin measures to solve the verification problem L(A_{P}) ⊆ L(A_{S}), where the program automaton A_{P} = (Σ, V_{P} , →_{P}, V_{P}^{0}) is nondeterministic and the specification automaton A_{S} = (Σ, V_{S}, →_{S}, {s^{0}}, C) is a deterministic Rabin automaton. In fact, it suffices to notice that L(A_{P}) ⊆ L(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 L(A_{P}) and L(A_{S})) satisfy the Rabin condition C.

Corollary 1 (of Theorem 1) Let A_{P} be an automaton and let A_{S} be a deterministic Rabin automaton. Then L(A_{P}) ⊆ L(A_{S}) if and only if there is progress measure for C on the jointly reachable states.

For further applications see [Kla90b], where the method for Rabin au-

8-6

Klarlund and Kozen Rabin Measures (Ref)

tomata is extended to the ∀-automata of [MP87] and applied to simplify the 19 method of [AS89].

9 Acknowledgments

Thanks to two anonymous referees for useful comments. We are also grateful

9-1

to the managing editor, Michael J. O’Donnell, for his careful help in polishing the article.

Acknowledgement of 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.

References

[AO83] K. R. Apt and E.-R. Olderog. Proof rules and transformations dealing with fairness. Science of Computer Programming, 3:65– 100, 1983.

[APS84] K. R. Apt, A. Pnueli, and J. Stavi. Fair termination revisited with delay. Theoretical Computer Science, 33:65–84, 1984.

[AS87] B. Alpern and F. B. Schneider. Recognizing safety and liveness. Distributed Computing, 2:117–126, 1987.

[AS89] B. Alpern and F. B. Schneider. Verifying temporal properties without temporal logic. ACM Transactions on Programming Languages and Systems, 11(1):147–167, January 1989.

[DH86] I. Dayan and D. Harel. Fair termination with cruel schedulers. Fundamenta Informatica, 9:1–12, 1986.

[EJ88] E. A. Emerson and C. S. Jutla. Complexity of tree automata and logics of programs. In Proceedings of the 29th Symposium on Foundations of Computer Science, pages 328–337, Los Alamitos, CA, 1988. Institute of Electrical and Electronics Engineers.

20 [EJ91] E. A. Emerson and C. S. Jutla. Tree automata, mu-calculus and

determinacy. In Proceedings of the 32nd Symposium on Foundations of Computer Science, San Juan, Puerto Rico, pages 368–377, Los Alamitos, CA, 1991. Institute of Electrical and Electronics Engineers.

[FK84] N. Francez and D. Kozen. Generalized fair termination. In Proceedings of the 11th Symposium on Principles of Programming Languages, Salt Lake City, pages 46–53. Association for Computing Machinery, January 1984.

[Fra86] N. Francez. Fairness. Springer-Verlag, Berlin, Heidelberg, 1986.

[GFMdR85] O. Grumberg, N. Francez, J. A. Makowsky, and W. P. de Roever. A proof rule for fair termination of guarded commands. Information and Control, 66(1/2):83–102, 1985.

[GH82] Y. Gurevich and L. Harrington. Trees, automata, and games. In Proceedings of the 14th Symposium on Theory of Computing, pages 60–65. Association for Computing Machinery, 1982.

[Jon87] B. Jonsson. Modular verification of asynchronous networks. In Proceedings of the 6th Symposium on the Principles of Distributed Computing, pages 152–166. Association for Computing Machinery, 1987.

[KK91] N. Klarlund and D. Kozen. Rabin measures and their applications to fairness and automata theory. In Proceedings of the 6th Symposium on Logic in Computer Science, pages 256–265, Los Alamitos, CA, 1991. Institute of Electrical and Electronics Engineers.

[Kla90a] N. Klarlund. Progress Measures and Finite Arguments for Infinite Computations. PhD thesis, Cornell University, August 1990. Available as Technical Report TR-1153.

[Kla90b] N. Klarlund. Verification conditions for ω-automata and applications to fairness. Technical Report TR-1080, Cornell University, February 1990.

21 [Kla91] N. Klarlund. Progress measures for complementation of ω-

automata with applications to temporal logic. In Proceedings of the 32nd Symposium on Foundations of Computer Science, San Juan, Puerto Rico, pages 358–367, Los Alamitos, CA, 1991. Institute of Electrical and Electronics Engineers.

[Kla92a] N. Klarlund. Liminf progress measures. In S. Brookes, M. Main, A. A. Melton, M. Mislove, and D. Schmidt, editors, Mathematical Foundations of Programming Semantics, 7th International Conference, March 1991, volume 598 of Lecture Notes in Computer Science, pages 477–491, Berlin, Heidelberg, 1992. Springer-Verlag.

[Kla92b] N. Klarlund. Progress measures and stack assertions for fair termination. In Proceedings of the 11th Symposium on Principles of Distributed Computing, Vancouver, pages 229–240, Los Alamitos, CA, 1992. Institute of Electrical and Electronics Engineers.

[Kla94a] N. Klarlund. The limit view of infinite computations. In Proceedings CONCUR ’94: Concurrency Theory, volume 836 of Lecture Notes in Computer Science, pages 351–368, Berlin, Heidelberg, 1994. Springer-Verlag.

[Kla94b] N. Klarlund. Progress measures, immediate determinacy, and a subset construction for tree automata. Journal of Pure and Applied Logic, 69:243–268, 1994. A preliminary version appeared in Proceedings of the 7th Symposium on Logic in Computer Science, 1992.

[LPS81] D. Lehmann, A. Pnueli, and J. Stavi. Impartiality, justice and fairness: the ethics of concurrent termination. In Proceedings of the 8th Colloquium on Automata, Language, and Programming, volume 115 of Lecture Notes in Computer Science, pages 264– 277, Berlin, Heidelberg, 1981. Springer-Verlag.

[Mai89] M. G. Main. Complete proof rules for strong fairness and strong extreme-fairness. Technical Report CU-CS-447-89, Department of Computer Science, University of Colorado, 1989.

22 [McN66] R. McNaughton. Testing and generating infinite sequences by

a finite automaton. Information and Control, 9:521–530, 1966.

[Mos84] A. W. Mostowski. Regular expressions for infinite trees and a standard form of automata. In Computation Theory, Proceedings of the 5th Symposium, volume 208 of Lecture Notes in Computer Science, pages 157–168, Berlin, Heidelberg, 1984. Springer-Verlag.

[MP84] Z. Manna and A. Pnueli. Adequate proof principles for invariance and liveness properties of concurrent programs. Science of Computer Programming, 4(3):257–290, 1984.

[MP87] Z. Manna and A. Pnueli. Specification and verification of concurrent programs by ∀-automata. In Proceedings of the 14th Symposium on Principles of Programming Languages, Munich, West Germany, pages 1–12. Association for Computing Machinery, 1987.

[OL82] S. Owicki and L. Lamport. Proving liveness of concurrent programs. ACM Transactions on Programming Languages and Systems, 4(3):455–495, 1982.

[Rab69] M. O. Rabin. Decidability of second-order theories and automata on infinite trees. Transactions of the American Mathematical Society, 141:1–35, 1969.

[RFG88] R. Rinat, N. Francez, and O. Grumberg. Infinite trees, markings and well-foundedness. Information and Computation, 79:131– 154, 1988.

[Rog67] Hartley Rogers, Jr. Theory of Recursive Functions and Effective Computability. McGraw-Hill Book Company, New York, NY, 1967.

[Saf88] S. Safra. On complexity of ω-automata. In Proceedings of the 29th Symposium on Foundations of Computer Science, pages 319–327. Institute of Electrical and Electronics Engineers, 1988.

23 [SdRG89] F. A. Stomp, W. P. de Roever, and R. T. Gerth. The μ-calculus

as an assertion-language for fairness arguments. Information and Computation, 82:278–322, 1989.

[Sis87] A. P. Sistla. On using automata in the verification of concurrent programs. Technical report, Computer and Intelligent Systems Laboratory, GTE Laboratories Inc, 1987.

[Var91] M. Vardi. Verification of concurrent programs: The automatatheoretic framework. Annals of Pure and Applied Logic, 51:79– 98, 1991.

[Var94] M. Vardi. Rank predicates vs. progress measures in concurrentprogram verification. Technical Report RJ 9879, IBM Research Division, 1994.

24