In our preceding books, we discussed methods for proving safety properties. While the class of safety properties is important, and normally occupies a large portion of a specification, it must be complemented by properties in the other classes. This book addresses the verification of progress properties. We are making the three chapters of the book available for personal and non-commercial use. Any usage of the material contained in the book should be cited as follows:
Zohar Manna and Amir Pnueli. Temporal Verification of Reactive Systems: Progress. Draft, 1996