Neighbourhood Abstraction in GROOVE

Arend Rensink; Eduardo Zambon

doi:10.14279/tuj.eceasst.32.501.475

Neighbourhood Abstraction in GROOVE

Arend Rensink, Eduardo Zambon

Research output: Contribution to journal › Conference article › Academic › peer-review

9 Citations (Scopus)

1 Downloads (Pure)

Abstract

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 language	English
Pages (from-to)	1-13
Number of pages	13
Journal	EASST electronic communications
Volume	32
DOIs	https://doi.org/10.14279/tuj.eceasst.32.501.475
Publication status	Published - 11 Apr 2011
Event	Fourth 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 2010 → 28 Sept 2010 Conference number: 4

Keywords

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

Access to Document

10.14279/tuj.eceasst.32.501.475

http://journal.ub.tu-berlin.de/index.php/eceasst/article/view/501

Cite this

@article{6d00ad2054b940508bc2ed12880b9efb,

title = "Neighbourhood Abstraction in GROOVE",

abstract = "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.",

keywords = "IR-76652, METIS-270989, Graph Abstraction, EWI-20018, GROOVE, Model Checking, Graph Transformation",

author = "Arend Rensink and Eduardo Zambon",

year = "2011",

month = apr,

day = "11",

doi = "10.14279/tuj.eceasst.32.501.475",

language = "English",

volume = "32",

pages = "1--13",

journal = "EASST electronic communications",

issn = "1863-2122",

publisher = "European Association of Software Science and Technology",

note = "Fourth International Workshop on Graph-Based Tools, GraBaTs 2010 : Proceedings of the Fourth International Workshop on Graph-Based Tools (GraBaTs 2010), GraBaTs 2010 ; Conference date: 28-09-2010 Through 28-09-2010",

}

TY - JOUR

T1 - Neighbourhood Abstraction in GROOVE

AU - Rensink, Arend

AU - Zambon, Eduardo

N1 - Conference code: 4

PY - 2011/4/11

Y1 - 2011/4/11

N2 - 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.

AB - 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.

KW - IR-76652

KW - METIS-270989

KW - Graph Abstraction

KW - EWI-20018

KW - GROOVE

KW - Model Checking

KW - Graph Transformation

UR - http://www.scopus.com/inward/record.url?scp=85042869981&partnerID=8YFLogxK

U2 - 10.14279/tuj.eceasst.32.501.475

DO - 10.14279/tuj.eceasst.32.501.475

M3 - Conference article

SN - 1863-2122

VL - 32

SP - 1

EP - 13

JO - EASST electronic communications

JF - EASST electronic communications

T2 - Fourth International Workshop on Graph-Based Tools, GraBaTs 2010

Y2 - 28 September 2010 through 28 September 2010

ER -

Neighbourhood Abstraction in GROOVE

Abstract

Keywords

Access to Document

Other files and links

Fingerprint

Cite this