Modular Construction of Time Petri Nets Reachability Graph
Time Petri nets are an extension of Petri nets formalism with time specifications on transitions. The formalism is convenient to model distributed systems and enables capturing the time characteristics of distributed system activities. The primary tool for models behaviour understanding is the reachability graph of a time Petri net. In "Time Petri Nets" by Louchka Popova-Zeugmann, the algorithm for constructing time Petri net reachability graphs was suggested. It is based on the notion of essential states reduction, but the number of states in the resultant net reachability graph increases when time specification are scaled up; while the behaviour of the net is invariant under the time specification scaling. We study the modification of this algorithm that allows to build Time Petri nets reachability graphs more efficiently using common divisors of the time specification in hammock components of a Time Petri net.