LoLA (a
Low
Level Petri Net
Analyzer)
has been implemented for the validation of reduction techniques for
place/transition net reachability graphs. LoLA features
symmetric as well as stubborn set based methods. Net symmetries are
automatically computed. Stubborn sets are customized to the particular
analysis task. LoLA can analyze reachability of a given state or state predicate,
boundedness
of the net or a place, deadlocks, dead transitions, reversibility, and existence of
home states. LoLA can verify formulas of a branching time logic.
Additionally, there is a memory-efficient semi-decision procedure
for the satisfiability of a given state predicate.
LoLA has been tested on several UNIX platforms (Solaris, SUN-OS, LINUX) as well
as under WINDOWS-NT using CYGNUS.
