Model Checking Graph Transformations: A Comparison of Two Approaches

Arend Rensink, Akos Schmidt, Dániel Varro

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

    61 Citations (Scopus)

    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
    Place of PublicationBerlin, Heidelberg
    PublisherSpringer
    Pages226-241
    Number of pages16
    ISBN (Electronic)978-3-540-30203-2
    ISBN (Print)978-3-540-23207-0
    DOIs
    Publication statusPublished - 2004
    Event2nd International Conference on Graph Transformations, ICGT 2004 - Rome, Italy
    Duration: 28 Sep 20041 Oct 2004
    Conference number: 2

    Publication series

    NameLecture Notes in Computer Science
    PublisherSpringer
    Volume3256
    ISSN (Print)0302-9743
    ISSN (Electronic)1611-3349

    Conference

    Conference2nd International Conference on Graph Transformations, ICGT 2004
    Abbreviated titleICGT
    CountryItaly
    CityRome
    Period28/09/041/10/04

    Fingerprint

    Model checking
    Hardware

    Keywords

    • METIS-220447
    • Llogic properties of graphs and transformations
    • Analysis of transformation systems
    • Semantics of visual techniques
    • Model checking

    Cite this

    Rensink, A., Schmidt, A., & Varro, D. (2004). Model Checking Graph Transformations: A Comparison of Two Approaches. In H. Ehrig, G. Engels, F. Parisi-Presicce, & G. Rozenberg (Eds.), Graph Transformations: Second International Conference, ICGT 2004, Rome, Italy, September 28–October 1, 2004. Proceedings (pp. 226-241). (Lecture Notes in Computer Science; Vol. 3256). Berlin, Heidelberg: Springer. https://doi.org/10.1007/b100934
    Rensink, Arend ; Schmidt, Akos ; Varro, Dániel. / Model Checking Graph Transformations : A Comparison of Two Approaches. Graph Transformations: Second International Conference, ICGT 2004, Rome, Italy, September 28–October 1, 2004. Proceedings. editor / Hartmut Ehrig ; Gregor Engels ; Francesco Parisi-Presicce ; Grzegorz Rozenberg. Berlin, Heidelberg : Springer, 2004. pp. 226-241 (Lecture Notes in Computer Science).
    @inproceedings{5c1af087e1cd449f95d4e2e6cddf4764,
    title = "Model Checking Graph Transformations: A Comparison of Two Approaches",
    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.",
    keywords = "METIS-220447, Llogic properties of graphs and transformations, Analysis of transformation systems, Semantics of visual techniques, Model checking",
    author = "Arend Rensink and Akos Schmidt and D{\'a}niel Varro",
    year = "2004",
    doi = "10.1007/b100934",
    language = "English",
    isbn = "978-3-540-23207-0",
    series = "Lecture Notes in Computer Science",
    publisher = "Springer",
    pages = "226--241",
    editor = "Hartmut Ehrig and Gregor Engels and Francesco Parisi-Presicce and Grzegorz Rozenberg",
    booktitle = "Graph Transformations",

    }

    Rensink, A, Schmidt, A & Varro, D 2004, Model Checking Graph Transformations: A Comparison of Two Approaches. in H Ehrig, G Engels, F Parisi-Presicce & G Rozenberg (eds), Graph Transformations: Second International Conference, ICGT 2004, Rome, Italy, September 28–October 1, 2004. Proceedings. Lecture Notes in Computer Science, vol. 3256, Springer, Berlin, Heidelberg, pp. 226-241, 2nd International Conference on Graph Transformations, ICGT 2004, Rome, Italy, 28/09/04. https://doi.org/10.1007/b100934

    Model Checking Graph Transformations : A Comparison of Two Approaches. / Rensink, Arend; Schmidt, Akos; Varro, Dániel.

    Graph Transformations: Second International Conference, ICGT 2004, Rome, Italy, September 28–October 1, 2004. Proceedings. ed. / Hartmut Ehrig; Gregor Engels; Francesco Parisi-Presicce; Grzegorz Rozenberg. Berlin, Heidelberg : Springer, 2004. p. 226-241 (Lecture Notes in Computer Science; Vol. 3256).

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

    TY - GEN

    T1 - Model Checking Graph Transformations

    T2 - A Comparison of Two Approaches

    AU - Rensink, Arend

    AU - Schmidt, Akos

    AU - Varro, Dániel

    PY - 2004

    Y1 - 2004

    N2 - 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.

    AB - 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.

    KW - METIS-220447

    KW - Llogic properties of graphs and transformations

    KW - Analysis of transformation systems

    KW - Semantics of visual techniques

    KW - Model checking

    U2 - 10.1007/b100934

    DO - 10.1007/b100934

    M3 - Conference contribution

    SN - 978-3-540-23207-0

    T3 - Lecture Notes in Computer Science

    SP - 226

    EP - 241

    BT - Graph Transformations

    A2 - Ehrig, Hartmut

    A2 - Engels, Gregor

    A2 - Parisi-Presicce, Francesco

    A2 - Rozenberg, Grzegorz

    PB - Springer

    CY - Berlin, Heidelberg

    ER -

    Rensink A, Schmidt A, Varro D. Model Checking Graph Transformations: A Comparison of Two Approaches. In Ehrig H, Engels G, Parisi-Presicce F, Rozenberg G, editors, Graph Transformations: Second International Conference, ICGT 2004, Rome, Italy, September 28–October 1, 2004. Proceedings. Berlin, Heidelberg: Springer. 2004. p. 226-241. (Lecture Notes in Computer Science). https://doi.org/10.1007/b100934