LoLA: 1.17 - A Low Level Petri Net Analyser

LoLA is a tool that can verify a broad variety of behavioral properties on a
given Petri net. It is based on explicit state space verification, i.e. an
exhaustive enumeration of reachable state. LoLA gets its power from several
state-of-the-art state space reduction techniques. These techniques have the
effect that only a tiny portion of the overall state space is explored which,
however, behaves equivalently to the original state space with respect to the
investigated property.

LoLA has been implemented for the validation of reduction techniques for
place/transition net state spaces. Its particular strengths include:

- A large number of available state space reduction techniques many of which
  may be applied jointly;
- A high degree of automation for various state space reduction techniques
- Availability of dedicated variations of state space reduction techniques
  for several frequently used properties
- efficient implementation exploiting the particular nature of Petri net models
- simple textual interaction for easy integration into other tools