Abstract: Although business process execution language for Web services (BPEL) has many features that make it suitable for describing service composition, it lacks formal semantics so that composition process cannot be strictly analyzed and verified. In this paper, a Petri net-based analysis method for composition process is proposed. Petri net is applied to describe the semantics of BPEL and define the basic activities and relationships of service processes. By constructing the example net of the target service, a decision theorem is proposed for BPEL composition process, and an algorithm is given to reduce the search space of services. Finally, a specific example is utilized to simulate the analysis procedure of service processes, which shows the effective of the proposed method.