LIPIcs.TIME.2023.21.pdf
- Filesize: 432 kB
- 3 pages
Document
Torwards Infinite-State Verification and Planning with Linear Temporal Logic Modulo Theories (Extended Abstract)
Authors
-
Part of:
Volume:
30th International Symposium on Temporal Representation and Reasoning (TIME 2023)
Series: Leibniz International Proceedings in Informatics (LIPIcs)
Conference: International Symposium on Temporal Representation and Reasoning (TIME) - License:
Creative Commons Attribution 4.0 International license
- Publication Date: 2023-09-18
Cite AsGet BibTex
Luca Geatti, Alessandro Gianola, and Nicola Gigante. Torwards Infinite-State Verification and Planning with Linear Temporal Logic Modulo Theories (Extended Abstract). In 30th International Symposium on Temporal Representation and Reasoning (TIME 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 278, pp. 21:1-21:3, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
https://doi.org/10.4230/LIPIcs.TIME.2023.21
https://doi.org/10.4230/LIPIcs.TIME.2023.21
Abstract
In this extended abstract, we discuss about Linear Temporal Logic Modulo Theories over finite traces (LTL_f^MT), a temporal logic that we recently introduced with the goal of providing an equilibrium between generality of the formalism and decidability of the logic. After recalling its distinguishing features, we discuss some future applications.
Subject Classification
ACM Subject Classification
- Theory of computation → Logic and verification
Keywords
- Linear Temporal Logic
- Satisfiability Modulo Theories
Metrics
- Access Statistics
-
Total Accesses (updated on a weekly basis)
0PDF Downloads
References
- 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.
- Diego Calvanese, Silvio Ghilardi, Alessandro Gianola, Marco Montali, and Andrey Rivkin. SMT-based verification of data-aware processes: a model-theoretic approach. Math. Struct. Comput. Sci., 30(3):271-313, 2020. URL: https://doi.org/10.1017/S0960129520000067.
- Alessandro Cimatti, Alberto Griggio, Enrico Magnago, Marco Roveri, and Stefano Tonetta. Smt-based satisfiability of first-order LTL with event freezing functions and metric operators. Inf. Comput., 272:104502, 2020. URL: https://doi.org/10.1016/j.ic.2019.104502.
-
Giuseppe De Giacomo and Moshe Y. Vardi. Linear temporal logic and linear dynamic logic on finite traces. In Francesca Rossi, editor, Proceedings of the 23rd International Joint Conference on Artificial Intelligence, pages 854-860. IJCAI/AAAI, 2013.
-
Alin Deutsch, Yuliang Li, and Victor Vianu. Verification of hierarchical artifact systems. ACM Trans. Database Syst., 44(3):12:1-12:68, 2019.
- Luca Geatti, Alessandro Gianola, and Nicola Gigante. Linear temporal logic modulo theories over finite traces. In Proceedings of the Thirty-First International Joint Conference on Artificial Intelligence, pages 2641-2647. ijcai.org, 2022. URL: https://doi.org/10.24963/ijcai.2022/366.
- Luca Geatti, Nicola Gigante, and Angelo Montanari. A sat-based encoding of the one-pass and tree-shaped tableau system for LTL. In Proceedings of the 28th International Conference on Automated Reasoning with Analytic Tableaux and Related Methods, volume 11714 of Lecture Notes in Computer Science, pages 3-20. Springer, 2019. URL: https://doi.org/10.1007/978-3-030-29026-9_1.
-
Luca Geatti, Nicola Gigante, and Angelo Montanari. BLACK: A fast, flexible and reliable LTL satisfiability checker. In Proceedings of the 3rd Workshop on Artificial Intelligence and Formal Verification, Logic, Automata, and Synthesis, volume 2987 of CEUR, pages 7-12, 2021.
- Roman Kontchakov, Carsten Lutz, Frank Wolter, and Michael Zakharyaschev. Temporalising tableaux. Stud Logica, 76(1):91-134, 2004. URL: https://doi.org/10.1023/B:STUD.0000027468.28935.6d.
- Marta Cialdea Mayer, Carla Limongelli, Andrea Orlandini, and Valentina Poggioni. Linear temporal logic as an executable semantics for planning languages. Journal of Logic, Language and Information, 16(1):63-89, 2007. URL: https://doi.org/10.1007/s10849-006-9022-1.
- A. Pnueli. The Temporal Logic of Programs. In Proc. of the 18th Annual Symposium on Foundations of Computer Science, pages 46-57. IEEE Computer Society, 1977. URL: https://doi.org/10.1109/SFCS.1977.32.