A better understanding of the behavior of a cell, as a system, depends on our ability to model and understand the complex regulatory mechanisms that control gene expression. High level, qualitative models of gene regulatory networks can be used to analyze and characterize the behavior of complex systems, and to provide important insights on the behavior of these systems. In this chapter, we describe a number of additional functionalities that, when supported by a symbolic model checker, make it possible to answer important questions about the nature of the state spaces of gene regulatory networks, such as the nature and size of attractors, and the characteristics of the basins of attraction. We illustrate the type of analysis that can be performed by applying an improved model checker to two well studied gene regulatory models, the network that controls the cell cycle in the yeast S. cerevisiae, and the network that regulates formation of the dorsal-ventral boundary in D. melanogaster. The results show that the insights provided by the analysis can be used to understand and improve the models, and to formulate hypotheses that are biologically relevant and that can be confirmed experimentally.