# LLM-based Framework for Generating and Verifying Parallel DEVS Statecharts

arXiv: https://arxiv.org/abs/2608.14956 · HTML: https://mlsanity.com/paper/2608.14956/

## Key facts

- No citing papers in the map yet (data through 14 Oct 2026).
- Placed in General LLM agent frameworks and benchmarks, one of 16 directions in LLM agents and tool use.
- Builds on 8 of its 29 references that are in the map.
- First posted on arXiv 15 Aug 2026.

## Placed in

- LLM agents and tool use / [General LLM agent frameworks and benchmarks](https://mlsanity.com/agents/general-llm-agent-frameworks-and-benchmarks/)

## Builds on (most cited first, 8 of 8)

- [Language Models are Few-Shot Learners](https://mlsanity.com/paper/2005.14165/) (2020)
- [Training Verifiers to Solve Math Word Problems](https://mlsanity.com/paper/2110.14168/) (2021)
- [Evaluating Large Language Models Trained on Code](https://mlsanity.com/paper/2107.03374/) (2021)
- [Language Models can Solve Computer Tasks](https://mlsanity.com/paper/2303.17491/) (2023)
- [A Bibliometric Review of Large Language Models Research from 2017 to 2023](https://mlsanity.com/paper/2304.02020/) (2023)
- [Large Language Models Can Self-Correct with Key Condition Verification](https://mlsanity.com/paper/2405.14092/) (2024)
- [GPT-Based Models Meet Simulation: How to Efficiently Use Large-Scale Pre-Trained Language Models Across Simulation Tasks](https://mlsanity.com/paper/2306.13679/) (2023)
- [SLGPT: Using Transfer Learning to Directly Generate Simulink Model Files and Find Bugs in the Simulink Toolchain](https://mlsanity.com/paper/2105.07465/) (2021)

## Abstract (arXiv)

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.