• Abstract
• Selected Case Studies
• Integration

Garavel's Challenge in the Petri Net Mailing List

In 2003, H. Garavel posted a place/transition net to the Petri net mailing list. It consited of 485 places and 776 transitions. He was interested in quasi-liveness, i.e. the absence of any transition that is dead in the initial marking. According to the posting, the example stems from the translation of a LOTOS specification into Petri nets. There were four responses reporting successful verification. One of them involved LoLA. With LoLA, we checked each transition separately for non-death. We succeeded for all but two transitions. For the remaining transitions, goal-oriented execution confirmed non-death. According to the oather responses which involved either symbolic (BDD based) verification or the use of the covering step graph technqiue, the full state space consisted of almost 10^22 states.

More information:   The original posting
  The summary of responses

  Exploration of biochemical networks