Modeling and analyzing place/transition nets (Petri nets)

Petri nets are a powerful formal model for describing the behavior of concurrent systems. It is often used as formal foundation for verifying the control flow of process models.The Academic Initiative includes Petri nets as a diagram type and offers various correctness criteria in order to identify well-behaving process models. Step-through simulation gives a hint about the control flow semantics.

A Petri net is "sound" if there are no deadlocks and no unreachable transitions. In workflow nets (having one input place and one output place), the net structure defines the initial and the final marking, which in turn are the basis for applying this classical notion of soundness. Weak soundness and relaxed soundness can also be checked by the tool.The implementation is based on a naive state space exploration. 

This is sufficient for examples with a small degree of concurrency. More advanced model checking techniques, such as LoLA (available on service-technology.org), allow for a more efficient verification of large state spaces.