Stepwise PCTL Generation with Closed-Loop Validation for Automated SysML Activity Diagram Verification

Abstract

Converting activity diagrams in System Modeling Language (SysML) and natural language requirements into executable probabilistic verification results remains a key bottleneck for safetycritical model-based systems engineering (MBSE). This process involves the use of probabilistic symbolic models (PRISM) and probabilistic computation tree logic (PCTL) specifications. Existing automation approaches suffer from high error rates due to one-shot generation, lack of intermediate validation, and absence of systematic error recovery. This paper proposes a progressive verification pipeline integrating three synergistic innovations: (1) stepwise PCTL generation decomposes synthesis into validated phases; (2) dual-layer structured intermediate representation separates rule-level validation from model-level validation; (3) closed-loop targeted repair applies type-specific correction strategies. Evaluation on 52 industrial cases across 16 domains demonstrates 92% PCTL accuracy and 92% PRISM equivalence, outperforming state-of-the-art baselines by 7-12 percentage points while reducing verification time by over 90%. Ablation studies confirm synergistic gains across all pipeline components.