Report Number: CS-TR-83-964
Institution: Stanford University, Department of Computer Science
Title: Proving precedence properties: the temporal way
Author: Manna, Z ohar
Author: Pnueli, Amir
Date: April 1983
Abstract: This paper explores the three important classes of temporal properties of concurrent programs: invariance, liveness and precedence. It presents the first methodological approach to the precedence properties, while providing a review of the invariance and liveness properties. The approach is based on the 'unless' operator, which is a weak version of the 'until' operator. For each class of properties, we present a single complete proof principle. Finally, we show that the properties of each class are decidable over finite state programs.
http://i.stanford.edu/pub/cstr/reports/cs/tr/83/964/CS-TR-83-964.pdf