Abstract
Linear Temporal Logic (\(\mathsf {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 \(\mathsf {LTL}\) and the first-order theory of one successor (\(\mathsf {S1S}[\mathsf {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 \(\mathsf {LTL}\). \(\mathsf {Safety\text {-} \mathsf {LTL}}\) (resp., \(\mathsf {coSafety\text {-} \mathsf {LTL}}\)) is a fragment of \(\mathsf {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 \(\mathsf {S1S}[\mathsf {FO}]\), called \(\mathsf {Safety\text {-} FO}\), and its dual \(\mathsf {coSafety\text {-} FO}\), which are expressively complete with regards to the \(\mathsf {LTL}\)-definable safety languages. In particular, we prove that they respectively characterise exactly \(\mathsf {Safety\text {-} \mathsf {LTL}}\) and \(\mathsf {coSafety\text {-} \mathsf {LTL}}\), a result that joins Kamp’s theorem, and provides a clearer view of the charactisations of (fragments of) \(\mathsf {LTL}\) in terms of first-order languages. In addition, it gives a direct, compact, and self-contained proof that any safety language definable in \(\mathsf {LTL}\) is definable in \(\mathsf {Safety\text {-} \mathsf {LTL}}\) as well. As a by-product, we obtain some interesting results on the expressive power of the weak tomorrow operator of \(\mathsf {Safety\text {-} \mathsf {LTL}}\) interpreted over finite and infinite traces.
Chapter PDF
Similar content being viewed by others
References
Biere, A., Artho, C., Schuppan, V.: Liveness checking as safety checking. Electronic Notes in Theoretical Computer Science 66(2), 160–177 (2002)
Buchi, J.R.: Weak second-order arithmetic and finite automata. Journal of Symbolic Logic 28(1) (1963)
Büchi, J.R.: On a decision method in restricted second order arithmetic. In: The collected works of J. Richard Büchi, pp. 425–435. Springer (1990)
Cerná, I., Pelánek, R.: Relating hierarchy of temporal properties to model checking. In: Rovan, B., Vojtás, P. (eds.) Proceedings of the 28th International Symposium on Mathematical Foundations of Computer Science 2003. Lecture Notes in Computer Science, vol. 2747, pp. 318–327. Springer (2003). https://doi.org/10.1007/978-3-540-45138-9_26
Chang, E.Y., Manna, Z., Pnueli, A.: Characterization of temporal property classes. In: Kuich, W. (ed.) Proceedings of the 19th International Colloquium on Automata, Languages and Programming. Lecture Notes in Computer Science, vol. 623, pp. 474–486. Springer (1992). https://doi.org/10.1007/3-540-55719-9_97
De Giacomo, G., Vardi, M.Y.: Linear temporal logic and linear dynamic logic on finite traces. In: Rossi, F. (ed.) Proceedings of the 23rd International Joint Conference on Artificial Intelligence. pp. 854–860. IJCAI/AAAI (2013)
De Giacomo, G., Vardi, M.Y.: Synthesis for LTL and LDL on finite traces. In: Yang, Q., Wooldridge, M.J. (eds.) Proceedings of the Twenty-Fourth International Joint Conference on Artificial Intelligence. pp. 1558–1564. AAAI Press (2015)
Gabbay, D., Pnueli, A., Shelah, S., Stavi, J.: On the temporal analysis of fairness. In: Proceedings of the 7th ACM SIGPLAN-SIGACT symposium on Principles of programming languages. pp. 163–173 (1980)
Giacomo, G.D., Masellis, R.D., Montali, M.: Reasoning on LTL on finite traces: Insensitivity to infiniteness. In: Brodley, C.E., Stone, P. (eds.) Proceedings of the Twenty-Eighth AAAI Conference on Artificial Intelligence. pp. 1027–1033. AAAI Press (2014)
Kamp, J.A.W.: Tense logic and the theory of linear order. University of California, Los Angeles (1968)
Kupferman, O., Vardi, M.Y.: Model checking of safety properties. Formal Methods in System Design 19(3), 291–314 (2001)
Lichtenstein, O., Pnueli, A., Zuck, L.: The glory of the past. In: Workshop on Logic of Programs. pp. 196–218. Springer (1985)
McNaughton, R., Papert, S.A.: Counter-Free Automata (MIT research monograph no. 65). The MIT Press (1971)
Pnueli, A.: The temporal logic of programs. In: 18th Annual Symposium on Foundations of Computer Science (sfcs 1977). pp. 46–57. IEEE (1977)
Rabinovich, A.: A Proof of Kamp’s theorem. Logical Methods in Computer Science Volume 10, Issue 1 (Feb 2014). https://doi.org/10.2168/LMCS-10(1:14)2014, https://lmcs.episciences.org/730
Sherman, R., Pnueli, A., Harel, D.: Is the interesting part of process logic uninteresting? A translation from PL to PDL. SIAM J. Comput. 13(4), 825–839 (1984). https://doi.org/10.1137/0213051
Sistla, A.P.: Safety, liveness and fairness in temporal logic. Formal Aspects of Computing 6(5), 495–511 (1994)
Strejcek, J.: Linear temporal logic: Expressiveness and model checking. Ph.D. thesis, Faculty of Informatics, Masaryk University in Brno (2004)
Thomas, W.: Safety-and liveness-properties in propositional temporal logic: characterizations and decidability. Banach Center Publications 1(21), 403–417 (1988)
Zhu, S., Tabajara, L.M., Li, J., Pu, G., Vardi, M.Y.: A Symbolic Approach to Safety LTL Synthesis. In: Strichman, O., Tzoref-Brill, R. (eds.) Proceedings of the 13th International Haifa Verification Conference. Lecture Notes in Computer Science, vol. 10629, pp. 147–162. Springer (2017). https://doi.org/10.1007/978-3-319-70389-3_10
Zuck, L.: Past temporal logic. Weizmann Institute of Science 67 (1986)
Author information
Authors and Affiliations
Corresponding authors
Editor information
Editors and Affiliations
Rights and permissions
Open Access This chapter is licensed under the terms of the Creative Commons Attribution 4.0 International License (http://creativecommons.org/licenses/by/4.0/), which permits use, sharing, adaptation, distribution and reproduction in any medium or format, as long as you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons license and indicate if changes were made.
The images or other third party material in this chapter are included in the chapter's Creative Commons license, unless indicated otherwise in a credit line to the material. If material is not included in the chapter's Creative Commons license and your intended use is not permitted by statutory regulation or exceeds the permitted use, you will need to obtain permission directly from the copyright holder.
Copyright information
© 2022 The Author(s)
About this paper
Cite this paper
Cimatti, A., Geatti, L., Gigante, N., Montanari, A., Tonetta, S. (2022). A first-order logic characterisation of safety and co-safety languages. In: Bouyer, P., Schröder, L. (eds) Foundations of Software Science and Computation Structures. FoSSaCS 2022. Lecture Notes in Computer Science, vol 13242. Springer, Cham. https://doi.org/10.1007/978-3-030-99253-8_13
Download citation
DOI: https://doi.org/10.1007/978-3-030-99253-8_13
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-030-99252-1
Online ISBN: 978-3-030-99253-8
eBook Packages: Computer ScienceComputer Science (R0)