論文の概要: Quantitative Monitoring of Signal First-Order Logic
- arxiv url: http://arxiv.org/abs/2603.00728v2
- Date: Tue, 03 Mar 2026 14:12:01 GMT
- ステータス: 翻訳完了
- システム内更新日: 2026-03-04 14:54:12.538271
- Title: Quantitative Monitoring of Signal First-Order Logic
- Title(参考訳): 信号第一次論理の定量的モニタリング
- Authors: Marek Chalupa, Thomas A. Henzinger, N. Ege Saraç, Emily Yu,
- Abstract要約: Signal First-Order Logic (SFO) のためのロバストネスに基づく最初の定量的意味論を提供する。
SFOはそのような信号に対して表現力のあるリアルタイム仕様を提供するが、現時点ではBooleanセマンティクスのみで、ツールサポートはない。
これは、完全なSFOのオンライン定量モニタリングのための最初の公開プロトタイプである。
- 参考スコア(独自算出の注目度): 11.310581148639088
- License: http://creativecommons.org/licenses/by/4.0/
- Abstract: Runtime monitoring checks, during execution, whether a partial signal produced by a hybrid system satisfies its specification. Signal First-Order Logic (SFO) offers expressive real-time specifications over such signals, but currently comes only with Boolean semantics and has no tool support. We provide the first robustness-based quantitative semantics for SFO, enabling the expression and evaluation of rich real-time properties beyond the scope of existing formalisms such as Signal Temporal Logic. To enable online monitoring, we identify a past-time fragment of SFO and give a pastification procedure that transforms bounded-response SFO formulas into equisatisfiable formulas in this fragment. We then develop an efficient runtime monitoring algorithm for this past-time fragment and evaluate its performance on a set of benchmarks, demonstrating the practicality and effectiveness of our approach. To the best of our knowledge, this is the first publicly available prototype for online quantitative monitoring of full SFO.
- Abstract(参考訳): 実行中に、ハイブリッドシステムによって生成された部分的な信号が仕様を満たすかどうか、ランタイム監視がチェックする。
Signal First-Order Logic (SFO)は、そのような信号に対して表現力のあるリアルタイム仕様を提供するが、現時点ではBooleanセマンティクスのみで、ツールサポートはない。
本稿では,信号時間論理などの既存の形式論の範囲を超えて,リッチなリアルタイム特性の表現と評価を可能にする,SFOのための最初のロバストネスに基づく定量的意味論を提供する。
オンラインモニタリングを実現するために,SFOの過去のフラグメントを特定し,そのフラグメント内の有界応答式を等価な式に変換するパスティフィケーション手順を提案する。
次に、この過去のフラグメントに対する効率的なランタイム監視アルゴリズムを開発し、その性能をベンチマークで評価し、我々のアプローチの実用性と有効性を示す。
我々の知る限りでは、これは完全なSFOのオンライン定量モニタリングのための最初の公開プロトタイプである。
関連論文リスト
- Order-Aware Test-Time Adaptation: Leveraging Temporal Dynamics for Robust Streaming Inference [18.524636088926425]
テスト時間適応(TTA)により、未ラベルのテスト時間ストリームから学習することで、事前訓練されたモデルが分散シフトに適応できる。
これを解決するために、オーダーアウェアテスト時間適応(OATTA)を導入する。
OATTAは確立されたベースラインを継続的に強化し、精度を最大6.35%向上させた。
論文 参考訳(メタデータ) (2026-01-28T20:07:40Z) - Interpretable Early Failure Detection via Machine Learning and Trace Checking-based Monitoring [9.565145785280452]
ベクトル化トレースチェックに基づく早期故障検出のためのフレームワークを開発する。
このフレームワークは、最先端の手法と比較して、主要なパフォーマンス指標を2-10%改善している。
論文 参考訳(メタデータ) (2025-08-25T08:30:01Z) - State Sequences Prediction via Fourier Transform for Representation
Learning [111.82376793413746]
本研究では,表現表現を効率よく学習する新しい方法である,フーリエ変換(SPF)による状態列予測を提案する。
本研究では,状態系列における構造情報の存在を理論的に解析する。
実験により,提案手法はサンプル効率と性能の両面で,最先端のアルゴリズムよりも優れていることが示された。
論文 参考訳(メタデータ) (2023-10-24T14:47:02Z) - Scalable Learning of Latent Language Structure With Logical Offline
Cycle Consistency [71.42261918225773]
概念的には、LOCCOは、トレーニング対象のセマンティクスを使用してラベルなしテキストのアノテーションを生成する、自己学習の一形態と見なすことができる。
追加ボーナスとして、LOCCOによって生成されたアノテーションは、神経テキスト生成モデルをトレーニングするために自明に再利用することができる。
論文 参考訳(メタデータ) (2023-05-31T16:47:20Z) - Time-to-Green predictions for fully-actuated signal control systems with
supervised learning [56.66331540599836]
本稿では,集約信号とループ検出データを用いた時系列予測フレームワークを提案する。
我々は、最先端の機械学習モデルを用いて、将来の信号位相の持続時間を予測する。
スイスのチューリッヒの信号制御システムから得られた経験的データに基づいて、機械学習モデルが従来の予測手法より優れていることを示す。
論文 参考訳(メタデータ) (2022-08-24T07:50:43Z) - Linear Temporal Logic Modulo Theories over Finite Traces (Extended
Version) [72.38188258853155]
有限トレース(LTLf)上の線形時間論理について検討する。
命題の文字は任意の理論で解釈された一階述語式に置き換えられる。
Satisfiability Modulo Theories (LTLfMT) と呼ばれる結果の論理は半決定可能である。
論文 参考訳(メタデータ) (2022-04-28T17:57:33Z) - Real-Time Scene Text Detection with Differentiable Binarization and
Adaptive Scale Fusion [62.269219152425556]
セグメンテーションに基づくシーンテキスト検出手法はシーンテキスト検出分野において大きな注目を集めている。
本稿では,二項化処理をセグメンテーションネットワークに統合する分散二項化(DB)モジュールを提案する。
アダプティブ・スケール・フュージョン (ASF) モジュールは, 異なるスケールの特徴を適応的に融合させることにより, スケールのロバスト性を向上させる。
論文 参考訳(メタデータ) (2022-02-21T15:30:14Z) - Sequential convolutional network for behavioral pattern extraction in
gait recognition [0.7874708385247353]
個人の歩行パターンを学習するための逐次畳み込みネットワーク(SCN)を提案する。
SCNでは、時系列の中間特徴写像を理解するために行動情報抽出器(BIE)を構築している。
SCNのマルチフレームアグリゲータは、モバイル3D畳み込み層を介して、長さが不確定なシーケンス上の機能統合を実行する。
論文 参考訳(メタデータ) (2021-04-23T08:44:10Z) - CoCoMoT: Conformance Checking of Multi-Perspective Processes via SMT
(Extended Version) [62.96267257163426]
我々はCoCoMoT(Computing Conformance Modulo Theories)フレームワークを紹介する。
まず、純粋な制御フロー設定で研究したSATベースのエンコーディングを、データ認識ケースに持ち上げる方法を示す。
次に,プロパティ保存型クラスタリングの概念に基づく新しい前処理手法を提案する。
論文 参考訳(メタデータ) (2021-03-18T20:22:50Z) - Unsupervised Online Anomaly Detection On Irregularly Sampled Or Missing
Valued Time-Series Data Using LSTM Networks [0.0]
異常検出について検討し,変長,不規則なサンプルシーケンス,あるいは欠落した値を含むシーケンスを処理するアルゴリズムを提案する。
しかし,本アルゴリズムは完全に教師なしであり,教師付きあるいは半教師付きケースに容易に拡張できる。
論文 参考訳(メタデータ) (2020-05-25T09:41:04Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト(すべての情報・翻訳含む)の品質を保証せず、本サイト(すべての情報・翻訳含む)を使用して発生したあらゆる結果について一切の責任を負いません。