LMNtal model checking using an integrated development environment

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

*Corresponding author for this work

Research output: Contribution to journalArticlepeer-review

1 Citation (Scopus)


LMNtal was designed and implemented as a unifying computational model based on hierarchical graph rewriting. In pursuit of its application to the fields of verification and search, the system has recently evolved into a model checker that employs LMNtal as a modeling language, and we have been accumulating experiences with modeling and verification. This paper describes LMNtalEditor, an integrated development environment (IDE) featuring both state space search and visualization of verification, and gives various examples of model description, verification and visualization. LMNtalEditor features the visualization and browsing of state space and counterexamples, the searching of states of interest, and so on. We have successfully run diverse examples taken from the fields including concurrency and AI search, and found that the IDE plays an essential role in understanding the models and counterexamples and thus greatly eases the task of verification. Furthermore, through the encoding of models in Promela, MSR and Coloured Petri Nets into LMNtal, we have extended the expressive power of LMNtal to the field of verification.

Original languageEnglish
Pages (from-to)197-214
Number of pages18
JournalComputer Software
Issue number4
Publication statusPublished - 2010 Dec 1

ASJC Scopus subject areas

  • Software


Dive into the research topics of 'LMNtal model checking using an integrated development environment'. Together they form a unique fingerprint.

Cite this