Graph Abstraction and Abstract Graph Transformation

I.B. Boneva, Arend Rensink, M.E. Kurban, J. Bauer

    Research output: Book/ReportReportProfessional

    402 Downloads (Pure)

    Abstract

    Many important systems like concurrent heap-manipulating programs, communication networks, or distributed algorithms are hard to verify due to their inherent dynamics and unboundedness. Graphs are an intuitive representation of states of these systems, where transitions can be conveniently described by graph transformation rules. We present a framework for the abstraction of graphs supporting abstract graph transformation. The abstraction method naturally generalises previous approaches to abstract graph transformation. The set of possible abstract graphs is finite. This has the pleasant consequence of generating a finite transition system for any start graph and any finite set of transformation rules. Moreover, abstraction preserves a simple logic for expressing properties on graph nodes. The precision of the abstraction can be adjusted according to properties expressed in this logic to be verified.
    Original languageUndefined
    Place of PublicationEnschede
    PublisherFormal Methods and Tools (FMT)
    Number of pages52
    Publication statusPublished - 23 Jul 2007

    Publication series

    NameCTIT Technical Report Series
    PublisherCentre for Telematics and Information Technology, University of Twente
    No.LNCS4549/TR-CTIT-07-50
    ISSN (Print)1381-3625

    Keywords

    • EWI-10786
    • METIS-241792
    • System Verification
    • Graph Transformation
    • IR-64257

    Cite this

    Boneva, I. B., Rensink, A., Kurban, M. E., & Bauer, J. (2007). Graph Abstraction and Abstract Graph Transformation. (CTIT Technical Report Series; No. LNCS4549/TR-CTIT-07-50). Enschede: Formal Methods and Tools (FMT).