In [AN01], one addresses the problem of analyzing systems modeled by (unbounded) Timed Petri Nets (TPNs) where each token is equipped with a real-valued clock representing the ``age'' of the token. Each arc in the net is provided with a subinterval of the natural numbers, restricting the ages of the tokens traveling the arc. The main idea consists of applying methodology which has been developed earlier based on the theory of better quasi orderings (BQOs), to derive an efficient constraint system for automatic verification of safety properties for TPNs. A prototype based on this method has been implemented and applied for verifying a parametrized version of Fischer's protocol.