Source-linked AI summary
LLM-based Framework for Generating and Verifying Parallel DEVS Statecharts
Vamsi Krishna Vasa, Hessam S. Sarjoughian, Edward J. Yellig
TL;DR
LLM-generated PDEVS statecharts can contain logical inconsistencies, motivating verification to support reliable model development. This paper introduces a propositional-logic controlled-correction framework that iteratively refines PDEVS specifications, and reports consistently enhanced correctness and completeness across multiple LLMs.
Problem
LLM-generated PDEVS statecharts can contain logical inconsistencies, creating a need for verification during model development.
Method
The framework identifies behavioral conditions, checks satisfiability, performs segregated propositional-logic entailment verification, and applies controlled correction before generating PDEVS statecharts.
Results
Across multiple publicly available LLMs, verification consistently enhanced statechart correctness, especially for internal transitions and output functions, and improved specification completeness.
Takeaways & Limitations
The framework supports iterative refinement of PDEVS specifications with improved logical alignment between generated statecharts and system descriptions.
Takeaways & Limitations
The framework depends on contradiction-free system descriptions and accurate LLM translation of natural language into propositional logic.
Abstract
from arXiv · showhide
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.
1. Introduction
The paper motivates LLM support for transforming conceptual system descriptions into simulatable PDEVS statecharts while addressing the logical inconsistencies that arise with behavioral complexity. It proposes Boolean propositional-logic verification to help correct plausible PDEVS specifications and improve logical representation of system descriptions.
- Motivation: Conceptual system descriptions initiate model development by conveying intended system understanding and anticipated simulated behavior.Modelers must also understand modeling-language concepts and methods to formalize structural and behavioral aspects.
- Motivation: Transformer-based agentic frameworks can generate input/output state-based models from system descriptions for simulating time-indexed behaviors.The introduction situates this capability within the growing role of machine learning in modeling and simulation.
- Limitations: PDEVS-LLM approaches generate PDEVS models and statecharts from plausible facts, but expert modelers must examine their correctness and viability.The approach uses grammars for the PDEVS formalism and PDEVS statecharts as the basis for LLM-based statechart generation.
- Problem: Increasing behavioral complexity can create logical misalignments with the conceptual description, requiring manual detection and correction of model inconsistencies.These misalignments motivate an automated verification mechanism for generated PDEVS specifications.
- Contribution: Boolean propositional-logic verification is proposed to aid correction of plausible PDEVS specifications and generate statecharts that logically represent system descriptions.The mechanism is presented as a response to inconsistencies introduced by increasing behavioral complexity.
2. Background
The background defines PDEVS as a modular, hierarchical formalism for discrete-event systems and focuses on atomic-model statecharts. It also introduces propositional-logic satisfiability and entailment as mechanisms for checking behavioral consistency.
- PDEVS foundations: PDEVS models discrete-event systems through interconnected atomic and coupled models within a modular, hierarchical foundation.Atomic models are basic building blocks, while coupled models combine atomic or other coupled models.
- PDEVS foundations: The study limits its specification discussion to atomic PDEVS models because its focus is controlled verification of LLM-generated atomic-model statecharts.Coupled-model specification is explicitly excluded.
- PDEVS statecharts: PDEVS statecharts concretize atomic models using UML statecharts, with external and internal transitions expressed through guarded events and action sequences.The formalism also supports output functions and time allocation through ALRT-DEVS notation.
- Logical verification: Propositional logic represents behavioral traits as formulae whose satisfiability requires a truth assignment making all facts true simultaneously.The PDEVS facts Γ_proc should be contradiction-free for a satisfiable model.
- Logical verification: Entailment Γ ⊧ φ can be verified by checking whether Γ ∪ {¬φ} is unsatisfiable, establishing that no assignment makes Γ true while φ is false.If the combined set is satisfiable, entailment does not hold.
3. Related Work
Prior work applies machine learning, NLP, reinforcement learning, and LLMs to automate simulation-model generation, modification, and refinement. However, existing tools and workflows generally emphasize synthesis or syntactic validity rather than formal correctness and behavioral accuracy.
- ML- and LLM-assisted modeling: NLP and LLM techniques support extracting model elements from text, analyzing simulation outputs, and streamlining modeling and simulation workflows.NLP has been used to identify and extract conceptual-model elements from narrative descriptions, while LLMs are positioned as aids across the simulation lifecycle.
- ML- and LLM-assisted modeling: Reinforcement learning can iteratively modify existing classic DEVS atomic models by mapping DEVS specifications to Markov Decision Processes.The cited approach implements modifications through a proximal policy optimization agent whose actions alter individual model components.
- LLM-based model generation: LLM-based frameworks generate executable simulation models from textual descriptions using human expertise, conversational agents, and Co-Pilot architectures.Examples include inventory-logistics model generation with GPT-Codex and classic DEVS specification through Concept and Formal Specifier agents.
- AI-enhanced simulation tools: Commercial simulation environments increasingly provide AI-assisted model construction, code generation, semantic transformations, and integration of learned models across multiple paradigms.Stella Architect, AnyLogic, and Simulink support AI-enhanced workflows for system dynamics, agent-based or discrete-event modeling, and control or physical-system modeling.
- Research gap: These AI-enhanced tools primarily synthesize models within fixed paradigms and seldom ensure formal correctness or hierarchical behavioral accuracy.Their components largely assist with diagram construction or code suggestions from textual prompts, leaving verification limitations.
- Verification-oriented prompting: Verification-oriented prompting improves generated responses through fact-checking, recursive criticism, key-condition extraction, and human-directed model refinement, but syntactic correctness can diverge from behavioral accuracy.Prior workflows include independently generated verification questions, substitution-based checks, syntactic correction, code generation, and simulation validation.
4. Methodology
The methodology combines agentic LLM generation of PDEVS plausible facts and behavioral conditions with propositional-logic verification and controlled correction. It generates atomic PDEVS statecharts, evaluates them through model checking and a manually aggregated correctness score, and supports iterative regeneration.
- Evaluation and limitations: Timed Automata replicas are manually verified in UPPAAL for deadlock and reachability, while a Statechart Correctness Score aggregates manual assessments of statechart elements.The framework compares model-checking results with and without the proposed verification mechanism and supports iterative, incremental regeneration by the human modeler.
- Framework overview: The revised framework generates atomic PDEVS statecharts from system descriptions using behavioral conditions and LLM-generated plausible PDEVS facts.Its phases include behavioral-condition identification, initial plausible-fact generation, satisfiability checking, and segregated entailment verification with controlled correction.
- Controlled correction: After correction, the plausible-fact set with the most entailed conditions is selected for PDEVS statechart generation.The framework uses an Atomic Model Generator Agent whose prompt incorporates the PDEVS statechart grammar in EBNF style.
- Behavioral representation: Behavioral conditions specify internal transitions, external transitions, and outputs in terms of state and time, while PDEVS functions remain distinct.The external and internal transition functions may read and write state variables; the output function only reads them.
- Logical verification: Natural-language facts and conditions are translated into propositional formulas and checked for satisfiability before verification proceeds.A SAT solver evaluates the logical consistency of facts Γ and conditions φ; contradictions can trigger rectification by a domain expert or LLM.
- Evaluation and limitations: Predefined revision thresholds for facts and conditions terminate the process when satisfiable sets cannot be obtained within the allowed revisions.The thresholds address inconsistencies originating directly from the system description.
5. Experimental Setup
The experiments evaluate an agentic PDEVS-LLM framework using multiple LLMs, propositional-logic verification, and controlled correction. Evaluation covers fourteen curated system descriptions and examines how segregated entailment verification improves generated PDEVS statecharts.
- Experimental configuration: Experiments use multiple base LLMs with temperature fixed at 0.3 and four separate calls for conditions, propositions, logic translation, and verification.The calls support identifying behavioral conditions, extracting system-description propositions, translating PDEVS facts into propositional logic, and verifying entailment.
- Verification implementation: The Boolean SAT solver uses Microsoft’s z3-solver Python library, with satisfiability thresholds m = n = 3 for conditions and facts.Entailment verification is reduced to a satisfiability-check problem.
- Evaluation set: The framework is evaluated on fourteen curated system descriptions, including standalone atomic components with varying behavioral complexity and MiniFab components.Completeness and correctness of generated PDEVS statecharts are compared using generated PDEVS facts.
- Phone case study: For the Phone system, the selected iteration entailed 5 out of 9 behavioral conditions, exceeding the other controlled-correction iterations.The PDEVS facts from this iteration were finalized for the corrected statechart.
- Phone case study: Before verification, the Phone statechart contained inconsistent phase transitions, an unreachable Ready phase, and missing transitions to Off.After correction, most inaccuracies were eliminated, phase reachability was resolved, and missing transitions were added, although the statechart might remain incomplete.
6. Statechart Evaluation
The evaluation combines manually constructed UPPAAL Timed Automata replicas with model checking, expert-based correctness scoring, and experiments across multiple LLMs. Controlled-correction generally improved logical properties and statechart correctness, though some individual scores declined.
- Model-checking evaluation: Model checking was applied to the generated Timed Automata replicas to evaluate properties such as deadlock and reachability.The Phone example included variables for interrupted calls, elapsed time, time advance, and service availability.
- Model-checking evaluation: UPPAAL Timed Automata replicas were manually constructed for PDEVS statecharts to support model checking of their timed behavior.The replicas used Global, Local, and System Declarations and followed an analogy defined for translating PDEVS statecharts into UPPAAL.
- LLM model-checking results: Eight publicly available LLMs were evaluated on 14 system descriptions, and most models improved deadlock and phase-reachability properties after controlled correction.Smaller models including Llama-3.1-8b and Ministral-8b also achieved relatively significant outcomes.
- Statechart correctness scoring: The correctness score evaluates whether transitions and outputs are needed and whether their guards, messages, actions, and time advances are correct.Domain experts assign 1 for Yes and 0 for No when assessing these elements.
- Statechart correctness results: After verification, the Phone statechart scored 0.8214 for external transitions, 0.6670 for internal transitions, and 1.0000 for outputs.External-transition correctness decreased because one incorrect transition remained, while internal-transition correctness showed significant improvement.
- Statechart correctness results: Across eight higher-complexity systems, most LLMs showed notable correctness improvements after verification-based correction, particularly for external transitions and outputs.The experiments compared Statechart Correctness Scores before verification and after verification.
7. Limitations
The framework remains limited by its reliance on contradiction-free system descriptions and accurate LLM translations into propositional logic. Propositional verification is also atemporal and does not adequately address time-advance behavior.
- The framework assumes that the system description contains sufficient information to construct models without contradictions.The system description is the only reference used to extract PDEVS specifications and determine behavior.
- LLM errors in identifying propositions or translating natural language into propositional formulas can misidentify behavioral conditions and produce incorrect PDEVS statecharts.The limitation persists despite providing clear instructions to the LLM.
- Propositional logic is an atemporal starting point that omits behaviors required for PDEVS specifications and cannot significantly improve time-advance verification.Time-advance properties for internal and external transition functions require temporal verification and modification; Timed Automata provide a comparison because they are temporal.
8. Conclusion
The paper proposes a logical-consistency verification mechanism for PDEVS plausible facts within an LLM-based framework. Evaluation indicates improved statechart correctness and completeness, while future work targets hierarchical PDEVS verification and behavioral evaluation frameworks.
- Contributions: The framework introduces logical-consistency verification for PDEVS plausible facts to address inconsistencies in LLM-generated models and code.The mechanism incorporates satisfiability-based verification.
- Evaluation: The verification mechanism consistently improved correctness, especially in internal transitions and output functions, and enhanced completeness across multiple publicly available LLMs.Evaluation combined manual correctness scoring with UPPAAL model checking of Timed Automata variants for deadlock and phase reachability.
- Future work: Future work will extend verification to hierarchical PDEVS models and develop evaluation frameworks for identifying and correcting behavioral issues.The current framework automatically generates coupled models but lacks a correctness-verification mechanism for hierarchical PDEVS behavior.
A. Test cases (systems) for Evaluation
The evaluation uses PDEVS systems curated from established models and characterized by behavioral complexity, including state variables, events, and transition/output functions. Statechart correctness is assessed on eight relatively complex systems to examine the verification mechanism’s handling of intricate behavioral logic.
- Test cases (systems) for Evaluation: The evaluation set comprises PDEVS systems curated from established models and characterized by primary and secondary state variables, input/output events, and transition/output functions.Table 9 presents the curated systems and their complexity dimensions.
- Test cases (systems) for Evaluation: Processor has two phases, two state transitions, and one output function, while Phone has five phases, eleven state transitions, and one output function.Processor comprises Idle and Busy; Phone comprises Active, Off, On, Ready, and SearchingForService.
- Test cases (systems) for Evaluation: Statechart correctness evaluation focuses on eight relatively behaviorally complex systems to highlight verification of intricate behavioral logic.The systems are CarWash, Phone, Coordinator, MachineAB, MachineE, BridgeSystem, and HummingbirdFeeder-1 & 2.