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.


For more information on the VIATRA2 model transformation framework, we kindly refer the reader to the VIATRA portal, the official website, and the Eclipse Wiki.

A thematic list of VIATRA2-related publications is available here. A comprehensive list is available on the portal.


EMF-IncQuery is an Eclipse-based framework that supports high-performance incremental model queries over large instance models. Based on the incremental graph pattern matching engine, core model-driven engineering applications such as on-the-fly well-formedness validation, model synchronization and view maintenance can be easily implemented in an extremely scalable way. More information is available on the official website of the project.

CAV 2014 Measurements

↓ To the results ↓

On this page we provide all of our measurements comparing some state-of-the-art model checkers to our algorithm. The tools and algorithms included in the measurements are the following: Read more »

TACAS 2015

Detailed Measurement Results for TACAS 2015

↓ To the results ↓

On this page we detail our most recent measurement results comparing some state-of-the-art model checkers to our algorithm based on models of the Model Checking Contest. A total of 7850 measurements were done with 4 tools. We process the collected data continuously, so this page is updated from time to time to present more detailed plots and descriptions. Read more »

Models for the Petri Nets 2015 paper

Models for the Petri Nets 2015 paper

Ákos Hajdu, András Vörös, Tamás Bartha: New search strategies for the Petri net CEGAR approach

Distant invariant models

The reachability problem for each model is to produce a token in p0, while the marking of other places must be unchanged. Read more »