On a Classification of Temporal Properties of Concurrent Programs

We consider properties of concurrent and sequential programs viewed as predicates over infinite sequences of program states. Four classes of such properties are identified, which we call here invariance, eventuality, infinitary progress, and asymptotic vanishing. Each class is characterised by the amount of finite information that suffices to decide membership of a trace, leading to a graded notion of decidability at runtime. The taxonomy refines the two-fold distinction of Lamport and Pnueli between properties that are violated in finite time and properties that are confirmed in the limit. The combinatorial structure of how the four classes interrelate is briefly suggested and left for subsequent work.