@inproceedings{07835345a9454ee598699d8a28e3d215,
title = "SYSLITE: Syntax-Guided Synthesis of PLTL Formulas from Finite Traces",
abstract = "We present an efficient approach to learn past-time linear temporal logic formulas (PLTL) from a set of propositional variables and a sample of finite traces over those variables. The efficiency of our approach can be attributed to a careful encoding of the PLTL formula learning problem as a bit-vector function synthesis problem, and the use of an enhanced Syntax-Guided Synthesis (SyGuS) engine to solve the latter. We implemented our approach in a tool called Syslite and empirically evaluated its efficacy with two case studies. In these case studies, we observe that Syslite on average enjoys a speedup of 44x over current learning approaches for temporal formulas while learning the expected formulas in the vast majority of cases.",
author = "\{Fareed Arif\}, M. and Daniel Larraz and Mitziu Echeverria and Andrew Reynolds and Omar Chowdhury and Cesare Tinelli",
note = "Publisher Copyright: {\textcopyright} 2020 FMCAD Association.; 20th International Conference on Formal Methods in Computer-Aided Design, FMCAD 2020 ; Conference date: 21-09-2020 Through 24-09-2020",
year = "2020",
month = sep,
day = "21",
doi = "10.34727/2020/isbn.978-3-85448-042-6\_16",
language = "English",
series = "Proceedings of the 20th Conference on Formal Methods in Computer-Aided Design, FMCAD 2020",
publisher = "Institute of Electrical and Electronics Engineers Inc.",
pages = "93--103",
editor = "Alexander Ivrii and Ofer Strichman and Hunt, \{Warren A.\} and Georg Weissenbacher",
booktitle = "Proceedings of the 20th Conference on Formal Methods in Computer-Aided Design, FMCAD 2020",
}