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

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. Its widespread use is also due to its strong foundational properties. One of them is Kamp’s theorem, showing that LTL and the first-order theory of one successor (S1S[ FO] ) are expressively equivalent. Safety and co-safety languages, where a finite prefix suffices to establish whether a word does not or does belong to the language, respectively, play a crucial role in lowering the complexity of problems like model checking and reactive synthesis for LTL. Safety- LTL (resp., coSafety- LTL ) is a fragment of LTL where only universal (resp., existential) temporal modalities are allowed, that recognises safety (resp., co-safety) languages only. In this paper, we introduce a fragment of S1S[ FO], called Safety- FO, and its dual coSafety- FO, which are expressively complete with regards to the LTL -definable safety languages. In particular, we prove that they respectively characterise exactly Safety- LTL and coSafety- LTL, a result that joins Kamp’s theorem, and provides a clearer view of the charactisations 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 Safety- LTL as well. As a by-product, we obtain some interesting results on the expressive power of the weak tomorrow operator of Safety- LTL interpreted over finite and infinite traces.