Document Open Access Logo

An Introduction to First-Order Linear Temporal Logic (Invited Talk)

Author Nicola Gigante

PDF

File

Thumbnail PDF
PDF
LIPIcs.TIME.2025.2.pdf
  • Filesize: 0.56 MB
  • 6 pages

Document Identifiers

Subject Classification

ACM Subject Classification
  • Theory of computation → Modal and temporal logics
Keywords
  • Temporal logic
  • first-order logic
  • knowledge-representation
  • infinite-state systems

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

Abstract

Linear temporal logic (LTL), most commonly defined as a propositional modal logic, is the de-facto standard language for specifying temporal properties of systems in formal verification, artificial intelligence, and other fields. First-order linear temporal logic (FOLTL) lifts LTL to the setting of first-order logic, obtaining a remarkably flexible and expressive formalism. First-order modal and temporal logics have a long history, but recent years have seen a rise of interest in (well-behaved fragments of) FOLTL for the specification of complex infinite-state systems. This tutorial is a gentle introduction to the field of first-order temporal logics, starting from classic results and exploring recent directions.

Cite As Get BibTex

Nicola Gigante. An Introduction to First-Order Linear Temporal Logic (Invited Talk). In 32nd International Symposium on Temporal Representation and Reasoning (TIME 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 355, pp. 2:1-2:6, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025) https://doi.org/10.4230/LIPIcs.TIME.2025.2

Author Details

Nicola Gigante
  • Free University of Bozen-Bolzano, Italy

References

  1. Alessandro Artale and Enrico Franconi. Temporal description logics. In Michael Fisher, Dov M. Gabbay, and Lluís Vila, editors, Handbook of Temporal Reasoning in Artificial Intelligence, volume 1 of Foundations of Artificial Intelligence, pages 375-388. Elsevier, 2005. URL: https://doi.org/10.1016/S1574-6526(05)80014-8.
  2. Clark W. Barrett, Roberto Sebastiani, Sanjit A. Seshia, and Cesare Tinelli. Satisfiability modulo theories. In Armin Biere, Marijn Heule, Hans van Maaren, and Toby Walsh, editors, Handbook of Satisfiability, volume 185 of Frontiers in Artificial Intelligence and Applications, pages 825-885. IOS Press, 2009. URL: https://doi.org/10.3233/978-1-58603-929-5-825.
  3. Giuseppe De Giacomo and Moshe Y. Vardi. Linear temporal logic and linear dynamic logic on finite traces. In Proceedings of 23rd IJCAI, pages 854-860, 2013. URL: http://www.aaai.org/ocs/index.php/IJCAI/IJCAI13/paper/view/6997.
  4. Giuseppe De Giacomo and Moshe Y. Vardi. Synthesis for LTL and LDL on finite traces. In Qiang Yang and Michael J. Wooldridge, editors, Proceedings of the Twenty-Fourth International Joint Conference on Artificial Intelligence, IJCAI 2015, Buenos Aires, Argentina, July 25-31, 2015, pages 1558-1564. AAAI Press, 2015. URL: http://ijcai.org/Abstract/15/223.
  5. D.M. Gabbay, A. Kurucz, F. Wolter, and M. Zakharyaschev. Fragments of first-order temporal logics. In Many-Dimensional Modal Logics, volume 148 of Studies in Logic and the Foundations of Mathematics, pages 465-545. Elsevier, 2003. URL: https://doi.org/10.1016/S0049-237X(03)80012-5.
  6. Luca Geatti, Alessandro Gianola, and Nicola Gigante. Linear temporal logic modulo theories over finite traces. In Proceedings of the 31st IJCAI, pages 2641-2647, 2022. URL: https://doi.org/10.24963/ijcai.2022/366.
  7. Luca Geatti, Alessandro Gianola, and Nicola Gigante. First-order automata. In Toby Walsh, Julie Shah, and Zico Kolter, editors, AAAI-25, Sponsored by the Association for the Advancement of Artificial Intelligence, February 25 - March 4, 2025, Philadelphia, PA, USA, pages 14940-14948. AAAI Press, 2025. URL: https://doi.org/10.1609/AAAI.V39I14.33638.
  8. Luca Geatti, Alessandro Gianola, Nicola Gigante, and Sarah Winkler. Decidable fragments of ltl_f modulo theories. In Proceedings of the 26th ECAI, volume 372 of Frontiers in Artificial Intelligence and Applications, pages 811-818. IOS Press, 2023. URL: https://doi.org/10.3233/FAIA230348.
  9. Luca Geatti, Nicola Gigante, Angelo Montanari, and Gabriele Venturato. SAT meets tableaux for linear temporal logic satisfiability. J. Autom. Reason., 68(2):6, 2024. URL: https://doi.org/10.1007/S10817-023-09691-1.
  10. Erich Grädel, Phokion G. Kolaitis, and Moshe Y. Vardi. On the decision problem for two-variable first-order logic. Bull. Symb. Log., 3(1):53-69, 1997. URL: https://doi.org/10.2307/421196.
  11. Arie Gurfinkel and Nikolaj S. Bjørner. The science, art, and magic of constrained horn clauses. In Proceedings of the 21st International Symposium on Symbolic and Numeric Algorithms for Scientific Computing, pages 6-10. IEEE, 2019. URL: https://doi.org/10.1109/SYNASC49474.2019.00010.
  12. Jianwen Li, Yinbo Yao, Geguang Pu, Lijun Zhang, and Jifeng He. Aalta: an LTL satisfiability checker over infinite/finite traces. In Shing-Chi Cheung, Alessandro Orso, and Margaret-Anne D. Storey, editors, Proc. of the 22nd ACM SIGSOFT International Symposium on Foundations of Software Engineering, pages 731-734. ACM, 2014. URL: https://doi.org/10.1145/2635868.2661669.
  13. Carsten Lutz, Frank Wolter, and Michael Zakharyaschev. Temporal description logics: A survey. In Stéphane Demri and Christian S. Jensen, editors, 15th International Symposium on Temporal Representation and Reasoning, TIME 2008, Université du Québec à Montréal, Canada, 16-18 June 2008, pages 3-14. IEEE Computer Society, 2008. URL: https://doi.org/10.1109/TIME.2008.14.
  14. Robert P. McArthur. Tense Logic. Springer, 1976. URL: https://doi.org/10.1007/978-94-017-3219-2.
  15. Kenneth L. McMillan. Interpolation and model checking. In Edmund M. Clarke, Thomas A. Henzinger, Helmut Veith, and Roderick Bloem, editors, Handbook of Model Checking, pages 421-446. Springer, 2018. URL: https://doi.org/10.1007/978-3-319-10575-8_14.
  16. Amir Pnueli. The temporal logic of programs. In 18th Annual Symposium on Foundations of Computer Science, pages 46-57. IEEE Computer Society, 1977. URL: https://doi.org/10.1109/SFCS.1977.32.
  17. Amir Pnueli and Roni Rosner. On the synthesis of an asynchronous reactive module. In 16th International Colloquium on Automata, Languages and Programming, volume 372 of Lecture Notes in Computer Science, pages 652-671. Springer, 1989. URL: https://doi.org/10.1007/BFB0035790.
  18. Mark Reynolds. A New Rule for LTL Tableaux. In Proc. of the 7th International Symposium on Games, Automata, Logics and Formal Verification, volume 226 of EPTCS, pages 287-301, 2016. URL: https://doi.org/10.4204/EPTCS.226.20.
  19. Andoni Rodriguez, Felipe Gorostiaga, and Cesar Sanchez. Counter example guided reactive synthesis for ltl modulo theories. In Proceedings of the 37th International Conference on Computer Aided Verification (CAV 2025), page to appear, 2025. Google Scholar
  20. Andoni Rodríguez and César Sánchez. Boolean abstractions for realizability modulo theories. In Proceedings of the 35th CAV, volume 13966 of Lecture Notes in Computer Science, pages 305-328. Springer, 2023. URL: https://doi.org/10.1007/978-3-031-37709-9_15.
  21. A. Prasad Sistla and Edmund M. Clarke. The complexity of propositional linear temporal logics. J. ACM, 32(3):733-749, 1985. URL: https://doi.org/10.1145/3828.3837.
  22. M. Suda and C. Weidenbach. A PLTL-Prover Based on Labelled Superposition with Partial Model Guidance. In Proc. of the 6th International Joint Conference on Automated Reasoning, volume 7364 of LNCS, pages 537-543. Springer, 2012. URL: https://doi.org/10.1007/978-3-642-31365-3_42.
  23. Peter van Emde Boas et al. The convenience of tilings. Lecture Notes in Pure and Applied Mathematics, pages 331-363, 1997. Google Scholar
Any Issues?
X

Feedback on the Current Page

CAPTCHA

Thanks for your feedback!

Feedback submitted to Dagstuhl Publishing

Could not send message

Please try again later or send an E-mail
© 2023-2025 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact