LTSmin: Distributed and Symbolic Reachability

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

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

    77 Citations (Scopus)
    114 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