It is important to reason about a number of desirable protocol properties to ensure correctness of a designed communicating system. Such properties can be formulated in some temporal logic. If the specification of a communicating system is finite-state, that is, the system has a finite number of distinct states, it is often possible to verify automatically by an efficient algorithm, called a model checking algorithm, whether the system satisfies a property expressed in the logic. We describe a model checking method for Communicating Systems. An implementation of this model-checking facility is obtained by combining two automated tools, namely, CWB (the Concurrency Workbench developed at Edinburgh, Sussex and SICS) and EMC (the Extended Model Checker developed by Emerson and Clarke). In the EMC, there is an efficient model checking algorithm for branching time temporal logic(CTL) with the standard semantics. We change the standard semantics for CTL in terms of communication actions. We implement a transformation of the transition graph into a finite number of distinct states so that it can be fed into EMC to use our logic.