HiPS: Hierarchical Petri Net design, simulation, verification and model checking tool

This paper introduces the Hierarchical Petri net Simulator (HiPS), which is a Petri net design tool implemented using C# and C++, the .NET Framework, and an interprocess communication channel. HiPS supports hierarchical modeling and can analyze the dynamic and structural properties of a Petri net by generating state spaces. The state space generation engine in HiPS provides a memory-saving technique and high-speed execution. We have also devised an extended coverability graph (ECG) mechanism to promote liveness and persistence properties in order to accurately maintain transition information. In this paper, we extend HiPS to include a liveness analyzer that utilizes the ECG mechanism and an on-the-fly model checker for event-based systems. We also describe an algorithm that generates state spaces by multithreading. Furthermore, we propose priority firing estimation with on-the-fly model checking for linear temporal logic.