Real-time property specific reduction for Time Petri Net

This paper presents a real-time property specific reduction approach for Time Petri Net (TPN). It divides TPN models into sub-nets of smaller size, and constructs an abstraction of reducible ones, which exhibits the same property specific behavior, but has less transitions and states. This directly reduces the amount of computation needed to generate the whole state space. This method adapts well to the verification of real-time properties in asynchronous systems. It should be possible to apply similar methods to other families of properties.