Fugu-MT 論文翻訳(概要): User-Driven Abstraction for Model Checking

論文の概要: User-Driven Abstraction for Model Checking

arxiv url: http://arxiv.org/abs/2307.15820v1
Date: Fri, 28 Jul 2023 21:33:15 GMT
ステータス: 処理完了
システム内更新日: 2023-10-23 16:02:19.976350
Title: User-Driven Abstraction for Model Checking
Title（参考訳）: モデルチェックのためのユーザ駆動抽象化
Authors: Glenn Bruns
Abstract要約: 本稿では,抽象ルールの適用によるモデル検査に先立って,システムを単純化する手法を提案する。このルールは、システム記述の状態空間を大幅に減らし、システムがプロパティを満たす理由を理解するのに役立つ。
参考スコア（独自算出の注目度）: 0.0
License: http://creativecommons.org/licenses/by-nc-nd/4.0/
Abstract: Model checking has found a role in the engineering of reactive systems. However, model checkers are still strongly limited by the size of the system description they can check. Here we present a technique in which a system is simplified prior to model checking by the application of abstraction rules. The rules can greatly reduce the state space of a system description and help in understanding why a system satisfies a property. We illustrate the use of the technique on examples, including Dekker's mutual exclusion algorithm.
Abstract（参考訳）: モデルチェックはリアクティブシステムのエンジニアリングにおいて重要な役割を担っている。しかし、モデルチェッカーは、チェック可能なシステム記述のサイズによって、依然として強く制限されている。本稿では,抽象ルールの適用によるモデルチェックの前に,システムを単純化する手法を提案する。このルールは、システム記述の状態空間を大幅に減らし、システムがプロパティを満たす理由を理解するのに役立つ。本稿では,Dekkerの相互排他アルゴリズムなど,この手法を例に紹介する。

関連論文リスト

Enabling Regional Explainability by Automatic and Model-agnostic Rule Extraction [44.23023063715179]
ルール抽出は、疾患の診断、疾患の進行予測、薬物発見などの分野に大きく貢献する可能性がある。既存のメソッドは、全体のパフォーマンスを最大化するために、マイナークラスのルールのパフォーマンスを損なう。本稿では,特定のサブグループからルールを抽出するモデルに依存しない手法を提案する。
論文参考訳（メタデータ） (2024-06-25T18:47:50Z)
Bisimulation Learning [55.859538562698496]
我々は、大きな、潜在的に無限の状態空間を持つ状態遷移系の有限バイシミュレートを計算する。提案手法は,実際に行われている他の最先端ツールよりも高速な検証結果が得られる。
論文参考訳（メタデータ） (2024-05-24T17:11:27Z)
A Hypergraph-based Formalization of Hierarchical Reactive Modules and a Compositional Verification Method [0.30458514384586394]
サイバー物理システムのモデル化によく使用される階層構造を持つ同期システムに対処する。反応加群の理論を再検討し,それをハイパーグラフに基づいて再構成し,モジュールの並列構成と階層的記述を明らかにする。階層型システムの自動検証手法を提案する。
論文参考訳（メタデータ） (2024-03-16T13:10:41Z)
Representing Timed Automata and Timing Anomalies of Cyber-Physical Production Systems in Knowledge Graphs [51.98400002538092]
本稿では,学習されたタイムドオートマトンとシステムに関する公式知識グラフを組み合わせることで,CPPSのモデルベース異常検出を改善することを目的とする。モデルと検出された異常の両方を知識グラフに記述し、モデルと検出された異常をより容易に解釈できるようにする。
論文参考訳（メタデータ） (2023-08-25T15:25:57Z)
OCTAL: Graph Representation Learning for LTL Model Checking [5.22145960878624]
GRLベースの新しいフレームワークモデルは、グラフ構造化システムと仕様の表現を学習するために設計されている。実験により、モデルが有望な精度を達成し、標準SOTAモデルチェッカーに対する全体的なスピードアップが最大で11倍になることが示された。
論文参考訳（メタデータ） (2023-08-19T15:11:18Z)
In-Distribution Barrier Functions: Self-Supervised Policy Filters that Avoid Out-of-Distribution States [84.24300005271185]
本稿では,任意の参照ポリシーをラップした制御フィルタを提案する。本手法は、トップダウンとエゴセントリックの両方のビュー設定を含むシミュレーション環境における2つの異なるビズモータ制御タスクに有効である。
論文参考訳（メタデータ） (2023-01-27T22:28:19Z)
Visual Exploration of Machine Learning Model Behavior with Hierarchical Surrogate Rule Sets [13.94542147252982]
本稿では,ユーザ定義パラメータに基づく階層的ルールを生成するアルゴリズムである階層的サロゲートルール(HSR)を提案する。我々はまた、HSRと対話型代理ルール可視化を統合した視覚分析(VA)システムであるSuREにも貢献する。パラメータ感度,時間性能,および代理決定木との比較により,本アルゴリズムの評価を行った。
論文参考訳（メタデータ） (2022-01-19T17:03:35Z)
Deep Learning Approximation of Diffeomorphisms via Linear-Control Systems [91.3755431537592]
我々は、制御に線形に依存する$dot x = sum_i=1lF_i(x)u_i$という形の制御系を考える。対応するフローを用いて、コンパクトな点のアンサンブル上の微分同相写像の作用を近似する。
論文参考訳（メタデータ） (2021-10-24T08:57:46Z)
Sparsity in Partially Controllable Linear Systems [56.142264865866636]
本研究では, 部分制御可能な線形力学系について, 基礎となる空間パターンを用いて検討する。最適制御には無関係な状態変数を特徴付ける。
論文参考訳（メタデータ） (2021-10-12T16:41:47Z)
Learning on Abstract Domains: A New Approach for Verifiable Guarantee in Reinforcement Learning [9.428825075908131]
有限抽象領域上でDRLシステムを学習するための抽象的アプローチを提案する。入力状態が有限なニューラルネットワークを生成し、ホスティングDRLシステムが直接検証可能である。
論文参考訳（メタデータ） (2021-06-13T06:28:40Z)
Rewriting a Deep Generative Model [56.91974064348137]
我々は,深層生成モデルによって符号化された特定の規則の操作という,新たな問題設定を導入する。本稿では,ディープネットワークの層を線形連想メモリとして操作することで,所望のルールを変更する定式化を提案する。本稿では,生成モデルのルールを対話的に変更し,望ましい効果を得られるユーザインタフェースを提案する。
論文参考訳（メタデータ） (2020-07-30T17:58:16Z)

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