TY - GEN
T1 - Learning Linear Temporal Properties from Noisy Data
T2 - 19th International Symposium on Automated Technology for Verification and Analysis, ATVA 2021
AU - Gaglione, Jean Raphaël
AU - Neider, Daniel
AU - Roy, Rajarshi
AU - Topcu, Ufuk
AU - Xu, Zhe
N1 - Funding Information:
Acknowledgements. This work has been supported by the Defense Advanced Research Projects Agency (DARPA) under Contract no. HR001120C0032, ARL W911NF2020132, ARL ACC-APG-RTP W911NF, NSF 1646522 and DFG Grant no. 434592664.
Publisher Copyright:
© 2021, Springer Nature Switzerland AG.
PY - 2021
Y1 - 2021
N2 - We address the problem of inferring descriptions of system behavior using Linear Temporal Logic (LTL) from a finite set of positive and negative examples. Most of the existing approaches for solving such a task rely on predefined templates for guiding the structure of the inferred formula. The approaches that can infer arbitrary LTL formulas, on the other hand, are not robust to noise in the data. To alleviate such limitations, we devise two algorithms for inferring concise LTL formulas even in the presence of noise. Our first algorithm infers minimal LTL formulas by reducing the inference problem to a problem in maximum satisfiability and then using off-the-shelf MaxSAT solvers to find a solution. To the best of our knowledge, we are the first to incorporate the usage of MaxSAT solvers for inferring formulas in LTL. Our second learning algorithm relies on the first algorithm to derive a decision tree over LTL formulas based on a decision tree learning algorithm. We have implemented both our algorithms and verified that our algorithms are efficient in extracting concise LTL descriptions even in the presence of noise.
AB - We address the problem of inferring descriptions of system behavior using Linear Temporal Logic (LTL) from a finite set of positive and negative examples. Most of the existing approaches for solving such a task rely on predefined templates for guiding the structure of the inferred formula. The approaches that can infer arbitrary LTL formulas, on the other hand, are not robust to noise in the data. To alleviate such limitations, we devise two algorithms for inferring concise LTL formulas even in the presence of noise. Our first algorithm infers minimal LTL formulas by reducing the inference problem to a problem in maximum satisfiability and then using off-the-shelf MaxSAT solvers to find a solution. To the best of our knowledge, we are the first to incorporate the usage of MaxSAT solvers for inferring formulas in LTL. Our second learning algorithm relies on the first algorithm to derive a decision tree over LTL formulas based on a decision tree learning algorithm. We have implemented both our algorithms and verified that our algorithms are efficient in extracting concise LTL descriptions even in the presence of noise.
KW - Explainable AI
KW - Linear temporal logic
KW - Specification mining
UR - http://www.scopus.com/inward/record.url?scp=85118141033&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=85118141033&partnerID=8YFLogxK
U2 - 10.1007/978-3-030-88885-5_6
DO - 10.1007/978-3-030-88885-5_6
M3 - Conference contribution
AN - SCOPUS:85118141033
SN - 9783030888848
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 74
EP - 90
BT - Automated Technology for Verification and Analysis - 19th International Symposium, ATVA 2021, Proceedings
A2 - Hou, Zhe
A2 - Ganesh, Vijay
PB - Springer Science and Business Media Deutschland GmbH
Y2 - 18 October 2021 through 22 October 2021
ER -