LTSmin: Distributed and Symbolic Reachability
Blom, Stefan and Pol van de, Jaco and Weber, Michael (2010) LTSmin: Distributed and Symbolic Reachability. In: 22nd International Conference on Computer Aided Verification, CAV 2010, 15-19 July 2010, Edinburgh, UK.
|PDF (Publisher's version) |
Restricted to UT campus only: Request a copy
|PDF (Author's version)|
|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.
|Item Type:||Conference or Workshop Item|
|Copyright:||© 2010 Springer|
Electrical Engineering, Mathematics and Computer Science (EEMCS)
|Link to this item:||http://purl.utwente.nl/publications/72417|
|Export this item as:||BibTeX|
Daily downloads in the past month
Monthly downloads in the past 12 months
Repository Staff Only: item control page
Metis ID: 270917