論文の概要: Distributed Monitoring of Timed Properties
- arxiv url: http://arxiv.org/abs/2410.00465v1
- Date: Tue, 1 Oct 2024 07:46:59 GMT
- ステータス: 処理完了
- システム内更新日: 2024-11-05 05:27:01.777376
- Title: Distributed Monitoring of Timed Properties
- Title(参考訳): 時間特性の分散モニタリング
- Authors: Léo Henry, Thierry Jéron, Nicolas Markey, Victor Roussanaly,
- Abstract要約: ランタイム監視は、あるプロパティを満たすかどうかをできるだけ早く決定するために、システムの実行を観察することで構成される。
我々は、到達性タイムドオートマトンとして与えられるプロパティについて、分散環境でのモニタリングを検討する。
本稿では,時間特性のオンラインモニタリングアルゴリズムを提案する。
- 参考スコア(独自算出の注目度): 0.22499166814992436
- License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
- Abstract: In formal verification, runtime monitoring consists of observing the execution of a system in order to decide as quickly as possible whether or not it satisfies a given property. We consider monitoring in a distributed setting, for properties given as reachability timed automata. In such a setting, the system is made of several components, each equipped with its own local clock and monitor. The monitors observe events occurring on their associated component, and receive timestamped events from other monitors through FIFO channels. Since clocks are local, they cannot be perfectly synchronized, resulting in imprecise timestamps. Consequently, they must be seen as intervals, leading monitors to consider possible reorderings of events. In this context, each monitor aims to provide, as early as possible, a verdict on the property it is monitoring, based on its potentially incomplete and imprecise knowledge of the current execution. In this paper, we propose an on-line monitoring algorithm for timed properties, robust to time imprecision and partial information from distant components. We first identify the date at which a monitor can safely compute a verdict based on received events. We then propose a monitoring algorithm that updates this date when new information arrives, maintains the current set of states in which the property can reside, and updates its verdict accordingly.
- Abstract(参考訳): 正式な検証では、ランタイム監視は、あるプロパティを満たすかどうかをできるだけ早く決定するために、システムの実行を観察する。
我々は、到達性タイムドオートマトンとして与えられるプロパティについて、分散環境でのモニタリングを検討する。
このような環境では、システムは複数のコンポーネントで構成され、それぞれ独自のローカルクロックとモニターを備えている。
モニタは、関連するコンポーネントで発生したイベントを観察し、他のモニタからFIFOチャネルを介してタイムスタンプされたイベントを受け取る。
クロックは局所的であるため、完全に同期することはできず、不正確なタイムスタンプとなる。
結果として、それらはインターバルと見なされなければならず、モニターはイベントの再注文を考慮せざるを得ない。
このコンテキストでは、各モニタは、現在の実行に関する潜在的に不完全で不正確な知識に基づいて、可能な限り早く、監視しているプロパティに関する判断を提供することを目的としている。
本稿では,時間特性のオンラインモニタリングアルゴリズムを提案する。
まず、受信したイベントに基づいて、モニターが安全に判定を計算できる日付を特定する。
次に、新しい情報が到着したときのこの日時を更新し、プロパティが居住可能な状態の現在のセットを維持し、それに応じて判断を更新する監視アルゴリズムを提案する。
関連論文リスト
- Tooling Offline Runtime Verification against Interaction Models :
recognizing sliced behaviors using parameterized simulation [0.4199844472131921]
オフライン実行時の検証には、仕様に対するシステムの実行の静的解析が含まれる。
分散システムでは、グローバルクロックが存在しないため、グローバルトレースの形での実行を特徴付けることは一般的に不可能である。
本稿では,インタラクションと呼ばれる形式仕様に対して,そのようなトレースの適合性を検証するアルゴリズムを提案する。
論文 参考訳(メタデータ) (2024-03-05T16:09:55Z) - Sound Concurrent Traces for Online Monitoring Technical Report [0.0]
並列プログラムは通常、抽象的なプログラム実行のためのトレースの収集に依存します。
まず、トレースが並列実行を表すときの概念を定義します。
次に,非ブロッキングベクトルクロックアルゴリズムを提案し,音の同時トレースをハエで収集する。
論文 参考訳(メタデータ) (2024-02-28T15:11:39Z) - Monitoring Algorithmic Fairness under Partial Observations [3.790015813774933]
実行時検証技術は、デプロイされたシステムのアルゴリズム的公正性を監視するために導入された。
従来の監視技術は、監視されたシステムの状態の完全な可観測性を前提としている。
我々は、部分的に観測されたマルコフ連鎖としてモデル化されたシステムにフェアネスモニタリングを拡張した。
論文 参考訳(メタデータ) (2023-08-01T07:35:54Z) - Runtime Monitoring of Dynamic Fairness Properties [3.372200852710289]
静的意思決定タスクで公平なマシン学習システムは、長期にわたる社会的影響に偏っている可能性がある。
既存の研究は、スマートシステム設計による長期バイアスの特定と緩和を目的としているが、我々は、リアルタイムに公正さを監視する技術を導入している。
私たちのゴールは、システムによって生成されるイベントの長いシーケンスを継続的に観察するモニターを構築し、デプロイすることにあります。
論文 参考訳(メタデータ) (2023-05-08T13:32:23Z) - End-to-end Tracking with a Multi-query Transformer [96.13468602635082]
マルチオブジェクトトラッキング(MOT)は、時間とともにシーン内のオブジェクトの位置、外観、アイデンティティを同時に推論する必要がある課題である。
本研究の目的は、トラッキング・バイ・ディテクト・アプローチを超えて、未知のオブジェクト・クラスに対してもよく機能するクラスに依存しないトラッキングへと移行することである。
論文 参考訳(メタデータ) (2022-10-26T10:19:37Z) - A Generalized & Robust Framework For Timestamp Supervision in Temporal
Action Segmentation [79.436224998992]
時間的アクションセグメンテーションでは、Timestampの監督はビデオシーケンスごとにわずかにラベル付きフレームを必要とする。
本稿では,未ラベルフレームのラベルの不確実性を利用した期待最大化に基づく新しい手法を提案する。
提案手法はSOTA結果を生成し,複数のメトリクスやデータセットの完全教師付き設定を超えている。
論文 参考訳(メタデータ) (2022-07-20T18:30:48Z) - Towards Partial Monitoring: It is Always too Soon to Give Up [0.0]
本稿では,監視可能性の概念を実践的観点から再考する。
監視不能なプロパティが部分的なモニタを生成するためにどのように使用できるかを示し、そのプロパティを部分的にチェックする。
論文 参考訳(メタデータ) (2021-10-25T01:55:05Z) - Content-Based Detection of Temporal Metadata Manipulation [91.34308819261905]
画像の撮像時間とその内容と地理的位置とが一致しているかどうかを検証するためのエンドツーエンドのアプローチを提案する。
中心となる考え方は、画像の内容、キャプチャ時間、地理的位置が一致する確率を予測するための教師付き一貫性検証の利用である。
我々のアプローチは、大規模なベンチマークデータセットの以前の作業により改善され、分類精度が59.03%から81.07%に向上した。
論文 参考訳(メタデータ) (2021-03-08T13:16:19Z) - Predicting Temporal Sets with Deep Neural Networks [50.53727580527024]
本稿では,時間集合予測のためのディープニューラルネットワークに基づく統合解を提案する。
ユニークな視点は、セットレベルの共起グラフを構築することで要素関係を学ぶことである。
我々は,要素や集合の時間依存性を適応的に学習するアテンションベースのモジュールを設計する。
論文 参考訳(メタデータ) (2020-06-20T03:29:02Z) - Towards Streaming Perception [70.68520310095155]
本稿では、リアルタイムオンライン知覚のための単一のメトリクスにレイテンシと精度を協調的に統合するアプローチを提案する。
この指標の背後にある重要な洞察は、瞬間ごとに認識スタック全体の出力を共同で評価することである。
本稿では,都市ビデオストリームにおけるオブジェクト検出とインスタンスセグメンテーションの具体的タスクに注目し,高品質で時間依存的なアノテーションを備えた新しいデータセットを寄贈する。
論文 参考訳(メタデータ) (2020-05-21T01:51:35Z) - Convergence of Update Aware Device Scheduling for Federated Learning at
the Wireless Edge [84.55126371346452]
遠隔パラメータサーバ(PS)の助けを借りて、ローカルデータセットを持つパワー制限デバイスが共同でジョイントモデルを訓練する無線エッジにおけるフェデレーション学習について研究する。
各ラウンドで送信するデバイスのサブセットを決定する新しいスケジューリングとリソース割り当てポリシーを設計する。
数値実験の結果,提案したスケジューリングポリシーは,チャネル条件と局所モデル更新の重要性の両方に基づいており,両者の指標のみに基づくスケジューリングポリシーよりも長期的性能がよいことがわかった。
論文 参考訳(メタデータ) (2020-01-28T15:15:22Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト(すべての情報・翻訳含む)の品質を保証せず、本サイト(すべての情報・翻訳含む)を使用して発生したあらゆる結果について一切の責任を負いません。