Document Open Access Logo

Linear Temporal Logic: From Infinite to Finite Horizon (Invited Talk)

Author Moshe Y. Vardi



PDF
Thumbnail PDF

File

LIPIcs.TIME.2022.1.pdf
  • Filesize: 344 kB
  • 1 pages

Document Identifiers

Author Details

Moshe Y. Vardi
  • Rice University, Houston, TX, USA

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

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)
    0
    PDF Downloads

References

  1. 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. Google Scholar
  2. 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. Google Scholar
  3. 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. Google Scholar
  4. 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. Google Scholar
  5. 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. Google Scholar
  6. 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. Google Scholar
  7. 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. Google Scholar
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail