The advent of ever more complex reactive systems in increasingly criti
cal areas calls for the development of automated verification techniqu
es. Model checking is one such technique, which has proven quite succe
ssful. However, the state-explosion problem remains a major stumbling
block. Recent experience indicates that solutions are to be found in t
he application of techniques for property-preserving abstraction and s
uccessive approximation of models. Most such applications have so far
been based solely on the property-preserving characteristics of simula
tion relations. A major drawback of all these results is that they do
not offer a satisfactory formalization of the notion of precision of a
bstractions. The theory of Abstract Interpretation offers a framework
for the definition and justification of property-preserving abstractio
ns. Furthermore, it provides a method for the effective computation of
abstract models directly from the text of a program, thereby avoiding
the need for intermediate storage of a full-blown model. Finally, it
formalizes the notion of optimality, while allowing to trade precision
for speed by computing suboptimal approximations. For a long time, ap
plications of Abstract Interpretation have mainly focused on the analy
sis of universal safety properties, i.e., properties that hold in all
states along every possible execution path. In this article, we extend
Abstract Interpretation to the analysis of both existential and unive
rsal reactive properties, as expressible in the modal mu-calculus. It
is shown how abstract models may be constructed by symbolic execution
of programs. A notion of approximation between abstract models is defi
ned while conditions are given under which optimal models can be const
ructed. Examples are given to illustrate this. We indicate conditions
under which also falsehood of formulae is preserved. Finally, we compa
re our approach to those based on simulation relations.