EECS 298-11: CAD Seminar Wednesday, March 20, 1996, 5pm 531 Cory Hall, Hogan Room New Looks at Old Concepts: Local Liveness and Finitary Fairness Thomas A. Henzinger Univ. of California, Berkeley We argue that the standard executability constraints on liveness conditions ---machine closure for closed systems, and receptiveness for open systems--- are unnecessarily weak and complex, and that liveness should, instead, be specified by augmenting transition systems with liveness conditions that satisfy a LOCALITY constraint. First, locality implies machine closure and receptiveness, and thus permits the modular verification of live transition systems. Second, while machine closure and receptiveness are based on infinite games, locality is based on repeated finite games, and thus easier to check. Third, no expressive power is lost by the restriction to local liveness conditions. We then argue that the standard definition of fairness is also unnecessarily weak and can be replaced by the stronger notion of FINITARY fairness. While standard fairness may require that no enabled transition is postponed forever, finitary fairness requires that for every run of a system there is an unknown bound k such that no enabled transition is postponed more than k consecutive times. If we prove a program property under the assumption of finitary fairness then, in a multiprogramming environment, the program satisfies the property for all fair finite-state schedulers, and in a distributed environment, the program 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 verification of liveness properties is simplified. Second, the fundamental problem of consensus in a faulty asynchronous distributed environment can be solved assuming finitary fairness. Upcoming seminars: March 27: No seminar due to Spring Break April 3: Luca De Alfaro, Stanford Univ. April 8: Henry Verheyen, Aptix Corp. April 10: N. Shankar and M. Srivas, SRI