Characterization of temporal property classes

Abstract

This paper presents two novel characterizations of the classes of properties of reactive systems in terms of their expression by temporal logic. The first family of characterizations concerns the safety-progress classification, which describes a hierarchy within the set of temporal properties. Previous characterizations of this hierarchy depended critically on the use of past temporal operators. The characterization presented here identifies the future formulas that belong to each class. This characterization is shown to be complete. The second characterization concerns the safety-liveness classification, which partitions temporal properties into the classes of safety and liveness. While automata-theoretic and temporal logic characterizations of the safety class have been known for some time, a complete characterization of the liveness class by temporal logic remained open. This paper provides such a characterization.