Formal dynamic semantics for semantically annotated process model

Semantically annotated process model (SPM) is a process model with semantic annotations, i.e., precondition/effect, labeled for its activities based on the domain ontology. Such model can increase the model's readability and reusability, and facilitate its implement as well as compliance analysis. However, SPM analysis is challenging, since its correctness is beyond the soundness of process model and its state transition needs to care about domain state change. To assure the correctness of SPM, the executablity analysis, i.e., whether each activity is executable when it is active, is essential and has also been identified as a coNP-hard problem. To tame the executability, we define a dynamic semantics for SPM based on the related variable set (RVA) model which is proposed for defining domain state transition. Our formal semantics paves the way for executability checking and compliance analysis.