Verification Techniques for Graph Rewriting (Tutorial)

Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademic

23 Downloads (Pure)

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
Publication statusPublished - Mar 2016

Publication series

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

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. https://doi.org/10.4230/DagRep.5.11.1
Rensink, Arend. / Verification Techniques for Graph Rewriting (Tutorial). Verification of Evolving Graph Structures. editor / Parosh Aziz Abdulla ; Fabio Gadducci ; Barbara König ; Viktor Vafeiadis. Dagstuhl, Germany : Dagstuhl Publishing, 2016. pp. 18-18 (Dagstuhl Reports; 11).
@inproceedings{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",
language = "Undefined",
series = "Dagstuhl Reports",
publisher = "Dagstuhl Publishing",
number = "11",
pages = "18--18",
editor = "Abdulla, {Parosh Aziz} and Fabio Gadducci and Barbara K{\"o}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. https://doi.org/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: Chapter in Book/Report/Conference proceedingConference contributionAcademic

TY - GEN

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

A2 - Abdulla, Parosh Aziz

A2 - Gadducci, Fabio

A2 - König, Barbara

A2 - Vafeiadis, Viktor

PB - Dagstuhl Publishing

CY - Dagstuhl, Germany

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). https://doi.org/10.4230/DagRep.5.11.1