Automatic Verifi cation of Bisimilarity on Graph Transformation Systems

In "Deriving Bisimulation Congruences in the DPO Approach to Graph
Rewriting" by Hartmut Ehrig and Barbara König it was shown that
bisimilarities derived via borrowed contexts are congruences.
In this talk we will discuss the main ideas of algorithms for the automatic creation and veri cation of bisimulation congruences on graph
transformation systems. Given two graphs sharing the same interface,
we have a look at the following steps: First we o ffer an option
to fi nd all possible steps for a given set of rules. Afterwards we reduce the resulting transition systems with up-to-context techniques
to possibly obtain a  finite relation, without changing the notion of behavioural equivalence. Given the two transition systems calculated by
the former steps, we fi nally obtain a bisimulation using the fixpoint-, or the Hirschkoff  algorithm. The concepts were realized in Mathematica
which will be introduced to show some examples at work.