Pith. sign in

REVIEW 2 cited by

Learning temporal formulas from examples is hard

Not yet reviewed by Pith; the record is open.

Re-run · record.json Download PDF Read on arXiv ↗

This paper has not been read by Pith yet. Machine review is queued; the pith claim, tier, and objections will appear here once it completes.

SPECIMEN: schema-true, not a live event

T0 review · schema-true

One-sentence machine reading of the paper's core claim.

pith:XXXXXXXX · record.json · timestamp

arxiv 2312.16336 v1 pith:4RIOETXL submitted 2023-12-26 cs.LG cs.AIcs.FLcs.LO

Corto Mascle , Nathanaël Fijalkow , Guillaume Lagarde This is my paper · ORCID
classification cs.LGcs.AIcs.FLcs.LO
keywords learningproblemcomplexityexamplesexpressingformulaslogicresults
verification ladder T0 review T1 audit T2 compute T3 formal

Signed reviews

No signed human review yet.

0 comments
read the original abstract

We study the problem of learning linear temporal logic (LTL) formulas from examples, as a first step towards expressing a property separating positive and negative instances in a way that is comprehensible for humans. In this paper we initiate the study of the computational complexity of the problem. Our main results are hardness results: we show that the LTL learning problem is NP-complete, both for the full logic and for almost all of its fragments. This motivates the search for efficient heuristics, and highlights the complexity of expressing separating properties in concise natural language.

Discussion (0). Continue with ORCID to comment.

Forward citations

Cited by 2 Pith papers

Reviewed papers in the Pith corpus that reference this work. Sorted by Pith novelty score. OpenAlex reports about 4 citations worldwide. Full citation record

  1. SAT-Based Bounded Fitting for the Description Logic ALC

    cs.AI 2025-07 accept novelty 7.0 of 10

    Bounded fitting in ALC fragments with existential or universal restrictions is NP-complete even for a single positive and negative example, and a SAT-based implementation, ALC-SAT+, performs competitively with existin...

  2. What is Formal Verification without Specifications? A Survey on mining LTL Specifications

    cs.FL 2025-01 conditional novelty 2.0 of 10

    This is a structured survey and qualitative comparison of recent algorithms for learning LTL specifications from positive and negative behavioral examples.

Pith tools