Efficient Reactive Synthesis Using Mode Decomposition
- URL: http://arxiv.org/abs/2312.08717v1
- Date: Thu, 14 Dec 2023 08:01:35 GMT
- Title: Efficient Reactive Synthesis Using Mode Decomposition
- Authors: Mat\'ias Brizzio, C\'esar S\'anchez
- Abstract summary: 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.
- Score: 0.0
- License: http://creativecommons.org/licenses/by/4.0/
- Abstract: Developing critical components, such as mission controllers or embedded
systems, is a challenging task. Reactive synthesis is a technique to
automatically produce correct controllers. Given a high-level specification
written in LTL, reactive synthesis consists of computing a system that
satisfies the specification as long as the environment respects the
assumptions. Unfortunately, LTL synthesis suffers from high computational
complexity which precludes its use for many large cases. A promising approach
to improve synthesis scalability consists of decomposing a safety specification
into smaller specifications, that can be processed independently and composed
into a solution for the original specification. Previous decomposition methods
focus on identifying independent parts of the specification whose systems are
combined via simultaneous execution. In this work, we propose a novel
decomposition algorithm based on modes, which consists of decomposing a complex
safety specification into smaller problems whose solution is then composed
sequentially (instead of simultaneously). 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 then the full specification is realizable. Moreover, we show how
to construct a system for the original specification from sub-systems for the
decomposed specifications. We finally illustrate the feasibility of our
approach with multiple case studies using off-the-self synthesis tools to
process the obtained sub-problems.
Related papers
- Predictable and Performant Reactive Synthesis Modulo Theories via Functional Synthesis [1.1797787239802762]
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.
arXiv Detail & Related papers (2024-07-12T15:23:27Z) - CorDA: Context-Oriented Decomposition Adaptation of Large Language Models for Task-Aware Parameter-Efficient Fine-tuning [101.81127587760831]
Current fine-tuning methods build adapters widely of the context of downstream task to learn, or the context of important knowledge to maintain.
We propose CorDA, a Context-oriented Decomposition Adaptation method that builds learnable task-aware adapters.
Our method enables two options, the knowledge-preserved adaptation and the instruction-previewed adaptation.
arXiv Detail & Related papers (2024-06-07T19:10:35Z) - Deep Learning Assisted Multiuser MIMO Load Modulated Systems for
Enhanced Downlink mmWave Communications [68.96633803796003]
This paper is focused on multiuser load modulation arrays (MU-LMAs) which are attractive due to their low system complexity and reduced cost for millimeter wave (mmWave) multi-input multi-output (MIMO) systems.
The existing precoding algorithm for downlink MU-LMA relies on a sub-array structured (SAS) transmitter which may suffer from decreased degrees of freedom and complex system configuration.
In this paper, we conceive an MU-LMA system employing a full-array structured (FAS) transmitter and propose two algorithms accordingly.
arXiv Detail & Related papers (2023-11-08T08:54:56Z) - 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) - 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) - Formal Controller Synthesis for Markov Jump Linear Systems with
Uncertain Dynamics [64.72260320446158]
We propose a method for synthesising controllers for Markov jump linear systems.
Our method is based on a finite-state abstraction that captures both the discrete (mode-jumping) and continuous (stochastic linear) behaviour of the MJLS.
We apply our method to multiple realistic benchmark problems, in particular, a temperature control and an aerial vehicle delivery problem.
arXiv Detail & Related papers (2022-12-01T17:36:30Z) - Compositional Generalization and Decomposition in Neural Program
Synthesis [59.356261137313275]
In this paper, we focus on measuring the ability of learned program synthesizers to compositionally generalize.
We first characterize several different axes along which program synthesis methods would be desired to generalize.
We introduce a benchmark suite of tasks to assess these abilities based on two popular existing datasets.
arXiv Detail & Related papers (2022-04-07T22:16:05Z) - Neural Circuit Synthesis from Specification Patterns [5.7923858184309385]
We train hierarchical Transformers on the task of synthesizing hardware circuits directly out of high-level logical specifications.
New approaches using machine learning might open a lot of possibilities in this area, but suffer from the lack of sufficient amounts of training data.
We show that hierarchical Transformers trained on this synthetic data solve a significant portion of problems from the synthesis competitions.
arXiv Detail & Related papers (2021-07-25T18:17:33Z) - Amortized Synthesis of Constrained Configurations Using a Differentiable
Surrogate [25.125736560730864]
In design, fabrication, and control problems, we are often faced with the task of synthesis.
This many-to-one map presents challenges to the supervised learning of feed-forward synthesis.
We address both of these problems with a two-stage neural network architecture that we may consider to be an autoencoder.
arXiv Detail & Related papers (2021-06-16T17:59:45Z) - Formal Synthesis of Lyapunov Neural Networks [61.79595926825511]
We propose an automatic and formally sound method for synthesising Lyapunov functions.
We employ a counterexample-guided approach where a numerical learner and a symbolic verifier interact to construct provably correct Lyapunov neural networks.
Our method synthesises Lyapunov functions faster and over wider spatial domains than the alternatives, yet providing stronger or equal guarantees.
arXiv Detail & Related papers (2020-03-19T17:21:02Z) - 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)
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.