Program Synthesis Of Linear Temporal Logic Over Finite Traces

Program synthesis is an approach of automatically designing a system that interacts continuously with an environment,using a declarative specification of the system's behaviors.A popular language for providing such a specification is Linear Temporal Logic,or LTL_for short.Standard LTL synthesis,however,is a hard problem to solve in practice.Therefore,many works have targeted on developing specific techniques for certain subclasses of LTL and obtained significant results,for example,GR(1).In this work,we focus on a new logic,Linear Temporal Logic over finite traces,or LTL_f,which interprets LTL formulas semantically on finite traces.Such interpretation allows for arbitrarily long but finite executions of the system,and is adequate for finite-horizon problems in Computer Science and Artificial Intelligence.In particular,we study here the problem of LTL_fsynthesis.The contributions of this dissertation are summarized as follows:· We introduce a symbolic LTL_fsynthesis framework.Given the unavoidable problem of space explosion in the classical solution to LTL_fsynthesis,we propose a formalization of symbolic DFA,which allows us to introduce here a BDD-based,fixpoint-based symbolic LTL_fsynthesis framework.We show,empirically,that this symbolic technique outperforms existing approaches.· We present a comprehensive study of different encodings for the translation to DFAfrom LTL_fformulas.In particular,we explore second-order encodings of LTL_fformulas,and present the first evaluation of the spectrum of encodings for LTL_ffrom first-order to second-order.First,we introduce a specific MSO encoding that captures LTL_fsemantics in a natural way.Then,we present Compact MSO encoding,which benefits from automata-theoretic minimization,thus suggesting a possible practical advantage.To that end,we propose a formulation of symbolic DFA represented in BDDs using secondorder logic,thus developing a novel connection between BDDs and MSO.The main result of our empirical evaluations is the superiority of the first-order encoding for LTL_f-to-DFA translation.· We investigate the power of automata minimization in LTL_fsynthesis.Our focus here is to understand the balance between the heavy minimization cost and the DFA size decreasing bonus.We introduce an indirect DFAconstruction approach,which first constructs an NFA and then performs symbolic determinization to directly obtain the symbolic DFA without minimizing.Our experiments show,however,that synthesis using the minimal DFA in general performs better than the symbolically-determinized DFA,even when determinization is performed on the fly.This is because in practice the minimal DFA surprisingly tends to be smaller than the NFA constructed in the alternative approach,despite the exponential gap in theory.This observation illustrates the indispensability of the automata minimization procedure in LTL_fsynthesis and leads to the conclusion that,rather than trying to work around minimization to improve DFA construction,we must find ways to take maximum advantage of its benefits while mitigating its weaknesses.· We generalize our symbolic LTL_fframework to LTL_fsynthesis with simple fairness assumptions.Based on the observations obtained from the previous work,we develop a specific BDD-based,nested fixpoint-based technique for solving this problem,which avoids the detour of a reduction to LTL synthesis.Our empirical evaluation shows the outperformance of this technique over existing approaches,which illustrates the simplicity of our approach in theory, and its promising potential in practice.