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)