LTSmin: Distributed and Symbolic Reachability

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

doi:10.1007/978-3-642-14295-6_31

LTSmin: Distributed and Symbolic Reachability

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

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › Academic › peer-review

83 Citations (Scopus)

353 Downloads (Pure)

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.

Original language	Undefined
Title of host publication	Computer Aided Verification
Editors	T. Touili, B. Cook, P. Jackson
Place of Publication	Berlin
Publisher	Springer
Pages	354-359
Number of pages	6
ISBN (Print)	978-3-642-14294-9
DOIs	https://doi.org/10.1007/978-3-642-14295-6_31
Publication status	Published - 9 Jul 2010
Event	Computer Aided Verification - Edinburgh Duration: 15 Jul 2010 → 19 Jul 2010

Publication series

Name	Lecture Notes in Computer Science
Publisher	Springer Verlag
Volume	6174
ISSN (Print)	0302-9743
ISSN (Electronic)	1611-3349

Conference

Conference	Computer Aided Verification
Period	15/07/10 → 19/07/10
Other	15-19 Jul 2010

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

Access to Document

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

http://eprints.eemcs.utwente.nl/secure2/18152/02/cav2010_BPW.pdf

Cite this

@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/).; Computer Aided Verification ; Conference date: 15-07-2010 Through 19-07-2010",

year = "2010",

month = jul,

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",

pages = "354--359",

editor = "T. Touili and B. Cook and P. Jackson",

booktitle = "Computer Aided Verification",

address = "Germany",

}

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, 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 proceeding › Conference contribution › Academic › peer-review

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

A2 - Touili, T.

A2 - Cook, B.

A2 - Jackson, P.

PB - Springer

CY - Berlin

T2 - Computer Aided Verification

Y2 - 15 July 2010 through 19 July 2010

ER -