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/9/28
Y1 - 2009/9/28
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
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 349
EP - 355
BT - Theoretical Aspects of Computing - ICTAC 2009 - 6th International Colloquium, Proceedings
T2 - 6th International Colloquium on Theoretical Aspects of Computing, ICTAC 2009
Y2 - 16 August 2009 through 20 August 2009
ER -