Hierarchical graph rewriting as a unifying tool for analyzing and understanding nondeterministic systems

Kazunori Ueda, Takayuki Ayano, Taisuke Hori, Hiroki Iwasawa, Seiji Ogawa

    Research output: Chapter in Book/Report/Conference proceedingConference contribution

    6 Citations (Scopus)

    Abstract

    We have designed and implemented LMNtal (pronounced "elemental"), a language based on hierarchical graph rewriting that allows us to encode diverse computational models involving concurrency, mobility and multiset rewriting. Towards its novel applications, the system has recently evolved into a model checker that employs LMNtal as the modeling language and PLTL as the specification language. The strengths of our LMNtal model checker are its powerful data structure, highly nondeterministic computation it can express, and virtually no discrepancy between programming and modeling languages. Models expressed in Promela, MSR, and Coloured Petri Nets can be easily encoded into LMNtal. The visualizer of the LMNtal IDE turned out to be extremely useful in understanding models by state space browsing. The LMNtal IDE has been used to run and visualize diverse examples taken from the fields of model checking, concurrency and AI search.

    Original languageEnglish
    Title of host publicationLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
    Pages349-355
    Number of pages7
    Volume5684 LNCS
    DOIs
    Publication statusPublished - 2009
    Event6th International Colloquium on Theoretical Aspects of Computing, ICTAC 2009 - Kuala Lumpur
    Duration: 2009 Aug 162009 Aug 20

    Publication series

    NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
    Volume5684 LNCS
    ISSN (Print)03029743
    ISSN (Electronic)16113349

    Other

    Other6th International Colloquium on Theoretical Aspects of Computing, ICTAC 2009
    CityKuala Lumpur
    Period09/8/1609/8/20

    Fingerprint

    Graph Rewriting
    Modeling Language
    Concurrency
    Colored Petri Nets
    Multiset
    Specification Languages
    Rewriting
    Browsing
    Model
    Specification languages
    Computational Model
    Model Checking
    Programming Languages
    Discrepancy
    Model checking
    Data Structures
    State Space
    Petri nets
    Express
    Computer programming languages

    ASJC Scopus subject areas

    • Computer Science(all)
    • Theoretical Computer Science

    Cite this

    Ueda, K., Ayano, T., Hori, T., Iwasawa, H., & Ogawa, S. (2009). Hierarchical graph rewriting as a unifying tool for analyzing and understanding nondeterministic systems. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 5684 LNCS, pp. 349-355). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 5684 LNCS). https://doi.org/10.1007/978-3-642-03466-4_24

    Hierarchical graph rewriting as a unifying tool for analyzing and understanding nondeterministic systems. / Ueda, Kazunori; Ayano, Takayuki; Hori, Taisuke; Iwasawa, Hiroki; Ogawa, Seiji.

    Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). Vol. 5684 LNCS 2009. p. 349-355 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 5684 LNCS).

    Research output: Chapter in Book/Report/Conference proceedingConference contribution

    Ueda, K, Ayano, T, Hori, T, Iwasawa, H & Ogawa, S 2009, Hierarchical graph rewriting as a unifying tool for analyzing and understanding nondeterministic systems. in Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). vol. 5684 LNCS, Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 5684 LNCS, pp. 349-355, 6th International Colloquium on Theoretical Aspects of Computing, ICTAC 2009, Kuala Lumpur, 09/8/16. https://doi.org/10.1007/978-3-642-03466-4_24
    Ueda K, Ayano T, Hori T, Iwasawa H, Ogawa S. Hierarchical graph rewriting as a unifying tool for analyzing and understanding nondeterministic systems. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). Vol. 5684 LNCS. 2009. p. 349-355. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). https://doi.org/10.1007/978-3-642-03466-4_24
    Ueda, Kazunori ; Ayano, Takayuki ; Hori, Taisuke ; Iwasawa, Hiroki ; Ogawa, Seiji. / Hierarchical graph rewriting as a unifying tool for analyzing and understanding nondeterministic systems. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). Vol. 5684 LNCS 2009. pp. 349-355 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).
    @inproceedings{9ba7fabdc7dc4211a9f20ddc2109686e,
    title = "Hierarchical graph rewriting as a unifying tool for analyzing and understanding nondeterministic systems",
    abstract = "We have designed and implemented LMNtal (pronounced {"}elemental{"}), a language based on hierarchical graph rewriting that allows us to encode diverse computational models involving concurrency, mobility and multiset rewriting. Towards its novel applications, the system has recently evolved into a model checker that employs LMNtal as the modeling language and PLTL as the specification language. The strengths of our LMNtal model checker are its powerful data structure, highly nondeterministic computation it can express, and virtually no discrepancy between programming and modeling languages. Models expressed in Promela, MSR, and Coloured Petri Nets can be easily encoded into LMNtal. The visualizer of the LMNtal IDE turned out to be extremely useful in understanding models by state space browsing. The LMNtal IDE has been used to run and visualize diverse examples taken from the fields of model checking, concurrency and AI search.",
    author = "Kazunori Ueda and Takayuki Ayano and Taisuke Hori and Hiroki Iwasawa and Seiji Ogawa",
    year = "2009",
    doi = "10.1007/978-3-642-03466-4_24",
    language = "English",
    isbn = "3642034659",
    volume = "5684 LNCS",
    series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
    pages = "349--355",
    booktitle = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",

    }

    TY - GEN

    T1 - Hierarchical graph rewriting as a unifying tool for analyzing and understanding nondeterministic systems

    AU - Ueda, Kazunori

    AU - Ayano, Takayuki

    AU - Hori, Taisuke

    AU - Iwasawa, Hiroki

    AU - Ogawa, Seiji

    PY - 2009

    Y1 - 2009

    N2 - We have designed and implemented LMNtal (pronounced "elemental"), a language based on hierarchical graph rewriting that allows us to encode diverse computational models involving concurrency, mobility and multiset rewriting. Towards its novel applications, the system has recently evolved into a model checker that employs LMNtal as the modeling language and PLTL as the specification language. The strengths of our LMNtal model checker are its powerful data structure, highly nondeterministic computation it can express, and virtually no discrepancy between programming and modeling languages. Models expressed in Promela, MSR, and Coloured Petri Nets can be easily encoded into LMNtal. The visualizer of the LMNtal IDE turned out to be extremely useful in understanding models by state space browsing. The LMNtal IDE has been used to run and visualize diverse examples taken from the fields of model checking, concurrency and AI search.

    AB - We have designed and implemented LMNtal (pronounced "elemental"), a language based on hierarchical graph rewriting that allows us to encode diverse computational models involving concurrency, mobility and multiset rewriting. Towards its novel applications, the system has recently evolved into a model checker that employs LMNtal as the modeling language and PLTL as the specification language. The strengths of our LMNtal model checker are its powerful data structure, highly nondeterministic computation it can express, and virtually no discrepancy between programming and modeling languages. Models expressed in Promela, MSR, and Coloured Petri Nets can be easily encoded into LMNtal. The visualizer of the LMNtal IDE turned out to be extremely useful in understanding models by state space browsing. The LMNtal IDE has been used to run and visualize diverse examples taken from the fields of model checking, concurrency and AI search.

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

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

    U2 - 10.1007/978-3-642-03466-4_24

    DO - 10.1007/978-3-642-03466-4_24

    M3 - Conference contribution

    AN - SCOPUS:70349319956

    SN - 3642034659

    SN - 9783642034657

    VL - 5684 LNCS

    T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

    SP - 349

    EP - 355

    BT - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

    ER -