Decidability Problems for Weak Time Petri Nets with Read, Reset and Transfer Arcs
摘要
We address the class of Time Petri Nets (TPNs) where time intervals are associated with transitions and constrain when those transitions can be fired. For TPN with strong semantics, i.e. where time elapsing cannot disable transitions, reachability, coverability and boundedness problems are undecidable. They are however decidable with the weak semantics in which time elapsing can disable transitions. We first propose an intermediate semantics allowing us to study the decidability border between weak and strong semantics. We prove that with only one transition in strong semantics, reachability, coverability and boundedness are undecidable. We then consider the so-called read, reset and transfer arcs for which the coverability problem is decidable in the untimed context and we study their impact on TPN with a weak semantics (weak TPN). We prove that coverability becomes undecidable for weak TPN when we add either 2 read arcs, or 2 reset arcs, or 2 transfer arcs. Lastly, considering bounded nets, we propose a state space computation algorithm for weak TPN with read, reset and transfer arcs that proves the decidability of the reachability problem.