論文の概要: Constraint-Driven Modeling Enabling Dual Model Checking and Simulation for Discrete Event Systems
- arxiv url: http://arxiv.org/abs/2608.22095v1
- Date: Sat, 22 Aug 2026 20:14:37 GMT
- ステータス: 翻訳完了
- システム内更新日: 2026-08-25 18:24:36.945368
- Title: Constraint-Driven Modeling Enabling Dual Model Checking and Simulation for Discrete Event Systems
- Title（参考訳）: 離散イベントシステムにおけるデュアルモデルチェックとシミュレーションを実現する制約駆動モデリング
- Abstract要約: 本稿では,モデルチェックにシミュレーションに加えて,自身を貸与する有界並列DEVSモデルを作成する手法であるConstraint-DEVSを紹介する。
私たちはDEVS-Suiteフレームワークを拡張してConstraint-DEVS仕様を作成します。
本研究を実証するために,ネットワーク・オン・チップのモデルを開発し,検証した。
- 参考スコア（独自算出の注目度）: 0.5371337604556311
- License: http://creativecommons.org/licenses/by-sa/4.0/
- Abstract: Verification and validation (V&V) are crucial methods for evaluating the requirements and specifications of dynamical models that fulfill their intended purposes. Parallel Discrete EVent System Specification (PDEVS) is a system-theoretic modeling approach for creating modular, hierarchical component-based simulation models. In this paper, we introduce Constraint-DEVS, a method for creating bounded Parallel DEVS models that lend themselves, in addition to simulation, to model checking. We extend the DEVS-Suite framework to create Constraint-DEVS specifications which can then be model checked using a proposed state exploration protocol with the Parallel DEVS abstract simulator protocol. These capabilities, along with the support for non-determinism, complex data transfer, and performance-related property checking, make Constraint-DEVS and its accompanying DEVS-Suite a unique framework for the development, verification, and validation of discrete-event systems. In order to demonstrate this work, we developed and verified models of Network-on-Chip. Also, we detail behavioral design artifacts for the DEVS-Suite framework's hybrid model-checking and simulation engine.
- Abstract（参考訳）: 検証と検証(V&V)は、彼らの意図した目的を満たす動的モデルの要件と仕様を評価するための重要な方法である。
Parallel Discrete EVent System Specification (PDEVS) は、モジュラーな階層的なコンポーネントベースのシミュレーションモデルを作成するためのシステム理論モデリング手法である。
本稿では,モデルチェックにシミュレーションに加えて,自身を貸与する有界並列DEVSモデルを作成する手法であるConstraint-DEVSを紹介する。
我々はDEVS-Suiteフレームワークを拡張してConstraint-DEVS仕様を作成し、Parallel DEVS抽象シミュレータプロトコルを用いて提案された状態探索プロトコルを用いてモデルチェックすることができる。
これらの機能は、非決定性、複雑なデータ転送、パフォーマンス関連のプロパティチェックをサポートするとともに、Constraint-DEVSとその付随するDEVS-Suiteは、離散イベントシステムの開発、検証、検証のためのユニークなフレームワークである。
本研究を実証するために,ネットワーク・オン・チップのモデルを開発し,検証した。
また、DEVS-Suiteフレームワークのハイブリッドモデルチェックおよびシミュレーションエンジンの動作設計アーティファクトについても詳述する。
関連論文リスト
- SAMpLE: A SystemC-AMS Machine LEarning-based Framework for Virtual Prototyping [1.4932318540666545]
本稿では,機械学習モデルを時系列データフローコンポーネントとして統合したオープンソースのフレームワークである textbftextitSAMpLE を提案する。
このフレームワークはONNXを標準モデル交換フォーマットとして使用し、外部で訓練されたMLモデルをSystemC-AMSシミュレーションに統合する。
論文 参考訳（メタデータ） (2026-08-26T15:26:21Z) - Model-Driven Discipline for Multi-Agent LLMs: Requirement-to-Verification Generation of Traceable System Models [62.62160094849002]
RADIANTは、MDEとMulti-Agent Large Language Modelを組み合わせたエンジニアリング方法論である。
工学的なフェーズにまたがる異種モデルを自動的に生成する。
正確かつ自動的な変更インパクト分析を提供する。
論文 参考訳（メタデータ） (2026-07-18T08:50:55Z) - Opt-Verifier: Unleashing the Power of LLMs for Optimization Modeling via Dual-Side Verification [53.763212981479455]
本稿では、構造と解の両方の観点から、デュアルサイド検証(Opt-Verifier)を用いた新しいフレームワークを提案する。
一般的なベンチマーク実験により、我々の手法は精度が20%以上向上していることが示された。
論文 参考訳（メタデータ） (2026-05-28T08:09:52Z) - CellScientist: Dual-Space Hierarchical Orchestration for Closed-Loop Refinement of Virtual Cell Models [62.281480231694]
VCM(Virtual Cell Modeling)は、摂動応答を予測できるだけでなく、予測が失敗した場合にターゲットリビジョンをサポートするモデルを必要とする。
現在のLCM支援モデリングでは、予測誤差が実行可能実装を通して観測されるという改善ルーティング問題に直面している。
提案するCellScientistは,高レベル仮説空間と低レベル実行可能実装空間を結合した,二重空間階層型フレームワークである。
論文 参考訳（メタデータ） (2026-05-08T06:40:24Z) - Specification-Driven Generation and Evaluation of Discrete-Event World Models via the DEVS Formalism [9.578714623643291]
我々は,明示的なシミュレータの信頼性と学習モデルの柔軟性を両立させる原理的な中間層を求める。
我々は、自然言語仕様から直接合成された明示的で実行可能な離散的世界モデルを提案する。
論文 参考訳（メタデータ） (2026-03-04T06:50:32Z) - Rethinking Scientific Modeling: Toward Physically Consistent and Simulation-Executable Programmatic Generation [8.067859101380389]
非実行可能または物理的に一貫性のない出力は、厳密な工学的制約の下では依然として一般的である。
物理に一貫性のある自動建築モデリングのための枠組みを提案する。
CivilInstructは、構造工学の知識と制約推論を形式化するドメイン固有のデータセットとして導入された。
MBEvalは、実行可能性と構造的ダイナミクスの一貫性を評価する検証駆動ベンチマークとして提示される。
論文 参考訳（メタデータ） (2026-02-06T06:57:04Z) - eUDEVS: Executable UML with DEVS Theory of Modeling and Simulation [0.0]
システム設計とプロトタイピングのためのモデリングとシミュレーション(M&S)は、今日では産業と学術の両方で行われている。
本稿では,eUDEVSを用いた相互変換とDEVSの相互変換に対する統合的なアプローチを提案する。
また、提案されたeUDEVSを、DEVS Unified Processと呼ばれるより大きな統一フレームワークに組み込んだ。
論文 参考訳（メタデータ） (2024-07-11T08:29:46Z) - Towards Aligned Layout Generation via Diffusion Model with Aesthetic Constraints [53.66698106829144]
広い範囲のレイアウト生成タスクを処理する統一モデルを提案する。
このモデルは連続拡散モデルに基づいている。
実験結果から,LACEは高品質なレイアウトを生成することがわかった。
論文 参考訳（メタデータ） (2024-02-07T11:12:41Z) - Formal Verification Of A Shopping Basket Application Model Using PRISM [0.0]
ショッピング・バスケット・アプリケーション・モデルにおけるPrism Model Checkerを用いたシミュレーションの結果を示す。
目的は、買い物客が買い物プロセスの多くの定義された状態を通過するときの行動をシミュレートすることである。
論文 参考訳（メタデータ） (2023-07-16T00:14:40Z) - Benchmarking Model Predictive Control Algorithms in Building Optimization Testing Framework (BOPTEST) [40.17692290400862]
物理に基づく建築エミュレータのためのデータ駆動モデリングおよび制御フレームワークを提案する。
a)モデル評価を加速し、コスト効率の良い勾配を提供し、モデル予測制御(MPC)における後退地平線に対する良好な予測精度を維持する、微分可能な代理モデルのオフライントレーニング。
ビルディング最適化テストフレームワーク(BOPTEST)で利用可能な様々なテストケースに対して、複数のサロゲートモデルと最適化フレームワークを用いて、モデリングと制御性能を広範囲に評価する。
論文 参考訳（メタデータ） (2023-01-31T06:55:19Z) - Switchable Representation Learning Framework with Self-compatibility [50.48336074436792]
自己整合性(SFSC)を考慮した交換可能な表現学習フレームワークを提案する。
SFSCは1つのトレーニングプロセスを通じて、異なる能力を持つ一連の互換性のあるサブモデルを生成する。
SFSCは評価データセット上で最先端のパフォーマンスを達成する。
論文 参考訳（メタデータ） (2022-06-16T16:46:32Z) - Lifted Model Checking for Relational MDPs [12.574454799055026]
pCTL-REBELは、リレーショナルMDP上のpCTL特性を検証するためのリフトモデルチェック手法である。
pCTLモデル検査手法は, 無限領域であっても, リレーショナルMDPに対して決定可能であることを示す。
論文 参考訳（メタデータ） (2021-06-22T13:12:36Z) - Control as Hybrid Inference [62.997667081978825]
本稿では、反復推論と償却推論のバランスを自然に仲介するCHIの実装について述べる。
連続的な制御ベンチマークでアルゴリズムのスケーラビリティを検証し、強力なモデルフリーおよびモデルベースラインを上回る性能を示す。
論文 参考訳（メタデータ） (2020-07-11T19:44:09Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。