論文の概要: Predictive Varanus: Combining CSP Conformance Monitoring with Predictive LTL Runtime Verification
- arxiv url: http://arxiv.org/abs/2609.17625v1
- Date: Tue, 15 Sep 2026 06:26:51 GMT
- ステータス: 翻訳完了
- システム内更新日: 2026-09-20 08:55:53.458935
- Title: Predictive Varanus: Combining CSP Conformance Monitoring with Predictive LTL Runtime Verification
- Title（参考訳）: Predictive Varanus: CSPコンパタンスモニタリングと予測LTL実行時の検証を組み合わせる
- Abstract要約: PreDICTIVE VARANUSはプロセス代数Communicating Sequential Processes (CSP)で記述されたモデルを使用する2段階検証パイプラインである。
CSPバリデーションと予測の組み合わせによって、標準的なランタイムモニタリングよりも早期の検証が可能になることを示す。
ケーススタディは、CSPバリデーションと予測の組み合わせが、標準のランタイムモニタリングよりも早期のバリデーションを提供する方法を示している。
- 参考スコア（独自算出の注目度）: 0.5996444607432799
- License: http://creativecommons.org/licenses/by/4.0/
- Abstract: Runtime Verification is well suited to autonomous and robotic systems because it checks the behaviour that is actually observed during execution. Its main limitation, however, is that it is usually reactive: the monitor detects a violation only after the system has already performed a bad event. This can be too late in domains where failures are costly or unsafe. In this paper we present PREDICTIVE VARANUS, a two-stage verification pipeline that combines VARANUS, a runtime verifier that uses models written in the process algebra Communicating Sequential Processes (CSP), with predictive runtime verification for LTL. A CSP model is first used as a conformance gate over the observed event trace; the same model is then translated into a Buchi automaton that constrains the futures explored by a predictive LTL monitor. In this way, out-of-model behaviour is rejected immediately, while model-consistent prefixes can be classified as already guaranteeing satisfaction, already forcing violation, or still being inconclusive for the monitored temporal property. We formalise the combined monitor, explain its implementation, and illustrate the approach on a robotic rover for nuclear-store inspection. The case study shows how the combination of CSP validation and predictive LTL can provide earlier verdicts than standard runtime monitoring while reusing an existing design-time CSP model.
- Abstract（参考訳）: 実行中に実際に観察される動作をチェックするため、自律システムやロボットシステムには実行時検証が適している。
モニターは、システムがすでに悪いイベントを実行した後のみ違反を検出する。
これは、障害がコストがかかる、あるいは安全でないドメインでは遅すぎる可能性がある。
本稿では,プロセス代数Communicating Sequential Processes(CSP)で記述されたモデルを用いた実行時検証と,LTLの予測実行時検証を組み合わせた2段階検証パイプラインであるPreDICTIVE VARANUSを提案する。
CSPモデルは、観測されたイベントトレース上のコンフォーマンスゲートとして最初に使用され、同じモデルがBuchiオートマトンに変換され、予測LTLモニターによって探索される未来を制限する。
このように、モデル外動作は直ちに拒否されるが、モデルに一貫性のあるプレフィックスは、すでに満足度を保証している、違反を強制している、あるいは監視対象の時間的特性に決定的でないと分類できる。
組み合わせたモニターを形式化し、その実装を説明し、核貯蔵検査のためのロボットローバーのアプローチを説明する。
ケーススタディは、CSPバリデーションと予測LTLの組み合わせが、既存の設計時CSPモデルを再利用しながら、標準ランタイムモニタリングよりも早期の検証を提供する方法を示している。
関連論文リスト
- FutureRTC: Real-Time Robot Execution with Anticipatory-Conditioned Action Chunking [51.97839311685636]
FutureRTCは、実行時の観察と非同期VLA制御の状態を予測するためのプラグイン・アンド・プレイ適応フレームワークである。
FutureRTCは推論遅延に対する堅牢性を実現し,よりスムーズな軌道,高速な実行,一貫したタスク成功率を実現している。
論文 参考訳（メタデータ） (2026-07-27T05:10:16Z) - Do Activation Monitors Survive Model Updates? Benchmarking, Predicting, and Repairing Activation-Monitor Staleness [0.16921396880325779]
ベースモデル上でトレーニングされたアクティベーションモニタが,定期的なモデル更新後も信頼性が保たれているかどうかを検証した。
量子化スタイルの更新は、主に凍結プローブのパフォーマンスを保ち、微調整スタイルの更新は、しばしばプローブを不安定にする。
また、前処理機能から劣化が予測可能であることも示し、再配置予算をモニターに向けてトリアージすることが可能となり、最も失敗する可能性が最も高い。
論文 参考訳（メタデータ） (2026-06-14T19:07:22Z) - CIAware-Bench: Benchmarking Control Intervention Awareness Across Frontier LLMs [100.38986535324284]
我々は、フロンティアモデル全体でのtextbfcontrol textbfintervention (CI) の認識を測定するベンチマークである textbfCIAware-Bench を紹介する。
CIAware-Benchは、モデルが自身の軌跡を制御介入によって修正されたものと区別できるかどうかをテストする。
論文 参考訳（メタデータ） (2026-06-09T16:24:16Z) - Explainable Runtime Dependency Tracking for AI-RAN Conflict Monitoring [0.0]
将来のAI統合無線アクセスネットワーク(AI-RAN)は、オープンプログラム可能性と学習可能なxApp、rApp、共有パラメータとキーパフォーマンスインジケータ(KPI)に作用するコントロール機能を組み合わせる。
競合監視では、どのアプリケーションがデプロイされているかを知るだけでは十分ではなく、実行時診断によって仮定されるパラメータ--KPI依存性が、現在の運用体制の下で有効であるかどうかを知る必要がある。
本稿では,ストリーミングテレメトリイベントから解釈可能な依存性表現を追跡する,軽量なモニタリングプリミティブについて検討する。
論文 参考訳（メタデータ） (2026-06-04T19:21:32Z) - Monitoring Data-aware Temporal Properties (Extended Version) [56.386411908764494]
有限トレース上の任意のSMT理論に富む線形時間特性の予測モニタリングについて考察する。
この設定での予測モニタリングは非常に困難であり、監視状態はこれまでのトレースプレフィックスと可能な有限継続の両方に依存している。
本研究は,表現的フラグメントオフMTにおける特性モニタリングのための新しい基礎的枠組みの正しさを提示し,正式に証明するものである。
論文 参考訳（メタデータ） (2026-05-14T10:23:11Z) - Detecting Object Tracking Failure via Sequential Hypothesis Testing [80.7891291021747]
ビデオにおけるリアルタイムのオンラインオブジェクト追跡は、コンピュータビジョンにおける中核的なタスクである。
本稿では,物体追跡を逐次的仮説テストとして解釈することを提案する。
本研究では,地中追跡情報と内部追跡情報の両方を活用することにより,教師なしと教師なしの両方の変種を提案する。
論文 参考訳（メタデータ） (2026-02-13T14:57:15Z) - Adaptive Attacks on Trusted Monitors Subvert AI Control Protocols [80.68060125494645]
プロトコルとモニタモデルを知っている信頼できないモデルによるアダプティブアタックについて検討する。
我々は、攻撃者がモデル出力に公知またはゼロショットプロンプトインジェクションを埋め込む単純な適応攻撃ベクトルをインスタンス化する。
論文 参考訳（メタデータ） (2025-10-10T15:12:44Z) - Interpretable Early Failure Detection via Machine Learning and Trace Checking-based Monitoring [9.565145785280452]
ベクトル化トレースチェックに基づく早期故障検出のためのフレームワークを開発する。
このフレームワークは、最先端の手法と比較して、主要なパフォーマンス指標を2-10%改善している。
論文 参考訳（メタデータ） (2025-08-25T08:30:01Z) - Varanus: Runtime Verification for CSP [0.0]
本稿では,CSP仕様から構築されたオラクルに対してシステムを監視するRVツールであるVaranusについて述べる。
本ツールは,核廃棄物貯蔵所を検査するロボットローバーを模擬したロボットローバーに適用し,その性能を異なる言語を用いた他の2つのRVツールと実証的に比較する。
論文 参考訳（メタデータ） (2025-06-17T11:42:14Z) - CARLA: Self-supervised Contrastive Representation Learning for Time Series Anomaly Detection [53.83593870825628]
時系列異常検出(TSAD)の主な課題は、多くの実生活シナリオにおいてラベル付きデータの欠如である。
既存の異常検出手法の多くは、教師なしの方法で非ラベル時系列の正常な振る舞いを学習することに焦点を当てている。
本稿では,時系列異常検出のためのエンドツーエンドの自己教師型コントラアスティブ表現学習手法を提案する。
論文 参考訳（メタデータ） (2023-08-18T04:45:56Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。