LLaMA-PG: A domain-knowledge-enhanced framework for verification property generation from BPMN models

The integration of 5G and AI technologies in the industrial internet supports collaborative production systems that orchestrate temporary compositions of industrial components. These compositions should be verified to ensure that their combined behavior satisfies expected functional requirements. However, the transfer of general large-language-model-based property-generation approaches to BPMN is non-trivial. BPMN models mix executable control-flow semantics with diagrammatic markup and encode business constraints through structural XML in an incomplete manner. They also require reasoning over gateways, loops, synchronization, and exception handling before temporal-logic properties can be formulated. To address these BPMN-specific difficulties, LLaMA-PG is proposed as an assistive framework for verification property generation from business workflows represented in BPMN. The framework comprises two task-oriented phases. In Phase 1, model-checking knowledge is injected into a base large language model through continued pre-training on a refined formal-verification corpus. This step enables the model to internalize the terminology and logical regularities required for BPMN verification. In Phase 2, the BPMN-to-property task is decomposed into four sequential steps, including attentional filtering, causal inference, property formulation, and symbolic translation. The model therefore generates properties through inspectable intermediate reasoning rather than direct black-box translation. In addition, a BPMN-oriented data preparation and quality-control pipeline is designed to reduce instances with structural inconsistency and semantic misalignment. Experimental results show that LLaMA-PG outperforms the compared methods in Syntactic Compliance Rate, Model-Checker Executability, Correctness, and Reference Coverage Recall, while maintaining a lower Redundancy Ratio in the generated property sets.