@article{LGS+95,
title = { Property Preserving Abstractions for the Verification of Concurrent Systems },
author = {Loiseaux, Claire and Graf, Susanne and Sifakis, Joseph and Bouajjani, Ahmed and Bensalem, Saddek},
month = {January},
year = {1995},
journal = {Formal Methods in System Design},
volume = {6, issue 1},
team = {DCS},
abstract = {We study property preserving transformations for reactive systems. The main idea is the use of simulations parameterized by Galois connections <I>(alpha,gamma)</I>, 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 <I>alpha</I> mapping sets of states of a system <I>S</I> into sets of states of a system <I>S\\\'</I>. Roughly speaking, <I>alpha</I> preserves <I>f</I> if the satisfaction of <I>f</I> at some state of <I>S</I> implies that <I>f</I> is satisfied by any state in the image of this state by <I>alpha</I>. We give results on the preservation of properties expressed in sublanguages of the branching time <I>mu</I>-calculus when two systems <I>S</I> and <I>S\\\'</I> are related via <I>(alpha,gamma)</I>-simulations. They can be used in particular to verify a property for a system by proving this 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 that appeared in CAV\\\'92 [BensalemBouajjaniLoiseauxSifakis92] and in TAPSOFT\\\'93 [GrafLoiseaux92]; the results are fully developed in the thesis of Claire Loiseaux (in French). },
}
