論文の概要: Structural Abstraction and Selective Refinement for Formal Verification

• arxiv url: http://arxiv.org/abs/2505.22982v1
• Date: Thu, 29 May 2025 01:44:47 GMT
• ステータス: 翻訳完了
• システム内更新日: 2025-05-30 18:14:07.61054
• Title: Structural Abstraction and Selective Refinement for Formal Verification
• Title（参考訳）: 形式的検証のための構造的抽象化と選択的精細化
• Authors: Christoph Luckeneder, Ralph Hoch, Hermann Kaindl,
• Abstract要約: ロボットアプリケーションの安全性検証は、ロボットが通常操作する環境の複雑さのため、非常に難しい。 通常のソリューションアプローチは抽象化であり、より正確に振る舞いの抽象化です。 そこで我々は,ロボット環境のボクセル表現の文脈において,構造的抽象化を提案する。
• 参考スコア（独自算出の注目度）: 0.5735035463793008
• License: http://creativecommons.org/licenses/by-nc-nd/4.0/
• Abstract: Safety verification of robot applications is extremely challenging due to the complexity of the environment that a robot typically operates in. Formal verification with model-checking provides guarantees but it may often take too long or even fail for complex models of the environment. A usual solution approach is abstraction, more precisely behavioral abstraction. Our new approach introduces structural abstraction instead, which we investigated in the context of voxel representation of the robot environment. This kind of abstraction leads to abstract voxels. We also propose a complete and automated verification workflow, which is based on an already existing methodology for robot applications, and inspired by the key ideas behind counterexample-guided abstraction refinement (CEGAR) - performing an initial abstraction and successively introducing refinements based on counterexamples, intertwined with model-checker runs. Hence, our approach uses selective refinement of structural abstractions to improve the runtime efficiency of model-checking. A fully-automated implementation of our approach showed its feasibility, since counterexamples have been found for a realistic scenario with a fairly high (maximal) resolution in a few minutes, while direct model-checker runs led to a crash after a couple of days.
• Abstract（参考訳）: ロボットアプリケーションの安全性検証は、ロボットが通常操作する環境の複雑さのため、非常に難しい。 モデルチェックによる形式的検証は保証を提供するが、環境の複雑なモデルでは時間がかかりすぎるか失敗することがある。 通常のソリューションアプローチは抽象化であり、より正確に振る舞いの抽象化です。 そこで本研究では,ロボット環境のボクセル表現の文脈において,構造的抽象化を導入する。 この種の抽象化は、抽象的なボクセルにつながる。 また,ロボットアプリケーションのための既存の方法論をベースとした完全かつ自動化された検証ワークフローを提案し,反例誘導抽象化改善(CEGAR)の背景にある重要なアイデアに触発され,初期抽象を行い,反例に基づく改善を連続的に導入し,モデルチェッカーの実行と連動させる。 したがって,本手法では構造的抽象化を選択的に改良し,モデルチェックの実行効率を向上させる。 提案手法の完全自動実装は,数分間で極めて高い(最大)解像度の現実的なシナリオに対して反例が発見され,直接モデルチェッカーの実行が数日後にクラッシュする可能性を示した。

関連論文リスト

• Unlocking Smarter Device Control: Foresighted Planning with a World Model-Driven Code Execution Approach [83.21177515180564]
  本研究では,自然言語理解と構造化推論を優先し,エージェントの環境に対するグローバルな理解を高める枠組みを提案する。 本手法は,従来の手法,特にタスク成功率の44.4%向上を達成している。
  論文  参考訳（メタデータ） (2025-05-22T09:08:47Z)
• Contract Based Program Models for Software Model Checking [0.0]
  構成モデル検査のために以前に開発された形式主義を提案する。 InCで書かれた組込み型安全クリティカルソフトウェアにおいて,提案する検証手法をサポートするために,作業フローとツールチェーンの構想について述べる。
  論文  参考訳（メタデータ） (2025-03-14T09:34:59Z)
• Model Checking for Closed-Loop Robot Reactive Planning [0.0]
  モデル検査を用いて、ディファレンシャルドライブホイールロボットの多段階計画を作成することにより、即時危険を回避できることを示す。 簡単な生物エージェントのエゴセントリックな反応を反映した,小型で汎用的なモデル検査アルゴリズムを用いて,リアルタイムで計画を生成する。
  論文  参考訳（メタデータ） (2023-11-16T11:02:29Z)
• Learning minimal representations of stochastic processes with variational autoencoders [52.99137594502433]
  プロセスを記述するのに必要なパラメータの最小セットを決定するために、教師なしの機械学習アプローチを導入する。 我々の手法はプロセスを記述する未知のパラメータの自律的な発見を可能にする。
  論文  参考訳（メタデータ） (2023-07-21T14:25:06Z)
• Neural Abstractions [72.42530499990028]
  本稿では,ニューラルネットワークを用いた非線形力学モデルの安全性検証手法を提案する。 提案手法は,既存のベンチマーク非線形モデルにおいて,成熟度の高いFlow*と同等に動作することを示す。
  論文  参考訳（メタデータ） (2023-01-27T12:38:09Z)
• Toward Certified Robustness Against Real-World Distribution Shifts [65.66374339500025]
  我々は、データから摂動を学ぶために生成モデルを訓練し、学習したモデルの出力に関して仕様を定義する。 この設定から生じるユニークな挑戦は、既存の検証者がシグモイドの活性化を厳密に近似できないことである。 本稿では,古典的な反例誘導的抽象的洗練の概念を活用するシグモイドアクティベーションを扱うための一般的なメタアルゴリズムを提案する。
  論文  参考訳（メタデータ） (2022-06-08T04:09:13Z)
• Automated Repair of Process Models with Non-Local Constraints Using State-Based Region Theory [0.19499120576896226]
  最先端プロセス発見手法は、イベントログから自由選択プロセスモデルを構築する。 本研究では,非自由選択構造を地域的手法で探索し,非自由選択構造を付加することで自由選択過程モデルを改善する手法を提案する。
  論文  参考訳（メタデータ） (2021-06-26T21:14:04Z)
• Model-Invariant State Abstractions for Model-Based Reinforcement Learning [54.616645151708994]
  textitmodel-invarianceという新しいタイプの状態抽象化を紹介します。 これにより、状態変数の見当たらない値の新しい組み合わせへの一般化が可能になる。 このモデル不変状態抽象化を通じて最適なポリシーを学習できることを実証する。
  論文  参考訳（メタデータ） (2021-02-19T10:37:54Z)

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

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