論文の概要: OCTAL: Graph Representation Learning for LTL Model Checking

• arxiv url: http://arxiv.org/abs/2207.11649v1
• Date: Sun, 24 Jul 2022 03:34:21 GMT
• ステータス: 処理完了
• システム内更新日: 2022-07-26 16:06:52.143845
• Title: OCTAL: Graph Representation Learning for LTL Model Checking
• Title（参考訳）: OCTAL:LTLモデル検査のためのグラフ表現学習
• Authors: Prasita Mukherjee, Haoteng Yin, Susheel Suresh, Tiark Rompf
• Abstract要約: 本稿では,線形時間論理(LTL)モデルチェックの解法としてグラフ表現学習(GRL)を提案する。 新たなGRLベースのフレームワークOCTALは、グラフ構造化システムと仕様の表現を学習するために設計されている。 実験により、OCTALは3つの異なるデータセット上の標準SOTAモデルチェッカーに対して同等の精度を達成することが示された。
• 参考スコア（独自算出の注目度）: 7.0827687977843645
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: Model Checking is widely applied in verifying the correctness of complex and concurrent systems against a specification. Pure symbolic approaches while popular, still suffer from the state space explosion problem that makes them impractical for large scale systems and/or specifications. In this paper, we propose to use graph representation learning (GRL) for solving linear temporal logic (LTL) model checking, where the system and the specification are expressed by a B\"uchi automaton and an LTL formula respectively. A novel GRL-based framework OCTAL, is designed to learn the representation of the graph-structured system and specification, which reduces the model checking problem to binary classification in the latent space. The empirical experiments show that OCTAL achieves comparable accuracy against canonical SOTA model checkers on three different datasets, with up to $5\times$ overall speedup and above $63\times$ for satisfiability checking alone.
• Abstract（参考訳）: モデルチェックは、複雑なシステムと並行システムの仕様に対する正確性を検証するのに広く適用されます。 純粋なシンボリックアプローチは人気があるものの、大規模システムや仕様では実用的でない状態空間爆発の問題に苦しんでいる。 本稿では,線形時相論理(ltl)モデルチェックにおけるグラフ表現学習(grl)を用いて,システムと仕様をそれぞれb\"uchiオートマトンとltl式で表現する手法を提案する。 新たなGRLベースのフレームワークOCTALは、グラフ構造化システムと仕様の表現を学習するために設計されており、モデルチェック問題を潜在空間におけるバイナリ分類に還元する。 実験の結果、octalは3つの異なるデータセットで標準のsomaモデルチェッカーと同等の精度を達成し、最高で$5\times$のスピードアップと$63\times$以上の満足度チェックが可能となった。

関連論文リスト

• Computational-Statistical Gaps in Gaussian Single-Index Models [77.1473134227844]
  単次元モデル(Single-Index Models)は、植木構造における高次元回帰問題である。 我々は,統計的クエリ (SQ) と低遅延多項式 (LDP) フレームワークの両方において,計算効率のよいアルゴリズムが必ずしも$Omega(dkstar/2)$サンプルを必要とすることを示した。
  論文  参考訳（メタデータ） (2024-03-08T18:50:19Z)
• Learning Interpretable Rules for Scalable Data Representation and Classification [11.393431987232425]
  ルールベースのLearner Representation (RRL)は、データ表現と分類のための解釈可能な非ファジィ規則を学習する。 RRLは容易に調整でき、異なるシナリオの分類精度とモデルの複雑さのトレードオフを得ることができる。
  論文  参考訳（メタデータ） (2023-10-22T15:55:58Z)
• OCTAL: Graph Representation Learning for LTL Model Checking [5.22145960878624]
  GRLベースの新しいフレームワークモデルは、グラフ構造化システムと仕様の表現を学習するために設計されている。 実験により、モデルが有望な精度を達成し、標準SOTAモデルチェッカーに対する全体的なスピードアップが最大で11倍になることが示された。
  論文  参考訳（メタデータ） (2023-08-19T15:11:18Z)
• Single-Stage Visual Relationship Learning using Conditional Queries [60.90880759475021]
  TraCQは、マルチタスク学習問題とエンティティペアの分布を回避する、シーングラフ生成の新しい定式化である。 我々は,DETRをベースとしたエンコーダ-デコーダ条件付きクエリを用いて,エンティティラベル空間を大幅に削減する。 実験結果から、TraCQは既存のシングルステージシーングラフ生成法よりも優れており、Visual Genomeデータセットの最先端の2段階メソッドを多く上回っていることがわかった。
  論文  参考訳（メタデータ） (2023-06-09T06:02:01Z)
• Automated classification of pre-defined movement patterns: A comparison between GNSS and UWB technology [55.41644538483948]
  リアルタイム位置情報システム(RTLS)は、人間の動きパターンからデータを収集することができる。 本研究の目的は、小さな領域における人間の動きパターンを分類する自動化された枠組みを設計し、評価することである。
  論文  参考訳（メタデータ） (2023-03-10T14:46:42Z)
• uGLAD: Sparse graph recovery by optimizing deep unrolled networks [11.48281545083889]
  深層ネットワークを最適化してスパースグラフ復元を行う新しい手法を提案する。 我々のモデルであるuGLADは、最先端モデルGLADを教師なし設定に構築し、拡張します。 我々は, 遺伝子調節ネットワークから生成した合成ガウスデータ, 非ガウスデータを用いて, モデル解析を行い, 嫌気性消化の事例研究を行った。
  論文  参考訳（メタデータ） (2022-05-23T20:20:27Z)
• Low-Rank Constraints for Fast Inference in Structured Models [110.38427965904266]
  この研究は、大規模構造化モデルの計算とメモリの複雑さを低減するための単純なアプローチを示す。 言語モデリング,ポリフォニック・ミュージック・モデリング,教師なし文法帰納法,ビデオ・モデリングのためのニューラルパラメータ構造モデルを用いた実験により,我々の手法は大規模状態空間における標準モデルの精度と一致することを示した。
  論文  参考訳（メタデータ） (2022-01-08T00:47:50Z)
• Sketching as a Tool for Understanding and Accelerating Self-attention for Long Sequences [52.6022911513076]
  トランスフォーマーベースのモデルは、自己アテンションモジュールの二次空間と時間的複雑さのために、長いシーケンスを処理するのに効率的ではない。 我々はLinformerとInformerを提案し、低次元投影と行選択により2次複雑性を線形(モジュラー対数因子)に還元する。 理論的解析に基づいて,Skeinformerを提案することにより,自己注意の促進と,自己注意への行列近似の精度の向上を図ることができる。
  論文  参考訳（メタデータ） (2021-12-10T06:58:05Z)
• Scalable Rule-Based Representation Learning for Interpretable Classification [12.736847587988853]
  ルールベースのLearner Representation (RRL)は、データ表現と分類のための解釈可能な非ファジィ規則を学習する。 RRLは容易に調整でき、異なるシナリオの分類精度とモデルの複雑さのトレードオフを得ることができる。
  論文  参考訳（メタデータ） (2021-09-30T13:07:42Z)
• Understanding Dynamics of Nonlinear Representation Learning and Its Application [12.697842097171119]
  暗黙的非線形表現学習のダイナミクスについて検討する。 我々は,データ構造アライメント条件がグローバル収束に十分であることを示す。 我々はデータ構造アライメント条件を満たす新しいトレーニングフレームワークを作成した。
  論文  参考訳（メタデータ） (2021-06-28T16:31:30Z)
• Spatial-spectral Hyperspectral Image Classification via Multiple Random Anchor Graphs Ensemble Learning [88.60285937702304]
  本稿では,複数のランダムアンカーグラフアンサンブル学習(RAGE)を用いた空間スペクトルHSI分類手法を提案する。 まず、各選択されたバンドのより記述的な特徴を抽出し、局所的な構造と領域の微妙な変化を保存するローカルバイナリパターンを採用する。 次に,アンカーグラフの構成に適応隣接代入を導入し,計算複雑性を低減した。
  論文  参考訳（メタデータ） (2021-03-25T09:31:41Z)

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

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