AbstractThe temporal logic model checking method is very useful for verification of concurrent programs that can be expressed by finite state transition systems. However, a major drawback to using this method is that as the scale of the programs increases, the computation costs for verification increase exponentially. An effective solution for this problem is compositional verification. Compositional verification is a method in which the bisimulation equivalence of concurrent programs is used to extract from each construction element (subprocess) only that abstract information necessary to verify each query, thereby avoiding an explosion in cost.In this paper, PQL (Process Query Language) is proposed as an improved method in the solution of this problem. PQL is based on modal logic which is the union of temporal and process logic. Also in this paper, the compositional verification method is proposed by using PQL with consideration of the “divergence by internal transition