With the rapid growth of networking and high-computing power, the demand of larger
and more complex software systems has increased dramatically. 
To deal with the complexity in designing large-scale complex software 
systems has gained popularity recently.
However, in pursing a component-based approach there are obstacols to overcome.
One of them is the state-explosion problem in the formal verifiaction of 
large-scale component-based systems.
In this paper, we introduce a modelling technique and two condensation 
theories to model and verify component-based systems. Our condensation 
theories are much weaker than current theories useful for compositional 
verifiaction.
More significantly, our new condensation theories can eliminate the 
interleaved behaviours caused by asynchronously sending actions. 
Therefore, our technique can efficiently analyze several state-based 
properties: deadlock state and reachable state. The experimental results 
shows a significant improvement in the analysis of large-scale component 
based systems