Reference:

J. Bauer, Iovka Boneva, Arend Rensink, and Marcos E. Kurban. A modal-logic based graph abstraction. In Reiko Heckel and Gabriele Taentzer, editors, International Conference of Graph Transformation. Springer, 2008.

Abstract:

Infinite or very large state spaces often prohibit the successful verification of graph transformation systems. Abstract graph transformation is an approach that tackles this problem by abstracting graphs to abstract graphs of bounded size and by lifting application of productions to abstract graphs. In this work, we present a new framework of abstractions unifying and generalising existing takes on abstract graph transformation. The precision of the abstraction can be adjusted according to the properties to be verified facilitating abstraction refinement. We present a modal logic defined on graphs, which is preserved and reflected by our abstractions. Finally, we demonstrate the usability of the framework by verifying a graph transformation model of a firewall.

Keywords:

graph abstractions, modal logic, property preservation and reflection, firewalls

Suggested BibTeX entry:

@inproceedings{BBRK08,
    author = {J. Bauer and Iovka Boneva and Arend Rensink and Marcos E. Kurban},
    booktitle = {International Conference of Graph Transformation},
    editor = {Reiko Heckel and Gabriele Taentzer},
    publisher = {Springer},
    title = {A Modal-Logic Based Graph Abstraction},
    year = {2008}
}