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
336Kb

Preview

PDF (Author's version)
281Kb

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
Faculty:	Electrical Engineering, Mathematics and Computer Science (EEMCS)
Research Group:	Formal Methods and Tools (FMT)
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

Show download statistics for this publication

Repository Staff Only: item control page

Metis ID: 270917