The Safety-Progress Classification

We propose a classification of temporal properties into a hierarchy, called the safety-progress classification. The classes of the hierarchy are characterized through four views: a language-theoretic view, a topological view, a temporal logic view, and an automata view. In the topological view, the considered hierarchy coincides with the two lower levels of the Borel hierarchy, starting with the closed and open sets. For properties that are expressible by temporal logic and automata, we provide syntactic characterizations of the formulas and automata that correspond to properties in the different classes. We relate this classification to the well-known safety-liveness classification, and show that in some sense the two are orthogonal to one another.