On the eventual invertibility of timed Petri nets

We view a Timed Petri Net (TPN) as an input-output system, where the input is a set of transition lifetimes and the output is the resulting system trajectory. We observe the output trajectory through an observation map. The trajectory is represented by a sequence of transitions, markings, and transition epochs. In a previous paper, we introduced the concept of “inversion” of TPNs, which is the process of extracting transition lifetimes from observation of a system trajectory, and investigated invertibility of TPNs. In this paper, we introduce the notion of “eventual inversion” of TPNs, which is less restrictive than inversion. We provide a necessary and sufficient condition for eventual invertibility of a TPN and an algorithm to check it from the coverability graph of the system