A Workflow Model with Temporal Logic Constraints and Its Automated Verification

Traditional workflow models are weak in describing the temporal properties and constraints between activities, while some high-level extensions based on time or temporal logic have another problem that the soundness verification of the model requires high academic knowledge. In order to solve these problems, a new workflow model LTL-WF based on WF-net and linear temporal logic is proposed in this paper. Besides introducing the new model, we also bring forward a method for automated verification of LTL-WF. The method proposed here provides the verification of workflow model with a convenient environment for model checking.