論文の概要: Monitoring Data-aware Temporal Properties (Extended Version)
- arxiv url: http://arxiv.org/abs/2605.14666v1
- Date: Thu, 14 May 2026 10:23:11 GMT
- ステータス: 翻訳完了
- システム内更新日: 2026-05-15 21:45:34.775982
- Title: Monitoring Data-aware Temporal Properties (Extended Version)
- Title（参考訳）: データ対応時間特性のモニタリング(拡張版)
- Abstract要約: 有限トレース上の任意のSMT理論に富む線形時間特性の予測モニタリングについて考察する。
この設定での予測モニタリングは非常に困難であり、監視状態はこれまでのトレースプレフィックスと可能な有限継続の両方に依存している。
本研究は,表現的フラグメントオフMTにおける特性モニタリングのための新しい基礎的枠組みの正しさを提示し,正式に証明するものである。
- 参考スコア（独自算出の注目度）: 56.386411908764494
- License: http://creativecommons.org/licenses/by/4.0/
- Abstract: Dynamic systems in AI are often complex and heterogeneous, so that an internal specification is not accessible and verification techniques such as model checking are not applicable. Monitoring is in such cases an attractive alternative, as it evaluates desirable properties along traces generated by an unknown dynamic system. In this work, we consider anticipatory monitoring of linear-time properties enriched with an arbitrary SMT theory over finite traces (LTLfMT). Anticipatory monitoring in this setting is highly challenging, as the monitoring state depends on both the trace prefix seen so far and all its possible finite continuations. Under reasonable assumptions on the background theory, we present and formally prove the correctness of a novel foundational framework for monitoring properties in an expressive fragment of LTLfMT. The framework combines automata-theoretic methods to handle the temporal aspects of the logic, with automated reasoning techniques to address the first-order dimension. Moreover, we identify for the first time decidable fragments of this monitoring problem that are practically relevant as they combine linear arithmetic with uninterpreted functions, which covers e.g. data-aware business processes and dynamic systems operating over a read-only database. Feasibility is witnessed by a prototype implementation and preliminary evaluation.
- Abstract（参考訳）: AIの動的システムは複雑で異種であるため、内部仕様はアクセスできないし、モデルチェックのような検証技術は適用できない。
このような場合、監視は、未知の動的システムによって生成されたトレースに沿って望ましい特性を評価するため、魅力的な代替手段である。
本研究では,有限トレース(LTLfMT)上の任意のSMT理論に富む線形時間特性の予測モニタリングについて考察する。
この設定での予測モニタリングは非常に困難であり、監視状態はこれまでのトレースプレフィックスと可能な有限継続の両方に依存している。
背景理論の合理的な仮定の下で、LTLfMTの表現的断片における特性をモニタリングするための新しい基盤的枠組みを提示し、正式に証明する。
このフレームワークは、論理の時間的側面を扱う自動理論手法と、一階次元に対処する自動推論技術を組み合わせている。
さらに、線形算術と非解釈関数を組み合わせ、例えば、データ認識のビジネスプロセスや、読み取り専用データベース上で動作している動的システムをカバーすることにより、この監視問題の破片を初めて特定する。
実現性はプロトタイプの実装と予備評価によって確認される。
関連論文リスト
- Embedding-Aware Feature Discovery: Bridging Latent Representations and Interpretable Features in Event Sequences [5.03287845497428]
産業金融システムは、トランザクション、ユーザアクション、システムログなどの一時的なイベントシーケンスを運用する。
学習した埋め込みと機能ベースのパイプラインのギャップを埋める統合フレームワークであるEmbeding-Aware Feature Discovery (EAFD)を紹介します。
EAFDは2つの相補的基準を用いて、生のイベントシーケンスから直接特徴を発見し、評価し、洗練する。
論文 参考訳（メタデータ） (2026-03-16T14:29:26Z) - Quantitative Monitoring of Signal First-Order Logic [11.310581148639088]
Signal First-Order Logic (SFO) のためのロバストネスに基づく最初の定量的意味論を提供する。
SFOはそのような信号に対して表現力のあるリアルタイム仕様を提供するが、現時点ではBooleanセマンティクスのみで、ツールサポートはない。
これは、完全なSFOのオンライン定量モニタリングのための最初の公開プロトタイプである。
論文 参考訳（メタデータ） (2026-02-28T16:23:11Z) - Labels Matter More Than Models: Quantifying the Benefit of Supervised Time Series Anomaly Detection [56.302586730134806]
時系列異常検出(TSAD)は、しばしばラベル不足によって制約される重要なデータマイニングタスクである。
現在の研究は、主に教師なし時系列異常検出に焦点を当てている。
本稿では,アーキテクチャの複雑さがTSADの最適経路である,という前提に挑戦する。
論文 参考訳（メタデータ） (2025-11-20T08:32:49Z) - Interpretable Early Failure Detection via Machine Learning and Trace Checking-based Monitoring [9.565145785280452]
ベクトル化トレースチェックに基づく早期故障検出のためのフレームワークを開発する。
このフレームワークは、最先端の手法と比較して、主要なパフォーマンス指標を2-10%改善している。
論文 参考訳（メタデータ） (2025-08-25T08:30:01Z) - A Poisson-Gamma Dynamic Factor Model with Time-Varying Transition Dynamics [51.147876395589925]
非定常PGDSは、基礎となる遷移行列が時間とともに進化できるように提案されている。
後続シミュレーションを行うために, 完全共役かつ効率的なギブスサンプリング装置を開発した。
実験により,提案した非定常PGDSは,関連するモデルと比較して予測性能が向上することを示した。
論文 参考訳（メタデータ） (2024-02-26T04:39:01Z) - Monitoring Algorithmic Fairness under Partial Observations [3.790015813774933]
実行時検証技術は、デプロイされたシステムのアルゴリズム的公正性を監視するために導入された。
従来の監視技術は、監視されたシステムの状態の完全な可観測性を前提としている。
我々は、部分的に観測されたマルコフ連鎖としてモデル化されたシステムにフェアネスモニタリングを拡張した。
論文 参考訳（メタデータ） (2023-08-01T07:35:54Z) - Uncovering the Missing Pattern: Unified Framework Towards Trajectory
Imputation and Prediction [60.60223171143206]
軌道予測は、観測されたシーケンスから実体運動や人間の行動を理解する上で重要な作業である。
現在の方法では、観測されたシーケンスが完了したと仮定し、欠落した値の可能性を無視する。
本稿では,グラフに基づく条件変動リカレントニューラルネットワーク (GC-VRNN) の統一フレームワークを提案する。
論文 参考訳（メタデータ） (2023-03-28T14:27:27Z) - Self-Supervised Representation Learning from Temporal Ordering of
Automated Driving Sequences [49.91741677556553]
本研究では、認識タスクのための地域レベルの特徴表現を事前学習するための時間順述前文タスクであるTempOを提案する。
我々は各フレームを、オブジェクト検出やトラッキングシステムにとって自然な表現である、未順序な特徴ベクトルのセットで埋め込む。
BDD100K、nu Images、MOT17データセットの大規模な評価は、私たちのTempO事前学習アプローチがシングルフレームの自己教師型学習方法よりも優れていることを示している。
論文 参考訳（メタデータ） (2023-02-17T18:18:27Z) - Linear-Time Verification of Data-Aware Dynamic Systems with Arithmetic [8.914271888521652]
我々は、忠実な有限状態抽象の存在を保証する「有限要約」という新しい意味的特性を導入する。
形式的手法やデータベース理論で研究されたいくつかの決定可能性条件は、この性質の具体的かつチェック可能な例と見なすことができる。
我々の結果は、以前のアプローチでは手の届かないシステムを分析することを可能にする。
論文 参考訳（メタデータ） (2022-03-15T15:14:25Z) - CoCoMoT: Conformance Checking of Multi-Perspective Processes via SMT
(Extended Version) [62.96267257163426]
我々はCoCoMoT(Computing Conformance Modulo Theories)フレームワークを紹介する。
まず、純粋な制御フロー設定で研究したSATベースのエンコーディングを、データ認識ケースに持ち上げる方法を示す。
次に,プロパティ保存型クラスタリングの概念に基づく新しい前処理手法を提案する。
論文 参考訳（メタデータ） (2021-03-18T20:22:50Z) - Stochastically forced ensemble dynamic mode decomposition for
forecasting and analysis of near-periodic systems [65.44033635330604]
本稿では,観測力学を強制線形系としてモデル化した新しい負荷予測手法を提案する。
固有線型力学の利用は、解釈可能性やパーシモニーの観点から、多くの望ましい性質を提供することを示す。
電力グリッドからの負荷データを用いたテストケースの結果が提示される。
論文 参考訳（メタデータ） (2020-10-08T20:25:52Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。