論文の概要: Regular Abstractions for Array Systems

• arxiv url: http://arxiv.org/abs/2401.02618v1
• Date: Fri, 5 Jan 2024 03:35:55 GMT
• ステータス: 処理完了
• システム内更新日: 2024-01-08 16:06:15.037631
• Title: Regular Abstractions for Array Systems
• Title（参考訳）: 配列システムの規則的抽象化
• Authors: Chih-Duo Hong, Anthony W. Lin
• Abstract要約: 本研究では,アレーシステム上での安全性と生存性を証明する新しいフレームワークを開発する。 フレームワークの要点は、配列システムを文字列書き換えシステムとしてオーバー近似することである。 これにより、文字列書き換えシステムの強力な検証手法を利用できる。
• 参考スコア（独自算出の注目度）: 0.0
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: Verifying safety and liveness over array systems is a highly challenging problem. Array systems naturally capture parameterized systems such as distributed protocols with an unbounded number of processes. Such distributed protocols often exploit process IDs during their computation, resulting in array systems whose element values range over an infinite domain. In this paper, we develop a novel framework for proving safety and liveness over array systems. The crux of the framework is to overapproximate an array system as a string rewriting system (i.e. over a finite alphabet) by means of a new predicate abstraction that exploits the so-called indexed predicates. This allows us to tap into powerful verification methods for string rewriting systems that have been heavily developed in the last few decades (e.g. regular model checking). We demonstrate how our method yields simple, automatically verifiable proofs of safety and liveness properties for challenging examples, including Dijkstra's self-stabilizing protocol and the Chang-Roberts leader election protocol.
• Abstract（参考訳）: 配列システムに対する安全性と生存性を検証することは、非常に難しい問題である。 配列システムは、無制限のプロセスを持つ分散プロトコルのようなパラメータ化されたシステムを自然にキャプチャする。 このような分散プロトコルは、計算中にプロセスIDを利用することが多く、その結果、要素値が無限のドメインにまたがる配列システムとなる。 本稿では,アレーシステム上での安全性と生存性を証明する新しいフレームワークを開発する。 このフレームワークの要点は、配列システムを文字列書き換えシステム(つまり有限アルファベット上の)として、いわゆるインデックス付き述語を利用する新しい述語抽象化によって過剰に近似することである。 これにより、過去数十年の間に大きく開発されてきた文字列書き換えシステム(例:正規モデルチェック)の強力な検証手法を利用できる。 本稿では,Dijkstra の自己安定化プロトコルや Chang-Roberts の指導者選挙プロトコルなど,難題に対する安全性と生活性の簡易かつ自動検証可能な証明方法を示す。

関連論文リスト

• Bisimulation Learning [55.859538562698496]
  我々は、大きな、潜在的に無限の状態空間を持つ状態遷移系の有限バイシミュレートを計算する。 提案手法は,実際に行われている他の最先端ツールよりも高速な検証結果が得られる。
  論文  参考訳（メタデータ） (2024-05-24T17:11:27Z)
• Bridging the Gap: Automated Analysis of Sancus [2.045495982086173]
  本研究では,サンクスの組込みセキュリティアーキテクチャにおけるこのギャップを減らすための新しい手法を提案する。 我々の手法は、与えられた脅威モデルにおける攻撃を見つけるか、システムのセキュリティに対する確率的保証を与える。
  論文  参考訳（メタデータ） (2024-04-15T07:26:36Z)
• A Hypergraph-based Formalization of Hierarchical Reactive Modules and a Compositional Verification Method [0.30458514384586394]
  サイバー物理システムのモデル化によく使用される階層構造を持つ同期システムに対処する。 反応加群の理論を再検討し,それをハイパーグラフに基づいて再構成し,モジュールの並列構成と階層的記述を明らかにする。 階層型システムの自動検証手法を提案する。
  論文  参考訳（メタデータ） (2024-03-16T13:10:41Z)
• RelayAttention for Efficient Large Language Model Serving with Long System Prompts [59.50256661158862]
  本稿では,長いシステムプロンプトを含むLCMサービスの効率を向上させることを目的とする。 これらのシステムプロンプトの処理には、既存の因果注意アルゴリズムにおいて、大量のメモリアクセスが必要である。 本稿では,DRAMから入力トークンのバッチに対して,DRAMから隠れた状態を正確に1回読み取ることのできるアテンションアルゴリズムであるRelayAttentionを提案する。
  論文  参考訳（メタデータ） (2024-02-22T18:58:28Z)
• Reverse-Engineering Decoding Strategies Given Blackbox Access to a Language Generation System [73.52878118434147]
  テキスト生成に使用する復号法をリバースエンジニアリングする手法を提案する。 どのようなデコード戦略が使われたかを検出する能力は、生成されたテキストを検出することに影響を及ぼす。
  論文  参考訳（メタデータ） (2023-09-09T18:19:47Z)
• Outline, Then Details: Syntactically Guided Coarse-To-Fine Code Generation [61.50286000143233]
  ChainCoderは、Pythonコードを段階的に生成するプログラム合成言語モデルである。 自然言語記述と構文的に整合したI/Oデータサンプルを共同で符号化するために、カスタマイズされたトランスフォーマーアーキテクチャを利用する。
  論文  参考訳（メタデータ） (2023-04-28T01:47:09Z)
• Dealing with Collinearity in Large-Scale Linear System Identification Using Gaussian Regression [3.04585143845864]
  複数の相互接続型動的システムからなるネットワークの推定について検討する。 我々は、任意のインパルス応答をゼロ平均ガウス過程の実現と見なすベイズ正規化フレームワークにキャストされた戦略を開発する。 我々はマルコフ連鎖モンテカルロスキームを設計し、コリナリティを効率的に扱うことでインパルス応答を後方に再構築する。
  論文  参考訳（メタデータ） (2023-02-21T19:35:47Z)
• Autoregressive Search Engines: Generating Substrings as Document Identifiers [53.0729058170278]
  自動回帰言語モデルは、回答を生成するデファクト標準として現れています。 これまでの研究は、探索空間を階層構造に分割する方法を探究してきた。 本研究では,検索空間の任意の構造を強制しない代替として,経路内のすべてのngramを識別子として使用することを提案する。
  論文  参考訳（メタデータ） (2022-04-22T10:45:01Z)
• Discovering Non-monotonic Autoregressive Orderings with Variational Inference [67.27561153666211]
  我々は、訓練データから高品質な生成順序を純粋に検出する、教師なし並列化可能な学習装置を開発した。 エンコーダを非因果的注意を持つトランスフォーマーとして実装し、1つのフォワードパスで置換を出力する。 言語モデリングタスクにおける経験的結果から,我々の手法は文脈認識であり,一定の順序と競合する,あるいはより優れた順序を見つけることができる。
  論文  参考訳（メタデータ） (2021-10-27T16:08:09Z)
• Self-Supervised Learning to Prove Equivalence Between Straight-Line Programs via Rewrite Rules [9.1570563482476]
  2つのプログラムは、1つのプログラムをもう1つのプログラムに書き換える、書き換え規則の一連の適用が存在する場合と同値である。 本稿では,プログラムペア間の等価性の証明を生成するために,トランスフォーマーモデルに基づくニューラルネットワークアーキテクチャを提案する。 我々のシステムであるS4Eqは、1万対の等価プログラムをキュレートしたデータセット上で97%の証明成功を達成した。
  論文  参考訳（メタデータ） (2021-09-22T01:37:08Z)
• Stochastic L-system Inference from Multiple String Sequence Inputs [1.8655840060559168]
  リンデンマイヤーシステム(Lindenmayer System、L-systems)は、文字列書き換え規則からなる文法体系である。 本稿では,文字列列を入力として与えられたL-システムの自動探索手法を提案する。
  論文  参考訳（メタデータ） (2020-01-29T16:11:02Z)

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

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