論文の概要: On Synthesis of Metric Interval Temporal Logics

• arxiv url: http://arxiv.org/abs/2609.01032v1
• Date: Tue, 01 Sep 2026 10:30:46 GMT
• ステータス: 翻訳完了
• システム内更新日: 2026-09-02 16:31:36.5533
• Title: On Synthesis of Metric Interval Temporal Logics
• Title（参考訳）: 計量時空間論理の合成について
• Authors: Hsi-Ming Ho, Shankaranarayanan Krishna, Khushraj Madnani,
• Abstract要約: 本稿では,表現型時間論理の適応型学習に最初に取り組む枠組みを提案する。 我々のアプローチは、タイムドラーニングの問題を、拡張性のある未使用のものに正式に還元します。 いくつかのベンチマークで実装を評価し,提案手法の有効性を実証した。
• 参考スコア（独自算出の注目度）: 0.5505634045241289
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: Automated mining of formal specifications is vital for verifying real-time systems. However, existing passive learning approaches remain restricted to deterministic specifications or limited fragments of Timed Regular Expressions (TRE). To our knowledge, this paper presents the first framework to tackle \emph{precise} passive learning for an expressive timed logic, \emph{Metric Interval Temporal Logic} (MITL) without relying on predefined templates or restricted logic fragments. Our approach formally reduces the timed learning problem into a scalable untimed one. By identifying quantitative timing differences between positive and negative traces, we synthesise precise timed constraints and inject them as new Boolean atomic propositions. This embeds timing into the alphabet, delegating the complex formula evaluation to highly optimised, off-the-shelf untimed LTL tools. Crucially, our framework is complete, guaranteeing a separating specification can always be found. We evaluate our implementation across several benchmarks, demonstrating the effectiveness of our approach.
• Abstract（参考訳）: 正式な仕様の自動マイニングは、リアルタイムシステムの検証に不可欠である。 しかし、既存の受動的学習アプローチは、決定論的仕様や時間正規表現(TRE)の限定的な断片に限定されている。 本稿では,事前定義されたテンプレートや制限された論理フラグメントを使わずに,表現型時間論理学における「emph{precise} 受動的学習」,「emph{Metric Interval Temporal Logic} (MITL)」に取り組むための最初のフレームワークを提案する。 我々のアプローチは、タイムドラーニングの問題を、拡張性のある未使用のものに正式に還元します。 正および負のトレース間の定量的なタイミング差を同定することにより、正確な時間制約を合成し、それらを新しいブール原子命題として注入する。 これはアルファベットにタイミングを埋め込み、複雑な公式評価を高度に最適化され、未使用のLTLツールに委譲する。 重要なことに、私たちのフレームワークは完成しており、仕様の分離が常に見つかることを保証しています。 いくつかのベンチマークで実装を評価し,提案手法の有効性を実証した。

関連論文リスト

• STAIR: Semantic-Temporal Automaton for Interpretable Reasoning in Temporal Question Answering [7.774935839413563]
  我々はtextbfSemantic-textbfTemporal textbfAutomaton for textbfInterpretable textbfReasoningを提案する。 LLMアダプタは、複雑な質問の定式化を正規化された時間的意図にマッピングし、決定論的時間的オートマトンは正準化された証拠に対して対応するポリシーを実行する。 STAIRは、TimeQA-Easy、TimeQA-Hard、TempReason-L2、TempReason-L3データセットにおいて、強いベースラインを一貫して上回る。
  論文  参考訳（メタデータ） (2026-08-17T07:59:45Z)
• Correct-by-Construction Behavior Tree Synthesis from Signal Temporal Logic Specifications with Application to Robotic Missions [5.524204636266904]
  動作木(BT)は、ロボット工学における複雑なタスク実行に広く採用されている。 この文字は、Signal Temporal Logic (STL)仕様から正しい構成BTを合成する。
  論文  参考訳（メタデータ） (2026-07-21T05:43:19Z)
• Learning Linear Temporal Specifications from Demonstrations with Uncertainty [0.0]
  本稿では,不確実性のある実演から最小の線形時間論理式を学習するための枠組みを提案する。 提案手法を最先端の学習手法に対して評価し,不確実性条件下での基幹構造とより密に整合した仕様を復元することを示す。
  論文  参考訳（メタデータ） (2026-07-12T20:43:52Z)
• How LLMs Fail and Generalize in RTL Coding for Hardware Design? [56.361436215029045]
  我々は,認知理論に触発された問題解決性に基づく新しい誤り分類法を導入する。 我々の分類学は、障害を構文、意味、解決可能な機能、解決不可能な機能タイプに分類する。
  論文  参考訳（メタデータ） (2026-04-26T14:34:49Z)
• Do It for HER: First-Order Temporal Logic Reward Specification in Reinforcement Learning (Extended Version) [49.462399222747024]
  本研究では,大規模状態空間を持つ決定過程(MDP)における非マルコフ報酬の論理的仕様に関する新しい枠組みを提案する。 我々のアプローチは有限トレース(LTLfMT)上での線形時間論理モデュロ理論を利用する 本稿では,報酬マシンとHER(Hindsight Experience Replay)をベースとした一階述語論理仕様の翻訳手法を提案する。
  論文  参考訳（メタデータ） (2026-02-05T22:11:28Z)
• Fast Controlled Generation from Language Models with Adaptive Weighted Rejection Sampling [90.86991492288487]
  トークンの制約を評価するのは 違法にコストがかかる LCDは文字列上のグローバル分布を歪め、ローカル情報のみに基づいてトークンをサンプリングすることができる。 我々のアプローチは最先端のベースラインよりも優れていることを示す。
  論文  参考訳（メタデータ） (2025-04-07T18:30:18Z)
• TLINet: Differentiable Neural Network Temporal Logic Inference [10.36033062385604]
  本稿では,STL式を学習するニューラルネットワークシンボリックフレームワークであるTLINetを紹介する。 従来の手法とは対照的に,時間論理に基づく勾配法に特化して設計された最大演算子の近似法を導入する。 我々のフレームワークは、構造だけでなく、STL公式のパラメータも学習し、演算子と様々な論理構造の柔軟な組み合わせを可能にします。
  論文  参考訳（メタデータ） (2024-05-03T16:38:14Z)
• Linear Temporal Logic Modulo Theories over Finite Traces (Extended Version) [72.38188258853155]
  有限トレース(LTLf)上の線形時間論理について検討する。 命題の文字は任意の理論で解釈された一階述語式に置き換えられる。 Satisfiability Modulo Theories (LTLfMT) と呼ばれる結果の論理は半決定可能である。
  論文  参考訳（メタデータ） (2022-04-28T17:57:33Z)
• Multi-Agent Reinforcement Learning with Temporal Logic Specifications [65.79056365594654]
  本研究では,時間論理仕様を満たすための学習課題を,未知の環境下でエージェントのグループで検討する。 我々は、時間論理仕様のための最初のマルチエージェント強化学習手法を開発した。 主アルゴリズムの正確性と収束性を保証する。
  論文  参考訳（メタデータ） (2021-02-01T01:13:03Z)
• Temporal Answer Set Programming [3.263632801414296]
  本稿では,その知識表現と宣言的問題解決への応用の観点から,時間論理プログラミングの概要を述べる。 本研究は,TEL(Temporal Equilibrium Logic)と呼ばれる非単調な形式論の最近の成果に焦点を当てる。 第2部では,ASP.NET に近い時間論理プログラムと呼ばれる構文的断片を定義し,この問題が解決器 TEINGO の構築においてどのように活用されたかを説明する。
  論文  参考訳（メタデータ） (2020-09-14T16:13:36Z)

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

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