
LTSmin: Distributed and Symbolic Reachability (tool paper accepted for publication to CAV 2010).
Abstract
In model checking, analysis algorithms are applied to large graphs (state spaces), which model the behavior of (computer) systems. These models are typically generated from specifications in high-level languages. The LTSmin toolset provides means to generate state spaces from high-level specifications, to check safety properties on-the-fly, to archive the resulting labelled transition systems (LTSs), and to minimize them with respect to (branching) bisimulation.
This is a tool paper; a companion technical report provides more
details on the methods (its sections on features and benchmarking are
by now outdated):
Stefan
Blom, Jaco van de
Pol and Michael
Weber. Bridging
the Gap between Enumerative and Symbolic Model Checkers,
Technical Report TR-CTIT-09-30, CTIT, University of Twente,
Enschede. (2009)