Bisimulation Verification for the DPO Approach with Borrowed Contexts

Abstract

Bisimilarity is the most widespread notion of behavioral equivalence and hence algorithms
for bisimulation checking are of fundamental importance for verifying that
two systems are behaviorally equivalent (seen from the perspective of the environment).
We investigate this problem in the context of behavioral equivalences of
graphs and graph transformation systems, where the extension of the DPO approach
to borrowed contexts provides us with a formal basis for reasoning about bisimilarity
of graphs. In this paper we extend Hirschkoff's on-the-fly algorithm for bisimulation
checking, enabling it to verify whether two graphs are bisimilar with respect to
a given set of productions. We then apply this framework to refactoring problems
and verify instances of a model transformation which describes the minimization of
deterministic finite automata.