ABSTRACT
I would like to conclude with a note about the origin and motivation for this work. When I turned towards computer science my co-workers were Menachem Magidor and Shai Ben-David, and the first questions we studied were about mutual exclusion protocols, and issues envisaged by L. Lamport concerning the concept of global time. Most of our results are not suitable for an introductory text, but their influence is evident, and the place of system executions in my work can be traced back to that period and is a testimony to the influence of Lamport’s [20] on my work. At that time I was interested in atomic register problems, and it was expressly in order to prove the correctness of the protocol found in [1] that the usage of higher-level properties developed.
