Document Open Access Logo

The Complexity of Learning LTL, CTL and ATL Formulas

Authors Benjamin Bordais , Daniel Neider , Rajarshi Roy

PDF
Thumbnail PDF

File

LIPIcs.STACS.2025.19.pdf
  • Filesize: 1.2 MB
  • 20 pages

Document Identifiers

Author Details

Benjamin Bordais
  • TU Dortmund University, Center for Trustworthy Data Science and Security, University Alliance Ruhr, Dortmund, Germany
Daniel Neider
  • TU Dortmund University, Center for Trustworthy Data Science and Security, University Alliance Ruhr, Dortmund, Germany
Rajarshi Roy
  • Department of Computer Science, University of Oxford, UK

Funding

Rajarshi Roy acknowledges partial funding by the ERC under the European Union’s Horizon 2020 research and innovation programme (grant agreement No.834115, FUN2MODEL).

Cite As Get BibTex

Benjamin Bordais, Daniel Neider, and Rajarshi Roy. The Complexity of Learning LTL, CTL and ATL Formulas. In 42nd International Symposium on Theoretical Aspects of Computer Science (STACS 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 327, pp. 19:1-19:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025) https://doi.org/10.4230/LIPIcs.STACS.2025.19

Abstract

We consider the problem of learning temporal logic formulas from examples of system behavior. Learning temporal properties has crystallized as an effective means to explain complex temporal behaviors. Several efficient algorithms have been designed for learning temporal formulas. However, the theoretical understanding of the complexity of the learning decision problems remains largely unexplored. To address this, we study the complexity of the passive learning problems of three prominent temporal logics, Linear Temporal Logic (LTL), Computation Tree Logic (CTL) and Alternating-time Temporal Logic (ATL) and several of their fragments. We show that learning formulas with unbounded occurrences of binary operators is NP-complete for all of these logics. On the other hand, when investigating the complexity of learning formulas with bounded occurrences of binary operators, we exhibit discrepancies between the complexity of learning LTL, CTL and ATL formulas (with a varying number of agents).

Subject Classification

ACM Subject Classification
  • Theory of computation
Keywords
  • Temporal logic
  • passive learning
  • complexity

Metrics

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

Related Versions

References

  1. Rajeev Alur, Thomas A. Henzinger, and Orna Kupferman. Alternating-time temporal logic. J. ACM, 49(5):672-713, September 2002. URL: https://doi.org/10.1145/585265.585270.
  2. Dana Angluin. On the complexity of minimum inference of regular sets. Inf. Control., 39(3):337-350, 1978. URL: https://doi.org/10.1016/S0019-9958(78)90683-6.
  3. M. Fareed Arif, Daniel Larraz, Mitziu Echeverria, Andrew Reynolds, Omar Chowdhury, and Cesare Tinelli. SYSLITE: syntax-guided synthesis of PLTL formulas from finite traces. In FMCAD, pages 93-103. IEEE, 2020. URL: https://doi.org/10.34727/2020/ISBN.978-3-85448-042-6_16.
  4. Ayca Balkan, Moshe Y. Vardi, and Paulo Tabuada. Mode-target games: Reactive synthesis for control applications. IEEE Trans. Autom. Control., 63(1):196-202, 2018. URL: https://doi.org/10.1109/TAC.2017.2722960.
  5. Elwyn R. Berlekamp, Robert J. McEliece, and Henk C. A. van Tilborg. On the inherent intractability of certain coding problems (corresp.). IEEE Trans. Inf. Theory, 24(3):384-386, 1978. URL: https://doi.org/10.1109/TIT.1978.1055873.
  6. Dines Bjørner and Klaus Havelund. 40 years of formal methods - some obstacles and some possibilities? In FM, volume 8442 of Lecture Notes in Computer Science, pages 42-61. Springer, 2014. URL: https://doi.org/10.1007/978-3-319-06410-9_4.
  7. Giuseppe Bombara, Cristian-Ioan Vasile, Francisco Penedo, Hirotoshi Yasuoka, and Calin Belta. A decision tree approach to data classification using signal temporal logic. In Proceedings of the 19th International Conference on Hybrid Systems: Computation and Control, HSCC '16, pages 1-10, New York, NY, USA, 2016. Association for Computing Machinery. URL: https://doi.org/10.1145/2883817.2883843.
  8. Benjamin Bordais, Daniel Neider, and Rajarshi Roy. The complexity of learning temporal properties. CoRR, abs/2408.04486, 2024. URL: https://doi.org/10.48550/arXiv.2408.04486.
  9. Benjamin Bordais, Daniel Neider, and Rajarshi Roy. Learning branching-time properties in CTL and ATL via constraint solving. In André Platzer, Kristin Yvonne Rozier, Matteo Pradella, and Matteo Rossi, editors, Formal Methods - 26th International Symposium, FM 2024, Milan, Italy, September 9-13, 2024, Proceedings, Part I, volume 14933 of Lecture Notes in Computer Science, pages 304-323. Springer, 2024. URL: https://doi.org/10.1007/978-3-031-71162-6_16.
  10. Alberto Camacho, Rodrigo Toro Icarte, Toryn Q. Klassen, Richard Anthony Valenzano, and Sheila A. McIlraith. LTL and beyond: Formal languages for reward function specification in reinforcement learning. In Sarit Kraus, editor, Proceedings of the Twenty-Eighth International Joint Conference on Artificial Intelligence, IJCAI 2019, Macao, China, August 10-16, 2019, pages 6065-6073. ijcai.org, 2019. URL: https://doi.org/10.24963/IJCAI.2019/840.
  11. Alberto Camacho and Sheila A. McIlraith. Learning interpretable models expressed in linear temporal logic. In ICAPS, pages 621-630. AAAI Press, 2019. URL: https://ojs.aaai.org/index.php/ICAPS/article/view/3529.
  12. 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 AAAI, pages 3716-3724. AAAI Press, 2017. URL: https://doi.org/10.1609/AAAI.V31I1.11058.
  13. Alessio Cecconi, Giuseppe De Giacomo, Claudio Di Ciccio, Fabrizio Maria Maggi, and Jan Mendling. Measuring the interestingness of temporal logic behavioral specifications in process mining. Inf. Syst., 107:101920, 2022. URL: https://doi.org/10.1016/J.IS.2021.101920.
  14. William Chan. Temporal-logic queries. In CAV, volume 1855 of Lecture Notes in Computer Science, pages 450-463. Springer, 2000. Google Scholar
  15. Edmund M. Clarke and E. Allen Emerson. Design and synthesis of synchronization skeletons using branching-time temporal logic. In Dexter Kozen, editor, Logics of Programs, Workshop, Yorktown Heights, New York, USA, May 1981, volume 131 of Lecture Notes in Computer Science, pages 52-71. Springer, 1981. URL: https://doi.org/10.1007/BFB0025774.
  16. Rüdiger Ehlers, Ivan Gavran, and Daniel Neider. Learning properties in LTL ∩ ACTL from positive examples only. In 2020 Formal Methods in Computer Aided Design, FMCAD 2020, Haifa, Israel, September 21-24, 2020, pages 104-112. IEEE, 2020. URL: https://doi.org/10.34727/2020/ISBN.978-3-85448-042-6_17.
  17. Georgios E. Fainekos, Hadas Kress-Gazit, and George J. Pappas. Temporal logic motion planning for mobile robots. In ICRA, pages 2020-2025. IEEE, 2005. URL: https://doi.org/10.1109/ROBOT.2005.1570410.
  18. Nathanaël Fijalkow and Guillaume Lagarde. The complexity of learning linear temporal formulas from examples. In Jane Chandlee, Rémi Eyraud, Jeff Heinz, Adam Jardine, and Menno van Zaanen, editors, Proceedings of the 15th International Conference on Grammatical Inference, 23-27 August 2021, Virtual Event, volume 153 of Proceedings of Machine Learning Research, pages 237-250. PMLR, 2021. URL: https://proceedings.mlr.press/v153/fijalkow21a.html.
  19. Marie Fortin, Boris Konev, Vladislav Ryzhikov, Yury Savateev, Frank Wolter, and Michael Zakharyaschev. Reverse engineering of temporal queries mediated by LTL ontologies. In Proceedings of the Thirty-Second International Joint Conference on Artificial Intelligence, IJCAI 2023, 19th-25th August 2023, Macao, SAR, China, pages 3230-3238. ijcai.org, 2023. URL: https://doi.org/10.24963/IJCAI.2023/360.
  20. Jean-Raphaël Gaglione, Daniel Neider, Rajarshi Roy, Ufuk Topcu, and Zhe Xu. Maxsat-based temporal logic inference from noisy data. Innov. Syst. Softw. Eng., 18(3):427-442, 2022. URL: https://doi.org/10.1007/S11334-022-00444-8.
  21. E. Mark Gold. Complexity of automaton identification from given data. Inf. Control., 37(3):302-320, 1978. URL: https://doi.org/10.1016/S0019-9958(78)90562-4.
  22. Antonio Ielo, Mark Law, Valeria Fionda, Francesco Ricca, Giuseppe De Giacomo, and Alessandra Russo. Towards ilp-based ltlf passive learning. In Inductive Logic Programming: 32nd International Conference, ILP 2023, Bari, Italy, November 13–15, 2023, Proceedings, pages 30-45, Berlin, Heidelberg, 2023. Springer-Verlag. URL: https://doi.org/10.1007/978-3-031-49299-0_3.
  23. Neil Immerman. Number of quantifiers is better than number of tape cells. J. Comput. Syst. Sci., 22(3):384-406, 1981. URL: https://doi.org/10.1016/0022-0000(81)90039-8.
  24. Jean Christoph Jung, Vladislav Ryzhikov, Frank Wolter, and Michael Zakharyaschev. Extremal separation problems for temporal instance queries. In Proceedings of the Thirty-Third International Joint Conference on Artificial Intelligence, IJCAI 2024, Jeju, South Korea, August 3-9, 2024, pages 3448-3456. ijcai.org, 2024. URL: https://www.ijcai.org/proceedings/2024/382.
  25. Xiao Li, Cristian Ioan Vasile, and Calin Belta. Reinforcement learning with temporal logic rewards. In 2017 IEEE/RSJ International Conference on Intelligent Robots and Systems, IROS 2017, Vancouver, BC, Canada, September 24-28, 2017, pages 3834-3839. IEEE, 2017. URL: https://doi.org/10.1109/IROS.2017.8206234.
  26. Weilin Luo, Pingjia Liang, Jianfeng Du, Hai Wan, Bo Peng, and Delong Zhang. Bridging ltlf inference to GNN inference for learning ltlf formulae. In AAAI, pages 9849-9857. AAAI Press, 2022. URL: https://doi.org/10.1609/AAAI.V36I9.21221.
  27. Corto Mascle, Nathanaël Fijalkow, and Guillaume Lagarde. Learning temporal formulas from examples is hard. CoRR, abs/2312.16336, 2023. URL: https://doi.org/10.48550/arXiv.2312.16336.
  28. Sara Mohammadinejad, Jyotirmoy V. Deshmukh, Aniruddh Gopinath Puranic, Marcell Vazquez-Chanlatte, and Alexandre Donzé. Interpretable classification of time-series data using efficient enumerative techniques. In HSCC '20: 23rd ACM International Conference on Hybrid Systems: Computation and Control, Sydney, New South Wales, Australia, April 21-24, 2020, pages 9:1-9:10. ACM, 2020. URL: https://doi.org/10.1145/3365365.3382218.
  29. Daniel Neider and Ivan Gavran. Learning linear temporal properties. In Nikolaj S. Bjørner and Arie Gurfinkel, editors, 2018 Formal Methods in Computer Aided Design, FMCAD 2018, Austin, TX, USA, October 30 - November 2, 2018, pages 1-10. IEEE, 2018. URL: https://doi.org/10.23919/FMCAD.2018.8603016.
  30. Daniel Neider and Rajarshi Roy. What Is Formal Verification Without Specifications? A Survey on Mining LTL Specifications, pages 109-125. Springer Nature Switzerland, Cham, 2025. URL: https://doi.org/10.1007/978-3-031-75778-5_6.
  31. C.H. Papadimitriou. Computational Complexity. Theoretical computer science. Addison-Wesley, 1994. URL: https://books.google.de/books?id=JogZAQAAIAAJ.
  32. Nir Piterman, Amir Pnueli, and Yaniv Sa'ar. Synthesis of reactive(1) designs. In E. Allen Emerson and Kedar S. Namjoshi, editors, Verification, Model Checking, and Abstract Interpretation, 7th International Conference, VMCAI 2006, Charleston, SC, USA, January 8-10, 2006, Proceedings, volume 3855 of Lecture Notes in Computer Science, pages 364-380. Springer, 2006. URL: https://doi.org/10.1007/11609773_24.
  33. Amir Pnueli. The temporal logic of programs. In Proc. 18th Annu. Symp. Found. Computer Sci., pages 46-57, 1977. URL: https://doi.org/10.1109/SFCS.1977.32.
  34. Adrien Pommellet, Daniel Stan, and Simon Scatton. Sat-based learning of computation tree logic. In Christoph Benzmüller, Marijn J. H. Heule, and Renate A. Schmidt, editors, Automated Reasoning - 12th International Joint Conference, IJCAR 2024, Nancy, France, July 3-6, 2024, Proceedings, Part I, volume 14739 of Lecture Notes in Computer Science, pages 366-385. Springer, 2024. URL: https://doi.org/10.1007/978-3-031-63498-7_22.
  35. Ritam Raha, Rajarshi Roy, Nathanaël Fijalkow, and Daniel Neider. Scalable anytime algorithms for learning fragments of linear temporal logic. In Dana Fisman and Grigore Rosu, editors, Tools and Algorithms for the Construction and Analysis of Systems, pages 263-280, Cham, 2022. Springer International Publishing. URL: https://doi.org/10.1007/978-3-030-99524-9_14.
  36. Ritam Raha, Rajarshi Roy, Nathanaël Fijalkow, Daniel Neider, and Guillermo A. Pérez. Synthesizing efficiently monitorable formulas in metric temporal logic. In VMCAI (2), volume 14500 of Lecture Notes in Computer Science, pages 264-288. Springer, 2024. URL: https://doi.org/10.1007/978-3-031-50521-8_13.
  37. Heinz Riener. Exact synthesis of LTL properties from traces. In FDL, pages 1-6. IEEE, 2019. URL: https://doi.org/10.1109/FDL.2019.8876900.
  38. Rajarshi Roy, Dana Fisman, and Daniel Neider. Learning interpretable models in the property specification language. In IJCAI, pages 2213-2219. ijcai.org, 2020. URL: https://doi.org/10.24963/IJCAI.2020/306.
  39. Kristin Yvonne Rozier. Specification: The biggest bottleneck in formal methods and autonomy. In VSTTE, volume 9971 of Lecture Notes in Computer Science, pages 8-26, 2016. URL: https://doi.org/10.1007/978-3-319-48869-1_2.
  40. Dorsa Sadigh, Eric S. Kim, Samuel Coogan, S. Shankar Sastry, and Sanjit A. Seshia. A learning based approach to control synthesis of markov decision processes for linear temporal logic specifications. In 53rd IEEE Conference on Decision and Control, CDC 2014, Los Angeles, CA, USA, December 15-17, 2014, pages 1091-1096. IEEE, 2014. URL: https://doi.org/10.1109/CDC.2014.7039527.
  41. Mojtaba Valizadeh, Nathanaël Fijalkow, and Martin Berger. LTL learning on gpus. In Arie Gurfinkel and Vijay Ganesh, editors, Computer Aided Verification - 36th International Conference, CAV 2024, Montreal, QC, Canada, July 24-27, 2024, Proceedings, Part III, volume 14683 of Lecture Notes in Computer Science, pages 209-231. Springer, 2024. URL: https://doi.org/10.1007/978-3-031-65633-0_10.
  42. Hai Wan, Pingjia Liang, Jianfeng Du, Weilin Luo, Rongzhen Ye, and Bo Peng. End-to-end learning of ltlf formulae by faithful ltlf encoding. In AAAI, pages 9071-9079. AAAI Press, 2024. URL: https://doi.org/10.1609/AAAI.V38I8.28757.
  43. Andrzej Wasylkowski and Andreas Zeller. Mining temporal specifications from object usage. Autom. Softw. Eng., 18(3-4):263-292, 2011. URL: https://doi.org/10.1007/S10515-011-0084-1.
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