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
----
[[ Petri Nets World: ]]
[[ http://www.informatik.uni-hamburg.de/TGI/PetriNets/ ]]
[[ Mailing list FAQ: ]]
[[ http://www.informatik.uni-hamburg.de/TGI/PetriNets/pnml/faq.html ]]
[[ Post messages/summary of replies: ]]
[[ [email protected] ]]
