Helena is an explicit state model checker. It is a free software available under the terms of the GNU general public license.
Helena works on a Linux platform. It is a command line oriented tool without graphical interface.

Features

• High level formalism
• Efficient firing rule
• Code generation to speed up the analysis
• Interface with C code
• Optimized state space storage method
• Structural abstractions techniques
• Partial order methods
• LTL model checking
• Interface with other Petri nets tools: Lola, Prod, Tina

Download links

• Current version:
  • 2.1: with binaries: 32 bits - 64 bits, without binaries
• Older versions:
  • 2.0: with binaries: 32 bits, without binaries
  • 1.5: with binaries: 32 bits, without binaries

Documentation

• The user's guide
• The syntax summary
• Example nets
  • The distributed database system
  • The load balancing system
  • The towers of Hanoi

Tools
Helena relies on several other tools/compilers. Among those:

• GNAT GPL to compile Ada code
• MLton to compile ML code
• ltl2ba to translate LTL formula to Buchi automata

Contact
Please send me an email if you have any question or wish to submit a bug report. You'll find my personal information here.