Neighbourhood Abstraction in GROOVE

Arend Rensink, Eduardo Zambon

    Research output: Contribution to journalConference articleAcademicpeer-review

    9 Citations (Scopus)


    Important classes of graph grammars have infinite state spaces and therefore cannot be verified with traditional model checking techniques. One way to address this problem is to perform graph abstraction, which allows us to generate a finite abstract state space that over-approximates the original one. In previous work we developed the theory of neighbourhood abstraction. In this paper, we present the implementation of this theory in GROOVE and illustrate its use with a small grammar that models operations on a single-linked list.
    Original languageEnglish
    Pages (from-to)1-13
    Number of pages13
    JournalEASST electronic communications
    Publication statusPublished - 11 Apr 2011
    EventFourth International Workshop on Graph-Based Tools, GraBaTs 2010: Proceedings of the Fourth International Workshop on Graph-Based Tools (GraBaTs 2010) - University of Twente, Enschede, Netherlands
    Duration: 28 Sept 201028 Sept 2010
    Conference number: 4


    • IR-76652
    • METIS-270989
    • Graph Abstraction
    • EWI-20018
    • GROOVE
    • Model Checking
    • Graph Transformation

    Cite this