Implementation of LMNtal Model Checkers: A Metaprogramming Approach

    Research output: Contribution to journalArticle

    Abstract

    LMNtal is a modeling language based on hierarchical graph rewriting, and its implementation SLIM features state space search and an LTL model checker. Several variations and extensions of the SLIM have been developed, and all of them achieve their functionalities by modifying SLIM written in C. If a model checker is implemented in the modeling language itself, it should be easy to develop prototypes of various model checkers without changing the base implementation of the model checker. This approach is called metaprogramming which has been taken extensively in Lisp and Prolog communities. In this paper, we design a framework for implementing extendable model checkers. First, we define first-class rewrite rules to extend a mod- eling language. Second, we design an API to operate on the states of programs. These features enable programmers to handle state transition graphs as first-class objects and implement diverse variants of a model checker without changing SLIM. We demonstrate it by implementing an LTL model checker and its variant and a CTL model checker. Furthermore, we show how easy it is to extend these model checkers in our framework by extending the CTL model checker to handle fairness constraints. The over- head of metainterpretation is around an order of magnitude or less. All these results demonstrate the viability of the resulting framework based on meta-interpreters that handle explicit state space in a flexible manner.

    Original languageEnglish
    JournalJournal of Object Technology
    Volume17
    Issue number1
    DOIs
    Publication statusPublished - 2018 Nov 1

    Fingerprint

    Application programming interfaces (API)
    Modeling languages

    Keywords

    • Graph rewriting
    • Meta-interpreters
    • Model checkers
    • State- space search

    ASJC Scopus subject areas

    • Software

    Cite this

    Implementation of LMNtal Model Checkers : A Metaprogramming Approach. / Tsunekawa, Yutaro; Tomioka, Taichi; Ueda, Kazunori.

    In: Journal of Object Technology, Vol. 17, No. 1, 01.11.2018.

    Research output: Contribution to journalArticle

    @article{1bb6126416bd4d8f88c31fb9226dff25,
    title = "Implementation of LMNtal Model Checkers: A Metaprogramming Approach",
    abstract = "LMNtal is a modeling language based on hierarchical graph rewriting, and its implementation SLIM features state space search and an LTL model checker. Several variations and extensions of the SLIM have been developed, and all of them achieve their functionalities by modifying SLIM written in C. If a model checker is implemented in the modeling language itself, it should be easy to develop prototypes of various model checkers without changing the base implementation of the model checker. This approach is called metaprogramming which has been taken extensively in Lisp and Prolog communities. In this paper, we design a framework for implementing extendable model checkers. First, we define first-class rewrite rules to extend a mod- eling language. Second, we design an API to operate on the states of programs. These features enable programmers to handle state transition graphs as first-class objects and implement diverse variants of a model checker without changing SLIM. We demonstrate it by implementing an LTL model checker and its variant and a CTL model checker. Furthermore, we show how easy it is to extend these model checkers in our framework by extending the CTL model checker to handle fairness constraints. The over- head of metainterpretation is around an order of magnitude or less. All these results demonstrate the viability of the resulting framework based on meta-interpreters that handle explicit state space in a flexible manner.",
    keywords = "Graph rewriting, Meta-interpreters, Model checkers, State- space search",
    author = "Yutaro Tsunekawa and Taichi Tomioka and Kazunori Ueda",
    year = "2018",
    month = "11",
    day = "1",
    doi = "10.5381/jot.2018.17.1.a1",
    language = "English",
    volume = "17",
    journal = "Journal of Object Technology",
    issn = "1660-1769",
    publisher = "Journal of Object Technology",
    number = "1",

    }

    TY - JOUR

    T1 - Implementation of LMNtal Model Checkers

    T2 - A Metaprogramming Approach

    AU - Tsunekawa, Yutaro

    AU - Tomioka, Taichi

    AU - Ueda, Kazunori

    PY - 2018/11/1

    Y1 - 2018/11/1

    N2 - LMNtal is a modeling language based on hierarchical graph rewriting, and its implementation SLIM features state space search and an LTL model checker. Several variations and extensions of the SLIM have been developed, and all of them achieve their functionalities by modifying SLIM written in C. If a model checker is implemented in the modeling language itself, it should be easy to develop prototypes of various model checkers without changing the base implementation of the model checker. This approach is called metaprogramming which has been taken extensively in Lisp and Prolog communities. In this paper, we design a framework for implementing extendable model checkers. First, we define first-class rewrite rules to extend a mod- eling language. Second, we design an API to operate on the states of programs. These features enable programmers to handle state transition graphs as first-class objects and implement diverse variants of a model checker without changing SLIM. We demonstrate it by implementing an LTL model checker and its variant and a CTL model checker. Furthermore, we show how easy it is to extend these model checkers in our framework by extending the CTL model checker to handle fairness constraints. The over- head of metainterpretation is around an order of magnitude or less. All these results demonstrate the viability of the resulting framework based on meta-interpreters that handle explicit state space in a flexible manner.

    AB - LMNtal is a modeling language based on hierarchical graph rewriting, and its implementation SLIM features state space search and an LTL model checker. Several variations and extensions of the SLIM have been developed, and all of them achieve their functionalities by modifying SLIM written in C. If a model checker is implemented in the modeling language itself, it should be easy to develop prototypes of various model checkers without changing the base implementation of the model checker. This approach is called metaprogramming which has been taken extensively in Lisp and Prolog communities. In this paper, we design a framework for implementing extendable model checkers. First, we define first-class rewrite rules to extend a mod- eling language. Second, we design an API to operate on the states of programs. These features enable programmers to handle state transition graphs as first-class objects and implement diverse variants of a model checker without changing SLIM. We demonstrate it by implementing an LTL model checker and its variant and a CTL model checker. Furthermore, we show how easy it is to extend these model checkers in our framework by extending the CTL model checker to handle fairness constraints. The over- head of metainterpretation is around an order of magnitude or less. All these results demonstrate the viability of the resulting framework based on meta-interpreters that handle explicit state space in a flexible manner.

    KW - Graph rewriting

    KW - Meta-interpreters

    KW - Model checkers

    KW - State- space search

    UR - http://www.scopus.com/inward/record.url?scp=85058782573&partnerID=8YFLogxK

    UR - http://www.scopus.com/inward/citedby.url?scp=85058782573&partnerID=8YFLogxK

    U2 - 10.5381/jot.2018.17.1.a1

    DO - 10.5381/jot.2018.17.1.a1

    M3 - Article

    AN - SCOPUS:85058782573

    VL - 17

    JO - Journal of Object Technology

    JF - Journal of Object Technology

    SN - 1660-1769

    IS - 1

    ER -