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 (a, ?), 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 a 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 (a, ?)-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.