Abstract:This paper addresses the state-space explosion problem in the context of verifying component composition. It adapts the counterexample guided abstraction refinement (CEGAR) scheme and proposes a compositional verification approach that the verification of component composition is transformed into local abstraction refinement for individual components participating in the composition in order to reduce analysis complexity. The existential quotient based on equivalence relation is employed to compute the abstraction of each component in component composition, and then the abstraction model for the component composition can be built by composing the existential quotients of components. A compositional validation theorem is proposed and proved, so validating if a generated counterexample is valid and refining the abstraction are all carried out component-wise. This approach does not require the construction of a complete state space of the concrete component composition under verification.