Controller Synthesis for Golog Programs over Finite Domains with Metric Temporal Constraints

• URL: http://arxiv.org/abs/2102.09837v1
• Date: Fri, 19 Feb 2021 10:07:29 GMT
• Title: Controller Synthesis for Golog Programs over Finite Domains with Metric Temporal Constraints
• Authors: Till Hofmann and Gerhard Lakemeyer
• Abstract summary: Executing a Golog program on an actual robot typically requires additional steps to account for hardware or software details of the robot platform. We describe how to formulate such constraints based on a modal variant of the Situation Calculus. We show that for programs over finite domains, the problem of synthesizing a controller that satisfies the constraints while preserving the effects of the original program can be reduced to MTL synthesis.
• Score: 5.254093731341154
• License: http://creativecommons.org/licenses/by-sa/4.0/
• Abstract: Executing a Golog program on an actual robot typically requires additional steps to account for hardware or software details of the robot platform, which can be formulated as constraints on the program. Such constraints are often temporal, refer to metric time, and require modifications to the abstract Golog program. We describe how to formulate such constraints based on a modal variant of the Situation Calculus. These constraints connect the abstract program with the platform models, which we describe using timed automata. We show that for programs over finite domains and with fully known initial state, the problem of synthesizing a controller that satisfies the constraints while preserving the effects of the original program can be reduced to MTL synthesis. We do this by constructing a timed automaton from the abstract program and synthesizing an MTL controller from this automaton, the platform models, and the constraints. We prove that the synthesized controller results in execution traces which are the same as those of the original program, possibly interleaved with platform-dependent actions, that they satisfy all constraints, and that they have the same effects as the traces of the original program. By doing so, we obtain a decidable procedure to synthesize a controller that satisfies the specification while preserving the original program.

Related papers

• Defining and executing temporal constraints for evaluating engineering artifact compliance [56.08728135126139]
  Process compliance focuses on ensuring that the actual engineering work is followed as closely as possible to the described engineering processes. Checking these process constraints is still a daunting task that requires a lot of manual work and delivers feedback to engineers only late in the process. We present an automated constraint checking approach that can incrementally check temporal constraints across inter-related engineering artifacts upon every artifact change.
  arXiv  Detail & Related papers  (2023-12-20T13:26:31Z)
• Synthesizing Efficiently Monitorable Formulas in Metric Temporal Logic [4.60607942851373]
  We consider the problem of automatically synthesizing formal specifications from system executions. Most of the classical approaches for synthesizing temporal logic formulas aim at minimizing the size of the formula. We formalize this notion and devise a learning algorithm that synthesizes concise formulas having bounded lookahead.
  arXiv  Detail & Related papers  (2023-10-26T14:13:15Z)
• Large Language Models as General Pattern Machines [64.75501424160748]
  We show that pre-trained large language models (LLMs) are capable of autoregressively completing complex token sequences. Surprisingly, pattern completion proficiency can be partially retained even when the sequences are expressed using tokens randomly sampled from the vocabulary. In this work, we investigate how these zero-shot capabilities may be applied to problems in robotics.
  arXiv  Detail & Related papers  (2023-07-10T17:32:13Z)
• Hierarchical Neural Program Synthesis [19.94176152035497]
  Program synthesis aims to automatically construct human-readable programs that satisfy given task specifications. We present a scalable program synthesis framework that instead synthesizes a program by hierarchically composing programs. We extensively evaluate our proposed framework in a string transformation domain with input/output pairs.
  arXiv  Detail & Related papers  (2023-03-09T18:20:07Z)
• 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)
• A Conversational Paradigm for Program Synthesis [110.94409515865867]
  We propose a conversational program synthesis approach via large language models. We train a family of large language models, called CodeGen, on natural language and programming language data. Our findings show the emergence of conversational capabilities and the effectiveness of the proposed conversational program synthesis paradigm.
  arXiv  Detail & Related papers  (2022-03-25T06:55:15Z)
• Composition Machines: Programming Self-Organising Software Models for the Emergence of Sequential Program Spaces [0.0]
  We propose an abstract machine, called the composition machine, which allows the definition and the execution of such models. Unlike typical abstract machines, our proposal does not compute individual programs but enables the emergence of multiple programs at once.
  arXiv  Detail & Related papers  (2021-08-11T18:39:47Z)
• 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)
• 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)
• Synthesize, Execute and Debug: Learning to Repair for Neural Program Synthesis [81.54148730967394]
  We propose SED, a neural program generation framework that incorporates synthesis, execution, and debug stages. SED first produces initial programs using the neural program synthesizer component, then utilizes a neural program debugger to iteratively repair the generated programs. On Karel, a challenging input-output program synthesis benchmark, SED reduces the error rate of the neural program synthesizer itself by a considerable margin, and outperforms the standard beam search for decoding.
  arXiv  Detail & Related papers  (2020-07-16T04:15:47Z)

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.