Property preserving abstractions for the verification of concurrent systems

We study property preserving transformations for reactive systems. The main idea is the use of simulations parameterized by Galois connections (, ), relating the lattices of properties of two systems. We propose and study a notion of preservation of properties expressed by formulas of a logic, by a function mapping sets of states of a systemS into sets of states of a systemS'. We give results on the preservation of properties expressed in sublanguages of the branching time -calculus when two systemsS andS' are related via (, )-simulations. They can be used to verify a property for a system by verifying the same property on a simpler system which is an abstraction of it. We show also under which conditions abstraction of concurrent systems can be computed from the abstraction of their components. This allows a compositional application of the proposed verification method.This is a revised version of the papers 2] and 16]; the results are fully developed in 28].This work was partially supported by ESPRIT Basic Research Action REACT.Verimag is a joint laboratory of CNRS, Institut National Polytechnique de Grenoble, Université J. Fourier and Verilog SA associated with IMAG.