論文の概要: LTLf Synthesis on Probabilistic Systems
- arxiv url: http://arxiv.org/abs/2009.10883v1
- Date: Wed, 23 Sep 2020 01:26:47 GMT
- ステータス: 処理完了
- システム内更新日: 2022-10-15 16:28:02.192812
- Title: LTLf Synthesis on Probabilistic Systems
- Title(参考訳): 確率システムのLTLf合成
- Authors: Andrew M. Wells (Rice University), Morteza Lahijanian (University of
Colorado at Boulder), Lydia E. Kavraki (Rice University), Moshe Y. Vardi
(Rice University)
- Abstract要約: 合成は、この行動を達成する確率を最大化するポリシーを見つけるために用いられる。
有限トレース特性を与えられた振る舞いに対するポリシー合成を解くための道具は存在しない。
本稿では,マルコフプロセスの削減による2つの問題を解決するアルゴリズムと,オートマトンフのための2番目のネイティブツールを提案する。
- 参考スコア(独自算出の注目度): 0.0
- License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
- Abstract: Many systems are naturally modeled as Markov Decision Processes (MDPs),
combining probabilities and strategic actions. Given a model of a system as an
MDP and some logical specification of system behavior, the goal of synthesis is
to find a policy that maximizes the probability of achieving this behavior. A
popular choice for defining behaviors is Linear Temporal Logic (LTL). Policy
synthesis on MDPs for properties specified in LTL has been well studied. LTL,
however, is defined over infinite traces, while many properties of interest are
inherently finite. Linear Temporal Logic over finite traces (LTLf) has been
used to express such properties, but no tools exist to solve policy synthesis
for MDP behaviors given finite-trace properties. We present two algorithms for
solving this synthesis problem: the first via reduction of LTLf to LTL and the
second using native tools for LTLf. We compare the scalability of these two
approaches for synthesis and show that the native approach offers better
scalability compared to existing automaton generation tools for LTL.
- Abstract(参考訳): 多くのシステムは自然にマルコフ決定過程 (mdps) としてモデル化され、確率と戦略行動を組み合わせる。
MDPとしてのシステムのモデルとシステム行動の論理的仕様が与えられた場合、合成の目標は、この行動を達成する確率を最大化するポリシーを見つけることである。
振る舞いを定義するための一般的な選択はLTL(Linear Temporal Logic)である。
LTLで特定された特性に対するMDPの政策合成はよく研究されている。
しかし LTL は無限のトレース上で定義されるが、興味のある性質の多くは本質的に有限である。
有限トレース(ltlf)上の線形時相論理は、そのような特性を表現するために用いられてきたが、有限トレース特性を与えるmdp動作のポリシー合成のツールは存在しない。
本稿では,LTLfをLTLに還元した第1のアルゴリズムと,LTLfのネイティブツールを用いた第2のアルゴリズムを提案する。
これら2つのアプローチのスケーラビリティを比較して,ネイティブアプローチがltl用の既存のオートマトン生成ツールよりも優れたスケーラビリティを提供することを示す。
関連論文リスト
- Synthesizing Efficiently Monitorable Formulas in Metric Temporal Logic [4.60607942851373]
システム実行から形式仕様を自動合成する問題を考察する。
時間論理式を合成するための古典的なアプローチの多くは、公式のサイズを最小化することを目的としている。
我々は,この概念を定式化し,有界な外見を持つ簡潔な公式を合成する学習アルゴリズムを考案する。
論文 参考訳(メタデータ) (2023-10-26T14:13:15Z) - Maximize to Explore: One Objective Function Fusing Estimation, Planning,
and Exploration [87.53543137162488]
我々はtextttMEX というオンライン強化学習(オンラインRL)フレームワークを提案する。
textttMEXは、自動的に探索エクスプロイトのバランスをとりながら、見積もりと計画コンポーネントを統合する。
様々な MuJoCo 環境では,ベースラインを安定的なマージンで上回り,十分な報酬を得られる。
論文 参考訳(メタデータ) (2023-05-29T17:25:26Z) - MULTIGAIN 2.0: MDP controller synthesis for multiple mean-payoff, LTL
and steady-state constraints [58.720142291102135]
我々は、コントローラ合成ツールMultiGainのメジャー拡張であるMultiGAIN 2.0を提案する。
この新バージョンはMultiGainの多目的能力を拡張し、確率システムのコントローラの形式的検証と合成を可能にする。
論文 参考訳(メタデータ) (2023-05-26T08:59:51Z) - Formal Controller Synthesis for Markov Jump Linear Systems with
Uncertain Dynamics [64.72260320446158]
マルコフジャンプ線形系に対する制御器の合成法を提案する。
本手法は,MJLSの離散(モードジャンピング)と連続(確率線形)の両方の挙動を捉える有限状態抽象化に基づいている。
本手法を複数の現実的なベンチマーク問題,特に温度制御と航空機の配送問題に適用する。
論文 参考訳(メタデータ) (2022-12-01T17:36:30Z) - Linear Temporal Logic Modulo Theories over Finite Traces (Extended
Version) [72.38188258853155]
有限トレース(LTLf)上の線形時間論理について検討する。
命題の文字は任意の理論で解釈された一階述語式に置き換えられる。
Satisfiability Modulo Theories (LTLfMT) と呼ばれる結果の論理は半決定可能である。
論文 参考訳(メタデータ) (2022-04-28T17:57:33Z) - Symbolic Learning to Optimize: Towards Interpretability and Scalability [113.23813868412954]
近年のL2O(Learning to Optimize)研究は,複雑なタスクに対する最適化手順の自動化と高速化に期待できる道のりを示唆している。
既存のL2Oモデルは、ニューラルネットワークによる最適化ルールをパラメータ化し、メタトレーニングを通じてそれらの数値ルールを学ぶ。
本稿では,L2Oの総合的な記号表現と解析の枠組みを確立する。
そこで本稿では,大規模問題にメタトレーニングを施す軽量なL2Oモデルを提案する。
論文 参考訳(メタデータ) (2022-03-13T06:04:25Z) - LTL-Constrained Steady-State Policy Synthesis [0.0]
マルコフ決定プロセス(MDP)とこれらすべての型を組み合わせた仕様について検討する。
マルチタイプの仕様を多次元の長期平均報酬に還元する統合ソリューションを提供する。
このアルゴリズムは一般の$omega$-regularプロパティにも拡張され、LDBAと同様にMDPのサイズで実行されます。
論文 参考訳(メタデータ) (2021-05-31T11:35:42Z) - Reinforcement Learning Based Temporal Logic Control with Maximum
Probabilistic Satisfaction [5.337302350000984]
本稿では,制御ポリシを合成するモデルレス強化学習アルゴリズムを提案する。
RLをベースとした制御合成の有効性をシミュレーションおよび実験により実証した。
論文 参考訳(メタデータ) (2020-10-14T03:49:16Z) - Towards Neural-Guided Program Synthesis for Linear Temporal Logic
Specifications [26.547133495699093]
ニューラルネットワークを用いてQ関数を学習し、探索を誘導し、その後正当性を検証したプログラムを構築する。
提案手法は,検索と深層学習を組み合わせることで,合成を実現するのにユニークな手法である。
論文 参考訳(メタデータ) (2019-12-31T17:09:49Z) - Certified Reinforcement Learning with Logic Guidance [78.2286146954051]
線形時間論理(LTL)を用いて未知の連続状態/動作マルコフ決定過程(MDP)のゴールを定式化できるモデルフリーなRLアルゴリズムを提案する。
このアルゴリズムは、トレースが仕様を最大確率で満たす制御ポリシーを合成することが保証される。
論文 参考訳(メタデータ) (2019-02-02T20:09:32Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト(すべての情報・翻訳含む)の品質を保証せず、本サイト(すべての情報・翻訳含む)を使用して発生したあらゆる結果について一切の責任を負いません。