Report Number: CS-TR-82-915
Institution: Stanford University, Department of Computer Science
Title: Verification of concurrent programs: proving eventualities by well-founded ranking
Author: Manna, Z ohar
Author: Pnueli, Amir
Date: May 1982
Abstract: In this paper, one of a series on verification of concurrent programs, we present proof methods for establishing eventuality and until properties. The methods are based on well-founded ranking and are applicable to both "just" and "fair" computations. These methods do not assume a decrcase of the rank at each computation step. It is sufficient that there exists one process which decreases the rank when activated. Fairness then ensures that the program will eventually attain its goal.
http://i.stanford.edu/pub/cstr/reports/cs/tr/82/915/CS-TR-82-915.pdf