論文の概要: Linear Temporal Logic Modulo Theories over Finite Traces (Extended Version)

• arxiv url: http://arxiv.org/abs/2204.13693v1
• Date: Thu, 28 Apr 2022 17:57:33 GMT
• ステータス: 処理完了
• システム内更新日: 2022-04-29 14:56:22.431686
• Title: Linear Temporal Logic Modulo Theories over Finite Traces (Extended Version)
• Title（参考訳）: 有限トレース上の線形時間論理モデュロ理論(拡張版)
• Authors: Luca Geatti, Alessandro Gianola and Nicola Gigante
• Abstract要約: 有限トレース(LTLf)上の線形時間論理について検討する。 命題の文字は任意の理論で解釈された一階述語式に置き換えられる。 Satisfiability Modulo Theories (LTLfMT) と呼ばれる結果の論理は半決定可能である。
• 参考スコア（独自算出の注目度）: 72.38188258853155
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: This paper studies Linear Temporal Logic over Finite Traces (LTLf) where proposition letters are replaced with first-order formulas interpreted over arbitrary theories, in the spirit of Satisfiability Modulo Theories. The resulting logic, called LTLf Modulo Theories (LTLfMT), is semi-decidable. Nevertheless, its high expressiveness comes useful in a number of use cases, such as model-checking of data-aware processes and data-aware planning. Despite the general undecidability of these problems, being able to solve satisfiable instances is a compromise worth studying. After motivating and describing such use cases, we provide a sound and complete semi-decision procedure for LTLfMT based on the SMT encoding of a one-pass tree-shaped tableau system. The algorithm is implemented in the BLACK satisfiability checking tool, and an experimental evaluation shows the feasibility of the approach on novel benchmarks.
• Abstract（参考訳）: 本稿では,任意の理論上で解釈された一階公式に命題文字が置き換えられる有限トレース(ltlf)上の線形時相論理について,満足性モジュラー理論の精神を用いて検討する。 結果として得られる論理は LTLf Modulo Theories (LTLfMT) と呼ばれ、半決定可能である。 それでも、その高い表現力は、データ認識プロセスのモデルチェックやデータ認識計画など、多くのユースケースで有用である。 これらの問題の一般的な不決定性にもかかわらず、満足できる事例を解くことは研究に値する妥協である。 このような事例のモチベーションと記述の後,一通り木型卓上システムのSMT符号化に基づくLTLfMTの完全半決定法を提案する。 このアルゴリズムはBLACK満足度チェックツールに実装され、新しいベンチマークにおけるアプローチの有効性を実験的に評価した。

関連論文リスト

• Bisimulation Learning [55.859538562698496]
  我々は、大きな、潜在的に無限の状態空間を持つ状態遷移系の有限バイシミュレートを計算する。 提案手法は,実際に行われている他の最先端ツールよりも高速な検証結果が得られる。
  論文  参考訳（メタデータ） (2024-05-24T17:11:27Z)
• TLINet: Differentiable Neural Network Temporal Logic Inference [10.36033062385604]
  本稿では,STL式を学習するニューラルネットワークシンボリックフレームワークであるTLINetを紹介する。 従来の手法とは対照的に,時間論理に基づく勾配法に特化して設計された最大演算子の近似法を導入する。 我々のフレームワークは、構造だけでなく、STL公式のパラメータも学習し、演算子と様々な論理構造の柔軟な組み合わせを可能にします。
  論文  参考訳（メタデータ） (2024-05-03T16:38:14Z)
• Synthesizing Efficiently Monitorable Formulas in Metric Temporal Logic [4.60607942851373]
  システム実行から形式仕様を自動合成する問題を考察する。 時間論理式を合成するための古典的なアプローチの多くは、公式のサイズを最小化することを目的としている。 我々は,この概念を定式化し,有界な外見を持つ簡潔な公式を合成する学習アルゴリズムを考案する。
  論文  参考訳（メタデータ） (2023-10-26T14:13:15Z)
• Decidable Fragments of LTLf Modulo Theories (Extended Version) [66.25779635347122]
  一般に、fMTは、任意の決定可能な一階述語理論(例えば、線形算術)に対して、テーブルーベースの半決定手順で半決定可能であることが示されている。 有限メモリと呼ぶ抽象的意味条件を満たす任意のfMT式に対して、新しい規則で拡張されたテーブルーもまた終了することが保証されていることを示す。
  論文  参考訳（メタデータ） (2023-07-31T17:02:23Z)
• Computing unsatisfiable cores for LTLf specifications [3.251765107970636]
  有限トレース上の線形時間時間時間論理(LTLf)は、多くのアプリケーション領域で仕様を作成するためのデファクト標準になりつつある。 満足度チェックのための最先端手法を用いて、不満足なコアを抽出する4つのアルゴリズムを提案する。 結果は、異なるアルゴリズムやツールの実現可能性、有効性、相補性を示している。
  論文  参考訳（メタデータ） (2022-03-09T16:08:43Z)
• CoCoMoT: Conformance Checking of Multi-Perspective Processes via SMT (Extended Version) [62.96267257163426]
  我々はCoCoMoT(Computing Conformance Modulo Theories)フレームワークを紹介する。 まず、純粋な制御フロー設定で研究したSATベースのエンコーディングを、データ認識ケースに持ち上げる方法を示す。 次に,プロパティ保存型クラスタリングの概念に基づく新しい前処理手法を提案する。
  論文  参考訳（メタデータ） (2021-03-18T20:22:50Z)
• Temporal Answer Set Programming [3.263632801414296]
  本稿では,その知識表現と宣言的問題解決への応用の観点から,時間論理プログラミングの概要を述べる。 本研究は,TEL(Temporal Equilibrium Logic)と呼ばれる非単調な形式論の最近の成果に焦点を当てる。 第2部では,ASP.NET に近い時間論理プログラムと呼ばれる構文的断片を定義し,この問題が解決器 TEINGO の構築においてどのように活用されたかを説明する。
  論文  参考訳（メタデータ） (2020-09-14T16:13:36Z)
• Learning Reasoning Strategies in End-to-End Differentiable Proving [50.9791149533921]
  条件付き定理プローバーは勾配に基づく最適化により最適規則選択戦略を学習する。 条件付き定理プローサは拡張性があり、CLUTRRデータセット上で最先端の結果が得られることを示す。
  論文  参考訳（メタデータ） (2020-07-13T16:22:14Z)
• Certified Reinforcement Learning with Logic Guidance [78.2286146954051]
  線形時間論理(LTL)を用いて未知の連続状態/動作マルコフ決定過程(MDP)のゴールを定式化できるモデルフリーなRLアルゴリズムを提案する。 このアルゴリズムは、トレースが仕様を最大確率で満たす制御ポリシーを合成することが保証される。
  論文  参考訳（メタデータ） (2019-02-02T20:09:32Z)

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

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