基于大语言模型的并行DEVS状态图生成与验证框架
LLM-based Framework for Generating and Verifying Parallel DEVS Statecharts
- Arizona State University（亚利桑那州立大学）
- Intel Corporation（英特尔公司）
机构由 AI 辅助整理，请以论文原文为准。
AI总结：
本研究提出智能体式PDEVS-LLM框架，辅助建模人员生成验证PDEVS状态图，经评估该框架可显著提升生成状态图的逻辑一致性。
AI中文摘要：
模型的开发需要扎实的建模与仿真知识以及领域知识，每个模型都应准确表征系统的动态特性且具备可验证性。为实现这一目标，本研究提出了一种智能体式PDEVS-LLM框架，用于辅助人类建模人员生成和验证PDEVS状态图，以对原子并行离散事件系统规范（Parallel Discrete Event System Specification，PDEVS）模型的行为进行建模。该框架支持利用用于生成合理事实的智能体式LLM，从系统描述提示中（重新）生成合理事实。合理事实中的不一致会导致生成的PDEVS状态图出现逻辑结构和行为不准确的问题。为此，本研究开发了一种受控修正机制，用于验证合理事实的逻辑一致性；智能体式LLM会从系统描述提示中生成关键行为条件，随后利用命题逻辑蕴含关系对合理事实进行有限次验证。验证结果可用于生成修正提示，以减少生成的合理事实中的错误，进而生成更准确的PDEVS状态图。为验证状态图的逻辑正确性，需手动创建其对应的时间自动机（Timed Automata），并对其死锁和可达性属性进行验证。人类建模人员可迭代且增量地重新生成合理事实和PDEVS状态图。本研究还引入了一种基础正确性指标，用于量化PDEVS状态图模型预期行为特性的完整性和准确性；开发了一组具有不同复杂度的示例系统，以展示LLM的能力与局限性。对所提出的验证机制的评估表明，生成的状态图的逻辑一致性得到了显著提升。
英文摘要：
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.
