Authors:
- Gijs Kant
- Alfons Laarman
- Jeroen Meijer
- Jaco van de Pol
- Stefan Blom
- Tom van Dijk
Published in: TACAS 2015 pp 692–707
DOI: 10.1007/978-3-662-46681-0_61
Abstract:
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:
@inproceedings{KantLMPBD15,
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}
}