Abstract Interpretation of Reactive Systems: Abstractions Preserving UniversalCTL(*), Existential CTL(*) and CTL(*)

摘要

The need for formal verification of systems on one hand, and the advent ofcomplex reactive systems on the other, call for the development of automated verification techniques. Model checking is one such technique. The theory of Abstract interpretation offers a framework for the definition and justification of property preserving abstractions. However, Abstract Interpretation has traditionally been focussed on abstractions that preserve safety properties of programs, properties that hold in all states along every possible execution path. In the paper, the authors show how it can be extended to the analysis of different kinds of reactive properties. To this purpose, they introduce two notions of abstraction of non-deterministic systems. One preserves Universal Computation Tree Logic (CTL*), the fragment of the branching time logic CTL* which allows only universal path quantification. Another preserves Existential CTL*, the fragment only allowing existential path quantification. Furthermore the authors show that a combination of both notions preserves full CTL*. This brings several powerful techniques from Abstract Interpretation within the reach of model checking, including the construction of abstract models by symbolic execution of programs and the use of approximations to find an optimum between precision and speed. Examples are given tol illustrate these.