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 algorithmrelies 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 10210 reachable states show that the proposed method can drastically reduce computational cost.

• Type: Conference
• Year: 1996
• Where: DAC
• Authors: Eric Verlind, Gjalt G. de Jong, Bill Lin
• Keywords: Computer Architecture, Concurrent Petri Nets, DAC 1996, Petri Nets, System's Reachable Behaviors