LLM Framework Generates and Verifies Parallel DEVS Statecharts

Developing accurate and verifiable models, particularly for complex system dynamics, requires both deep modeling expertise and domain-specific knowledge. This new research presents the PDEVS-LLM framework, an agentic system designed to aid human modelers in creating and validating Parallel Discrete Event System Specification (PDEVS) statecharts. The framework leverages large language models (LLMs) to generate plausible facts from a system description. A crucial component is a controlled-correction mechanism that verifies the logical consistency of these generated facts, as inconsistencies can lead to inaccurate statecharts. The LLM also generates key behavioral conditions, against which the plausible facts are checked using propositional logic. This iterative verification process allows for the generation of modification prompts, reducing errors and improving the accuracy of the resulting PDEVS statecharts. To further ensure correctness, the generated statecharts' Timed Automata counterparts are manually created and verified for properties like deadlock and reachability. The framework introduces a metric to quantify the completeness and accuracy of the statecharts' expected behavioral traits. Demonstrations with various system complexities highlight the LLMs' capabilities and limitations in this specialized modeling task.