LTSmin: Distributed and Symbolic Reachability

ions 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. For end users, this implies that they can exploit other, scalable, verification algorithms than supported by their native tools, without changing specification language. Our experiments (Sec. 4) show that the LTSMIN toolset can match, and often outperform, existing tools tailored to their own specification language. From an algorithm engineering point of view, LTSMIN fosters the availability of benchmark suites across multiple specification languages and verification communities. This makes benchmarking studies more robust, by separating out language-specific issues, which is of separate scientific interest. The LTS...

• Type: Conference
• Year: 2010
• Where: CAV
• Authors: Stefan Blom, Jaco van de Pol, Michael Weber
• Keywords: CAV 2010, Hardware, LTSMIN Toolset, Model Checking, Specification Languages