論文の概要: LLM-based Framework for Generating and Verifying Parallel DEVS Statecharts
- arxiv url: http://arxiv.org/abs/2608.14956v1
- Date: Sat, 15 Aug 2026 01:08:39 GMT
- ステータス: 翻訳完了
- システム内更新日: 2026-08-18 19:59:03.13701
- Title: LLM-based Framework for Generating and Verifying Parallel DEVS Statecharts
- Title（参考訳）: 並列DVSステートチャートの生成と検証のためのLLMベースのフレームワーク
- Abstract要約: 本研究では,PDEVS状態チャートの生成と検証において,人間のモデリングを支援するエージェント型PDEVS-LLMフレームワークを提案する。
可算事実の論理的整合性を検証するための制御補正機構を開発した。
提案手法の評価は, 生成した状態チャートの論理的整合性を大幅に向上させたことを示す。
- 参考スコア（独自算出の注目度）: 0.4779196219827507
- License: http://creativecommons.org/licenses/by-sa/4.0/
- Abstract: The development of models demands sound modeling and simulation knowledge as well as domain knowledge. Every model should accurately represent a system's dynamics and be verifiable. Toward this objective, this research introduces an agentic PDEVS-LLM framework to assist human modelers in generating and verifying PDEVS statecharts for behavior modeling of atomic Parallel Discrete Event System Specification (PDEVS) models. The framework supports (re)generating plausible facts from a system description prompt using the agentic LLM used for generating plausible facts. Inconsistencies in plausible facts lead to incorrect PDEVS statecharts having logical structure and behavioral inaccuracies. A controlled-correction mechanism is developed to verify the logical consistency of the plausible facts. The agentic LLM is used to generate key behavioral conditions from the system description prompt. The plausible facts are then verified against the behavioral conditions using propositional logic entailment for a finite number of times. The verification results enable the generation of modification prompts that can reduce errors in generated plausible facts, resulting in more accurate PDEVS statecharts. To verify a statechart's logical correctness, its Timed Automata counterpart is manually created and verified for deadlock and reachability properties. The human modeler may regenerate plausible facts and PDEVS statecharts iteratively and incrementally. A basic correctness metric is introduced to quantify the completeness and accuracy of the expected behavioral traits of the PDEVS statechart models. A collection of example systems with varying levels of complexity is developed to demonstrate the capabilities and limitations of LLMs. The evaluation of the proposed verification mechanism shows a substantial improvement in the logical consistency of generated statecharts.
- Abstract（参考訳）: モデルの開発には、ドメイン知識だけでなく、音響モデリングとシミュレーション知識が必要である。
すべてのモデルはシステムのダイナミクスを正確に表現し、検証しなければなりません。
そこで本研究では,原子並列離散イベントシステム仕様(PDEVS)モデルの動作モデリングのためのPDEVS状態チャートの生成と検証を支援するエージェント型PDEVS-LLMフレームワークを提案する。
このフレームワークは、システム記述プロンプトから可塑性事実を生成するために使用されるエージェントLSMを用いて、可塑性事実を(再)生成する。
妥当な事実の不整合は、論理的構造と行動的不正確性を持つ不正確なPDEVSステートチャートにつながる。
可算事実の論理的整合性を検証するための制御補正機構を開発した。
エージェントLSMは、システム記述プロンプトから重要な行動条件を生成するために使用される。
証明可能な事実は、命題論理的含意を用いて有限回にわたり行動条件に対して検証される。
検証結果は、生成した可視事実の誤りを低減し、より正確なPDEVSステートチャートを生成する修正プロンプトの生成を可能にする。
ステートチャートの論理的正当性を検証するために、Timed Automataは手動で作成され、デッドロックとリーチビリティ特性の検証を行う。
ヒトモデラーは、可塑性事実とPDEVSステートチャートを反復的に、段階的に再生することができる。
PDEVS状態チャートモデルの予測行動特性の完全性と精度を定量化するために、基本的な正確性指標が導入された。
LLMの能力と限界を示すために、様々なレベルの複雑性を持つサンプルシステムのコレクションが開発されている。
提案手法の評価は, 生成した状態チャートの論理的整合性を大幅に向上させたことを示す。
関連論文リスト
- 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) - LiveFMBench: Unveiling the Power and Limits of Agentic Workflows in Specification Generation [75.05397479715576]
大規模言語モデル(LLM)とエージェントは有望な進歩を示しているが、その真の能力と失敗モードは未だ不明である。
CプログラムのためのLCMおよびエージェントベースの形式仕様生成に関する、最初の体系的および汚染に配慮した研究を提案する。
論文 参考訳（メタデータ） (2026-05-02T11:31:33Z) - xFODE+: Explainable Type-2 Fuzzy Additive ODEs for Uncertainty Quantification [6.5745172279769255]
本稿では,解釈可能なSysIDモデルであるUQ (xFODE+) 用の Explainable Type-2 Fuzzy Additive ODE を紹介する。
xFODE+は、物理的に意味のあるインクリメンタル状態を維持しながら、ポイント予測と並行してPIを生成する。
ベンチマークSysIDデータセットの結果、xFODE+はPIの品質でFODEと一致し、同等の精度を実現している。
論文 参考訳（メタデータ） (2026-04-16T11:16:34Z) - Ambiguity Detection and Elimination in Automated Executable Process Modeling [1.014361347202587]
本稿では,鍵性能指標の実験的分布から行動の不整合を検出する診断駆動型フレームワークを提案する。
糖尿病性腎症の健康誘導政策に関する実験は、再生モデル行動の変動を減少させることを示した。
論文 参考訳（メタデータ） (2026-04-13T01:11:01Z) - Addressing Explainability of Generative AI using SMILE (Statistical Model-agnostic Interpretability with Local Explanations) [0.0]
この論文では、生成モデルの説明可能性のための統一的なフレームワークであるgSMILEを紹介している。
gSMILEはテキスト入力の制御された摂動、ワッサーシュタイン距離測定、重み付き代理モデリングを採用している。
頑丈で人間に順応した属性を生成し、最先端のジェネレーティブモデルで効果的に一般化する。
論文 参考訳（メタデータ） (2026-02-01T12:54:51Z) - Every Step Counts: Decoding Trajectories as Authorship Fingerprints of dLLMs [63.82840470917859]
本稿では,dLLMの復号化機構をモデル属性の強力なツールとして利用できることを示す。
本稿では、デコードステップ間の構造的関係を捉え、モデル固有の振る舞いをよりよく明らかにする、DDM(Directed Decoding Map)と呼ばれる新しい情報抽出手法を提案する。
論文 参考訳（メタデータ） (2025-10-02T06:25:10Z) - PAT-Agent: Autoformalization for Model Checking [17.082027022913998]
PAT-Agentは自然言語の自動形式化と形式モデル修復のためのエンドツーエンドフレームワークである。
これは、大きな言語モデルの生成能力と形式的検証の厳密さを組み合わせたものである。
論文 参考訳（メタデータ） (2025-09-28T06:32:14Z) - Representing Timed Automata and Timing Anomalies of Cyber-Physical
Production Systems in Knowledge Graphs [51.98400002538092]
本稿では,学習されたタイムドオートマトンとシステムに関する公式知識グラフを組み合わせることで,CPPSのモデルベース異常検出を改善することを目的とする。
モデルと検出された異常の両方を知識グラフに記述し、モデルと検出された異常をより容易に解釈できるようにする。
論文 参考訳（メタデータ） (2023-08-25T15:25:57Z) - Explainability in Process Outcome Prediction: Guidelines to Obtain
Interpretable and Faithful Models [77.34726150561087]
本稿では、プロセス結果予測の分野における説明可能性モデルと説明可能性モデルの忠実性を通して、説明可能性を定義する。
本稿では,イベントログの仕様に基づいて適切なモデルを選択することのできる,X-MOPというガイドラインのセットを提案する。
論文 参考訳（メタデータ） (2022-03-30T05:59:50Z) - Structural Causal Models Are (Solvable by) Credal Networks [70.45873402967297]
因果推論は、干潟網の更新のための標準的なアルゴリズムによって得ることができる。
この貢献は, 干潟ネットワークによる構造因果モデルを表現するための体系的なアプローチと見なされるべきである。
実験により, 実規模問題における因果推論には, クレーダルネットワークの近似アルゴリズムがすぐに利用できることがわかった。
論文 参考訳（メタデータ） (2020-08-02T11:19:36Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。