LoLA is a tool that can check whether a system (given as Petri net) satisfies a specified property. The property is evaluated by exhaustive and explicit exploration of a reduced state space. LoLA uses a broad range of state-of-the-art reduction techniques most of which can be applied jointly. Hence, LoLA typically needs to explore only a tiny fraction of the actual state space. The particularly strength of LoLA is the evaluation of simple properties such as deadlock freedom or reachability. Here, additional reduction techniques and specialized variants of techniques are applied.

Understand LoLA

LoLA is a pure verification tool. It is not designed for supporting modeling. However, the interface is made such that integration of LoLA into a modeling framework is very easy. Input and output is organized as data streams (which may be files). LoLA reads a Petri net from an ASCII file and gets a property from another file or as command line parameter. The property (given as a formula in CTL*) is analysed and deferred to a suitable anaylzing routine (a CTL model checker, an LTL model checker, a reachability checker, or a deadlock checker). CTL* formulas that are not in one of the mentioned fragments, cannot be analysed. LoLA then outputs whether or not the property holds. In some cases, it can additionally produce a witness or counterexample path. Application of reduction techniques can be controlled by command line parameters.
State space reduction technqiues in LoLA include

• a symmetry method where, in contrast to most other tools, symmetries are detected automatically such that they preserve the net staructure as well as the formula;
• a partial order reduction that, in contrast to many other tools, uses specific variants for simple properties such as deadlock or reachability checking;
• the sweep-line method where, in contrast to other tool, a suitable progress measure (which is a pre-requisite for this method) is automatically computed;
• Bloom filters (a reduction of states to hash values) where the number of involved hash functions can be controlled using a command line parameter;
• The coverability graph construction that can abstract infinite state spaces to a finite graph;
• Petri net specific preprocessing that accelerates some of the techniques.

Most techniques exploit the particular nature of Petri nets and therefore have the potential to outperform model checkers that work on general transition systems. LoLA has been successfully applied to systems in various domains, including

• hazard detection in real asynchronous circuits
• validation of a formal semantics of the WS-BPEL language
• verification of web service choreographies
• verification iof soundness of numerous business process models
• exploration of biochecmical reaction systems solving AI planning problems, e.g. for web service composition
• verification of several challenge problems

LoLA has participated several time in the model checking contest that takes place with the Petri Nets conferences and has shown competetive performance.

Get LoLA

LoLA can be downloaded from here.

Download includes a detailed user manual that describes both the installation procedure and the use of LoLA.