Many temporal logics include weak and strong versions of operators: a strong one guarantees that a property eventually holds while a weak one does not. This paper characterizes which operators form a weak/strong pair, making precise the folklore knowledge that formulas containing only weak operators are easier to model check than formulas including strong operators. As an important application, operators in the Institute of Electrical and Electronics Engineers (IEEE) standard temporal logics property specification language (PSL) and SystemVerilog assertions (SVA) that are intuitively expected to form a weak/strong pair are shown in fact not to be related in such a way.

Topology is generally important in semantics, and especially the Cantor space often plays a universal role (see, for example, domain theory). For example, any compact metric space is a quotient of Cantor space. The characterization of weak/strong operators is topological in nature. The main result is that the words satisfying a weak formula form an open set in Cantor space, so taking interiors gives a weak version of an operator. Closed sets similarly correspond to strong formulas.

The historical starting point is a 1985 paper by Alpern and Schneider [1], who consider safety properties (“something bad doesn’t happen”) and liveness properties (“something good eventually happens”), and show that any property decomposes into safety and liveness components whose intersection is the original formula. Intuitively, one might expect that safety properties correspond to weak formulas and liveness properties to strong formulas. However, this is not exactly true, and the comparison only works up to pathologies. As an application, the authors strengthen Kupferman and Vardi’s 1999 work [2] by showing that semantically weak formulas are precisely the non-pathological safety properties.