LTSmin: Distributed and Symbolic Reachability

Stefan Blom, Jan Cornelis van de Pol, M. Weber

Research output: Chapter in Book/Report/Conference proceedingConference contribution

  • 66 Citations

Abstract

The LTSMIN toolset provides a new level of modular design to high-performance model checkers. Its distinguishing feature is the wide spectrum of supported specification languages and model checking paradigms. On the language side, it supports process algebras (MCRL), state based languages (PROMELA, DVE) and even discrete abstractions of ODE models (MAPLE, GNA). On the algorithmic side (Sec. 3.2), it supports two main streams in high-performance model checking: reachability analysis based on BDDs (symbolic) and on a cluster of workstations (distributed, enumerative). LTSMIN also incorporates a distributed implementation of state space minimization, preserving strong or branching bisimulation.
LanguageUndefined
Title of host publicationComputer Aided Verification
EditorsT. Touili, B. Cook, P. Jackson
Place of PublicationBerlin
PublisherSpringer Verlag
Pages354-359
Number of pages6
ISBN (Print)978-3-642-14294-9
DOIs
StatePublished - 9 Jul 2010

Publication series

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

Keywords

  • METIS-270917
  • IR-72417
  • LTSMIN
  • Distributed model checking
  • CR-D.2.4
  • Symbolic model checking
  • FMT-MC: MODEL CHECKING
  • EWI-18152
  • EC Grant Agreement nr.: FP6/043235

Cite this

Blom, S., van de Pol, J. C., & Weber, M. (2010). LTSmin: Distributed and Symbolic Reachability. In T. Touili, B. Cook, & P. Jackson (Eds.), Computer Aided Verification (pp. 354-359). [10.1007/978-3-642-14295-6_31] (Lecture Notes in Computer Science; Vol. 6174). Berlin: Springer Verlag. DOI: 10.1007/978-3-642-14295-6_31
Blom, Stefan ; van de Pol, Jan Cornelis ; Weber, M./ LTSmin: Distributed and Symbolic Reachability. Computer Aided Verification. editor / T. Touili ; B. Cook ; P. Jackson. Berlin : Springer Verlag, 2010. pp. 354-359 (Lecture Notes in Computer Science).
@inproceedings{dac5adf9e90b4cb38e39bd80db1d9f2e,
title = "LTSmin: Distributed and Symbolic Reachability",
abstract = "The LTSMIN toolset provides a new level of modular design to high-performance model checkers. Its distinguishing feature is the wide spectrum of supported specification languages and model checking paradigms. On the language side, it supports process algebras (MCRL), state based languages (PROMELA, DVE) and even discrete abstractions of ODE models (MAPLE, GNA). On the algorithmic side (Sec. 3.2), it supports two main streams in high-performance model checking: reachability analysis based on BDDs (symbolic) and on a cluster of workstations (distributed, enumerative). LTSMIN also incorporates a distributed implementation of state space minimization, preserving strong or branching bisimulation.",
keywords = "METIS-270917, IR-72417, LTSMIN, Distributed model checking, CR-D.2.4, Symbolic model checking, FMT-MC: MODEL CHECKING, EWI-18152, EC Grant Agreement nr.: FP6/043235",
author = "Stefan Blom and {van de Pol}, {Jan Cornelis} and M. Weber",
note = "See also Technical Report TR-CTIT-09-30 (http://eprints.eemcs.utwente.nl/15703/).",
year = "2010",
month = "7",
day = "9",
doi = "10.1007/978-3-642-14295-6_31",
language = "Undefined",
isbn = "978-3-642-14294-9",
series = "Lecture Notes in Computer Science",
publisher = "Springer Verlag",
pages = "354--359",
editor = "T. Touili and B. Cook and P. Jackson",
booktitle = "Computer Aided Verification",
address = "Germany",

}

Blom, S, van de Pol, JC & Weber, M 2010, LTSmin: Distributed and Symbolic Reachability. in T Touili, B Cook & P Jackson (eds), Computer Aided Verification., 10.1007/978-3-642-14295-6_31, Lecture Notes in Computer Science, vol. 6174, Springer Verlag, Berlin, pp. 354-359. DOI: 10.1007/978-3-642-14295-6_31

LTSmin: Distributed and Symbolic Reachability. / Blom, Stefan; van de Pol, Jan Cornelis; Weber, M.

Computer Aided Verification. ed. / T. Touili; B. Cook; P. Jackson. Berlin : Springer Verlag, 2010. p. 354-359 10.1007/978-3-642-14295-6_31 (Lecture Notes in Computer Science; Vol. 6174).

Research output: Chapter in Book/Report/Conference proceedingConference contribution

TY - GEN

T1 - LTSmin: Distributed and Symbolic Reachability

AU - Blom,Stefan

AU - van de Pol,Jan Cornelis

AU - Weber,M.

N1 - See also Technical Report TR-CTIT-09-30 (http://eprints.eemcs.utwente.nl/15703/).

PY - 2010/7/9

Y1 - 2010/7/9

N2 - The LTSMIN toolset provides a new level of modular design to high-performance model checkers. Its distinguishing feature is the wide spectrum of supported specification languages and model checking paradigms. On the language side, it supports process algebras (MCRL), state based languages (PROMELA, DVE) and even discrete abstractions of ODE models (MAPLE, GNA). On the algorithmic side (Sec. 3.2), it supports two main streams in high-performance model checking: reachability analysis based on BDDs (symbolic) and on a cluster of workstations (distributed, enumerative). LTSMIN also incorporates a distributed implementation of state space minimization, preserving strong or branching bisimulation.

AB - The LTSMIN toolset provides a new level of modular design to high-performance model checkers. Its distinguishing feature is the wide spectrum of supported specification languages and model checking paradigms. On the language side, it supports process algebras (MCRL), state based languages (PROMELA, DVE) and even discrete abstractions of ODE models (MAPLE, GNA). On the algorithmic side (Sec. 3.2), it supports two main streams in high-performance model checking: reachability analysis based on BDDs (symbolic) and on a cluster of workstations (distributed, enumerative). LTSMIN also incorporates a distributed implementation of state space minimization, preserving strong or branching bisimulation.

KW - METIS-270917

KW - IR-72417

KW - LTSMIN

KW - Distributed model checking

KW - CR-D.2.4

KW - Symbolic model checking

KW - FMT-MC: MODEL CHECKING

KW - EWI-18152

KW - EC Grant Agreement nr.: FP6/043235

U2 - 10.1007/978-3-642-14295-6_31

DO - 10.1007/978-3-642-14295-6_31

M3 - Conference contribution

SN - 978-3-642-14294-9

T3 - Lecture Notes in Computer Science

SP - 354

EP - 359

BT - Computer Aided Verification

PB - Springer Verlag

CY - Berlin

ER -

Blom S, van de Pol JC, Weber M. LTSmin: Distributed and Symbolic Reachability. In Touili T, Cook B, Jackson P, editors, Computer Aided Verification. Berlin: Springer Verlag. 2010. p. 354-359. 10.1007/978-3-642-14295-6_31. (Lecture Notes in Computer Science). Available from, DOI: 10.1007/978-3-642-14295-6_31