Conference proceeding
SYSLITE: Syntax-Guided Synthesis of PLTL Formulas from Finite Traces
2020 Formal Methods in Computer Aided Design (FMCAD), pp.93-103
09/21/2020
DOI: 10.34727/2020/isbn.978-3-85448-042-6_16
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.
Details
- Title: Subtitle
- SYSLITE: Syntax-Guided Synthesis of PLTL Formulas from Finite Traces
- Creators
- M. Fareed Arif - University of IowaDaniel Larraz - University of IowaMitziu Echeverria - University of IowaAndrew Reynolds - University of IowaOmar Chowdhury - University of IowaCesare Tinelli - University of Iowa
- Resource Type
- Conference proceeding
- Publication Details
- 2020 Formal Methods in Computer Aided Design (FMCAD), pp.93-103
- DOI
- 10.34727/2020/isbn.978-3-85448-042-6_16
- eISSN
- 2708-7824
- Publisher
- FMCAD Association
- Grant note
- D19AP00039 / DARPA (10.13039/100000185) 1656926 / NSF (10.13039/501100001809)
- Language
- English
- Date published
- 09/21/2020
- Academic Unit
- Computer Science
- Record Identifier
- 9984259476902771
Metrics
27 Record Views