LTSmin: Distributed and Symbolic Reachability

9 years 8 months ago
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...
Stefan Blom, Jaco van de Pol, Michael Weber
Added 15 Aug 2010
Updated 15 Aug 2010
Type Conference
Year 2010
Where CAV
Authors Stefan Blom, Jaco van de Pol, Michael Weber
Comments (0)