Paper Revirew

DEFINING LIVENESS Bowen ALPERN and Fred B. SCHNEIDER

This paper provides a formal definition of liveness property and has shown that no less restrictive definition would be correct. It also proves some theorems based on the definition. After the formalization of safety property, this paper provides some insight on liveness properties and shows that all properties are the intersection of safety and liveness properties.

This research is important because it converts the definition of liveness property from “someting good will happen” to an expression which helps understand the meaning and characteristics of liveness properties. As mentioned in the conclusion, ‘good things’ and ‘bad things’ are not well-defined concepts, the topological definition given in the paper indeed gives correct intuition about liveness properties. Though it might be unnecessary, when temporal logic been mentioned the first time, it should be given some explanations.

In general, this paper clearly states the definition the liveness properties and explains in an understandble way.