Definition. Safety closure [ltp-000J]

(from Defining Liveness)

Given a property $P \subseteq \Sigma ^\omega$ , the safety closure of $P$ , written $\overline {P}$ , is the smallest superset of $P$ which is a safety property. It is the dual of the guarantee kernel, so $\underline {P^\complement } = \overline {P}^\complement$ . This means that the safety closure of $P$ contains all behaviours which cannot be shown to violate $P$ by a finite bad prefix.

It follows that $P$ is a safety property iff $\overline {P} = P$ .

This is a closure operator, so it is extensive ( $\overline {P} \supseteq P$ ), idempotent ( $\overline {\overline {P}} = \overline {P}$ ), and monotonic ( $P \subseteq R$ implies $\overline {P} \subseteq \overline {R}$ ).

Topologically speaking, the safety closure is the (limit-)closure.

Intuitively, the safety closure of $P$ is all behaviours for which any finite prefix extended in some way will get into $P$ .