LTSmin: High-Performance Language-Independent Model Checking



Published in: TACAS 2015 pp 692–707

DOI: 10.1007/978-3-662-46681-0_61



In recent years, the LTSmin model checker has been extended with support for several new modelling languages, including probabilistic (Mapa) and timed systems (Uppaal). Also, connecting additional language front-ends or ad-hoc state-space generators to LTSmin was simplified using custom C-code. From symbolic and distributed reachability analysis and minimisation, LTSmin’s functionality has developed into a model checker with multi-core algorithms for on-the-fly LTL checking with partial-order reduction, and multi-core symbolic checking for the modal μ calculus, based on the multi-core decision diagram package Sylvan.

In LTSmin, the modelling languages and the model checking algorithms are connected through a Partitioned Next-State Interface (Pins), that allows to abstract away from language details in the implementation of the analysis algorithms and on-the-fly optimisations. In the current paper, we present an overview of the toolset and its recent changes, and we demonstrate its performance and versatility in two case studies.

BibTeX entry:

 author = {Gijs Kant and Alfons Laarman and Jeroen Meijer and Jaco van de Pol and Stefan Blom and Tom van Dijk},
 booktitle = {TACAS 2015},
 doi = {10.1007/978-3-662-46681-0_61},
 pages = {692--707},
 title = {{LTSmin: High-Performance Language-Independent Model Checking}},
 year = {2015}