PETRI NETS 2011
ACSD 2011

Kanazawa, Japan, June 20-24, 2011

Full Day Tutorial: Veri cation with LoLA

Authors: Karsten Wolf and Niels Lohmann
Universität Rostock, Institut für Informatik, 18051 Rostock, Germany
http://wwwteo.informatik.uni-rostock.de/ls_tpp
firstname.lastname@uni-rostock.de

Abstract: LoLA is a tool that solves veri cation problems through the explicit construction of a reduced state space for a Petri net. During the last years, it has received increasing attention for solving real-world problems in various domains including work ow models, web service models, asynchronous circuits, biochemical systems, and parameterized boolean programs.
In the tutorial, we introduce the tool and its capabilities.We demonstrate how to use LoLA in serious case studies and how to integrate LoLA into modeling frameworks.

Objective: Participants understand the capabilities of LoLA and can assess the applicability of the tool in their context. They learn how to optimally exploit the available state space reduction techniques. They learn about several opportunities for linking LoLA to their problem domain and to their own tools.

More Information on Content: The home page of LoLA is http://wwwteo.informatik.uni-rostock.de/ls_tpp/lola/. Some of the intended content has been presented (in rather con-densed form) in Karsten Wolf. Generating Petri Net State Spaces. PETRI NETS 2007.

Tentative Outline: The program of this half-day tutorial is organized as follows.
  1. Opening and Introduction
    • Motivation, background and history
    • Preview and outline of the tutorial
    • Basic notions for state spaces: transition system, properties, search algorithms
    • First tool demo
  2. State space techniques available in LoLA and LoLA-speci c variations
    • Stubborn sets
    • Symmetries
    • Coverability graph
    • Sweep-line method
    • Incomplete state spaces (bit hashing, cycle coverage)
    • Tool demo showing impact of techniques and theor combinations
  3. The LoLA input language
    • Low Level net input
    • Verification task input
    • High-Level net input
    • Tool demo showing the capabilities of the input language
  4. Using LoLA
    • How to chose the optimal con guration for certain problem domains?
    • How to ask the right veri cation questions?
    • How to optimally model a Petri net?
    • How to employ scripts, make les, etc.?
    • How to manage several LoLA con gurations concurrently?
    • How to call LoLA from another tool?
    • Tool demo
  5. Case studies
    • Exploring Biochemical reaction chains
    • Searching hazards in GALS circuits
    • Verifying service choreographies
    • Verifying soundness in business process models
    • Solving AI planning problems
    • Verifying paraneterized boolean programs
  6. Integrating LoLA
    • as a plugin: ProM
    • as a service: Oryx
    • as a web page: service-technology.org/live
    • as a script: Model Checking Kit
    • via wrappers: PEP, CPN-AMI, Petri Net Kernel
  7. Implementation
    • Basic routines (firing, checking activation, backtracking)
    • search (DFS, BFS, detecting SCC and TSCC, fairness)
    • Organizing the set of known markings
    • Stubborn set generation
    • Symmetry organization
    • Sweep-line method organization and generation of a progress measure

Presenters:
Karsten Wolf is a full professor at the University of Rostock. He has imple- mented most of the LoLA code and presented several papers on the various reduction techniques in LoLA.

Niels Lohmann is a Postdoc in Karsten's group. He has been responsible for several case studies involving LoLA and for several integrations of LoLA into other tools.