Complexity of Safety and coSafety Fragments of Linear Temporal Logic

Summary

This partial ingest is based on the extracted full PDF text. Artale et al. give a systematic complexity map for safety and co-safety fragments of LTL over infinite and finite traces. They study satisfiability, validity, and realizability for syntactic fragments such as Safety-LTL, coSafety-LTL, G(pLTL), F(pLTL), and bounded-future/past variants, showing that expressively equivalent fragments can have different realizability complexity.

Key Claims

• Most safety and co-safety fragments retain PSPACE-complete satisfiability and validity over infinite traces, matching full LTL.
• For co-safety fragments, the main complexity results transfer from infinite to finite traces.
• For safety fragments over finite traces, satisfiability drops to NP-complete and realizability drops to Pi^P_2-complete.
• Realizability is more sensitive to syntax than satisfiability: expressively equivalent fragments can range from 2EXPTIME-complete to EXPTIME-complete.
• Past-modal or bounded-fragment formulations can be computationally better behaved for realizability than more general safety/co-safety syntax.

Methods / Formalism

• The paper treats LTL with future and past operators and compares fragments including Safety-LTL, coSafety-LTL, G(pLTL), F(pLTL), LTL[X,F], and LTL[X~,G].
• Safety and co-safety languages are defined by finite prefixes: co-safety membership can be confirmed by a finite good prefix, and safety is the complement notion.
• Proposition 1 links semantic safety/co-safety languages to syntactic fragments such as Safety-LTL/coSafety-LTL and G(pLTL)/F(pLTL).
• The main results distinguish satisfiability/validity from realizability and infinite-trace semantics from finite-trace semantics.
• Safety LTL Automata and Games records the finite-prefix and complexity anchors used by this batch.

Evidence / Experiments

• The paper is theoretical. It proves upper and lower bounds for the selected fragments and summarizes them in tables for safety and co-safety.
• Key proof devices include suffix independence for co-safety-style fragments, a bounded model property for safety languages of finite words, and reductions from known LTL and finite-trace realizability problems.
• The paper uses duality between safety/co-safety and between controller/environment strategies to transfer some realizability results.

Connections

• Sharpens Safety and Co-Safety Properties by showing that “finite-prefix” structure does not automatically imply low complexity.
• Provides the complexity backdrop for Zhu2020 - A Symbolic Approach to Safety LTL Synthesis, whose algorithmic gains depend on a restricted Safety LTL synthesis setting.
• Connects Linear Temporal Logic to EXPTIME and 2EXPTIME-style synthesis bounds.
• Helps route finite-trace specification work in Temporal Logic, especially where LTLf, G(pLTL), or F(pLTL) are options.

Open Questions

• Which safety/co-safety fragment should be recommended for future wiki notes on runtime monitoring, synthesis, and reward-machine objectives?
• Should the wiki add dedicated pages for PSPACE and 2EXPTIME if more temporal-logic complexity notes accumulate?
• Which safe-RL or shielding papers silently rely on a fragment whose realizability complexity differs from its semantic expressiveness?

Citation

Artale, Alessandro, Luca Geatti, Nicola Gigante, Andrea Mazzullo, and Angelo Montanari. 2023. “Complexity of Safety and coSafety Fragments of Linear Temporal Logic.” In Proceedings of the Thirty-Seventh AAAI Conference on Artificial Intelligence.