Skip to main content
SpringerLink
Log in

Hierarchical Graph Rewriting as a Unifying Tool for Analyzing and Understanding Nondeterministic Systems

  • Conference paper
Book cover Theoretical Aspects of Computing - ICTAC 2009 (ICTAC 2009)

Part of the book series: Lecture Notes in Computer Science ((LNTCS,volume 5684))

Included in the following conference series:

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.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Cervesato, I., et al.: A Meta-notation for Protocol Analysis. In: Proc. CSFW 1999, pp. 55–69. IEEE Computer Society, Los Alamitos (1999)

    Google Scholar 

  2. Holzmann, G.: The SPIN Model Checker. Addison-Wesley, Reading (2004)

    Google Scholar 

  3. Murayama, K., et al.: Implementation of the Hierarchical Graph Rewriting Language LMNtal. Computer Software 25(2), 47–77 (2008)

    Google Scholar 

  4. Ueda, K., Kato, N.: LMNtal: A Language Model with Links and Membranes. In: Mauri, G., Păun, G., Jesús Pérez-Jímenez, M., Rozenberg, G., Salomaa, A. (eds.) WMC 2004. LNCS, vol. 3365, pp. 110–125. Springer, Heidelberg (2005)

    Chapter  Google Scholar 

  5. Ueda, K.: Encoding Distributed Process Calculi into LMNtal. Electronic Notes in Theoretical Computer Science 209, 187–200 (2008)

    Article  MATH  Google Scholar 

  6. Ueda, K.: Encoding the Pure Lambda Calculus into Hierarchical Graph Rewriting. In: Voronkov, A. (ed.) RTA 2008. LNCS, vol. 5117, pp. 392–408. Springer, Heidelberg (2008)

    Chapter  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Dept. of Computer Science and Engineering, Waseda University, 3-4-1, Okubo, Shinjuku-ku, Tokyo, 169-8555, Japan

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

Authors
  1. Kazunori Ueda
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Takayuki Ayano
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Taisuke Hori
    View author publications

    You can also search for this author in PubMed Google Scholar

  4. Hiroki Iwasawa
    View author publications

    You can also search for this author in PubMed Google Scholar

  5. Seiji Ogawa
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Institut für Informatik, TU München, Boltzmannstr. 3, 85748, Garching, Germany

    Martin Leucker

  2. School of Computer Science and Engineering, University of New South Wales, Sydney, Australia

    Carroll Morgan

Rights and permissions

Reprints and permissions

Copyright information

© 2009 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

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: Leucker, M., Morgan, C. (eds) Theoretical Aspects of Computing - ICTAC 2009. ICTAC 2009. Lecture Notes in Computer Science, vol 5684. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-03466-4_24

Download citation

  • DOI: https://doi.org/10.1007/978-3-642-03466-4_24

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-642-03465-7

  • Online ISBN: 978-3-642-03466-4

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation