Non-reachability in Petri Nets with Delaying Places

The correctness of systems is frequently proved by demonstrating the non-reachability of certain (incorrect) states with the help of formal frameworks, e.g., Petri nets. Especially for real-time systems, the timely behavior has to be considered. Thus, there exist several extensions that allow the modeling of time in Petri nets. Non-reachability proofs in time-dependent Petri nets are usually done by proving the non-reachability within the time-less skeleton. However, in many cases this approach fails to prove non-reachability, since the skeleton can reach more markings than the timedependent Petri net. In this paper, we introduce a state equation for a class of time-augmented Petri nets and demonstrate in an example application how this state equation can be used to prove non-reachability within the actual timedependent net.