ABSTRACT INTERPRETATION OF REACTIVE SYSTEMS

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.