Séminaire invité : Kazunori UEDA (Université de Waseda, Japon)

L’équipe TASC a le plaisir de recevoir le professeur Kazunori Ueda (Université de Waseda, Japon) au LS2N qui fera une présentation en anglais sur

« Analyzing and Understanding Nondeterministic Systems with LMNtal and LaViT »

jeudi 7 mars 2019 à 10h, en salle 3 au RDC du bâtiment 11, sur le site FST .

Abstract:
This talk is a gentle introduction to state-space search and model checking with LMNtal and LaViT, an IDE for LMNtal powered by visualizers.
LMNtal is a language model based on hierarchical graph rewriting that uses point-to-point links to represent connectivity and membranes to represent hierarchy. LMNtal was designed to be a substrate language of various computational models, especially those addressing concurrency, mobility and multiset rewriting. It has close connections with Colored Petri Nets, Interaction Nets, Chemical Abstract Machines, Constraint Handling Rules and Bigraphs. The expressive power of the language was demonstrated through the encoding of diverse computational models including the strong lambda calculus.
Our publicly available LMNtal implementation has evolved into a parallel LTL model checker. The strengths of our LMNtal model checker are its powerful data structures with an inherent symmetry reduction mechanism, highly nondeterministic computation it can express, and little discrepancy between programming and modeling languages. The
implementation achieved high scalability on shared-memory machines and enabled us to handle models with more than a billion states.
The visualizer of the LaViT IDE turned out to be extremely useful in understanding models by state space browsing, which is in sharp contrast with other black-box model checkers. The talk will be given with live demos of examples taken from the fields of model checking, concurrency and AI search.