PetriDotNet is a framework for the editing, simulation and analysis of Petri nets. The framework is developed by the Fault Tolerant Systems Research Group at the Budapest University of Technology and Economics.

Our aim is an easy to use and extendable tool to support Petri net based modelling and verification.

We have implemented and made available many advanced algorithms for the verification of Petri nets.

We are dealing with the following researches:

  • saturation based symbolic state space exploration and CTL model checking,
  • LTL model checking based on saturation,
  • verification of infinite state systems: CEGAR based Petri net reachability checking.


Case study

We used our tool for the verification of an industrial embedde safety-critical system. Further details can be found here.


The tool and the algorithms are under development, but the following versions can be dowloaded (we send other versions and the model checking moduls upon request):

The program requires .Net 4.0 runtime environment.

Contact persons:



Some of our main publications: