On d-inversion in timed discrete event systems with interruption

We consider a timed discrete event system (DES) with interruption, modeled by an interruptive timed automaton. The system is observed via an observation scheme that consists of an event observation map and a state observation map. We define inversion as the process of extracting event lifetimes from the observations of the system trajectory. In this paper, we introduce the concept of d-invertibility for a single event, which corresponds to being able to extract every lifetime of the event from the observations of the previous transitions and at most d-additional transitions. We give a necessary and sufficient structural condition for d-invertibility for a single event