A Symbolic Approach to Safety LTL Synthesis

Summary

This partial ingest is based on the extracted full PDF text. Zhu et al. study Reactive Synthesis for a syntactic Safety LTL fragment: formulas in negation normal form without Until. The paper reduces Safety LTL synthesis to Safety Games, gives an explicit Horn-SAT reduction, and gives a symbolic BDD/MONA-based construction that builds automata for bad prefixes and solves the resulting game by a greatest-fixpoint computation.

Key Claims

• General LTL synthesis remains difficult in practice because classical pipelines translate specifications to deterministic parity automata and solve parity games.
• Safety LTL admits a simpler synthesis path because every violation has a finite bad prefix.
• A deterministic finite automaton for bad prefixes can be used as the dual of a deterministic safety automaton for the safety game.
• The explicit safety-game approach can be encoded as Horn-SAT, solvable in linear time in the explicit game graph.
• The symbolic approach, implemented as SSyft, performs best overall in the paper’s experiments against general LTL-synthesis tools such as Acacia+ and Unbeast.

Methods / Formalism

• The paper defines safe and co-safe formulas through bad and good prefixes, with phi safe iff not phi is co-safe.
• Safety LTL is taken to be the Until-free fragment of LTL in negation normal form; Co-Safety LTL is the dual Release-free fragment.
• Safety synthesis is formulated over input variables X, output variables Y, and a strategy

$$g:(2^X{)}^{\ast }\to 2^Y$$

that must satisfy the specification for every environment input sequence.

• For a deterministic safety automaton, winning states are computed by the greatest fixed point

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

where Pre(E) keeps states from which the controller can force the next state into E for every environment move.

• Safety LTL Automata and Games records the bad-prefix automaton, Horn-SAT, and symbolic fixed-point setup.

Evidence / Experiments

• The authors compare the explicit Horn-SAT approach and SSyft against Acacia+ and Unbeast on Safety LTL synthesis instances.
• The explicit approach is competitive on smaller formulas but can suffer when the explicit game graph grows.
• The symbolic approach benefits from BDD-style state-set manipulation and an early unrealizability check when the initial state drops out of the current winning approximation.
• SSyft solves more instances overall in the reported one-minute comparisons, especially on unrealizable cases.

Connections

• Builds directly on the finite bad-prefix perspective in Latvala2002 - Efficient Model Checking of Safety Properties and related safety-property model checking.
• Complements Artale2023 - Complexity of Safety and coSafety Fragments of Linear Temporal Logic, which clarifies the worst-case complexity landscape of these fragments.
• Gives general Safety Games machinery that also underlies Shield Synthesis and LTL-based Shielding.
• Connects to Hausmann2024 - Symbolic Solution of Emerson-Lei Games for Reactive Synthesis through symbolic synthesis fragments that separate safety structure from richer winning conditions.

Open Questions

• How often do practical robotics, shielding, or controller specifications land in the paper’s syntactic Safety LTL fragment rather than requiring liveness or richer assumptions?
• How should symbolic Safety LTL synthesis be combined with compositional shield synthesis when the environment model is factored?
• Can bad-prefix automata generated for synthesis also provide useful explanations for runtime intervention?

Citation

Zhu, Shufang, Lucas M. Tabajara, Jianwen Li, Geguang Pu, and Moshe Y. Vardi. 2020. “A Symbolic Approach to Safety LTL Synthesis.” arXiv:1709.07495.