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

DOI10.46298/LMCS-19(3:13)2023MaRDI QIDQ6135783zbMATH OpenOpenAlexFDO

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

Publication date 26 August 2023

Published in Logical Methods in Computer Science (Search for Journal in Brave)

Copyright license Creative Commons Attribution 4.0 International

Full work available at URL https://arxiv.org/abs/2209.02307

zbMATH Keywords

first-order logicLTLsafety fragment

Mathematics Subject Classification ID

Logic in computer science (03B70) Computer science (68-XX)

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.

Cites work

• scientific article; zbMATH DE number 4153903 (Why is no real title available?)
• scientific article; zbMATH DE number 3940713 (Why is no real title available?)
• scientific article; zbMATH DE number 44695 (Why is no real title available?)
• scientific article; zbMATH DE number 139631 (Why is no real title available?)
• scientific article; zbMATH DE number 2102708 (Why is no real title available?)
• scientific article; zbMATH DE number 3368555 (Why is no real title available?)
• A Proof of Kamp's theorem
• A first-order logic characterization of safety and co-safety languages
• Characterization of temporal property classes
• Counter-free automata, first-order logic, and star-free expressions extended by prefix oracles
• Is the Interesting Part of Process Logic uninteresting?: A Translation from PL to PDL
• Model checking of safety properties
• Safety, liveness and fairness in temporal logic
• Star-free regular sets of ω-sequences

Cited in

(4)

• A first-order logic characterization of safety and co-safety languages
• Towards the exact complexity of realizability for safety LTL
• First-order temporal logic on finite traces: semantic properties, decidable fragments, and applications
• Towards an efficient implementation of a tableau method for reactive safety specifications

This page was built for publication: A first-order logic characterization of safety and co-safety languages

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6135783)