LLM-based Framework for Generating and Verifying Parallel DEVS Statecharts

Vamsi Krishna Vasa; Hessam S. Sarjoughian; Edward J. Yellig

cs.LGAug 15, 2026

LLM-based Framework for Generating and Verifying Parallel DEVS Statecharts

Authors: Vamsi Krishna Vasa, Hessam S. Sarjoughian, Edward J. Yellig

Organizations: Arizona State University, Tempe, Arizona, USA · Intel Corporation, Chandler, Arizona, USA

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.

Figures & tables

Proposition	Definition
$b$	Processor is in busy state
$g$	Job is generated by generator
$i$	Processor is in idle state
$j$	Job signal is received by processor
$o$	Processed job is sent to output port
$p$	Job is being processed by processor

Table 1: Defined propositions for Processor with Queue system.

PDEVS Specifications	Natural Language	Propositional Logic
Internal Transitions	whenever state is “busy” and “queue” is empty, the state must be “idle” and time_advance must be infinity (duration to wait for the next job).	$(b\land\lnot q)\Rightarrow i$
	whenever state is “busy” and “queue” is not empty, the state must be “busy” and time_advance must be 2 (to process the next job).	$(b\land q)\Rightarrow b$
External Transitions	whenever a job is received at job_in and the state is “idle”, the state must be “busy” and time_advance must be 2 (indicating processing time).	$(j\land i)\Rightarrow b$
	whenever a job is received at job_in , the state is “busy”, the job is added to the “queue” and time_advance must be the remaining processing time for the current job.	$(j\land b)\Rightarrow q$
Output Function	whenever the state is “busy”, the first job must be removed from the “queue”, the job is sent to processed_job_out .	$(b)\Rightarrow(p\land o)$

Table 2: PDEVS specifications for a processor with queue expressed in natural language and their propositional logic equivalents.

Panel of Figure 1 — Figure 1: Snapshot of the Processor with Queue system as Timed Automata in UPPAAL

Figure 2: Overview for the proposed framework to generate. The Red arrows represents API LLM calls, both Agentic and Non-Agentic. The Blue arrows represent the Python function calls. The Green arrow represent the feedback for controlled-correction with Modification Prompt.

Figure 3: Illustration of the Proposed Framework.

Proposition	Definition
$a$	Phone is active
$c$	Call is received by phone
$f$	Service is found
$i$	Phone is interrupted by another call
$m$	Interrupting call is stored in memory
$n$	Phone is on

Table 3: Extracted propositions for Phone component

Panel of Figure 4 — Figure 4: Desired and Generated PDEVS statecharts for Phone system visualized using CoSMoS modeling tool.

PDEVS Statecharts	UPPAAL Timed Automata
Phases	Locations
State variables	defined as Local Declarations .
Input/output ports and messages	defined as synchronization channels .
External Transition Function	External events can be defined using channels . Guard and Action can be declared in Guard and Update properties of the UPPAAL transition respectively. Time Advance can be handled using a clock variable locally declared.
Internal Transition Function	Triggered by adding the invariant $[\,\text{internal clock}\geq\text{Time advance}\,]$ in the Guard property of the transition. Guard and Action can be declared in the Guard and Update properties.
Output Function	Omitted

Table 5: Analogy to model a Timed Automata for given PDEVS Statechart.

Panel of Figure 5 — Figure 5: Manually generated Timed Automata replicas for the Phone example using UPPAAL. The snapshots are taken from the Editor tab of UPPAAL.

	No. of Systems suffering with Deadlock		No. of Systems not satisfying Phase reachability
LLM	BV	AV	BV	AV
Llama-3.1-8b †	5	2	5	2
Ministral-3b †	1	1	1	0
Ministral-8b †	4	2	1	0
Llama-3.3-70b $\ddagger$	1	0	1	0
Mistral-7b-instruct *	2	3	2	0

Table 6: Model Checking results over the test set comprising of 14 system descriptions using various publicly available LLMs as base model for PDEVS Specification Generator Agent. These models are categorized as small models (¡ 10B parameters) † , large models (¿ 30B parameters)

\ddagger

, instruction tuned * , and reasoning oriented § . BV , and AV stands for the stats before and after verification respectively.

Table 7: Statechart correctness scores for the Phone PDEVS statechart resulted from the PDEVS facts before correction. The values in green cells are calculated by averaging the values in blue cells from the same row. The values in yellow cell is calculated by averaging the values in green cells. The red cells are avoided in the calculations as they represent the wrong specification.

	External Transition Fn.		Internal Transition Fn.		Output Fn.
Model	BV	AV	BV	AV	BV	AV
Llama-3.1-8b	0.9434	0.8809	0.6416	0.7736	0.7935	0.8571
Ministral-3b	0.8065	0.7755	0.6427	0.7801	0.8809	0.9047
Ministral-8b	0.8392	0.8142	0.7857	0.7857	0.8571	0.8571
Llama-3.3-70b	0.8244	0.8928	0.6548	0.7991	0.7856	0.9285
Mistral-7b-instruct	0.8100	0.8100	0.7976	0.8214	0.7142	0.7142

Table 8: Performance of multiple LLMs as base model for PDEVS Specification Generator in terms of the proposed Statechart Correctness Score Before Verification (BV) and After Verification (AV). The improvement and decline in the scores is highlighted in red and green respectively.

Appendix figures & tables1 asset

Supplementary material from the paper’s appendix.

Appendix

System	Description
Processor	Processes incoming jobs with a 2-second delay, transitioning between idle and busy states.
Processor with Queue	Another variant of processor with a queuing mechanism.
CarWash	A carwash that services cars and trucks with a 20-time-unit wash duration for cars and 40-time-unit for trucks; queues cars and denies service to trucks if busy.
Phone	Manages power, service search, and call handling while maintaining active conversations and handling interruptions using FIFO order.
Counter	Counts up, resets, stops, or provides the current count based on received inputs.
Coordinator (MiniFab)	Manages overall workflow by routing jobs between machines and synchronizing their operations.

Appendix

Table 9: Descriptions of systems considered for evaluating the proposed framework.

Explore similar work

Mar 4, 2026

Specification-Driven Generation and Evaluation of Discrete-Event World Models via the DEVS Formalism

World models are central to LLM agents that must evaluate actions over long horizons. Yet much existing work focuses on environments governed by physical dynamics or spatial structure, whereas many high-impact domains, including supply chains, procurement networks, and business processes, evolve through discrete events, timing constraints, and causal dependencies. These settings call for discrete-event world models. Existing approaches to constructing world models often fall near two extremes: hand-engineered simulators provide consistency and reproducibility, but are costly to build and adapt; neural models are flexible, but can suffer from compounding inconsistency over long-horizon rollouts. We seek a principled middle ground by synthesizing discrete-event world models online from natural-language specifications, retaining the reliability of explicit simulators while gaining the adaptability of neural models. We adopt the DEVS formalism and introduce a staged LLM-based generation pipeline that separates structural inference over component interactions from component-level event and timing logic. For evaluation, we develop benchmark suites in which simulators emit structured event traces, which are then validated against specification-derived temporal, causal, and semantic constraints. This enables reproducible verification and localized diagnostics. Together, these contributions produce world models that remain consistent over long-horizon rollouts, can be verified from observable behavior, and can be synthesized efficiently on demand during online execution.

Zheyu Chen, Huiteng Zhuang, Zhuohuan Li +1

Zhili College, Tsinghua University · School of Transportation Science and Engineering, Beihang University · Department of Industrial Engineering, Tsinghua University

LLM World Models World Model Evaluation

Ask PDF

Mar 26, 2026

ExVerus: Verus Proof Repair via Counterexample Reasoning

Large Language Models (LLMs) have shown promising results in automating formal verification. However, existing approaches treat proof generation as a static, end-to-end prediction over source code, relying on limited verifier feedback and lacking access to concrete program behaviors. We present EXVERUS, a counterexample-guided framework that enables LLMs to reason about proofs using behavioral feedback via counterexamples. When a proof fails, EXVERUS automatically generates and validates counterexamples, and then guides the LLM to generalize them into inductive invariants to block these failures. Our evaluation shows that EXVERUS significantly improves proof accuracy, robustness, and token efficiency over the state-of-the-art prompting-based Verus proof generator.

Jun Yang, Yuechun Sun, Yi Wu +5

The University of Chicago · Purdue University · The University of Toronto +1

Formal Verification

Ask PDF

Oct 6, 2026

A Survey on LLM-Integrated Hardware Design Verification

Large language models (LLMs) are increasingly being integrated into hardware verification to automate specification interpretation, verification-artifact generation, debugging, formal reasoning, and tool orchestration. This survey provides a systematic review of LLM-assisted hardware functional verification across SystemVerilog assertion generation, stimulus and testbench generation, bug localization and design repair, model checking and equivalence checking, SAT/SMT optimization, and emerging agentic verification workflows. We organize the literature by methodology, verification objective, tool interaction, benchmark, and evaluation criterion, and examine both inference-time techniques--including prompting, retrieval, structured reasoning, and agentic workflows--and training-time adaptation. Across these areas, a common pattern emerges: LLMs are most effective as semantic reasoning, search, and orchestration components embedded within verification-aware workflows, while simulators, formal engines, coverage tools, and solvers provide executable feedback and correctness evidence. However, tool acceptance alone does not establish verification correctness, since assertions, tests, repairs, or proofs may satisfy available checks without faithfully capturing the complete design intent. We therefore identify semantic alignment between specifications and verification evidence, scalable integration with deterministic tools, generalization to unseen designs, and rigorous evaluation of correctness, cost, robustness, and human effort as key challenges. Finally, we discuss emerging directions toward specification-centered, neuro-symbolic, and persistent agentic verification systems that combine LLM flexibility with independently checkable verification evidence.

Hao Zheng, Jaime Rafael Imperial, Bardia Nadimi +1

Bellini College of Cybersecurity, AI, and Computing, University of South Florida Tampa, FL, USA

LLM Agent Verification Formal Hardware Verification

Ask PDF