Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

A first-order logic characterization of safety and co-safety languages

Alessandro Cimatti, Luca Geatti, Nicola Gigante, Angelo Montanari, Stefano Tonetta

TL;DR

The paper establishes a first-order characterization of safety and co-safety languages by introducing two forward-looking FO fragments, $SafetyFO$ and $coSafetyFO$, and proves they are expressively complete for the $LTL$-definable safety and co-safety languages, respectively, via Kamp-style correspondences with $SafetyLTL$ and $coSafetyLTL$. It provides a compact, self-contained proof that $SafetyFO$ captures all $-$definable safety languages and analyzes the dual fragment for co-safety, including the nuanced role of the weak tomorrow operator. The finite-word analysis shows that forbidding certain operators yields equivalent safety/co-safety fragments over finite words, and the work connects to succinct translations, practical reactive synthesis implications, and alternative FO characterizations such as Thomas’s bounded fragments. The results unify temporal and first-order viewpoints, extend Kamp’s theorem to ($co$-)safety, and illuminate the expressive power of different logics and automata in capturing safety and co-safety properties, with directions for future improvements in translation efficiency and finite-word generalization.

Abstract

Linear Temporal Logic (LTL) is one of the most popular temporal logics, that comes into play in a variety of branches of computer science. Among the various reasons of its widespread use there are its strong foundational properties: LTL is equivalent to counter-free omega-automata, to star-free omega-regular expressions, and (by Kamp's theorem) to the First-Order Theory of Linear Orders (FO-TLO). Safety and co-safety languages, where a finite prefix suffices to establish whether a word does not belong or belongs to the language, respectively, play a crucial role in lowering the complexity of problems like model checking and reactive synthesis for LTL. SafetyLTL (resp., coSafetyLTL) is a fragment of LTL where only universal (resp., existential) temporal modalities are allowed, that recognises safety (resp., co-safety) languages only. The main contribution of this paper is the introduction of a fragment of FO-TLO, called SafetyFO, and of its dual coSafetyFO, which are expressively complete with respect to the LTL-definable safety and co-safety languages. We prove that they exactly characterize SafetyLTL and coSafetyLTL, respectively, a result that joins Kamp's theorem, and provides a clearer view of the characterization of (fragments of) LTL in terms of first-order languages. In addition, it gives a direct, compact, and self-contained proof that any safety language definable in LTL is definable in SafetyLTL as well. As a by-product, we obtain some interesting results on the expressive power of the weak tomorrow operator of SafetyLTL, interpreted over finite and infinite words. Moreover, we prove that, when interpreted over finite words, SafetyLTL (resp. coSafetyLTL) devoid of the tomorrow (resp., weak tomorrow) operator captures the safety (resp., co-safety) fragment of LTL over finite words.

A first-order logic characterization of safety and co-safety languages

TL;DR

The paper establishes a first-order characterization of safety and co-safety languages by introducing two forward-looking FO fragments, and , and proves they are expressively complete for the -definable safety and co-safety languages, respectively, via Kamp-style correspondences with and . It provides a compact, self-contained proof that captures all definable safety languages and analyzes the dual fragment for co-safety, including the nuanced role of the weak tomorrow operator. The finite-word analysis shows that forbidding certain operators yields equivalent safety/co-safety fragments over finite words, and the work connects to succinct translations, practical reactive synthesis implications, and alternative FO characterizations such as Thomas’s bounded fragments. The results unify temporal and first-order viewpoints, extend Kamp’s theorem to (-)safety, and illuminate the expressive power of different logics and automata in capturing safety and co-safety properties, with directions for future improvements in translation efficiency and finite-word generalization.

Abstract

Linear Temporal Logic (LTL) is one of the most popular temporal logics, that comes into play in a variety of branches of computer science. Among the various reasons of its widespread use there are its strong foundational properties: LTL is equivalent to counter-free omega-automata, to star-free omega-regular expressions, and (by Kamp's theorem) to the First-Order Theory of Linear Orders (FO-TLO). Safety and co-safety languages, where a finite prefix suffices to establish whether a word does not belong or belongs to the language, respectively, play a crucial role in lowering the complexity of problems like model checking and reactive synthesis for LTL. SafetyLTL (resp., coSafetyLTL) is a fragment of LTL where only universal (resp., existential) temporal modalities are allowed, that recognises safety (resp., co-safety) languages only. The main contribution of this paper is the introduction of a fragment of FO-TLO, called SafetyFO, and of its dual coSafetyFO, which are expressively complete with respect to the LTL-definable safety and co-safety languages. We prove that they exactly characterize SafetyLTL and coSafetyLTL, respectively, a result that joins Kamp's theorem, and provides a clearer view of the characterization of (fragments of) LTL in terms of first-order languages. In addition, it gives a direct, compact, and self-contained proof that any safety language definable in LTL is definable in SafetyLTL as well. As a by-product, we obtain some interesting results on the expressive power of the weak tomorrow operator of SafetyLTL, interpreted over finite and infinite words. Moreover, we prove that, when interpreted over finite words, SafetyLTL (resp. coSafetyLTL) devoid of the tomorrow (resp., weak tomorrow) operator captures the safety (resp., co-safety) fragment of LTL over finite words.
Paper Structure (15 sections, 17 equations, 3 figures)

This paper contains 15 sections, 17 equations, 3 figures.

Table of Contents

  1. Introduction
  2. Preliminaries
  3. and
  4. captures -definable safety languages
  5. The (co)safety fragment of over finite words
  6. Comparison with related fragments
  7. Succinctness of with respect to
  8. A practical feedback of
  9. An alternative first-order logic characterization of (co)safety properties
  10. Comparison between and
  11. Other Characterizations of the (co-)safety fragment of
  12. Temporal and first-order logics
  13. Regular and ω-regular expressions
  14. Automata
  15. Conclusions

Figures (3)

  • Figure 1: Summary of the results about languages over infinite words on the left and over finite words on the right. Solid arrows are own results; dashed arrows are known from literature.
  • Figure 2: Different characterizations for the co-safety fragment of over (a) infinite words and (b) finite words.
  • Figure 3: Different characterizations for the safety fragment of over (a) infinite words and (b) finite words.

Theorems & Definitions (17)

  • proof
  • proof
  • proof
  • proof
  • proof
  • proof
  • proof
  • proof
  • proof
  • proof
  • ...and 7 more