Exact Synthesis of LTL Properties from Traces

We present an exact approach to synthesize temporal-logic formulas in linear temporal logic (LTL) from a set of given positive and negative example traces. Our approach uses topology structures, in particular partial DAGs, to partition the search space into small and manageable subproblems. The algorithm then solves each subproblem independently with the aid of an oracle for deciding satisfiability modulo propositional logic. This strategy is capable of achieving a super-linear speedup when parallelized. We have implemented a bounded synthesis approach to find an LTL formula of minimum size using the proposed topology-guided exact synthesis approach. In an experimental evaluation, we show that the proposed approach achieves a 20x runtime improvement over the state-of-the-art approach.

Published in:
Proceedings Of The 2019 Forum On Specification And Design Languages (Fdl)
Presented at:
Forum on Specification and Design Languages (FDL), Southampton, ENGLAND, Sep 02-04, 2019
Jan 01 2019
New York, IEEE

 Record created 2020-09-17, last modified 2020-10-29

Rate this document:

Rate this document:
(Not yet reviewed)