論文の概要: Program Dependence Net and On-demand Slicing for Property Verification of Concurrent System and Software

• arxiv url: http://arxiv.org/abs/2301.11723v2
• Date: Wed, 15 Nov 2023 09:45:41 GMT
• ステータス: 処理完了
• システム内更新日: 2023-11-16 21:04:54.993528
• Title: Program Dependence Net and On-demand Slicing for Property Verification of Concurrent System and Software
• Title（参考訳）: コンカレントシステムとソフトウェアのプロパティ検証のためのプログラム依存ネットとオンデマンドスライシング
• Authors: Zhijun Ding, Shuo Li, Cheng Chen and Cong He
• Abstract要約: ペトリネット理論に基づくプログラム依存ネット(PDNet)を提案する。 PDNetは、コンバージョンを避けるために、制御フロー構造と依存関係を組み合わせる。 本稿では,PDNetスライシング手法を提案する。
• 参考スコア（独自算出の注目度）: 8.569594114587504
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: When checking concurrent software using a finite-state model, we face a formidable state explosion problem. One solution to this problem is dependence-based program slicing, whose use can effectively reduce verification time. It is orthogonal to other model-checking reduction techniques. However, when slicing concurrent programs for model checking, there are conversions between multiple irreplaceable models, and dependencies need to be found for variables irrelevant to the verified property, which results in redundant computation. To resolve this issue, we propose a Program Dependence Net (PDNet) based on Petri net theory. It is a unified model that combines a control-flow structure with dependencies to avoid conversions. For reduction, we present a PDNet slicing method to capture the relevant variables' dependencies when needed. PDNet in verifying linear temporal logic and its on-demand slicing can be used to significantly reduce computation cost. We implement a model-checking tool based on PDNet and its on-demand slicing, and validate the advantages of our proposed methods.
• Abstract（参考訳）: 有限状態モデルを用いて並行ソフトウェアをチェックするとき、我々は恐ろしい状態爆発問題に直面する。 この問題に対する1つの解決策は依存型プログラムスライシングであり、その使用は検証時間を効果的に削減できる。 他のモデルチェックの削減手法と直交する。 しかし、モデルチェックのために並列プログラムをスライシングする場合、複数の非置換可能なモデルの間で変換が行われ、検証されたプロパティとは無関係な変数に対して依存関係を見つける必要がある。 そこで本研究では,ペトリネット理論に基づくプログラム依存ネット(PDNet)を提案する。 変換を避けるために、制御フロー構造と依存関係を組み合わせた統一モデルである。 そこで本研究では,PDNetスライシング手法を用いて,変数の依存関係を抽出する手法を提案する。 線形時相論理とそのオンデマンドスライシングを検証するpdnetは、計算コストを大幅に削減することができる。 我々は,pdnetに基づくモデルチェックツールとそのオンデマンドスライシングを実装し,提案手法の利点を検証する。

関連論文リスト

• RL-Pruner: Structured Pruning Using Reinforcement Learning for CNN Compression and Acceleration [0.0]
  RL-Prunerを提案する。このRL-Prunerは、強化学習を用いて最適プルーニング分布を学習する。 RL-Prunerは、モデル固有のプルーニング実装を必要とせずに、入力モデル内のフィルタ間の依存関係を自動的に抽出し、プルーニングを実行する。
  論文  参考訳（メタデータ） (2024-11-10T13:35:10Z)
• Augmenting Interpolation-Based Model Checking with Auxiliary Invariants (Extended Version) [4.309079367183251]
  モデル検査に外部不変量を注入する拡張型検証アルゴリズムを提案する。 インジェクション不変により安全性の証明に必要なクエリ数が削減され,実行時の効率が向上することがわかった。
  論文  参考訳（メタデータ） (2024-03-12T17:02:53Z)
• Retentive Network: A Successor to Transformer for Large Language Models [91.6652200825638]
  大規模言語モデルの基盤アーキテクチャとしてRetentive Network(RetNet)を提案する。 理論的には、再発と注意の関係を導出する。 言語モデリングの実験結果から、RetNetは優れたスケーリング結果、並列トレーニング、低コストなデプロイメント、効率的な推論を実現している。
  論文  参考訳（メタデータ） (2023-07-17T16:40:01Z)
• Automating Model Comparison in Factor Graphs [3.119859292303397]
  本稿では,Forney型因子グラフ上のメッセージパッシングによるベイズモデルの平均化,選択,組み合わせを,独自の混合ノードで効率的に自動化する。 このアプローチは、モデル設計サイクルを短縮し、複雑な時間変化のプロセスをモデル化するために、階層的および時間的モデルへの直接拡張を可能にする。
  論文  参考訳（メタデータ） (2023-06-09T15:33:30Z)
• Cheaply Evaluating Inference Efficiency Metrics for Autoregressive Transformer APIs [66.30706841821123]
  大規模言語モデル(LLM)は、自然言語処理において多くの最先端システムに電力を供給する。 LLMは、推論時でさえ非常に計算コストが高い。 モデル間での推論効率を比較するための新しい指標を提案する。
  論文  参考訳（メタデータ） (2023-05-03T21:51:42Z)
• LegoNet: A Fast and Exact Unlearning Architecture [59.49058450583149]
  機械学習は、トレーニングされたモデルから削除された要求に対する特定のトレーニングサンプルの影響を削除することを目的としている。 固定エンコーダ+複数アダプタのフレームワークを採用した新しいネットワークである textitLegoNet を提案する。 我々は、LegoNetが許容できる性能を維持しつつ、高速かつ正確な未学習を実現し、未学習のベースラインを総合的に上回っていることを示す。
  論文  参考訳（メタデータ） (2022-10-28T09:53:05Z)
• Interpretations Steered Network Pruning via Amortized Inferred Saliency Maps [85.49020931411825]
  限られたリソースを持つエッジデバイスにこれらのモデルをデプロイするには、畳み込みニューラルネットワーク(CNN)圧縮が不可欠である。 本稿では,新しい視点からチャネルプルーニング問題に対処するために,モデルの解釈を活用して,プルーニング過程を解析する手法を提案する。 本研究では,実時間スムーズなスムーズなスムーズなスムーズなマスク予測を行うセレクタモデルを導入することで,この問題に対処する。
  論文  参考訳（メタデータ） (2022-09-07T01:12:11Z)
• Manifold Regularized Dynamic Network Pruning [102.24146031250034]
  本稿では,全インスタンスの多様体情報をプルーンドネットワークの空間に埋め込むことにより,冗長フィルタを動的に除去する新しいパラダイムを提案する。 提案手法の有効性をいくつかのベンチマークで検証し,精度と計算コストの両面で優れた性能を示す。
  論文  参考訳（メタデータ） (2021-03-10T03:59:03Z)
• The Right Tool for the Job: Matching Model and Instance Complexities [62.95183777679024]
  NLPモデルが大きくなればなるほど、訓練されたモデルを実行するには、金銭的・環境的なコストを発生させる重要な計算資源が必要である。 我々は、推論中、早期(かつ高速)の"exit"を可能にする文脈表現微調整の修正を提案する。 3つのテキスト分類データセットと2つの自然言語推論ベンチマークの2つのタスクで、5つの異なるデータセットに対して提案した修正を検証した。
  論文  参考訳（メタデータ） (2020-04-16T04:28:08Z)
• Controlling Computation versus Quality for Neural Sequence Models [42.525463454120256]
  条件付き計算は、推論中にニューラルシーケンスモデル(トランスフォーマー)をより効率的かつ計算に適応させる。 i)WMT英仏訳と(ii)教師なし表現学習(BERT)の2つの課題に対するアプローチを評価する。
  論文  参考訳（メタデータ） (2020-02-17T17:54:27Z)

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

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