We have released version 1.5 of LTSmin. The following improvements have been implemented:

• New frontend DVE (requires DiVinE-cluster)
• Bignum support for state counts in spec-reach tools
  (Jeroen Ketema)
• spec-reach clean-up
• 'tree' vector set implementation based on AtermDD

The source code, installation instructions and manuals are available online:

LTSmin is currently being developed by the Formal Methods and Tools group at the University of Twente, The Netherlands.

The previous release was LTSmin 1.4.

We have released version 1.4 of LTSmin. The following improvements have been implemented:

• New tool ce-mpi for distributed cycle elimination (Simona Orzan)
• New tool ltsmin-tracepp for pretty-printing traces to deadlock states
• TorX support factored out into separate tools {lpo,lps,nips}2torx
• Enumerative DFS support
• Enumerative deadlock detection and trace output
• Reworked ETF support (non-backwards compatible)
• bash completion for LTSmin tools (see contrib/bash-completion/)

The source code, installation instructions and manuals are available online:

LTSmin is currently being developed by the Formal Methods and Tools group at the University of Twente, The Netherlands.

The previous release was LTSmin 1.3.

We have released version 1.3 of LTSmin. The following improvements have been implemented:

• Regrouping optimizations of the PINS matrix
• Connection to the CADP toolkit via pins_open
• Tuning of the BDD usage
• Significant performance improvements
• Symbolic deadlock detection and trace output

The source code, installation instructions and manuals are available online:

LTSmin is currently being developed by the Formal Methods and Tools group at the University of Twente, The Netherlands.

The previous release was LTSmin 1.2.

We have released version 1.2 of LTSmin. The following improvements have been implemented:

• Option parsing is now performed using the popt library. Thus, all long options now start with a double minus.
• Users can choose between BuDDy and ATermDD as the decision diagram library used in the symbolic tools.
• A new compressed file format for labeled transition systems with arbitrary numbers of state and edge labels has been implemented.
• The symbolic tools can write the results of the reachability analysis in the form of an ETF (Enumerated Table Format) file. This ETF file can be used as input for the reachabilty tools and can be directly translated to DVE.

The source code, installation instructions and manuals are available online:

LTSmin is currently being developed by the Formal Methods and Tools group at the University of Twente, The Netherlands.

The previous release was LTSmin 1.1.

A Database Approach to Distributed State Space Generation.

Abstract

We study distributed state-space generation on a cluster of workstations. It is explained why state-space partitioning by a global hash function is problematic when states contain variables from unbounded domains, such as lists or other recursive data types. Our solution is to introduce a database which maintains a global numbering of state values. We also describe tree compression, a technique of recursive state folding, and show that it is superior to manipulating plain state vectors. This solution is implemented and linked to the µCRL toolset, where state values are implemented as maximally shared terms (ATerms). However, it is applicable to other models as well, e.g. PROMELA or LOTOS models. Our experiments show the trade-offs between keeping the database global, replicated or local, depending on the available network bandwidth and latency.

This paper is a journal version of an earlier article. We explain tree compression in more detail and added more measurements.