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 http://ltsmin.utwente.nl for pre-built binaries, and installation instructions. The web page http://ltsmin.utwente.nl/changelog.html 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