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

• arxiv url: http://arxiv.org/abs/2308.13474v1
• Date: Sat, 19 Aug 2023 15:11:18 GMT
• ステータス: 処理完了
• システム内更新日: 2023-09-03 21:42:44.745096
• Title: OCTAL: Graph Representation Learning for LTL Model Checking
• Title（参考訳）: OCTAL:LTLモデル検査のためのグラフ表現学習
• Authors: Prasita Mukherjee and Haoteng Yin
• Abstract要約: GRLベースの新しいフレームワークモデルは、グラフ構造化システムと仕様の表現を学習するために設計されている。 実験により、モデルが有望な精度を達成し、標準SOTAモデルチェッカーに対する全体的なスピードアップが最大で11倍になることが示された。
• 参考スコア（独自算出の注目度）: 5.22145960878624
• 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, suffer from the state space explosion problem due to cross product operations required that make them prohibitively expensive 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{\"u}chi automaton and an LTL formula, respectively. A novel GRL-based framework \model, is designed to learn the representation of the graph-structured system and specification, which reduces the model checking problem to binary classification. Empirical experiments on two model checking scenarios show that \model achieves promising accuracy, with up to $11\times$ overall speedup against canonical SOTA model checkers and $31\times$ for satisfiability checking alone.
• Abstract（参考訳）: モデルチェックは、複雑なシステムと並行システムの仕様に対する正確性を検証するのに広く適用されます。 純粋なシンボリックアプローチは人気があるものの、大規模システムや/または仕様に制限的にコストがかかるようなクロスプロダクト操作が必要なため、国家空間の爆発的な問題に苦しめられている。 本稿では,線形時相論理(ltl)モデルチェックにおけるグラフ表現学習(grl)を用いて,システムと仕様をそれぞれb{\"u}chiオートマトンとltl式で表現する手法を提案する。 GRLベースの新しいフレームワーク \model は、グラフ構造化システムと仕様の表現を学習するために設計されており、モデルチェック問題を二項分類に還元する。 2つのモデルチェックシナリオに関する実証実験は、 \modelが有望な精度を達成し、標準SOTAモデルチェッカーに対する全体的なスピードアップが最大11ドル、満足度チェッカーだけで311ドルであることを示している。

関連論文リスト

• 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)
• Representing Timed Automata and Timing Anomalies of Cyber-Physical Production Systems in Knowledge Graphs [51.98400002538092]
  本稿では,学習されたタイムドオートマトンとシステムに関する公式知識グラフを組み合わせることで,CPPSのモデルベース異常検出を改善することを目的とする。 モデルと検出された異常の両方を知識グラフに記述し、モデルと検出された異常をより容易に解釈できるようにする。
  論文  参考訳（メタデータ） (2023-08-25T15:25:57Z)
• Single-Stage Visual Relationship Learning using Conditional Queries [60.90880759475021]
  TraCQは、マルチタスク学習問題とエンティティペアの分布を回避する、シーングラフ生成の新しい定式化である。 我々は,DETRをベースとしたエンコーダ-デコーダ条件付きクエリを用いて,エンティティラベル空間を大幅に削減する。 実験結果から、TraCQは既存のシングルステージシーングラフ生成法よりも優れており、Visual Genomeデータセットの最先端の2段階メソッドを多く上回っていることがわかった。
  論文  参考訳（メタデータ） (2023-06-09T06:02:01Z)
• OCTAL: Graph Representation Learning for LTL Model Checking [7.0827687977843645]
  本稿では,線形時間論理(LTL)モデルチェックの解法としてグラフ表現学習(GRL)を提案する。 新たなGRLベースのフレームワークOCTALは、グラフ構造化システムと仕様の表現を学習するために設計されている。 実験により、OCTALは3つの異なるデータセット上の標準SOTAモデルチェッカーに対して同等の精度を達成することが示された。
  論文  参考訳（メタデータ） (2022-07-24T03:34:21Z)
• 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)
• Sparse Universum Quadratic Surface Support Vector Machine Models for Binary Classification [0.0]
  カーネルフリーな2次曲面サポートベクターマシンモデルを設計する。 二次曲面のヘシアンにおける潜在的空間パターンの検出に有用であるL1ノルム正規化版を提案する。 提案モデルの実現可能性と有効性を示すために、人工的および公共のベンチマークデータセットの数値実験を実施します。
  論文  参考訳（メタデータ） (2021-04-03T07:40:30Z)
• Learning Gaussian Graphical Models via Multiplicative Weights [54.252053139374205]
  乗算重み更新法に基づいて,Klivans と Meka のアルゴリズムを適用した。 アルゴリズムは、文献の他のものと質的に類似したサンプル複雑性境界を楽しみます。 ランタイムが低い$O(mp2)$で、$m$サンプルと$p$ノードの場合には、簡単にオンライン形式で実装できる。
  論文  参考訳（メタデータ） (2020-02-20T10:50:58Z)

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

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