論文の概要: Controller Synthesis for Golog Programs over Finite Domains with Metric
Temporal Constraints
- arxiv url: http://arxiv.org/abs/2102.09837v1
- Date: Fri, 19 Feb 2021 10:07:29 GMT
- ステータス: 処理完了
- システム内更新日: 2021-02-22 22:25:07.938027
- Title: Controller Synthesis for Golog Programs over Finite Domains with Metric
Temporal Constraints
- Title(参考訳): 計量時間制約を持つ有限領域上のgologプログラムの制御器合成
- Authors: Till Hofmann and Gerhard Lakemeyer
- Abstract要約: 実際のロボット上でgologプログラムを実行するには、通常、ロボットプラットフォームのハードウェアやソフトウェアの詳細を考慮する追加ステップが必要になる。
本稿では,状況計算の様相変種に基づく制約の定式化について述べる。
有限領域上のプログラムでは、制約を満たしつつ元のプログラムの効果を保ちながらコントローラを合成する問題をMTL合成に還元できることを示した。
- 参考スコア(独自算出の注目度): 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.
- Abstract(参考訳): 実際のロボット上でgologプログラムを実行するには、通常、プログラムの制約として定式化できる、ロボットプラットフォームのハードウェアやソフトウェアの詳細を考慮する追加ステップが必要である。
このような制約はしばしば時間的であり、計量時間を参照し、抽象的なゴーログプログラムを変更する必要がある。
本稿では,状況計算の様相変種に基づく制約の定式化について述べる。
これらの制約は、時間付きオートマトンを用いて記述したプラットフォームモデルと抽象プログラムを結びつける。
有限領域上のプログラムおよび完全に既知の初期状態の場合、元のプログラムの効果を維持しながら制約を満たすコントローラを合成する問題は、MTL合成に還元できることを示した。
私たちは、抽象プログラムからタイムド・オートマトンを構築し、このオートマトン、プラットフォームモデル、および制約からmtlコントローラを合成することでこれを行います。
我々は、合成されたコントローラは、元のプログラムと同じ実行トレース、おそらくプラットフォームに依存したアクションとインターリーブされ、それらがすべての制約を満たすこと、およびそれらが元のプログラムのトレースと同じ効果を有することを証明します。
これにより、元のプログラムを維持しながら、仕様を満たすコントローラを合成するための決定可能な手順を得る。
関連論文リスト
- Defining and executing temporal constraints for evaluating engineering
artifact compliance [56.08728135126139]
プロセスコンプライアンスは、実際のエンジニアリング作業が記述されたエンジニアリングプロセスに可能な限り密接に従うことを保証することに焦点を当てます。
これらのプロセスの制約をチェックすることは、依然として大変な作業であり、多くの手作業を必要とし、プロセスの後半にエンジニアにフィードバックを提供する。
関連するエンジニアリングアーティファクト間の時間的制約を,アーティファクトの変更毎に段階的にチェックする,自動制約チェックアプローチを提案する。
論文 参考訳(メタデータ) (2023-12-20T13:26:31Z) - Synthesizing Efficiently Monitorable Formulas in Metric Temporal Logic [4.60607942851373]
システム実行から形式仕様を自動合成する問題を考察する。
時間論理式を合成するための古典的なアプローチの多くは、公式のサイズを最小化することを目的としている。
我々は,この概念を定式化し,有界な外見を持つ簡潔な公式を合成する学習アルゴリズムを考案する。
論文 参考訳(メタデータ) (2023-10-26T14:13:15Z) - Large Language Models as General Pattern Machines [64.75501424160748]
我々は,事前訓練された大規模言語モデル (LLM) が,複雑なトークンシーケンスを自動回帰的に完了することを示す。
驚いたことに、語彙からランダムにサンプリングされたトークンを用いてシーケンスが表現された場合でも、パターン完了の習熟度を部分的に保持することができる。
本研究では,ロボット工学における問題に対して,これらのゼロショット機能がどのように適用されるかを検討する。
論文 参考訳(メタデータ) (2023-07-10T17:32:13Z) - Hierarchical Neural Program Synthesis [19.94176152035497]
プログラム合成は、与えられたタスク仕様を満たす人間可読プログラムを自動構築することを目的としている。
プログラムを階層的に構成することでプログラムを合成するスケーラブルなプログラム合成フレームワークを提案する。
入力/出力ペアを持つ文字列変換領域において,提案するフレームワークを広範囲に評価する。
論文 参考訳(メタデータ) (2023-03-09T18:20:07Z) - Controlling Golog Programs against MTL Constraints [4.56877715768796]
本稿では、クロックによるGologの拡張と、必要な理論的基礎と決定可能性の結果について述べる。
本稿では,高レベルプログラムと低レベルプラットフォーム操作を同時に実行するコントローラを合成する手法について述べる。
論文 参考訳(メタデータ) (2022-04-07T17:16:37Z) - A Conversational Paradigm for Program Synthesis [110.94409515865867]
本稿では,大規模言語モデルを用いた対話型プログラム合成手法を提案する。
私たちは、自然言語とプログラミング言語のデータに基づいて、CodeGenと呼ばれる大規模な言語モデルのファミリーを訓練します。
本研究は,会話能力の出現と,提案した会話プログラム合成パラダイムの有効性を示すものである。
論文 参考訳(メタデータ) (2022-03-25T06:55:15Z) - Composition Machines: Programming Self-Organising Software Models for
the Emergence of Sequential Program Spaces [0.0]
本稿では,そのようなモデルの定義と実行を可能にする,合成機械と呼ばれる抽象機械を提案する。
一般的な抽象機械とは異なり、提案手法は個々のプログラムを計算せず、一度に複数のプログラムが出現することを可能にする。
論文 参考訳(メタデータ) (2021-08-11T18:39:47Z) - Latent Execution for Neural Program Synthesis Beyond Domain-Specific
Languages [97.58968222942173]
入力出力の例からCプログラムを合成する第一歩を踏み出す。
特に,部分生成プログラムの実行を近似するために潜在表現を学習するLa Synthを提案する。
これらのプログラムのトレーニングにより,Karel と C のプログラム合成における予測性能がさらに向上することを示す。
論文 参考訳(メタデータ) (2021-06-29T02:21:32Z) - Optimal Neural Program Synthesis from Multimodal Specifications [45.35689345004124]
マルチモーダルプログラム合成は、プログラム合成を挑戦的な設定に拡張する魅力的な方法である。
本稿では,ユーザが提供する制約を満たすプログラムを見つけることを目的とした,最適なニューラルシンセサイザー手法を提案する。
論文 参考訳(メタデータ) (2020-10-04T20:51:21Z) - Synthesize, Execute and Debug: Learning to Repair for Neural Program
Synthesis [81.54148730967394]
本稿では,合成,実行,デバッグの段階を組み込んだニューラルネットワーク生成フレームワークであるSEDを提案する。
SEDはまず、神経プログラムシンセサイザーコンポーネントを使用して初期プログラムを生成し、その後、神経プログラムデバッガを使用して生成されたプログラムを反復的に修復する。
挑戦的な入出力プログラム合成ベンチマークであるKarelでは、SEDはニューラルプログラムシンセサイザー自体のエラー率をかなりのマージンで削減し、デコードのための標準ビームサーチより優れている。
論文 参考訳(メタデータ) (2020-07-16T04:15:47Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト(すべての情報・翻訳含む)の品質を保証せず、本サイト(すべての情報・翻訳含む)を使用して発生したあらゆる結果について一切の責任を負いません。