Tools

Workcraft - a framework for capturing, simulation, synthesis and verification of interpreted graph models (Finite State Machines, Petri nets, Signal Transition Graphs (STG), asynchronous digital circuits, etc.). It uses Unfolding Tools (see below) as back-ends.
Unfolding Tools - a suit of tools including PUNF, MPSAT, PCOMP and MP2DOT. They provide the verification and synthesis flows based on Petri net unfoldings and are used by Workcraft as back-ends.
FCP2PN - a tool implementing a polynomial translation of Finite Control Processes (an important subset of pi-calculus) to safe Petri nets. This allows for verification of systems with mobility using efficient techniques for Petri nets.
CLP - Linear programming model checker. It uses a finite complete prefix of a Petri net and can check deadlock freeness, reachability or coverability of a marking, or performs an extended reachability analysis, i.e. checks if there exists a marking satisfying the given predicate. You can use the PUNF tool from Unfolding Tools for generating a finite and complete prefix of a safe Petri net. CLP can be used both as a separate utility or as a part of the PEP tool. Note that Unfolding Tools provides another tool, MPSAT, which can check a significantly wider range of properties expressed in the REACH language.
WEASELOID - A simple tool demonstrating the detrimental impact of irreducible complexities on the performance of genetic algorithms.