Symbolic Reachability Analysis of Integer Timed Petri Nets

Petri nets are an effective formalism to model discrete event systems, and several variants have been defined to explicitly include real time in the model. We consider two fundamental reachability problems for Timed Petri Nets with positive integer Firing times: timed reachability (find all markings where the model can be at a given finite time) and earliest reachability (find the minimum time when each reachable marking is entered). For these two problems, we define efficient symbolic algorithms that make use of both ordinary and edge-valued decision diagrams, and provide runtime results on an extensive suite of models.