Learning Temporal Properties is NP-hard
Logic in Computer Science
2023-12-19 v1
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.
Cite
@article{arxiv.2312.11403,
title = {Learning Temporal Properties is NP-hard},
author = {Benjamin Bordais and Daniel Neider and Rajarshi Roy},
journal= {arXiv preprint arXiv:2312.11403},
year = {2023}
}