Model checking is emerging as a practical tool for automated debugging of reactive systems such as embedded controllers and network protocols [9,11]. Since model checking is based on exhaustive state-space exploration, and the size of the state space of a design grows exponentially with the size of the description, scalability remains a challenge. The goal of our recent research has been to develop techniques for exploiting the modular design structure during model checking. Software design notations (e.g. Statecharts [10], Uml) provide rich constructs to facilitate modular descriptions. Instead of destroying this structure by compiling the descriptions into flat state-transition graphs, we are developing algorithms that are optimized for modular descriptions. In this talk, we summarize research concerning two different notions of hierarchy: architectural and behavioral.