用大模型自动生成并验证并行DEVS状态图，提升建模准确性。
LLM-based Framework for Generating and Verifying Parallel DEVS Statecharts
- 基于代理式大模型生成系统行为事实，自动构建状态图。
- 通过逻辑蕴含验证事实一致性，错误率显著降低。
- 适合需要高可靠性的系统建模与验证的工程师使用。
模型开发需具备建模仿真知识与领域知识，每个模型应准确反映系统动态且可验证。本研究提出一种基于代理的PDEVS-LLM框架，协助人类建模者生成和验证原子并行离散事件系统规范（PDEVS）的状态图。该框架利用代理大模型从系统描述中生成合理的行为事实；若事实不一致，将导致状态图逻辑结构或行为错误。为此，设计了受控修正机制，通过命题逻辑蕴含对事实进行有限次验证，并根据结果生成修改提示，减少事实错误，提高状态图准确性。为验证状态图逻辑正确性，手动构建其时序自动机对应物，并检查死锁与可达性性质。建模者可迭代、增量地重生成事实与状态图。引入基础正确性度量以量化状态图预期行为特征的完整性和准确性。通过不同复杂度示例系统展示大模型的能力与局限。评估表明，所提验证机制显著提升了生成状态图的逻辑一致性。
原文摘要 · Abstract (English)
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.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。