論文の概要: 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用の既存のオートマトン生成ツールよりも優れたスケーラビリティを提供することを示す。

関連論文リスト

• LLM-based Optimization of Compound AI Systems: A Survey [64.39860384538338]
  複合AIシステムでは、LLMコール、レトリバー、コードインタプリタ、ツールなどのコンポーネントが相互接続される。 近年の進歩により, LLM を用いたパラメータのエンドツーエンド最適化が可能となった。 本稿では,複合AIシステムのLCMに基づく最適化の原理と動向について述べる。
  論文  参考訳（メタデータ） (2024-10-21T18:06:25Z)
• Tractable Offline Learning of Regular Decision Processes [50.11277112628193]
  この研究は、正則決定過程(RDP)と呼ばれる非マルコフ環境のクラスにおけるオフライン強化学習(RL)を研究する。 インスは、未来の観測と過去の相互作用からの報酬の未知の依存を実験的に捉えることができる。 多くのアルゴリズムは、まずこの未知の依存関係を自動学習技術を用いて再構築する。
  論文  参考訳（メタデータ） (2024-09-04T14:26:58Z)
• Directed Exploration in Reinforcement Learning from Linear Temporal Logic [59.707408697394534]
  リニア時間論理(LTL)は強化学習におけるタスク仕様のための強力な言語である。 合成された報酬信号は基本的に疎結合であり,探索が困難であることを示す。 我々は、仕様をさらに活用し、それに対応するリミット決定性B"uchi Automaton(LDBA)をマルコフ報酬プロセスとしてキャストすることで、よりよい探索を実現することができることを示す。
  論文  参考訳（メタデータ） (2024-08-18T14:25:44Z)
• Predictable and Performant Reactive Synthesis Modulo Theories via Functional Synthesis [1.1797787239802762]
  本稿では,古典的リアクティブハンドル(命題)を仕様言語として,時間論理仕様から正しいコントローラを生成する方法を示す。 また,制御器が常に最小の安全値を提供するために出力を最適化できるという意味で応答が可能であることを示す。
  論文  参考訳（メタデータ） (2024-07-12T15:23:27Z)
• Two-Stage ML-Guided Decision Rules for Sequential Decision Making under Uncertainty [55.06411438416805]
  SDMU (Sequential Decision Making Under Uncertainty) は、エネルギー、金融、サプライチェーンといった多くの領域において、ユビキタスである。 いくつかのSDMUは、自然にマルチステージ問題(MSP)としてモデル化されているが、結果として得られる最適化は、計算の観点からは明らかに困難である。 本稿では,2段階の一般決定規則(TS-GDR)を導入し,線形関数を超えて政策空間を一般化する手法を提案する。 TS-GDRの有効性は、TS-LDR(Two-Stage Deep Decision Rules)と呼ばれるディープリカレントニューラルネットワークを用いたインスタンス化によって実証される。
  論文  参考訳（メタデータ） (2024-05-23T18:19:47Z)
• Linear Temporal Logic Modulo Theories over Finite Traces (Extended Version) [72.38188258853155]
  有限トレース(LTLf)上の線形時間論理について検討する。 命題の文字は任意の理論で解釈された一階述語式に置き換えられる。 Satisfiability Modulo Theories (LTLfMT) と呼ばれる結果の論理は半決定可能である。
  論文  参考訳（メタデータ） (2022-04-28T17:57:33Z)
• 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)

関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。

指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。