2026-07-20T05:46:26Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:22844 2025-10-02T13:35:16Z ddc:004 open_access

The Complexity of Learning LTL, CTL and ATL Formulas Bordais, Benjamin Neider, Daniel Roy, Rajarshi Temporal logic passive learning complexity 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). Schloss Dagstuhl – Leibniz-Zentrum für Informatik Benjamin Bordais and Daniel Neider and Rajarshi Roy 2025 Is Part Of LIPIcs, Volume 327, 42nd International Symposium on Theoretical Aspects of Computer Science (STACS 2025) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.STACS.2025.19 urn:nbn:de:0030-drops-228441 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.STACS.2025.19 eng https://creativecommons.org/licenses/by/4.0/legalcode