論文の概要: Computing unsatisfiable cores for LTLf specifications

• arxiv url: http://arxiv.org/abs/2203.04834v1
• Date: Wed, 9 Mar 2022 16:08:43 GMT
• ステータス: 処理完了
• システム内更新日: 2022-03-10 20:39:34.870472
• Title: Computing unsatisfiable cores for LTLf specifications
• Title（参考訳）: LTLf仕様に対する不満足なコアの計算
• Authors: Marco Roveri and Claudio Di Ciccio and Chiara Di Francescomarino and Chiara Ghidini
• Abstract要約: 有限トレース上の線形時間時間時間論理(LTLf)は、多くのアプリケーション領域で仕様を作成するためのデファクト標準になりつつある。 満足度チェックのための最先端手法を用いて、不満足なコアを抽出する4つのアルゴリズムを提案する。 結果は、異なるアルゴリズムやツールの実現可能性、有効性、相補性を示している。
• 参考スコア（独自算出の注目度）: 3.251765107970636
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: Linear-time temporal logic on finite traces (LTLf) is rapidly becoming a de-facto standard to produce specifications in many application domains (e.g., planning, business process management, run-time monitoring, reactive synthesis). Several studies approached the respective satisfiability problem. In this paper, we investigate the problem of extracting the unsatisfiable core in LTLf specifications. We provide four algorithms for extracting an unsatisfiable core leveraging the adaptation of state-of-the-art approaches to LTLf satisfiability checking. We implement the different approaches within the respective tools and carry out an experimental evaluation on a set of reference benchmarks, restricting to the unsatisfiable ones. The results show the feasibility, effectiveness, and complementarities of the different algorithms and tools.
• Abstract（参考訳）: 有限トレース(ltlf: linear-time temporal logic on finite traces)は、多くのアプリケーションドメイン(例えば、計画、ビジネスプロセス管理、実行時のモニタリング、リアクティブ合成)で仕様を作成するためのデファクトスタンダードになりつつある。 いくつかの研究がそれぞれの満足度問題にアプローチした。 本稿では,LTLf仕様における不満足なコア抽出の問題について検討する。 LTLfの適合性チェックへの最先端アプローチの適応を利用して、不満足なコアを抽出する4つのアルゴリズムを提案する。 それぞれのツールに異なるアプローチを実装し、一連の基準ベンチマークで実験的な評価を行い、満足できないものに制限する。 結果は、異なるアルゴリズムやツールの実現可能性、有効性、相補性を示している。

関連論文リスト

• Time-Series Forecasting in Smart Manufacturing Systems: An Experimental Evaluation of the State-of-the-art Algorithms [0.0]
  TSFは製造を含む様々な領域で成長している。 本研究の目的は、13の製造データセット上でのSoTA TSFアルゴリズムの評価により、このギャップを埋めることである。
  論文  参考訳（メタデータ） (2024-11-26T15:10:31Z)
• Benchmarking Agentic Workflow Generation [80.74757493266057]
  複数面シナリオと複雑なグラフワークフロー構造を備えた統合ワークフロー生成ベンチマークであるWorFBenchを紹介する。 また,サブシーケンスとサブグラフマッチングアルゴリズムを利用したシステム評価プロトコルWorFEvalを提案する。 我々は、生成されたタスクが下流のタスクを強化し、推論中により少ない時間で優れたパフォーマンスを達成することができることを観察する。
  論文  参考訳（メタデータ） (2024-10-10T12:41:19Z)
• 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)
• TSI-Bench: Benchmarking Time Series Imputation [52.27004336123575]
  TSI-Benchは、ディープラーニング技術を利用した時系列計算のための総合ベンチマークスイートである。 TSI-Benchパイプラインは、実験的な設定を標準化し、計算アルゴリズムの公平な評価を可能にする。 TSI-Benchは、計算目的のために時系列予測アルゴリズムを調整するための体系的なパラダイムを革新的に提供する。
  論文  参考訳（メタデータ） (2024-06-18T16:07:33Z)
• Policy Optimization with Linear Temporal Logic Constraints [37.27882290236194]
  本稿では,線形時間論理制約を用いた政策最適化の問題点について考察する。 我々は,タスク満足度とコスト最適性の両方を保証するために,サンプル複雑性分析を楽しむモデルベースアプローチを開発した。
  論文  参考訳（メタデータ） (2022-06-20T02:58:02Z)
• Exploring Viable Algorithmic Options for Learning from Demonstration (LfD): A Parameterized Complexity Approach [0.0]
  本稿では,パラメータ化複雑性解析を用いて,アルゴリズムの選択肢を体系的に探索する方法を示す。 環境、実演、ポリシーに対する多くの(しばしば同時に)制限に対して、我々の問題は、一般的にも、あるいは相対的に、効率的に解決できないことを示す。
  論文  参考訳（メタデータ） (2022-05-10T15:54:06Z)
• Linear Temporal Logic Modulo Theories over Finite Traces (Extended Version) [72.38188258853155]
  有限トレース(LTLf)上の線形時間論理について検討する。 命題の文字は任意の理論で解釈された一階述語式に置き換えられる。 Satisfiability Modulo Theories (LTLfMT) と呼ばれる結果の論理は半決定可能である。
  論文  参考訳（メタデータ） (2022-04-28T17:57:33Z)
• Certified Reinforcement Learning with Logic Guidance [78.2286146954051]
  線形時間論理(LTL)を用いて未知の連続状態/動作マルコフ決定過程(MDP)のゴールを定式化できるモデルフリーなRLアルゴリズムを提案する。 このアルゴリズムは、トレースが仕様を最大確率で満たす制御ポリシーを合成することが保証される。
  論文  参考訳（メタデータ） (2019-02-02T20:09:32Z)

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

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