Many business processes are modeled as workflows and workflow management systems are used to specify and co-ordinate the execution of those business processes. The ex-ecution of workflows is often constrained, e.g. by business rules, legal requirements or access control. It is therefore important to know whether a workflow spec-ification is consistent and so implementable. This question of workflow satisfiability has been studied by the computer security community in the past. But the solutions produced tend to be tailored to a particular workflow model and don't, therefore, adapt easily to other models or to richer forms of analysis, e.g. those between instances of the same workflow. In this paper we demonstrate that tried and tested tools and techniques from formal methods, notably model check-ing based on linear-time temporal logic and its automata-theoretic extensions (Vardi and Wolper 1994), can be fruit-fully transferred to this setting to provide more robust, uni-form, and expressive foundations for creating and validating plans for authorized workflows. We also discuss the limita-tions of this and other formal approaches in trying to de-cide the satisfiability problem for richer workflow models and briefly explore how hybrid techniques might help solve the problem.