The Complexity of Learning Temporal Properties

TL;DR

This paper explores the computational complexity of learning temporal logic formulas from system behavior examples, revealing NP-completeness for unbounded cases and complexity differences among various temporal logics with bounded operators.

Contribution

It provides the first comprehensive complexity analysis of learning temporal logic formulas across multiple logics and their fragments.

Findings

Learning formulas with unbounded binary operators is NP-complete for LTL, CTL, and ATL.

Complexity varies among LTL, CTL, and ATL when binary operators are bounded.

Discrepancies exist in the complexity of learning formulas across different temporal logics.

Abstract

We consider the problem of learning temporal logic formulas from examples of system behavior. Learning temporal properties has crystallized as an effective mean 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 using an unbounded amount of 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 amount of occurrences of binary operators, we exhibit discrepancies between the complexity of learning LTL, CTL and ATL formulas (with a varying number of agents).