Paper Info
Title
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) [IL 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.
Year
DOI
Venue
2022
10.1007/978-3-030-99253-8_13
FOUNDATIONS OF SOFTWARE SCIENCE AND COMPUTATION STRUCTURES (FOSSACS 2022)
DocType
Volume
ISSN
Conference
13242
0302-9743
Citations 
PageRank 
References 
0
0.34
0
Authors
5
Name
Order
Citations
PageRank
Alessandro Cimatti15064323.15
Luca Geatti200.34
Nicola Gigante300.34
Angelo Montanari41535135.04
Stefano Tonetta501.69