Reduction Rules for Petri Net with Inhibitor Arcs Based Representation for Embedded Systems

Abstract

Petri-net-based Representation for Embedded Systems (PRES+) can describe embedded systems. To improve the modeling ability of PRES+, we add inhibitor arcs to the PRES+ model. Then, Petri net with Inhibitor arcs based Representation for Embedded Systems (PIRES+) is obtained. However, the state space explosion problem is a disadvantage for PIRES+’s ability to model and verify complex embedded systems. In order to solve this problem, reduction rules are proposed. Under certain conditions, these reduction rules preserve total-equivalence.