Efficient partial enumeration for timing analysis of asynchronous systems

This paper presents an efficient method for the timing verification of concurrent systems, modeled as labeled Timed Petri nets. The verification problems we consider require us to analyze the system´s reachable behaviors under the specified time delays. Our geometric timing analysis algorithm improves over existing ones by enumerating the state space only partially. The algorithm relies on a concept called pre-mature firing and a new, extended notion of clocks with a negative age. We have tested the fully automated procedure on a number of examples. Experimental results obtained on highly concurrent Petri nets with more than 6000 nodes and 10²¹⁰ reachable states show that the proposed method can drastically reduce computational cost