LTSmin: Distributed and Symbolic Reachability


Share/Save/Bookmark

Blom, Stefan and Pol, Jaco van de 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 (pp. pp. 354-359).

[img] PDF (Publisher's version)
Restricted to UT campus only
: Request a copy
344kB
[img]
Preview
PDF (Author's version)
288kB
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
Additional information:See also Technical Report TR-CTIT-09-30 (http://eprints.eemcs.utwente.nl/15703/)
Copyright:© 2010 Springer
Faculty:
Electrical Engineering, Mathematics and Computer Science (EEMCS)
Research Group:
Link to this item:http://purl.utwente.nl/publications/72417
Official URL:http://dx.doi.org/10.1007/978-3-642-14295-6_31
Export this item as:BibTeX
EndNote
HTML Citation
Reference Manager

 

Repository Staff Only: item control page

Metis ID: 270917