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 (alpha, gamma), 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 alpha mapping sets of states of a system S into sets of states of a system S'. We give results on the preservation of properties expressed in sublanguages of the branching time mu-calculus when two systems S and S' are related via [alpha, gamma]-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].