Finitary fairness.
Fairness is a mathematical abstraction: in a multiprogramming environment, fairness abstracts the details of admissible (fair) schedulers; in a distributed environment, fairness abstracts the relative speeds of processors. We argue that the standard definition of fairness often is unnecessarily weak and can be replaced by the stronger, yet still abstract, notion of finitary fairness. While standard weak fairness requires that no enabled transition is postponed forever, finitary weak fairness requires that for every computation of a system there is an unknown bound k such that no enabled transition is postponed more than k consecutive times. In general, the finitary restriction fin(F) of any given fairness  requirement Fis the union of all &ohgr;-regular safety properties contained in F. The adequacy of the proposed abstraction is shown in two ways. Suppose we prove a program property under the assumption of finitary fairness. In a multiprogramming environment, the program then satisfies the property for all fair finite-state schedulers. In a distributed environment, the program then satisfies the property for all choices of lower and upper bounds on the speeds (or timings) of processors. The benefits of finitary fairness are twofold. First, the proof rules for verifying liveness properties of concurrent programs are simplified: well-founded induction over the natural numbers is adequate to prove termination under finitary fairness. Second, the fundamental  problem of consensus in a faulty asynchronous distributed environment can be solved assuming finitary fairness.
Introduction
Interleaving semantics provides an elegant and abstract way of modeling concurrent computation.
In this approach, a computation of a concurrent system is obtained by letting, at each step, one of
the enabled processes execute an atomic instruction. If all interleaving computations of a system
satisfy a property, then the property holds for all implementations of the program independent of
whether the tasks are multiprogrammed on the same processor and which scheduling policy is used,
or whether the system is distributed and what the speeds of different processors are. Furthermore,
the interleaving model is very simple as it reduces concurrency to nondeterminism.
A preliminary version of this paper appears in Proceedings of the Ninth IEEE Symposium on Logic in Computer
Science, pp. 52-61, 1994.
y On leave from Bell Laboratories, Lucent Technologies.
z Supported in part by the ONR YIP award N00014-95-1-0520, by the NSF CAREER award CCR-9501708, by
the NSF grant CCR-9504469, by the AFOSR contract F49620-93-1-0056, by the ARPA grant NAG2-892, and by the
contract 95-DC-324A.
The interleaving abstraction is adequate for proving safety properties of systems (a safety property
is of the form "something bad never happens," for example, mutual exclusion). However, it is
usually not suitable to prove guarantee properties (a guarantee property is of the form "something
good will eventually happen," for example, termination) or more general liveness properties. The
traditional approach to establishing guarantee properties is to require that all fair computations,
instead of all computations, satisfy the property. Intuitively, fairness means that no individual
process is ignored forever. Since all reasonable implementations of the system, whether in multi-programming
or in multiprocessing, are expected to be fair, if we prove that a program satisfies
a property under the assumption of fairness, it follows that the property holds for all possible
implementations of the program.
While the theory of specification and verification using different forms of fairness is well understood
(see, for example, [LPS82, Fra86, MP91]), fairness has two major drawbacks. First, the
mathematical treatment of fairness, both in verification and in semantics, is complicated and requires
higher ordinals. Second, fairness is too weak to yield a suitable model for fault-tolerant
distributed computing. This is illustrated by the celebrated result of Fischer, Lynch, and Paterson
that, under the standard fairness assumption, processes cannot reach agreement in an asynchronous
distributed system even if one process fails. We quote from their paper [FLP85]:
These results do not show that such problems [distributed consensus] cannot be solved
in practice; rather, they point out the need for more refined models of distributed
computing that better reflect realistic assumptions about processor and communication
timings.
We propose one such "more refined" model by introducing the notion of finitary fairness. We argue
that finitary fairness (1) is sufficiently abstract to capture all possible implementations, both in
the context of multiprogramming and in the context of distributed computing, and (2) does not
suffer from either of the two aforementioned disadvantages associated with the standard notion of
fairness.
Justification of finitary fairness
A fairness requirement is specified as a subset F of the set of all possible ways of scheduling different
processes of a program. Let us first consider a multiprogramming environment, where all tasks are
scheduled on a single processor. A scheduler that meets a given fairness requirement F is a program
whose language (i.e., set of computations) is contained in F . The language of any program is a
safety property (i.e., it is closed under limits). Furthermore, if the scheduler is finite-state, then
its language is !-regular. Thus, to capture all finite-state schedulers that implement F , it suffices
to consider the (countable) union of all !-regular safety properties that are contained in F . There
are several popular definitions of F , such as strong fairness, weak fairness, etc. [LPS82, Fra86].
For every choice of F , we obtain its finitary version fin(F ) as the union of all !-regular safety
properties contained in F . In the case of weak fairness F , we show that the finitary version fin(F )
is particularly intuitive: while F prohibits a schedule if it postpones a task forever, fin(F ) also
prohibits a schedule if there is no bound on how many consecutive times a task is postponed. In
general, a fairness requirement F is an !-regular liveness property [AFK88]. We show that the
finitary version fin(F ), then, is still live, but not !-regular.
Now let us consider a distributed environment, where all tasks are executed concurrently on
different processors. Here, finitary fairness corresponds to the assumption that the execution speeds
of all processors stay within certain unknown, but fixed, bounds. Formally, a distributed system
can be modeled as a transition system that imposes lower and upper time bounds on the transitions
[HMP94]. We show that a timed transition system satisfies a property for all choices of lower
and upper time bounds iff the underlying untimed transition system satisfies the same property
under finitary weak fairness. This correspondence theorem not only establishes the adequacy of
finitary fairness for distributed systems, but in addition provides a method for proving properties
of timed systems whose timing is not known a priori.
To summarize, finitary fairness abstracts the details of fair finite-state schedulers and the details
of the independent speeds (timings) of processors with bounded drift. The parametric definition
of finitary fairness also lends itself to generalizations such as computable fairness : the computable
version com(F ) of a fairness assumption F is the (countable) union of all recursive safety properties
that are contained in F . In a multiprogramming environment, computable fairness abstracts the
details of fair computable schedulers; in a distributed environment, computable fairness abstracts
the independent speeds of processors whose drift is bounded by any recursive function.
Benefits of finitary fairness
Verification. We address the problem of verifying that a program satisfies a property under a
finitary fairness assumption fin(F ). Since fin(F ) is not !-regular, it is not specifiable in temporal
logic. This, however, is not an obstacle for verification. For finite-state programs, we show that a
program satisfies a temporal-logic specification under fin(F ) iff it satisfies the specification under
F itself. This means that for finite-state programs, the move to finitary fairness does not call for a
change in the verification algorithm.
For general programs, the proof rules for verifying liveness properties are simplified by the
use of finitary fairness. Suppose we wish to prove that a program terminates. To prove that all
computations of a program terminate, one typically identifies a ranking (variant) function from the
states of the program to the natural numbers such that the rank decreases with every transition
of the program. This method is not complete for proving the termination of all fair computations.
First, there may not be a ranking function that decreases at every step. The standard complete
verification rule, rather, relies on a ranking function that never increases and is guaranteed to
decrease eventually [LPS82, Fra86]. For this purpose, one needs to identify so-called "helpful"
transitions that cause the ranking function to decrease. Second, induction over the natural numbers
is not complete for proving fair termination and one may have to resort to induction over ordinals
higher than !.
We show that proving the termination of a program under finitary weak fairness can be reduced
to proving the termination of all computations of a transformed program. The transformed
program uses a new integer variable, with unspecified initial value, to represent the bound on how
many consecutive times an enabled transition may be postponed. Since the termination of all computations
of the transformed program can be proved using a strictly decreasing ranking function on
the natural numbers, reasoning with finitary fairness is conceptually simpler than reasoning with
standard fairness.
Distributed consensus. A central problem in fault-tolerant distributed computing is the consensus
problem, which requires that the non-faulty processes of a distributed system agree on a
common output value [PSL80]. Although consensus cannot be reached in the asynchronous model
if one process fails [FLP85], in practice, consensus is achieved in distributed applications using
constructs like timeouts. This suggests that the asynchronous model with its standard fairness
assumption is not a useful abstraction for studying fault-tolerance. One proposed solution to this
problem considers the unknown-delay model (also called partially synchronous model) in which there
is fixed upper bound on the relative speeds of different components, but this bound is not known a
priori [DLS88, AAT97, RW92]. The asynchronous model with the finitary fairness assumption is an
abstract formulation of the unknown-delay model. In particular, we prove that the asynchronous
model with the finitary fairness assumption admits a wait-free solution for consensus that tolerates
an arbitrary number of process failures, by showing that finitary fairness can substitute the timing
assumptions of the solution of [AAT97].
Informal Motivation: Bounded Fairness
Before introducing the general definition of finitary fairness (Section 3) and its applications (Sec-
tions 4 and 5), we begin by motivating the finitary version of weak fairness through the intuitive
concept of bounded fairness. Consider the following simple program P 0 with a boolean variable x
and an integer variable y:
initially
repeat x := x forever k repeat y
The program P 0 consists of two processes, each with one transition. The transition l complements
the value of the boolean variable x; the transition r increments the value of the integer variable y.
A computation of P 0 is an infinite sequence of states, starting from the initial state
and such that every state is obtained from its predecessor by applying one of the two
transitions. For the purpose of this example, a schedule is an infinite word over the alphabet fl; rg.
Each computation of P 0 corresponds, then, to a schedule, which specifies the order of the transitions
that are taken during the computation. The two processes of P 0 can be executed either by
multiprogramming or in a distributed environment.
Multiprogramming
In a multiprogramming environment, the two processes of P 0 are scheduled on a single processor.
A scheduler is a set of possible schedules. One typically requires that the scheduler is "fair"; that
is, it does not shut out one of the two processes forever. Formally, a schedule is fair iff it contains
infinitely many l transitions and infinitely many r transitions; a scheduler is fair iff it contains only
fair schedules.
be the set of fair schedules. If we restrict the set of computations of the
program P 0 to those that correspond to fair schedules, then P 0 satisfies a property OE iff every
computation of P 0 whose schedule is in F1 satisfies OE. For instance, under the fairness assumption
F1 , the program P 0 satisfies the property
that is, in any fair computation, the value of x is true in infinitely many states, and the value of
y is even in infinitely many states. Note that there are computations of P 0 that correspond to
unfair schedules, and do not satisfy the formula OE 1 . Thus, the fairness assumption is necessary to
establish that the program P 0 satisfies the property OE 1 .
The fairness requirement F1 is an abstraction of all admissible real-life schedulers, namely, those
that schedule each transition "eventually." Any (non-probabilistic) real-life scheduler, however, is
finite-state and therefore must put a bound on this eventuality.
Consider, for instance, a round-robin scheduler that schedules the transitions l and r alternately.
For round-robin schedulers, we can replace the fairness assumption F1 by the much stronger
assumption F 1 that contains only two schedules, (lr) ! and (rl) ! . Under F 1 , the program P 0
satisfies the property
which implies the property OE 1 . We call F 1 a 1-bounded scheduler. In general, for a positive integer
k, a k-bounded scheduler never schedules one transition more than k times in a row. Formally,
a schedule is k-bounded, for k - 1, iff it contains neither the subsequence l k+1 nor r k+1 ; a scheduler
is k-bounded iff it contains only k-bounded schedules (similar definition is considered in [Jay88]).
Let F k be the set of k-bounded schedules. The assumption F k of k-boundedness is, of course,
not sufficiently abstract, because for any k, it is easy to build a fair finite-state scheduler that is
not k-bounded. So let us say a schedule is bounded iff it is k-bounded for some positive integer k,
and a scheduler is bounded iff it contains only bounded schedules. Clearly, every fair finite-state
scheduler is bounded. In order to prove a property of the program for all implementations, then,
it suffices to prove the property for all bounded schedulers.
be the set of bounded schedules. If we restrict the set of computations of
the program P 0 to those that correspond to bounded schedules, then P 0 satisfies a property OE iff
every computation of P 0 whose schedule is in F ! satisfies OE. We call F ! the finitary restriction of
the fairness assumption F1 .
Three observations about F ! are immediate. First, the finitary version F ! is a proper subset
of F1 ; in particular, the schedule is fair but unbounded, and therefore belongs to
. Second, the set F ! itself is not a finite-state scheduler, but is the countable union of
all fair finite-state schedulers. Third, F ! is again a liveness property, in the sense that a stepwise
scheduler cannot paint itself into a corner [AFK88]: every finite word over fl; rg can be extended
into a bounded schedule 1 .
Since the finitary fairness assumption F ! is stronger than the fairness assumption F1 , a program
may satisfy more properties under F ! . Consider, for example, the property
where the state predicate power-of-2 (y) is true in a state iff the value of y is a power of 2. If a
computation of P 0 does not satisfy OE ! , then it must be the case that the transition l is scheduled
only when power-of-2 (y) holds. It follows that for every positive integer k, there is a subsequence of
length greater than k that contains only r transitions. Such a schedule does not belong to F ! and,
hence, the program P 0 satisfies the property OE ! under F ! . On the other hand, it is easy to construct
a fair schedule that does not satisfy OE ! , which shows that P 0 does not satisfy OE ! under F1 .
Multiprocessing
In a distributed environment, the two processes of P 0 are executed simultaneously on two processors.
While the speeds of the two processors may be different, one typically requires of a (non-faulty)
processor that each transition consumes only a finite amount of time. Again, the fairness requirement
F1 is an abstraction of all admissible real-life processors, namely, those that complete each
transition "eventually." Again, the fairness assumption F1 is unnecessarily weak.
Assume that the transition l, executed on Processor I, requires at least time ' l and at most
time u l , for two unknown rational numbers ' l and u l with u l - ' l ? 0. Similarly, the transition r,
It should also be noted that the set F! does not capture randomized schedulers. For, given a randomized scheduler
that chooses at every step one of the two transitions with equal probability, the probability that the resulting schedule
is in F! is 0. On the other hand, the probability that the resulting schedule is in F1 is 1.
executed on Processor II, requires at least time ' r ? 0 and at most time u r - ' r . Irrespective of
the size of the four time bounds, there is an integer k - 1 such that both k \Delta ' l ? u r and k \Delta ' r ? u l .
Each computation corresponds, then, to a k-bounded schedule. It follows that finitary fairness is
an adequate abstraction for speed-independent processors. It should be noted that finitary fairness
is not adequate if the speeds of different processors can drift apart without bound. For this case,
we later generalize the notion of finitary fairness.
Finitary Fairness
3.1 Sets of infinite words
An !-language over an alphabet \Sigma is a subset of the set \Sigma ! of all infinite words over \Sigma. For instance,
the set of computations of a program is an !-language over the alphabet of program states.
Regularity
An !-language is !-regular iff it is recognized by a B-uchi automaton, which is a nondeterministic
finite-state machine whose acceptance condition is modified suitably so as to accept infinite
words [B-uc62]. The class of !-regular languages is very robust with many alternative characterizations
(see [Tho90] for an overview of the theory of !-regular languages). In particular, the
set of models of any formula of (propositional) linear temporal logic (PTL) is an !-regular language
[GPSS80]. The set of computations of a finite-state program is an !-regular language. The
set F1 (Section 2) of fair schedules over the alphabet fl; rg is an !-regular language (23 l - 23 r),
and so is the set F k of k-bounded schedules, for every k - 1.
Safety and Liveness
For an !-language \Pi ' \Sigma ! , let pref (\Pi) ' \Sigma   be the set of finite prefixes of words in \Pi. The
!-language \Pi is a safety property (or limit-closed) iff for all infinite words w, if all finite prefixes of
w are in pref (\Pi) then w 2 \Pi [ADS86]. Every safety property \Pi is fully characterized by pref (\Pi).
Since a program can be executed step by step, the set of computations of a program is a safe
!-language over the alphabet of program states.
A safety property is !-regular iff it is recognized by a B-uchi automaton without acceptance
conditions. Properties defined by temporal-logic formulas of the form 2 p, where p is a past formula
of PTL, are safe and !-regular. For every k - 1, the set F k (Section 2) of k-bounded schedules is
an !-regular safety property.
The !-language \Pi is a liveness property iff pref that is, every finite word can
be extended into a word in \Pi. The set F1 (Section 2) of fair schedules is an !-regular liveness
property.
Topological characterization
Consider the Cantor topology on infinite words: the distance between two distinct infinite words
w and w 0 is 1=2 i , where i is the largest nonnegative integer such that w
The closed sets of the Cantor topology are the safety properties; the dense sets are the liveness
properties. All !-regular languages lie on the first two-and-a-half levels of the Borel hierarchy:
every !-regular language is in F oeffi " G ffioe . 2
There is also a temporal characterization of the first two-and-a-half levels of the Borel hierarchy
[MP90]. Let p be a past formula of PTL. Then every formula of the form 2 p defines an
F-set; every formula of the form 3 p, a G-set; every formula of the form 23 p, a G ffi -set; and every
formula of the form 32 p, an F oe -set. For example, the set F1 of fair schedules is a G ffi -set.
3.2 The finitary restriction of an !-language
Now we are ready to define the operator fin:
The finitary restriction fin(\Pi) of an !-language \Pi is the (countable) union of all !-regular
safety languages that are contained in \Pi.
By definition, the finitary restriction of every !-language is in F oe . Also, by definition, fin(\Pi) ' \Pi.
The following theorem states some properties of the operator fin.
Theorem 1 Let \Pi, \Pi 0 be !-languages:
1.
2. fin is monotonic: if \Pi ae \Pi 0 then fin(\Pi) ae fin(\Pi 0 ).
3. fin distributes over intersection: fin(\Pi "
Proof. The first two follow immediately from the definition of fin. Since \Pi " \Pi 0 is contained in
\Pi as well as in \Pi 0 , from the monotonicity, we have To prove the
inclusion From the definition
of fin, there exist !-regular safety properties
1 .
The class of safety properties is closed under intersection, and so is the class of !-regular languages.
Hence,
1 is an !-regular safety property. Since w
The following proposition formalizes the claims we made about the example in Section 2. It also
shows that the finitary restriction of an !-regular language is not necessarily !-regular.
Proposition 2 Let F1 be the set of fair schedules from Section 2, and let F ! be the set of bounded
schedules. Then F ! is the finitary restriction of F1 (that is, neither
!-regular nor safe.
Proof. Recall that F is the union of !-regular safety properties contained
in F1 . Each F k is an !-regular safety property and F k ae F1 . Hence,
Now consider an !-regular safety property G contained in F1 . Suppose G is accepted by a
B-uchi automaton MG over the alphabet fl; rg. Without loss of generality, assume that every state
of MG is reachable from some initial state, and every state is an accepting state (since G is a safety
property). We wish to prove that if MG has k states then G ' F k . Suppose not. Then there is a
word w such that MG accepts w and w contains consecutive symbols of the same type, say
l. Thus Since MG has only k states, it follows
2 The first level of the Borel hierarchy consists of the class F of closed sets and the class G of open sets; the second
level, of the class G ffi of countable intersections of open sets and the class F oe of countable unions of closed sets; the
third level, of the class F oeffi of countable intersections of F oe -sets and the class G ffioe of countable unions of G ffi -sets.
that there is a state s of MG such that there is a path from the initial state to s labeled with w 0 l i
for some 0 - i - k, and there is a cycle that contains s and all of whose edges are labeled with
l. This implies that MG accepts the word w which is not a fair schedule, a contradiction to the
inclusion G ' F1 .
Observe that, for each k - 1, the schedule l k can be extended to a word in F k , and hence
implying that F ! is not closed under limits, that is, F ! is not a
safety property.
Now we prove that F ! is not !-regular. Suppose F ! is !-regular. From the closure properties
of !-regular languages, the set of unbounded fair schedules is also !-regular. We
know that G is nonempty (it contains the schedule From the properties of !-
regular languages it follows that G contains a word w such that for two finite words
contains at least one l and one r symbol. This means that, for
a contradiction to the assumption that w 62 F ! .
In other words, although F ! is a countable union of safety properties that are definable in PTL, F !
itself is neither a safety property nor definable in PTL. To define F ! in temporal logic, one would
need infinitary disjunction. In general, the operator fin does not preserve liveness also. That is,
it may happen that pref However, when applied to !-regular
properties, liveness is preserved.
Theorem 3 If \Pi be an !-regular language then pref
Proof. Since fin(\Pi) ' \Pi and pref is monotonic, pref (fin(\Pi)) ' pref (\Pi). To prove the inclusion
pref (\Pi) ' pref (fin(\Pi)), suppose \Pi is !-regular language over \Sigma, and consider w 2 pref (\Pi). From
!-regularity of \Pi, it follows that there is a word w 0 2 \Pi such that w
2 for finite words
. The language containing the single word w 0 is !-regular, safe, and contained in \Pi.
Hence,
This immediately leads to the following corollary:
Corollary 4 If \Pi is an !-regular liveness property then fin(\Pi) is live.
Observe that the language F1 is !-regular and live, and hence, F ! is also live: pref
This means that when executing a program, the fairness requirement F ! , just like the original
requirement F1 , can be satisfied after any finite number of steps.
The operator fin is illustrated on some typical languages below:
9k such that every subsequence of length k has some pg;
9k such that every subsequence with k p's has some qg.
3.3 Transition systems
From standard fairness to finitary fairness
Concurrent programs, including shared-memory and message-passing programs, can be modeled as
transition systems [MP91].
A transition system P is a triple (Q; a set of states, T is a finite set of
transitions, and Q 0 ' Q is a set of initial states. Each state q 2 Q is an assignment of values to all
program variables; each transition - 2 T is a binary relation on the states (that is, - ' Q 2 ). For a
state q and a transition - , let be the set of -successors of q. A computation
q of the transition system P is an infinite sequence of states such that q 0 2 Q 0 and for all i - 0,
there is a transition - 2 T with q for the set of computations of P . The
set \Pi(P ) is a safe !-language over Q. If Q is finite, then \Pi(P ) is !-regular.
A transition - is enabled at the i-th step of a computation q iff -(q i ) is nonempty, and - is
taken at the i-th step of q iff q loss of generality, we assume that the set of
program variables contains for every transition - 2 T a boolean variable enabled(-) and a boolean
variable taken(- ). Let the scheduling alphabet \Sigma T be the (finite) set of interpretations of these
boolean variables, that is, \Sigma T is the power set of the set fenabled(-); taken(-) j - 2 Tg. Given a
computation q of P , the schedule oe(q) of q is the projection of q to the scheduling alphabet. The
set of schedules of P , then, is a safety property over \Sigma T .
A fairness requirement F for the transition system P is an !-language over the finite scheduling
alphabet \Sigma T . The fairness requirement restricts the set of allowed computations of the program.
In general, F is an !-regular liveness property [AFK88]. The requirement of liveness ensures that,
when executing a program, a fairness requirement can be satisfied after any finite number of steps.
In particular, the requirement of weak fairness WF for P is the set of all infinite words w
such that for every transition - 2 T , there are infinitely many integers i - 0 with taken(-) 2 w i or
no transition is enabled forever without being taken. It is specified by the
following
The requirement WF is !-regular and live.
The requirement of strong fairness SF for P is the set of all infinite words w
T such that
for every transition - 2 T , if there are infinitely many steps
there are infinitely many steps no transition is enabled infinitely
often without being taken. It is a stronger requirement than the weak fairness (SF ae WF ), and is
specified by the formula -
The weak-fairness requirement WF is a G ffi -set; the strong-fairness requirement SF is neither
in G ffi nor in F oe , but lies in F oeffi " G ffioe . Since both sets are !-regular, their finitary restrictions
fin(WF) and fin(SF ), which belong to F oe , are again live (Corollary 4).
The next theorem (a generalization of Proposition 2) shows that the finitary restriction of weak
and strong fairness coincide with the appropriate notions of bounded fairness. Define a schedule
T to be weakly-k-bounded , for a nonnegative integer k, iff for all transitions - of P , - cannot be
enabled for more than k consecutive steps without being taken, that is, for all integers i - 0, there
is an integer j, or enabled(-) 62 w j . A schedule is weakly-bounded
if it is weakly-k-bounded for some k - 0. Similarly, a schedule w is strongly-k-bounded iff for all
transitions - , if a subsequence of w contains k distinct positions where - is enabled, then it contains
a position where - is taken, that is, for all integers
for
A schedule is strongly-bounded if it is
strongly-k-bounded for some k - 0.
Theorem 5 Let P be a transition system with the transition set T and the weak and strong fairness
requirements WF and SF . For all infinite words w over \Sigma T , w
and w 2 fin(SF) iff w is strongly-bounded.
Proof. We will consider only the weak fairness. The set of weakly-k-bounded schedules, for a
fixed k, is defined by the formula
where wf (-) stands for the disjunction taken(-:enabled(- ). It follows that the set of weakly-k-
bounded schedules is safe and !-regular, for all k - 0. Thus, every weakly-bounded schedule is in
Now consider an !-regular safety property G contained in WF . Suppose G is accepted by a
B-uchi automaton MG over the alphabet \Sigma T . Without loss of generality, assume that every state
of MG is reachable from its initial state, and every path in MG is an accepting path. It suffices to
prove that if MG has k states then every schedule in G is weakly-k-bounded. Suppose not. Let us
say that a symbol of \Sigma T is weakly-unfair to a transition - , if it contains enabled(-) and does not
contain taken(- ). From assumption, there is a word w accepted by MG and a transition - such
that w contains k consecutive symbols all of which are weakly-unfair to - . Since MG has only
states, it follows that there is a cycle in MG all of whose edges are labeled with symbols that
are weakly-unfair to - . This implies that MG accepts a schedule that is not weakly-fair to - , a
contradiction to the inclusion G ' WF .
Observe that for the example program P 0 of Section 2, rg, the propositions enabled(l) and
are true in every state, and the fairness requirement F1 equals both WF and SF . This
implies that
Corollary 6 If P is a transition system with at least two transitions, then both fin(WF ) and
fin(SF) are neither !-regular nor safe.
A computation q of the transition system P is fair with respect to the fairness requirement F
We write \Pi F (P ) for the set of fair computations of P . A specification \Phi for the
transition system P is a set of infinite words over the alphabet Q. The transition system P satisfies
the specification \Phi under the fairness requirement F iff \Pi F (P ) ' \Phi. If we prove that P satisfies \Phi
under the fairness assumption F , then P satisfies \Phi for all implementations of F ; if we prove that P
satisfies \Phi under the finitary restriction fin(F ), then P satisfies \Phi for all finite-state implementations
of F . In Section 4, we show that proving the latter is conceptually simpler than proving the former.
3.4 Timed transition systems
From timing to finitary fairness
Standard models for real-time systems place lower and upper time bounds on the duration of
delays [HMP94, MMT91]. Since the exact values of the time bounds are often not known a priori,
it is desirable to design programs that work for all possible choices of time bounds. It has been
long realized that the timing-based model with unknown delays is different from, and often more
appropriate than, the asynchronous model (with standard fairness) [DLS88, AAT97, RW92]. We
show that the unknown-delay model is equivalent to the asynchronous model with finitary fairness.
Real-time programs can be modeled as timed transition systems [HMP94]. A timed transition
system P ';u consists of a transition system two functions ' and u from the set
T of transitions to the set Q?0 of positive rational numbers. The function ' associates with each
transition - a lower bound ' - ? 0; the function u associates with - an upper bound u - .
The interleaving semantics of transition systems is extended to timed transition systems by
labeling every state of a computation with a real-valued time stamp. A time sequence t is an
infinite nondecreasing and unbounded sequence of real numbers. For t to be consistent with a
given computation q of the underlying transition system P , we require that a transition - has
to be enabled continuously at least for time ' - before it is taken, and it must not stay enabled
continuously longer than time u - without being taken. Note that if a transition - is enabled in
all states q n , for i - n - j, and - is not taken in all states q n , for then it has been
continuously enabled for t Then, the time
sequence t is consistent with the computation q iff for every transition - 2 T ,
[Lower bound ] if taken(-) 2 q j , then for all steps i with
and taken(-) 62 q
[Upper bound ] if enabled(-) 2 q k for all steps k with i - k - j, and taken(-) 62 q k for all steps k
with
A timed computation (q; t) of the timed transition system P ';u consists of a computation q of P
together with a consistent time sequence t. The first component of each timed computation of P ';u
is an untimed computation of P ';u . We write \Pi ';u (P ) for the set of untimed computations of P ';u .
In general, \Pi ';u (P ) is a strict subset of \Pi(P ); that is, the timing information ' and u plays the same
role as fairness, namely, the role of restricting the admissible interleavings of enabled transitions.
If Q is finite then, like \Pi(P ), \Pi ';u (P ) is also !-regular [AD94] (but not necessarily safe).
While the timed computations are required for checking if a system satisfies a specification that
refers to time, the untimed computations suffice for checking if the system satisfies an untimed
specification \Phi ' timed transition system P ';u satisfies the specification \Phi iff \Pi ';u (P
In the unknown-delay model, we do not know the bound functions ' and u, but rather wish to prove
that a transition system P satisfies the specification \Phi for all possible choices of bound functions;
that is, we wish to prove that the union [ ';u \Pi ';u (P ) is contained in \Phi. The following theorem
shows that in order to verify a system in the unknown-delay model, it suffices to verify the system
under finitary weak fairness; that is, the union [ ';u \Pi ';u (P ) is same as the set \Pi fin(WF) (P ).
Theorem 7 Let P be a transition system with the set T of transitions, let WF be the weak fairness
requirement for P , and let q be a computation of P . Then q 2 \Pi fin(WF) (P ) iff for some function '
and u from T to Q?0 , q 2 \Pi ';u (P ).
Proof. Consider a weakly-bounded computation q 2 \Pi fin(WF) (P ). From Theorem 5, there is a
nonnegative integer k such that the schedule corresponding to q is weakly-k-bounded. Let the
bound functions be defined as ' . Consider the time
sequence increases by 1 at every step, it is clear that the
lower bound requirement is trivially satisfied. Since q is weakly-k-bounded, no transition is enabled
for more than k consecutive steps (and hence, for more than k being taken.
Thus, the consistency requirements are satisfied, and (q; t) is a timed computation of P ';u , implying
To prove the converse, suppose q 2 \Pi ';u (P ) for some choice of ' and u. Let t be a time
sequence such that (q; t) is a timed computation of P ';u . Let '   be the (nonzero) minimum of all
the lower bounds ' - , and u   be the (finite) maximum of all the upper bounds u - . Let the number
of transitions in T be n. Let k be an integer such that k ? nu
'   . We claim that the schedule
corresponding to q is weakly-k-bounded. Suppose not. Then there is a transition - and i - 0 such
that - is enabled but not taken at all states q . At every step of q, taken(- 0 ) holds for
some transition - 0 . Since k ? nu
'   , it follows that, there is a transition - 0 such that taken(- 0 ) holds
at more than u
'   distinct states between q i and q i+k . Since '(- 0 , from the assumption that t
satisfies the lower bound requirement, we have t
implies that t violates the upper bound requirement of consistency, a contradiction. In conclusion,
q is weakly-k-bounded, and hence, q 2 \Pi fin(WF) (P ).
We point out that all lower bounds are, although arbitrarily small, nonzero, and all upper bounds
are finite. This is necessary, and justified because we universally quantify over all choices of bound
functions. We also point out that reasoning in a timing-based model with specific bound functions-
i.e., reasoning about timed computations-can be significantly more complicated than untimed
reasoning [HMP94]. Our analysis shows, therefore, that the verification of specifications that do
not refer to time is conceptually simpler in the unknown-delay model than in the known-delay
model.
3.5 The gap between finitary and standard fairness
The definition of finitary fairness replaces a given !-language \Pi by the union of all !-regular safety
properties contained in \Pi. While this definition seems satisfactory in practice, there are obvious
mathematical generalizations.
First, observe that the (uncountable) union of all safety properties contained in \Pi is \Pi itself.
Not all safety properties, however, are definable by programs. We can obtain the computable
restriction com(\Pi) of \Pi by taking the (countable) union of all recursive safety properties that are
contained in \Pi (an !-language is recursive iff it is the language of a Turing machine). Clearly,
com(\Pi) captures all possible implementations of \Pi, finite-state or not, and typically falls strictly
between fin(\Pi) and \Pi. Computable fairness, however, does not have the two advantages of finitary
fairness, namely, simpler verification rules and a solvable consensus problem.
There are also alternatives between fin(\Pi) and com(\Pi), which capture all implementations of
\Pi with limited computing power. Recall the sample program P 0 from Section 2. For every schedule
in fin(\Pi), there is a bound, unknown but fixed, on how long a transition can be postponed. Suppose
that we let this bound vary, and call a schedule linearly bounded iff the bound is allowed to increase
linearly with time. While every bounded schedule is linearly bounded, the schedule
is linearly bounded but not bounded. In general, given a function f(n) over the natural numbers,
a schedule w O(f)-bounded iff there exists a constant k such that each of the two
transitions l and r appears at least once in the subsequence w n w
Finitary fairness, then, is O(1)-fairness. Moreover, for any fairness requirement F , we obtain a
strict hierarchy of stronger fairness requirements f(F ), where f(F ) is the union of all O(f)-bounded
schedulers that are contained in F . The algorithm presented in Section 5 can be modified so that it
solves distributed consensus under the fairness requirement f(F ) for any fixed, computable choice
of f .
4 Application: Program Verification
We now consider the problem of verifying that a program satisfies a specification under a finitary
fairness assumption.
4.1 Model checking
If all program variables range over finite domains, then the set of program states is finite. The
problem of verifying that such a finite-state program satisfies a temporal-logic specification is called
model checking . Automated tools for model checking have been successfully used to check the
correctness of digital hardware and communication protocols [CK96]. Here we examine the effects
of finitary fairness on the algorithms that underlie these tools.
Untimed systems
Consider a finite-state transition system P with the state set Q. The set \Pi(P of computations
of P is an !-regular safety property. Since Q is finite, we choose the scheduling alphabet
to be Q itself. Let F ' Q ! be an !-regular fairness requirement, and let \Phi ' Q ! be an !-regular
specification (given, say, by a PTL formula or a B-uchi automaton). The verification question, then,
is a problem of language inclusion: P satisfies \Phi under F iff \Pi(P This problem can be
solved algorithmically, because all involved languages are !-regular. Assuming finitary fairness, we
need to check the language inclusion \Pi(P It is, however, not obvious how to check
this, because fin(F ) is not necessarily !-regular (Corollary 6). The following theorem shows that
finite-state verification for finitary fairness can be reduced to verification under standard fairness.
Theorem 8 For all !-regular languages \Pi 1 and \Pi 2 ,
Proof. We have then so is fin(\Pi
suppose that \Pi 1 " \Pi 2 is nonempty. Since both \Pi 1 and \Pi 2 are !-regular, so is
contains a word w such that
. The language containing the
single word w is safe, !-regular, and contained in \Pi 1 . Hence, w 2 fin(\Pi 1 ), and also in fin(\Pi 1
implying that fin(\Pi 1 nonempty.
As a corollary we obtain that for model checking under finitary fairness, we can continue to use
the algorithms that have been developed to deal with standard fairness:
Corollary 9 For a finite-state program P with set Q of states, an !-regular fairness requirement
and an !-regular specification \Phi ' under the fairness assumption F iff
satisfies \Phi under the fairness assumption fin(F ).
Proof. We want to show that
Let G be the !-language \Pi(P From the assumption that P is finite-state, \Pi(P ) is
!-regular. Since \Phi is also !-regular, so is G. Now \Pi(P
is empty (by Theorem
Timed systems
Consider a finite-state timed transition system P ';u with set Q of states. Suppose the specification
does not refer to time at all, and is given as an !-regular specification \Phi ' Q ! . To verify that P ';u
satisfies \Phi, we want to check the inclusion \Pi ';u (P This problem is solved by constructing
a B-uchi automaton that recognizes the language \Pi ';u (P ) [AD94]. This method is applicable only
when the bound functions ' and u are fully specified. In the parametric verification problem, the
bound maps are not fully specified [AHV93]. The bounds are viewed as parameters:
values of these parameters are not known, but are required to satisfy certain (linear) constraints
(such as ' - 1
,
). The parametric verification problem, then, is specified by
1. a finite-state transition system
2. an !-regular specification \Phi '
3. a set LU consisting of pairs ('; u) of functions from T to Q?0 .
The verification problem is to check that, for every choice of ('; u) 2 LU , the resulting timed
transition system P ';u satisfies the specification \Phi. Define
(';u)2LU
\Pi ';u (P
Then, we want to check \Pi LU (P Theorem 8, together with Theorem 7, implies that the
parametric verification problem is decidable when the set LU consists of all function pairs.
If P is a finite-state transition system, \Phi is !-regular, and
the parametric verification problem of checking the inclusion \Pi LU (P ) ' \Phi is decidable.
The parametric verification problem, in general, is undecidable if the class LU constrains the allowed
choices of the bound maps [AHV93]. For instance, if LU requires that '
then the parametric verification problem is undecidable.
4.2 Proof rules for termination
We now turn to the verification of programs that are not finite-state. Since safety specifications
are proved independent of any fairness assumptions, we need to be concerned only with liveness
specifications. We limit ourselves to proving the termination of programs (or, equivalently, to
proving specifications of the form 3 p for a state predicate p) under finitary weak fairness. It
is straightforward to extend the proposed method to the verification of arbitrary temporal-logic
specifications under the finitary versions of both weak and strong fairness.
Total termination versus just termination
system. The standard method for proving the termination of
sequential deterministic programs can be adopted to prove that all computations of the (nondeter-
ministic) transition system P terminate, which is called the total termination of P . Essentially, we
need to identify a well-founded domain (W; OE) and a ranking (variant) function from the program
states to W such that the rank decreases with every program transition. As an example, consider
the rule T from [LPS82].
Rule T for proving total termination:
Find a ranking function ae from Q to a well-founded domain (W; OE), and a state predicate
(T2) For all states q; q

Figure

The rule T is complete for proving total termination; that is, all computations of a transition
system P terminate iff the rule T is applicable [LPS82]. Furthermore, it is always sufficient to
choose the set N of natural numbers as the well-founded domain W .
Now consider the requirement that all weakly-fair computations of P terminate, which is called
the just termination of P . While the rule T is obviously sound for proving just termination, it is
not complete. The problem is that there may not be a ranking function that decreases with every
program transition. The standard solution is to identify a ranking function that never increases, and
that is guaranteed to decrease eventually. The decrease is caused by so-called "helpful" transitions,
whose occurrence is ensured by the weak-fairness requirement. As an example, consider the rule J
from [LPS82].
Rule J for proving just termination:
Find a ranking function ae from Q to a well-founded domain (W; OE), and a set R - of
state predicates, one for each transition - 2 T . Let R be the union of all R - for - 2 T .
Show for all states q; q 0 2 Q and all transitions -
some transition is enabled in q, then - is enabled in q.
The rule J is complete for proving just termination: all weakly-fair computations of a transition
system P terminate iff the rule J is applicable. Completeness, however, no longer holds if we require
the well-founded domain to be the set N of natural numbers: there are transition systems for which
transfinite induction over ordinals higher than ! is needed to prove just termination.
An example
Before we present the method for proving termination of finitary fair computations, let us consider
an example. Consider the transition system P 1 of Figure 1. A state of the program P 1 is given by
the values of its two variables: the location variable - ranges over f0; 1g, and the data variable x
is a nonnegative integer; initially The four transitions e 1 are as shown in the
figure.
We want to prove that all weakly-fair computations of P 1 terminate. Initially
transitions e 1 and e 2 are continuously enabled. Fairness to e 2 ensures that eventually
e 4 is enabled as long as x is positive, and decrements x each time, fairness to e 4 ensures that

Figure

2: Transformed program fin(P 1 )
eventually resulting in termination. To prove termination formally, we apply the rule J. As
the well-founded domain, we choose the set N[f!g of natural numbers together with the ordinal !.
Choose R e 1
and R e 3
to be the empty sets; a state (-; x) belongs to R e 2
belongs to R e 4
1. The ranking function is defined as: ae(0; x. The transitions e 1 and
e 3 leave the rank unchanged, while e 2 and e 4 cause a decrease. The reader can check that the five
premises (J1)-(J5) of the rule J are indeed satisfied. Notice that there is no bound on the number
of steps before P 1 terminates. This unbounded nondeterminism is what makes the mathematical
treatment of fairness difficult.
Proving the termination of P 1 under finitary weak fairness-that is, proving the finitary just
termination of P 1 -is conceptually simpler. Recall that for every computation in fin(WF ), there is
an integer k such that a transition cannot be enabled continuously for more than k steps without
being taken (Theorem 5). It follows that, under finitary weak fairness, P 1 must terminate within a
bounded number of steps, where the bound depends on the unknown constant k. To capture this
intuition, we transform the program P 1 by introducing the two auxiliary variables b and c. The
initial value of the variable b is an unspecified nonnegative integer, and the program transitions do
not change its value. The integer variable c is used to ensure that no transition is enabled for more
than b steps without being taken. We thus obtain the new program fin(P 1 ) of Figure 2.
The original program P 1 terminates under the finitary weak fairness assumption fin(WF) iff all
computations of the transformed program fin(P 1 ) terminate. Thus, we have reduced the problem
of proving the finitary just termination of P 1 to the problem of proving the total termination of
That is, the simple rule T with induction over the natural numbers is sufficient to prove
finitary just termination. A state of fin(P 1 ) is a tuple (-; x; c; b). To apply the rule T, we choose
the set R to be the set of reachable states: (0; x; c; b) 2 R iff
b. The ranking function is a mapping from R to the natural numbers defined by
ae(0; c. The reader should check that every
transition, applied to any state in R, causes the ranking function to decrease.
Notice that the transformed program fin(P 1 ) has infinitely many initial states, but for any
given initial state, it terminates within a bounded number of steps. Consequently, fin(P 1 ) does not
suffer from the problems caused by unbounded nondeterminism. The tradeoff between proving just
termination of P 1 , and total termination of fin(P 1 ) should be clear: while the rule J used for the
former is more complex than the rule T used for the latter, the program fin(P 1 ) is more complex
than
Finitary transformation of a program
Let us consider a general transformation for a given transition system
consist of m transitions . The finitary transformation fin(P ) of the transition system
P is obtained by introducing a new integer variable b, and for each transition -
new integer variable c i . Thus, the state space of fin(P ) is Q \Theta N m+1 . The initial value of b is
arbitrary; the initial value of each c i is 0. Thus, the set of initial states of fin(P ) is Q 0 \Theta N \Theta f0g m .
For every transition - 2 T , the transition system fin(P ) contains a transition fin(-) such that
1.
2.
3. for 1
The following theorem establishes the transformation fin together with the simple rule T as a sound
and complete proof method for finitary just termination.
Theorem 11 A transition system P terminates under finitary weak fairness iff all computations
of the transition system fin(P ) terminate.
Proof. Suppose the program fin(P ) has a nonterminating computation q. Consider the projection
q 0 of q on the state-space of P . From the transition rules of fin(P ), it is clear that q 0 is also a
computation of P . The value of the bound variable b stays unchanged throughout q, let it be
k. Furthermore, c i - k, is an invariant over the computation q for all 1 - i - m. Since for each
transition - i , c i is incremented each time - i is enabled but not taken, it follows that the computation
q 0 is weakly-k-bounded. Hence, P has a weakly-fair nonterminating computation.
Conversely, consider a weakly-fair nonterminating computation q of P . From Theorem 5, q is
weakly-k-bounded for some k. Define the sequence q 0 over the state-space of fin(P ) as follows.
For all i - 0, q 0
j is the maximum nonnegative integer n such that the
transition - j is enabled but not taken in all states q n 0 for It is easy to check that,
since q is weakly-k-bounded, if the transition - j is enabled, but not taken, in state q i then c i
Consequently, q 0 is a (nonterminating) computation of fin(P ).
Thus, the language \Pi fin(WF) (P ) of finitary weak-fair computations of the transition system P is
the projection of the language \Pi(fin(P )) of the transformed program fin(P ). It is known that given
a transition system P and a fairness requirement F , there exists a transition system P 0 such that
requires uncountably many states (the
transformed program P 0 has one initial state for every fair computation in F ), and does not yield
a proof principle for which well-founded induction over N is adequate.
5 Application: Distributed Consensus
We consider the consensus problem in a shared-memory model where the only atomic operations
allowed on a shared register are read and write. Formally, the consensus problem is defined as
follows. There are n processes each with a boolean input value in i 2 f0; 1g. The
process decides on the value v 2 f0; 1g by executing the statement decide(v). To model failures,
we introduce a special transition fail i for each process. The transition fail i is enabled only if the
Shared registers: initially: out =?, y[
1. while out =? do
2. x[r
3. if y[r i
4. if x[r
5. else for do skip od;
7. r i := r
8. fi
9. od;
10. decide(out).

Figure

3: Consensus, assuming finitary weak-fairness (program for process P i with input in i )
process P i has not yet decided on a value. When P i takes the transition fail i , all of its transitions
are disabled, and P i stops participating.
A solution to the consensus problem must satisfy agreement-that is, no two processes decide
on conflicting values-and validity-that is, if a process decides on the value v, then v is equal to
the input value of some process. Apart from these two safety requirements, we want the nonfailing
processes to decide eventually: wait-freedom asserts that each process P i eventually either decides
on some value or fails. Thus a process must not prevent another process from reaching a decision,
and the algorithm must tolerate any number of process failures. The implicit fairness assumption
in the asynchronous model is the weak-fairness requirement WF for all program transitions except
the newly introduced fail i transitions. It is known that, even for there is no program that
satisfies all three consensus requirements under the weak-fairness assumption WF [FLP85, LA87].
On the other hand, consensus can be solved in the unknown-delay model, where it is assumed
that there is an upper bound \Delta on memory-access time, but the bound is unknown to the processes
a priori and a solution is required to work for all values of \Delta [AAT97]. We show that the consensus
algorithm of [AAT97] for the unknown-delay model solves, in fact, consensus under the finitary
weak-fairness requirement fin(WF ). The algorithm is shown in Figure 3. The algorithm proceeds
in rounds and uses the following shared data structures: an infinite two-dimensional array x[ ; 2]
of bits, and an infinite array y[ ] whose elements have the value ?, 0, or 1. The decision value
(i.e., the value that the processes decide on) is written to the shared bit out, which initially has the
value ?. In addition, each process P i has a local register v i that contains its current preference for
the decision value, and a local register r i that contains its current round number.
If all processes in a round r have the same preference v, then the bit x[r; -v] is never set to 1,
and consequently, processes decide on the value v in round r. Furthermore, if a process decides on
a value v in round r, then y[r] is never set to the conflicting value -
v, and every process that reaches
round has the preference v for that round. This ensures agreement (see [AAT97] for more
details of proofs). It is easy to check that if all processes have the same initial input v, then no
process will ever decide on - v; implying the requirement of validity.
It is possible that two processes with conflicting preferences for round r cannot resolve their
conflict in round r, and proceed to round (r conflicting preferences. This happens
only if both of them find y[r] =? first (line 3), and one of them proceeds and chooses its preference
for the next round (line 7) before the other one finishes the assignment to y[r]. The finitary fairness
requirement ensures that this behavior cannot be repeated in every round. In every finitarily fair
computation, there is a bound k such that every process that has neither failed nor terminated
takes a step at least once every k steps. Once the round number exceeds the (unknown) bound k,
while a process is executing its for loop, all other processes are forced to take at least one step.
This suffices to ensure termination.
Theorem 12 The program of Figure 3 satisfies the requirements of agreement, validity, and wait-
freedom under the finitary fairness assumption fin(WF ).
By contrast, the program does not satisfy wait-freedom under the standard fairness assumption WF .
Also observe that the algorithm uses potentially unbounded space, and therefore is not a finite-state
program. The results of Section 4 imply that there is no algorithm that uses a fixed number of
bounded registers and solves consensus under finitary fairness.
Theorem 13 For two processes, there is no algorithm that uses finite memory, and satisfies the requirements
of agreement, validity, and wait-freedom under the finitary fairness assumption fin(WF)
(or equivalently, in the unknown-delay model).
The unknown-delay model of [DLS88] consists of distributed processes communicating via messages,
where the delivery time for each message is bounded, but is not known a priori. They establish
bounds on the number of process-failures that can be tolerated by consensus protocol under various
fault models. These bounds can be established using the finitary weak-fairness. Similar observation
applies to the results on the session problem for the unknown-delay model [RW92].

Acknowledgments

. Notions that are similar to k-bounded fairness, for a fixed k, have been
defined in several places [Jay88]; the notion of bounded fairness seems to be part of the folklore, but
we do not know of any published account. We thank Leslie Lamport, Amir Pnueli, Fred Schneider,
Gadi Taubenfeld, and Sam Toueg for pointers to the literature and for helpful discussions.



--R


A theory of timed automata.
Safety without stuttering.
Appraising fairness in languages for distributed programming.
Parametric real-time reasoning
Defining liveness.
On a decision method in restricted second-order arithmetic

Consensus in the presence of partial synchrony.
Impossibility of distributed consensus with one faulty process.

On the temporal analysis of fairness.
Temporal proof methodologies for timed transition systems.
Communication and Synchronization in Parallel Computation.
Memory requirements for agreement among unreliable asynchronous processes.

Time constrained automata.
A hierarchy of temporal properties.
The temporal logic of reactive and concurrent systems.
Reaching agreement in the presence of faults.
The impact of time on the session problem.
Automata on infinite objects.
Verification of concurrent programs: the automata-theoretic framework
--TR
Fairness
Safety without stuttering
Consensus in the presence of partial synchrony
A hierarchy of temporal properties (invited paper, 1989)
Automata on infinite objects
The temporal logic of reactive and concurrent systems
The impact of time on the session problem
Parametric real-time reasoning
A theory of timed automata
Temporal proof methodologies for timed transition systems
Impossibility of distributed consensus with one faulty process
Computer-aided verification
Formal methods
Time-Adaptive Algorithms for Synchronization
Reaching Agreement in the Presence of Faults
On the temporal analysis of fairness
Impartiality, Justice and Fairness
Time-Constrained Automata (Extended Abstract)
Design and Synthesis of Synchronization Skeletons Using Branching-Time Temporal Logic
Communication and synchronization in parallel computation
distributed consensus;modeling of asynchronous systems;fairness;program verification