• Abstract
• Selected Case Studies
• Integration

LoLA - A Low Level Petri Net Analyser

Abstract

LoLA (a Low Level Petri Net Analyzer) 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

LoLA has been tested on several UNIX platforms (Solaris, SUN-OS, LINUX) as well as under WINDOWS using the CYGWIN environment.

Selected Case Studies

The following list gives a short summary of some case studies involving the use of LoLA.

  Verification of a GALS wrapper

  Validation of a Petri Net Semantics for WS-BPEL

  Verification of WS-BPEL choreographies

  Garavel's challenge in the Petri Net Mailing List

  Exploration of biochemical networks

Integration

LoLA has been integrated into various other tools.

  The Petri Net Kernel

  The Model Checking Kit

  CPN-AMI