2015/11/03 by Guilherme Rangel, Rangel, Guilherme, Barbara König +3
Computer Science · #Advanced Software Engineering Methodologies #Formal Methods in Verification #Model-Driven Software Engineering Techniques
paper · doi:10.14279/tuj.eceasst.6.70
openalex publication_date 2024/03/12 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/01
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.