文章基本信息

标题：Bisimulation Verification for the DPO Approach with Borrowed Contexts
本地全文：下载
作者：Guilherme Rangel ; Barbara König ; Hartmut Ehrig 等
期刊名称：Electronic Communications of the EASST
电子版ISSN：1863-2122
出版年度：2007
卷号：6
语种：English
出版社：European Association of Software Science and Technology (EASST)
摘要：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.