論文の概要: Progression- vs Automata-based Anticipatory Monitoring of LTL over Finite Traces (Extended Version)
- arxiv url: http://arxiv.org/abs/2609.32912v1
- Date: Sat, 26 Sep 2026 20:03:31 GMT
- ステータス: 翻訳完了
- システム内更新日: 2026-10-06 12:00:11.732186
- Title: Progression- vs Automata-based Anticipatory Monitoring of LTL over Finite Traces (Extended Version)
- Title（参考訳）: 有限トレース上のTLLの進展とオートマタによる予測モニタリング(拡張版)
- Abstract要約: 予測監視(precipatory monitoring)は,実行時検証の先進的な形式である。
算術的制約を伴う線形時間特性のモニタリングに着目する。
本稿では,提案手法と算術的設定法の両方に対して,進捗と満足度チェックに基づく代替手法を提案する。
- 参考スコア（独自算出の注目度）: 10.990236689737094
- License: http://creativecommons.org/licenses/by/4.0/
- Abstract: When safety-critical systems are developed from a known internal specification, their correctness can be established by model checking. In the frequent case where such a specification is unknown or inaccessible, runtime verification presents an attractive alternative, e.g., to ascertain that autonomous and agentic systems as well as business processes satisfy desirable properties and/or comply with safety requirements. In this paper we study anticipatory monitoring, an advanced form of runtime verification, where the monitoring state is determined by both the trace prefix seen so far, and all its possible finite-length, future continuations. We focus on monitoring linear-time properties that may involve arithmetic constraints. Automata-based approaches, the de-facto standard in this setting, are notorious for their computational complexity. We propose an alternative approach based on progression and LTLf satisfiability checking, for both propositional and arithmetic settings. We experimentally compare the automata- and progression-based approaches, and a third method that combines the two. Our experiments suggest that the progression-based approach often succeeds in producing a verdict when the automata constructions do not terminate, especially for the arithmetic setting. For the propositional setting, the combined technique provides a good tradeoff.
- Abstract（参考訳）: 安全クリティカルなシステムが既知の内部仕様から開発された場合、その正確性はモデル検査によって確立できる。
このような仕様が不明またはアクセス不能な頻繁な場合、実行時検証は、例えば、自律的およびエージェント的なシステムとビジネスプロセスが望ましい特性を満たし、または/または安全要件を満たすことを確認するための魅力的な代替手段を示す。
本稿では,これまで見てきたトレースプレフィックスと,その可能性のある有限長,将来の継続によって,監視状態が決定される,高度なランタイム検証方式である予測監視について検討する。
算術的制約を伴う線形時間特性のモニタリングに着目する。
この設定におけるデファクト標準であるオートマタベースのアプローチは、その計算複雑性で悪名高い。
本稿では,提案手法と算術的設定法の両方に対して,進行度とLTLf満足度チェックに基づく代替手法を提案する。
提案手法は,オートマタとプログレッシションに基づくアプローチと,この2つを組み合わせた第3の手法を実験的に比較した。
提案実験は,特に算術的設定において,オートマトン構築が終了しない場合,進行に基づくアプローチが検証に成功することを示唆している。
提案的な設定では、組み合わせたテクニックは良いトレードオフを提供します。
関連論文リスト
- Developing a Totally Unimodular Linear Program for Optimal Conformance Checking: When and Why It Complements A* [0.324890820102255]
本稿では、完全一様線形プログラム(LP)としてのアライメントに基づく整合性チェックの再構成を提案する。
基礎となるネットワークフロー構造を利用することで、LP緩和による最適極点解が保証される。
両手法を併用した単純なアルゴリズム選択ガイドラインを導出し, 平均実行時節約率38.6%, 選択精度96%を実現した。
論文 参考訳（メタデータ） (2026-05-26T12:30:23Z) - Monitoring Data-aware Temporal Properties (Extended Version) [56.386411908764494]
有限トレース上の任意のSMT理論に富む線形時間特性の予測モニタリングについて考察する。
この設定での予測モニタリングは非常に困難であり、監視状態はこれまでのトレースプレフィックスと可能な有限継続の両方に依存している。
本研究は,表現的フラグメントオフMTにおける特性モニタリングのための新しい基礎的枠組みの正しさを提示し,正式に証明するものである。
論文 参考訳（メタデータ） (2026-05-14T10:23:11Z) - HIPO: Instruction Hierarchy via Constrained Reinforcement Learning [57.40686733111483]
textscHIPOは、制約付きマルコフ決定プロセスとしてHIFを定式化する新しいアライメントフレームワークである。
textscHIPOはシステムプロンプトを単に入力コンテキストから厳密なアルゴリズム境界まで高める。
論文 参考訳（メタデータ） (2026-03-17T06:12:41Z) - Detecting Object Tracking Failure via Sequential Hypothesis Testing [80.7891291021747]
ビデオにおけるリアルタイムのオンラインオブジェクト追跡は、コンピュータビジョンにおける中核的なタスクである。
本稿では,物体追跡を逐次的仮説テストとして解釈することを提案する。
本研究では,地中追跡情報と内部追跡情報の両方を活用することにより,教師なしと教師なしの両方の変種を提案する。
論文 参考訳（メタデータ） (2026-02-13T14:57:15Z) - Interpretable Early Failure Detection via Machine Learning and Trace Checking-based Monitoring [9.565145785280452]
ベクトル化トレースチェックに基づく早期故障検出のためのフレームワークを開発する。
このフレームワークは、最先端の手法と比較して、主要なパフォーマンス指標を2-10%改善している。
論文 参考訳（メタデータ） (2025-08-25T08:30:01Z) - Discovering Decision Manifolds to Assure Trusted Autonomous Systems [0.0]
本稿では,システムが提示できる正誤応答の範囲を最適化した探索手法を提案する。
この多様体は、従来のテストやモンテカルロシミュレーションよりもシステムの信頼性をより詳細に理解する。
この概念実証では,本手法を自動運転車のループ内ソフトウェア評価に適用する。
論文 参考訳（メタデータ） (2024-02-12T16:55:58Z) - Scope Compliance Uncertainty Estimate [0.4262974002462632]
SafeMLはそのような監視を行うためのモデルに依存しないアプローチである。
この研究は、二項決定を連続計量に変換することによってこれらの制限に対処する。
論文 参考訳（メタデータ） (2023-12-17T19:44:20Z) - CoCoMoT: Conformance Checking of Multi-Perspective Processes via SMT
(Extended Version) [62.96267257163426]
我々はCoCoMoT(Computing Conformance Modulo Theories)フレームワークを紹介する。
まず、純粋な制御フロー設定で研究したSATベースのエンコーディングを、データ認識ケースに持ち上げる方法を示す。
次に,プロパティ保存型クラスタリングの概念に基づく新しい前処理手法を提案する。
論文 参考訳（メタデータ） (2021-03-18T20:22:50Z) - Higher Performance Visual Tracking with Dual-Modal Localization [106.91097443275035]
Visual Object Tracking (VOT)は、堅牢性と正確性の両方に同期性を必要とする。
ONRによるロバストなローカリゼーション抑制器とOFCによるターゲットセンターへの正確なローカリゼーションにより、ターゲットローカリゼーションのためのデュアルモーダルフレームワークを提案します。
論文 参考訳（メタデータ） (2021-03-18T08:47:56Z) - SMT-based Safety Verification of Parameterised Multi-Agent Systems [78.04236259129524]
パラメータ化マルチエージェントシステム(MAS)の検証について検討する。
特に、与えられた状態公式として特徴づけられる不要な状態が、所定のMASで到達可能かどうかについて検討する。
論文 参考訳（メタデータ） (2020-08-11T15:24:05Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。