工作流系统中的活动是与时间有紧密关系的，如何保证恰当的活动在恰当时间被执行是工作流系统中的关键问题。探讨了如何利用时序逻辑来解决上述问题，提出了工作流系统中有效性的概念，给出了基于时序逻辑的有效性约束模型，并利用模型检测技术提供了验证有效性约束的方法，最后给出一个实例说明该方法的正确性。

The activities are closely related with time in workflow systems．How to guarantee that the activity is executed at a appropriate time has became the crucial problem in workflow systems．In this paper， temporal logic was used to solve this problem．Firstly，the concept of validity in workflow system was presented．Then propose a model of validity constraint based on temporal logic and the method to verify the validity constraint of the model．Finally，a instance is used for showing the validity of the method．