## Local Liveness for Compositional Modeling of Fair Reactive Systems

*Rajeev Alur and
Thomas A. Henzinger*
We argue that the standard constraints on liveness conditions in nonblocking
trace models--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 acceptance
conditions that satisfy a *locality* constraint.
First, locality implies machine closure and receptiveness, and thus permits
the composition and 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 illustrate the appeal of local liveness using the model of
*Fair Reactive Systems*, a nonblocking trace model of communicating
processes.

*Proceedings of the
Seventh International Conference on Computer-aided Verification*
(CAV 1995),
Lecture Notes in Computer Science 939,
Springer-Verlag, 1995, pp. 166-179.