SYSLITE: Syntax-Guided Synthesis of PLTL Formulas from Finite Traces
M. Fareed Arif, Daniel Larraz, Mitziu Echeverria, Andrew J. Reynolds, Omar Chowdhury, Cesare Tinelli · 2020
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.