論文の概要: Decidable Fragments of LTLf Modulo Theories (Extended Version)

• arxiv url: http://arxiv.org/abs/2307.16840v1
• Date: Mon, 31 Jul 2023 17:02:23 GMT
• ステータス: 処理完了
• システム内更新日: 2023-08-01 13:21:23.382386
• Title: Decidable Fragments of LTLf Modulo Theories (Extended Version)
• Title（参考訳）: LTLfモデュロ理論の決定可能なフラグメント(拡張版)
• Authors: Luca Geatti and Alessandro Gianola and Nicola Gigante and Sarah Winkler
• Abstract要約: 一般に、fMTは、任意の決定可能な一階述語理論(例えば、線形算術)に対して、テーブルーベースの半決定手順で半決定可能であることが示されている。 有限メモリと呼ぶ抽象的意味条件を満たす任意のfMT式に対して、新しい規則で拡張されたテーブルーもまた終了することが保証されていることを示す。
• 参考スコア（独自算出の注目度）: 66.25779635347122
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: We study Linear Temporal Logic Modulo Theories over Finite Traces (LTLfMT), a recently introduced extension of LTL over finite traces (LTLf) where propositions are replaced by first-order formulas and where first-order variables referring to different time points can be compared. In general, LTLfMT was shown to be semi-decidable for any decidable first-order theory (e.g., linear arithmetics), with a tableau-based semi-decision procedure. In this paper we present a sound and complete pruning rule for the LTLfMT tableau. We show that for any LTLfMT formula that satisfies an abstract, semantic condition, that we call finite memory, the tableau augmented with the new rule is also guaranteed to terminate. Last but not least, this technique allows us to establish novel decidability results for the satisfiability of several fragments of LTLfMT, as well as to give new decidability proofs for classes that are already known.
• Abstract（参考訳）: 最近導入された有限トレース(LTLf)上のLTLの拡張である有限トレース(LTLfMT)上の線形時相論理モデュロ理論(LTLfMT)について検討し、命題を1次式に置き換え、異なる時間点を参照する1次変数を比較する。 一般に、ltlfmt は任意の決定可能な一階理論(例えば線形算術)に対して半決定可能であることが示され、tableau ベースの半決定手続きを持つ。 本稿では,LTLfMTテーブルーの音響および完全プルーニング規則を提案する。 有限メモリと呼ぶ抽象的意味条件を満たす LTLfMT の公式に対して、新しい規則で拡張されたテーブルーもまた終了することが保証されていることを示す。 最後に、この手法により、LTLfMTのいくつかのフラグメントが満足できるような新しい決定可能性結果を確立し、既に知られているクラスに対して新しい決定性証明を行うことができる。

関連論文リスト

• Alchemy: Amplifying Theorem-Proving Capability through Symbolic Mutation [71.32761934724867]
  この研究は、記号的突然変異を通じて形式的な定理を構成するデータ合成のフレームワークであるAlchemyを提案する。 マドリブにおける各候補定理について、書き直しや適用に使用できるすべてのイベーシブルな定理を同定する。 その結果、マドリブの定理の数は110kから6Mへと桁違いに増加する。
  論文  参考訳（メタデータ） (2024-10-21T08:04:21Z)
• DeepLTL: Learning to Efficiently Satisfy Complex LTL Specifications [59.01527054553122]
  リニア時間論理(LTL)は、強化学習(RL)における複雑で時間的に拡張されたタスクを特定する強力なフォーマリズムとして最近採用されている。 既存のアプローチはいくつかの欠点に悩まされており、それらは有限水平フラグメントにのみ適用でき、最適以下の解に制限され、安全制約を適切に扱えない。 本研究では,これらの問題に対処するための新しい学習手法を提案する。 提案手法は, 自動仕様のセマンティクスを明示的に表現したB"uchiaの構造を利用して, 所望の式を満たすための真理代入の順序を条件としたポリシーを学習する。
  論文  参考訳（メタデータ） (2024-10-06T21:30:38Z)
• Directed Exploration in Reinforcement Learning from Linear Temporal Logic [59.707408697394534]
  リニア時間論理(LTL)は強化学習におけるタスク仕様のための強力な言語である。 合成された報酬信号は基本的に疎結合であり,探索が困難であることを示す。 我々は、仕様をさらに活用し、それに対応するリミット決定性B"uchi Automaton(LDBA)をマルコフ報酬プロセスとしてキャストすることで、よりよい探索を実現することができることを示す。
  論文  参考訳（メタデータ） (2024-08-18T14:25:44Z)
• Independent Component Alignment for Multi-Task Learning [2.5234156040689237]
  マルチタスク学習(MTL)では、複数のタスクに共同で取り組むために単一のモデルを訓練する。 MTL最適化の安定性基準として線形勾配系の条件数を用いる。 本稿では,提案基準に基づく新しいMTL最適化手法であるAligned-MTLを提案する。
  論文  参考訳（メタデータ） (2023-05-30T12:56:36Z)
• 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)
• LTLf Synthesis on Probabilistic Systems [0.0]
  合成は、この行動を達成する確率を最大化するポリシーを見つけるために用いられる。 有限トレース特性を与えられた振る舞いに対するポリシー合成を解くための道具は存在しない。 本稿では,マルコフプロセスの削減による2つの問題を解決するアルゴリズムと,オートマトンフのための2番目のネイティブツールを提案する。
  論文  参考訳（メタデータ） (2020-09-23T01:26:47Z)
• What to Do When You Can't Do It All: Temporal Logic Planning with Soft Temporal Logic Constraints [28.072597424460472]
  ソフト仕様の集合から最適な選択を満足する無限軌跡を見つけることを目的とした時間論理計画問題を考える。 提案アルゴリズムはまず,計画問題を最小限のコストで計算できる製品を構築する。 このような短いラッソを計算することは難しいが、短いラッソを合成するための効率的なグリージーなアプローチも導入する。
  論文  参考訳（メタデータ） (2020-08-05T04:18:59Z)
• A Generic First-Order Algorithmic Framework for Bi-Level Programming Beyond Lower-Level Singleton [49.23948907229656]
  Bi-level Descent Aggregationは、汎用的な双方向最適化のためのフレキシブルでモジュール化されたアルゴリズムフレームワークである。 LLS条件なしでBDAの収束を証明する新しい手法を導出する。 我々の研究は、BDAが特定の一階計算モジュールの検証と互換性があることも示している。
  論文  参考訳（メタデータ） (2020-06-07T05:18:50Z)

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

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