LTSmin: Distributed and Symbolic Reachability

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

    Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

    74 Citations (Scopus)
    87 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 languageUndefined
    Title of host publicationComputer Aided Verification
    EditorsT. Touili, B. Cook, P. Jackson
    Place of PublicationBerlin
    PublisherSpringer
    Pages354-359
    Number of pages6
    ISBN (Print)978-3-642-14294-9
    DOIs
    Publication statusPublished - 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. https://doi.org/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, 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",
    pages = "354--359",
    editor = "T. Touili and B. Cook and P. Jackson",
    booktitle = "Computer Aided Verification",

    }

    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, Berlin, pp. 354-359. https://doi.org/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, 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 contributionAcademicpeer-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

    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. 2010. p. 354-359. 10.1007/978-3-642-14295-6_31. (Lecture Notes in Computer Science). https://doi.org/10.1007/978-3-642-14295-6_31