View in EDS

Linear temporal constraints for sketch-based synthesizers.

Saved in:
Bibliographic Details
Title: Linear temporal constraints for sketch-based synthesizers.
Authors: Galicia-Mendoza, Fernando A.1 (AUTHOR) fernandogamen@ciencias.unam.mx, Rosenblueth, David A.2 (AUTHOR) drosenbl@unam.mx, Solar-Lezama, Armando3 (AUTHOR) asolar@csail.mit.edu
Source: Formal Methods in System Design. Jun2026, Vol. 68 Issue 3, p1-34. 34p.
Subjects: Program generators (Computer programs), Computer software, Finite state machines
Abstract: Sketch-based program synthesis allows users to guide the synthesizer by writing partial programs (sketches). Traditionally, the specifications of these sketches are safety properties expressed either as assertions or semantic equivalences. These specifications, however, lack expressiveness when the user wants to establish how the execution of the desired program evolves over time. This is especially important when synthesizing reactive programs, where the whole specification is about how the computation evolves over time. We explore an alternative method letting the user specify desired program executions as linear temporal logic (LTL) formulae. We define a method for transforming sketches with LTL assertions into sketches with only standard assertions. Specifically, for terminating programs, our method transforms and implements, within the sketch, the LTL formulae as runtime monitors. For non-terminating programs, our procedure defines and implements, into the sketch, fairness conditions (analyzing when an acceptance state of the Büchi automata equivalent to these LTL formulae occurs infinitely often). We prove the correctness of both constructions. Evaluation of our implementation in Sketch shows that our method enables the system to synthesize non-terminating programs, such as a round-robin arbiter for a variable number of devices and a lift controller for a variable number of floors. For terminating programs, our approach improves the synthesizer performance by restricting the search of program candidates without modifying the sketches structures. [ABSTRACT FROM AUTHOR]
Copyright of Formal Methods in System Design is the property of Springer Nature and its content may not be copied or emailed to multiple sites without the copyright holder's express written permission. Additionally, content may not be used with any artificial intelligence tools or machine learning technologies. However, users may print, download, or email articles for individual use. This abstract may be abridged. No warranty is given about the accuracy of the copy. Users should refer to the original published version of the material for the full abstract. (Copyright applies to all Abstracts.)
Database: Engineering Source
Description
Abstract:Sketch-based program synthesis allows users to guide the synthesizer by writing partial programs (sketches). Traditionally, the specifications of these sketches are safety properties expressed either as assertions or semantic equivalences. These specifications, however, lack expressiveness when the user wants to establish how the execution of the desired program evolves over time. This is especially important when synthesizing reactive programs, where the whole specification is about how the computation evolves over time. We explore an alternative method letting the user specify desired program executions as linear temporal logic (LTL) formulae. We define a method for transforming sketches with LTL assertions into sketches with only standard assertions. Specifically, for terminating programs, our method transforms and implements, within the sketch, the LTL formulae as runtime monitors. For non-terminating programs, our procedure defines and implements, into the sketch, fairness conditions (analyzing when an acceptance state of the Büchi automata equivalent to these LTL formulae occurs infinitely often). We prove the correctness of both constructions. Evaluation of our implementation in Sketch shows that our method enables the system to synthesize non-terminating programs, such as a round-robin arbiter for a variable number of devices and a lift controller for a variable number of floors. For terminating programs, our approach improves the synthesizer performance by restricting the search of program candidates without modifying the sketches structures. [ABSTRACT FROM AUTHOR]
ISSN:09259856
DOI:10.1007/s10703-026-00495-8