Bisimulation Verification for the DPO Approach with Borrowed Contexts - Rangel, Guilherme; König, Barbara; Ehrig, Hartmut (Electronic Communications of the EASST, 2007)
Bisimilarity is the most widespread notion of behavioral equivalence and hence algorithmsfor bisimulation checking are of fundamental importance for verifying thattwo systems are behaviorally equivalent (seen from the perspective of the environment).We investigate this problem in the context of behavioral equivalences ofgraphs and graph transformation systems, where the extension of the DPO approachto borrowed contexts provides us with a formal basis for reasoning about bisimilarityof graphs. In this paper we extend Hirschkoff's on-the-fly algorithm for bisimulationchecking, enabling it to verify whether two graphs are bisimilar with respect toa given set of productions. We then apply this framework to refactoring problemsand verify instances of a model transformation which describes the minimization ofdeterministic finite automata.