Model checking (model verification of) a Petri Net is a time-consuming task, if not impractical, due to the huge size of the state space (the so-called ‘state space explosion problem’). The Petri Net slicing has become active research to find various ways of reducing the size of the Petri Nets and therefore the resulting state space. The General-purpose Petri Net Simulator (GPenSIM). GPenSIM is a simulator for modeling, simulation, and performance analysis of discrete-event systems. GPenSIM is also used as a model-based controller.

Papers:

R. Davidrajuh. “Developing a Toolbox for Modeling and Simulation of Elevators”. In 2019 UKSim-AMSS 21st International Conference on Computer Modelling and Simulation (UKSim). IEEE.

U. Mutarraf, K. Barkaoui, Z. Li, N. Wu, and T. Qu. “Transformation of Business Process Model and Notation models onto Petri nets and their analysis.” Advances in Mechanical Engineering, 10(12), 2018. Doi: 1687814018808170.

General-purpose Petri Net Simulator (GPenSIM): http://www.davidrajuh.net/gpensim/ (2019).

R. Davidrajuh, Modeling Discrete-Event Systems with GPenSIM: An Introduction. Springer International Publishing. 2018.