Verification Techniques for Graph Rewriting (Tutorial)

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

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