LLM-based Framework for Generating and Verifying Parallel DEVS Statecharts

• URL: http://arxiv.org/abs/2608.14956v1
• Date: Sat, 15 Aug 2026 01:08:39 GMT
• Title: LLM-based Framework for Generating and Verifying Parallel DEVS Statecharts
• Abstract summary: This research introduces an agentic PDEVS-LLM framework to assist human modelers in generating and verifying PDEVS statecharts.<n>A controlled-correction mechanism is developed to verify the logical consistency of the plausible facts.<n>The evaluation of the proposed verification mechanism shows a substantial improvement in the logical consistency of generated statecharts.
• Score: 0.4779196219827507
• License: http://creativecommons.org/licenses/by-sa/4.0/
• 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.

Related papers

• Opt-Verifier: Unleashing the Power of LLMs for Optimization Modeling via Dual-Side Verification [53.763212981479455]
  We propose a novel framework with Dual-side Verification (Opt-Verifier) from both structure and solution perspectives.<n> Experiments on popular benchmarks demonstrate that our approach achieves over 20% improvement in accuracy.
  arXiv  Detail & Related papers  (2026-05-28T08:09:52Z)
• CellScientist: Dual-Space Hierarchical Orchestration for Closed-Loop Refinement of Virtual Cell Models [62.281480231694]
  Virtual Cell Modeling (VCM) requires models that not only predict perturbation responses, but also support targeted revision when predictions fail.<n>Current LLM-assisted modeling face a refinement-routing problem: prediction discrepancies are observed through executable implementations.<n>We propose CellScientist, a dual-space hierarchical framework that couples a high-level hypothesis space with a low-level executable implementation space.
  arXiv  Detail & Related papers  (2026-05-08T06:40:24Z)
• LiveFMBench: Unveiling the Power and Limits of Agentic Workflows in Specification Generation [75.05397479715576]
  Large language models (LLMs) and agents have shown promising progress, but their true capabilities and failure modes remain unclear.<n>We present the first systematic and contamination-aware study of LLM- and agent-based formal specification generation for C programs.
  arXiv  Detail & Related papers  (2026-05-02T11:31:33Z)
• xFODE+: Explainable Type-2 Fuzzy Additive ODEs for Uncertainty Quantification [6.5745172279769255]
  We introduce Explainable Type-2 Fuzzy Additive ODEs for UQ (xFODE+), an interpretable SysID model.<n>xFODE+ produces PIs alongside point predictions while retaining physically meaningful incremental states.<n>Results on benchmark SysID datasets show that xFODE+ matches FODE in PI quality and achieves comparable accuracy.
  arXiv  Detail & Related papers  (2026-04-16T11:16:34Z)
• Ambiguity Detection and Elimination in Automated Executable Process Modeling [1.014361347202587]
  We present a diagnosis-driven framework that detects behavioral inconsistency from the empirical distribution of key performance indicators.<n> Experiments on diabetic nephropathy health-guidance policies show that the method reduces variability in regenerated model behavior.
  arXiv  Detail & Related papers  (2026-04-13T01:11:01Z)
• Addressing Explainability of Generative AI using SMILE (Statistical Model-agnostic Interpretability with Local Explanations) [0.0]
  This thesis introduces gSMILE, a unified framework for the explainability of generative models.<n>gSMILE employs controlled perturbations of textual input, Wasserstein distance metrics, and weighted surrogate modelling.<n>It produces robust, human-aligned attributions and generalises effectively across state-of-the-art generative models.
  arXiv  Detail & Related papers  (2026-02-01T12:54:51Z)
• Every Step Counts: Decoding Trajectories as Authorship Fingerprints of dLLMs [63.82840470917859]
  We show that the decoding mechanism of dLLMs can be used as a powerful tool for model attribution.<n>We propose a novel information extraction scheme called the Directed Decoding Map (DDM), which captures structural relationships between decoding steps and better reveals model-specific behaviors.
  arXiv  Detail & Related papers  (2025-10-02T06:25:10Z)
• PAT-Agent: Autoformalization for Model Checking [17.082027022913998]
  PAT-Agent is an end-to-end framework for natural language autoformalization and formal model repair.<n>It combines the generative capabilities of large language models with the rigor of formal verification.
  arXiv  Detail & Related papers  (2025-09-28T06:32:14Z)
• Representing Timed Automata and Timing Anomalies of Cyber-Physical Production Systems in Knowledge Graphs [51.98400002538092]
  This paper aims to improve model-based anomaly detection in CPPS by combining the learned timed automaton with a formal knowledge graph about the system. Both the model and the detected anomalies are described in the knowledge graph in order to allow operators an easier interpretation of the model and the detected anomalies.
  arXiv  Detail & Related papers  (2023-08-25T15:25:57Z)
• Explainability in Process Outcome Prediction: Guidelines to Obtain Interpretable and Faithful Models [77.34726150561087]
  We define explainability through the interpretability of the explanations and the faithfulness of the explainability model in the field of process outcome prediction. This paper contributes a set of guidelines named X-MOP which allows selecting the appropriate model based on the event log specifications.
  arXiv  Detail & Related papers  (2022-03-30T05:59:50Z)
• Structural Causal Models Are (Solvable by) Credal Networks [70.45873402967297]
  Causal inferences can be obtained by standard algorithms for the updating of credal nets. This contribution should be regarded as a systematic approach to represent structural causal models by credal networks. Experiments show that approximate algorithms for credal networks can immediately be used to do causal inference in real-size problems.
  arXiv  Detail & Related papers  (2020-08-02T11:19:36Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.