@inbook{83c98fda17864851b7b0e95fb02f3ed4,
title = "LTSmin: High-Performance Language-Independent Model Checking",
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{\textquoteright}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.",
keywords = "EWI-26128, FMT-MC: MODEL CHECKING, LTSMIN, Parallel, METIS-312662, high performance, IR-97118, Model Checking, Multi-Core, symbolic",
author = "Gijs Kant and Alfons Laarman and Jeroen Meijer and {van de Pol}, {Jan Cornelis} and Stefan Blom and {van Dijk}, Tom",
note = "10.1007/978-3-662-46681-0_61 ; 21st International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2015 ; Conference date: 11-04-2015 Through 18-04-2015",
year = "2015",
month = apr,
doi = "10.1007/978-3-662-46681-0_61",
language = "English",
isbn = "978-3-662-46680-3",
series = "Lecture Notes in Computer Science",
publisher = "Springer",
number = "9035",
pages = "692--707",
editor = "Christel Baier and Cesare Tinelli",
booktitle = "Tools and Algorithms for the Construction and Analysis of Systems",
address = "Germany",
}