Collaboration-based designs [2, 8, 11] are an effective software development approach due to its achievement in separation of concerns [5, 12]. These designs also demand a new model checking technique allowing to prove system correctness by verifying each collaboration individually with a minimum assumption about other collaborations. To verify a collaboration of multiple actors, a typical technique consists of constructing a standard cross-product of actor statecharts as global state space and then checking properties with respect to that global space.This paper initially points out some drawbacks of a previous approach [2] in verifying collaboration. Then, in addition to intra-object behaviors in statecharts as of [2], we first improve the technique by imposing additional constraints to model checking process via protocol invariants which are essentially inter-object behaviors. Due to these additional constraints, state space is reduced and more importantly, our model reflects more accurately about system behavior by eliminating those unreachable states. Second, a more general form, i.e. multiple exit and re-entry states, of the interface between two collaborations is used instead of a fixed interface with single exit and re-entry states. Some pre-processing work on reentry states and solutions to specifics of properties to be verified are also discussed regarding to the soundness of the verification algorithm.