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 proceedingChapter

  • 38 Citations

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.
LanguageEnglish
Title of host publicationTools and Algorithms for the Construction and Analysis of Systems
EditorsChristel Baier, Cesare Tinelli
Place of PublicationLondon
PublisherSpringer Verlag
Pages692-707
Number of pages16
ISBN (Print)978-3-662-46680-3
DOIs
StatePublished - Apr 2015

Publication series

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

Fingerprint

Model checking
Interface states
Modeling languages

Keywords

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

Cite this

Kant, G., Laarman, A., Meijer, J., van de Pol, J. C., Blom, S., & van Dijk, T. (2015). LTSmin: High-Performance Language-Independent Model Checking. In C. Baier, & C. Tinelli (Eds.), Tools and Algorithms for the Construction and Analysis of Systems (pp. 692-707). (Lecture Notes in Computer Science; Vol. 9035, No. 9035). London: Springer Verlag. DOI: 10.1007/978-3-662-46681-0_61
Kant, Gijs ; Laarman, Alfons ; Meijer, Jeroen ; van de Pol, Jan Cornelis ; Blom, Stefan ; van Dijk, Tom. / LTSmin: High-Performance Language-Independent Model Checking. Tools and Algorithms for the Construction and Analysis of Systems. editor / Christel Baier ; Cesare Tinelli. London : Springer Verlag, 2015. pp. 692-707 (Lecture Notes in Computer Science; 9035).
@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’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",
year = "2015",
month = "4",
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 Verlag",
number = "9035",
pages = "692--707",
editor = "Christel Baier and Cesare Tinelli",
booktitle = "Tools and Algorithms for the Construction and Analysis of Systems",
address = "Germany",

}

Kant, G, Laarman, A, Meijer, J, van de Pol, JC, Blom, S & van Dijk, T 2015, LTSmin: High-Performance Language-Independent Model Checking. in C Baier & C Tinelli (eds), Tools and Algorithms for the Construction and Analysis of Systems. Lecture Notes in Computer Science, no. 9035, vol. 9035, Springer Verlag, London, pp. 692-707. DOI: 10.1007/978-3-662-46681-0_61

LTSmin: High-Performance Language-Independent Model Checking. / Kant, Gijs; Laarman, Alfons; Meijer, Jeroen; van de Pol, Jan Cornelis; Blom, Stefan; van Dijk, Tom.

Tools and Algorithms for the Construction and Analysis of Systems. ed. / Christel Baier; Cesare Tinelli. London : Springer Verlag, 2015. p. 692-707 (Lecture Notes in Computer Science; Vol. 9035, No. 9035).

Research output: Chapter in Book/Report/Conference proceedingChapter

TY - CHAP

T1 - LTSmin: High-Performance Language-Independent Model Checking

AU - Kant,Gijs

AU - Laarman,Alfons

AU - Meijer,Jeroen

AU - van de Pol,Jan Cornelis

AU - Blom,Stefan

AU - van Dijk,Tom

N1 - 10.1007/978-3-662-46681-0_61

PY - 2015/4

Y1 - 2015/4

N2 - 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.

AB - 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.

KW - EWI-26128

KW - FMT-MC: MODEL CHECKING

KW - LTSMIN

KW - Parallel

KW - METIS-312662

KW - high performance

KW - IR-97118

KW - Model Checking

KW - Multi-Core

KW - symbolic

U2 - 10.1007/978-3-662-46681-0_61

DO - 10.1007/978-3-662-46681-0_61

M3 - Chapter

SN - 978-3-662-46680-3

T3 - Lecture Notes in Computer Science

SP - 692

EP - 707

BT - Tools and Algorithms for the Construction and Analysis of Systems

PB - Springer Verlag

CY - London

ER -

Kant G, Laarman A, Meijer J, van de Pol JC, Blom S, van Dijk T. LTSmin: High-Performance Language-Independent Model Checking. In Baier C, Tinelli C, editors, Tools and Algorithms for the Construction and Analysis of Systems. London: Springer Verlag. 2015. p. 692-707. (Lecture Notes in Computer Science; 9035). Available from, DOI: 10.1007/978-3-662-46681-0_61