Safety and Co-Safety Properties

Definition

A safety property is a temporal property whose violations can be witnessed by a finite bad prefix. A co-safety property is the dual notion: satisfactions can be witnessed by a finite good prefix.

Why It Matters

Finite-prefix structure is what makes many monitoring, testing, model-checking, shielding, and synthesis workflows practical. It lets a verifier stop once a violation or satisfaction has become unavoidable, and it permits finite automata or safety games in places where full omega-automata would be heavier.

Formalism / Key Objects

• For a language L subseteq Sigma^omega, a finite word x in Sigma^* is a bad prefix when

$$\forall y\in {\Sigma }^{\omega },xy\notin L.$$

• A finite word x is a good prefix when

$$\forall y\in {\Sigma }^{\omega },xy\in L.$$

• L is safety when every word outside L has a bad prefix.
• L is co-safety when every word inside L has a good prefix.
• In LTL, G p is the canonical safety shape and F p is the canonical co-safety shape.
• Safety LTL Automata and Games records how bad/good prefixes become automata, games, and complexity results.

Connections

• Linear Temporal Logic supplies the usual specification language for the finite-prefix formulas in this wiki.
• Runtime Verification and testing can observe finite bad prefixes directly.
• Reactive Synthesis can reduce Safety LTL to Safety Games rather than full parity games in restricted settings.
• Shielding uses safety specifications to block or correct actions before a finite bad prefix is completed.
• Probabilistic Model Checking uses co-safe LTL as a stopping condition for accumulated reward distributions.

Common Confusions

• “Safety” here is a formal trace-language class, not a general claim that a system is safe in deployment.
• A semantic safety property need not be syntactically obvious in a chosen LTL grammar.
• Co-safety is not the absence of safety; it is the finite-prefix dual for witnessing satisfaction.
• Finite-prefix structure helps algorithms, but it does not by itself make all reasoning problems easy.

Key Sources

• Latvala2002 - Efficient Model Checking of Safety Properties
• Zhu2020 - A Symbolic Approach to Safety LTL Synthesis
• Artale2023 - Complexity of Safety and coSafety Fragments of Linear Temporal Logic