PetriDotNet is a framework for the editing, simulation and analysis of Petri nets. Our aim is an easy to use and extendable tool to support Petri net based modelling and verification. It provides a convenient graphical editor for creating (ordinary or coloured) Petri nets. It is extended with analysis of structural and dynamic properties of Petri nets, simulation, reachability and model checking capabilities. Furthermore, PetriDotNet is a simple, generic and extensible platform for new, Petri net-based algorithms that provides wide access to the Petri net data structures and the graphical user interface.

The framework is developed by the Fault Tolerant Systems Research Group at the Budapest University of Technology and Economics.

We are dealing with the following research directions:

  • 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,
  • Markovian stochastic analysis.


Case study

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


A large number of measurements and comparisons were done in our paper at TACAS 2015, these measurements are available here.

The synthetic models used in the paper presented at Petri nets 2015 are available here.

Models for the measurements of the stochastic analysis are available here.


The latest version of the tool and the algorithms can be downloaded:

The program requires Microsoft .NET 4.0 runtime environment.

Contact persons:

Technical support: <the name of the tool> at


Full list of publications

Main publications