LTSmin 3 released

by Jeroen Meijer, Aug. 7, 2018

LTSmin 3 released

With pleasure we announce the release of LTSmin 3. LTSmin is a language-independent model checking toolset that offers a wide spectrum of parallel and symbolic algorithms to deal with the state space explosion of different verification problems. Key features of LTSmin include:

  •  Symbolic CTL/mu-calculus model checking using different BDD/MDD packages, including the parallel BDD/MDD package Sylvan.
  •  Sequential and Multi-core LTL model checking with partial order reduction.
  •  Distributed LTS instantiation, export, and minimization modulo branching/strong bisimulation.
LTSmin allows developers to easily connect their own modeling language through its Partitioned Interface to the Next-State function (PINS). LTSmin currently supports ten modeling formalisms as front-ends. The front-ends are:
  • muCRL's process algebra,
  • mCRL2's process algebra,
  • DiVinE's DVE language,
  • builtin symbolic ETF format,
  • SPIN's Promela,
  • UPPAAL's timed automata,
  • SCOOP's process algebra for Markov Automata, and
  • POSIX'/UNIX' dlopen API.
The latest LTSmin version adds support for:
  • Petri nets (in PNML, and ANDL), and
  • B/Event-B/Z/TLA+ through ProB.

Other major new features are as follows:

  • Parallel symbolic checking of invariants and mu-calculus formulae.
  • Several bandwidth reduction algorithms have been implemented for static variable ordering.
  • LTSmin now integrates with Spot, which translates LTL formulae to Büchi automata.
  • A new parallel algorithm to detect strongly connected components, for LTL model checking.
  • Add support for transition-based generalized Büchi automata.
  • LTSmin now builds on Travis CI.
Please visit LTSmin's website at for pre-built binaries, and installation instructions. The web page shows detailed release notes. To stay up-to-date on LTSmin subscribe to our mailing list at [email protected]. For support, do not hesitate to send us an e-mail at [email protected].

We hope you enjoy the result of three years of hard work.

The LTSmin development team
University of Twente