Predictable and Performant Reactive Synthesis Modulo Theories via Functional Synthesis

• URL: http://arxiv.org/abs/2407.09348v1
• Date: Fri, 12 Jul 2024 15:23:27 GMT
• Title: Predictable and Performant Reactive Synthesis Modulo Theories via Functional Synthesis
• Authors: Andoni Rodríguez, Felipe Gorostiaga, César Sánchez,
• Abstract summary: We show how to generate correct controllers from temporal logic specifications using classical reactive handles (propositional) as a specification language. We also show that our method allows responses in the sense that the controller can optimize its outputs in order to always provide the smallest safe values.
• Score: 1.1797787239802762
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: Reactive synthesis is the process of generating correct controllers from temporal logic specifications. Classical LTL reactive synthesis handles (propositional) LTL as a specification language. Boolean abstractions allow reducing LTLt specifications (i.e., LTL with propositions replaced by literals from a theory calT), into equi-realizable LTL specifications. In this paper we extend these results into a full static synthesis procedure. The synthesized system receives from the environment valuations of variables from a rich theory calT and outputs valuations of system variables from calT. We use the abstraction method to synthesize a reactive Boolean controller from the LTL specification, and we combine it with functional synthesis to obtain a static controller for the original LTLt specification. We also show that our method allows responses in the sense that the controller can optimize its outputs in order to e.g., always provide the smallest safe values. This is the first full static synthesis method for LTLt, which is a deterministic program (hence predictable and efficient).

Related papers

• LTLf+ and PPLTL+: Extending LTLf and PPLTL to Infinite Traces [44.35335751462176]
  DFA-based synthesis techniques for automatf+/PPLTL+ are presented. We show that the full expressive power of PPLTL+ is EXPTIME-complete instead of 2EXPTIME-complete.
  arXiv  Detail & Related papers  (2024-11-14T11:17:06Z)
• SynthesizRR: Generating Diverse Datasets with Retrieval Augmentation [55.2480439325792]
  We study the synthesis of six datasets, covering topic classification, sentiment analysis, tone detection, and humor. We find that SynthesizRR greatly improves lexical and semantic diversity, similarity to human-written text, and distillation performance.
  arXiv  Detail & Related papers  (2024-05-16T12:22:41Z)
• Guiding Enumerative Program Synthesis with Large Language Models [15.500250058226474]
  In this paper, we evaluate the abilities of Large Language Models to solve formal synthesis benchmarks. When one-shot synthesis fails, we propose a novel enumerative synthesis algorithm. We find that GPT-3.5 as a stand-alone tool for formal synthesis is easily outperformed by state-of-the-art formal synthesis algorithms.
  arXiv  Detail & Related papers  (2024-03-06T19:13:53Z)
• Efficient Reactive Synthesis Using Mode Decomposition [0.0]
  We propose a novel decomposition algorithm based on modes. The input to our algorithm is the original specification and the description of the modes. We show how to generate sub-specifications automatically and we prove that if all sub-problems are realizable the full specification is realizable.
  arXiv  Detail & Related papers  (2023-12-14T08:01:35Z)
• Decidable Fragments of LTLf Modulo Theories (Extended Version) [66.25779635347122]
  In general,fMT was shown to be semi-decidable for any decidable first-order theory (e.g., linear arithmetics) with a tableau-based semi-decision procedure. We show that for anyfMT formula satisfies an abstract, semantic condition, that we call finite memory, the tableau augmented with a new rule is also guaranteed to terminate.
  arXiv  Detail & Related papers  (2023-07-31T17:02:23Z)
• Model Checking Strategies from Synthesis Over Finite Traces [25.871354900295056]
  For model checking, two types of transducers are fundamentally different. We show that for model checking of non-terminating transducers is emphexponentially harder than that of terminating transducers.
  arXiv  Detail & Related papers  (2023-05-15T03:09:20Z)
• Learning Bounded Context-Free-Grammar via LSTM and the Transformer:Difference and Explanations [51.77000472945441]
  Long Short-Term Memory (LSTM) and Transformers are two popular neural architectures used for natural language processing tasks. In practice, it is often observed that Transformer models have better representation power than LSTM. We study such practical differences between LSTM and Transformer and propose an explanation based on their latent space decomposition patterns.
  arXiv  Detail & Related papers  (2021-12-16T19:56:44Z)
• LTLf Synthesis on Probabilistic Systems [0.0]
  synthesis is used to find a policy that maximizes the probability of achieving this behavior. No tools exist to solve policy synthesis for behaviors given finite-trace properties. We present two algorithms for solving this problem: the first via reduction of Markov Processes and the second native tools for automatonf.
  arXiv  Detail & Related papers  (2020-09-23T01:26:47Z)
• Automated and Sound Synthesis of Lyapunov Functions with SMT Solvers [70.70479436076238]
  We synthesise Lyapunov functions for linear, non-linear (polynomial) and parametric models. We exploit an inductive framework to synthesise Lyapunov functions, starting from parametric templates.
  arXiv  Detail & Related papers  (2020-07-21T14:45:23Z)
• Towards Neural-Guided Program Synthesis for Linear Temporal Logic Specifications [26.547133495699093]
  We use a neural network to learn a Q-function that is then used to guide search, and to construct programs that are subsequently verified for correctness. Our method is unique in combining search with deep learning to realize synthesis.
  arXiv  Detail & Related papers  (2019-12-31T17:09:49Z)
• Certified Reinforcement Learning with Logic Guidance [78.2286146954051]
  We propose a model-free RL algorithm that enables the use of Linear Temporal Logic (LTL) to formulate a goal for unknown continuous-state/action Markov Decision Processes (MDPs) The algorithm is guaranteed to synthesise a control policy whose traces satisfy the specification with maximal probability.
  arXiv  Detail & Related papers  (2019-02-02T20:09:32Z)

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.