論文の概要: A Hypergraph-based Formalization of Hierarchical Reactive Modules and a Compositional Verification Method
- arxiv url: http://arxiv.org/abs/2403.10919v1
- Date: Sat, 16 Mar 2024 13:10:41 GMT
- ステータス: 処理完了
- システム内更新日: 2024-03-19 21:06:03.158034
- Title: A Hypergraph-based Formalization of Hierarchical Reactive Modules and a Compositional Verification Method
- Title（参考訳）: ハイパーグラフによる階層型反応性モジュールの形式化と構成検証法
- Authors: Daisuke Ishii,
- Abstract要約: サイバー物理システムのモデル化によく使用される階層構造を持つ同期システムに対処する。
反応加群の理論を再検討し,それをハイパーグラフに基づいて再構成し,モジュールの並列構成と階層的記述を明らかにする。
階層型システムの自動検証手法を提案する。
- 参考スコア（独自算出の注目度）: 0.30458514384586394
- License: http://creativecommons.org/licenses/by/4.0/
- Abstract: The compositional approach is important for reasoning about large and complex systems. In this work, we address synchronous systems with hierarchical structures, which are often used to model cyber-physical systems. We revisit the theory of reactive modules and reformulate it based on hypergraphs to clarify the parallel composition and the hierarchical description of modules. Then, we propose an automatic verification method for hierarchical systems. Given a system description annotated with assume-guarantee contracts, the proposed method divides the system into modules and verifies them separately to show that the top-level system satisfies its contract. Our method allows an input to be a circular system in which submodules mutually depend on each other. Experimental result shows our method can be effectively implemented using an SMT-based model checker.
- Abstract（参考訳）: 構成的アプローチは、大規模で複雑なシステムについて推論するために重要である。
本研究では,サイバー物理システムのモデル化によく用いられる階層構造を持つ同期システムについて述べる。
反応加群の理論を再検討し,それをハイパーグラフに基づいて再構成し,モジュールの並列構成と階層的記述を明らかにする。
そこで本研究では,階層型システムの自動検証手法を提案する。
想定保証契約に注釈を付けたシステム記述が与えられた場合、提案手法はシステムをモジュールに分割し、上位レベルのシステムがその契約を満たすことを示すためにそれらを別々に検証する。
提案手法は,サブモジュール同士が相互に依存する円形システムであることを示す。
実験結果から,本手法はSMTモデルチェッカーを用いて効果的に実装可能であることが示された。
関連論文リスト
- A process algebraic framework for multi-agent dynamic epistemic systems [55.2480439325792]
本稿では,マルチエージェント,知識ベース,動的システムのモデリングと解析のための統合フレームワークを提案する。
モデリング側では,このようなフレームワークを実用的な目的に使いやすくするプロセス代数的,エージェント指向の仕様言語を提案する。
論文 参考訳（メタデータ） (2024-07-24T08:35:50Z) - Bisimulation Learning [55.859538562698496]
我々は、大きな、潜在的に無限の状態空間を持つ状態遷移系の有限バイシミュレートを計算する。
提案手法は,実際に行われている他の最先端ツールよりも高速な検証結果が得られる。
論文 参考訳（メタデータ） (2024-05-24T17:11:27Z) - Formal Methods for Autonomous Systems [21.989467515686858]
形式的手法は安全クリティカルシステムの正当性を確立する上で重要な役割を果たしてきた。
形式的なメソッドの主なビルディングブロックはモデルと仕様です。
様々な定式化の下で, 正しい構成合成を考察する。
論文 参考訳（メタデータ） (2023-11-02T14:18:43Z) - Interactive System-wise Anomaly Detection [66.3766756452743]
異常検出は様々なアプリケーションにおいて基本的な役割を果たす。
既存のメソッドでは、インスタンスがデータとして容易に観察できないシステムであるシナリオを扱うのが難しい。
システム埋め込みを学習するエンコーダデコーダモジュールを含むエンドツーエンドアプローチを開発する。
論文 参考訳（メタデータ） (2023-04-21T02:20:24Z) - Dealing with Collinearity in Large-Scale Linear System Identification
Using Gaussian Regression [3.04585143845864]
複数の相互接続型動的システムからなるネットワークの推定について検討する。
我々は、任意のインパルス応答をゼロ平均ガウス過程の実現と見なすベイズ正規化フレームワークにキャストされた戦略を開発する。
我々はマルコフ連鎖モンテカルロスキームを設計し、コリナリティを効率的に扱うことでインパルス応答を後方に再構築する。
論文 参考訳（メタデータ） (2023-02-21T19:35:47Z) - Learning Modular Simulations for Homogeneous Systems [23.355189771765644]
等質多体力学系をモデル化するためのモジュラーシミュレーションフレームワークを提案する。
任意の数の加群を組み合わせることで、様々な結合トポロジーの系をシミュレートすることができる。
我々のモデルは、スクラッチからトレーニングされたモデルと比較して、データ要件やトレーニングの労力が低い新しいシステム構成に移行可能であることを示しています。
論文 参考訳（メタデータ） (2022-10-28T17:48:01Z) - Is a Modular Architecture Enough? [80.32451720642209]
我々は、シンプルで既知のモジュラーデータ分散のレンズを通して、共通のモジュラーアーキテクチャを徹底的に評価する。
モジュール化と疎結合のメリットを強調し、モジュール化システムの最適化において直面する課題に関する洞察を明らかにします。
論文 参考訳（メタデータ） (2022-06-06T16:12:06Z) - Activity Recognition in Assembly Tasks by Bayesian Filtering in
Multi-Hypergraphs [1.2961180148172198]
組立作業などの手作業プロセスにおいて,センサによる人間の活動認識について検討する。
本手法では,システム状態はマルチハイパーグラフで表現され,システムダイナミクスはグラフ書き換え規則によってモデル化される。
マルチハイパーグラフ上の分布を全列挙よりもコンパクトに表現できる予備概念を示し、このコンパクト表現に直接作用する推論アルゴリズムを提案する。
論文 参考訳（メタデータ） (2022-02-01T11:01:09Z) - Neural Function Modules with Sparse Arguments: A Dynamic Approach to
Integrating Information across Layers [84.57980167400513]
Neural Function Modules (NFM)は、ディープラーニングに同じ構造機能を導入することを目的としている。
トップダウンとボトムアップのフィードバックを組み合わせたフィードフォワードネットワークのコンテキストにおける作業のほとんどは、分類の問題に限られている。
私たちの仕事の重要な貢献は、フレキシブルなアルゴリズムで注意、疎結合、トップダウン、ボトムアップのフィードバックを組み合わせることです。
論文 参考訳（メタデータ） (2020-10-15T20:43:17Z) - S2RMs: Spatially Structured Recurrent Modules [105.0377129434636]
モジュール構造とテンポラル構造の両方を同時に活用できる動的構造を利用するための一歩を踏み出します。
我々のモデルは利用可能なビューの数に対して堅牢であり、追加のトレーニングなしで新しいタスクに一般化できる。
論文 参考訳（メタデータ） (2020-07-13T17:44:30Z) - Generation of accessible sets in the dynamical modelling of quantum
network systems [9.295724747694194]
量子ビットからなる量子ネットワークのクラスの動的モデリングについて考察する。
様々なアプリケーションにとって、状態空間モデルはシステムのダイナミクスをモデル化するのに有用な方法である。
論文 参考訳（メタデータ） (2020-04-30T09:53:18Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。