The complexity of learning LTL, CTL and ATL formulas

Conference item

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).

Authors: Bordais, B; Neider, D; Roy, R

• Publication status: Published
• Peer review status: Peer reviewed
• Publisher: Schloss Dagstuhl – Leibniz-Zentrum für Informatik
• Host title: 42nd International Symposium on Theoretical Aspects of Computer Science (STACS 2025)
• Pages: 19:1-19:20
• Article number: 19
• Series: Leibniz International Proceedings in Informatics (LIPIcs)
• Series number: 327
• Publication date: 2025-02-24
• Acceptance date: 2024-12-12
• Event title: 42nd International Symposium on Theoretical Aspects of Computer Science (STACS 2025)
• Event location: Jena, Germany
• Event website: https://stacs2025.de/
• Event start date: 2025-03-04
• Event end date: 2025-03-07
• DOI: 10.4230/LIPICS.STACS.2025.19
• ISSN: 1868-8969
• ISBN: 9783959773652
• Language: English
• Keywords: temporal logic; passive learning; complexity