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

    120 Citations (Scopus)
    588 Downloads (Pure)

    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.
    Original languageEnglish
    Title of host publicationTools and Algorithms for the Construction and Analysis of Systems
    EditorsChristel Baier, Cesare Tinelli
    Place of PublicationLondon
    PublisherSpringer
    Pages692-707
    Number of pages16
    ISBN (Print)978-3-662-46680-3
    DOIs
    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
    Number9035
    Volume9035
    ISSN (Print)0302-9743
    ISSN (Electronic)1611-3349

    Conference

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

    Keywords

    • EWI-26128
    • FMT-MC: MODEL CHECKING
    • LTSMIN
    • Parallel
    • METIS-312662
    • high performance
    • IR-97118
    • Model Checking
    • Multi-Core
    • symbolic

    Fingerprint

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

    Cite this