LIPIcs.TIME.2022.1.pdf
- Filesize: 344 kB
- 1 pages
Document
Linear Temporal Logic: From Infinite to Finite Horizon (Invited Talk)
Author
Moshe Y. Vardi 
-
Part of:
Volume:
29th International Symposium on Temporal Representation and Reasoning (TIME 2022)
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: 2022-10-29
File
Document Identifiers
Author Details
Cite AsGet BibTex
Moshe Y. Vardi. Linear Temporal Logic: From Infinite to Finite Horizon (Invited Talk). In 29th International Symposium on Temporal Representation and Reasoning (TIME 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 247, p. 1:1, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
https://doi.org/10.4230/LIPIcs.TIME.2022.1
https://doi.org/10.4230/LIPIcs.TIME.2022.1
Abstract
Linear Temporal Logic (LTL), proposed in 1977 by Amir Pnueli for reasoning about ongoing programs, was defined over infinite traces. The motivation for this was the desire to model arbitrarily long computations. While this approach has been highly successful in the context of model checking, it has been less successful in the context of reactive synthesis, due to the chalenging algorithmics of infinite-horizon temporal synthesis. In this talk we show that focusing on finite-horizon temporal synthesis offers enough algorithmic advantages to compensate for the loss in expressiveness. In fact, finite-horizon reasonings is useful even in the context of infinite-horizon applications.
Subject Classification
ACM Subject Classification
- Theory of computation → Modal and temporal logics
Keywords
- Temporal Logic
Metrics
- Access Statistics
-
Total Accesses (updated on a weekly basis)
0PDF Downloads
References
-
G. De Giacomo and M.Y. Vardi. Linear temporal logic and linear dynamic logic on finite traces. In Proc. 23rd Int'l Joint Conf. on Artificial Intelligence, pages 854-860, 2013.
-
G. De Giacomo and M.Y. Vardi. Synthesis for LTL and LDL on finite traces. In Proc. 24th Int'l Joint Conf. on Artificial Intelligence, pages 1558-1564. AAAI Press, 2015.
-
G. De Giacomo and M.Y. Vardi. LTLf and ldlf synthesis under partial observability. In Proc. of the 25th Int'l Joint Conf. on Artificial Intelligence, pages 1044-1050. IJCAI/AAAI Press, 2016.
-
G. De Giacomo, A. Di Stasio, L.M. Tabajara, M.Y. Vardi, and S. Zhu. Finite-trace and generalized-reactivity specifications in temporal synthesis. In Proc. 30th Int'l Joint Conf. on Artificial Intelligence, pages 1852-1858. ijcai.org, 2021.
-
S. Xiao, J. Li, S. Zhu, Y. Shi, G. Pu, and M.Y. Vardi. On-the-fly synthesis for LTL over finite traces. In 35th AAAI Conf. on Artificial Intelligence, pages 6530-6537. AAAI Press, 2021.
-
S. Zhu, L.M. Tabajara, J. Li, G. Pu, and M.Y. Vardi. A symbolic approach to safety LTL synthesis. In Proc.. 13th Int'l Haifa Verification Conf. on Hardware and Software: Verification and Testing, volume 10629 of Lecture Notes in Computer Science, pages 147-162. Springer, 2017.
-
S. Zhu, L.M. Tabajara, J. Li, G. Pu, and M.Y. Vardi. Symbolic LTLf synthesis. In Proc. 26th Int'l Joint Conf. on Artificial Intelligence, pages 1362-1369. ijcai.org, 2017.