Unfolding Shape Graphs

P.W. Sathyanathan, Arend Rensink

    Research output: Book/ReportReportProfessional

    39 Downloads (Pure)


    Shape graphs have been introduced in [Ren04a, Ren04b] as an abstraction to be used in model checking object oriented software, where states of the system are represented as graphs. Intuitively, the graphs modeling the states represent the structure of objects dynamically allocated in the heap. State transitions are then generated by applying graph transformation rules corresponding to the statements of the program. Since the state space of such systems is potentially unbounded, the graphs representing the states are abstracted by shape graphs. Graph transformation systems may be analyzed [BCK01, BK02] by constructing finite structures that approximate their behaviour with arbitrary accuracy, by using techniques developed in the context of Petri nets. The approach of [BK02] is to construct a chain of finite under-approximations of the Winskel’s style unfolding of a graph grammar, as well as a chain of finite over-approximations of the unfolding, where both chains converge to the full unfolding. The approximations may then be used to check properties of the underlying graph transformation system. We apply this technique to approximate the behaviour of systems represented by shape graphs and graph tranformation rules.
    Original languageUndefined
    Place of PublicationEnschede
    PublisherCentre for Telematics and Information Technology (CTIT)
    Number of pages28
    Publication statusPublished - 22 Nov 2006

    Publication series

    NameCTIT Technical Report Series
    PublisherCentre for Telematics and Information Technology, University of Twente
    ISSN (Print)1381-3625


    • IR-66524
    • METIS-238695
    • EWI-7576

    Cite this