LMNtal, a unifying language and model checking tools

LMNtal (pronounced "elemental") is a programming and modeling language based on hierarchical graph rewriting. It was designed to be a substrate language of diverse computational models, especially those addressing concurrency, mobility and multiset rewriting, including (Colored) Petri Nets, Interaction Nets, the Pi-Calculus, Chemical Abstract Machines, Constraint Handling Rules, and Bigraphs. It features

  • point-to-point links to represent connectivity,
  • membranes to represent hierarchy and locality, and
  • graphical view of programs and computation (see Figure below).

Our full-fledged implementation supports nondeterministic state-space search and LTL model checking as well as ordinary graph-rewriting execution, making it an expressive verification tool.

Various unique features have been integrated into LaViT (LMNtal Visual Tools), an integrated development environment of LMNtal, that supports graph visualizer and state-space visualizer that turns out to be very useful for understanding as well as debugging your models and programs.

Programming and modeling with links and membranes

The power of LMNtal comes from two structuring mechanisms,

  • links for expressing connectivity and
  • membranes for expressing hierarchy.

The figure below (click to enlarge) illustrates how hierarchical graphs allow you to represent various concepts appearing in computer science.

around

State-space search and model checking with LMNtal and LaViT

Our LMNtal implementation supports both ordinary execution (as a rule-based programming language) and state-space search (as a language for modeling and verification), and state-space search can further be combined with LTL model checking.

The LMNtal model checker is unique in three ways: (i) the modeling language itself, (ii) state-space visualization, and (iii) scalable parallel state-space construction.

Firstly, LMNtal allows extremely terse representation of some transition systems. For example, with only one rewrite rule, the state space of the Tower of Hanoi can be constructed and visualized (click the image to enlarge and view the program). This conciseness is thanks to the powerful symmetry reduction mechanism inherent in the hierarchical graph representation of states.

around

Secondly, LaViT's state-space visualizer demonstrates that it is extremely useful for understanding as well as debugging your models and programs. LaViT can be and has been used to run and visualize diverse examples taken from the fields of model checking, concurrency and AI search.

Thirdly, LMNtal's rich data structures are efficiently handled by our scalable parallel implementation, which can now handle a state space with >10^8 states on shared-memory machines with tens of cores.

Developers

The language and the implementation has been developed since 2002 by the LMNtal team, Dept. of Computer Science and Engineering, Waseda University.

mailto: lmntal _AtSign_ ueda.info.waseda.ac.jp


Copyright © 2004-2014, Ueda Laboratory LMNtal Group, All rights reserved.
Last-modified: Thu, 05 Jun 2014 10:22:55 JST (175d)