Pith. sign in

REVIEW 1 cited by

Learning Temporal Properties is NP-hard

Not yet reviewed by Pith; the record is open.

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.11403 v1 pith:56QXO4R7 submitted 2023-12-18 cs.LO

classification cs.LO
keywords learningwordsfinitenp-hardgivennegativeperiodicpositive
verification ladder T0 review T1 audit T2 compute T3 formal

Signed reviews

No signed human review yet.

0 comments
read the original abstract

We investigate the complexity of LTL learning, which consists in deciding given a finite set of positive ultimately periodic words, a finite set of negative ultimately periodic words, and a bound B given in unary, if there is an LTL-formula of size less than or equal to B that all positive words satisfy and that all negative violate. We prove that this decision problem is NP-hard. We then use this result to show that CTL learning is also NP-hard. CTL learning is similar to LTL learning except that words are replaced by finite Kripke structures and we look for the existence of CTL formulae.

Discussion (0). Continue with ORCID to comment.

Forward citations

Cited by 1 Pith paper

Reviewed papers in the Pith corpus that reference this work. Sorted by Pith novelty score. Full citation record

  1. Learning Linear Temporal Specifications from Demonstrations with Uncertainty

    cs.AI 2026-07 conditional novelty 6.0 of 10

    Minimal LTL formulas can be learned from uncertain traces by Hamming-ball groups plus a Pseudo-Boolean optimization that forces at least one consistent estimate per group.

Pith tools