The reduction technique is an important analysis method for business process models. Existing informal reduction methods suffer from the infirm completeness because of their lack of formal fundamental. Also, Petri-net-based reduction methods available cannot guarantee the soundness due to their unspecific applications for process models. A sound and complete set of reduction rules is presented for free choice WF-nets. The soundness determines that the behavioral correctness of such a model is preserved during the reduction, and the completeness ensures that every such a correct WF-net can be finally reduced to its simplest form. Based on this, a sound and complete set of synthesis rules are given, which facilitates the design and refinement of process models.