論文の概要: Synthesizing Efficiently Monitorable Formulas in Metric Temporal Logic

• arxiv url: http://arxiv.org/abs/2310.17410v1
• Date: Thu, 26 Oct 2023 14:13:15 GMT
• ステータス: 処理完了
• システム内更新日: 2023-10-27 20:10:27.003576
• Title: Synthesizing Efficiently Monitorable Formulas in Metric Temporal Logic
• Title（参考訳）: 計量時間論理における効率的な監視可能な公式の合成
• Authors: Ritam Raha, Rajarshi Roy, Nathanael Fijalkow, Daniel Neider and Guillermo A. Perez
• Abstract要約: システム実行から形式仕様を自動合成する問題を考察する。 時間論理式を合成するための古典的なアプローチの多くは、公式のサイズを最小化することを目的としている。 我々は,この概念を定式化し,有界な外見を持つ簡潔な公式を合成する学習アルゴリズムを考案する。
• 参考スコア（独自算出の注目度）: 4.60607942851373
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: In runtime verification, manually formalizing a specification for monitoring system executions is a tedious and error-prone process. To address this issue, we consider the problem of automatically synthesizing formal specifications from system executions. To demonstrate our approach, we consider the popular specification language Metric Temporal Logic (MTL), which is particularly tailored towards specifying temporal properties for cyber-physical systems (CPS). Most of the classical approaches for synthesizing temporal logic formulas aim at minimizing the size of the formula. However, for efficiency in monitoring, along with the size, the amount of "lookahead" required for the specification becomes relevant, especially for safety-critical applications. We formalize this notion and devise a learning algorithm that synthesizes concise formulas having bounded lookahead. To do so, our algorithm reduces the synthesis task to a series of satisfiability problems in Linear Real Arithmetic (LRA) and generates MTL formulas from their satisfying assignments. The reduction uses a novel encoding of a popular MTL monitoring procedure using LRA. Finally, we implement our algorithm in a tool called TEAL and demonstrate its ability to synthesize efficiently monitorable MTL formulas in a CPS application.
• Abstract（参考訳）: 実行時の検証では、システム実行を監視するための仕様を手動で定式化するのは面倒でエラーを起こしやすいプロセスである。 この問題に対処するために,システム実行から形式仕様を自動的に合成する問題を考える。 本稿では,サイバー物理システム(CPS)の時間特性の特定に特化している,一般的な仕様言語 Metric Temporal Logic (MTL) について考察する。 時間論理式を合成するための古典的なアプローチの多くは、公式のサイズを最小化することを目的としている。 しかしながら、監視の効率性やサイズについては、特に安全クリティカルなアプリケーションにおいて、仕様に必要な"ルックヘッド"の量が重要となる。 我々は,この概念を定式化し,有界な外見を持つ簡潔な公式を合成する学習アルゴリズムを考案する。 そこで本アルゴリズムは,LRA(Linear Real Arithmetic)において,合成タスクを一連の満足度問題に還元し,満足な代入からMTL式を生成する。 このリダクションは、LRAを用いた一般的なMTL監視手順の新たなエンコーディングを使用する。 最後に,本アルゴリズムをtealというツールで実装し,cpsアプリケーションで効率的にモニタ可能なmtl式を合成する能力を示す。

関連論文リスト

• Smoothing Methods for Automatic Differentiation Across Conditional Branches [0.0]
  スムース解釈(SI)は、プログラムの出力とガウス核との畳み込みを近似し、原理的にその出力を滑らかにする。 SIと自動微分(AD)を組み合わせることで、スムーズなプログラムの勾配を効率的に計算する。 本稿では,ADとサンプリングを組み合わせたスムーズなプログラムの勾配を推定することにより,基礎となる仮定を回避する新しいモンテカルロ推定法を提案する。
  論文  参考訳（メタデータ） (2023-10-05T15:08:37Z)
• Large Language Models as General Pattern Machines [64.75501424160748]
  我々は,事前訓練された大規模言語モデル (LLM) が,複雑なトークンシーケンスを自動回帰的に完了することを示す。 驚いたことに、語彙からランダムにサンプリングされたトークンを用いてシーケンスが表現された場合でも、パターン完了の習熟度を部分的に保持することができる。 本研究では,ロボット工学における問題に対して,これらのゼロショット機能がどのように適用されるかを検討する。
  論文  参考訳（メタデータ） (2023-07-10T17:32:13Z)
• Formal Controller Synthesis for Markov Jump Linear Systems with Uncertain Dynamics [64.72260320446158]
  マルコフジャンプ線形系に対する制御器の合成法を提案する。 本手法は,MJLSの離散(モードジャンピング)と連続(確率線形)の両方の挙動を捉える有限状態抽象化に基づいている。 本手法を複数の現実的なベンチマーク問題,特に温度制御と航空機の配送問題に適用する。
  論文  参考訳（メタデータ） (2022-12-01T17:36:30Z)
• Linear Temporal Logic Modulo Theories over Finite Traces (Extended Version) [72.38188258853155]
  有限トレース(LTLf)上の線形時間論理について検討する。 命題の文字は任意の理論で解釈された一階述語式に置き換えられる。 Satisfiability Modulo Theories (LTLfMT) と呼ばれる結果の論理は半決定可能である。
  論文  参考訳（メタデータ） (2022-04-28T17:57:33Z)
• Scalable Anytime Algorithms for Learning Formulas in Linear Temporal Logic [2.631744051718347]
  トレースを分類する公式を学習する際の問題点を考察する。 既存の解には2つの制限がある: それらは小さな公式を超えてスケールせず、結果を返すことなく計算資源を消費する。 我々は,両問題に対処する新しいアルゴリズムを導入する。我々のアルゴリズムは,従来よりも桁違いに大きい式を構築でき,いつでも可能である。
  論文  参考訳（メタデータ） (2021-10-13T13:57:31Z)
• Activation Relaxation: A Local Dynamical Approximation to Backpropagation in the Brain [62.997667081978825]
  活性化緩和(AR)は、バックプロパゲーション勾配を力学系の平衡点として構成することで動機付けられる。 我々のアルゴリズムは、正しいバックプロパゲーション勾配に迅速かつ堅牢に収束し、単一のタイプの計算単位しか必要とせず、任意の計算グラフで操作できる。
  論文  参考訳（メタデータ） (2020-09-11T11:56:34Z)
• Backpropagation through Signal Temporal Logic Specifications: Infusing Logical Structure into Gradient-Based Methods [28.72161643908351]
  本稿では,STLCG(Signal Temporal Logic)公式の定量的意味を計算グラフを用いて計算する手法を提案する。 STLは、連続系とハイブリッド系の両方で生成される信号の空間的および時間的特性を指定できる、強力で表現力のある形式言語である。
  論文  参考訳（メタデータ） (2020-07-31T22:01:39Z)
• Iterative Algorithm Induced Deep-Unfolding Neural Networks: Precoding Design for Multiuser MIMO Systems [59.804810122136345]
  本稿では,AIIDNN(ディープ・アンフォールディング・ニューラルネット)を一般化した,ディープ・アンフォールディングのためのフレームワークを提案する。 古典的重み付き最小二乗誤差(WMMSE)反復アルゴリズムの構造に基づく効率的なIAIDNNを提案する。 提案したIAIDNNは,計算複雑性を低減した反復WMMSEアルゴリズムの性能を効率よく向上することを示す。
  論文  参考訳（メタデータ） (2020-06-15T02:57:57Z)
• 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)

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

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