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). },


Contact | Site Map | Site powered by SPIP 4.2.13 + AHUNTSIC [CC License]

info visites 4003108