Model checking has been successfully applied to system verification. However, in model checking, the state explosion problem occurs when one checks systems of industrial size. Abstraction-based methods have been particularly successful in this regard. This paper describes a technique to decompose a model checking problem into sub-problems by partitioning the search space. The partitioning is based on the usage of extra variables remembering the history of non-deterministic choices in the model. Furthermore, the search space can be partitioned stepwise in order to get better reduction. Finally, the partition-refinement paradigm is extended to the setting of abstract systems. We show how the partition-based approach used in abstract model checking can improve the efficiency of verification with respect to the requirement of memory by illustrating an application example.