Abstract

This tutorial paints a high-level picture of the concepts involved in verification of graph transformation systems. We distinguish three fundamentally different application scenarios for graph rewriting: (1) as grammars (in which case we are interested in the language, or set, of terminal graphs for a fixed start graph); (2) as production systems (in which case we are interested in the relation between start and terminal graphs); or (3) as behavioural specifications (in which case we are interested in the transition system as a whole). We then list some types of questions one might want to answer through verification: confluence and termination, reachability, temporal properties, or contractual properties. Finally, we list some techniques that can help in providing answers: model checking, unfolding, assertional reasoning, and abstraction.
Original languageUndefined
Title of host publicationVerification of Evolving Graph Structures
EditorsParosh Aziz Abdulla, Fabio Gadducci, Barbara König, Viktor Vafeiadis
Place of PublicationDagstuhl, Germany
PublisherDagstuhl Publishing
Pages18-18
Number of pages1
DOIs
StatePublished - Mar 2016

Publication series

NameDagstuhl Reports
PublisherDagstuhl Publishing
Number11
Volume5
ISSN (Print)2192-5283

Fingerprint

Model checking
Paint
Specifications

Keywords

  • EWI-26905
  • METIS-316865
  • IR-100130

Cite this

Rensink, A. (2016). Verification Techniques for Graph Rewriting (Tutorial). In P. A. Abdulla, F. Gadducci, B. König, & V. Vafeiadis (Eds.), Verification of Evolving Graph Structures (pp. 18-18). (Dagstuhl Reports; Vol. 5, No. 11). Dagstuhl, Germany: Dagstuhl Publishing. DOI: 10.4230/DagRep.5.11.1

Rensink, Arend / Verification Techniques for Graph Rewriting (Tutorial).

Verification of Evolving Graph Structures. ed. / Parosh Aziz Abdulla; Fabio Gadducci; Barbara König; Viktor Vafeiadis. Dagstuhl, Germany : Dagstuhl Publishing, 2016. p. 18-18 (Dagstuhl Reports; Vol. 5, No. 11).

Research output: ScientificConference contribution

@inbook{fca68549859041178515997b499e9eec,
title = "Verification Techniques for Graph Rewriting (Tutorial)",
abstract = "This tutorial paints a high-level picture of the concepts involved in verification of graph transformation systems. We distinguish three fundamentally different application scenarios for graph rewriting: (1) as grammars (in which case we are interested in the language, or set, of terminal graphs for a fixed start graph); (2) as production systems (in which case we are interested in the relation between start and terminal graphs); or (3) as behavioural specifications (in which case we are interested in the transition system as a whole). We then list some types of questions one might want to answer through verification: confluence and termination, reachability, temporal properties, or contractual properties. Finally, we list some techniques that can help in providing answers: model checking, unfolding, assertional reasoning, and abstraction.",
keywords = "EWI-26905, METIS-316865, IR-100130",
author = "Arend Rensink",
note = "eemcs-eprint-26905",
year = "2016",
month = "3",
doi = "10.4230/DagRep.5.11.1",
series = "Dagstuhl Reports",
publisher = "Dagstuhl Publishing",
number = "11",
pages = "18--18",
editor = "Abdulla, {Parosh Aziz} and Fabio Gadducci and Barbara König and Viktor Vafeiadis",
booktitle = "Verification of Evolving Graph Structures",

}

Rensink, A 2016, Verification Techniques for Graph Rewriting (Tutorial). in PA Abdulla, F Gadducci, B König & V Vafeiadis (eds), Verification of Evolving Graph Structures. Dagstuhl Reports, no. 11, vol. 5, Dagstuhl Publishing, Dagstuhl, Germany, pp. 18-18. DOI: 10.4230/DagRep.5.11.1

Verification Techniques for Graph Rewriting (Tutorial). / Rensink, Arend.

Verification of Evolving Graph Structures. ed. / Parosh Aziz Abdulla; Fabio Gadducci; Barbara König; Viktor Vafeiadis. Dagstuhl, Germany : Dagstuhl Publishing, 2016. p. 18-18 (Dagstuhl Reports; Vol. 5, No. 11).

Research output: ScientificConference contribution

TY - CHAP

T1 - Verification Techniques for Graph Rewriting (Tutorial)

AU - Rensink,Arend

N1 - eemcs-eprint-26905

PY - 2016/3

Y1 - 2016/3

N2 - This tutorial paints a high-level picture of the concepts involved in verification of graph transformation systems. We distinguish three fundamentally different application scenarios for graph rewriting: (1) as grammars (in which case we are interested in the language, or set, of terminal graphs for a fixed start graph); (2) as production systems (in which case we are interested in the relation between start and terminal graphs); or (3) as behavioural specifications (in which case we are interested in the transition system as a whole). We then list some types of questions one might want to answer through verification: confluence and termination, reachability, temporal properties, or contractual properties. Finally, we list some techniques that can help in providing answers: model checking, unfolding, assertional reasoning, and abstraction.

AB - This tutorial paints a high-level picture of the concepts involved in verification of graph transformation systems. We distinguish three fundamentally different application scenarios for graph rewriting: (1) as grammars (in which case we are interested in the language, or set, of terminal graphs for a fixed start graph); (2) as production systems (in which case we are interested in the relation between start and terminal graphs); or (3) as behavioural specifications (in which case we are interested in the transition system as a whole). We then list some types of questions one might want to answer through verification: confluence and termination, reachability, temporal properties, or contractual properties. Finally, we list some techniques that can help in providing answers: model checking, unfolding, assertional reasoning, and abstraction.

KW - EWI-26905

KW - METIS-316865

KW - IR-100130

U2 - 10.4230/DagRep.5.11.1

DO - 10.4230/DagRep.5.11.1

M3 - Conference contribution

T3 - Dagstuhl Reports

SP - 18

EP - 18

BT - Verification of Evolving Graph Structures

PB - Dagstuhl Publishing

ER -

Rensink A. Verification Techniques for Graph Rewriting (Tutorial). In Abdulla PA, Gadducci F, König B, Vafeiadis V, editors, Verification of Evolving Graph Structures. Dagstuhl, Germany: Dagstuhl Publishing. 2016. p. 18-18. (Dagstuhl Reports; 11). Available from, DOI: 10.4230/DagRep.5.11.1