Tapaal

TAPAAL is a tool for modelling, simulation, and verification of Timed-Arc Petri nets. The TAPAAL tool offers a graphical editor for drawing TAPN models, a simulator for experimenting with the designed nets, and a verification environment that automatically answers logical queries formulated in a subset of CTL logic (essentially EF, EG, AF, AG formulae without nesting).

It also allows the user to check whether a given net is k-bounded for a given number k. The newest version of TAPAAL is now equipped with three open-source verification engines distributed together with TAPAAL.