LTSmin: High-Performance Language-Independent Model Checking

Gijs Kant, Alfons Laarman, Jeroen Meijer, Jan Cornelis van de Pol, Stefan Blom, Tom van Dijk

    Research output: Chapter in Book/Report/Conference proceedingChapterAcademicpeer-review

    99 Citations (Scopus)
    376 Downloads (Pure)


    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.
    Original languageEnglish
    Title of host publicationTools and Algorithms for the Construction and Analysis of Systems
    EditorsChristel Baier, Cesare Tinelli
    Place of PublicationLondon
    Number of pages16
    ISBN (Print)978-3-662-46680-3
    Publication statusPublished - Apr 2015
    Event21st International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2015 - London, UK
    Duration: 11 Apr 201518 Apr 2015

    Publication series

    NameLecture Notes in Computer Science
    PublisherSpringer Verlag
    ISSN (Print)0302-9743
    ISSN (Electronic)1611-3349


    Conference21st International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2015
    Other11-18 April 2015


    • EWI-26128
    • LTSMIN
    • Parallel
    • METIS-312662
    • high performance
    • IR-97118
    • Model Checking
    • Multi-Core
    • symbolic


    Dive into the research topics of 'LTSmin: High-Performance Language-Independent Model Checking'. Together they form a unique fingerprint.

    Cite this