LTLf Synthesis on First-Order Action Theories

• URL: http://arxiv.org/abs/2410.00726v1
• Date: Tue, 1 Oct 2024 14:15:14 GMT
• Title: LTLf Synthesis on First-Order Action Theories
• Authors: Till Hofmann, Jens Claßen,
• Abstract summary: Golog is an expressive high-level agent language that includes nondeterministic operators. In this paper, we consider the more realistic case where parts of the non-determinism are under the control of the environment. A successful realization executes the program and satisfies the temporal goal for all possible environment actions.
• Score: 2.209921757303168
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: Golog is an expressive high-level agent language that includes nondeterministic operators which allow to leave some of the decisions to be made only at execution time. This so-called program realization is typically implemented by means of search, or in an incremental online fashion. In this paper, we consider the more realistic case where parts of the non-determinism are under the control of the environment. Program realization then becomes a synthesis problem, where a successful realization executes the program and satisfies the temporal goal for all possible environment actions. We consider Golog programs in combination with an expressive class of first-order action theories that allow for an unbounded number of objects and non-local effects, together with a temporal goal specified in a first-order extension of LTLf. We solve the synthesis problem by constructing a game arena that captures all possible executions of the program while tracking the satisfaction of the temporal goal and then solving the resulting two-player game. We evaluate the approach in two domains, showing the general feasibility of the approach.

Related papers

• IPSynth: Interprocedural Program Synthesis for Software Security Implementation [3.1119394814248253]
  We introduce IP Synth, a novel inter-procedural program synthesis approach that automatically learns the specification of the tactic. Our results show that our approach can accurately locate corresponding spots in the program, synthesize needed code snippets, add them to the program, and outperform ChatGPT in inter-procedural tactic synthesis tasks.
  arXiv  Detail & Related papers  (2024-03-16T07:12:24Z)
• ExeDec: Execution Decomposition for Compositional Generalization in Neural Program Synthesis [54.18659323181771]
  We characterize several different forms of compositional generalization that are desirable in program synthesis. We propose ExeDec, a novel decomposition-based strategy that predicts execution subgoals to solve problems step-by-step informed by program execution at each step.
  arXiv  Detail & Related papers  (2023-07-26T01:07:52Z)
• Controlling Golog Programs against MTL Constraints [4.56877715768796]
  We present an extension to Golog by clocks together with the required theoretical foundations as well as decidability results. We describe a method to synthesize a controller that executes both the high-level program and the low-level platform operations concurrently.
  arXiv  Detail & Related papers  (2022-04-07T17:16:37Z)
• Searching for More Efficient Dynamic Programs [61.79535031840558]
  We describe a set of program transformations, a simple metric for assessing the efficiency of a transformed program, and a search procedure to improve this metric. We show that in practice, automated search can find substantial improvements to the initial program.
  arXiv  Detail & Related papers  (2021-09-14T20:52:55Z)
• Latent Execution for Neural Program Synthesis Beyond Domain-Specific Languages [97.58968222942173]
  We take the first step to synthesize C programs from input-output examples. In particular, we propose La Synth, which learns the latent representation to approximate the execution of partially generated programs. We show that training on these synthesized programs further improves the prediction performance for both Karel and C program synthesis.
  arXiv  Detail & Related papers  (2021-06-29T02:21:32Z)
• Representing Partial Programs with Blended Abstract Semantics [62.20775388513027]
  We introduce a technique for representing partially written programs in a program synthesis engine. We learn an approximate execution model implemented as a modular neural network. We show that these hybrid neuro-symbolic representations enable execution-guided synthesizers to use more powerful language constructs.
  arXiv  Detail & Related papers  (2020-12-23T20:40:18Z)
• Latent Programmer: Discrete Latent Codes for Program Synthesis [56.37993487589351]
  In many sequence learning tasks, such as program synthesis and document summarization, a key problem is searching over a large space of possible output sequences. We propose to learn representations of the outputs that are specifically meant for search: rich enough to specify the desired output but compact enough to make search more efficient. We introduce the emphLatent Programmer, a program synthesis method that first predicts a discrete latent code from input/output examples, and then generates the program in the target language.
  arXiv  Detail & Related papers  (2020-12-01T10:11:35Z)
• Optimal Neural Program Synthesis from Multimodal Specifications [45.35689345004124]
  Multimodal program synthesis is an attractive way to scale program synthesis to challenging settings. This paper proposes an optimal neural synthesis approach where the goal is to find a program that satisfies user-provided constraints.
  arXiv  Detail & Related papers  (2020-10-04T20:51:21Z)
• BUSTLE: Bottom-Up Program Synthesis Through Learning-Guided Exploration [72.88493072196094]
  We present a new synthesis approach that leverages learning to guide a bottom-up search over programs. In particular, we train a model to prioritize compositions of intermediate values during search conditioned on a set of input-output examples. We show that the combination of learning and bottom-up search is remarkably effective, even with simple supervised learning approaches.
  arXiv  Detail & Related papers  (2020-07-28T17:46:18Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.