論文の概要: Efficient Reactive Synthesis Using Mode Decomposition
- arxiv url: http://arxiv.org/abs/2312.08717v1
- Date: Thu, 14 Dec 2023 08:01:35 GMT
- ステータス: 処理完了
- システム内更新日: 2023-12-15 23:32:29.769881
- Title: Efficient Reactive Synthesis Using Mode Decomposition
- Title（参考訳）: モード分解を利用した効率的な反応合成
- Authors: Mat\'ias Brizzio, C\'esar S\'anchez
- Abstract要約: そこで本研究では,モードに基づく新しい分解アルゴリズムを提案する。
我々のアルゴリズムへの入力は、元の仕様とモードの記述である。
サブ仕様の自動生成方法を示し、全てのサブプロブレムが実現可能であれば、完全な仕様が実現可能であることを示す。
- 参考スコア（独自算出の注目度）: 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.
- Abstract（参考訳）: ミッションコントローラや組み込みシステムといった重要なコンポーネントの開発は難しい作業です。
反応合成は、正しいコントローラを自動生成する技術である。
LTLで書かれた高レベル仕様が与えられた場合、リアクティブ合成は、環境が仮定を尊重する限り、仕様を満たすシステムを計算する。
残念ながら、LTL合成は、多くのケースでの使用を妨げる高い計算複雑性に悩まされている。
合成のスケーラビリティを改善するための有望なアプローチは、安全仕様を小さな仕様に分解し、独立して処理し、元の仕様のソリューションを構成することができる。
従来の分解方法は、同時実行によってシステムを構成する仕様の独立した部分を特定することに重点を置いていた。
本研究では,複雑な安全性仕様をより小さな問題に分解し,その解を順次(同時に)構成するモードに基づく新しい分解アルゴリズムを提案する。
我々のアルゴリズムへの入力は、元の仕様とモードの記述である。
サブ仕様の自動生成方法を示し、全てのサブプロブレムが実現可能であれば、完全な仕様が実現可能であることを示す。
さらに,分解仕様のサブシステムから,原仕様のシステムを構築する方法を示す。
最後に, 自己合成ツールを用いて得られたサブプロブレムを処理した複数のケーススタディを用いて, 提案手法の実現可能性を示す。
関連論文リスト
- Automated Placement of Analog Integrated Circuits using Priority-based Constructive Heuristic [0.0]
われわれは,いわゆるポケット,合併の可能性,デバイス間のパラメトリジブルな最小距離を必要とする,特定の種類のアナログ配置に注目した。
我々の解は回路の境界ボックスの周長と近似ワイヤ長を最小化する。
本手法は,手作業による設計を伴い,合成された産業事例と実物実物実物実物実物実物実物実物実物実物実物実物実物実物実物実物実物実物実物実物実物実物実物実物実物実物実物実物実物実物実物実物実物実物実物実物実物実物実物実物実物実物実物実物実物実物実物実物実
論文 参考訳（メタデータ） (2024-10-18T07:16:59Z) - Predictable and Performant Reactive Synthesis Modulo Theories via Functional Synthesis [1.1797787239802762]
本稿では,古典的リアクティブハンドル(命題)を仕様言語として,時間論理仕様から正しいコントローラを生成する方法を示す。
また,制御器が常に最小の安全値を提供するために出力を最適化できるという意味で応答が可能であることを示す。
論文 参考訳（メタデータ） (2024-07-12T15:23:27Z) - CorDA: Context-Oriented Decomposition Adaptation of Large Language Models for Task-Aware Parameter-Efficient Fine-tuning [101.81127587760831]
現在の微調整手法は、学習すべき下流タスクのコンテキストや、維持すべき重要な知識のコンテキストに広く適用できるアダプタを構築している。
学習可能なタスク対応アダプタを構築するコンテキスト指向の分解適応手法であるCorDAを提案する。
本手法は,知識保存型適応と指導レビュー型適応の2つの選択肢を実現する。
論文 参考訳（メタデータ） (2024-06-07T19:10:35Z) - SynthesizRR: Generating Diverse Datasets with Retrieval Augmentation [55.2480439325792]
トピック分類,感情分析,トーン検出,ユーモアの6つのデータセットの合成について検討した。
その結果,SynthesizRRは語彙や意味の多様性,人文との類似性,蒸留性能を大幅に向上させることがわかった。
論文 参考訳（メタデータ） (2024-05-16T12:22:41Z) - Deep Learning Assisted Multiuser MIMO Load Modulated Systems for
Enhanced Downlink mmWave Communications [68.96633803796003]
本稿では, マルチユーザ負荷変調アレイ (MU-LMA) に着目し, マイクロウェーブ (mmWave) マルチインプット・マルチアウトプット (MIMO) システムにおいて, マルチユーザ負荷変調アレイ (MU-LMA) の小型化とコスト削減を図っている。
ダウンリンクMU-LMAの既存のプリコーディングアルゴリズムは、自由度と複雑なシステム構成の低下に悩まされるサブアレイ構造化(SAS)送信機に依存している。
本稿では,FAS (Full-array Structured) 送信機を用いたMU-LMAシステムを提案し,それに応じて2つのアルゴリズムを提案する。
論文 参考訳（メタデータ） (2023-11-08T08:54:56Z) - Synthesizing Efficiently Monitorable Formulas in Metric Temporal Logic [4.60607942851373]
システム実行から形式仕様を自動合成する問題を考察する。
時間論理式を合成するための古典的なアプローチの多くは、公式のサイズを最小化することを目的としている。
我々は,この概念を定式化し,有界な外見を持つ簡潔な公式を合成する学習アルゴリズムを考案する。
論文 参考訳（メタデータ） (2023-10-26T14:13:15Z) - ExeDec: Execution Decomposition for Compositional Generalization in Neural Program Synthesis [54.18659323181771]
プログラム合成において望ましいいくつかの異なる構成一般化形式を特徴付ける。
本稿では,ExeDecを提案する。ExeDecは,実行サブゴールを予測し,各ステップでプログラム実行によって段階的に通知される問題を解くための,新しい分解ベースの戦略である。
論文 参考訳（メタデータ） (2023-07-26T01:07:52Z) - Formal Controller Synthesis for Markov Jump Linear Systems with
Uncertain Dynamics [64.72260320446158]
マルコフジャンプ線形系に対する制御器の合成法を提案する。
本手法は,MJLSの離散(モードジャンピング)と連続(確率線形)の両方の挙動を捉える有限状態抽象化に基づいている。
本手法を複数の現実的なベンチマーク問題,特に温度制御と航空機の配送問題に適用する。
論文 参考訳（メタデータ） (2022-12-01T17:36:30Z) - Compositional Generalization and Decomposition in Neural Program
Synthesis [59.356261137313275]
本稿では,学習プログラムシンセサイザーの合成一般化能力の測定に焦点をあてる。
まず、プログラム合成法が一般化されるであろういくつかの異なる軸を特徴付ける。
2つの一般的な既存のデータセットに基づいて、これらの能力を評価するためのタスクのベンチマークスイートを導入する。
論文 参考訳（メタデータ） (2022-04-07T22:16:05Z) - Amortized Synthesis of Constrained Configurations Using a Differentiable
Surrogate [25.125736560730864]
設計、製造、制御の問題において、我々はしばしば合成の課題に直面している。
この多対一の地図は、フィードフォワード合成の教師あり学習に挑戦する。
どちらの問題にも,オートエンコーダであると考えられる2段階のニューラルネットワークアーキテクチャで対処する。
論文 参考訳（メタデータ） (2021-06-16T17:59:45Z) - Towards Neural-Guided Program Synthesis for Linear Temporal Logic
Specifications [26.547133495699093]
ニューラルネットワークを用いてQ関数を学習し、探索を誘導し、その後正当性を検証したプログラムを構築する。
提案手法は,検索と深層学習を組み合わせることで,合成を実現するのにユニークな手法である。
論文 参考訳（メタデータ） (2019-12-31T17:09:49Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。