論文の概要: Monitoring Second-Order Hyperproperties

• arxiv url: http://arxiv.org/abs/2404.09652v1
• Date: Mon, 15 Apr 2024 10:33:39 GMT
• ステータス: 処理完了
• システム内更新日: 2024-04-16 12:40:28.478822
• Title: Monitoring Second-Order Hyperproperties
• Title（参考訳）: 2次ハイパープロパタイトモニタリング
• Authors: Raven Beutner, Bernd Finkbeiner, Hadar Frenkel, Niklas Metzger,
• Abstract要約: 本研究では,実行時の複雑なハイパープロパティのモニタリングについて検討する。 より表現力に富んだ2次超越性に対する最初のモニタリングアルゴリズムを提案する。 本稿では,Hyper$2$LTL$_f$の2次ハイパープロパティの監視を1次ハイパープロパティの監視に還元できることを示す。
• 参考スコア（独自算出の注目度）: 4.099848175176399
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: Hyperproperties express the relationship between multiple executions of a system. This is needed in many AI-related fields, such as knowledge representation and planning, to capture system properties related to knowledge, information flow, and privacy. In this paper, we study the monitoring of complex hyperproperties at runtime. Previous work in this area has either focused on the simpler problem of monitoring trace properties (which are sets of traces, while hyperproperties are sets of sets of traces) or on monitoring first-order hyperproperties, which are expressible in temporal logics with first-order quantification over traces, such as HyperLTL. We present the first monitoring algorithm for the much more expressive class of second-order hyperproperties. Second-order hyperproperties include system properties like common knowledge, which cannot be expressed in first-order logics like HyperLTL. We introduce Hyper$^2$LTL$_f$, a temporal logic over finite traces that allows for second-order quantification over sets of traces. We study the monitoring problem in two fundamental execution models: (1) the parallel model, where a fixed number of traces is monitored in parallel, and (2) the sequential model, where an unbounded number of traces is observed sequentially, one trace after the other. For the parallel model, we show that the monitoring of the second-order hyperproperties of Hyper$^2$LTL$_f$ can be reduced to monitoring first-order hyperproperties. For the sequential model, we present a monitoring algorithm that handles second-order quantification efficiently, exploiting optimizations based on the monotonicity of subformulas, graph-based storing of executions, and fixpoint hashing. We present experimental results from a range of benchmarks, including examples from common knowledge and planning.
• Abstract（参考訳）: ハイパープロパティは、システムの複数実行間の関係を表現する。 これは知識表現や計画など、多くのAI関連分野において、知識、情報フロー、プライバシに関連するシステム特性をキャプチャするために必要である。 本稿では,実行時の複雑なハイパープロパティのモニタリングについて検討する。 この領域におけるこれまでの研究は、トレース特性(トレースの集合であるが、ハイパープロパティはトレースの集合である)の監視のより単純な問題や、HyperLTLのようなトレース上の一階量子化を持つ時間論理で表現可能な一階のハイパープロパティの監視に重点を置いていた。 より表現力に富んだ2次超越性に対する最初のモニタリングアルゴリズムを提案する。 2階超越性には、共通知識のようなシステム特性が含まれており、HyperLTLのような一階述語論理では表現できない。 有限トレース上の時間論理であるHyper$^2$LTL$_f$を導入し、トレースの集合上の2階量子化を可能にする。 本研究では,(1)一定数のトレースを並列に監視する並列モデル,(2)非有界数のトレースを逐次観測する逐次モデル,の2つの基本実行モデルについて検討する。 並列モデルでは,Hyper$2$LTL$_f$の2次ハイパープロパティの監視を1次ハイパープロパティの監視に還元できることを示す。 逐次モデルでは, 2次量子化を効率的に処理し, サブフォーミュラの単調性, グラフベースの実行の保存, 固定点ハッシュに基づいて最適化を行う。 一般的な知識や計画の例を含む,さまざまなベンチマークによる実験結果を示す。

関連論文リスト

• Interaction Event Forecasting in Multi-Relational Recursive HyperGraphs: A Temporal Point Process Approach [12.142292322071299]
  本研究は,マルチリレーショナル再帰的ハイパーグラフにおける高次相互作用事象の予測問題に対処する。 提案したモデルであるtextitRelational Recursive Hyperedge Temporal Point Process (RRHyperTPP) は,歴史的相互作用パターンに基づいて動的ノード表現を学習するエンコーダを使用する。 我々は,従来のインタラクション予測手法よりも優れた性能を示すことを示す。
  論文  参考訳（メタデータ） (2024-04-27T15:46:54Z)
• TimeGraphs: Graph-based Temporal Reasoning [64.18083371645956]
  TimeGraphsは階層的時間グラフとして動的相互作用を特徴付ける新しいアプローチである。 提案手法は,コンパクトなグラフベース表現を用いて相互作用をモデル化し,多種多様な時間スケールでの適応推論を可能にする。 我々は,サッカーシミュレータ,抵抗ゲーム,MOMA人間活動データセットなど,複雑でダイナミックなエージェントインタラクションを持つ複数のデータセット上でTimeGraphsを評価する。
  論文  参考訳（メタデータ） (2024-01-06T06:26:49Z)
• Joint Entity and Relation Extraction with Span Pruning and Hypergraph Neural Networks [58.43972540643903]
  PLマーカ(最先端マーカーベースピプレリンモデル)上に構築されたEREのためのHyperGraphニューラルネットワーク(hgnn$)を提案する。 エラーの伝播を軽減するため,NERモジュールからのエンティティ識別とラベル付けの負担をモデルのジョイントモジュールに転送するために,ハイリコールプルーナー機構を用いる。 EREタスクに広く使用されている3つのベンチマークの実験は、以前の最先端のPLマーカーよりも大幅に改善されている。
  論文  参考訳（メタデータ） (2023-10-26T08:36:39Z)
• HyperAttention: Long-context Attention in Near-Linear Time [78.33061530066185]
  本稿では,長期的文脈の複雑さの増大に伴う計算課題に対処するため,HyperAttentionという近似的な注意機構を提案する。 実証的には、大規模なエントリを特定するためにLocality Sensitive Hashing(LSH)を使用して、HyperAttentionは既存のメソッドよりも優れています。 各種長文長データセットにおけるHyperAttentionの実証的性能を検証した。
  論文  参考訳（メタデータ） (2023-10-09T17:05:25Z)
• Unified Sequence-to-Sequence Learning for Single- and Multi-Modal Visual Object Tracking [64.28025685503376]
  SeqTrackは、ビジュアルトラッキングをシーケンス生成タスクとしてキャストし、オブジェクト境界ボックスを自動回帰的に予測する。 SeqTrackv2は補助モダリティのための統一インターフェースとタスクを指定するためのタスクプロンプトトークンのセットを統合している。 このシーケンス学習パラダイムは、トラッキングフレームワークを単純化するだけでなく、14の挑戦的なベンチマークで優れたパフォーマンスを示す。
  論文  参考訳（メタデータ） (2023-04-27T17:56:29Z)
• End-to-end Tracking with a Multi-query Transformer [96.13468602635082]
  マルチオブジェクトトラッキング(MOT)は、時間とともにシーン内のオブジェクトの位置、外観、アイデンティティを同時に推論する必要がある課題である。 本研究の目的は、トラッキング・バイ・ディテクト・アプローチを超えて、未知のオブジェクト・クラスに対してもよく機能するクラスに依存しないトラッキングへと移行することである。
  論文  参考訳（メタデータ） (2022-10-26T10:19:37Z)
• Multivariate Time Series Forecasting with Dynamic Graph Neural ODEs [65.18780403244178]
  動的グラフニューラル正規微分方程式(MTGODE)を用いた多変量時系列予測連続モデルを提案する。 具体的には、まず、時間進化するノードの特徴と未知のグラフ構造を持つ動的グラフに多変量時系列を抽象化する。 そして、欠落したグラフトポロジを補完し、空間的および時間的メッセージパッシングを統一するために、ニューラルODEを設計、解決する。
  論文  参考訳（メタデータ） (2022-02-17T02:17:31Z)
• Exploiting Multiple Timescales in Hierarchical Echo State Networks [0.0]
  エコー状態ネットワーク(ESN)は、線形出力重みのトレーニングのみを必要とする貯水池コンピューティングの強力な形態である。 ここでは,貯水池を2つの小さな貯水池に分割した階層型esnの時間スケールを考察する。
  論文  参考訳（メタデータ） (2021-01-11T22:33:17Z)
• Analyzing Unaligned Multimodal Sequence via Graph Convolution and Graph Pooling Fusion [28.077474663199062]
  本稿では,マルチモーダルシーケンシャルデータモデリングにおけるグラフニューラルネットワーク(GNN)の有効性を検討するために,マルチモーダルグラフと呼ばれる新しいモデルを提案する。 グラフベースのモデルは、2つのベンチマークデータセット上で最先端のパフォーマンスに達する。
  論文  参考訳（メタデータ） (2020-11-27T06:12:14Z)

関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。

指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。