@inproceedings{RKE07,
Title = {Bisimulation Verification for the DPO Approach with Borrowed Contexts},
Author = {Rangel, G. and K\"onig, B. and Ehrig, H.},
Booktitle = {Workshop on Graph Transformation and Visual Modelling Techniques (GT-VMT'07)},
Year = {2007},
Isbn = {ISSN 1863-2122},
Editor = {Ehrig, K. and Giese, H.},
Publisher = {Electronic Communications of the EASST},
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 ver- ify instances of a model transformation which describes the minimization of deterministic finite automata.},
Url = {http://tfs.cs.tu-berlin.de/publikationen/Papers07/RKE07.pdf},
Keywords = {graph transformations,bisimulation, refactoring, automata}
}