*LMNtal, a unifying language and model checking tools [#nb83a963]

LMNtal (pronounced "elemental") is a concurrent language based on
hierarchical graph rewriting.  It features:
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

-rule-based multiset rewriting,
-connectivity represented using 1-to-1 links,
-hierarchy represented using membranes,
-locality of rewrite rules,
-dynamic process/rule migration,
-graphical view of programs and computation,
-uniform treatment of processes and data,
-and so on.
-point-to-point '''links''' to represent connectivity,
-'''membranes''' to represent hierarchy and locality, and
// -rule-based multiset rewriting,
// -locality of rewrite rules,
// -dynamic migration of processes and rewrite rules, and
-graphical view of programs and computation (see Figure below).
// -uniform treatment of processes and data,
// -and so on.

An implementation (a translator into intermediate code and
a runtime system) running on a Java platform is available.
It features 
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.

-nondeterministic execution (exhaustive search),
-foreign-language interface to Java,
-read-eval-print loop,
-redex/rule selection strategies, and
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.

The following figures illustrate some diagrams that can be
represented and handled nicely in LMNtal:
**Programming and modeling with links and membranes [#pa0251c2]

The power of LMNtal comes from two structuring mechanisms,
-links for expressing connectivity and
-membranes for expressing hierarchy.

The language and the implemenation has been developed since 2002 by
the LMNtal team, Dept. of Computer Science, Waseda University.
The figure below (click to enlarge) illustrates how hierarchical graphs allow you to represent various concepts appearing in computer science. 

// http://www.ueda.info.waseda.ac.jp/lmntal/image/diagrams-low.png

**State-space search and model checking with LMNtal and LaViT [#r9123801]

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.

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 more than a billion (10^9) states on shared-memory machines with tens of cores.

// An implementation (a translator into intermediate code and
// a runtime system) running on a Java platform is available.
// It features 

//-nondeterministic execution (exhaustive search),
//-foreign-language interface to Java,
//-read-eval-print loop,
//-redex/rule selection strategies, and

**Developers [#a4d9020a]

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

//**Sample Input 1
//    a,a,a,a,a,a, (a,a :- {a}), ({$p,a},{$q} :- $p,$q) 
//**Sample Input 2
//[[Download]] (append.lmn)

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

//--started to copy contents -- [[nakajima]] &new{2004-01-30 (Fri) 22:13:40};
//--edited the menubar to hide titles written in EUC-JP -- [[nakajima]] &new{2004-02-01 (Sun) 21:33:05};
//--added edit auth -- [[nakajima]] &new{2004-02-03 (Tue) 17:47:44};
//--new skin installed -- [[nakajima]] &new{2004-02-13 (Fri) 17:19:23};
-Hi, nice site!<a href="http://zovirax.medlp.com/">Zovirax</a><a href="fioricet.medlp.com">fioricet</a><a href="rogaine.medlp.com">rogaine</a><a href="valtrex.medlp.com">valtrex</a><a href="prescription.medlp.com">prescription</a><a href="prozac.medlp.com">prozac</a><a href="alprazolam.medlp.com">alprazolam</a><a href="http://phentermine1.za.pl">phentermine</a><a href="paxil.medlp.com">paxil</a><a href="http://adipex.medlp.com">Adipex</a><a href="http://xanax.medlp.com/">xanax</a><a href="http://sildenafil.medlp.com>sildenafil</a><a href="tramadol.medlp.com">tramadol</a><a href="http://gymboree.medlp.com/">gymboree</a><a href="prevacid.medlp.com">prevacid</a><a href="http://zyrtec.medlp.com/">Zyrtec</a><a href="http://viagra.medlp.com">Viagra</a><a href="http://ambien.medlp.com">http://ambien</a><a href="holdem.medlp.com">no limit texas holdem</a><a href="prilosec.medlp.com">prilosec</a><a href="vaniqa.medlp.com">vaniqa</a><a href="http://didrex.medlp.com">Didrex</a><a href="http://filenes.medlp.com/">filenes</a><a href="bvalium.medlp.com">buying valium online</a><a href="pharmacies.medlp.com">order from reliable foreign pharmacies</a><a href="http://zyban.medlp.com/">zyban</a><a href="http://sibutramine.medlp.com/">sibutramine</a><a href="renova.medlp.com">renova</a><a href="medicapharma.medlp.com">medicapharma  online pharmacy for all</a><a href="ultram.medlp.com">ultram</a><a href="http://valium.medlp.com/">valium</a><a href="pharmacy.medlp.com">usa pharmacy - online scripts - no fees</a> -- [[Nike]] &new{2006-05-14 (Sun) 00:33:43};
-TARRIFIC SITE!<a href='http://searchshopsite.info/casinos/casinos-in-washington.php'> casinos in washington</a><a href='http://searchshopsite.info/gaming/index.php'> index</a> -- [[Ahmed]] &new{2006-05-17 (Wed) 13:37:22};
-<a href='http://www.yahoo.com'></a>Welcome! http://www.dirare.com/India/ <a href='http://www.dirare.com'>business yellowpages</a>. <a href="http://www.dirare.com ">international directory</a>: About DIRare, Search in Business Category, Yellowpages search. Also [url]http://www.dirare.com/China/[/url] and [link=http://www.dirare.com]companies of the world[/link] from yellow pages . -- [[yellow pages main]] &new{2006-05-22 (Mon) 01:50:08};
-Welcome!!! http://www.dirare.com/Sweden/ online directory. [URL=http://www.dirare.com]YP national[/URL]: About DIRare, Search in Business Category, Yellowpages search. Also [url=http://www.dirare.com]global directory[/url] from online directory . -- [[online directory main]] &new{2006-05-22 (Mon) 01:50:11};
-hello! http://www.dirare.com/Sweden/ online directory. About DIRare, Search in Business Category, Yellowpages search. From online directory . -- [[online directory main]] &new{2006-05-22 (Mon) 01:50:11};


Front page List of pages Search Recent changes Backup   Help   RSS of recent changes