Document Open Access Logo

LTL over Finite Words Can Be Exponentially More Succinct Than Pure-Past LTL, and vice versa

Authors Alessandro Artale , Luca Geatti , Nicola Gigante , Andrea Mazzullo , Angelo Montanari

PDF
Thumbnail PDF

File

LIPIcs.TIME.2023.2.pdf
  • Filesize: 0.74 MB
  • 14 pages

Document Identifiers

Author Details

Alessandro Artale
  • Free University of Bozen-Bolzano, Italy
Luca Geatti
  • University of Udine, Italy
Nicola Gigante
  • Free University of Bozen-Bolzano, Italy
Andrea Mazzullo
  • Free University of Bozen-Bolzano, Italy
Angelo Montanari
  • University of Udine, Italy

Funding

Luca Geatti and Angelo Montanari acknowledge the support from the 2022 Italian INdAM-GNCS project "Elaborazione del Linguaggio Naturale e Logica Temporale per la Formalizzazione di Testi", ref. no. CUP_E55F22000270001. Andrea Mazzullo and Angelo Montanari acknowledge the support of the MUR PNRR project FAIR - Future AI Research (PE00000013) funded by the NextGenerationEU. Nicola Gigante acknowledges the support of the PURPLE project, in the context of the AIPlan4EU project’s First Open Call for Innovators.

Cite As Get BibTex

Alessandro Artale, Luca Geatti, Nicola Gigante, Andrea Mazzullo, and Angelo Montanari. LTL over Finite Words Can Be Exponentially More Succinct Than Pure-Past LTL, and vice versa. In 30th International Symposium on Temporal Representation and Reasoning (TIME 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 278, pp. 2:1-2:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023) https://doi.org/10.4230/LIPIcs.TIME.2023.2

Abstract

Linear Temporal Logic over finite traces (LTL_𝖿) has proved itself to be an important and effective formalism in formal verification as well as in artificial intelligence. Pure past LTL_𝖿 (pLTL) is the logic obtained from LTL_𝖿 by replacing each (future) temporal operator by a corresponding past one, and is naturally interpreted at the end of a finite trace. It is known that each property definable in LTL_𝖿 is also definable in pLTL, and ǐceversa. However, despite being extensively used in practice, to the best of our knowledge, there is no systematic study of their succinctness. 
In this paper, we investigate the succinctness of LTL_𝖿 and pLTL. First, we prove that pLTL can be exponentially more succinct than LTL_𝖿 by showing that there exists a property definable with a pLTL formula of size n such that the size of all LTL_𝖿 formulas defining it is at least exponential in n. Then, we prove that LTL_𝖿 can be exponentially more succinct than pLTL as well. This result shows that, although being expressively equivalent, LTL_𝖿 and pLTL are incomparable when succinctness is concerned. In addition, we study the succinctness of Safety-LTL (the syntactic safety fragment of LTL over infinite traces) with respect to its canonical form G(pLTL), whose formulas are of the form G(α), G being the globally operator and α a pLTL formula. We prove that G(pLTL) can be exponentially more succinct than Safety-LTL, and that the same holds for the dual cosafety fragment.

Subject Classification

ACM Subject Classification
  • Theory of computation → Modal and temporal logics
  • Theory of computation → Logic and verification
Keywords
  • Temporal Logic
  • Succinctness
  • LTLf
  • Finite Traces
  • Pure past LTL

Metrics

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

References

  1. Micah Adler and Neil Immerman. An n! lower bound on formula size. ACM Transactions on Computational Logic (TOCL), 4(3):296-314, 2003. Google Scholar
  2. Alessandro Artale, Luca Geatti, Nicola Gigante, Andrea Mazzullo, and Angelo Montanari. Complexity of safety and cosafety fragments of Linear Temporal Logic. In Proc. of the 36th AAAI Conf. on Artificial Intelligence (AAAI-22). AAAI Press, 2023. Google Scholar
  3. Howard Barringer, Michael Fisher, Dov Gabbay, Graham Gough, and Richard Owens. Metatem: A framework for programming in temporal logic. In Stepwise Refinement of Distributed Systems Models, Formalisms, Correctness: REX Workshop, Mook, The Netherlands May 29-June 2, 1989 Proceedings, pages 94-129. Springer, 1990. Google Scholar
  4. Ronen I. Brafman and Giuseppe De Giacomo. Planning for LTLf/LDLf goals in non-markovian fully observable nondeterministic domains. In Sarit Kraus, editor, Proceedings of the Twenty-Eighth International Joint Conference on Artificial Intelligence, pages 1602-1608. ijcai.org, 2019. Google Scholar
  5. Alberto Camacho, Jorge Baier, Christian Muise, and Sheila McIlraith. Finite ltl synthesis as planning. In Proceedings of the International Conference on Automated Planning and Scheduling, volume 28, pages 29-38, 2018. Google Scholar
  6. Alberto Camacho, Eleni Triantafillou, Christian J. Muise, Jorge A. Baier, and Sheila A. McIlraith. Non-deterministic planning with temporally extended goals: LTL over finite and infinite traces. In Satinder Singh and Shaul Markovitch, editors, Proceedings of the Thirty-First AAAI Conference on Artificial Intelligence, pages 3716-3724. AAAI Press, 2017. Google Scholar
  7. Edward Y. Chang, Zohar Manna, and Amir Pnueli. Characterization of temporal property classes. In Werner Kuich, editor, Proceedings of the 19th International Colloquium on Automata, Languages and Programming, volume 623 of Lecture Notes in Computer Science, pages 474-486. Springer, 1992. Google Scholar
  8. Alessandro Cimatti, Luca Geatti, Nicola Gigante, Angelo Montanari, and Stefano Tonetta. Extended bounded response LTL: a new safety fragment for efficient reactive synthesis. Formal Methods in System Design, pages 1-49, 2021. Google Scholar
  9. Giuseppe De Giacomo, Antonio Di Stasio, Francesco Fuggitti, and Sasha Rubin. Pure-past linear temporal and dynamic logic on finite traces. In Proceedings of the Twenty-Ninth International Conference on International Joint Conferences on Artificial Intelligence, pages 4959-4965, 2021. Google Scholar
  10. Giuseppe De Giacomo, Antonio Di Stasio, Lucas M. Tabajara, Moshe Y. Vardi, and Shufang Zhu. Finite-trace and generalized-reactivity specifications in temporal synthesis. In Zhi-Hua Zhou, editor, Proceedings of the Thirtieth International Joint Conference on Artificial Intelligence, pages 1852-1858. ijcai.org, 2021. Google Scholar
  11. 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. Google Scholar
  12. 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, pages 1558-1564. AAAI Press, 2015. Google Scholar
  13. Kousha Etessami, Moshe Y Vardi, and Thomas Wilke. First-order logic with two variables and unary temporal logic. Information and computation, 179(2):279-295, 2002. Google Scholar
  14. Dov Gabbay. The declarative past and imperative future: Executable temporal logic for interactive systems. In Temporal Logic in Specification: Altrincham, UK, April 8-10, 1987 Proceedings, pages 409-448. Springer, 1989. Google Scholar
  15. Lauri Hella and Miikka Vilander. Formula size games for modal logic and μ-calculus. J. Log. Comput., 29(8):1311-1344, 2019. Google Scholar
  16. Orna Lichtenstein, Amir Pnueli, and Lenore Zuck. The glory of the past. In Workshop on Logic of Programs, pages 196-218. Springer, 1985. Google Scholar
  17. Oded Maler and Amir Pnueli. Tight bounds on the complexity of cascaded decomposition of automata. In Proceedings [1990] 31st Annual Symposium on Foundations of Computer Science, pages 672-682. IEEE, 1990. Google Scholar
  18. Nicolas Markey. Temporal logic with past is exponentially more succinct. Bull. EATCS, 79:122-128, 2003. Google Scholar
  19. Maja Pesic, Helen Schonenberg, and Wil MP Van der Aalst. Declare: Full support for loosely-structured processes. In 11th IEEE international enterprise distributed object computing conference (EDOC 2007), pages 287-287. IEEE, 2007. Google Scholar
  20. Maja Pesic and Wil MP Van der Aalst. A declarative approach for flexible business processes management. In Business Process Management Workshops: BPM 2006 International Workshops, BPD, BPI, ENEI, GPWW, DPM, semantics4ws, Vienna, Austria, September 4-7, 2006. Proceedings 4, pages 169-180. Springer, 2006. Google Scholar
  21. A. Prasad Sistla. On characterization of safety and liveness properties in temporal logic. In Proceedings of the fourth annual ACM symposium on Principles of distributed computing, pages 39-48, 1985. Google Scholar
  22. Wolfgang Thomas. On the ehrenfeucht-fraïssé game in theoretical computer science. In TAPSOFT'93: Theory and Practice of Software Development: 4th International Joint Conference CAAP/FASE Orsay, France, April 13-17, 1993 Proceedings, pages 559-568. Springer, 2005. Google Scholar
  23. Shufang Zhu, Giuseppe De Giacomo, Geguang Pu, and Moshe Y. Vardi. Ltlf synthesis with fairness and stability assumptions. In The Thirty-Fourth AAAI Conference on Artificial Intelligence, AAAI 2020, The Thirty-Second Innovative Applications of Artificial Intelligence Conference, IAAI 2020, The Tenth AAAI Symposium on Educational Advances in Artificial Intelligence, EAAI 2020, New York, NY, USA, February 7-12, 2020, pages 3088-3095. AAAI Press, 2020. Google Scholar
  24. Shufang Zhu, Lucas M. Tabajara, Jianwen Li, Geguang Pu, and Moshe Y. Vardi. A Symbolic Approach to Safety LTL Synthesis. In Ofer Strichman and Rachel Tzoref-Brill, editors, Proceedings of the 13th International Haifa Verification Conference, volume 10629 of Lecture Notes in Computer Science, pages 147-162. Springer, 2017. URL: https://doi.org/10.1007/978-3-319-70389-3_10.
  25. Lenore Zuck. Past temporal logic. Weizmann Institute of Science, 67, 1986. 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
© 2023-2024 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact