Safety LTL Automata and Games

Context

This annex collects the reusable formal payload behind the May 2026 safety/co-safety LTL batch: finite bad/good prefixes, finite automata for safety checking, safety-game synthesis, and complexity boundaries for safety/co-safety fragments.

Formal Statement

For L subseteq Sigma^omega, a bad prefix is a finite word x such that all infinite extensions violate L:

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

A good prefix is a finite word x such that all infinite extensions satisfy L:

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

Safety languages are those where every violating word has a bad prefix. Co-safety languages are those where every satisfying word has a good prefix. For LTL, phi is safe iff not phi is co-safe, and bad prefixes for phi are good prefixes for not phi.

For Safety LTL synthesis, a deterministic safety automaton induces a safety game. With environment variables X, controller variables Y, and transition function delta, the controllable predecessor of a set E is

$$Pre(E)=\{s\mid \forall X\in 2^X.\exists Y\in 2^Y.\delta (s,X\cup Y)\in E\}.$$

The winning region is the greatest fixed point:

$$W_0=S,W_{i+1}=W_i\cap Pre(W_i).$$

Derivation / Construction

• Latvala constructs finite automata for informative bad prefixes of LTL safety formulas and checks whether a formula is pathological.
• Zhu et al. define a syntactic Safety LTL fragment as negation-normal formulas without Until, then build bad-prefix automata for the negated co-safe formula.
• The explicit Zhu et al. pipeline encodes safety-game realizability as Horn-SAT over state, state-input, and state-input-output variables.
• The symbolic Zhu et al. pipeline constructs a DFA for bad prefixes through finite-trace logic/MONA, removes accepting bad-prefix states to obtain a safety automaton, and computes the winning region symbolically.
• Artale et al. show that finite-prefix structure changes complexity unevenly: many satisfiability/validity problems remain PSPACE-complete, while some finite-trace safety problems drop to NP or Pi^P_2, and realizability can vary from EXPTIME to 2EXPTIME across expressively related fragments.

Implications

Safety/co-safety structure is algorithmically useful but not a magic tractability guarantee. It helps most when the workflow can exploit finite bad/good prefixes directly, as in runtime monitoring, model checking, and safety-game synthesis. The exact syntax of the fragment still matters for realizability complexity and for whether symbolic constructions avoid heavyweight omega-automata.

Links

• Safety and Co-Safety Properties
• Safety Games
• Reactive Synthesis
• 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