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 LTLWF. The method proposed here provides the verification of workflow model with a convenient environment for model checking.