Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

The Complexity of Learning Temporal Properties

Benjamin Bordais, Daniel Neider, Rajarshi Roy

TL;DR

The paper analyzes the passive learning problem for temporal logics, showing that learning formulas with an unbounded number of binary operator occurrences is NP-complete across LTL, CTL, and ATL. It then investigates fragments with a bounded number of binary operators, revealing a nuanced landscape where LTL, CTL, and ATL differ in complexity depending on unary/binary operator sets and the number of agents. A central contribution is an abstract hitting-set-based reduction framework that systematically proves NP-hardness for many fragments, while also identifying polynomial-time cases (notably certain two-agent ATL with restricted operators). The results illuminate the intrinsic complexity of inferring temporal properties from behavior data and delineate boundaries between tractable vs intractable learning tasks in temporal logics, with potential implications for specification mining and automated verification. The work also highlights the role of operator arity and agent count in the learnability of temporal properties, suggesting future work on tractable templates and approximation strategies.

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

The Complexity of Learning Temporal Properties

TL;DR

The paper analyzes the passive learning problem for temporal logics, showing that learning formulas with an unbounded number of binary operator occurrences is NP-complete across LTL, CTL, and ATL. It then investigates fragments with a bounded number of binary operators, revealing a nuanced landscape where LTL, CTL, and ATL differ in complexity depending on unary/binary operator sets and the number of agents. A central contribution is an abstract hitting-set-based reduction framework that systematically proves NP-hardness for many fragments, while also identifying polynomial-time cases (notably certain two-agent ATL with restricted operators). The results illuminate the intrinsic complexity of inferring temporal properties from behavior data and delineate boundaries between tractable vs intractable learning tasks in temporal logics, with potential implications for specification mining and automated verification. The work also highlights the role of operator arity and agent count in the learnability of temporal properties, suggesting future work on tractable templates and approximation strategies.

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).
Paper Structure (54 sections, 69 theorems, 74 equations, 13 figures, 1 table)

This paper contains 54 sections, 69 theorems, 74 equations, 13 figures, 1 table.

Table of Contents

  1. Introduction
  2. Related Works.
  3. Definitions
  4. Complexity classes
  5. Some notations
  6. $\mathsf{LTL}$: syntax and semantics
  7. Infinite and ultimately periodic words.
  8. Set of operators
  9. Syntax.
  10. Semantics.
  11. $\mathsf{ATL}$ and $\mathsf{CTL}$: syntax and semantics
  12. Syntax.
  13. Semantics.
  14. Decision problems
  15. Learning with non-unary binary operators is $\mathsf{NP}$-hard
  16. ...and 39 more sections

Key Result

Proposition 6

For all $\mathsf{U}^\mathsf{t} \subseteq \mathsf{Op}_{\mathsf{Un}}^{\mathsf{}}$, $\mathsf{B}^\mathsf{t} \subseteq \mathsf{Op}_{\mathsf{Bin}}^{\mathsf{tp}}$, $\mathsf{B}^\mathsf{l} \subseteq \mathsf{Op}_{\mathsf{Bin}}^{\mathsf{lg}}$ and $n \in \mathbb{N} \cup \{\infty\}$, the decision problems $\math

Figures (13)

  • Figure 1: Algorithm $\mathsf{DecideLTL}_{\mathsf{Unif}}(\varphi,w,i)$.
  • Figure 2: The Kripke structure $K^{\mathcal{P}}_{l}$.
  • Figure 3: The Kripke structure $K^{\mathcal{N}}_{l}$.
  • Figure 4: The Kripke structure $K_{(5,\{ 2,5 \})}$.
  • Figure 5: The Kripke structure $K^5_{\exists > 2}$.
  • ...and 8 more figures

Theorems & Definitions (188)

  • Definition 1
  • Definition 2
  • Definition 3
  • Definition 4
  • Definition 5
  • Proposition 6
  • Definition 7: Hitting set problem
  • Theorem 8: DBLP:conf/coco/Karp72
  • Theorem 10
  • Lemma 11
  • ...and 178 more