Model Checking Graph Transformations: A Comparison of Two Approaches

H Ehrig (Editor), Arend Rensink, G. Engels (Editor), Á. Schmidt, F. Parise-Presicce (Editor), D. Varró, G. Rozenberg (Editor)

    Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

    8 Downloads (Pure)


    Abstract. Model checking is increasingly popular for hardware and, more recently, software verification. In this paper we describe two different approaches to extend the benefits of model checking to systems whose behavior is specified by graph transformation systems. One approach is to encode the graphs into the fixed state vectors and the transformation rules into guarded commands that modify these state vectors appropriately to enjoy all the benefits of the years of experience incorporated in existing model checking tools. The other approach is to simulate the graph production rules directly and build the state space directly from the resultant graphs and derivations. This avoids the preprocessing phase, and makes additional abstraction techniques available to handle symmetries and dynamic allocation. In this paper we compare these approaches on the basis of three case studies elaborated in both of them, and we evaluate the results. Our conclusion is that the first approach outperforms the second if the dynamic and/or symmetric nature of the problem under analysis is limited, while the second shows its superiority for inherently dynamic and symmetric problems.
    Original languageEnglish
    Title of host publicationGraph Transformations
    Subtitle of host publicationSecond International Conference, ICGT 2004, Rome, Italy, September 28–October 1, 2004. Proceedings
    EditorsHartmut Ehrig, Gregor Engels, Francesco Parisi-Presicce, Grzegorz Rozenberg
    Number of pages16
    ISBN (Electronic)978-3-540-30203-2
    ISBN (Print)978-3-540-23207-0
    Publication statusPublished - 2004
    Event2nd International Conference on Graph Transformations, ICGT 2004 - Rome, Italy
    Duration: 28 Sep 20041 Oct 2004
    Conference number: 2


    Conference2nd International Conference on Graph Transformations, ICGT 2004
    Abbreviated titleICGT


    • IR-66360
    • EWI-6929


    Dive into the research topics of 'Model Checking Graph Transformations: A Comparison of Two Approaches'. Together they form a unique fingerprint.

    Cite this