Prof. Dr. Barbara König, Universität Duisburg-Essen, Duisburg

Abstract:

Dynamic systems can often be naturally described in terms of graphs and their graph transformation rules. In oder to verify such systems it is necessary to specify graphs using siutable logics or specification languages. I will review such logics, mainly first-order and monadic second-order logics and nested graph conditions. In addition I will focus on an cospan-based view on graphs, where graphs are composed of building blocks consisting of a left and a right interface.

With the helf of these logics one can define suitable verification techniques, for invariant checking, computation of pre- and postconditions and confluence analyses. In addition I will present some ideas for a general framework for the abstract interpretation of graph transformation systems.