Executive Summary : | Automated functional synthesis is the problem of algorithmically generating programs or circuits that provably satisfy a given specification. Typically, the specification is given as a formula in an appropriate logic, relating the inputs and outputs of the program. The synthesis task starts from such a (relational) specification and generates a program or circuit for computing each output in terms of the inputs such that the specification is satisfied. In recent years, there has been a surge of interest in designing practical algorithms for functional synthesis from propositional specifications. A foundational understanding of complexity and algorithmic issues involved in synthesis from first-order logic (FOL) specifications has however been missing from the literature. In this project, we propose to investigate some of these open foundational questions and bridge this gap. Specifically, the project will investigate classes of FOL specifications that admit terms (in the underlying logic) as Skolem functions, and that admit Turing machines (algorithms) with running time that grows polynomially in the input size as Skolem functions. The project will attempt to arrive at a characterization of sub-classes of FOL specifications that admit (i) efficient synthesis of Turing machines (algorithms) implementing the Skolem functions even if the algorithms themselves are not efficient, and (ii) synthesis of efficiently evaluatable Skolem functions, even if the process of synthesizing Turing machines that implement such Skolem functions is not efficient. A particularly interesting class of specifications would be those that satisfy both of the above criteria. The work proposed to be done as part of this project will complement work already done by the applicant in synthesis of Skolem functions from propositional specifications. Papers arising out of the proposed work are expected to be published at leading formal methods conferences and journals. |