A comparison between LTSmin and other model checkers

Introduction

This page compares the performance of DiVinE, SPIN and LTSmin.

Two sets of inputs are used: BEEM models and Promela case studies from inter alia the Promela Database.

The BEEM models were written in DVE format which can be directly parsed by DiVinE and LTSmin. A translation to Promela enables these models to be used in SPIN. However, the translation also introduces differences in the state and transition count rendering the performance results incomparable. Other models are simply too small to obtain measurable results. Therefore, the set of models can be limited to those of interest.

Step 1: Select Properties to Limit the Set of Models

Verification type:
Correct (only for LTL):
Minimum number of states:
Similar state count in SPIN (±10%):
Allow the selection of multiple models:

Step 2: Select a Model/Tool

Step 3: Copy or Bookmark the Link to the Current Selection

Copy this link to return to your current selection